Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

PUBLIC: [P4-Constraints] Aggregate two symbolic maps into a single struct. #109

Merged
merged 1 commit into from
Sep 27, 2023
Merged

PUBLIC: [P4-Constraints] Aggregate two symbolic maps into a single struct. #109

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
80 changes: 32 additions & 48 deletions p4_constraints/backend/symbolic_interpreter.cc
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading