Skip to content

Commit

Permalink
PUBLIC: [P4-Constraints] Add top-level function to populate solver an…
Browse files Browse the repository at this point in the history 
…d symbolic variable maps using TableInfo. (#110)

PiperOrigin-RevId: 559219621

Co-authored-by: PINS Team <[email protected]>
  • Loading branch information
@jonathan-dilorenzo
jonathan-dilorenzo and PINS Team authored Oct 4, 2023
1 parent 7390f6d commit e097da9
Show file tree
Hide file tree
Showing 3 changed files with 238 additions and 43 deletions.
47 changes: 47 additions & 0 deletions p4_constraints/backend/symbolic_interpreter.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -573,6 +573,8 @@ absl::StatusOr<std::optional<p4::v1::FieldMatch>> ConcretizeKey(

} // namespace

namespace internal_interpreter {

absl::StatusOr<SymbolicKey> AddSymbolicKey(const KeyInfo& key,
z3::solver& solver) {
ASSIGN_OR_RETURN(int bitwidth, ast::TypeBitwidthOrStatus(key.type));
Expand Down Expand Up @@ -667,6 +669,8 @@ absl::StatusOr<z3::expr> EvaluateConstraintSymbolically(
environment, solver);
}

} // namespace internal_interpreter

absl::StatusOr<p4::v1::TableEntry> ConcretizeEntry(
const z3::model& model, const TableInfo& table_info,
const SymbolicEnvironment& environment,
Expand Down Expand Up @@ -711,6 +715,49 @@ absl::StatusOr<p4::v1::TableEntry> ConcretizeEntry(
return table_entry;
}

absl::StatusOr<SymbolicEnvironment> EncodeValidTableEntryInZ3(
const TableInfo& table, z3::solver& solver,
std::function<absl::StatusOr<bool>(absl::string_view key_name)>
skip_key_named) {
SymbolicEnvironment environment;
environment.symbolic_key_by_name.reserve(table.keys_by_name.size());

// Add keys to solver and map and determine whether the table needs a
// priority.
bool requires_priority = false;
for (const auto& [key_name, key_info] : table.keys_by_name) {
if (key_info.type.has_ternary() || key_info.type.has_optional_match()) {
// In P4Runtime, all tables with ternaries or optionals require priorities
// for their entries.
requires_priority = true;
}
ASSIGN_OR_RETURN(bool key_should_be_skipped, 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)});
}

if (requires_priority) {
SymbolicAttribute priority =
internal_interpreter::AddSymbolicPriority(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);
}

return environment;
}

absl::StatusOr<z3::expr> GetValue(const SymbolicKey& symbolic_key) {
return GetFieldAccess(symbolic_key, "value");
}
Expand Down
113 changes: 70 additions & 43 deletions p4_constraints/backend/symbolic_interpreter.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,54 +89,35 @@ struct SymbolicEnvironment {

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

// Creates a `SymbolicKey` that symbolically represents the match field key
// given by `key` in Z3 and adds the match to the context in `solver`. Also adds
// two forms of well-formedness constraints for that `key`:
// 1) Domain constraints, enforcing the bitwidth of the various `value`s and the
// allowed values for `prefix_length` (for LPMs) and `mask` (for optionals).
// 2) Canonicity constraints, enforcing that `value`s and their `mask`s or
// `prefix_length`s correspond to ensure compatibility with P4Runtime. E.g.
// on a switch, the following value and mask pairs behave identically, but we
// disallow the second with canonicity constraints:
// - 10 & 10
// - 11 & 10
// This is required to concretize symbolic keys to valid P4Runtime keys that
// still satisfy any p4-constraints.
//
// Expects `key` to have a non-zero bitwidth.
// NOTE: This API will only work correctly if the `solver` represents a single
// table entry (as opposed to multiple).
absl::StatusOr<SymbolicKey> AddSymbolicKey(const KeyInfo& key,
z3::solver& solver);

// Creates and returns a attribute key for table priority and constrains it to
// be between 1 and MAX_INT32 (inclusive).
// 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 (as opposed to multiple).
SymbolicAttribute AddSymbolicPriority(z3::solver& solver);

// Translates a P4-Constraints expression into a Z3 expression using the
// `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 SymbolicEnvironment& environment, z3::solver& solver);
// 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<SymbolicEnvironment> EncodeValidTableEntryInZ3(
const TableInfo& table, z3::solver& solver,
std::function<absl::StatusOr<bool>(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 will only work
// correctly if the `model` represents a single table entry (as opposed to
// multiple).
// 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<p4::v1::TableEntry> ConcretizeEntry(
const z3::model& model, const TableInfo& table_info,
Expand Down Expand Up @@ -218,6 +199,52 @@ inline std::ostream& operator<<(std::ostream& os,
return os << absl::StrCat(result);
}

// Exposed for testing only.
namespace internal_interpreter {

// Creates a `SymbolicKey` that symbolically represents the match field key
// given by `key` in Z3 and adds the match to the context in `solver`. Also adds
// two forms of well-formedness constraints for that `key`:
// 1) Domain constraints, enforcing the bitwidth of the various `value`s and the
// allowed values for `prefix_length` (for LPMs) and `mask` (for optionals).
// 2) Canonicity constraints, enforcing that `value`s and their `mask`s or
// `prefix_length`s correspond to ensure compatibility with P4Runtime. E.g.
// on a switch, the following value and mask pairs behave identically, but we
// disallow the second with canonicity constraints:
// - 10 & 10
// - 11 & 10
// This is required to concretize symbolic keys to valid P4Runtime keys that
// still satisfy any p4-constraints.
//
// Expects `key` to have a non-zero bitwidth.
// NOTE: This API will only work correctly if the `solver` represents a single
// table entry (as opposed to multiple).
absl::StatusOr<SymbolicKey> AddSymbolicKey(const KeyInfo& key,
z3::solver& solver);

// Creates and returns a attribute key for table priority and constrains it to
// be between 1 and MAX_INT32 (inclusive).
// 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 (as opposed to multiple).
SymbolicAttribute AddSymbolicPriority(z3::solver& solver);

// Translates a P4-Constraints expression into a Z3 expression using the
// `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 SymbolicEnvironment& environment, z3::solver& solver);

} // namespace internal_interpreter

} // namespace p4_constraints

#endif // P4_CONSTRAINTS_BACKEND_SYMBOLIC_INTERPRETER_H_
121 changes: 121 additions & 0 deletions p4_constraints/backend/symbolic_interpreter_test.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
#include <gmock/gmock.h>
#include <gtest/gtest.h>

#include <optional>
#include <string>
#include <utility>
#include <vector>
Expand Down Expand Up @@ -38,6 +39,10 @@ using ::gutils::testing::status::IsOkAndHolds;
using ::gutils::testing::status::StatusIs;
using ::p4_constraints::ast::Expression;
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.
Expand Down Expand Up @@ -632,6 +637,84 @@ TEST_P(ConstraintTest, ConcretizeEntryGivesEntrySatisfyingConstraints) {
<< "\nAnd solver state: " << solver.to_smt2();
}

TEST(EncodeValidTableEntryInZ3Test, WorksWithoutConstraints) {
z3::context solver_context;
z3::solver solver(solver_context);

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);
}

TEST(EncodeValidTableEntryInZ3Test, WorksWithoutPriority) {
z3::context solver_context;
z3::solver solver(solver_context);

TableInfo table_info = GetTableInfoWithConstraint("true");

// Remove the ternaries and optionals, so that no priority is required.
std::vector<KeyInfo> keys_to_remove;
for (const auto& [key_name, key_info] : table_info.keys_by_name) {
if (key_info.type.has_ternary() || key_info.type.has_optional_match()) {
keys_to_remove.push_back(key_info);
}
}
for (const KeyInfo& key : keys_to_remove) {
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);
}

TEST_P(ConstraintTest, EncodeValidTableEntryInZ3CheckSatAndUnsatCorrectness) {
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));
EXPECT_EQ(solver.check(), GetParam().is_sat ? z3::sat : z3::unsat);
}

TEST_P(ConstraintTest, EncodeValidTableEntryInZ3AndConcretizeEntry) {
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));

// The empty string signifies that the entry doesn't violate the constraint.
ConstraintInfo context{{table_info.id, table_info}};
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<ConstraintTestCase>{
Expand Down Expand Up @@ -798,6 +881,44 @@ TEST_P(FullySpecifiedConstraintTest, ConcretizeEntryGivesExactEntry) {
GetParam().expected_concretized_entry)));
}

TEST_P(FullySpecifiedConstraintTest,
EncodeValidTableEntryInZ3AndConcretizeEntryGivesExactEntry) {
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();
}

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,
[&](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<FullySpecifiedConstraintTestCase>{
Expand Down

0 comments on commit e097da9

Please sign in to comment.