Skip to content

Commit

Permalink
PUBLIC:[p4_constraint] Refactor Constraint solver into a class
Browse files Browse the repository at this point in the history 
PiperOrigin-RevId: 627162779
  • Loading branch information
@verios-google
PINS Team authored and verios-google committed Apr 29, 2024
1 parent f81f1de commit fa64aec
Show file tree
Hide file tree
Showing 5 changed files with 406 additions and 245 deletions.
2 changes: 2 additions & 0 deletions p4_constraints/backend/BUILD.bazel
View file
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,8 @@ cc_library(
"//p4_constraints:ast",
"//p4_constraints:ast_cc_proto",
"//p4_constraints:constraint_source",
"//p4_constraints/frontend:constraint_kind",
"//p4_constraints/frontend:parser",
"@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
"@com_github_z3prover_z3//:api",
"@com_google_absl//absl/container:flat_hash_map",
Expand Down
106 changes: 79 additions & 27 deletions p4_constraints/backend/symbolic_interpreter.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,10 @@
#include "p4_constraints/ast.pb.h"
#include "p4_constraints/backend/constraint_info.h"
#include "p4_constraints/backend/errors.h"
#include "p4_constraints/backend/type_checker.h"
#include "p4_constraints/constraint_source.h"
#include "p4_constraints/frontend/constraint_kind.h"
#include "p4_constraints/frontend/parser.h"
#include "z3++.h"

namespace p4_constraints {
Expand Down Expand Up @@ -676,22 +679,24 @@ absl::StatusOr<z3::expr> EvaluateConstraintSymbolically(

} // namespace internal_interpreter

absl::StatusOr<p4::v1::TableEntry> ConcretizeEntry(
const z3::model& model, const TableInfo& table_info,
const SymbolicEnvironment& environment,
std::function<absl::StatusOr<bool>(absl::string_view key_name)>
skip_key_named) {
absl::StatusOr<p4::v1::TableEntry> ConstraintSolver::ConcretizeEntry() {
if (solver_.check() != z3::sat) {
return gutils::InternalErrorBuilder(GUTILS_LOC)
<< "Constraints are not satisfiable.";
}

z3::model model = solver_.get_model();
p4::v1::TableEntry table_entry;
table_entry.set_table_id(table_info.id);
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));
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(environment.symbolic_key_by_name, key_name));
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 @@ -703,7 +708,7 @@ absl::StatusOr<p4::v1::TableEntry> ConcretizeEntry(

// Set priority if it exists.
if (auto priority_key =
gutils::FindPtrOrStatus(environment.symbolic_attribute_by_name,
gutils::FindPtrOrStatus(environment_.symbolic_attribute_by_name,
kSymbolicPriorityAttributeName);
priority_key.ok()) {
if (model.has_interp((*priority_key)->value.decl())) {
Expand All @@ -720,12 +725,53 @@ absl::StatusOr<p4::v1::TableEntry> ConcretizeEntry(
return table_entry;
}

absl::StatusOr<SymbolicEnvironment> EncodeValidTableEntryInZ3(
const TableInfo& table, z3::solver& solver,
absl::StatusOr<bool> ConstraintSolver::AddConstraint(
const ast::Expression& constraint,
const ConstraintSource& constraint_source) {
if (solver_.check() != z3::sat) {
return gutils::InternalErrorBuilder(GUTILS_LOC)
<< "Stored constraints are unsatisfiable. Constraint solver must "
"hold a satisfiable constraint at all times.";
};

ASSIGN_OR_RETURN(z3::expr z3_constraint,
internal_interpreter::EvaluateConstraintSymbolically(
constraint, constraint_source, environment_, solver_));
solver_.push();
solver_.add(z3_constraint);
if (solver_.check() != z3::sat) {
solver_.pop();
return false;
}
return true;
};

absl::StatusOr<bool> ConstraintSolver::AddConstraint(
absl::string_view constraint_string) {
ast::SourceLocation source_location;
source_location.set_table_name(table_info_.name);

ConstraintSource constraint_source{
.constraint_string = std::string(constraint_string),
.constraint_location = source_location,
};

ASSIGN_OR_RETURN(
ast::Expression constraint_ast,
ParseConstraint(ConstraintKind::kTableConstraint, constraint_source));

RETURN_IF_ERROR(InferAndCheckTypes(&constraint_ast, table_info_));

return ConstraintSolver::AddConstraint(constraint_ast, constraint_source);
}

absl::StatusOr<ConstraintSolver> ConstraintSolver::Create(
const TableInfo& table,
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());
ConstraintSolver constraint_solver = ConstraintSolver();
constraint_solver.table_info_ = std::move(table);
constraint_solver.skip_key_named_ = std::move(skip_key_named);

// Add keys to solver and map and determine whether the table needs a
// priority.
Expand All @@ -736,31 +782,37 @@ absl::StatusOr<SymbolicEnvironment> EncodeValidTableEntryInZ3(
// for their entries.
requires_priority = true;
}
ASSIGN_OR_RETURN(bool key_should_be_skipped, skip_key_named(key_name));
ASSIGN_OR_RETURN(bool key_should_be_skipped,
constraint_solver.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)});
ASSIGN_OR_RETURN(SymbolicKey key, internal_interpreter::AddSymbolicKey(
key_info, constraint_solver.solver_));
constraint_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(
internal_interpreter::AddSymbolicPriority(constraint_solver.solver_);
constraint_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);
ASSIGN_OR_RETURN(bool modeled_constraint_added,
constraint_solver.AddConstraint(*table.constraint,
table.constraint_source));
if (!modeled_constraint_added) {
return gutils::InvalidArgumentErrorBuilder(GUTILS_LOC)
<< "TableInfo provided an unsatisfiable constraint. "
"ConstraintSolver must contain a satisfiable constraint at all "
"times so creation failed.\n Unsatisfiable Constraint: "
<< table.constraint_source.constraint_string;
}
}

return environment;
return constraint_solver;
}

absl::StatusOr<z3::expr> GetValue(const SymbolicKey& symbolic_key) {
Expand Down
92 changes: 55 additions & 37 deletions p4_constraints/backend/symbolic_interpreter.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@
#define P4_CONSTRAINTS_BACKEND_SYMBOLIC_INTERPRETER_H_

#include <functional>
#include <memory>
#include <ostream>
#include <string>
#include <variant>
Expand Down Expand Up @@ -87,43 +88,60 @@ struct SymbolicEnvironment {
symbolic_attribute_by_name;
};

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

// 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 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,
const SymbolicEnvironment& environment,
std::function<absl::StatusOr<bool>(absl::string_view key_name)>
skip_key_named = [](absl::string_view key_name) { return false; });
// -- Main Class ---------------------------------------------------------------

// A solver for constraints on a table.
// NOTE: Encodes a single table entry for the table given to the constructor. A
// single instantiation can not be used to encode multiple entries.
class ConstraintSolver {
public:
// Constructs a ConstraintSolver representing an entry for `table` that
// respects its P4-Constraints and is well-formed according to the P4Runtime
// specification. An entry encoded by the resulting ConstraintSolver does not
// include any `key` for which `skip_key_named(key)` is true.
static absl::StatusOr<ConstraintSolver> Create(
const TableInfo& table,
std::function<absl::StatusOr<bool>(absl::string_view key_name)>
skip_key_named = [](absl::string_view key_name) { return false; });

// Returns true and adds constraint to the solver. If `constraint` would make
// the current ConstraintSolver unable to generate an entry, returns false and
// does not change the state of the ConstraintSolver. If `constraint` is
// malformed returns error and `constraint_source` is used for debugging info.
absl::StatusOr<bool> AddConstraint(const ast::Expression& constraint,
const ConstraintSource& constraint_source);
// Similar to overload above except that both the AST expression and its
// source are derived from `constraint`. Additionally returns an error if a
// valid AST cannot be produced from `constraint`.
absl::StatusOr<bool> AddConstraint(absl::string_view constraint);

// Returns the entry encoded by the object.
// NOTE: The entry will NOT contain an action and is thus not a valid
// P4Runtime entry without modification.
// TODO(b/242201770): Extract actions once action constraints are supported.
absl::StatusOr<p4::v1::TableEntry> ConcretizeEntry();

private:
explicit ConstraintSolver()
: context_(std::make_unique<z3::context>()),
solver_(z3::solver(*context_)) {}

// Z3 context and solver. Solver requires a reference to `context` for
// construction so it is privately stored to avoid dangling reference.
std::unique_ptr<z3::context> context_;
z3::solver solver_;

// TableInfo of table that is being constrained.
TableInfo table_info_;

// Symbolic environment for storing information on symbolic keys.
SymbolicEnvironment environment_;

// Function to determine whether a key should be ignored while creating
// `environment_` and generating a concrete entry.
std::function<absl::StatusOr<bool>(absl::string_view key_name)>
skip_key_named_;
};

// -- Accessors ----------------------------------------------------------------

Expand Down
Loading

0 comments on commit fa64aec

Please sign in to comment.