<commit_before>// Copyright 2020 Google LLC
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//      http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

// Contains functions used to symbolically evaluate P4 tables and their entries.
// A table is turned into a sequence of if-conditions (one per entry),
// each condition corresponds to having that entry matched on, and the
// corresponding then body invokes the appropriate symbolic action expression
// with the parameters specified in the entry.

#include "p4_symbolic/symbolic/table.h"

#include <algorithm>
#include <utility>

#include "absl/status/status.h"
#include "absl/strings/str_cat.h"
#include "p4_symbolic/symbolic/action.h"
#include "p4_symbolic/symbolic/operators.h"
#include "p4_symbolic/symbolic/util.h"
#include "z3++.h"

namespace p4_symbolic {
namespace symbolic {
namespace table {

namespace {

// Sort the given table entries by priority.
// Priority depends on the match types.
// If the matches contain one or more ternary matches, priority is the explicit
// numeric priority assigned to the the entry.
// If no ternary matches exist, and there is *exactly* one lpm match, priority
// is determined by the length of the prefix to match, such that longer
// prefixes have higher priority.
// Finally, if the matches only contain exact matches, there is no priority.
//
// The function returns a vector of pairs, where the second element
// is a table entry, and the first is its index in the old unsorted array.
// The pairs are sorted by priority, such that the element with highest priority
// appears first.
// Elements with equal priority maintaing their relative ordering.
//
// We return the old index so that Symbolic and Concrete TableMatches are
// set up against the indices as they appear in the input table entries array,
// and not the sorted array.
std::vector<std::pair<size_t, pdpi::IrTableEntry>> SortEntries(
    const ir::Table &table, const std::vector<pdpi::IrTableEntry> &entries) {
  // Find which *definition* of priority we should use by looking at the
  // table's match types.
  const pdpi::IrTableDefinition &table_definition = table.table_definition();
  bool has_ternary = false;
  bool has_lpm = false;
  int lpm_index = -1;
  for (const auto &[id, match_field_definition] :
       table_definition.match_fields_by_id()) {
    switch (match_field_definition.match_field().match_type()) {
      case p4::config::v1::MatchField::TERNARY: {
        has_ternary = true;
        break;
      }
      case p4::config::v1::MatchField::LPM: {
        has_lpm = true;
        // The match id starts from 1 (instead of zero).
        lpm_index = id - 1;
      }
      default: {
        // Exact or some other unsupported type, no need to do anything here.
        // An absl error will be returned if the type is unsupported in
        // "EvaluateSingleMatch".
        break;
      }
    }
  }

  // The output array.
  std::vector<std::pair<size_t, pdpi::IrTableEntry>> sorted_entries;
  for (size_t i = 0; i < entries.size(); i++) {
    const pdpi::IrTableEntry &entry = entries.at(i);
    sorted_entries.push_back(std::make_pair(i, entry));
  }

  // The sort comparator depends on the match types.
  std::function<bool(const std::pair<size_t, pdpi::IrTableEntry> &,
                     const std::pair<size_t, pdpi::IrTableEntry> &)>
      comparator;
  if (has_ternary) {
    // Sort by explicit priority.
    comparator = [](const std::pair<size_t, pdpi::IrTableEntry> &entry1,
                    const std::pair<size_t, pdpi::IrTableEntry> &entry2) {
      return entry1.second.priority() > entry2.second.priority();
    };
  } else if (has_lpm) {
    // Sort by prefix length.
    comparator = [lpm_index](
                     const std::pair<size_t, pdpi::IrTableEntry> &entry1,
                     const std::pair<size_t, pdpi::IrTableEntry> &entry2) {
      return entry1.second.matches(lpm_index).lpm().prefix_length() >
             entry2.second.matches(lpm_index).lpm().prefix_length();
    };
  } else {
    return sorted_entries;
  }

  // Using stable_sort, we preserve the relative order of entries with the same
  // priority.
  std::stable_sort(sorted_entries.begin(), sorted_entries.end(), comparator);
  return sorted_entries;
}

// Analyze a single match that is part of a table entry.
// Constructs a symbolic expression that semantically corresponds to this
// match.
gutil::StatusOr<z3::expr> EvaluateSingleMatch(
    p4::config::v1::MatchField match_definition,
    const z3::expr &field_expression, const pdpi::IrMatch &match) {
  if (match_definition.match_case() != p4::config::v1::MatchField::kMatchType) {
    // Arch-specific match type.
    return absl::InvalidArgumentError(
        absl::StrCat("Found match with non-standard type"));
  }

  switch (match_definition.match_type()) {
    case p4::config::v1::MatchField::EXACT: {
      if (match.match_value_case() != pdpi::IrMatch::kExact) {
        return absl::InvalidArgumentError(
            absl::StrCat("Match definition in table has type \"Exact\" but its "
                         "invocation in TableEntry has a different type ",
                         match_definition.DebugString()));
      }
      ASSIGN_OR_RETURN(z3::expr value_expression,
                       util::IrValueToZ3Expr(match.exact()));
      return operators::Eq(field_expression, value_expression);
    }

    case p4::config::v1::MatchField::LPM: {
      if (match.match_value_case() != pdpi::IrMatch::kLpm) {
        return absl::InvalidArgumentError(
            absl::StrCat("Match definition in table has type \"LPM\" but its "
                         "invocation in TableEntry has a different type ",
                         match_definition.DebugString()));
      }

      ASSIGN_OR_RETURN(z3::expr value_expression,
                       util::IrValueToZ3Expr(match.lpm().value()));
      return operators::PrefixEq(
          field_expression, value_expression,
          static_cast<unsigned int>(match.lpm().prefix_length()));
    }

    case p4::config::v1::MatchField::TERNARY: {
      if (match.match_value_case() != pdpi::IrMatch::kTernary) {
        return absl::InvalidArgumentError(
            absl::StrCat("Match definition in table has type \"TERNARY\" but "
                         "its invocation in TableEntry has a different type ",
                         match_definition.DebugString()));
      }

      ASSIGN_OR_RETURN(z3::expr mask_expression,
                       util::IrValueToZ3Expr(match.ternary().mask()));
      ASSIGN_OR_RETURN(z3::expr value_expression,
                       util::IrValueToZ3Expr(match.ternary().value()));
      ASSIGN_OR_RETURN(z3::expr masked_field,
                       operators::And(field_expression, mask_expression));
      return operators::Eq(masked_field, value_expression);
    }

    default:
      return absl::UnimplementedError(absl::StrCat(
          "Found unsupported match type ", match_definition.DebugString()));
  }
}

// Constructs a symbolic expression that is true if and only if this entry
// is matched on.
gutil::StatusOr<z3::expr> EvaluateTableEntryCondition(
    const ir::Table &table, const pdpi::IrTableEntry &entry,
    const SymbolicPerPacketState &state) {
  // Make sure number of match keys is the same in the table definition and<commit_msg>typo fix: use BitAnd instead of And in interpretation of Ternary field<commit_after>// Copyright 2020 Google LLC
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//      http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

// Contains functions used to symbolically evaluate P4 tables and their entries.
// A table is turned into a sequence of if-conditions (one per entry),
// each condition corresponds to having that entry matched on, and the
// corresponding then body invokes the appropriate symbolic action expression
// with the parameters specified in the entry.

#include "p4_symbolic/symbolic/table.h"

#include <algorithm>
#include <utility>

#include "absl/status/status.h"
#include "absl/strings/str_cat.h"
#include "p4_symbolic/symbolic/action.h"
#include "p4_symbolic/symbolic/operators.h"
#include "p4_symbolic/symbolic/util.h"
#include "z3++.h"

namespace p4_symbolic {
namespace symbolic {
namespace table {

namespace {

// Sort the given table entries by priority.
// Priority depends on the match types.
// If the matches contain one or more ternary matches, priority is the explicit
// numeric priority assigned to the the entry.
// If no ternary matches exist, and there is *exactly* one lpm match, priority
// is determined by the length of the prefix to match, such that longer
// prefixes have higher priority.
// Finally, if the matches only contain exact matches, there is no priority.
//
// The function returns a vector of pairs, where the second element
// is a table entry, and the first is its index in the old unsorted array.
// The pairs are sorted by priority, such that the element with highest priority
// appears first.
// Elements with equal priority maintaing their relative ordering.
//
// We return the old index so that Symbolic and Concrete TableMatches are
// set up against the indices as they appear in the input table entries array,
// and not the sorted array.
std::vector<std::pair<size_t, pdpi::IrTableEntry>> SortEntries(
    const ir::Table &table, const std::vector<pdpi::IrTableEntry> &entries) {
  // Find which *definition* of priority we should use by looking at the
  // table's match types.
  const pdpi::IrTableDefinition &table_definition = table.table_definition();
  bool has_ternary = false;
  bool has_lpm = false;
  int lpm_index = -1;
  for (const auto &[id, match_field_definition] :
       table_definition.match_fields_by_id()) {
    switch (match_field_definition.match_field().match_type()) {
      case p4::config::v1::MatchField::TERNARY: {
        has_ternary = true;
        break;
      }
      case p4::config::v1::MatchField::LPM: {
        has_lpm = true;
        // The match id starts from 1 (instead of zero).
        lpm_index = id - 1;
      }
      default: {
        // Exact or some other unsupported type, no need to do anything here.
        // An absl error will be returned if the type is unsupported in
        // "EvaluateSingleMatch".
        break;
      }
    }
  }

  // The output array.
  std::vector<std::pair<size_t, pdpi::IrTableEntry>> sorted_entries;
  for (size_t i = 0; i < entries.size(); i++) {
    const pdpi::IrTableEntry &entry = entries.at(i);
    sorted_entries.push_back(std::make_pair(i, entry));
  }

  // The sort comparator depends on the match types.
  std::function<bool(const std::pair<size_t, pdpi::IrTableEntry> &,
                     const std::pair<size_t, pdpi::IrTableEntry> &)>
      comparator;
  if (has_ternary) {
    // Sort by explicit priority.
    comparator = [](const std::pair<size_t, pdpi::IrTableEntry> &entry1,
                    const std::pair<size_t, pdpi::IrTableEntry> &entry2) {
      return entry1.second.priority() > entry2.second.priority();
    };
  } else if (has_lpm) {
    // Sort by prefix length.
    comparator = [lpm_index](
                     const std::pair<size_t, pdpi::IrTableEntry> &entry1,
                     const std::pair<size_t, pdpi::IrTableEntry> &entry2) {
      return entry1.second.matches(lpm_index).lpm().prefix_length() >
             entry2.second.matches(lpm_index).lpm().prefix_length();
    };
  } else {
    return sorted_entries;
  }

  // Using stable_sort, we preserve the relative order of entries with the same
  // priority.
  std::stable_sort(sorted_entries.begin(), sorted_entries.end(), comparator);
  return sorted_entries;
}

// Analyze a single match that is part of a table entry.
// Constructs a symbolic expression that semantically corresponds to this
// match.
gutil::StatusOr<z3::expr> EvaluateSingleMatch(
    p4::config::v1::MatchField match_definition,
    const z3::expr &field_expression, const pdpi::IrMatch &match) {
  if (match_definition.match_case() != p4::config::v1::MatchField::kMatchType) {
    // Arch-specific match type.
    return absl::InvalidArgumentError(
        absl::StrCat("Found match with non-standard type"));
  }

  switch (match_definition.match_type()) {
    case p4::config::v1::MatchField::EXACT: {
      if (match.match_value_case() != pdpi::IrMatch::kExact) {
        return absl::InvalidArgumentError(
            absl::StrCat("Match definition in table has type \"Exact\" but its "
                         "invocation in TableEntry has a different type ",
                         match_definition.DebugString()));
      }
      ASSIGN_OR_RETURN(z3::expr value_expression,
                       util::IrValueToZ3Expr(match.exact()));
      return operators::Eq(field_expression, value_expression);
    }

    case p4::config::v1::MatchField::LPM: {
      if (match.match_value_case() != pdpi::IrMatch::kLpm) {
        return absl::InvalidArgumentError(
            absl::StrCat("Match definition in table has type \"LPM\" but its "
                         "invocation in TableEntry has a different type ",
                         match_definition.DebugString()));
      }

      ASSIGN_OR_RETURN(z3::expr value_expression,
                       util::IrValueToZ3Expr(match.lpm().value()));
      return operators::PrefixEq(
          field_expression, value_expression,
          static_cast<unsigned int>(match.lpm().prefix_length()));
    }

    case p4::config::v1::MatchField::TERNARY: {
      if (match.match_value_case() != pdpi::IrMatch::kTernary) {
        return absl::InvalidArgumentError(
            absl::StrCat("Match definition in table has type \"TERNARY\" but "
                         "its invocation in TableEntry has a different type ",
                         match_definition.DebugString()));
      }

      ASSIGN_OR_RETURN(z3::expr mask_expression,
                       util::IrValueToZ3Expr(match.ternary().mask()));
      ASSIGN_OR_RETURN(z3::expr value_expression,
                       util::IrValueToZ3Expr(match.ternary().value()));
      ASSIGN_OR_RETURN(z3::expr masked_field,
                       operators::BitAnd(field_expression, mask_expression));
      return operators::Eq(masked_field, value_expression);
    }

    default:
      return absl::UnimplementedError(absl::StrCat(
          "Found unsupported match type ", match_definition.DebugString()));
  }
}

// Constructs a symbolic expression that is true if and only if this entry
// is matched on.
gutil::StatusOr<z3::expr> EvaluateTableEntryCondition(
    const ir::Table &table, const pdpi::IrTableEntry &entry,
    const SymbolicPerPacketState &state) {
  // Make sure number of match keys is the same in the table definition and
{'fraction_non_alphanumeric': 0.1076735844222393, 'fraction_numerical': 0.006789648987957981, 'mean_word_length': 3.1022070415133998, 'pattern_counts': {'":': 0, '<': 39, '<?xml version=': 0, '>': 41, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3370867', 'n_tokens_mistral': 4494, 'n_tokens_neox': 4415, 'n_words': 1398}