Skip to content

Commit

Permalink
PUBLIC: [P4-Constraints] Aggregate two symbolic maps into a single st…
Browse files Browse the repository at this point in the history 
…ruct. (#109)

This is in preparation for returning them from a 'construct everything' function.

PiperOrigin-RevId: 559132097

Co-authored-by: PINS Team <[email protected]>
  • Loading branch information
@jonathan-dilorenzo
jonathan-dilorenzo and PINS Team authored Sep 27, 2023
1 parent d9c1108 commit 7390f6d
Show file tree
Hide file tree
Showing 3 changed files with 79 additions and 107 deletions.
80 changes: 32 additions & 48 deletions p4_constraints/backend/symbolic_interpreter.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -300,22 +300,16 @@ absl::StatusOr<SymbolicEvalResult> EvalTypeCast(
// Forward declared to allow mutual-recursion.
absl::StatusOr<SymbolicEvalResult> EvalSymbolically(
const ast::Expression& expr, const ConstraintSource& constraint_source,
const absl::flat_hash_map<std::string, SymbolicKey>& symbolic_key_by_name,
const absl::flat_hash_map<std::string, SymbolicAttribute>&
symbolic_attribute_by_name,
z3::solver& solver);
const SymbolicEnvironment& environment, z3::solver& solver);

template <class T>
absl::StatusOr<T> EvalSymbolicallyTo(
const ast::Expression& expr, const ConstraintSource& constraint_source,
const absl::flat_hash_map<std::string, SymbolicKey>& symbolic_key_by_name,
const absl::flat_hash_map<std::string, SymbolicAttribute>&
symbolic_attribute_by_name,
z3::solver& solver) {
absl::StatusOr<T> 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<T>(&result);
if (t == nullptr) {
Expand All @@ -330,10 +324,7 @@ absl::StatusOr<T> EvalSymbolicallyTo(

absl::StatusOr<SymbolicEvalResult> EvalSymbolically(
const ast::Expression& expr, const ConstraintSource& constraint_source,
const absl::flat_hash_map<std::string, SymbolicKey>& symbolic_key_by_name,
const absl::flat_hash_map<std::string, SymbolicAttribute>&
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());
Expand All @@ -342,8 +333,7 @@ absl::StatusOr<SymbolicEvalResult> EvalSymbolically(
ASSIGN_OR_RETURN(
z3::expr bool_result,
EvalSymbolicallyTo<z3::expr>(expr.boolean_negation(),
constraint_source, symbolic_key_by_name,
symbolic_attribute_by_name, solver));
constraint_source, environment, solver));
return !bool_result;
}

Expand All @@ -354,15 +344,14 @@ absl::StatusOr<SymbolicEvalResult> EvalSymbolically(
ASSIGN_OR_RETURN(
z3::expr int_result,
EvalSymbolicallyTo<z3::expr>(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;
}

Expand All @@ -371,7 +360,7 @@ absl::StatusOr<SymbolicEvalResult> 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());
}
Expand All @@ -380,20 +369,20 @@ absl::StatusOr<SymbolicEvalResult> 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);
}
Expand All @@ -402,8 +391,7 @@ absl::StatusOr<SymbolicEvalResult> EvalSymbolically(
ASSIGN_OR_RETURN(
z3::expr pre_type_cast_result,
EvalSymbolicallyTo<z3::expr>(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);
}

Expand Down Expand Up @@ -668,26 +656,20 @@ SymbolicAttribute AddSymbolicPriority(z3::solver& solver) {
absl::StatusOr<z3::expr> EvaluateConstraintSymbolically(
const ast::Expression& constraint,
const ConstraintSource& constraint_source,
const absl::flat_hash_map<std::string, SymbolicKey>& symbolic_key_by_name,
const absl::flat_hash_map<std::string, SymbolicAttribute>&
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)
<< "expected a constraint of type boolean, but got:\n"
<< constraint.DebugString();
}
return EvalSymbolicallyTo<z3::expr>(constraint, constraint_source,
symbolic_key_by_name,
symbolic_attribute_by_name, solver);
environment, solver);
}

absl::StatusOr<p4::v1::TableEntry> ConcretizeEntry(
const z3::model& model, const TableInfo& table_info,
const absl::flat_hash_map<std::string, SymbolicKey>& symbolic_key_by_name,
const absl::flat_hash_map<std::string, SymbolicAttribute>&
symbolic_attribute_by_name,
const SymbolicEnvironment& environment,
std::function<absl::StatusOr<bool>(absl::string_view key_name)>
skip_key_named) {
p4::v1::TableEntry table_entry;
Expand All @@ -698,8 +680,9 @@ absl::StatusOr<p4::v1::TableEntry> 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<p4::v1::FieldMatch> match,
ConcretizeKey(*symbolic_key, key_info, model));

Expand All @@ -710,8 +693,9 @@ absl::StatusOr<p4::v1::TableEntry> 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(
Expand Down
36 changes: 18 additions & 18 deletions p4_constraints/backend/symbolic_interpreter.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,12 @@ constexpr char kSymbolicPriorityAttributeName[] = "priority";
// Z3 representation of a single match key in a P4 table entry.
using SymbolicKey = std::variant<SymbolicExact, SymbolicTernary, SymbolicLpm>;

struct SymbolicEnvironment {
absl::flat_hash_map<std::string, SymbolicKey> symbolic_key_by_name;
absl::flat_hash_map<std::string, SymbolicAttribute>
symbolic_attribute_by_name;
};

// -- Main Functions -----------------------------------------------------------

// Creates a `SymbolicKey` that symbolically represents the match field key
Expand Down Expand Up @@ -112,35 +118,29 @@ absl::StatusOr<SymbolicKey> 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<z3::expr> EvaluateConstraintSymbolically(
const ast::Expression& constraint,
const ConstraintSource& constraint_source,
const absl::flat_hash_map<std::string, SymbolicKey>& symbolic_key_by_name,
const absl::flat_hash_map<std::string, SymbolicAttribute>&
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<p4::v1::TableEntry> ConcretizeEntry(
const z3::model& model, const TableInfo& table_info,
const absl::flat_hash_map<std::string, SymbolicKey>& symbolic_key_by_name,
const absl::flat_hash_map<std::string, SymbolicAttribute>&
symbolic_attribute_by_name,
const SymbolicEnvironment& environment,
std::function<absl::StatusOr<bool>(absl::string_view key_name)>
skip_key_named = [](absl::string_view key_name) { return false; });

Expand Down
70 changes: 29 additions & 41 deletions p4_constraints/backend/symbolic_interpreter_test.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
}

Expand All @@ -563,24 +562,21 @@ TEST_P(ConstraintTest,
GetTableInfoWithConstraint(GetParam().constraint_string);

// Add symbolic table keys to symbolic key map.
absl::flat_hash_map<std::string, SymbolicKey> 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<std::string, SymbolicAttribute>
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);
}
Expand All @@ -596,31 +592,27 @@ TEST_P(ConstraintTest, ConcretizeEntryGivesEntrySatisfyingConstraints) {
GetTableInfoWithConstraint(GetParam().constraint_string);

// Add symbolic table keys to symbolic key map.
absl::flat_hash_map<std::string, SymbolicKey> 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<std::string, SymbolicAttribute>
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()) {
Expand Down Expand Up @@ -777,31 +769,27 @@ TEST_P(FullySpecifiedConstraintTest, ConcretizeEntryGivesExactEntry) {
}

// Add symbolic table keys to symbolic key map.
absl::flat_hash_map<std::string, SymbolicKey> 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<std::string, SymbolicAttribute>
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);
}));
Expand Down

0 comments on commit 7390f6d

Please sign in to comment.