From 3be308bd222227736226e6e60ce4c09a9103fd74 Mon Sep 17 00:00:00 2001 From: kishanps Date: Wed, 9 Aug 2023 00:40:28 -0700 Subject: [PATCH] [P4_Symbolic] Use absl numeric bit_width instead of custom implementation.Evaluate symbolic table entries with symbolic headers. --- p4_symbolic/symbolic/BUILD.bazel | 1 + p4_symbolic/symbolic/action.cc | 109 ++++-- p4_symbolic/symbolic/action.h | 39 +- p4_symbolic/symbolic/conditional.cc | 4 +- p4_symbolic/symbolic/conditional.h | 2 +- p4_symbolic/symbolic/control.cc | 4 +- p4_symbolic/symbolic/control.h | 4 +- p4_symbolic/symbolic/operators.cc | 10 + p4_symbolic/symbolic/parser.cc | 2 +- p4_symbolic/symbolic/symbolic.cc | 9 +- p4_symbolic/symbolic/table.cc | 334 ++++++++++-------- p4_symbolic/symbolic/table.h | 2 +- p4_symbolic/symbolic/v1model.cc | 4 +- p4_symbolic/symbolic/values.cc | 18 +- p4_symbolic/tests/BUILD.bazel | 4 +- .../tests/symbolic_table_entries_test.cc | 44 ++- 16 files changed, 346 insertions(+), 244 deletions(-) diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel index 6268775c..83b607f8 100644 --- a/p4_symbolic/symbolic/BUILD.bazel +++ b/p4_symbolic/symbolic/BUILD.bazel @@ -77,6 +77,7 @@ cc_library( "@com_google_absl//absl/cleanup", "@com_google_absl//absl/container:btree", "@com_google_absl//absl/container:flat_hash_map", + "@com_google_absl//absl/numeric:bits", "@com_google_absl//absl/status", "@com_google_absl//absl/status:statusor", "@com_google_absl//absl/strings", diff --git a/p4_symbolic/symbolic/action.cc b/p4_symbolic/symbolic/action.cc index 6c750155..2da1674c 100644 --- a/p4_symbolic/symbolic/action.cc +++ b/p4_symbolic/symbolic/action.cc @@ -26,11 +26,13 @@ #include "google/protobuf/repeated_ptr_field.h" #include "gutil/collections.h" #include "gutil/status.h" +#include "p4_pdpi/internal/ordered_map.h" #include "p4_pdpi/ir.pb.h" #include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/operators.h" #include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/table_entry.h" #include "p4_symbolic/symbolic/v1model.h" #include "p4_symbolic/symbolic/values.h" #include "p4_symbolic/z3_util.h" @@ -41,41 +43,41 @@ namespace symbolic { namespace action { absl::Status EvaluateStatement(const ir::Statement &statement, - SymbolicPerPacketState *state, + SymbolicPerPacketState &headers, ActionContext *context, z3::context &z3_context, const z3::expr &guard) { switch (statement.statement_case()) { case ir::Statement::kAssignment: { - return EvaluateAssignmentStatement(statement.assignment(), state, context, - z3_context, guard); + return EvaluateAssignmentStatement(statement.assignment(), headers, + context, z3_context, guard); } case ir::Statement::kClone: { // TODO: Add support for cloning. - return state->Set(std::string(kGotClonedPseudoField), - z3_context.bool_val(true), guard); + return headers.Set(std::string(kGotClonedPseudoField), + z3_context.bool_val(true), guard); } case ir::Statement::kDrop: { // https://github.com/p4lang/p4c/blob/7ee76d16da63883c5092ab0c28321f04c2646759/p4include/v1model.p4#L435 const std::string &header_name = statement.drop().header().header_name(); - RETURN_IF_ERROR(state->Set(absl::StrFormat("%s.egress_spec", header_name), - v1model::EgressSpecDroppedValue(z3_context), - guard)); + RETURN_IF_ERROR( + headers.Set(absl::StrFormat("%s.egress_spec", header_name), + v1model::EgressSpecDroppedValue(z3_context), guard)); return absl::OkStatus(); } case ir::Statement::kHash: { const ir::FieldValue &field = statement.hash().field(); std::string field_name = absl::StrFormat("%s.%s", field.header_name(), field.field_name()); - if (!state->ContainsKey(field_name)) { + if (!headers.ContainsKey(field_name)) { return absl::NotFoundError(absl::StrCat( "Action ", context->action_name, " hashes to unknown header field ", field.DebugString())); } - ASSIGN_OR_RETURN(z3::expr old_value, state->Get(field_name)); + ASSIGN_OR_RETURN(z3::expr old_value, headers.Get(field_name)); ASSIGN_OR_RETURN( z3::expr free_variable, operators::FreeVariable(field_name, old_value.get_sort())); - RETURN_IF_ERROR(state->Set(field_name, free_variable, guard)); + RETURN_IF_ERROR(headers.Set(field_name, free_variable, guard)); return absl::OkStatus(); } case ir::Statement::kExit: { @@ -95,18 +97,18 @@ absl::Status EvaluateStatement(const ir::Statement &statement, // constrains it in an enclosing assignment expression, or stores it in // the action scope. absl::Status EvaluateAssignmentStatement( - const ir::AssignmentStatement &assignment, SymbolicPerPacketState *state, + const ir::AssignmentStatement &assignment, SymbolicPerPacketState &headers, ActionContext *context, z3::context &z3_context, const z3::expr &guard) { // Evaluate RValue recursively, evaluate LValue in this function, then // assign RValue to the scope at LValue. - ASSIGN_OR_RETURN(z3::expr right, EvaluateRValue(assignment.right(), *state, + ASSIGN_OR_RETURN(z3::expr right, EvaluateRValue(assignment.right(), headers, *context, z3_context)); switch (assignment.left().lvalue_case()) { case ir::LValue::kFieldValue: { const ir::FieldValue &field_value = assignment.left().field_value(); - RETURN_IF_ERROR(state->Set(field_value.header_name(), - field_value.field_name(), right, guard)); + RETURN_IF_ERROR(headers.Set(field_value.header_name(), + field_value.field_name(), right, guard)); return absl::OkStatus(); } @@ -126,12 +128,12 @@ absl::Status EvaluateAssignmentStatement( // Constructs a symbolic expression corresponding to this value, according // to its type. absl::StatusOr EvaluateRValue(const ir::RValue &rvalue, - const SymbolicPerPacketState &state, + const SymbolicPerPacketState &headers, const ActionContext &context, z3::context &z3_context) { switch (rvalue.rvalue_case()) { case ir::RValue::kFieldValue: - return EvaluateFieldValue(rvalue.field_value(), state); + return EvaluateFieldValue(rvalue.field_value(), headers); case ir::RValue::kHexstrValue: return EvaluateHexStr(rvalue.hexstr_value(), z3_context); @@ -146,7 +148,7 @@ absl::StatusOr EvaluateRValue(const ir::RValue &rvalue, return EvaluateVariable(rvalue.variable_value(), context); case ir::RValue::kExpressionValue: - return EvaluateRExpression(rvalue.expression_value(), state, context, + return EvaluateRExpression(rvalue.expression_value(), headers, context, z3_context); default: @@ -158,8 +160,8 @@ absl::StatusOr EvaluateRValue(const ir::RValue &rvalue, // Extract the field symbolic value from the symbolic state. absl::StatusOr EvaluateFieldValue( - const ir::FieldValue &field_value, const SymbolicPerPacketState &state) { - return state.Get(field_value.header_name(), field_value.field_name()); + const ir::FieldValue &field_value, const SymbolicPerPacketState &headers) { + return headers.Get(field_value.header_name(), field_value.field_name()); } // Turns bmv2 values to Symbolic Expressions. @@ -200,14 +202,14 @@ absl::StatusOr EvaluateVariable(const ir::Variable &variable, // Recursively evaluate expressions. absl::StatusOr EvaluateRExpression( - const ir::RExpression &expr, const SymbolicPerPacketState &state, + const ir::RExpression &expr, const SymbolicPerPacketState &headers, const ActionContext &context, z3::context &z3_context) { switch (expr.expression_case()) { case ir::RExpression::kBinaryExpression: { ir::BinaryExpression bin_expr = expr.binary_expression(); - ASSIGN_OR_RETURN(z3::expr left, EvaluateRValue(bin_expr.left(), state, + ASSIGN_OR_RETURN(z3::expr left, EvaluateRValue(bin_expr.left(), headers, context, z3_context)); - ASSIGN_OR_RETURN(z3::expr right, EvaluateRValue(bin_expr.right(), state, + ASSIGN_OR_RETURN(z3::expr right, EvaluateRValue(bin_expr.right(), headers, context, z3_context)); switch (bin_expr.operation()) { case ir::BinaryExpression::PLUS: @@ -255,7 +257,7 @@ absl::StatusOr EvaluateRExpression( ir::UnaryExpression un_expr = expr.unary_expression(); ASSIGN_OR_RETURN( z3::expr operand, - EvaluateRValue(un_expr.operand(), state, context, z3_context)); + EvaluateRValue(un_expr.operand(), headers, context, z3_context)); switch (un_expr.operation()) { case ir::UnaryExpression::NOT: return operators::Not(operand); @@ -273,11 +275,12 @@ absl::StatusOr EvaluateRExpression( ir::TernaryExpression tern_expr = expr.ternary_expression(); ASSIGN_OR_RETURN( z3::expr condition, - EvaluateRValue(tern_expr.condition(), state, context, z3_context)); - ASSIGN_OR_RETURN(z3::expr left, EvaluateRValue(tern_expr.left(), state, + EvaluateRValue(tern_expr.condition(), headers, context, z3_context)); + ASSIGN_OR_RETURN(z3::expr left, EvaluateRValue(tern_expr.left(), headers, context, z3_context)); - ASSIGN_OR_RETURN(z3::expr right, EvaluateRValue(tern_expr.right(), state, - context, z3_context)); + ASSIGN_OR_RETURN( + z3::expr right, + EvaluateRValue(tern_expr.right(), headers, context, z3_context)); return operators::Ite(condition, left, right); } @@ -286,8 +289,8 @@ absl::StatusOr EvaluateRExpression( // Evaluate arguments. std::vector args; for (const auto &arg_value : builtin_expr.arguments()) { - ASSIGN_OR_RETURN(z3::expr arg, - EvaluateRValue(arg_value, state, context, z3_context)); + ASSIGN_OR_RETURN(z3::expr arg, EvaluateRValue(arg_value, headers, + context, z3_context)); args.push_back(arg); } @@ -311,15 +314,12 @@ absl::StatusOr EvaluateRExpression( } } -// Symbolically evaluates the given action on the given symbolic parameters. -// This produces a symbolic expression on the symbolic parameters that is -// semantically equivalent to the behavior of the action on its concrete -// parameters. -absl::Status EvaluateAction(const ir::Action &action, - const google::protobuf::RepeatedPtrField< - pdpi::IrActionInvocation::IrActionParam> &args, - SolverState &state, SymbolicPerPacketState *headers, - const z3::expr &guard) { +absl::Status EvaluateConcreteAction( + const ir::Action &action, + const google::protobuf::RepeatedPtrField< + pdpi::IrActionInvocation::IrActionParam> &args, + SolverState &state, SymbolicPerPacketState &headers, + const z3::expr &guard) { // Construct this action's context. ActionContext context; context.action_name = action.action_definition().preamble().name(); @@ -362,6 +362,37 @@ absl::Status EvaluateAction(const ir::Action &action, return absl::OkStatus(); } +absl::Status EvaluateSymbolicAction(const ir::Action &action, + const TableEntry &entry, SolverState &state, + SymbolicPerPacketState &headers, + const z3::expr &guard) { + // At this point the table must exists because otherwise an absl error would + // have been returned upon initializing the table entries, so no exception + // will be thrown. + const ir::Table &table = state.program.tables().at(entry.GetTableName()); + +// Construct the action's context. + ActionContext context; + context.action_name = action.action_definition().preamble().name(); + +// Add the symbolic action parameters to scope. + for (const auto &[param_name, _] : + Ordered(action.action_definition().params_by_name())) { + ASSIGN_OR_RETURN(z3::expr param_value, + entry.GetActionParameter(param_name, action, table, + *state.context.z3_context)); + context.scope.insert({param_name, param_value}); + } + +// Iterate over the body in order, and evaluate each statement. + for (const auto &statement : action.action_implementation().action_body()) { + RETURN_IF_ERROR(EvaluateStatement(statement, headers, &context, + *state.context.z3_context, guard)); + } + + return absl::OkStatus(); +} + } // namespace action } // namespace symbolic } // namespace p4_symbolic diff --git a/p4_symbolic/symbolic/action.h b/p4_symbolic/symbolic/action.h index b5082fbb..34278dbb 100644 --- a/p4_symbolic/symbolic/action.h +++ b/p4_symbolic/symbolic/action.h @@ -29,22 +29,13 @@ #include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/table_entry.h" #include "z3++.h" namespace p4_symbolic { namespace symbolic { namespace action { -// Symbolically evaluates the given action on the given symbolic parameters. -// This produces a symbolic expression on the symbolic parameters that is -// semantically equivalent to the behavior of the action on its concrete -// parameters. -absl::Status EvaluateAction(const ir::Action &action, - const google::protobuf::RepeatedPtrField< - pdpi::IrActionInvocation::IrActionParam> &args, - SolverState &state, SymbolicPerPacketState *headers, - const z3::expr &guard); - // Internal functions used to Evaluate statements and expressions within an // action body. These are internal functions not used beyond this header and its // associated source file. @@ -58,7 +49,7 @@ struct ActionContext { // Performs a switch case over support statement types and call the // appropriate function. absl::Status EvaluateStatement(const ir::Statement &statement, - SymbolicPerPacketState *state, + SymbolicPerPacketState &headers, ActionContext *context, z3::context &z3_context, const z3::expr &guard); @@ -66,19 +57,19 @@ absl::Status EvaluateStatement(const ir::Statement &statement, // constrains it in an enclosing assignment expression, or stores it in // the action scope. absl::Status EvaluateAssignmentStatement( - const ir::AssignmentStatement &assignment, SymbolicPerPacketState *state, + const ir::AssignmentStatement &assignment, SymbolicPerPacketState &headers, ActionContext *context, z3::context &z3_context, const z3::expr &guard); // Constructs a symbolic expression corresponding to this value, according // to its type. absl::StatusOr EvaluateRValue(const ir::RValue &rvalue, - const SymbolicPerPacketState &state, + const SymbolicPerPacketState &headers, const ActionContext &context, z3::context &z3_context); // Extract the field symbolic value from the symbolic state. absl::StatusOr EvaluateFieldValue( - const ir::FieldValue &field_value, const SymbolicPerPacketState &state); + const ir::FieldValue &field_value, const SymbolicPerPacketState &headers); // Parse and format literal values as symbolic expression. absl::StatusOr EvaluateHexStr(const ir::HexstrValue &hexstr, @@ -97,9 +88,27 @@ absl::StatusOr EvaluateVariable(const ir::Variable &variable, // Evaluate expression by recursively evaluating operands and applying the // symbolic version of the operator to them. absl::StatusOr EvaluateRExpression( - const ir::RExpression &expr, const SymbolicPerPacketState &state, + const ir::RExpression &expr, const SymbolicPerPacketState &headers, const ActionContext &context, z3::context &z3_context); +// Symbolically evaluates the given `action` based on the given concrete +// parameters in `args`. +// This applies the action with concrete parameters on the symbolic `headers`. +absl::Status EvaluateConcreteAction( + const ir::Action &action, + const google::protobuf::RepeatedPtrField< + pdpi::IrActionInvocation::IrActionParam> &args, + SolverState &state, SymbolicPerPacketState &headers, const z3::expr &guard); + +// Symbolically evaluates the given `action` based on the given symbolic +// parameters of the given `entry`. +// This applies the action with symbolic parameters on the symbolic `headers`. +absl::Status EvaluateSymbolicAction(const ir::Action &action, + const TableEntry &entry, SolverState &state, + SymbolicPerPacketState &headers, + const z3::expr &guard); + + } // namespace action } // namespace symbolic } // namespace p4_symbolic diff --git a/p4_symbolic/symbolic/conditional.cc b/p4_symbolic/symbolic/conditional.cc index c5b7ee81..7fab055a 100644 --- a/p4_symbolic/symbolic/conditional.cc +++ b/p4_symbolic/symbolic/conditional.cc @@ -37,12 +37,12 @@ namespace conditional { absl::StatusOr EvaluateConditional( const ir::Conditional &conditional, SolverState &state, - SymbolicPerPacketState *headers, const z3::expr &guard) { + SymbolicPerPacketState &headers, const z3::expr &guard) { // Evaluate the condition. action::ActionContext fake_context = {conditional.name(), {}}; ASSIGN_OR_RETURN( z3::expr condition, - action::EvaluateRValue(conditional.condition(), *headers, fake_context, + action::EvaluateRValue(conditional.condition(), headers, fake_context, *state.context.z3_context)); ASSIGN_OR_RETURN(z3::expr negated_condition, operators::Not(condition)); diff --git a/p4_symbolic/symbolic/conditional.h b/p4_symbolic/symbolic/conditional.h index fb6eb8d0..69279675 100644 --- a/p4_symbolic/symbolic/conditional.h +++ b/p4_symbolic/symbolic/conditional.h @@ -30,7 +30,7 @@ namespace conditional { absl::StatusOr EvaluateConditional( const ir::Conditional &conditional, SolverState &state, - SymbolicPerPacketState *headers, const z3::expr &guard); + SymbolicPerPacketState &headers, const z3::expr &guard); } // namespace conditional } // namespace symbolic diff --git a/p4_symbolic/symbolic/control.cc b/p4_symbolic/symbolic/control.cc index 91066ebc..76acd950 100644 --- a/p4_symbolic/symbolic/control.cc +++ b/p4_symbolic/symbolic/control.cc @@ -38,7 +38,7 @@ namespace p4_symbolic::symbolic::control { absl::StatusOr EvaluatePipeline( const std::string &pipeline_name, SolverState &state, - SymbolicPerPacketState *headers, const z3::expr &guard) { + SymbolicPerPacketState &headers, const z3::expr &guard) { if (auto it = state.program.pipeline().find(pipeline_name); it != state.program.pipeline().end()) { return EvaluateControl(it->second.initial_control(), state, headers, guard); @@ -49,7 +49,7 @@ absl::StatusOr EvaluatePipeline( absl::StatusOr EvaluateControl( const std::string &control_name, SolverState &state, - SymbolicPerPacketState *headers, const z3::expr &guard) { + SymbolicPerPacketState &headers, const z3::expr &guard) { // Base case: we got to the end of the evaluation, no more controls! if (control_name == ir::EndOfPipeline()) return SymbolicTableMatches(); diff --git a/p4_symbolic/symbolic/control.h b/p4_symbolic/symbolic/control.h index 6969fc61..5a4a6b3f 100644 --- a/p4_symbolic/symbolic/control.h +++ b/p4_symbolic/symbolic/control.h @@ -71,12 +71,12 @@ namespace control { // Evaluate the passed pipeline. absl::StatusOr EvaluatePipeline( const std::string &pipeline_name, SolverState &state, - SymbolicPerPacketState *headers, const z3::expr &guard); + SymbolicPerPacketState &headers, const z3::expr &guard); // Evaluate the passed control construct. absl::StatusOr EvaluateControl( const std::string &control_name, SolverState &state, - SymbolicPerPacketState *headers, const z3::expr &guard); + SymbolicPerPacketState &headers, const z3::expr &guard); } // namespace control } // namespace symbolic diff --git a/p4_symbolic/symbolic/operators.cc b/p4_symbolic/symbolic/operators.cc index 5b979b38..0f47310b 100644 --- a/p4_symbolic/symbolic/operators.cc +++ b/p4_symbolic/symbolic/operators.cc @@ -19,13 +19,16 @@ #include "p4_symbolic/symbolic/operators.h" +#include #include #include "absl/status/status.h" +#include "absl/status/statusor.h" #include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" #include "gutil/status.h" #include "z3++.h" +#include "z3_api.h" namespace p4_symbolic { namespace symbolic { @@ -236,6 +239,13 @@ absl::StatusOr BitNeg(const z3::expr &a) { return ~a; } // since our semantics do not allow arbitrary extraction to smaller sizes, but // do allow arbitrary padding. absl::StatusOr BitAnd(const z3::expr &a, const z3::expr &b) { + // Coerce bool to bit<1>. + if (a.is_bool() && b.is_bv() && b.get_sort().bv_size() == 1) { + return z3::ite(a, b, a.ctx().bv_val(0, 1)); + } + if (b.is_bool() && a.is_bv() && a.get_sort().bv_size() == 1) { + return z3::ite(b, a, b.ctx().bv_val(0, 1)); + } ASSIGN_OR_RETURN(auto pair, p4_symbolic::symbolic::operators::SortCheckAndExtract(a, b)); auto &[a_expr, b_expr] = pair; diff --git a/p4_symbolic/symbolic/parser.cc b/p4_symbolic/symbolic/parser.cc index 0b604988..d44abd35 100644 --- a/p4_symbolic/symbolic/parser.cc +++ b/p4_symbolic/symbolic/parser.cc @@ -133,7 +133,7 @@ absl::Status EvaluatePrimitiveParserOperation( switch (primitive.statement_case()) { case ir::ParserOperation::Primitive::StatementCase::kAssignment: { return action::EvaluateAssignmentStatement( - primitive.assignment(), &headers, &context, z3_context, guard); + primitive.assignment(), headers, &context, z3_context, guard); } default: { return gutil::UnimplementedErrorBuilder() diff --git a/p4_symbolic/symbolic/symbolic.cc b/p4_symbolic/symbolic/symbolic.cc index fbcc00fd..4285cbbd 100644 --- a/p4_symbolic/symbolic/symbolic.cc +++ b/p4_symbolic/symbolic/symbolic.cc @@ -80,8 +80,13 @@ absl::Status InitializeTableEntries(SolverState &state, // For each IR entry, create a table entry object. for (size_t index = 0; index < per_table_ir_entries.size(); ++index) { ir::TableEntry &ir_entry = per_table_ir_entries[index]; - state.context.table_entries[table_name].push_back( - TableEntry(index, std::move(ir_entry))); + TableEntry entry(index, std::move(ir_entry)); + if (!entry.IsConcrete() && !entry.IsSymbolic()) { + return gutil::InvalidArgumentErrorBuilder() + << "A table entry must be either concrete or symbolic. Found: " + << entry.GetPdpiIrTableEntry().DebugString(); + } + state.context.table_entries[table_name].push_back(std::move(entry)); } } diff --git a/p4_symbolic/symbolic/table.cc b/p4_symbolic/symbolic/table.cc index bd2aedb8..24817773 100644 --- a/p4_symbolic/symbolic/table.cc +++ b/p4_symbolic/symbolic/table.cc @@ -30,14 +30,13 @@ #include "absl/container/btree_map.h" #include "absl/status/status.h" #include "absl/status/statusor.h" -#include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" +#include "absl/strings/string_view.h" #include "absl/strings/substitute.h" #include "absl/types/optional.h" #include "google/protobuf/map.h" #include "gutil/status.h" #include "p4/config/v1/p4info.pb.h" -#include "p4_pdpi/internal/ordered_map.h" #include "p4_pdpi/ir.pb.h" #include "p4_symbolic/ir/ir.h" #include "p4_symbolic/ir/ir.pb.h" @@ -57,21 +56,6 @@ namespace table { namespace { -// Finds a match field with the given match name in the given table entry. -// Returns the index of that match field inside the matches array in entry, or -// -1 if no such match was found. -int FindMatchWithName(const pdpi::IrTableEntry &entry, - const std::string &name) { - int index = -1; - for (int i = 0; i < entry.matches_size(); i++) { - if (entry.matches(i).name() == name) { - index = i; - break; - } - } - return index; -} - // Sort the given table entries by priority. // The priority depends on the match types. // If the table matches contain at least one ternary or optional match, the @@ -170,169 +154,240 @@ std::vector SortEntries(const ir::Table &table, return sorted_entries; } -// Analyze a single match that is part of a table entry. -// Constructs a symbolic expression that semantically corresponds to this match. -absl::StatusOr EvaluateSingleMatch( - const p4::config::v1::MatchField &match_definition, - const std::string &field_name, const z3::expr &field_expression, - const pdpi::IrMatch &match, SolverState &state) { - if (match_definition.match_case() != p4::config::v1::MatchField::kMatchType) { - // Arch-specific match type. - return absl::InvalidArgumentError( - absl::StrCat("Found match with non-standard type")); +// Analyzes a single symbolic match of a table entry. +// Constructs a symbolic expression that semantically corresponds to the given +// symbolic match. +absl::StatusOr EvaluateSymbolicMatch(absl::string_view match_name, + const z3::expr &field_value, + const TableEntry &entry, + const ir::Table &table, + SolverState &state) { + ASSIGN_OR_RETURN(SymbolicMatchVariables variables, + entry.GetMatchValues(match_name, table, state.program, + *state.context.z3_context)); + ASSIGN_OR_RETURN(z3::expr masked_field, + operators::BitAnd(field_value, variables.mask)); + return operators::Eq(masked_field, variables.value); +} + +// Analyzes a single concrete match of a table entry. +// Constructs a symbolic expression that semantically corresponds to the given +// concrete match. +absl::StatusOr EvaluateConcreteMatch( + const pdpi::IrMatch &ir_match, const p4::config::v1::MatchField &pi_match, + const std::string &field_name, const z3::expr &field_value, + SolverState &state) { + if (!pi_match.has_match_type()) { + // Architecture-specific match type. + return gutil::InvalidArgumentErrorBuilder() + << "Found match with non-standard type"; } + // Translates the given `value` read from the match of a table entry into a Z3 + // expression. + auto GetZ3Value = + [&field_name, &pi_match, + &state](const pdpi::IrValue &value) -> absl::StatusOr { + return values::FormatP4RTValue(field_name, pi_match.type_name().name(), + value, pi_match.bitwidth(), + *state.context.z3_context, state.translator); + }; + absl::Status mismatch = gutil::InvalidArgumentErrorBuilder() << "match on field '" << field_name << "' must be of type " - << p4::config::v1::MatchField::MatchType_Name( - match_definition.match_type()) + << p4::config::v1::MatchField::MatchType_Name(pi_match.match_type()) << " according to the table definition, but got entry with match: " - << match_definition.ShortDebugString(); - - auto GetZ3Value = - [&](const pdpi::IrValue &value) -> absl::StatusOr { - return values::FormatP4RTValue(field_name, - match_definition.type_name().name(), value, - match_definition.bitwidth(), - *state.context.z3_context, state.translator); - }; + << ir_match.ShortDebugString(); - switch (match_definition.match_type()) { + switch (pi_match.match_type()) { case p4::config::v1::MatchField::EXACT: { - if (match.match_value_case() != pdpi::IrMatch::kExact) return mismatch; - ASSIGN_OR_RETURN(z3::expr value_expression, GetZ3Value(match.exact())); - return operators::Eq(field_expression, value_expression); + if (!ir_match.has_exact()) return mismatch; + + ASSIGN_OR_RETURN(z3::expr exact_value, GetZ3Value(ir_match.exact())); + return operators::Eq(field_value, exact_value); } case p4::config::v1::MatchField::LPM: { - if (match.match_value_case() != pdpi::IrMatch::kLpm) return mismatch; + if (!ir_match.has_lpm()) return mismatch; - ASSIGN_OR_RETURN(z3::expr value_expression, - GetZ3Value(match.lpm().value())); + ASSIGN_OR_RETURN(z3::expr lpm_value, GetZ3Value(ir_match.lpm().value())); return operators::PrefixEq( - field_expression, value_expression, - static_cast(match.lpm().prefix_length())); + field_value, lpm_value, + static_cast(ir_match.lpm().prefix_length())); } case p4::config::v1::MatchField::TERNARY: { - if (match.match_value_case() != pdpi::IrMatch::kTernary) return mismatch; + if (!ir_match.has_ternary()) return mismatch; - ASSIGN_OR_RETURN(z3::expr mask_expression, - GetZ3Value(match.ternary().mask())); - ASSIGN_OR_RETURN(z3::expr value_expression, - GetZ3Value(match.ternary().value())); + ASSIGN_OR_RETURN(z3::expr ternary_value, + GetZ3Value(ir_match.ternary().value())); + ASSIGN_OR_RETURN(z3::expr ternary_mask, + GetZ3Value(ir_match.ternary().mask())); ASSIGN_OR_RETURN(z3::expr masked_field, - operators::BitAnd(field_expression, mask_expression)); - return operators::Eq(masked_field, value_expression); + operators::BitAnd(field_value, ternary_mask)); + return operators::Eq(masked_field, ternary_value); } case p4::config::v1::MatchField::OPTIONAL: { - if (match.match_value_case() != pdpi::IrMatch::kOptional) return mismatch; + if (!ir_match.has_optional()) return mismatch; + // According to the P4Runtime spec, "for don't care matches, the P4Runtime // client must omit the field's entire FieldMatch entry when building the // match repeated field of the TableEntry message". Therefore, if the // match value is present for an optional match type, it must be a // concrete value. - ASSIGN_OR_RETURN(z3::expr value_expression, - GetZ3Value(match.optional().value())); - return operators::Eq(field_expression, value_expression); + ASSIGN_OR_RETURN(z3::expr optional_value, + GetZ3Value(ir_match.optional().value())); + return operators::Eq(field_value, optional_value); } - default: - return absl::UnimplementedError(absl::StrCat( - "Found unsupported match type ", match_definition.DebugString())); + default: { + return gutil::UnimplementedErrorBuilder() + << "Found unsupported match type " << pi_match.DebugString(); + } } } // Constructs a symbolic expression that is true if and only if this entry // is matched on. absl::StatusOr EvaluateTableEntryCondition( - const ir::Table &table, const pdpi::IrTableEntry &entry, SolverState &state, + const ir::Table &table, const TableEntry &entry, SolverState &state, const SymbolicPerPacketState &headers) { const std::string &table_name = table.table_definition().preamble().name(); + const google::protobuf::Map + &match_name_to_header_fields = + table.table_implementation().match_name_to_field(); + const google::protobuf::Map + &match_definition_by_name = + table.table_definition().match_fields_by_name(); // Construct the match condition expression. - z3::expr condition_expression = state.context.z3_context->bool_val(true); - const google::protobuf::Map &match_to_fields = - table.table_implementation().match_name_to_field(); - - // It is desirable for P4Symbolic to produce deterministic outputs. Therefore, - // all containers need to be traversed in a deterministic order. - const auto sorted_match_fields_by_name = - Ordered(table.table_definition().match_fields_by_name()); - - for (const auto &[name, match_fields] : sorted_match_fields_by_name) { - p4::config::v1::MatchField match_definition = match_fields.match_field(); - - int match_field_index = FindMatchWithName(entry, name); - if (match_field_index == -1) { - // Table entry does not specify a value for this match key, means - // it is a wildcard, no need to do any symbolic condition for it. - continue; + z3::expr match_condition = state.context.z3_context->bool_val(true); + + // TODO: Consider sorting the matches before evaluating them to + // ensure equivalent entries produce the same formulae. + for (const pdpi::IrMatch &ir_match : entry.GetPdpiIrTableEntry().matches()) { + const std::string &match_name = ir_match.name(); + + // Check if the match exists in the table definition. + if (!match_definition_by_name.contains(match_name)) { + return gutil::InvalidArgumentErrorBuilder() + << "Match '" << match_name + << "' not found in the definition of table '" << table_name << "'"; } - const pdpi::IrMatch &match = entry.matches(match_field_index); - // We get the match name for pdpi/p4info for simplicity, however that - // file only contains the match name as a string, which is the same as the - // match target expression in most cases but not always. - // For conciseness, we get the corresponding accurate match target from - // bmv2 by looking up the match name there. + // We get the match name from pdpi/p4info for simplicity, however that file + // only contains the match name as a string, which is the same as the match + // target expression in most cases but not always. + // For conciseness, we get the corresponding accurate match target from bmv2 + // by looking up the match name there. // In certain cases this is important, e.g. a match defined over field // "dstAddr" may have aliases of that field as a match name, but will always // have the fully qualified name of the field in the bmv2 format. - if (match_to_fields.count(match_definition.name()) != 1) { - return absl::InvalidArgumentError(absl::StrCat( - "Match key with name \"", match_definition.name(), - "\" was not found in implementation of table \"", table_name, "\"")); + if (!match_name_to_header_fields.contains(match_name)) { + return gutil::InvalidArgumentErrorBuilder() + << "Match '" << match_name + << "' not found in the implementation of table '" << table_name + << "'"; } - ir::FieldValue match_field = match_to_fields.at(match_definition.name()); - std::string field_name = absl::StrFormat("%s.%s", match_field.header_name(), - match_field.field_name()); - ASSIGN_OR_RETURN(z3::expr field_expr, - action::EvaluateFieldValue(match_field, headers)); - ASSIGN_OR_RETURN(z3::expr match_expression, - EvaluateSingleMatch(match_definition, field_name, - field_expr, match, state)); - ASSIGN_OR_RETURN(condition_expression, - operators::And(condition_expression, match_expression)); + const p4::config::v1::MatchField &pi_match = + match_definition_by_name.at(match_name).match_field(); + const ir::FieldValue &matched_field = + match_name_to_header_fields.at(match_name); + std::string field_name = absl::StrFormat( + "%s.%s", matched_field.header_name(), matched_field.field_name()); + ASSIGN_OR_RETURN(z3::expr field_value, + action::EvaluateFieldValue(matched_field, headers)); + + // Evaluate the condition of the specific match. + z3::expr match_expression(*state.context.z3_context); + if (entry.IsSymbolic()) { + ASSIGN_OR_RETURN( + match_expression, + EvaluateSymbolicMatch(match_name, field_value, entry, table, state)); + } else { + ASSIGN_OR_RETURN(match_expression, + EvaluateConcreteMatch(ir_match, pi_match, field_name, + field_value, state)); + } + + ASSIGN_OR_RETURN(match_condition, + operators::And(match_condition, match_expression)); } - return condition_expression; + return match_condition; } -absl::Status EvaluateSingeTableEntryAction( - const pdpi::IrActionInvocation &action, - const google::protobuf::Map &actions, - SolverState &state, SymbolicPerPacketState *headers, - const z3::expr &guard) { - // Check that the action invoked by entry exists. - if (actions.count(action.name()) != 1) { +absl::Status EvaluateSingeConcreteAction(const pdpi::IrActionInvocation &action, + SolverState &state, + SymbolicPerPacketState &headers, + const z3::expr &guard) { + const google::protobuf::Map &actions = + state.program.actions(); + + // Check if the action invoked by entry exists. + if (!actions.contains(action.name())) { return gutil::InvalidArgumentErrorBuilder() << "unknown action '" << action.name() << "'"; } - return action::EvaluateAction(actions.at(action.name()), action.params(), - state, headers, guard); + return action::EvaluateConcreteAction(actions.at(action.name()), + action.params(), state, headers, guard); +} + +absl::Status EvaluateSingleSymbolicAction(absl::string_view action_name, + const TableEntry &entry, + SolverState &state, + SymbolicPerPacketState &headers, + const z3::expr &guard) { + const google::protobuf::Map &actions = + state.program.actions(); + + // Check if the action from the table definition exists. + if (!actions.contains(action_name)) { + return gutil::InternalErrorBuilder() + << "unknown action '" << action_name << "'"; + } + return action::EvaluateSymbolicAction(actions.at(action_name), entry, state, + headers, guard); } // Constructs a symbolic expressions that represents the action invocation // corresponding to this entry. -absl::Status EvaluateTableEntryAction( - const ir::Table &table, const TableEntry &entry, - const google::protobuf::Map &actions, - SolverState &state, SymbolicPerPacketState *headers, - const z3::expr &guard) { +absl::Status EvaluateTableEntryAction(const ir::Table &table, + const TableEntry &entry, + SolverState &state, + SymbolicPerPacketState &headers, + const z3::expr &guard) { const pdpi::IrTableEntry &ir_entry = entry.GetPdpiIrTableEntry(); - switch (ir_entry.type_case()) { - case pdpi::IrTableEntry::kAction: - RETURN_IF_ERROR(EvaluateSingeTableEntryAction(ir_entry.action(), actions, - state, headers, guard)) + if (entry.IsSymbolic()) { + // Entries with symbolic action sets are not supported for now. + if (table.table_definition().has_action_profile_id()) { + return gutil::UnimplementedErrorBuilder() + << "Table entries with symbolic action sets are not supported " + "at the moment."; + } + + // Evaluate each symbolic action of a symbolic table entry. + for (const pdpi::IrActionReference &action_ref : + table.table_definition().entry_actions()) { + absl::string_view action_name = action_ref.action().preamble().name(); + ASSIGN_OR_RETURN(z3::expr action_is_applied, + entry.GetActionInvocation(action_name, table, + *state.context.z3_context)); + RETURN_IF_ERROR(EvaluateSingleSymbolicAction( + action_name, entry, state, headers, guard && action_is_applied)); + } + } else { + // Evaluate the concrete action or action set of a concrete table entry. + if (ir_entry.has_action()) { + RETURN_IF_ERROR( + EvaluateSingeConcreteAction(ir_entry.action(), state, headers, guard)) .SetPrepend() << "In table entry '" << ir_entry.ShortDebugString() << "':"; - return absl::OkStatus(); - case pdpi::IrTableEntry::kActionSet: { + } else if (ir_entry.has_action_set()) { auto &action_set = ir_entry.action_set().actions(); // For action sets, we introduce a new free integer variable "selector" // whose value determines which action is executed: to a first @@ -348,27 +403,28 @@ absl::Status EvaluateTableEntryAction( bool is_last_action = i == action_set.size() - 1; z3::expr selected = is_last_action ? unselected : (selector == i); unselected = unselected && !selected; - RETURN_IF_ERROR(EvaluateSingeTableEntryAction( - action, actions, state, headers, guard && selected)) + RETURN_IF_ERROR(EvaluateSingeConcreteAction(action, state, headers, + guard && selected)) .SetPrepend() << "In table entry '" << ir_entry.ShortDebugString() << "':"; } - return absl::OkStatus(); + } else { + return gutil::InvalidArgumentErrorBuilder() + << "unexpected or missing action in table entry: " + << ir_entry.DebugString(); } - default: - break; } - return gutil::InvalidArgumentErrorBuilder() - << "unexpected or missing action in table entry: " - << ir_entry.DebugString(); + + return absl::OkStatus(); } } // namespace absl::StatusOr EvaluateTable( - const ir::Table &table, SolverState &state, SymbolicPerPacketState *headers, + const ir::Table &table, SolverState &state, SymbolicPerPacketState &headers, const z3::expr &guard) { const std::string &table_name = table.table_definition().preamble().name(); + // Sort entries by priority deduced from match types. std::vector sorted_entries; if (auto it = state.context.table_entries.find(table_name); @@ -416,16 +472,8 @@ absl::StatusOr EvaluateTable( // Find all entries match conditions. std::vector entries_matches; for (const auto &entry : sorted_entries) { - if (entry.IsSymbolic()) { - return gutil::UnimplementedErrorBuilder() - << "Symbolic entries are not supported at the moment."; - } - - // We are passing state by const reference here, so we do not need - // any guard yet. ASSIGN_OR_RETURN(z3::expr entry_match, - EvaluateTableEntryCondition( - table, entry.GetPdpiIrTableEntry(), state, *headers)); + EvaluateTableEntryCondition(table, entry, state, headers)); entries_matches.push_back(entry_match); } @@ -471,9 +519,8 @@ absl::StatusOr EvaluateTable( // Start with the default entry z3::expr match_index = state.context.z3_context->int_val(kDefaultActionEntryIndex); - RETURN_IF_ERROR( - EvaluateTableEntryAction(table, default_entry, state.program.actions(), - state, headers, default_entry_assignment_guard)); + RETURN_IF_ERROR(EvaluateTableEntryAction(table, default_entry, state, headers, + default_entry_assignment_guard)); // Continue evaluating each table entry in reverse priority for (int row = sorted_entries.size() - 1; row >= 0; row--) { @@ -488,9 +535,8 @@ absl::StatusOr EvaluateTable( // Evaluate the entry's action guarded by its complete assignment guard. z3::expr entry_assignment_guard = assignment_guards.at(row); - RETURN_IF_ERROR(EvaluateTableEntryAction(table, entry, - state.program.actions(), state, - headers, entry_assignment_guard)); + RETURN_IF_ERROR(EvaluateTableEntryAction(table, entry, state, headers, + entry_assignment_guard)); } const std::string &merge_point = table.table_implementation() diff --git a/p4_symbolic/symbolic/table.h b/p4_symbolic/symbolic/table.h index 2f9ee2b1..055ab1d7 100644 --- a/p4_symbolic/symbolic/table.h +++ b/p4_symbolic/symbolic/table.h @@ -35,7 +35,7 @@ namespace table { constexpr int kDefaultActionEntryIndex = -1; absl::StatusOr EvaluateTable( - const ir::Table &table, SolverState &state, SymbolicPerPacketState *headers, + const ir::Table &table, SolverState &state, SymbolicPerPacketState &headers, const z3::expr &guard); } // namespace table diff --git a/p4_symbolic/symbolic/v1model.cc b/p4_symbolic/symbolic/v1model.cc index 5bfe5efc..eb8b4b5d 100644 --- a/p4_symbolic/symbolic/v1model.cc +++ b/p4_symbolic/symbolic/v1model.cc @@ -221,7 +221,7 @@ absl::Status EvaluateV1model(SolverState &state, // https://github.com/p4lang/behavioral-model/blob/main/docs/simple_switch.md#pseudocode-for-what-happens-at-the-end-of-ingress-and-egress-processing ASSIGN_OR_RETURN( SymbolicTableMatches matches, - control::EvaluatePipeline("ingress", state, &context.egress_headers, + control::EvaluatePipeline("ingress", state, context.egress_headers, /*guard=*/context.z3_context->bool_val(true))); ASSIGN_OR_RETURN(z3::expr dropped, IsDropped(context.egress_headers, *context.z3_context)); @@ -237,7 +237,7 @@ absl::Status EvaluateV1model(SolverState &state, // Evaluate the egress pipeline. ASSIGN_OR_RETURN( SymbolicTableMatches egress_matches, - control::EvaluatePipeline("egress", state, &context.egress_headers, + control::EvaluatePipeline("egress", state, context.egress_headers, /*guard=*/!dropped)); matches.merge(std::move(egress_matches)); diff --git a/p4_symbolic/symbolic/values.cc b/p4_symbolic/symbolic/values.cc index 50063172..536ec002 100644 --- a/p4_symbolic/symbolic/values.cc +++ b/p4_symbolic/symbolic/values.cc @@ -23,6 +23,7 @@ #include #include +#include "absl/numeric/bits.h" #include "absl/status/status.h" #include "absl/status/statusor.h" #include "absl/strings/match.h" @@ -49,21 +50,6 @@ namespace p4_symbolic { namespace symbolic { namespace values { -namespace { - -// Finds the minimum bit size required for representing the given value. -unsigned int FindBitsize(uint64_t value) { - unsigned int bitsize = 0; - uint64_t pow = 1; - while (bitsize <= 64 && pow <= value) { - pow = pow * 2; - bitsize++; - } - return (bitsize > 1 ? bitsize : 1); // At least 1 bit. -} - -} // namespace - absl::StatusOr ParseIrValue(const std::string &value) { // Format according to type. if (absl::StartsWith(value, "0x")) { @@ -103,7 +89,7 @@ absl::StatusOr FormatP4RTValue(const std::string &field_name, ASSIGN_OR_RETURN(uint64_t int_value, allocator.AllocateId(string_value)); if (bitwidth == 0) { - bitwidth = FindBitsize(int_value); + bitwidth = int_value == 0 ? 1 : absl::bit_width(int_value); } else { return absl::InvalidArgumentError(absl::Substitute( "Translated type '$0' is expected to have bitwidth 0, got $1", diff --git a/p4_symbolic/tests/BUILD.bazel b/p4_symbolic/tests/BUILD.bazel index 66f54d22..455b8405 100644 --- a/p4_symbolic/tests/BUILD.bazel +++ b/p4_symbolic/tests/BUILD.bazel @@ -43,6 +43,7 @@ cc_test( ], deps = [ "//gutil:status_matchers", + "//gutil:test_artifact_writer", "//p4_symbolic:test_util", "//p4_symbolic/ir", "//p4_symbolic/ir:ir_cc_proto", @@ -50,11 +51,8 @@ cc_test( "//p4_symbolic/ir:table_entries", "//p4_symbolic/sai", "//p4_symbolic/symbolic", - "//thinkit:bazel_test_environment", - "//thinkit:test_environment", "@com_github_google_glog//:glog", "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", - "@com_google_absl//absl/status", "@com_google_absl//absl/strings", "@com_google_absl//absl/time", "@com_google_googletest//:gtest_main", diff --git a/p4_symbolic/tests/symbolic_table_entries_test.cc b/p4_symbolic/tests/symbolic_table_entries_test.cc index 0af15f91..43cdba15 100644 --- a/p4_symbolic/tests/symbolic_table_entries_test.cc +++ b/p4_symbolic/tests/symbolic_table_entries_test.cc @@ -13,10 +13,11 @@ // limitations under the License. #include +#include #include #include -#include "absl/status/status.h" +#include "absl/strings/str_cat.h" #include "absl/strings/string_view.h" #include "absl/time/clock.h" #include "absl/time/time.h" @@ -24,6 +25,7 @@ #include "gmock/gmock.h" #include "gtest/gtest.h" #include "gutil/status_matchers.h" +#include "gutil/test_artifact_writer.h" #include "p4/v1/p4runtime.pb.h" #include "p4_symbolic/ir/ir.h" #include "p4_symbolic/ir/ir.pb.h" @@ -34,16 +36,12 @@ #include "p4_symbolic/symbolic/table_entry.h" #include "p4_symbolic/symbolic/values.h" #include "p4_symbolic/test_util.h" -#include "thinkit/bazel_test_environment.h" -#include "thinkit/test_environment.h" namespace p4_symbolic { namespace { class SymbolicTableEntriesIPv4BasicTest : public testing::Test { public: - thinkit::TestEnvironment& Environment() { return *environment_; } - void SetUp() override { constexpr absl::string_view bmv2_json_path = "p4_symbolic/testdata/ipv4-routing/" @@ -67,9 +65,7 @@ class SymbolicTableEntriesIPv4BasicTest : public testing::Test { } protected: - std::unique_ptr environment_ = - std::make_unique( - /*mask_known_failures=*/true); + gutil::BazelTestArtifactWriter artifact_writer_; ir::P4Program program_; ir::TableEntries ir_entries_; }; @@ -78,9 +74,13 @@ TEST_F(SymbolicTableEntriesIPv4BasicTest, OneSymbolicEntryPerTable) { constexpr int priority = 0; constexpr int prefix_length = 16; - // Create a symbolic IR entry for each table. + // Remove all existing concrete table entries. ir_entries_.clear(); + + // Create a symbolic IR entry for each table. for (const auto& [table_name, table] : program_.tables()) { + // Skip tables that are not in the original P4 program. + if (table.table_definition().preamble().id() == 0) continue; ASSERT_OK_AND_ASSIGN( ir::TableEntry ir_entry, symbolic::CreateSymbolicIrTableEntry(table, priority, prefix_length)); @@ -99,13 +99,29 @@ TEST_F(SymbolicTableEntriesIPv4BasicTest, OneSymbolicEntryPerTable) { .static_mapping = {{"", 0}}, .dynamic_translation = true, }; - LOG(INFO) << "Building model ..."; + LOG(INFO) << "Building model..."; absl::Time start_time = absl::Now(); - EXPECT_THAT( - symbolic::EvaluateP4Program(program_, ir_entries_, ports, translations), - gutil::StatusIs(absl::StatusCode::kUnimplemented, - "Symbolic entries are not supported at the moment.")); + ASSERT_OK_AND_ASSIGN( + std::unique_ptr state, + symbolic::EvaluateP4Program(program_, ir_entries_, ports, translations)); LOG(INFO) << "-> done in " << (absl::Now() - start_time); + + // Dump solver state. + for (const auto& [table_name, entries] : state->context.table_entries) { + std::string banner = + absl::StrCat("== ", table_name, " ", + std::string(80 - table_name.size() - 4, '='), "\n"); + EXPECT_OK(artifact_writer_.AppendToTestArtifact("table_entries.textproto", + banner)); + for (const auto& entry : entries) { + EXPECT_OK(artifact_writer_.AppendToTestArtifact( + "table_entries.textproto", entry.GetP4SymbolicIrTableEntry())); + } + } + EXPECT_OK( + artifact_writer_.StoreTestArtifact("program.textproto", state->program)); + EXPECT_OK(artifact_writer_.StoreTestArtifact( + "all_smt_formulae.txt", state->GetHeadersAndSolverConstraintsSMT())); } } // namespace