diff --git a/p4_constraints/backend/BUILD.bazel b/p4_constraints/backend/BUILD.bazel index 84cdf9b..445dd06 100644 --- a/p4_constraints/backend/BUILD.bazel +++ b/p4_constraints/backend/BUILD.bazel @@ -164,6 +164,8 @@ cc_library( "//p4_constraints:ast", "//p4_constraints:ast_cc_proto", "//p4_constraints:constraint_source", + "//p4_constraints/frontend:constraint_kind", + "//p4_constraints/frontend:parser", "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", "@com_github_z3prover_z3//:api", "@com_google_absl//absl/container:flat_hash_map", diff --git a/p4_constraints/backend/symbolic_interpreter.cc b/p4_constraints/backend/symbolic_interpreter.cc index 34477b9..96e8403 100644 --- a/p4_constraints/backend/symbolic_interpreter.cc +++ b/p4_constraints/backend/symbolic_interpreter.cc @@ -41,7 +41,10 @@ #include "p4_constraints/ast.pb.h" #include "p4_constraints/backend/constraint_info.h" #include "p4_constraints/backend/errors.h" +#include "p4_constraints/backend/type_checker.h" #include "p4_constraints/constraint_source.h" +#include "p4_constraints/frontend/constraint_kind.h" +#include "p4_constraints/frontend/parser.h" #include "z3++.h" namespace p4_constraints { @@ -676,22 +679,24 @@ absl::StatusOr EvaluateConstraintSymbolically( } // namespace internal_interpreter -absl::StatusOr ConcretizeEntry( - const z3::model& model, const TableInfo& table_info, - const SymbolicEnvironment& environment, - std::function(absl::string_view key_name)> - skip_key_named) { +absl::StatusOr ConstraintSolver::ConcretizeEntry() { + if (solver_.check() != z3::sat) { + return gutils::InternalErrorBuilder(GUTILS_LOC) + << "Constraints are not satisfiable."; + } + + z3::model model = solver_.get_model(); p4::v1::TableEntry table_entry; - table_entry.set_table_id(table_info.id); + table_entry.set_table_id(table_info_.id); // Construct match fields by evaluating their respective entries in the model. - for (const auto& [key_name, key_info] : table_info.keys_by_name) { - ASSIGN_OR_RETURN(bool key_should_be_skipped, skip_key_named(key_name)); + for (const auto& [key_name, key_info] : table_info_.keys_by_name) { + ASSIGN_OR_RETURN(bool key_should_be_skipped, skip_key_named_(key_name)); if (key_should_be_skipped) continue; ASSIGN_OR_RETURN( const SymbolicKey* symbolic_key, - gutils::FindPtrOrStatus(environment.symbolic_key_by_name, key_name)); + gutils::FindPtrOrStatus(environment_.symbolic_key_by_name, key_name)); ASSIGN_OR_RETURN(std::optional match, ConcretizeKey(*symbolic_key, key_info, model)); @@ -703,7 +708,7 @@ absl::StatusOr ConcretizeEntry( // Set priority if it exists. if (auto priority_key = - gutils::FindPtrOrStatus(environment.symbolic_attribute_by_name, + gutils::FindPtrOrStatus(environment_.symbolic_attribute_by_name, kSymbolicPriorityAttributeName); priority_key.ok()) { if (model.has_interp((*priority_key)->value.decl())) { @@ -720,12 +725,53 @@ absl::StatusOr ConcretizeEntry( return table_entry; } -absl::StatusOr EncodeValidTableEntryInZ3( - const TableInfo& table, z3::solver& solver, +absl::StatusOr ConstraintSolver::AddConstraint( + const ast::Expression& constraint, + const ConstraintSource& constraint_source) { + if (solver_.check() != z3::sat) { + return gutils::InternalErrorBuilder(GUTILS_LOC) + << "Stored constraints are unsatisfiable. Constraint solver must " + "hold a satisfiable constraint at all times."; + }; + + ASSIGN_OR_RETURN(z3::expr z3_constraint, + internal_interpreter::EvaluateConstraintSymbolically( + constraint, constraint_source, environment_, solver_)); + solver_.push(); + solver_.add(z3_constraint); + if (solver_.check() != z3::sat) { + solver_.pop(); + return false; + } + return true; +}; + +absl::StatusOr ConstraintSolver::AddConstraint( + absl::string_view constraint_string) { + ast::SourceLocation source_location; + source_location.set_table_name(table_info_.name); + + ConstraintSource constraint_source{ + .constraint_string = std::string(constraint_string), + .constraint_location = source_location, + }; + + ASSIGN_OR_RETURN( + ast::Expression constraint_ast, + ParseConstraint(ConstraintKind::kTableConstraint, constraint_source)); + + RETURN_IF_ERROR(InferAndCheckTypes(&constraint_ast, table_info_)); + + return ConstraintSolver::AddConstraint(constraint_ast, constraint_source); +} + +absl::StatusOr ConstraintSolver::Create( + const TableInfo& table, std::function(absl::string_view key_name)> skip_key_named) { - SymbolicEnvironment environment; - environment.symbolic_key_by_name.reserve(table.keys_by_name.size()); + ConstraintSolver constraint_solver = ConstraintSolver(); + constraint_solver.table_info_ = std::move(table); + constraint_solver.skip_key_named_ = std::move(skip_key_named); // Add keys to solver and map and determine whether the table needs a // priority. @@ -736,31 +782,37 @@ absl::StatusOr EncodeValidTableEntryInZ3( // for their entries. requires_priority = true; } - ASSIGN_OR_RETURN(bool key_should_be_skipped, skip_key_named(key_name)); + ASSIGN_OR_RETURN(bool key_should_be_skipped, + constraint_solver.skip_key_named_(key_name)); if (key_should_be_skipped) continue; - ASSIGN_OR_RETURN(SymbolicKey key, - internal_interpreter::AddSymbolicKey(key_info, solver)); - environment.symbolic_key_by_name.insert({key_name, std::move(key)}); + ASSIGN_OR_RETURN(SymbolicKey key, internal_interpreter::AddSymbolicKey( + key_info, constraint_solver.solver_)); + constraint_solver.environment_.symbolic_key_by_name.insert( + {key_name, std::move(key)}); } if (requires_priority) { SymbolicAttribute priority = - internal_interpreter::AddSymbolicPriority(solver); - environment.symbolic_attribute_by_name.insert( + internal_interpreter::AddSymbolicPriority(constraint_solver.solver_); + constraint_solver.environment_.symbolic_attribute_by_name.insert( {kSymbolicPriorityAttributeName, std::move(priority)}); } - // Add constraint if it exists. if (table.constraint.has_value()) { - ASSIGN_OR_RETURN( - z3::expr constraint, - internal_interpreter::EvaluateConstraintSymbolically( - *table.constraint, table.constraint_source, environment, solver)); - solver.add(constraint); + ASSIGN_OR_RETURN(bool modeled_constraint_added, + constraint_solver.AddConstraint(*table.constraint, + table.constraint_source)); + if (!modeled_constraint_added) { + return gutils::InvalidArgumentErrorBuilder(GUTILS_LOC) + << "TableInfo provided an unsatisfiable constraint. " + "ConstraintSolver must contain a satisfiable constraint at all " + "times so creation failed.\n Unsatisfiable Constraint: " + << table.constraint_source.constraint_string; + } } - return environment; + return constraint_solver; } absl::StatusOr GetValue(const SymbolicKey& symbolic_key) { diff --git a/p4_constraints/backend/symbolic_interpreter.h b/p4_constraints/backend/symbolic_interpreter.h index a986dab..f452410 100644 --- a/p4_constraints/backend/symbolic_interpreter.h +++ b/p4_constraints/backend/symbolic_interpreter.h @@ -25,6 +25,7 @@ #define P4_CONSTRAINTS_BACKEND_SYMBOLIC_INTERPRETER_H_ #include +#include #include #include #include @@ -87,43 +88,60 @@ struct SymbolicEnvironment { symbolic_attribute_by_name; }; -// -- Main Functions ----------------------------------------------------------- - -// Adds sufficient symbolic constraints to `solver` to represent an entry for -// `table` that respects its P4-Constraints and is well-formed according to the -// P4Runtime specification. -// Specifically, populates `solver` with all of the keys from `table` aside from -// those skipped through `skip_key_named`. Also adds well-formedness constraints -// (further described at the `AddSymbolicKey` function below) for each key and -// Z3 versions of any p4-constraints given by `table.constraints`. If the -// P4Runtime standard requires the table's entries to have a priority (i.e. -// because at least one key is either Optional or Ternary), then a symbolic -// priority with well-formedness constraints is also added. Returns a -// SymbolicEnvironment mapping the names of all symbolic variables to their -// symbolic expression counterparts. -// NOTE: This API will only encode a single table entry (as opposed to multiple) -// for a given `solver`. In other words, it is NOT possible to encode -// constraints for multiple entries by calling this function more than once with -// the same `solver`. -absl::StatusOr EncodeValidTableEntryInZ3( - const TableInfo& table, z3::solver& solver, - std::function(absl::string_view key_name)> - skip_key_named = [](absl::string_view key_name) { return false; }); - -// Returns an entry for the table given by `table_info` derived from `model`. -// All keys named in `table_info` must be mapped by -// `environment.symbolic_key_by_name` unless `skip_key_named(name)` holds for -// the key `name`. NOTE: The entry will NOT contain an action and is thus not a -// valid P4Runtime entry without modification. -// NOTE: This API expects the `model` to represent a single table entry (as -// opposed to multiple). This can be achieved by a call to -// `EncodeValidTableEntryInZ3`. -// TODO(b/242201770): Extract actions once action constraints are supported. -absl::StatusOr ConcretizeEntry( - const z3::model& model, const TableInfo& table_info, - const SymbolicEnvironment& environment, - std::function(absl::string_view key_name)> - skip_key_named = [](absl::string_view key_name) { return false; }); +// -- Main Class --------------------------------------------------------------- + +// A solver for constraints on a table. +// NOTE: Encodes a single table entry for the table given to the constructor. A +// single instantiation can not be used to encode multiple entries. +class ConstraintSolver { + public: + // Constructs a ConstraintSolver representing an entry for `table` that + // respects its P4-Constraints and is well-formed according to the P4Runtime + // specification. An entry encoded by the resulting ConstraintSolver does not + // include any `key` for which `skip_key_named(key)` is true. + static absl::StatusOr Create( + const TableInfo& table, + std::function(absl::string_view key_name)> + skip_key_named = [](absl::string_view key_name) { return false; }); + + // Returns true and adds constraint to the solver. If `constraint` would make + // the current ConstraintSolver unable to generate an entry, returns false and + // does not change the state of the ConstraintSolver. If `constraint` is + // malformed returns error and `constraint_source` is used for debugging info. + absl::StatusOr AddConstraint(const ast::Expression& constraint, + const ConstraintSource& constraint_source); + // Similar to overload above except that both the AST expression and its + // source are derived from `constraint`. Additionally returns an error if a + // valid AST cannot be produced from `constraint`. + absl::StatusOr AddConstraint(absl::string_view constraint); + + // Returns the entry encoded by the object. + // NOTE: The entry will NOT contain an action and is thus not a valid + // P4Runtime entry without modification. + // TODO(b/242201770): Extract actions once action constraints are supported. + absl::StatusOr ConcretizeEntry(); + + private: + explicit ConstraintSolver() + : context_(std::make_unique()), + solver_(z3::solver(*context_)) {} + + // Z3 context and solver. Solver requires a reference to `context` for + // construction so it is privately stored to avoid dangling reference. + std::unique_ptr context_; + z3::solver solver_; + + // TableInfo of table that is being constrained. + TableInfo table_info_; + + // Symbolic environment for storing information on symbolic keys. + SymbolicEnvironment environment_; + + // Function to determine whether a key should be ignored while creating + // `environment_` and generating a concrete entry. + std::function(absl::string_view key_name)> + skip_key_named_; +}; // -- Accessors ---------------------------------------------------------------- diff --git a/p4_constraints/backend/symbolic_interpreter_test.cc b/p4_constraints/backend/symbolic_interpreter_test.cc index b0204fe..fcb2259 100644 --- a/p4_constraints/backend/symbolic_interpreter_test.cc +++ b/p4_constraints/backend/symbolic_interpreter_test.cc @@ -12,7 +12,6 @@ #include "absl/container/flat_hash_set.h" #include "absl/log/check.h" #include "absl/status/status.h" -#include "absl/strings/match.h" #include "absl/strings/string_view.h" #include "gutils/parse_text_proto.h" #include "gutils/protocol_buffer_matchers.h" @@ -43,7 +42,6 @@ using ::p4_constraints::ast::Type; using ::p4_constraints::internal_interpreter::AddSymbolicKey; using ::p4_constraints::internal_interpreter::AddSymbolicPriority; using ::p4_constraints::internal_interpreter::EvaluateConstraintSymbolically; -using ::testing::IsEmpty; using ::testing::Not; // Tests basic properties with a suite of simple test cases. @@ -588,80 +586,14 @@ TEST_P(ConstraintTest, EXPECT_EQ(solver.check(), GetParam().is_sat ? z3::sat : z3::unsat); } -TEST_P(ConstraintTest, ConcretizeEntryGivesEntrySatisfyingConstraints) { - if (!GetParam().is_sat) { - GTEST_SKIP() << "Test only sensible for satisfiable constraints"; - } - z3::context solver_context; - z3::solver solver(solver_context); - - TableInfo table_info = - GetTableInfoWithConstraint(GetParam().constraint_string); - - // Add symbolic table keys to symbolic key map. - SymbolicEnvironment environment; - for (const auto& [key_name, key_info] : table_info.keys_by_name) { - ASSERT_OK_AND_ASSIGN(SymbolicKey key, AddSymbolicKey(key_info, solver)); - environment.symbolic_key_by_name.insert({key_name, std::move(key)}); - } - - // Add symbolic priority to attribute map. - SymbolicAttribute symbolic_priority = AddSymbolicPriority(solver); - environment.symbolic_attribute_by_name.insert( - {kSymbolicPriorityAttributeName, std::move(symbolic_priority)}); - - ASSERT_OK_AND_ASSIGN(z3::expr z3_constraint, - EvaluateConstraintSymbolically( - *table_info.constraint, table_info.constraint_source, - environment, solver)); - solver.add(z3_constraint); - - ASSERT_EQ(solver.check(), z3::sat); - ASSERT_OK_AND_ASSIGN( - p4::v1::TableEntry concretized_entry, - ConcretizeEntry(solver.get_model(), table_info, environment)); - - // Sanity check that every exact value is not the empty string. - for (const auto& match : concretized_entry.match()) { - if (match.has_exact()) { - EXPECT_NE(match.exact().value(), ""); - } - } - - ConstraintInfo context{ - .action_info_by_id = {}, - .table_info_by_id = {{ - table_info.id, - table_info, - }}, - }; - // The empty string signifies that the entry doesn't violate the constraint. - EXPECT_THAT(ReasonEntryViolatesConstraint(concretized_entry, context), - IsOkAndHolds("")) - << "\nFor entry:\n" - << concretized_entry.DebugString() - << "\nConstraint string: " << GetParam().constraint_string - << "\nConstraint: " << table_info.constraint->DebugString() - << "\nAnd solver state: " << solver.to_smt2(); -} - -TEST(EncodeValidTableEntryInZ3Test, WorksWithoutConstraints) { - z3::context solver_context; - z3::solver solver(solver_context); - +TEST(CreateConstraintSolver, WorksWithoutConstraints) { TableInfo table_info = GetTableInfoWithConstraint("true"); table_info.constraint = std::nullopt; - ASSERT_OK_AND_ASSIGN(SymbolicEnvironment environment, - EncodeValidTableEntryInZ3(table_info, solver)); - - EXPECT_EQ(solver.check(), z3::sat); + EXPECT_OK(ConstraintSolver::Create(table_info)); } -TEST(EncodeValidTableEntryInZ3Test, WorksWithoutPriority) { - z3::context solver_context; - z3::solver solver(solver_context); - +TEST(CreateConstraintSolverAddConstraint, WorksWithoutPriority) { TableInfo table_info = GetTableInfoWithConstraint("true"); // Remove the ternaries and optionals, so that no priority is required. @@ -675,42 +607,31 @@ TEST(EncodeValidTableEntryInZ3Test, WorksWithoutPriority) { table_info.keys_by_name.erase(key.name); table_info.keys_by_id.erase(key.id); } - - ASSERT_OK_AND_ASSIGN(SymbolicEnvironment environment, - EncodeValidTableEntryInZ3(table_info, solver)); - EXPECT_THAT(environment.symbolic_attribute_by_name, IsEmpty()); - - EXPECT_EQ(solver.check(), z3::sat); + EXPECT_OK(ConstraintSolver::Create(table_info)); } -TEST_P(ConstraintTest, EncodeValidTableEntryInZ3CheckSatAndUnsatCorrectness) { - z3::context solver_context; - z3::solver solver(solver_context); - +TEST_P(ConstraintTest, CreateOnlyWorksWithSatisfiableConstraints) { TableInfo table_info = GetTableInfoWithConstraint(GetParam().constraint_string); - ASSERT_OK_AND_ASSIGN(SymbolicEnvironment environment, - EncodeValidTableEntryInZ3(table_info, solver)); - EXPECT_EQ(solver.check(), GetParam().is_sat ? z3::sat : z3::unsat); + EXPECT_THAT( + ConstraintSolver::Create(table_info), + (GetParam().is_sat ? StatusIs(absl::StatusCode::kOk) + : StatusIs(absl::StatusCode::kInvalidArgument))); } -TEST_P(ConstraintTest, EncodeValidTableEntryInZ3AndConcretizeEntry) { +TEST_P(ConstraintTest, CreateConstraintSolverAndConcretizeEntry) { if (!GetParam().is_sat) { GTEST_SKIP() << "Test only sensible for satisfiable constraints"; } - z3::context solver_context; - z3::solver solver(solver_context); - TableInfo table_info = GetTableInfoWithConstraint(GetParam().constraint_string); - ASSERT_OK_AND_ASSIGN(SymbolicEnvironment environment, - EncodeValidTableEntryInZ3(table_info, solver)); - ASSERT_EQ(solver.check(), z3::sat); - ASSERT_OK_AND_ASSIGN( - p4::v1::TableEntry concretized_entry, - ConcretizeEntry(solver.get_model(), table_info, environment)); + ASSERT_OK_AND_ASSIGN(ConstraintSolver constraint_solver, + ConstraintSolver::Create(table_info)); + + ASSERT_OK_AND_ASSIGN(p4::v1::TableEntry concretized_entry, + constraint_solver.ConcretizeEntry()); // The empty string signifies that the entry doesn't violate the constraint. ConstraintInfo context{ @@ -725,8 +646,7 @@ TEST_P(ConstraintTest, EncodeValidTableEntryInZ3AndConcretizeEntry) { << "\nFor entry:\n" << concretized_entry.DebugString() << "\nConstraint string: " << GetParam().constraint_string - << "\nConstraint: " << table_info.constraint->DebugString() - << "\nAnd solver state: " << solver.to_smt2(); + << "\nConstraint: " << table_info.constraint->DebugString(); } INSTANTIATE_TEST_SUITE_P( @@ -843,69 +763,8 @@ struct FullySpecifiedConstraintTestCase { using FullySpecifiedConstraintTest = testing::TestWithParam; -TEST_P(FullySpecifiedConstraintTest, ConcretizeEntryGivesExactEntry) { - z3::context solver_context; - z3::solver solver(solver_context); - - TableInfo table_info = - GetTableInfoWithConstraint(GetParam().constraint_string); - ConstraintInfo context{ - .action_info_by_id = {}, - .table_info_by_id = {{ - table_info.id, - table_info, - }}, - }; - // TODO(b/297400616): p4-constraints currently does not correctly translate - // the bytestring representing 1280 to 1280 (instead turning it into 5). - if (!absl::StrContains(GetParam().constraint_string, "1280")) { - // Sanity check that the expected entry actually satisfies the constraint. - // The empty string signifies that the entry doesn't violate the constraint. - ASSERT_THAT(ReasonEntryViolatesConstraint( - GetParam().expected_concretized_entry, context), - IsOkAndHolds("")) - << "\nFor entry:\n" - << GetParam().expected_concretized_entry.DebugString() - << "\nConstraint string: " << GetParam().constraint_string - << "\nConstraint: " << table_info.constraint->DebugString() - << "\nAnd solver state: " << solver.to_smt2(); - } - - // Add symbolic table keys to symbolic key map. - SymbolicEnvironment environment; - for (const auto& [key_name, key_info] : table_info.keys_by_name) { - ASSERT_OK_AND_ASSIGN(SymbolicKey key, AddSymbolicKey(key_info, solver)); - environment.symbolic_key_by_name.insert({key_name, std::move(key)}); - } - - // Add symbolic priority to attribute map. - SymbolicAttribute symbolic_priority = AddSymbolicPriority(solver); - environment.symbolic_attribute_by_name.insert( - {kSymbolicPriorityAttributeName, std::move(symbolic_priority)}); - - ASSERT_OK_AND_ASSIGN(z3::expr z3_constraint, - EvaluateConstraintSymbolically( - *table_info.constraint, table_info.constraint_source, - environment, solver)); - solver.add(z3_constraint); - - ASSERT_EQ(solver.check(), z3::sat); - ASSERT_OK_AND_ASSIGN( - p4::v1::TableEntry concretized_entry, - ConcretizeEntry(solver.get_model(), table_info, environment, - [&](absl::string_view key_name) { - return GetParam().keys_to_skip.contains(key_name); - })); - - EXPECT_THAT(concretized_entry, IgnoringRepeatedFieldOrdering(EqualsProto( - GetParam().expected_concretized_entry))); -} - TEST_P(FullySpecifiedConstraintTest, - EncodeValidTableEntryInZ3AndConcretizeEntryGivesExactEntry) { - z3::context solver_context; - z3::solver solver(solver_context); - + CreateConstraintSolverAndConcretizeEntryGivesExactEntry) { TableInfo table_info = GetTableInfoWithConstraint(GetParam().constraint_string); ConstraintInfo context{ @@ -915,31 +774,25 @@ TEST_P(FullySpecifiedConstraintTest, table_info, }}, }; - // TODO(b/297400616): p4-constraints currently does not correctly translate - // the bytestring representing 1280 to 1280 (instead turning it into 5). - if (!absl::StrContains(GetParam().constraint_string, "1280")) { - // Sanity check that the expected entry actually satisfies the constraint. - // The empty string signifies that the entry doesn't violate the constraint. - ASSERT_THAT(ReasonEntryViolatesConstraint( - GetParam().expected_concretized_entry, context), - IsOkAndHolds("")) - << "\nFor entry:\n" - << GetParam().expected_concretized_entry.DebugString() - << "\nConstraint string: " << GetParam().constraint_string - << "\nConstraint: " << table_info.constraint->DebugString() - << "\nAnd solver state: " << solver.to_smt2(); - } - ASSERT_OK_AND_ASSIGN(SymbolicEnvironment environment, - EncodeValidTableEntryInZ3(table_info, solver)); + // Sanity check that the expected entry actually satisfies the constraint. + // The empty string signifies that the entry doesn't violate the constraint. + ASSERT_THAT(ReasonEntryViolatesConstraint( + GetParam().expected_concretized_entry, context), + IsOkAndHolds("")) + << "\nFor entry:\n" + << GetParam().expected_concretized_entry.DebugString() + << "\nConstraint string: " << GetParam().constraint_string + << "\nConstraint: " << table_info.constraint->DebugString(); - ASSERT_EQ(solver.check(), z3::sat); ASSERT_OK_AND_ASSIGN( - p4::v1::TableEntry concretized_entry, - ConcretizeEntry(solver.get_model(), table_info, environment, - [&](absl::string_view key_name) { - return GetParam().keys_to_skip.contains(key_name); - })); + ConstraintSolver constraint_solver, + ConstraintSolver::Create(table_info, [&](absl::string_view key_name) { + return GetParam().keys_to_skip.contains(key_name); + })); + + ASSERT_OK_AND_ASSIGN(p4::v1::TableEntry concretized_entry, + constraint_solver.ConcretizeEntry()); EXPECT_THAT(concretized_entry, IgnoringRepeatedFieldOrdering(EqualsProto( GetParam().expected_concretized_entry))); @@ -1128,5 +981,237 @@ INSTANTIATE_TEST_SUITE_P( [](const testing::TestParamInfo& info) { return SnakeCaseToCamelCase(info.param.test_name); }); + +TEST(AddConstraint, NonBooleanConstraintGivesInvalidArgument) { + ASSERT_OK_AND_ASSIGN( + ConstraintSolver constraint_solver, + ConstraintSolver::Create(GetTableInfoWithConstraint("true"))); + + EXPECT_THAT(constraint_solver.AddConstraint("42"), + StatusIs(absl::StatusCode::kInvalidArgument)); +} + +TEST(AddConstraintToZ3Solver, UnknownVariableGivesInvalidArgument) { + ASSERT_OK_AND_ASSIGN( + ConstraintSolver constraint_solver, + ConstraintSolver::Create(GetTableInfoWithConstraint("true"))); + + EXPECT_THAT(constraint_solver.AddConstraint("dragon == 42"), + StatusIs(absl::StatusCode::kInvalidArgument)); +} + +TEST(AddConstraintToZ3Solver, OnlySatisfiableConstraintCanBeAdded) { + ASSERT_OK_AND_ASSIGN( + ConstraintSolver constraint_solver, + ConstraintSolver::Create(GetTableInfoWithConstraint("true"))); + + EXPECT_THAT(constraint_solver.AddConstraint("false"), IsOkAndHolds(false)); + + EXPECT_THAT(constraint_solver.AddConstraint("true"), IsOkAndHolds(true)); +} + +struct AdditionalConstraintTestCase { + std::string test_name; + // A protobuf string representing a boolean AST Expression representing a + // constraint. + std::string p4_program_constraint_string; + std::string custom_constraint_string; + bool is_sat; +}; + +using AdditionalConstraintTest = + testing::TestWithParam; + +TEST_P(AdditionalConstraintTest, + AddConstraintToZ3SolverCheckSatAndUnsatCorrectness) { + TableInfo table_info = + GetTableInfoWithConstraint(GetParam().p4_program_constraint_string); + + ASSERT_OK_AND_ASSIGN(ConstraintSolver constraint_solver, + ConstraintSolver::Create(table_info)); + + EXPECT_THAT( + constraint_solver.AddConstraint(GetParam().custom_constraint_string), + IsOkAndHolds(GetParam().is_sat)); +} + +TEST_P(AdditionalConstraintTest, AddConstraintToZ3SolverAndConcretizeEntry) { + if (!GetParam().is_sat) { + GTEST_SKIP() << "Test only sensible for satisfiable constraints"; + } + + TableInfo table_info = + GetTableInfoWithConstraint(GetParam().p4_program_constraint_string); + + ASSERT_OK_AND_ASSIGN(ConstraintSolver constraint_solver, + ConstraintSolver::Create(table_info)); + + ASSERT_THAT( + constraint_solver.AddConstraint(GetParam().custom_constraint_string), + IsOkAndHolds(true)); + + ASSERT_OK_AND_ASSIGN(p4::v1::TableEntry concretized_entry, + constraint_solver.ConcretizeEntry()); + + // The empty string signifies that the entry doesn't violate the + ConstraintInfo context{ + .action_info_by_id = {}, + .table_info_by_id = {{ + table_info.id, + table_info, + }}, + }; + EXPECT_THAT(ReasonEntryViolatesConstraint(concretized_entry, context), + IsOkAndHolds("")) + << "\nFor entry:\n" + << concretized_entry.DebugString() << "\nP4 program constraint string: " + << "\nP4 program constraint: " << table_info.constraint->DebugString() + << GetParam().p4_program_constraint_string + << "\nCustom constraint string: " << GetParam().custom_constraint_string; +} + +INSTANTIATE_TEST_SUITE_P( + AddtionalConstraintSatisfiabilityTests, AdditionalConstraintTest, + testing::ValuesIn(std::vector{ + { + .test_name = "adding_sat_does_not_affect_sat", + .p4_program_constraint_string = "true", + .custom_constraint_string = "true", + .is_sat = true, + }, + { + .test_name = "adding_unsat_forces_unsat", + .p4_program_constraint_string = "true", + .custom_constraint_string = "false", + .is_sat = false, + }, + { + .test_name = "independent_sats_are_sat", + .p4_program_constraint_string = "exact32 == 42;", + .custom_constraint_string = "optional32 != 42", + .is_sat = true, + }, + { + .test_name = "related_and_compatible_sats_are_sat", + .p4_program_constraint_string = "exact32 == 42;", + .custom_constraint_string = "exact32 != 7", + .is_sat = true, + }, + { + .test_name = "related_and_conflicting_sats_are_unsat", + .p4_program_constraint_string = "exact32 == 42;", + .custom_constraint_string = "exact32 != 42", + .is_sat = false, + }, + }), + [](const testing::TestParamInfo& info) { + return SnakeCaseToCamelCase(info.param.test_name); + }); + +struct FullySpecifiedAdditionalConstraintTestCase { + std::string test_name; + // Protobuf strings representing a boolean AST Expression coming from a p4 + // program and additional custom constraint respectively. The combination of + // both must fully specify the entry given below. + std::string p4_info_constraint_string; + std::string custom_constraint_string; + // Should be set with the only entry that can possibly meet the combination + // of constraint strings. + p4::v1::TableEntry expected_concretized_entry; + // Optionally, specify a set of keys that should be skipped when + // concretizing the table entry. This only makes sense for non-required keys. + absl::flat_hash_set keys_to_skip; +}; + +using FullySpecifiedAdditionalConstraintTest = + testing::TestWithParam; + +TEST_P(FullySpecifiedAdditionalConstraintTest, + EncodeValidTableEntryInZ3AndConcretizeEntryGivesExactEntry) { + TableInfo table_info = + GetTableInfoWithConstraint(GetParam().p4_info_constraint_string); + ConstraintInfo context{ + .action_info_by_id = {}, + .table_info_by_id = {{ + table_info.id, + table_info, + }}, + }; + + // Sanity check that the expected entry actually satisfies the constraint. + // The empty string signifies that the entry doesn't violate the + ASSERT_THAT(ReasonEntryViolatesConstraint( + GetParam().expected_concretized_entry, context), + IsOkAndHolds("")) + << "\nFor entry:\n" + << GetParam().expected_concretized_entry.DebugString() + << "\nConstraint string: " << GetParam().p4_info_constraint_string + << "\nConstraint: " << table_info.constraint->DebugString(); + + ASSERT_OK_AND_ASSIGN(ConstraintSolver constraint_solver, + ConstraintSolver::Create(table_info)); + + ASSERT_THAT( + constraint_solver.AddConstraint(GetParam().custom_constraint_string), + IsOkAndHolds(true)); + + ASSERT_OK_AND_ASSIGN(p4::v1::TableEntry concretized_entry, + constraint_solver.ConcretizeEntry()); + + EXPECT_THAT(concretized_entry, IgnoringRepeatedFieldOrdering(EqualsProto( + GetParam().expected_concretized_entry))); +} + +INSTANTIATE_TEST_SUITE_P( + CheckExactEntryOutput, FullySpecifiedAdditionalConstraintTest, + testing::ValuesIn(std::vector{ + { + .test_name = "only_equals_across_both_constraints", + .p4_info_constraint_string = + "exact11 == 5; ::priority == 50; " + "optional32::mask == 0; optional28::mask == 0;", + .custom_constraint_string = + "exact32 == 5; " + "lpm32::prefix_length == 0; ternary32::mask == 0; ", + .expected_concretized_entry = + ParseTextProtoOrDie(R"pb( + table_id: 1 + match { + field_id: 1 + exact { value: "\005" } + } + match { + field_id: 5 + exact { value: "\005" } + } + priority: 50 + )pb"), + }, + { + .test_name = "exact_inequalities_across_both_constraints", + .p4_info_constraint_string = + "::priority > 1; exact32::value > 1; exact11::value > 1;" + "lpm32::prefix_length == 0; ternary32::mask == 0;" + " optional32::mask == 0; optional28::mask == 0;", + .custom_constraint_string = + "::priority < 3; exact32::value < 3; exact11::value < 3;", + .expected_concretized_entry = + ParseTextProtoOrDie(R"pb( + table_id: 1 + match { + field_id: 1 + exact { value: "\002" } + } + match { + field_id: 5 + exact { value: "\002" } + } + priority: 2 + )pb"), + }, + }), + [](const testing::TestParamInfo& + info) { return SnakeCaseToCamelCase(info.param.test_name); }); + } // namespace } // namespace p4_constraints diff --git a/p4_constraints/frontend/BUILD.bazel b/p4_constraints/frontend/BUILD.bazel index ccd1d2b..38b0b9f 100644 --- a/p4_constraints/frontend/BUILD.bazel +++ b/p4_constraints/frontend/BUILD.bazel @@ -103,7 +103,7 @@ cc_library( "-lgmp", "-lgmpxx", ], - visibility = ["//p4_constraints/backend:__pkg__"], + visibility = ["//visibility:private"], deps = [ ":constraint_kind", ":token",