From 6f0c0d92c3bfde521a06ee6fdec33c84a0f28e24 Mon Sep 17 00:00:00 2001 From: kishanps Date: Tue, 8 Aug 2023 14:58:00 -0700 Subject: [PATCH] [P4-Symbolic] Create symbolic variables and add constraints for symbolic table entries. --- p4_symbolic/ir/ir.proto | 3 + p4_symbolic/symbolic/symbolic.cc | 45 +++ p4_symbolic/symbolic/table_entry.cc | 368 ++++++++++++++++++ p4_symbolic/symbolic/table_entry.h | 24 ++ p4_symbolic/tests/BUILD.bazel | 28 ++ .../tests/symbolic_table_entries_test.cc | 112 ++++++ 6 files changed, 580 insertions(+) create mode 100644 p4_symbolic/tests/symbolic_table_entries_test.cc diff --git a/p4_symbolic/ir/ir.proto b/p4_symbolic/ir/ir.proto index 48c6fcb7..b95ee746 100644 --- a/p4_symbolic/ir/ir.proto +++ b/p4_symbolic/ir/ir.proto @@ -512,6 +512,9 @@ message SymbolicTableEntry { // https://p4.org/p4-spec/p4runtime/v1.3.0/P4Runtime-Spec.html#sec-match-format // - To specify a symbolic match, provide a concrete match name without any // values. + // - For the prefix lengths in symbolic LPM matches, any negative value + // denotes a symbolic prefix length and a non-negative value represents a + // concrete prefix length value. // - The `priority` must be concrete. It must be strictly positive if there // are range, ternary, or optional matches, and must be zero if there are // only LPM or exact matches. diff --git a/p4_symbolic/symbolic/symbolic.cc b/p4_symbolic/symbolic/symbolic.cc index a5082eba..fbcc00fd 100644 --- a/p4_symbolic/symbolic/symbolic.cc +++ b/p4_symbolic/symbolic/symbolic.cc @@ -23,13 +23,16 @@ #include #include "absl/cleanup/cleanup.h" +#include "absl/container/btree_map.h" #include "absl/status/status.h" #include "absl/status/statusor.h" +#include "absl/strings/string_view.h" #include "absl/types/optional.h" #include "glog/logging.h" #include "gutil/status.h" #include "p4/v1/p4runtime.pb.h" #include "p4_pdpi/internal/ordered_map.h" +#include "p4_pdpi/ir.pb.h" #include "p4_symbolic/ir/ir.h" #include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/ir/parser.h" @@ -46,6 +49,19 @@ namespace symbolic { namespace { +// Returns a pointer to the P4-Symbolic IR table with the given `table_name` +// from the `program` IR. The returned pointer would not be null when the status +// is ok. +absl::StatusOr GetIrTable(const ir::P4Program &program, + absl::string_view table_name) { + auto it = program.tables().find(table_name); + if (it == program.tables().end()) { + return gutil::NotFoundErrorBuilder() + << "Table '" << table_name << "' not found"; + } + return &it->second; +} + // Initializes the table entry objects in the symbolic context based on the // given `ir_entries`. For symbolic table entries, symbolic variables and their // corresponding constraints will be created within the given solver context. @@ -69,6 +85,35 @@ absl::Status InitializeTableEntries(SolverState &state, } } + // For each symbolic table entry object in each table, create respective + // symbolic variables and add corresponding constraints as Z3 assertions. + for (auto &[table_name, table_entries] : state.context.table_entries) { + ASSIGN_OR_RETURN(const ir::Table *table, + GetIrTable(state.program, table_name)); + + for (TableEntry &entry : table_entries) { + // Skip concrete table entries. + if (entry.IsConcrete()) continue; + + // Initialize the symbolic match fields of the current entry. + RETURN_IF_ERROR(InitializeSymbolicMatches( + entry, *table, state.program, *state.context.z3_context, + *state.solver, state.translator)); + + // Entries with symbolic action sets are not supported for now. + if (table->table_definition().has_action_profile_id()) { + return gutil::UnimplementedErrorBuilder() + << "Table entries with symbolic action sets are not supported " + "at the moment."; + } + + // Initialize the symbolic actions of the current entry. + RETURN_IF_ERROR(InitializeSymbolicActions( + entry, *table, state.program, *state.context.z3_context, + *state.solver, state.translator)); + } + } + return absl::OkStatus(); } diff --git a/p4_symbolic/symbolic/table_entry.cc b/p4_symbolic/symbolic/table_entry.cc index f186a541..da0adc57 100644 --- a/p4_symbolic/symbolic/table_entry.cc +++ b/p4_symbolic/symbolic/table_entry.cc @@ -20,16 +20,22 @@ #include #include +#include "absl/container/btree_map.h" #include "absl/container/flat_hash_map.h" +#include "absl/status/status.h" #include "absl/status/statusor.h" #include "absl/strings/str_cat.h" +#include "absl/strings/str_format.h" #include "absl/strings/string_view.h" +#include "gutil/collections.h" #include "gutil/status.h" #include "p4/config/v1/p4info.pb.h" #include "p4_pdpi/internal/ordered_map.h" #include "p4_pdpi/ir.pb.h" #include "p4_symbolic/ir/ir.pb.h" +#include "p4_symbolic/symbolic/operators.h" #include "p4_symbolic/symbolic/util.h" +#include "p4_symbolic/symbolic/values.h" #include "z3++.h" namespace p4_symbolic::symbolic { @@ -46,6 +52,285 @@ const absl::flat_hash_map match_type_to_str = { {MatchType::MatchField_MatchType_OPTIONAL, "optional"}, }; +// Translates the given `value` read from the `match` of an entry in the given +// `table` into a Z3 expression. +absl::StatusOr GetZ3Value(const pdpi::IrValue &value, + const p4::config::v1::MatchField &match, + const ir::Table &table, + z3::context &z3_context, + values::P4RuntimeTranslator &translator) { + const google::protobuf::Map + &match_name_to_field = table.table_implementation().match_name_to_field(); + const auto it = match_name_to_field.find(match.name()); + if (it == match_name_to_field.end()) { + return gutil::InvalidArgumentErrorBuilder() + << "Match key with name '" << match.name() + << "' was not found in implementation of table '" + << table.table_definition().preamble().name() << "'"; + } + const ir::FieldValue &matched_field = it->second; + std::string field_name = absl::StrFormat("%s.%s", matched_field.header_name(), + matched_field.field_name()); + return values::FormatP4RTValue(field_name, match.type_name().name(), value, + match.bitwidth(), z3_context, translator); +} + +// Adds constraints for the specific match types for encoding them as ternary +// values and masks. +absl::Status AddMatchTypeConstraintsForSymbolicMatch( + const SymbolicMatchVariables &variables, z3::context &z3_context, + z3::solver &solver) { + // Add type constraints on the symbolic match variables. + switch (variables.match_type) { + case p4::config::v1::MatchField::EXACT: { + // For exact matches, the mask bit-vector must be all-1s. + int bitwidth = variables.mask.get_sort().bv_size(); + z3::expr all_ones = z3_context.bv_val((1UL << bitwidth) - 1, bitwidth); + ASSIGN_OR_RETURN(z3::expr mask_constraint, + operators::Eq(variables.mask, all_ones)); + solver.add(mask_constraint); + break; + } + case p4::config::v1::MatchField::LPM: { + // For LPM matches, the mask bit-vector must comply with the LPM format. + // I.e. (~lpm_mask) & (~lpm_mask + 1) == 0 + int bitwidth = variables.mask.get_sort().bv_size(); + ASSIGN_OR_RETURN(z3::expr negated_mask, + operators::BitNeg(variables.mask)); + ASSIGN_OR_RETURN( + z3::expr negated_mask_plus_one, + operators::Plus(negated_mask, z3_context.bv_val(1, bitwidth))); + ASSIGN_OR_RETURN(z3::expr result, + operators::BitAnd(negated_mask, negated_mask_plus_one)); + ASSIGN_OR_RETURN(z3::expr mask_constraint, + operators::Eq(result, z3_context.bv_val(0, bitwidth))); + solver.add(mask_constraint); + break; + } + case p4::config::v1::MatchField::OPTIONAL: { + // For optional matches, the mask bit-vector must be either all-1s + // (present) or all-0s (don't-care). + int bitwidth = variables.mask.get_sort().bv_size(); + z3::expr all_ones = z3_context.bv_val((1UL << bitwidth) - 1, bitwidth); + z3::expr all_zeroes = z3_context.bv_val(0, bitwidth); + ASSIGN_OR_RETURN(z3::expr mask_is_all_ones, + operators::Eq(variables.mask, all_ones)); + ASSIGN_OR_RETURN(z3::expr mask_is_all_zeroes, + operators::Eq(variables.mask, all_zeroes)); + ASSIGN_OR_RETURN(z3::expr mask_constraint, + operators::Or(mask_is_all_ones, mask_is_all_zeroes)); + solver.add(mask_constraint); + break; + } + case p4::config::v1::MatchField::TERNARY: { + // No type constraint is required for ternary matches. + break; + } + default: { + return gutil::InvalidArgumentErrorBuilder() + << "Unsupported match type: " << variables.match_type + << ". Expected: EXACT, LPM, TERNARY, or OPTIONAL"; + } + } + + return absl::OkStatus(); +} + +// Adds canonicity constraints for P4Runtime updates. +// Since the P4Runtime API rejects entry updates where the non-masked bits are +// not zero, here we add the constraint to avoid synthesizing such entries. +// Namely, "(value & mask == value)". +absl::Status AddCanonicityConstraintForSymbolicMatch( + const SymbolicMatchVariables &variables, z3::solver &solver) { + ASSIGN_OR_RETURN(z3::expr masked_value, + operators::BitAnd(variables.value, variables.mask)); + ASSIGN_OR_RETURN(z3::expr constraint, + operators::Eq(masked_value, variables.value)); + solver.add(constraint); + return absl::OkStatus(); +} + +// Adds equality constraints on the given `variables` corresponding to the +// concrete parts of the given symbolic `ir_match` of a table entry in the given +// `table`. +absl::Status AddConstraintsForConcretePartsOfSymbolicMatch( + const SymbolicMatchVariables &variables, const pdpi::IrMatch &ir_match, + const ir::Table &table, z3::context &z3_context, z3::solver &solver, + values::P4RuntimeTranslator &translator) { + // If the symbolic variables are created successfully, it means that a + // match with the match name exists in the table definition, so no + // exception will be thrown here. + const p4::config::v1::MatchField &pi_match = table.table_definition() + .match_fields_by_name() + .at(ir_match.name()) + .match_field(); + + // Add equality constraints if a match value is set. + // If no concrete value is specified, no equality constraint is asserted. + if (ir_match.has_exact()) { + ASSIGN_OR_RETURN( + z3::expr concrete_exact_value, + GetZ3Value(ir_match.exact(), pi_match, table, z3_context, translator)); + ASSIGN_OR_RETURN(z3::expr constraint, + operators::Eq(variables.value, concrete_exact_value)); + solver.add(constraint); + } else if (ir_match.has_lpm()) { + if (ir_match.lpm().has_value()) { + ASSIGN_OR_RETURN(z3::expr concrete_lpm_value, + GetZ3Value(ir_match.lpm().value(), pi_match, table, + z3_context, translator)); + ASSIGN_OR_RETURN(z3::expr value_constraint, + operators::Eq(variables.value, concrete_lpm_value)); + solver.add(value_constraint); + } + if (ir_match.lpm().prefix_length() >= 0) { + int bitwidth = variables.value.get_sort().bv_size(); + int prefix_length = ir_match.lpm().prefix_length(); + if (prefix_length < 0 || prefix_length > bitwidth) { + return gutil::InvalidArgumentErrorBuilder() + << "Prefix length of match '" << ir_match.name() + << "' must fall in the range [0, " << bitwidth + << "]. Found: " << ir_match.DebugString(); + } + z3::expr ones = + z3_context.bv_val((1UL << prefix_length) - 1, prefix_length); + z3::expr zeroes = z3_context.bv_val(0, bitwidth - prefix_length); + z3::expr concrete_lpm_mask = z3::concat(ones, zeroes); + + // Constrain the symbolic variables of the LPM match to be equal to + // the specified concrete values. + ASSIGN_OR_RETURN(z3::expr mask_constraint, + operators::Eq(variables.mask, concrete_lpm_mask)); + solver.add(mask_constraint); + } + } else if (ir_match.has_ternary()) { + if (ir_match.ternary().has_value()) { + ASSIGN_OR_RETURN(z3::expr concrete_ternary_value, + GetZ3Value(ir_match.ternary().value(), pi_match, table, + z3_context, translator)); + ASSIGN_OR_RETURN(z3::expr value_constraint, + operators::Eq(variables.value, concrete_ternary_value)); + solver.add(value_constraint); + } + if (ir_match.ternary().has_mask()) { + ASSIGN_OR_RETURN(z3::expr concrete_ternary_mask, + GetZ3Value(ir_match.ternary().mask(), pi_match, table, + z3_context, translator)); + ASSIGN_OR_RETURN(z3::expr mask_constraint, + operators::Eq(variables.mask, concrete_ternary_mask)); + solver.add(mask_constraint); + } + } else if (ir_match.has_optional() && ir_match.optional().has_value()) { + ASSIGN_OR_RETURN(z3::expr concrete_optional_value, + GetZ3Value(ir_match.optional().value(), pi_match, table, + z3_context, translator)); + ASSIGN_OR_RETURN(z3::expr value_constraint, + operators::Eq(variables.value, concrete_optional_value)); + solver.add(value_constraint); + } + + return absl::OkStatus(); +} + +// Add constraints enforcing exactly one action to be chosen for a symbolic +// action, for entries in a direct match table. +void AddSingleActionChoiceConstraintForSymbolicAction( + const absl::btree_map &action_choices_by_name, + z3::context &z3_context, z3::solver &solver) { + z3::expr overall_constraint = z3_context.bool_val(false); + + for (const auto &[applied_action_name, applied_action] : + action_choices_by_name) { + z3::expr assignment_constraint = + (applied_action == z3_context.bool_val(true)); + + for (const auto &[action_name, action] : action_choices_by_name) { + if (action_name != applied_action_name) { + assignment_constraint = + (assignment_constraint && (action == z3_context.bool_val(false))); + } + } + + overall_constraint = overall_constraint || assignment_constraint; + } + + solver.add(overall_constraint); +} + +// Adds equality constraints to the solver according to the given `ir_action`. +absl::Status AddConstraintsForConcretePartsOfSymbolicAction( + const pdpi::IrActionInvocation &ir_action, + const absl::btree_map &action_invocations_by_name, + const absl::flat_hash_map> + &action_params_by_name, + const ir::P4Program &program, z3::context &z3_context, z3::solver &solver, + values::P4RuntimeTranslator &translator) { + // If the action name of the invocation is empty, it is treated as an + // unconstrained symbolic action. No constraint is asserted and no concrete + // parameters should be specified. + if (ir_action.name().empty()) { + if (!ir_action.params().empty()) { + return gutil::InvalidArgumentErrorBuilder() + << "Action parameters must not be specified in a fully " + "symbolic action. Found: " + << ir_action.DebugString(); + } + return absl::OkStatus(); + } + + // Check if the specified action name is valid. + if (!action_invocations_by_name.contains(ir_action.name()) || + !action_params_by_name.contains(ir_action.name())) { + return gutil::InvalidArgumentErrorBuilder() + << "Invalid action name: '" << ir_action.name() << "'"; + } + + // Check if the specified action parameter names are valid. + for (const auto ¶m : ir_action.params()) { + if (!action_params_by_name.at(ir_action.name()).contains(param.name())) { + return gutil::InvalidArgumentErrorBuilder() + << "Invalid action parameter name: '" << param.name() << "'"; + } + } + + // Constrain the symbolic action invocation with the specified action name to + // true and all other action invocations to false. + solver.add(action_invocations_by_name.at(ir_action.name()) == + z3_context.bool_val(true)); + + for (const auto &[action_name, action] : action_invocations_by_name) { + if (action_name != ir_action.name()) { + solver.add(action == z3_context.bool_val(false)); + } + } + + // Add equality constraints on the symbolic action parameters with the + // specified concrete parameter values. + for (const auto ¶m : ir_action.params()) { + z3::expr action_param = + action_params_by_name.at(ir_action.name()).at(param.name()); + ASSIGN_OR_RETURN(const pdpi::IrActionDefinition::IrActionParamDefinition + *param_definition, + gutil::FindPtrOrStatus(program.actions() + .at(ir_action.name()) + .action_definition() + .params_by_name(), + param.name())); + ASSIGN_OR_RETURN( + z3::expr concrete_param_value, + values::FormatP4RTValue( + /*field_name=*/"", param_definition->param().type_name().name(), + param.value(), param_definition->param().bitwidth(), z3_context, + translator)); + ASSIGN_OR_RETURN(z3::expr param_constraint, + operators::Eq(action_param, concrete_param_value)); + solver.add(param_constraint); + } + + return absl::OkStatus(); +} + } // namespace TableEntry::TableEntry(int index, ir::TableEntry ir_entry) @@ -373,4 +658,87 @@ absl::StatusOr CreateSymbolicIrTableEntry( return ir_entry; } +absl::Status InitializeSymbolicMatches( + const TableEntry &entry, const ir::Table &table, + const ir::P4Program &program, z3::context &z3_context, z3::solver &solver, + values::P4RuntimeTranslator &translator) { + for (const pdpi::IrMatch &match : entry.GetPdpiIrTableEntry().matches()) { + if (match.name().empty()) { + return gutil::InvalidArgumentErrorBuilder() + << "The match name must not be empty. Found: " + << match.DebugString(); + } + + // Create symbolic variables for the symbolic match. + ASSIGN_OR_RETURN( + SymbolicMatchVariables variables, + entry.GetMatchValues(match.name(), table, program, z3_context)); + // Add various constraints for the symbolic match. + RETURN_IF_ERROR( + AddMatchTypeConstraintsForSymbolicMatch(variables, z3_context, solver)); + RETURN_IF_ERROR(AddCanonicityConstraintForSymbolicMatch(variables, solver)); + RETURN_IF_ERROR(AddConstraintsForConcretePartsOfSymbolicMatch( + variables, match, table, z3_context, solver, translator)); + } + return absl::OkStatus(); +} + +absl::Status InitializeSymbolicActions( + const TableEntry &entry, const ir::Table &table, + const ir::P4Program &program, z3::context &z3_context, z3::solver &solver, + values::P4RuntimeTranslator &translator) { + absl::btree_map action_choices_by_name; + absl::flat_hash_map> + action_params_by_name; + + // Create symbolic variables for each valid action of the table. + for (const pdpi::IrActionReference &action_ref : + table.table_definition().entry_actions()) { + const std::string &action_name = action_ref.action().preamble().name(); + + // Check if the action referred by the table definition exists. + auto it = program.actions().find(action_name); + if (it == program.actions().end()) { + return gutil::NotFoundErrorBuilder() + << "Action not found: '" << action_name << "'"; + } + const ir::Action &action = it->second; + + // Create a symbolic variable for the action invocation. + ASSIGN_OR_RETURN(z3::expr action_invocation, + entry.GetActionInvocation(action_name, table, z3_context)); + action_choices_by_name.insert_or_assign(action_name, action_invocation); + + // Create a symbolic variable for each action parameter. + for (const auto &[param_name, param_definition] : + Ordered(action.action_definition().params_by_name())) { + ASSIGN_OR_RETURN( + z3::expr action_param, + entry.GetActionParameter(param_name, action, table, z3_context)); + action_params_by_name[action_name].insert_or_assign(param_name, + action_param); + } + } + + // Add well-formedness constraints for the symbolic actions of this entry. + AddSingleActionChoiceConstraintForSymbolicAction(action_choices_by_name, + z3_context, solver); + + // Add equality constraints for the symbolic actions if concrete values are + // specified. + const pdpi::IrTableEntry &ir_entry = entry.GetPdpiIrTableEntry(); + if (ir_entry.has_action()) { + RETURN_IF_ERROR(AddConstraintsForConcretePartsOfSymbolicAction( + ir_entry.action(), action_choices_by_name, action_params_by_name, + program, z3_context, solver, translator)); + } else if (ir_entry.has_action_set()) { + return gutil::InvalidArgumentErrorBuilder() + << "Action set should not be specified in a direct match table. " + "Found: " + << ir_entry.DebugString(); + } + + return absl::OkStatus(); +} + } // namespace p4_symbolic::symbolic diff --git a/p4_symbolic/symbolic/table_entry.h b/p4_symbolic/symbolic/table_entry.h index 4f5dd9ec..c90af2e4 100644 --- a/p4_symbolic/symbolic/table_entry.h +++ b/p4_symbolic/symbolic/table_entry.h @@ -21,11 +21,13 @@ #include #include "absl/container/btree_map.h" +#include "absl/status/status.h" #include "absl/status/statusor.h" #include "absl/strings/string_view.h" #include "p4/config/v1/p4info.pb.h" #include "p4_pdpi/ir.pb.h" #include "p4_symbolic/ir/ir.pb.h" +#include "p4_symbolic/symbolic/values.h" #include "z3++.h" namespace p4_symbolic::symbolic { @@ -139,6 +141,28 @@ absl::StatusOr CreateSymbolicIrTableEntry( const ir::Table &table, int priority = 0, std::optional prefix_length = std::nullopt); +// Creates symbolic variables and adds constraints for each field match of the +// given `entry` in the given `table`. We don't create symbolic variables for +// omitted matches as the omitted matches are treated as explicit wildcards +// based on the P4Runtime specification. If those symbolic variables are needed +// later, calling the `GetMatchValues` function will automatically create the +// corresponding variables for the entry match. +absl::Status InitializeSymbolicMatches(const TableEntry &entry, + const ir::Table &table, + const ir::P4Program &program, + z3::context &z3_context, + z3::solver &solver, + values::P4RuntimeTranslator &translator); + +// Creates symbolic variables and adds constraints for the given `entry`, for +// each action and each action parameter in the given `table`. +absl::Status InitializeSymbolicActions(const TableEntry &entry, + const ir::Table &table, + const ir::P4Program &program, + z3::context &z3_context, + z3::solver &solver, + values::P4RuntimeTranslator &translator); + } // namespace p4_symbolic::symbolic #endif // PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_ diff --git a/p4_symbolic/tests/BUILD.bazel b/p4_symbolic/tests/BUILD.bazel index 72ed6659..66f54d22 100644 --- a/p4_symbolic/tests/BUILD.bazel +++ b/p4_symbolic/tests/BUILD.bazel @@ -32,3 +32,31 @@ cc_test( "@com_google_googletest//:gtest_main", ], ) + +cc_test( + name = "symbolic_table_entries_test", + srcs = ["symbolic_table_entries_test.cc"], + data = [ + "//p4_symbolic/testdata:ipv4-routing/basic.config.json", + "//p4_symbolic/testdata:ipv4-routing/basic.p4info.pb.txt", + "//p4_symbolic/testdata:ipv4-routing/entries.pb.txt", + ], + deps = [ + "//gutil:status_matchers", + "//p4_symbolic:test_util", + "//p4_symbolic/ir", + "//p4_symbolic/ir:ir_cc_proto", + "//p4_symbolic/ir:parser", + "//p4_symbolic/ir:table_entries", + "//p4_symbolic/sai", + "//p4_symbolic/symbolic", + "//thinkit:bazel_test_environment", + "//thinkit:test_environment", + "@com_github_google_glog//:glog", + "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", + "@com_google_absl//absl/status", + "@com_google_absl//absl/strings", + "@com_google_absl//absl/time", + "@com_google_googletest//:gtest_main", + ], +) diff --git a/p4_symbolic/tests/symbolic_table_entries_test.cc b/p4_symbolic/tests/symbolic_table_entries_test.cc new file mode 100644 index 00000000..0af15f91 --- /dev/null +++ b/p4_symbolic/tests/symbolic_table_entries_test.cc @@ -0,0 +1,112 @@ +// Copyright 2024 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. + +#include +#include +#include + +#include "absl/status/status.h" +#include "absl/strings/string_view.h" +#include "absl/time/clock.h" +#include "absl/time/time.h" +#include "glog/logging.h" +#include "gmock/gmock.h" +#include "gtest/gtest.h" +#include "gutil/status_matchers.h" +#include "p4/v1/p4runtime.pb.h" +#include "p4_symbolic/ir/ir.h" +#include "p4_symbolic/ir/ir.pb.h" +#include "p4_symbolic/ir/parser.h" +#include "p4_symbolic/ir/table_entries.h" +#include "p4_symbolic/sai/sai.h" +#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/table_entry.h" +#include "p4_symbolic/symbolic/values.h" +#include "p4_symbolic/test_util.h" +#include "thinkit/bazel_test_environment.h" +#include "thinkit/test_environment.h" + +namespace p4_symbolic { +namespace { + +class SymbolicTableEntriesIPv4BasicTest : public testing::Test { + public: + thinkit::TestEnvironment& Environment() { return *environment_; } + + void SetUp() override { + constexpr absl::string_view bmv2_json_path = + "p4_symbolic/testdata/ipv4-routing/" + "basic.config.json"; + constexpr absl::string_view p4info_path = + "p4_symbolic/testdata/ipv4-routing/" + "basic.p4info.pb.txt"; + constexpr absl::string_view entries_path = + "p4_symbolic/testdata/ipv4-routing/" + "entries.pb.txt"; + ASSERT_OK_AND_ASSIGN( + p4::v1::ForwardingPipelineConfig config, + ParseToForwardingPipelineConfig(bmv2_json_path, p4info_path)); + ASSERT_OK_AND_ASSIGN( + std::vector pi_entries, + GetPiTableEntriesFromPiUpdatesProtoTextFile(entries_path)); + ASSERT_OK_AND_ASSIGN(ir::Dataplane dataplane, + ir::ParseToIr(config, pi_entries)); + program_ = std::move(dataplane.program); + ir_entries_ = std::move(dataplane.entries); + } + + protected: + std::unique_ptr environment_ = + std::make_unique( + /*mask_known_failures=*/true); + ir::P4Program program_; + ir::TableEntries ir_entries_; +}; + +TEST_F(SymbolicTableEntriesIPv4BasicTest, OneSymbolicEntryPerTable) { + constexpr int priority = 0; + constexpr int prefix_length = 16; + + // Create a symbolic IR entry for each table. + ir_entries_.clear(); + for (const auto& [table_name, table] : program_.tables()) { + ASSERT_OK_AND_ASSIGN( + ir::TableEntry ir_entry, + symbolic::CreateSymbolicIrTableEntry(table, priority, prefix_length)); + ir_entries_[table_name].push_back(std::move(ir_entry)); + } + + // Symbolically evaluate the program with symbolic table entries. + std::vector ports = {1, 2, 3, 4, 5}; + symbolic::TranslationPerType translations; + translations[p4_symbolic::kPortIdTypeName] = + symbolic::values::TranslationData{ + .static_mapping = {{"1", 1}, {"2", 2}, {"3", 3}, {"4", 4}, {"5", 5}}, + .dynamic_translation = false, + }; + translations[p4_symbolic::kVrfIdTypeName] = symbolic::values::TranslationData{ + .static_mapping = {{"", 0}}, + .dynamic_translation = true, + }; + LOG(INFO) << "Building model ..."; + absl::Time start_time = absl::Now(); + EXPECT_THAT( + symbolic::EvaluateP4Program(program_, ir_entries_, ports, translations), + gutil::StatusIs(absl::StatusCode::kUnimplemented, + "Symbolic entries are not supported at the moment.")); + LOG(INFO) << "-> done in " << (absl::Now() - start_time); +} + +} // namespace +} // namespace p4_symbolic