From 87a786b500e517cd6bed851cbe21191f7341cef3 Mon Sep 17 00:00:00 2001 From: PINS Team Date: Tue, 22 Aug 2023 16:17:45 +0000 Subject: [PATCH] PUBLIC: [P4-Constraints] Aggregate two symbolic maps into a single struct. This is in preparation for returning them from a 'construct everything' function. PiperOrigin-RevId: 559132097 --- .../backend/symbolic_interpreter.cc | 80 ++++++++----------- p4_constraints/backend/symbolic_interpreter.h | 36 ++++----- .../backend/symbolic_interpreter_test.cc | 70 +++++++--------- 3 files changed, 79 insertions(+), 107 deletions(-) diff --git a/p4_constraints/backend/symbolic_interpreter.cc b/p4_constraints/backend/symbolic_interpreter.cc index f75c7a0..127c426 100644 --- a/p4_constraints/backend/symbolic_interpreter.cc +++ b/p4_constraints/backend/symbolic_interpreter.cc @@ -300,22 +300,16 @@ absl::StatusOr EvalTypeCast( // Forward declared to allow mutual-recursion. absl::StatusOr EvalSymbolically( const ast::Expression& expr, const ConstraintSource& constraint_source, - const absl::flat_hash_map& symbolic_key_by_name, - const absl::flat_hash_map& - symbolic_attribute_by_name, - z3::solver& solver); + const SymbolicEnvironment& environment, z3::solver& solver); template -absl::StatusOr EvalSymbolicallyTo( - const ast::Expression& expr, const ConstraintSource& constraint_source, - const absl::flat_hash_map& symbolic_key_by_name, - const absl::flat_hash_map& - symbolic_attribute_by_name, - z3::solver& solver) { +absl::StatusOr EvalSymbolicallyTo(const ast::Expression& expr, + const ConstraintSource& constraint_source, + const SymbolicEnvironment& environment, + z3::solver& solver) { ASSIGN_OR_RETURN( SymbolicEvalResult result, - EvalSymbolically(expr, constraint_source, symbolic_key_by_name, - symbolic_attribute_by_name, solver)); + EvalSymbolically(expr, constraint_source, environment, solver)); T* t = std::get_if(&result); if (t == nullptr) { @@ -330,10 +324,7 @@ absl::StatusOr EvalSymbolicallyTo( absl::StatusOr EvalSymbolically( const ast::Expression& expr, const ConstraintSource& constraint_source, - const absl::flat_hash_map& symbolic_key_by_name, - const absl::flat_hash_map& - symbolic_attribute_by_name, - z3::solver& solver) { + const SymbolicEnvironment& environment, z3::solver& solver) { switch (expr.expression_case()) { case ast::Expression::kBooleanConstant: return solver.ctx().bool_val(expr.boolean_constant()); @@ -342,8 +333,7 @@ absl::StatusOr EvalSymbolically( ASSIGN_OR_RETURN( z3::expr bool_result, EvalSymbolicallyTo(expr.boolean_negation(), - constraint_source, symbolic_key_by_name, - symbolic_attribute_by_name, solver)); + constraint_source, environment, solver)); return !bool_result; } @@ -354,15 +344,14 @@ absl::StatusOr EvalSymbolically( ASSIGN_OR_RETURN( z3::expr int_result, EvalSymbolicallyTo(expr.arithmetic_negation(), - constraint_source, symbolic_key_by_name, - symbolic_attribute_by_name, solver)); + constraint_source, environment, solver)); return -int_result; } case ast::Expression::kKey: { - ASSIGN_OR_RETURN( - const SymbolicKey* key, - gutils::FindPtrOrStatus(symbolic_key_by_name, expr.key())); + ASSIGN_OR_RETURN(const SymbolicKey* key, + gutils::FindPtrOrStatus(environment.symbolic_key_by_name, + expr.key())); return *key; } @@ -371,7 +360,7 @@ absl::StatusOr EvalSymbolically( // moment. If there were, this logic would need to change. ASSIGN_OR_RETURN( const SymbolicKey* key, - gutils::FindPtrOrStatus(symbolic_key_by_name, + gutils::FindPtrOrStatus(environment.symbolic_key_by_name, expr.field_access().expr().key())); return GetFieldAccess(*key, expr.field_access().field()); } @@ -380,20 +369,20 @@ absl::StatusOr EvalSymbolically( // All attributes should be in the map. ASSIGN_OR_RETURN( const SymbolicAttribute* attribute, - gutils::FindPtrOrStatus(symbolic_attribute_by_name, + gutils::FindPtrOrStatus(environment.symbolic_attribute_by_name, expr.attribute_access().attribute_name())); return attribute->value; } case ast::Expression::kBinaryExpression: { - ASSIGN_OR_RETURN(SymbolicEvalResult left_result, - EvalSymbolically(expr.binary_expression().left(), - constraint_source, symbolic_key_by_name, - symbolic_attribute_by_name, solver)); - ASSIGN_OR_RETURN(SymbolicEvalResult right_result, - EvalSymbolically(expr.binary_expression().right(), - constraint_source, symbolic_key_by_name, - symbolic_attribute_by_name, solver)); + ASSIGN_OR_RETURN( + SymbolicEvalResult left_result, + EvalSymbolically(expr.binary_expression().left(), constraint_source, + environment, solver)); + ASSIGN_OR_RETURN( + SymbolicEvalResult right_result, + EvalSymbolically(expr.binary_expression().right(), constraint_source, + environment, solver)); return EvalBinaryExpression(left_result, expr.binary_expression().binop(), right_result); } @@ -402,8 +391,7 @@ absl::StatusOr EvalSymbolically( ASSIGN_OR_RETURN( z3::expr pre_type_cast_result, EvalSymbolicallyTo(expr.type_cast(), constraint_source, - symbolic_key_by_name, - symbolic_attribute_by_name, solver)); + environment, solver)); return EvalTypeCast(pre_type_cast_result, expr.type(), solver); } @@ -668,10 +656,7 @@ SymbolicAttribute AddSymbolicPriority(z3::solver& solver) { absl::StatusOr EvaluateConstraintSymbolically( const ast::Expression& constraint, const ConstraintSource& constraint_source, - const absl::flat_hash_map& symbolic_key_by_name, - const absl::flat_hash_map& - symbolic_attribute_by_name, - z3::solver& solver) { + const SymbolicEnvironment& environment, z3::solver& solver) { // TODO(b/296865478): Run the typechecker here instead when it is idempotent. if (!constraint.type().has_boolean()) { return gutils::InvalidArgumentErrorBuilder(GUTILS_LOC) @@ -679,15 +664,12 @@ absl::StatusOr EvaluateConstraintSymbolically( << constraint.DebugString(); } return EvalSymbolicallyTo(constraint, constraint_source, - symbolic_key_by_name, - symbolic_attribute_by_name, solver); + environment, 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, + const SymbolicEnvironment& environment, std::function(absl::string_view key_name)> skip_key_named) { p4::v1::TableEntry table_entry; @@ -698,8 +680,9 @@ absl::StatusOr ConcretizeEntry( 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( + const SymbolicKey* symbolic_key, + gutils::FindPtrOrStatus(environment.symbolic_key_by_name, key_name)); ASSIGN_OR_RETURN(std::optional match, ConcretizeKey(*symbolic_key, key_info, model)); @@ -710,8 +693,9 @@ absl::StatusOr ConcretizeEntry( } // Set priority if it exists. - if (auto priority_key = gutils::FindPtrOrStatus( - symbolic_attribute_by_name, kSymbolicPriorityAttributeName); + if (auto priority_key = + gutils::FindPtrOrStatus(environment.symbolic_attribute_by_name, + kSymbolicPriorityAttributeName); priority_key.ok()) { if (model.has_interp((*priority_key)->value.decl())) { table_entry.set_priority( diff --git a/p4_constraints/backend/symbolic_interpreter.h b/p4_constraints/backend/symbolic_interpreter.h index 4b8753f..6ab0f86 100644 --- a/p4_constraints/backend/symbolic_interpreter.h +++ b/p4_constraints/backend/symbolic_interpreter.h @@ -81,6 +81,12 @@ constexpr char kSymbolicPriorityAttributeName[] = "priority"; // Z3 representation of a single match key in a P4 table entry. using SymbolicKey = std::variant; +struct SymbolicEnvironment { + absl::flat_hash_map symbolic_key_by_name; + absl::flat_hash_map + symbolic_attribute_by_name; +}; + // -- Main Functions ----------------------------------------------------------- // Creates a `SymbolicKey` that symbolically represents the match field key @@ -112,35 +118,29 @@ absl::StatusOr AddSymbolicKey(const KeyInfo& key, SymbolicAttribute AddSymbolicPriority(z3::solver& solver); // Translates a P4-Constraints expression into a Z3 expression using the -// `symbolic_key_by_name` and `symbolic_attribute_by_name` mappings to interpret -// keys and attributes respectively in the constraint. All symbolic keys -// and attributes must already exist in the solver's context. -// Invalid or not properly type-checked constraints will yield an -// InvalidArgumentError or InternalError. The `constraint_source` is used to +// `environment` maps to interpret keys and attributes in the +// constraint. All symbolic keys and attributes must already exist in the +// solver's context. Invalid or not properly type-checked constraints will yield +// an 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 (as opposed to multiple). absl::StatusOr EvaluateConstraintSymbolically( const ast::Expression& constraint, const ConstraintSource& constraint_source, - const absl::flat_hash_map& symbolic_key_by_name, - const absl::flat_hash_map& - symbolic_attribute_by_name, - z3::solver& solver); + const SymbolicEnvironment& environment, 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). +// 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 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, + const SymbolicEnvironment& environment, std::function(absl::string_view key_name)> skip_key_named = [](absl::string_view key_name) { return false; }); diff --git a/p4_constraints/backend/symbolic_interpreter_test.cc b/p4_constraints/backend/symbolic_interpreter_test.cc index 69cb42f..80a8ac8 100644 --- a/p4_constraints/backend/symbolic_interpreter_test.cc +++ b/p4_constraints/backend/symbolic_interpreter_test.cc @@ -537,10 +537,9 @@ TEST(EvaluateConstraintSymbolicallyTest, for (const auto& [name, key] : table_info.keys_by_name) { ASSERT_OK(AddSymbolicKey(key, solver)); } - EXPECT_THAT(EvaluateConstraintSymbolically( - *table_info.constraint, table_info.constraint_source, - /*symbolic_key_by_name=*/{}, - /*symbolic_attribute_by_name=*/{}, solver), + EXPECT_THAT(EvaluateConstraintSymbolically(*table_info.constraint, + table_info.constraint_source, + /*environment=*/{}, solver), StatusIs(absl::StatusCode::kInvalidArgument)); } @@ -563,24 +562,21 @@ TEST_P(ConstraintTest, GetTableInfoWithConstraint(GetParam().constraint_string); // Add symbolic table keys to symbolic key map. - absl::flat_hash_map symbolic_key_by_name; + SymbolicEnvironment environment; 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)); + environment.symbolic_key_by_name.insert({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)); + 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, - symbolic_key_by_name, symbolic_attribute_by_name, solver)); + ASSERT_OK_AND_ASSIGN(z3::expr z3_constraint, + EvaluateConstraintSymbolically( + *table_info.constraint, table_info.constraint_source, + environment, solver)); solver.add(z3_constraint); EXPECT_EQ(solver.check(), GetParam().is_sat ? z3::sat : z3::unsat); } @@ -596,31 +592,27 @@ TEST_P(ConstraintTest, ConcretizeEntryGivesEntrySatisfyingConstraints) { GetTableInfoWithConstraint(GetParam().constraint_string); // Add symbolic table keys to symbolic key map. - absl::flat_hash_map symbolic_key_by_name; + SymbolicEnvironment environment; 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)); + environment.symbolic_key_by_name.insert({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)); + 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, - symbolic_key_by_name, symbolic_attribute_by_name, solver)); + 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, symbolic_key_by_name, - symbolic_attribute_by_name)); + 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()) { @@ -777,31 +769,27 @@ TEST_P(FullySpecifiedConstraintTest, ConcretizeEntryGivesExactEntry) { } // Add symbolic table keys to symbolic key map. - absl::flat_hash_map symbolic_key_by_name; + SymbolicEnvironment environment; 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)); + environment.symbolic_key_by_name.insert({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)); + 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, - symbolic_key_by_name, symbolic_attribute_by_name, solver)); + 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, symbolic_key_by_name, - symbolic_attribute_by_name, + ConcretizeEntry(solver.get_model(), table_info, environment, [&](absl::string_view key_name) { return GetParam().keys_to_skip.contains(key_name); }));