From a5cdfa9813ce171c5df51ffced4244e1e62dfa02 Mon Sep 17 00:00:00 2001 From: PINS Team Date: Thu, 27 Jul 2023 17:57:11 +0000 Subject: [PATCH] PUBLIC: [P4-Constraint] Add a function to concretize symbolic entries. PiperOrigin-RevId: 551581204 --- p4_constraints/backend/BUILD.bazel | 3 + p4_constraints/backend/interpreter_test.cc | 69 +++- .../backend/symbolic_interpreter.cc | 221 ++++++++++- p4_constraints/backend/symbolic_interpreter.h | 27 +- .../backend/symbolic_interpreter_test.cc | 361 +++++++++++++++++- 5 files changed, 666 insertions(+), 15 deletions(-) diff --git a/p4_constraints/backend/BUILD.bazel b/p4_constraints/backend/BUILD.bazel index b776f2d..217e8ee 100644 --- a/p4_constraints/backend/BUILD.bazel +++ b/p4_constraints/backend/BUILD.bazel @@ -161,6 +161,7 @@ cc_library( "//p4_constraints:ast", "//p4_constraints:ast_cc_proto", "//p4_constraints:constraint_source", + "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", "@com_github_z3prover_z3//:api", "@com_google_absl//absl/container:flat_hash_map", "@com_google_absl//absl/status", @@ -192,6 +193,7 @@ cc_test( ":interpreter", ":symbolic_interpreter", "//gutils:parse_text_proto", + "//gutils:protocol_buffer_matchers", "//gutils:status_matchers", "//gutils:testing", "//p4_constraints:ast_cc_proto", @@ -200,6 +202,7 @@ cc_test( "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", "@com_github_z3prover_z3//:api", "@com_google_absl//absl/container:flat_hash_map", + "@com_google_absl//absl/container:flat_hash_set", "@com_google_absl//absl/log:check", "@com_google_absl//absl/status", "@com_google_absl//absl/strings", diff --git a/p4_constraints/backend/interpreter_test.cc b/p4_constraints/backend/interpreter_test.cc index 7d790e4..5dd39f1 100644 --- a/p4_constraints/backend/interpreter_test.cc +++ b/p4_constraints/backend/interpreter_test.cc @@ -244,12 +244,79 @@ TEST_F(EntryMeetsConstraintTest, EntriesWithLeadingZeroesWork) { // Modify entry to have leading zeroes. p4::v1::TableEntry modified_entry = kTableEntry; modified_entry.mutable_match(0)->mutable_exact()->set_value( - absl::StrCat("\0", kTableEntry.match(0).exact().value())); + absl::StrCat(std::string{'\0'}, kTableEntry.match(0).exact().value())); EXPECT_THAT(EntryMeetsConstraint(modified_entry, MakeConstraintInfo(exact_equals_num)), IsOkAndHolds(true)); } +TEST_F(EntryMeetsConstraintTest, EntriesWithOnlyZeroesWork) { + const Expression exact_equals_num = ExpressionWithType(kBool, R"pb( + binary_expression { + binop: EQ + left { + type { exact { bitwidth: 32 } } + key: "exact32" + } + right { + type { exact { bitwidth: 32 } } + type_cast { + type { fixed_unsigned { bitwidth: 32 } } + type_cast { + type { arbitrary_int {} } + integer_constant: "0" + } + } + } + } + )pb"); + // Unmodified entry should not meet constraint since exact32 != 0. + ASSERT_THAT( + EntryMeetsConstraint(kTableEntry, MakeConstraintInfo(exact_equals_num)), + IsOkAndHolds(false)); + + // Modify entry to be zero. + p4::v1::TableEntry modified_entry = kTableEntry; + modified_entry.mutable_match(0)->mutable_exact()->set_value( + std::string{'\0'}); + ASSERT_THAT(EntryMeetsConstraint(modified_entry, + MakeConstraintInfo(exact_equals_num)), + IsOkAndHolds(true)); +} + +TEST_F(EntryMeetsConstraintTest, EntriesWithZeroAsciiValueWorks) { + const Expression exact_equals_num = ExpressionWithType(kBool, R"pb( + binary_expression { + binop: EQ + left { + type { exact { bitwidth: 32 } } + key: "exact32" + } + right { + type { exact { bitwidth: 32 } } + type_cast { + type { fixed_unsigned { bitwidth: 32 } } + type_cast { + type { arbitrary_int {} } + integer_constant: "48" + } + } + } + } + )pb"); + // Unmodified entry should not meet constraint since exact32 != 48. + ASSERT_THAT( + EntryMeetsConstraint(kTableEntry, MakeConstraintInfo(exact_equals_num)), + IsOkAndHolds(false)); + + // Modify entry to be zero character. + p4::v1::TableEntry modified_entry = kTableEntry; + modified_entry.mutable_match(0)->mutable_exact()->set_value("0"); + ASSERT_THAT(EntryMeetsConstraint(modified_entry, + MakeConstraintInfo(exact_equals_num)), + IsOkAndHolds(true)); +} + Expression GetPriorityEqualityConstraint(const int32_t priority) { constexpr absl::string_view kPriorityEqualityConstraint = R"pb( type { boolean {} } diff --git a/p4_constraints/backend/symbolic_interpreter.cc b/p4_constraints/backend/symbolic_interpreter.cc index 3a7dba7..424172a 100644 --- a/p4_constraints/backend/symbolic_interpreter.cc +++ b/p4_constraints/backend/symbolic_interpreter.cc @@ -17,7 +17,9 @@ #include "p4_constraints/backend/symbolic_interpreter.h" #include +#include #include +#include #include #include #include @@ -25,13 +27,16 @@ #include "absl/container/flat_hash_map.h" #include "absl/status/status.h" #include "absl/status/statusor.h" +#include "absl/strings/escaping.h" #include "absl/strings/str_cat.h" #include "absl/strings/string_view.h" +#include "absl/strings/strip.h" #include "gutils/collections.h" #include "gutils/overload.h" #include "gutils/source_location.h" #include "gutils/status_builder.h" #include "gutils/status_macros.h" +#include "p4/v1/p4runtime.pb.h" #include "p4_constraints/ast.h" #include "p4_constraints/ast.pb.h" #include "p4_constraints/backend/constraint_info.h" @@ -409,6 +414,175 @@ absl::StatusOr EvalSymbolically( << "got invalid expression: " << expr.DebugString(); } +// Turns a bitstring (expressed as a normal string with only 0s and 1s) into a +// compact P4Runtime bytestring (i.e. one without leading 0s). +absl::StatusOr BitstringToP4RuntimeBytestring( + absl::string_view bitstring, int bitwidth) { + std::string padded_bitstring(bitstring); + // If bitwidth is not divisible by 8, pad beginning with 0s. + if (bitwidth % 8 != 0) { + padded_bitstring = + absl::StrCat(std::string(8 - bitwidth % 8, '0'), padded_bitstring); + } + + // Construct a bytestring bit-by-bit. + std::string bytestring; + bytestring.reserve((bitwidth + 7) / 8); + uint8_t byte = 0; + // Track if we've seen non-zero byte to skip leading zeroes. + bool seen_non_zero_byte = false; + for (int i = 0; i < padded_bitstring.size(); i++) { + byte <<= 1; + if (padded_bitstring[i] == '1') { + byte += 1; + } + if ((i + 1) % 8 == 0) { + // Skip leading zero bytes. + if (seen_non_zero_byte || byte != 0) { + bytestring += byte; + seen_non_zero_byte = true; + } + byte = 0; + } + } + // Bytestrings may not be empty, so if the bitstring is all 0s, then we + // concretize it to be the zero byte. + if (bytestring.empty()) { + bytestring = std::string{'\0'}; + } + return bytestring; +} + +// Turns a hexstring into a compact P4Runtime bytestring (i.e. one without +// leading 0s). +absl::StatusOr HexstringToP4RuntimeBytestring( + absl::string_view hexstring) { + // Get rid of leading zeroes. + if (hexstring.find_first_not_of('0') < hexstring.size()) { + hexstring.remove_prefix(hexstring.find_first_not_of('0')); + } else { + // hexstring was just 0, so we make it a byte-sized hex string equal to 0. + return std::string{'\0'}; + } + // The hex string length needs to be divisible by 2 to be convertible to a + // bytestring, so we pad with a 0 if it's too short. + return absl::HexStringToBytes( + hexstring.length() % 2 != 0 ? absl::StrCat("0", hexstring) : hexstring); +} + +absl::StatusOr Z3BitvectorValueToP4RuntimeBytestring( + absl::string_view z3_value, int bitwidth) { + if (absl::ConsumePrefix(&z3_value, "#x")) { + return HexstringToP4RuntimeBytestring(z3_value); + } + if (absl::ConsumePrefix(&z3_value, "#b")) { + return BitstringToP4RuntimeBytestring(z3_value, bitwidth); + } + return gutils::InvalidArgumentErrorBuilder() + << "Expected a Z3 bitvector value starting with '#x' or '#b', but got " + "'" + << z3_value << "'."; +} + +absl::StatusOr> ConcretizeKey( + const SymbolicKey& match_key, const p4_constraints::KeyInfo& key_info, + const z3::model& model) { + p4::v1::FieldMatch match; + match.set_field_id(key_info.id); + ASSIGN_OR_RETURN(int bitwidth, + p4_constraints::ast::TypeBitwidthOrStatus(key_info.type)); + switch (key_info.type.type_case()) { + case p4_constraints::ast::Type::kExact: { + ASSIGN_OR_RETURN(z3::expr match_key_value, GetValue(match_key)); + ASSIGN_OR_RETURN( + *match.mutable_exact()->mutable_value(), + // Even if the match_key_value is uninterpreted in the model, we + // require the evaluation to generate a value for it, since exact + // matches must be present. + Z3BitvectorValueToP4RuntimeBytestring( + model.eval(match_key_value, /*model_completion=*/true) + .to_string(), + bitwidth)); + return match; + } + case p4_constraints::ast::Type::kOptionalMatch: + case p4_constraints::ast::Type::kTernary: { + ASSIGN_OR_RETURN(z3::expr key_mask, GetMask(match_key)); + // We use a mask of all 0 bits to denote the wildcard match in our Z3 + // encoding. + if (model.eval(key_mask == 0, /*model_completion=*/true).is_true()) + return std::nullopt; + ASSIGN_OR_RETURN(z3::expr match_key_value, GetValue(match_key)); + + if (key_info.type.has_optional_match()) { + ASSIGN_OR_RETURN( + *match.mutable_optional()->mutable_value(), + Z3BitvectorValueToP4RuntimeBytestring( + model.eval(match_key_value, /*model_completion=*/true) + .to_string(), + bitwidth)); + } else { + ASSIGN_OR_RETURN( + *match.mutable_ternary()->mutable_value(), + Z3BitvectorValueToP4RuntimeBytestring( + model.eval(match_key_value, /*model_completion=*/true) + .to_string(), + bitwidth)); + ASSIGN_OR_RETURN( + *match.mutable_ternary()->mutable_mask(), + Z3BitvectorValueToP4RuntimeBytestring( + model.eval(key_mask, /*model_completion=*/true).to_string(), + bitwidth)); + } + return match; + } + + case p4_constraints::ast::Type::kLpm: { + ASSIGN_OR_RETURN(z3::expr key_prefix_length, GetPrefixLength(match_key)); + if (!model.eval(key_prefix_length, /*model_completion=*/true) + .is_numeral()) { + return gutils::InternalErrorBuilder(GUTILS_LOC) + << "Prefix length should always be an integer. Instead, got '" + << model.eval(key_prefix_length) + << "' for key: " << key_info.name; + } + int prefix_length = + model.eval(key_prefix_length, /*model_completion=*/true) + .get_numeral_int(); + // We use a prefix length of 0 to denote the wildcard match in Z3. + if (prefix_length == 0) return std::nullopt; + ASSIGN_OR_RETURN(z3::expr match_key_value, GetValue(match_key)); + + ASSIGN_OR_RETURN( + *match.mutable_lpm()->mutable_value(), + Z3BitvectorValueToP4RuntimeBytestring( + model.eval(match_key_value, /*model_completion=*/true) + .to_string(), + bitwidth)); + match.mutable_lpm()->set_prefix_len(prefix_length); + return match; + } + + // TODO(b/291779521): Range matches are not currently supported. + case ast::Type::kRange: + return gutils::UnimplementedErrorBuilder() + << "Range matches are not currently supported by the " + "p4-constraints symbolic representation."; + + // Non-match types. + case p4_constraints::ast::Type::kUnknown: + case p4_constraints::ast::Type::kUnsupported: + case p4_constraints::ast::Type::kBoolean: + case p4_constraints::ast::Type::kArbitraryInt: + case p4_constraints::ast::Type::kFixedUnsigned: + case p4_constraints::ast::Type::TYPE_NOT_SET: + return gutils::InvalidArgumentErrorBuilder() + << "expected a match type, but got: " << key_info; + } + return gutils::InvalidArgumentErrorBuilder() + << "got invalid type: " << key_info; +} + } // namespace absl::StatusOr AddSymbolicKey(const KeyInfo& key, @@ -484,7 +658,8 @@ absl::StatusOr AddSymbolicKey(const KeyInfo& key, } SymbolicAttribute AddSymbolicPriority(z3::solver& solver) { - z3::expr priority_key = solver.ctx().int_const("priority"); + z3::expr priority_key = + solver.ctx().int_const(kSymbolicPriorityAttributeName); solver.add(priority_key > 0); solver.add(priority_key <= std::numeric_limits::max()); return SymbolicAttribute{.value = priority_key}; @@ -508,6 +683,50 @@ absl::StatusOr EvaluateConstraintSymbolically( symbolic_attribute_by_name, solver); } +absl::StatusOr ConcretizeEntry( + const z3::model& model, const TableInfo& table_info, + const absl::flat_hash_map& symbolic_key_by_name, + const absl::flat_hash_map& + symbolic_attribute_by_name, + std::function(absl::string_view key_name)> + skip_key_named) { + p4::v1::TableEntry table_entry; + 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)); + if (key_should_be_skipped) continue; + + ASSIGN_OR_RETURN(const SymbolicKey* symbolic_key, + gutils::FindPtrOrStatus(symbolic_key_by_name, key_name)); + ASSIGN_OR_RETURN(std::optional match, + ConcretizeKey(*symbolic_key, key_info, model)); + + // A match without a value indicates a wildcard match. + if (match.has_value()) { + *table_entry.add_match() = *match; + } + } + + // Set priority if it exists. + if (auto priority_key = gutils::FindPtrOrStatus( + symbolic_attribute_by_name, kSymbolicPriorityAttributeName); + priority_key.ok()) { + if (model.has_interp((*priority_key)->value.decl())) { + table_entry.set_priority( + model.eval((*priority_key)->value).get_numeral_int()); + } else { + return gutils::InvalidArgumentErrorBuilder() + << "A priority SymbolicAttribute existed, but it was not " + "constrained. This should never happen. Please use " + "AddSymbolicPriority to initialize a priority for the symbolic " + "interpreter."; + } + } + return table_entry; +} + absl::StatusOr GetValue(const SymbolicKey& symbolic_key) { return GetFieldAccess(symbolic_key, "value"); } diff --git a/p4_constraints/backend/symbolic_interpreter.h b/p4_constraints/backend/symbolic_interpreter.h index 7a8978b..4b8753f 100644 --- a/p4_constraints/backend/symbolic_interpreter.h +++ b/p4_constraints/backend/symbolic_interpreter.h @@ -24,6 +24,7 @@ #ifndef P4_CONSTRAINTS_BACKEND_SYMBOLIC_INTERPRETER_H_ #define P4_CONSTRAINTS_BACKEND_SYMBOLIC_INTERPRETER_H_ +#include #include #include #include @@ -32,7 +33,9 @@ #include "absl/status/statusor.h" #include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" +#include "absl/strings/string_view.h" #include "gutils/overload.h" +#include "p4/v1/p4runtime.pb.h" #include "p4_constraints/ast.pb.h" #include "p4_constraints/backend/constraint_info.h" #include "p4_constraints/constraint_source.h" @@ -73,6 +76,8 @@ struct SymbolicAttribute { z3::expr value; }; +constexpr char kSymbolicPriorityAttributeName[] = "priority"; + // Z3 representation of a single match key in a P4 table entry. using SymbolicKey = std::variant; @@ -94,7 +99,7 @@ using SymbolicKey = std::variant; // // Expects `key` to have a non-zero bitwidth. // NOTE: This API will only work correctly if the `solver` represents a single -// table entry. +// table entry (as opposed to multiple). absl::StatusOr AddSymbolicKey(const KeyInfo& key, z3::solver& solver); @@ -103,7 +108,7 @@ absl::StatusOr AddSymbolicKey(const KeyInfo& key, // NOTE: Only needed for (and should only be used with) tables that // require/expect priority. // NOTE: This API will only work correctly if the `solver` represents a single -// table entry. +// table entry (as opposed to multiple). SymbolicAttribute AddSymbolicPriority(z3::solver& solver); // Translates a P4-Constraints expression into a Z3 expression using the @@ -114,7 +119,7 @@ SymbolicAttribute AddSymbolicPriority(z3::solver& solver); // InvalidArgumentError or InternalError. The `constraint_source` is used to // construct more palatable error messages. // NOTE: This API will only work correctly if the `solver` represents a single -// table entry. +// table entry (as opposed to multiple). absl::StatusOr EvaluateConstraintSymbolically( const ast::Expression& constraint, const ConstraintSource& constraint_source, @@ -123,6 +128,22 @@ absl::StatusOr EvaluateConstraintSymbolically( symbolic_attribute_by_name, z3::solver& solver); +// Returns an entry for the table given by `table_info` derived from `model`. +// All keys named in `table_info` must be mapped by `name_to_symbolic_key` +// 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 will only work correctly if the `model` represents a single +// table entry (as opposed to multiple). +// TODO(b/242201770): Extract actions once action constraints are supported. +absl::StatusOr ConcretizeEntry( + const z3::model& model, const TableInfo& table_info, + const absl::flat_hash_map& symbolic_key_by_name, + const absl::flat_hash_map& + symbolic_attribute_by_name, + std::function(absl::string_view key_name)> + skip_key_named = [](absl::string_view key_name) { return false; }); + // -- Accessors ---------------------------------------------------------------- // Gets the Z3 expression in the `value` field of `symbolic_key`, if it is diff --git a/p4_constraints/backend/symbolic_interpreter_test.cc b/p4_constraints/backend/symbolic_interpreter_test.cc index 636ff97..69cb42f 100644 --- a/p4_constraints/backend/symbolic_interpreter_test.cc +++ b/p4_constraints/backend/symbolic_interpreter_test.cc @@ -8,14 +8,19 @@ #include #include "absl/container/flat_hash_map.h" +#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" #include "gutils/status_matchers.h" #include "gutils/testing.h" +#include "p4/v1/p4runtime.pb.h" #include "p4_constraints/ast.pb.h" #include "p4_constraints/backend/constraint_info.h" +#include "p4_constraints/backend/interpreter.h" #include "p4_constraints/backend/type_checker.h" #include "p4_constraints/constraint_source.h" #include "p4_constraints/frontend/parser.h" @@ -26,7 +31,10 @@ namespace { using ::gutils::ParseTextProtoOrDie; using ::gutils::SnakeCaseToCamelCase; +using ::gutils::testing::EqualsProto; +using ::gutils::testing::proto::IgnoringRepeatedFieldOrdering; using ::gutils::testing::status::IsOk; +using ::gutils::testing::status::IsOkAndHolds; using ::gutils::testing::status::StatusIs; using ::p4_constraints::ast::Expression; using ::p4_constraints::ast::Type; @@ -458,6 +466,11 @@ TableInfo GetTableInfoWithConstraint(absl::string_view constraint_string) { const Type kLpm32 = ParseTextProtoOrDie("lpm { bitwidth: 32 }"); const Type kOptional32 = ParseTextProtoOrDie("optional_match { bitwidth: 32 }"); + // Keys whose bitwidth is not a multiple of 8 may be handled somewhat + // differently, so they are good to test. + const Type kExact11 = ParseTextProtoOrDie("exact { bitwidth: 11 }"); + const Type kOptional28 = + ParseTextProtoOrDie("optional_match { bitwidth: 28 }"); const std::string kTableName = "table"; ConstraintSource source{ @@ -476,6 +489,8 @@ TableInfo GetTableInfoWithConstraint(absl::string_view constraint_string) { {2, {2, "ternary32", kTernary32}}, {3, {3, "lpm32", kLpm32}}, {4, {4, "optional32", kOptional32}}, + {5, {5, "exact11", kExact11}}, + {6, {6, "optional28", kOptional28}}, }, .keys_by_name = { @@ -483,6 +498,8 @@ TableInfo GetTableInfoWithConstraint(absl::string_view constraint_string) { {"ternary32", {2, "ternary32", kTernary32}}, {"lpm32", {3, "lpm32", kLpm32}}, {"optional32", {4, "optional32", kOptional32}}, + {"exact11", {5, "exact11", kExact11}}, + {"optional28", {6, "optional28", kOptional28}}, }, }; @@ -522,8 +539,8 @@ TEST(EvaluateConstraintSymbolicallyTest, } EXPECT_THAT(EvaluateConstraintSymbolically( *table_info.constraint, table_info.constraint_source, - /*name_to_symbolic_key=*/{}, - /*name_to_symbolic_attribute=*/{}, solver), + /*symbolic_key_by_name=*/{}, + /*symbolic_attribute_by_name=*/{}, solver), StatusIs(absl::StatusCode::kInvalidArgument)); } @@ -544,31 +561,85 @@ TEST_P(ConstraintTest, TableInfo table_info = GetTableInfoWithConstraint(GetParam().constraint_string); - // Constraint type must be boolean to not fail early. - table_info.constraint->mutable_type()->mutable_boolean(); // Add symbolic table keys to symbolic key map. - absl::flat_hash_map name_to_symbolic_key; + absl::flat_hash_map symbolic_key_by_name; for (const auto& [key_name, key_info] : table_info.keys_by_name) { ASSERT_OK_AND_ASSIGN(SymbolicKey key, AddSymbolicKey(key_info, solver)); - name_to_symbolic_key.emplace(key_name, std::move(key)); + symbolic_key_by_name.emplace(key_name, std::move(key)); } // Add symbolic priority to attribute map. absl::flat_hash_map - name_to_symbolic_attribute; + symbolic_attribute_by_name; SymbolicAttribute symbolic_priority = AddSymbolicPriority(solver); - name_to_symbolic_attribute.emplace("priority", std::move(symbolic_priority)); + symbolic_attribute_by_name.emplace(kSymbolicPriorityAttributeName, + std::move(symbolic_priority)); ASSERT_OK_AND_ASSIGN( z3::expr z3_constraint, EvaluateConstraintSymbolically( *table_info.constraint, table_info.constraint_source, - name_to_symbolic_key, name_to_symbolic_attribute, solver)); + symbolic_key_by_name, symbolic_attribute_by_name, solver)); solver.add(z3_constraint); 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. + absl::flat_hash_map symbolic_key_by_name; + for (const auto& [key_name, key_info] : table_info.keys_by_name) { + ASSERT_OK_AND_ASSIGN(SymbolicKey key, AddSymbolicKey(key_info, solver)); + symbolic_key_by_name.emplace(key_name, std::move(key)); + } + + // Add symbolic priority to attribute map. + absl::flat_hash_map + symbolic_attribute_by_name; + SymbolicAttribute symbolic_priority = AddSymbolicPriority(solver); + symbolic_attribute_by_name.emplace(kSymbolicPriorityAttributeName, + std::move(symbolic_priority)); + + ASSERT_OK_AND_ASSIGN( + z3::expr z3_constraint, + EvaluateConstraintSymbolically( + *table_info.constraint, table_info.constraint_source, + symbolic_key_by_name, symbolic_attribute_by_name, 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, symbolic_key_by_name, + symbolic_attribute_by_name)); + + // 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{{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(); +} + INSTANTIATE_TEST_SUITE_P( EvaluateConstraintSatisfiabilityTests, ConstraintTest, testing::ValuesIn(std::vector{ @@ -624,7 +695,7 @@ INSTANTIATE_TEST_SUITE_P( }, { .test_name = "optional_equals_sat", - .constraint_string = "optional32 == 42", + .constraint_string = "optional32 == 1", .is_sat = true, }, { @@ -647,10 +718,280 @@ INSTANTIATE_TEST_SUITE_P( .constraint_string = "::priority > 50", .is_sat = true, }, + { + .test_name = "exact_may_have_odd_bitwidth", + .constraint_string = "exact11 == 137", + .is_sat = true, + }, + { + .test_name = "lpm_can_have_zero_prefix", + .constraint_string = "lpm32::prefix_length == 0", + .is_sat = true, + }, + { + .test_name = "optional28_equals_sat", + .constraint_string = "optional28 == 1", + .is_sat = true, + }, }), [](const testing::TestParamInfo& info) { return SnakeCaseToCamelCase(info.param.test_name); }); +struct FullySpecifiedConstraintTestCase { + std::string test_name; + // A protobuf string representing an boolean AST Expression representing a + // constraint. Must fully specify the entry given below. + std::string constraint_string; + // Should be set with the only entry that can possibly meet the constraint + // string. + 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 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{{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. + absl::flat_hash_map symbolic_key_by_name; + for (const auto& [key_name, key_info] : table_info.keys_by_name) { + ASSERT_OK_AND_ASSIGN(SymbolicKey key, AddSymbolicKey(key_info, solver)); + symbolic_key_by_name.emplace(key_name, std::move(key)); + } + + // Add symbolic priority to attribute map. + absl::flat_hash_map + symbolic_attribute_by_name; + SymbolicAttribute symbolic_priority = AddSymbolicPriority(solver); + symbolic_attribute_by_name.emplace(kSymbolicPriorityAttributeName, + std::move(symbolic_priority)); + + ASSERT_OK_AND_ASSIGN( + z3::expr z3_constraint, + EvaluateConstraintSymbolically( + *table_info.constraint, table_info.constraint_source, + symbolic_key_by_name, symbolic_attribute_by_name, 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, symbolic_key_by_name, + symbolic_attribute_by_name, + [&](absl::string_view key_name) { + return GetParam().keys_to_skip.contains(key_name); + })); + + EXPECT_THAT(concretized_entry, IgnoringRepeatedFieldOrdering(EqualsProto( + GetParam().expected_concretized_entry))); +} + +INSTANTIATE_TEST_SUITE_P( + CheckExactEntryOutput, FullySpecifiedConstraintTest, + testing::ValuesIn(std::vector{ + { + .test_name = "only_equals", + .constraint_string = + "exact11 == 5; exact32 == 5; ::priority == 50; " + "lpm32::prefix_length == 0; ternary32::mask == 0; " + "optional32::mask == 0; optional28::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 = "last_byte_zero_in_exacts", + .constraint_string = + "exact11 == 1280; exact32 == 1280; ::priority == 50; " + "lpm32::prefix_length == 0; ternary32::mask == 0; " + "optional32::mask == 0; optional28::mask == 0;", + .expected_concretized_entry = + ParseTextProtoOrDie(R"pb( + table_id: 1 + match { + field_id: 1 + exact { value: "\005\000" } + } + match { + field_id: 5 + exact { value: "\005\000" } + } + priority: 50 + )pb"), + }, + { + .test_name = "with_inequalities", + .constraint_string = "::priority > 1; ::priority < 3; " + "lpm32::prefix_length == 0; ternary32::mask " + "== 0; optional32::mask == 0; exact11 == 1; " + "exact32 == 1; optional28::mask == 0;", + .expected_concretized_entry = + ParseTextProtoOrDie(R"pb( + table_id: 1 + match { + field_id: 1 + exact { value: "\001" } + } + match { + field_id: 5 + exact { value: "\001" } + } + priority: 2 + )pb"), + }, + { + .test_name = "set_lpm", + .constraint_string = "lpm32 == 5; " + "ternary32::mask == 0; optional32::mask == 0; " + "exact11 == 1; exact32 == 1; ::priority == 1; " + "optional28::mask == 0;", + .expected_concretized_entry = + ParseTextProtoOrDie(R"pb( + table_id: 1 + match { + field_id: 1 + exact { value: "\001" } + } + match { + field_id: 3 + lpm { value: "\005" prefix_len: 32 } + } + match { + field_id: 5 + exact { value: "\001" } + } + priority: 1 + )pb"), + }, + { + .test_name = "set_ternary", + .constraint_string = + "ternary32 == 5; " + "lpm32::prefix_length == 0; optional32::mask == 0; exact11 == " + "1; exact32 == 1; ::priority == 1; optional28::mask == 0;", + .expected_concretized_entry = + ParseTextProtoOrDie(R"pb( + table_id: 1 + match { + field_id: 1 + exact { value: "\001" } + } + match { + field_id: 2 + ternary { value: "\005" mask: "\377\377\377\377" } + } + match { + field_id: 5 + exact { value: "\001" } + } + priority: 1 + )pb"), + }, + { + .test_name = "set_optional32", + .constraint_string = + "optional32 == 5; " + "lpm32::prefix_length == 0; ternary32::mask == 0; exact11 == " + "1; exact32 == 1; ::priority == 1; optional28::mask == 0;", + .expected_concretized_entry = + ParseTextProtoOrDie(R"pb( + table_id: 1 + match { + field_id: 1 + exact { value: "\001" } + } + match { + field_id: 4 + optional { value: "\005" } + } + match { + field_id: 5 + exact { value: "\001" } + } + priority: 1 + )pb"), + }, + { + .test_name = "set_optional28", + .constraint_string = + "optional28 == 5; " + "lpm32::prefix_length == 0; ternary32::mask == 0; exact11 == " + "1; exact32 == 1; ::priority == 1; optional32::mask == 0;", + .expected_concretized_entry = + ParseTextProtoOrDie(R"pb( + table_id: 1 + match { + field_id: 1 + exact { value: "\001" } + } + match { + field_id: 5 + exact { value: "\001" } + } + match { + field_id: 6 + optional { value: "\005" } + } + priority: 1 + )pb"), + }, + { + .test_name = "skip_optionals", + .constraint_string = + "lpm32::prefix_length == 0; ternary32::mask == 0; exact11 == 1;" + "exact32 == 1; ::priority == 1;", + .expected_concretized_entry = + ParseTextProtoOrDie(R"pb( + table_id: 1 + match { + field_id: 1 + exact { value: "\001" } + } + match { + field_id: 5 + exact { value: "\001" } + } + priority: 1 + )pb"), + .keys_to_skip = {"optional32", "optional28"}, + }, + }), + [](const testing::TestParamInfo& info) { + return SnakeCaseToCamelCase(info.param.test_name); + }); } // namespace } // namespace p4_constraints