From 40756ecb0f88cfb464cc3d602687d57b97bfe371 Mon Sep 17 00:00:00 2001 From: kishanps Date: Tue, 8 Aug 2023 08:21:19 -0700 Subject: [PATCH] [P4-Symbolic] Create a class for symbolic table entries. --- p4_symbolic/BUILD.bazel | 1 + p4_symbolic/ir/BUILD.bazel | 1 + p4_symbolic/ir/ir.proto | 2 + p4_symbolic/ir/table_entries.h | 11 +- p4_symbolic/main.cc | 22 +- .../packet_synthesizer/criteria_generator.cc | 7 +- p4_symbolic/symbolic/BUILD.bazel | 36 +- p4_symbolic/symbolic/action.cc | 24 +- p4_symbolic/symbolic/action.h | 9 +- p4_symbolic/symbolic/conditional.cc | 49 +- p4_symbolic/symbolic/conditional.h | 9 +- p4_symbolic/symbolic/context.h | 2 + p4_symbolic/symbolic/control.cc | 40 +- p4_symbolic/symbolic/control.h | 14 +- p4_symbolic/symbolic/parser.cc | 68 +-- p4_symbolic/symbolic/symbolic.cc | 132 ++++-- p4_symbolic/symbolic/symbolic.h | 31 +- p4_symbolic/symbolic/table.cc | 181 ++++---- p4_symbolic/symbolic/table.h | 9 +- p4_symbolic/symbolic/table_entry_test.cc | 417 ++++++++++++++++++ p4_symbolic/symbolic/v1model.cc | 27 +- p4_symbolic/symbolic/v1model.h | 12 +- p4_symbolic/symbolic/values.cc | 23 +- p4_symbolic/symbolic/values.h | 9 +- p4_symbolic/symbolic/values_test.cc | 31 +- p4_symbolic/tests/BUILD.bazel | 9 +- 26 files changed, 855 insertions(+), 321 deletions(-) create mode 100644 p4_symbolic/symbolic/table_entry_test.cc diff --git a/p4_symbolic/BUILD.bazel b/p4_symbolic/BUILD.bazel index b4283043..f4e62fae 100644 --- a/p4_symbolic/BUILD.bazel +++ b/p4_symbolic/BUILD.bazel @@ -36,6 +36,7 @@ cc_binary( "@com_google_absl//absl/flags:usage", "@com_google_absl//absl/status", "@com_google_absl//absl/strings:str_format", + "@com_google_protobuf//:protobuf", ], ) diff --git a/p4_symbolic/ir/BUILD.bazel b/p4_symbolic/ir/BUILD.bazel index cf7f1797..7550d50f 100644 --- a/p4_symbolic/ir/BUILD.bazel +++ b/p4_symbolic/ir/BUILD.bazel @@ -47,6 +47,7 @@ cc_library( "//p4_pdpi:ir", "//p4_pdpi:ir_cc_proto", "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", + "@com_google_absl//absl/container:btree", "@com_google_absl//absl/status", "@com_google_absl//absl/status:statusor", "@com_google_absl//absl/types:span", diff --git a/p4_symbolic/ir/ir.proto b/p4_symbolic/ir/ir.proto index a961b232..48c6fcb7 100644 --- a/p4_symbolic/ir/ir.proto +++ b/p4_symbolic/ir/ir.proto @@ -522,6 +522,8 @@ message SymbolicTableEntry { // symbolic action or action set following the P4Info specification. // - An `IrActionInvocation` with an empty `name` also denotes a symbolic // action, in which case the `params` must also be empty. + // - All symbolic actions in an action set must be explicitly specified with + // empty action names and parameters. // // In the future, we may copy the fields over from the PDPI IR to have more // flexbility if needed. diff --git a/p4_symbolic/ir/table_entries.h b/p4_symbolic/ir/table_entries.h index b64d7ac1..b535b8ca 100644 --- a/p4_symbolic/ir/table_entries.h +++ b/p4_symbolic/ir/table_entries.h @@ -19,9 +19,9 @@ #define P4_SYMBOLIC_IR_TABLE_ENTRIES_H_ #include -#include #include +#include "absl/container/btree_map.h" #include "absl/status/statusor.h" #include "absl/types/span.h" #include "p4/v1/p4runtime.pb.h" @@ -31,8 +31,13 @@ namespace p4_symbolic { namespace ir { -// Table entries by table name. -using TableEntries = std::unordered_map>; +// IR table entries keyed by table name. +// An ordered map is required because in `InitializeTableEntries` we loop +// through each table entry of each table to construct the symbolic variables +// and constraints of the symbolic table entries. If the map were to be +// unordered, the resulting order of symbolic variables and the SMT formulae +// will be nondeterministic. +using TableEntries = absl::btree_map>; // Returns table entries in P4-Symbolic IR, keyed by table name. absl::StatusOr ParseTableEntries( diff --git a/p4_symbolic/main.cc b/p4_symbolic/main.cc index d449908e..388bb608 100644 --- a/p4_symbolic/main.cc +++ b/p4_symbolic/main.cc @@ -18,8 +18,11 @@ // Produces test packets that hit every row in the P4 program tables. #include -#include +#include +#include +#include #include +#include #include "absl/flags/flag.h" #include "absl/flags/parse.h" @@ -27,9 +30,12 @@ #include "absl/status/status.h" #include "absl/strings/str_format.h" #include "glog/logging.h" +#include "google/protobuf/message_lite.h" #include "gutil/io.h" +#include "gutil/status.h" #include "p4/v1/p4runtime.pb.h" #include "p4_pdpi/internal/ordered_map.h" +#include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/test_util.h" @@ -54,21 +60,23 @@ absl::StatusOr GetConcretePacketsCoveringAllTableEntries( // Loop over tables in a deterministic order for output consistency // (important for CI tests). - for (const auto &[name, table] : Ordered(solver_state.program.tables())) { + for (const auto &[table_name, table] : + Ordered(solver_state.program.tables())) { int row_count = 0; - if (solver_state.entries.count(name) > 0) { - row_count = static_cast(solver_state.entries.at(name).size()); + if (solver_state.context.table_entries.count(table_name) > 0) { + row_count = static_cast( + solver_state.context.table_entries.at(table_name).size()); } for (int i = -1; i < row_count; i++) { - std::string banner = - "Finding packet for table " + name + " and row " + std::to_string(i); + std::string banner = "Finding packet for table " + table_name + + " and row " + std::to_string(i); result << std::string(kColumnSize, '=') << std::endl << banner << std::endl << std::string(kColumnSize, '=') << std::endl; p4_symbolic::symbolic::Assertion table_entry_assertion = - [name = name, + [name = table_name, i](const p4_symbolic::symbolic::SymbolicContext &symbolic_context) { const p4_symbolic::symbolic::SymbolicTableMatch &match = symbolic_context.trace.matched_entries.at(name); diff --git a/p4_symbolic/packet_synthesizer/criteria_generator.cc b/p4_symbolic/packet_synthesizer/criteria_generator.cc index c86174c5..cc6e44e0 100644 --- a/p4_symbolic/packet_synthesizer/criteria_generator.cc +++ b/p4_symbolic/packet_synthesizer/criteria_generator.cc @@ -28,6 +28,7 @@ #include "p4_symbolic/packet_synthesizer/packet_synthesis_criteria.pb.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/symbolic/table.h" +#include "p4_symbolic/symbolic/table_entry.h" #include "p4_symbolic/symbolic/util.h" namespace p4_symbolic::packet_synthesizer { @@ -81,9 +82,9 @@ GenerateSynthesisCriteriaFor(const EntryCoverageGoal& goal, // Add one synthesis criteria with table entry reachability constraint per // each table entry. bool table_is_empty = true; - auto it = solver_state.entries.find(table_name); - if (it != solver_state.entries.end()) { - const std::vector& entries = it->second; + auto it = solver_state.context.table_entries.find(table_name); + if (it != solver_state.context.table_entries.end()) { + const std::vector& entries = it->second; if (!entries.empty()) table_is_empty = false; for (int i = 0; i < entries.size(); i++) { criteria.mutable_table_entry_reachability_criteria()->set_match_index( diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel index b5e302f4..6268775c 100644 --- a/p4_symbolic/symbolic/BUILD.bazel +++ b/p4_symbolic/symbolic/BUILD.bazel @@ -31,6 +31,7 @@ cc_library( "parser.cc", "symbolic.cc", "table.cc", + "table_entry.cc", "util.cc", "v1model.cc", "values.cc", @@ -45,6 +46,7 @@ cc_library( "parser.h", "symbolic.h", "table.h", + "table_entry.h", "util.h", "v1model.h", "v1model_intrinsic.h", @@ -73,6 +75,8 @@ cc_library( "@com_gnu_gmp//:gmp", "@com_google_absl//absl/base:core_headers", "@com_google_absl//absl/cleanup", + "@com_google_absl//absl/container:btree", + "@com_google_absl//absl/container:flat_hash_map", "@com_google_absl//absl/status", "@com_google_absl//absl/status:statusor", "@com_google_absl//absl/strings", @@ -132,12 +136,13 @@ cc_test( srcs = ["values_test.cc"], deps = [ ":symbolic", + "//gutil:proto", "//gutil:status_matchers", - "//gutil:testing", "//p4_pdpi:ir_cc_proto", "//p4_symbolic:z3_util", "@com_github_z3prover_z3//:api", "@com_google_absl//absl/container:flat_hash_map", + "@com_google_absl//absl/status", "@com_google_absl//absl/strings", "@com_google_googletest//:gtest_main", ], @@ -172,3 +177,32 @@ cc_test( "@com_google_googletest//:gtest_main", ], ) + +cc_test( + name = "table_entry_test", + srcs = ["table_entry_test.cc"], + data = [ + "//p4_symbolic/testdata:ipv4-routing/basic.config.json", + "//p4_symbolic/testdata:ipv4-routing/basic.p4info.pb.txt", + "//p4_symbolic/testdata:ipv4-routing/entries.pb.txt", + ], + deps = [ + ":symbolic", + "//gutil:status", + "//gutil:status_matchers", + "//p4_pdpi:ir_cc_proto", + "//p4_symbolic:test_util", + "//p4_symbolic/ir", + "//p4_symbolic/ir:ir_cc_proto", + "//p4_symbolic/ir:parser", + "//p4_symbolic/ir:table_entries", + "@com_github_p4lang_p4runtime//:p4info_cc_proto", + "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", + "@com_github_z3prover_z3//:api", + "@com_google_absl//absl/status", + "@com_google_absl//absl/status:statusor", + "@com_google_absl//absl/strings", + "@com_google_googletest//:gtest_main", + "@com_google_protobuf//:protobuf", + ], +) diff --git a/p4_symbolic/symbolic/action.cc b/p4_symbolic/symbolic/action.cc index 389c02a1..6c750155 100644 --- a/p4_symbolic/symbolic/action.cc +++ b/p4_symbolic/symbolic/action.cc @@ -14,18 +14,27 @@ #include "p4_symbolic/symbolic/action.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 "absl/strings/string_view.h" #include "glog/logging.h" +#include "google/protobuf/repeated_ptr_field.h" #include "gutil/collections.h" +#include "gutil/status.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/v1model.h" +#include "p4_symbolic/symbolic/values.h" #include "p4_symbolic/z3_util.h" +#include "z3++.h" namespace p4_symbolic { namespace symbolic { @@ -309,9 +318,8 @@ absl::StatusOr EvaluateRExpression( absl::Status EvaluateAction(const ir::Action &action, const google::protobuf::RepeatedPtrField< pdpi::IrActionInvocation::IrActionParam> &args, - SymbolicPerPacketState *state, - values::P4RuntimeTranslator *translator, - z3::context &z3_context, const z3::expr &guard) { + SolverState &state, SymbolicPerPacketState *headers, + const z3::expr &guard) { // Construct this action's context. ActionContext context; context.action_name = action.action_definition().preamble().name(); @@ -339,16 +347,16 @@ absl::Status EvaluateAction(const ir::Action &action, ASSIGN_OR_RETURN( z3::expr parameter_value, values::FormatP4RTValue( - z3_context, /*field_name=*/"", - param_definition->param().type_name().name(), arg.value(), - param_definition->param().bitwidth(), translator)); + /*field_name=*/"", param_definition->param().type_name().name(), + arg.value(), param_definition->param().bitwidth(), + *state.context.z3_context, state.translator)); context.scope.insert({param_definition->param().name(), parameter_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, state, &context, z3_context, guard)); + RETURN_IF_ERROR(EvaluateStatement(statement, headers, &context, + *state.context.z3_context, guard)); } return absl::OkStatus(); diff --git a/p4_symbolic/symbolic/action.h b/p4_symbolic/symbolic/action.h index 5a4ab7f0..b5082fbb 100644 --- a/p4_symbolic/symbolic/action.h +++ b/p4_symbolic/symbolic/action.h @@ -22,11 +22,13 @@ #include #include +#include "absl/status/status.h" +#include "absl/status/statusor.h" #include "google/protobuf/repeated_ptr_field.h" #include "p4_pdpi/ir.pb.h" #include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/symbolic/context.h" -#include "p4_symbolic/symbolic/values.h" +#include "p4_symbolic/symbolic/symbolic.h" #include "z3++.h" namespace p4_symbolic { @@ -40,9 +42,8 @@ namespace action { absl::Status EvaluateAction(const ir::Action &action, const google::protobuf::RepeatedPtrField< pdpi::IrActionInvocation::IrActionParam> &args, - SymbolicPerPacketState *state, - values::P4RuntimeTranslator *translator, - z3::context &z3_context, const z3::expr &guard); + 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 diff --git a/p4_symbolic/symbolic/conditional.cc b/p4_symbolic/symbolic/conditional.cc index 6334f96c..c5b7ee81 100644 --- a/p4_symbolic/symbolic/conditional.cc +++ b/p4_symbolic/symbolic/conditional.cc @@ -17,14 +17,17 @@ #include "p4_symbolic/symbolic/conditional.h" -#include "absl/status/status.h" -#include "absl/strings/string_view.h" -#include "absl/strings/substitute.h" +#include + +#include "absl/status/statusor.h" #include "gutil/status.h" #include "p4_symbolic/ir/ir.h" +#include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/symbolic/action.h" +#include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/control.h" #include "p4_symbolic/symbolic/operators.h" +#include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/symbolic/util.h" #include "z3++.h" @@ -33,14 +36,14 @@ namespace symbolic { namespace conditional { absl::StatusOr EvaluateConditional( - const ir::Dataplane &data_plane, const ir::Conditional &conditional, - SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, - z3::context &z3_context, const z3::expr &guard) { + const ir::Conditional &conditional, SolverState &state, + 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(), *state, - fake_context, z3_context)); + ASSIGN_OR_RETURN( + z3::expr condition, + action::EvaluateRValue(conditional.condition(), *headers, fake_context, + *state.context.z3_context)); ASSIGN_OR_RETURN(z3::expr negated_condition, operators::Not(condition)); // Build new guards for each branch. @@ -56,21 +59,20 @@ absl::StatusOr EvaluateConditional( }; // Evaluate both branches. - ASSIGN_OR_RETURN( - SymbolicTableMatches if_matches, - control::EvaluateControl( - data_plane, get_next_control_for_branch(conditional.if_branch()), - state, translator, z3_context, if_guard)); - ASSIGN_OR_RETURN( - SymbolicTableMatches else_matches, - control::EvaluateControl( - data_plane, get_next_control_for_branch(conditional.else_branch()), - state, translator, z3_context, else_guard)); + ASSIGN_OR_RETURN(SymbolicTableMatches if_matches, + control::EvaluateControl( + get_next_control_for_branch(conditional.if_branch()), + state, headers, if_guard)); + ASSIGN_OR_RETURN(SymbolicTableMatches else_matches, + control::EvaluateControl( + get_next_control_for_branch(conditional.else_branch()), + state, headers, else_guard)); // Now we have two traces that need merging. - ASSIGN_OR_RETURN(SymbolicTableMatches merged_matches, - util::MergeMatchesOnCondition(condition, if_matches, - else_matches, z3_context)); + ASSIGN_OR_RETURN( + SymbolicTableMatches merged_matches, + util::MergeMatchesOnCondition(condition, if_matches, else_matches, + *state.context.z3_context)); if (!conditional.optimized_symbolic_execution_info() .continue_to_merge_point()) { @@ -82,9 +84,8 @@ absl::StatusOr EvaluateConditional( ASSIGN_OR_RETURN( SymbolicTableMatches result, control::EvaluateControl( - data_plane, conditional.optimized_symbolic_execution_info().merge_point(), - state, translator, z3_context, guard)); + state, headers, guard)); // Merge the result of execution from the merge point with the result of // merged if/else branches. diff --git a/p4_symbolic/symbolic/conditional.h b/p4_symbolic/symbolic/conditional.h index 4b1e9a0d..fb6eb8d0 100644 --- a/p4_symbolic/symbolic/conditional.h +++ b/p4_symbolic/symbolic/conditional.h @@ -18,10 +18,10 @@ #ifndef P4_SYMBOLIC_SYMBOLIC_CONDITIONAL_H_ #define P4_SYMBOLIC_SYMBOLIC_CONDITIONAL_H_ -#include "p4_symbolic/ir/ir.h" +#include "absl/status/statusor.h" #include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/symbolic/context.h" -#include "p4_symbolic/symbolic/values.h" +#include "p4_symbolic/symbolic/symbolic.h" #include "z3++.h" namespace p4_symbolic { @@ -29,9 +29,8 @@ namespace symbolic { namespace conditional { absl::StatusOr EvaluateConditional( - const ir::Dataplane &data_plane, const ir::Conditional &conditional, - SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, - z3::context &z3_context, const z3::expr &guard); + const ir::Conditional &conditional, SolverState &state, + SymbolicPerPacketState *headers, const z3::expr &guard); } // namespace conditional } // namespace symbolic diff --git a/p4_symbolic/symbolic/context.h b/p4_symbolic/symbolic/context.h index 35faeee0..492bc8fc 100644 --- a/p4_symbolic/symbolic/context.h +++ b/p4_symbolic/symbolic/context.h @@ -20,6 +20,7 @@ #include "absl/container/btree_map.h" #include "p4_symbolic/symbolic/guarded_map.h" +#include "p4_symbolic/symbolic/table_entry.h" #include "z3++.h" namespace p4_symbolic { @@ -130,6 +131,7 @@ class SymbolicContext { SymbolicPerPacketState ingress_headers; SymbolicPerPacketState parsed_headers; SymbolicPerPacketState egress_headers; + TableEntries table_entries; SymbolicTrace trace; }; diff --git a/p4_symbolic/symbolic/control.cc b/p4_symbolic/symbolic/control.cc index cdac32e6..91066ebc 100644 --- a/p4_symbolic/symbolic/control.cc +++ b/p4_symbolic/symbolic/control.cc @@ -20,55 +20,49 @@ #include "p4_symbolic/symbolic/control.h" -#include +#include #include "absl/status/status.h" +#include "absl/status/statusor.h" #include "absl/strings/str_cat.h" #include "gutil/status.h" #include "p4_symbolic/ir/ir.h" #include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/symbolic/conditional.h" #include "p4_symbolic/symbolic/context.h" +#include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/symbolic/table.h" +#include "z3++.h" namespace p4_symbolic::symbolic::control { absl::StatusOr EvaluatePipeline( - const ir::Dataplane &data_plane, const std::string &pipeline_name, - SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, - z3::context &z3_context, const z3::expr &guard) { - if (auto it = data_plane.program.pipeline().find(pipeline_name); - it != data_plane.program.pipeline().end()) { - return EvaluateControl(data_plane, it->second.initial_control(), state, - translator, z3_context, guard); + const std::string &pipeline_name, SolverState &state, + 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); } return gutil::InvalidArgumentErrorBuilder() << "cannot evaluate unknown pipeline: '" << pipeline_name << "'"; } absl::StatusOr EvaluateControl( - const ir::Dataplane &data_plane, const std::string &control_name, - SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, - z3::context &z3_context, const z3::expr &guard) { + const std::string &control_name, SolverState &state, + 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(); // Find out what type of control we need to evaluate. - if (data_plane.program.tables().count(control_name) == 1) { + if (state.program.tables().contains(control_name)) { // Table: call EvaluateTable on table and its entries. - const ir::Table &table = data_plane.program.tables().at(control_name); - std::vector table_entries; - if (data_plane.entries.count(control_name) == 1) { - table_entries = data_plane.entries.at(control_name); - } - return table::EvaluateTable(data_plane, table, table_entries, state, - translator, z3_context, guard); - } else if (data_plane.program.conditionals().count(control_name) == 1) { + const ir::Table &table = state.program.tables().at(control_name); + return table::EvaluateTable(table, state, headers, guard); + } else if (state.program.conditionals().contains(control_name)) { // Conditional: let EvaluateConditional handle it. const ir::Conditional &conditional = - data_plane.program.conditionals().at(control_name); - return conditional::EvaluateConditional(data_plane, conditional, state, - translator, z3_context, guard); + state.program.conditionals().at(control_name); + return conditional::EvaluateConditional(conditional, state, headers, guard); } else { // Something else: unsupported. return absl::UnimplementedError( diff --git a/p4_symbolic/symbolic/control.h b/p4_symbolic/symbolic/control.h index 6be661bd..6969fc61 100644 --- a/p4_symbolic/symbolic/control.h +++ b/p4_symbolic/symbolic/control.h @@ -59,9 +59,9 @@ #include -#include "p4_symbolic/ir/ir.h" +#include "absl/status/statusor.h" #include "p4_symbolic/symbolic/context.h" -#include "p4_symbolic/symbolic/values.h" +#include "p4_symbolic/symbolic/symbolic.h" #include "z3++.h" namespace p4_symbolic { @@ -70,15 +70,13 @@ namespace control { // Evaluate the passed pipeline. absl::StatusOr EvaluatePipeline( - const ir::Dataplane &data_plane, const std::string &pipeline_name, - SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, - z3::context &z3_context, const z3::expr &guard); + const std::string &pipeline_name, SolverState &state, + SymbolicPerPacketState *headers, const z3::expr &guard); // Evaluate the passed control construct. absl::StatusOr EvaluateControl( - const ir::Dataplane &data_plane, const std::string &control_name, - SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, - z3::context &z3_context, const z3::expr &guard); + const std::string &control_name, SolverState &state, + SymbolicPerPacketState *headers, const z3::expr &guard); } // namespace control } // namespace symbolic diff --git a/p4_symbolic/symbolic/parser.cc b/p4_symbolic/symbolic/parser.cc index db5fe9b7..0b604988 100644 --- a/p4_symbolic/symbolic/parser.cc +++ b/p4_symbolic/symbolic/parser.cc @@ -14,16 +14,21 @@ #include "p4_symbolic/symbolic/parser.h" +#include #include +#include #include #include "absl/status/status.h" +#include "absl/status/statusor.h" #include "absl/strings/str_format.h" +#include "absl/types/optional.h" #include "gutil/status.h" #include "p4_pdpi/internal/ordered_map.h" #include "p4_symbolic/ir/ir.h" #include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/symbolic/action.h" +#include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/operators.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/symbolic/util.h" @@ -43,7 +48,7 @@ namespace { absl::Status EvaluateExtractParserOperation( const ir::P4Program &program, const ir::ParserOperation::Extract &extract_op, - SymbolicPerPacketState &state, z3::context &z3_context, + SymbolicPerPacketState &headers, z3::context &z3_context, const z3::expr &guard) { // The extracted header must exists. const std::string &header_name = extract_op.header().header_name(); @@ -53,16 +58,16 @@ absl::Status EvaluateExtractParserOperation( } // Set the "valid" and "extracted" fields of the header to `guard`. - RETURN_IF_ERROR(state.Set(header_name, kValidPseudoField, - z3_context.bool_val(true), guard)); - RETURN_IF_ERROR(state.Set(header_name, kExtractedPseudoField, - z3_context.bool_val(true), guard)); + RETURN_IF_ERROR(headers.Set(header_name, kValidPseudoField, + z3_context.bool_val(true), guard)); + RETURN_IF_ERROR(headers.Set(header_name, kExtractedPseudoField, + z3_context.bool_val(true), guard)); // Verify if all fields of the header are single, free bit-vector variables. for (const auto &[field_name, ir_field] : Ordered(it->second.fields())) { std::string field_full_name = absl::StrFormat("%s.%s", header_name, field_name); - ASSIGN_OR_RETURN(const z3::expr &field, state.Get(field_full_name)); + ASSIGN_OR_RETURN(const z3::expr &field, headers.Get(field_full_name)); if (field.to_string() != field_full_name || !field.is_bv() || field.get_sort().bv_size() != static_cast(ir_field.bitwidth())) { @@ -78,11 +83,12 @@ absl::Status EvaluateExtractParserOperation( // Constructs a symbolic expression corresponding to the given R-value of the // set operation. absl::StatusOr EvaluateSetOperationRValue( - const ir::ParserOperation::Set &set_op, const SymbolicPerPacketState &state, - const action::ActionContext &context, z3::context &z3_context) { + const ir::ParserOperation::Set &set_op, + const SymbolicPerPacketState &headers, const action::ActionContext &context, + z3::context &z3_context) { switch (set_op.rvalue_case()) { case ir::ParserOperation::Set::RvalueCase::kFieldRvalue: { - return action::EvaluateFieldValue(set_op.field_rvalue(), state); + return action::EvaluateFieldValue(set_op.field_rvalue(), headers); } case ir::ParserOperation::Set::RvalueCase::kHexstrRvalue: { return action::EvaluateHexStr(set_op.hexstr_rvalue(), z3_context); @@ -92,7 +98,7 @@ absl::StatusOr EvaluateSetOperationRValue( << "Lookahead R-values for set operations are not supported."; } case ir::ParserOperation::Set::RvalueCase::kExpressionRvalue: { - return action::EvaluateRExpression(set_op.expression_rvalue(), state, + return action::EvaluateRExpression(set_op.expression_rvalue(), headers, context, z3_context); } default: { @@ -105,29 +111,29 @@ absl::StatusOr EvaluateSetOperationRValue( // Evaluates the given "set" parser operation. absl::Status EvaluateSetParserOperation(const ir::ParserOperation::Set &set_op, - SymbolicPerPacketState &state, + SymbolicPerPacketState &headers, const action::ActionContext &context, z3::context &z3_context, const z3::expr &guard) { // Get the field name of the L-value and the expression of the R-value. const ir::FieldValue &field_value = set_op.lvalue(); ASSIGN_OR_RETURN(z3::expr rvalue, EvaluateSetOperationRValue( - set_op, state, context, z3_context)); + set_op, headers, context, z3_context)); // Set the header field to the symbolic expression. - RETURN_IF_ERROR(state.Set(field_value.header_name(), field_value.field_name(), - rvalue, guard)); + RETURN_IF_ERROR(headers.Set(field_value.header_name(), + field_value.field_name(), rvalue, guard)); return absl::OkStatus(); } // Evaluates the given "primitive" parser operation. absl::Status EvaluatePrimitiveParserOperation( const ir::ParserOperation::Primitive &primitive, - SymbolicPerPacketState &state, action::ActionContext &context, + SymbolicPerPacketState &headers, action::ActionContext &context, z3::context &z3_context, const z3::expr &guard) { switch (primitive.statement_case()) { case ir::ParserOperation::Primitive::StatementCase::kAssignment: { - return action::EvaluateAssignmentStatement(primitive.assignment(), &state, - &context, z3_context, guard); + return action::EvaluateAssignmentStatement( + primitive.assignment(), &headers, &context, z3_context, guard); } default: { return gutil::UnimplementedErrorBuilder() @@ -143,21 +149,21 @@ absl::Status EvaluatePrimitiveParserOperation( // Evaluates the given parser operation. absl::Status EvaluateParserOperation(const ir::P4Program &program, const ir::ParserOperation &op, - SymbolicPerPacketState &state, + SymbolicPerPacketState &headers, action::ActionContext &context, z3::context &z3_context, const z3::expr &guard) { switch (op.operation_case()) { case ir::ParserOperation::OperationCase::kExtract: { - return EvaluateExtractParserOperation(program, op.extract(), state, + return EvaluateExtractParserOperation(program, op.extract(), headers, z3_context, guard); } case ir::ParserOperation::OperationCase::kSet: { - return EvaluateSetParserOperation(op.set(), state, context, z3_context, + return EvaluateSetParserOperation(op.set(), headers, context, z3_context, guard); } case ir::ParserOperation::OperationCase::kPrimitive: { - return EvaluatePrimitiveParserOperation(op.primitive(), state, context, + return EvaluatePrimitiveParserOperation(op.primitive(), headers, context, z3_context, guard); } default: { @@ -205,7 +211,7 @@ absl::StatusOr ConstructHexStringMatchCondition( // independently regardless of whether the transition key in the given // `parse_state` matches another transition or not. absl::StatusOr> ConstructMatchConditions( - const ir::ParseState &parse_state, const SymbolicPerPacketState &state, + const ir::ParseState &parse_state, const SymbolicPerPacketState &headers, z3::context &z3_context, const z3::expr &guard) { // Collect all transition key fields to construct the transition key. z3::expr_vector key_fields(z3_context); @@ -222,7 +228,7 @@ absl::StatusOr> ConstructMatchConditions( const ir::FieldValue &field_value = key_field.field(); ASSIGN_OR_RETURN( z3::expr key_field_expr, - state.Get(field_value.header_name(), field_value.field_name())); + headers.Get(field_value.header_name(), field_value.field_name())); key_fields.push_back(std::move(key_field_expr)); } @@ -357,19 +363,19 @@ absl::StatusOr GetNextState( absl::Status SetParserError(const ir::P4Program &program, z3::context &z3_context, - SymbolicPerPacketState &state, + SymbolicPerPacketState &headers, const std::string &error_name, const z3::expr &guard) { ASSIGN_OR_RETURN(z3::expr error_code, GetErrorCodeExpression(program, error_name, z3_context)); - return state.Set(v1model::kParserErrorField, std::move(error_code), guard); + return headers.Set(v1model::kParserErrorField, std::move(error_code), guard); } // Evaluates the parse state with the given `state_name` in the given parser. absl::Status EvaluateParseState(const ir::P4Program &program, const ir::Parser &parser, const std::string &state_name, - SymbolicPerPacketState &state, + SymbolicPerPacketState &headers, z3::context &z3_context, const z3::expr &guard) { // Base case. We got to the end of the parser execution path. @@ -405,14 +411,14 @@ absl::Status EvaluateParseState(const ir::P4Program &program, // Evaluate the parser operations in this parse state. action::ActionContext fake_context = {state_name, {}}; for (const ir::ParserOperation &op : parse_state.parser_ops()) { - RETURN_IF_ERROR(EvaluateParserOperation(program, op, state, fake_context, + RETURN_IF_ERROR(EvaluateParserOperation(program, op, headers, fake_context, z3_context, guard)); } // Construct the match condition of each transition. ASSIGN_OR_RETURN( std::vector match_conditions, - ConstructMatchConditions(parse_state, state, z3_context, guard)); + ConstructMatchConditions(parse_state, headers, z3_context, guard)); // Construct the transition guard of each transition. std::vector transition_guards = ConstructTransitionGuards(match_conditions, guard); @@ -425,7 +431,7 @@ absl::Status EvaluateParseState(const ir::P4Program &program, ASSIGN_OR_RETURN(std::string next_state, GetNextState(parse_state.transitions(i))); if (next_state != merge_point) { - RETURN_IF_ERROR(EvaluateParseState(program, parser, next_state, state, + RETURN_IF_ERROR(EvaluateParseState(program, parser, next_state, headers, z3_context, transition_guards[i])); } } @@ -453,7 +459,7 @@ absl::Status EvaluateParseState(const ir::P4Program &program, // state" in this case will be the end of parser, so there is no need to do // anything else. The fall-through guard should be sufficient to ensure that // if the fall-through guard is true, no other transitions will happen. - RETURN_IF_ERROR(SetParserError(program, z3_context, state, "NoMatch", + RETURN_IF_ERROR(SetParserError(program, z3_context, headers, "NoMatch", fall_through_guard)); // If a fall-through is possible, the `merge_point_guard` should be the @@ -466,7 +472,7 @@ absl::Status EvaluateParseState(const ir::P4Program &program, // different path. if (parse_state.optimized_symbolic_execution_info() .continue_to_merge_point()) { - return EvaluateParseState(program, parser, merge_point, state, z3_context, + return EvaluateParseState(program, parser, merge_point, headers, z3_context, merge_point_guard); } else { return absl::OkStatus(); diff --git a/p4_symbolic/symbolic/symbolic.cc b/p4_symbolic/symbolic/symbolic.cc index e53920e7..a5082eba 100644 --- a/p4_symbolic/symbolic/symbolic.cc +++ b/p4_symbolic/symbolic/symbolic.cc @@ -14,8 +14,13 @@ #include "p4_symbolic/symbolic/symbolic.h" +#include +#include #include +#include +#include #include +#include #include "absl/cleanup/cleanup.h" #include "absl/status/status.h" @@ -23,8 +28,14 @@ #include "absl/types/optional.h" #include "glog/logging.h" #include "gutil/status.h" +#include "p4/v1/p4runtime.pb.h" #include "p4_pdpi/internal/ordered_map.h" +#include "p4_symbolic/ir/ir.h" +#include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/ir/parser.h" +#include "p4_symbolic/ir/table_entries.h" +#include "p4_symbolic/symbolic/context.h" +#include "p4_symbolic/symbolic/table_entry.h" #include "p4_symbolic/symbolic/util.h" #include "p4_symbolic/symbolic/v1model.h" #include "p4_symbolic/symbolic/values.h" @@ -33,6 +44,36 @@ namespace p4_symbolic { namespace symbolic { +namespace { + +// Initializes the table entry objects in the symbolic context based on the +// given `ir_entries`. For symbolic table entries, symbolic variables and their +// corresponding constraints will be created within the given solver context. +absl::Status InitializeTableEntries(SolverState &state, + ir::TableEntries ir_entries) { + // Create table entry objects for both concrete and symbolic entries. + for (auto &[table_name, per_table_ir_entries] : ir_entries) { + // Check that the table entries do not exist for the table. + if (auto it = state.context.table_entries.find(table_name); + it != state.context.table_entries.end() && !it->second.empty()) { + return gutil::InternalErrorBuilder() + << "Expected no table entry for table '" << table_name + << "'. Found: " << it->second.size() << " entries."; + } + + // 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))); + } + } + + return absl::OkStatus(); +} + +} // namespace + std::string SolverState::GetSolverSMT() { if (!solver) return ""; return solver->to_smt2(); @@ -55,34 +96,32 @@ std::string SolverState::GetHeadersAndSolverConstraintsSMT() { return result.str(); } -absl::StatusOr> EvaluateP4Program( - const p4::v1::ForwardingPipelineConfig &config, - const std::vector &entries, +absl::StatusOr> EvaluateP4Program( + const ir::P4Program &program, const ir::TableEntries &entries, const std::vector &physical_ports, const TranslationPerType &translation_per_type) { - // Parse the P4 config and entries into the P4-symbolic IR. - ASSIGN_OR_RETURN(ir::Dataplane dataplane, ir::ParseToIr(config, entries)); + // Initialize the solver state. + auto state = std::make_unique(program); + SymbolicContext &context = state->context; - auto solver_state = - std::make_unique(dataplane.program, dataplane.entries); - SymbolicContext &context = solver_state->context; - values::P4RuntimeTranslator &translator = solver_state->translator; + // Initialize the table entries. + RETURN_IF_ERROR(InitializeTableEntries(*state, entries)); // Initialize the p4runtime translator with statically translated types. for (const auto &[type, translation] : translation_per_type) { - translator.p4runtime_translation_allocators.emplace( + state->translator.p4runtime_translation_allocators.emplace( type, values::IdAllocator(translation)); } // Evaluate the main program, assuming it conforms to V1 model. - RETURN_IF_ERROR( - v1model::EvaluateV1model(dataplane, physical_ports, context, translator)); + RETURN_IF_ERROR(v1model::EvaluateV1model(*state, physical_ports)); // Restrict the value of all fields with (purely static, i.e. // dynamic_translation = false) P4RT translated types to what has been used in // TranslationPerType. This should be done after the symbolic execution since // P4Symbolic does not initially know which fields have translated types. - for (const auto &[field, type] : Ordered(translator.fields_p4runtime_type)) { + for (const auto &[field, type] : + Ordered(state->translator.fields_p4runtime_type)) { if (auto it = translation_per_type.find(type); it != translation_per_type.end() && !it->second.dynamic_translation) { ASSIGN_OR_RETURN(z3::expr field_expr, context.ingress_headers.Get(field)); @@ -92,15 +131,15 @@ absl::StatusOr> EvaluateP4Program( constraint = constraint || (field_expr == static_cast(numeric_value)); } - solver_state->solver->add(constraint); + state->solver->add(constraint); } } // Restrict ports to the available physical ports. // TODO: Support generating packet-out packets from the CPU port. if (physical_ports.empty()) { - solver_state->solver->add(context.ingress_port != kCpuPort); - solver_state->solver->add(context.ingress_port != kDropPort); + state->solver->add(context.ingress_port != kCpuPort); + state->solver->add(context.ingress_port != kDropPort); } else { z3::expr ingress_port_is_physical = context.z3_context->bool_val(false); z3::expr egress_port_is_physical = context.z3_context->bool_val(false); @@ -110,30 +149,39 @@ absl::StatusOr> EvaluateP4Program( egress_port_is_physical = egress_port_is_physical || context.egress_port == port; } - solver_state->solver->add(ingress_port_is_physical); + state->solver->add(ingress_port_is_physical); // TODO: Lift this constraint, it should not be necessary and // prevents generation of packet-ins. - solver_state->solver->add(context.trace.dropped || egress_port_is_physical); + state->solver->add(context.trace.dropped || egress_port_is_physical); } // Assemble and return result. - return solver_state; + return state; } -absl::StatusOr> Solve( - SolverState &solver_state) { - z3::check_result check_result = solver_state.solver->check(); +absl::StatusOr> EvaluateP4Program( + const p4::v1::ForwardingPipelineConfig &config, + const std::vector &entries, + const std::vector &physical_ports, + const TranslationPerType &translation_per_type) { + // Parse the P4 config and concrete PI entries into the P4-symbolic IR. + ASSIGN_OR_RETURN(ir::Dataplane dataplane, ir::ParseToIr(config, entries)); + return EvaluateP4Program(dataplane.program, dataplane.entries, physical_ports, + translation_per_type); +} + +absl::StatusOr> Solve(SolverState &state) { + z3::check_result check_result = state.solver->check(); switch (check_result) { case z3::unsat: case z3::unknown: return absl::nullopt; case z3::sat: - z3::model packet_model = solver_state.solver->get_model(); - ASSIGN_OR_RETURN( - ConcreteContext result, - util::ExtractFromModel(solver_state.context, packet_model, - solver_state.translator)); + z3::model packet_model = state.solver->get_model(); + ASSIGN_OR_RETURN(ConcreteContext result, + util::ExtractFromModel(state.context, packet_model, + state.translator)); return result; } LOG(DFATAL) << "invalid Z3 check() result: " @@ -142,32 +190,26 @@ absl::StatusOr> Solve( } absl::StatusOr> Solve( - SolverState &solver_state, const Assertion &assertion) { - ASSIGN_OR_RETURN(z3::expr constraint, assertion(solver_state.context)); - solver_state.solver->push(); - solver_state.solver->add(constraint); - auto pop = absl::Cleanup([&] { solver_state.solver->pop(); }); - return Solve(solver_state); -} - -absl::StatusOr> Solve( - const std::unique_ptr &solver_state, - const Assertion &assertion) { - return Solve(*solver_state, assertion); + SolverState &state, const Assertion &assertion) { + ASSIGN_OR_RETURN(z3::expr constraint, assertion(state.context)); + state.solver->push(); + state.solver->add(constraint); + auto pop = absl::Cleanup([&] { state.solver->pop(); }); + return Solve(state); } -std::string DebugSMT(const std::unique_ptr &solver_state, +std::string DebugSMT(const std::unique_ptr &state, const Assertion &assertion) { - absl::StatusOr constraint = assertion(solver_state->context); + absl::StatusOr constraint = assertion(state->context); if (!constraint.ok()) { return "Failed to evaluate the given assertion. " + constraint.status().ToString(); } - solver_state->solver->push(); - solver_state->solver->add(*constraint); - std::string smt = solver_state->GetSolverSMT(); - solver_state->solver->pop(); + state->solver->push(); + state->solver->add(*constraint); + std::string smt = state->GetSolverSMT(); + state->solver->pop(); return smt; } diff --git a/p4_symbolic/symbolic/symbolic.h b/p4_symbolic/symbolic/symbolic.h index 4f0b44e4..31bec062 100644 --- a/p4_symbolic/symbolic/symbolic.h +++ b/p4_symbolic/symbolic/symbolic.h @@ -18,13 +18,18 @@ #ifndef P4_SYMBOLIC_SYMBOLIC_SYMBOLIC_H_ #define P4_SYMBOLIC_SYMBOLIC_SYMBOLIC_H_ +#include +#include #include #include #include +#include #include "absl/container/btree_map.h" +#include "absl/status/statusor.h" #include "absl/strings/string_view.h" #include "p4/v1/p4runtime.pb.h" +#include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/ir/table_entries.h" #include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/values.h" @@ -72,9 +77,8 @@ constexpr absl::string_view kGotClonedPseudoField = "$got_cloned$"; // many times. class SolverState { public: - SolverState(ir::P4Program program, ir::TableEntries entries) + SolverState(ir::P4Program program) : program(std::move(program)), - entries(std::move(entries)), solver(std::make_unique(*context.z3_context)) {} SolverState(const SolverState &) = delete; SolverState(SolverState &&) = default; @@ -95,8 +99,6 @@ class SolverState { // The IR of the p4 program being analyzed. ir::P4Program program; - // Maps the name of a table to a list of its entries. - ir::TableEntries entries; // The symbolic context of our interpretation/analysis of the program, // including symbolic handles on packet headers and its trace. A new // z3::context object is created within each symbolic context. Note that this @@ -106,6 +108,7 @@ class SolverState { // Having the z3 solver defined here allows Z3 to remember interesting // deductions it made while solving for one particular assertion, and re-use // them during solving with future assertions. + // Note that the unique_ptr wrapper is necessary for b/291010571. std::unique_ptr solver; // Store the p4 runtime translator state for use by .Solve(...). values::P4RuntimeTranslator translator; @@ -134,7 +137,19 @@ using TranslationPerType = // string) annotation, a static mapping between the P4RT values and the // underlying bitvector values may be provided. Otherwise, a mapping is // inferred dynamically for such types. -absl::StatusOr> EvaluateP4Program( +// The given `entries` may contain symbolic or concrete table entries. +absl::StatusOr> EvaluateP4Program( + const ir::P4Program &program, const ir::TableEntries &entries, + const std::vector &physical_ports = {}, + const TranslationPerType &translation_per_type = {}); + +// Symbolically evaluates/interprets the given program against the given +// entries for every table in the program, and the available physical ports +// on the switch. Optionally, for types that have @p4runtime_translate(_, +// string) annotation, a static mapping between the P4RT values and the +// underlying bitvector values may be provided. Otherwise, a mapping is +// inferred dynamically for such types. +absl::StatusOr> EvaluateP4Program( const p4::v1::ForwardingPipelineConfig &config, const std::vector &entries, const std::vector &physical_ports = {}, @@ -142,12 +157,12 @@ absl::StatusOr> EvaluateP4Program( // Finds a concrete packet and flow in the program that satisfies the given // assertion and meets the structure constrained by solver_state. -absl::StatusOr> Solve(SolverState &solver_state); +absl::StatusOr> Solve(SolverState &state); absl::StatusOr> Solve( - SolverState &solver_state, const Assertion &assertion); + SolverState &state, const Assertion &assertion); // Dumps the underlying SMT program for debugging. -std::string DebugSMT(const std::unique_ptr &solver_state, +std::string DebugSMT(const std::unique_ptr &state, const Assertion &assertion); } // namespace symbolic diff --git a/p4_symbolic/symbolic/table.cc b/p4_symbolic/symbolic/table.cc index 059938f6..bd2aedb8 100644 --- a/p4_symbolic/symbolic/table.cc +++ b/p4_symbolic/symbolic/table.cc @@ -21,11 +21,15 @@ #include "p4_symbolic/symbolic/table.h" #include +#include +#include #include #include +#include #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/substitute.h" @@ -38,8 +42,11 @@ #include "p4_symbolic/ir/ir.h" #include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/symbolic/action.h" +#include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/control.h" #include "p4_symbolic/symbolic/operators.h" +#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/table_entry.h" #include "p4_symbolic/symbolic/util.h" #include "p4_symbolic/symbolic/values.h" #include "z3++.h" @@ -50,12 +57,6 @@ namespace table { namespace { -const pdpi::IrTableEntry &GetConcreteOrSymbolicPdpiIrTableEntry( - const ir::TableEntry &entry) { - return entry.has_concrete_entry() ? entry.concrete_entry() - : entry.symbolic_entry().sketch(); -} - // 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. @@ -100,8 +101,8 @@ int FindMatchWithName(const pdpi::IrTableEntry &entry, // - BMv2 - simple_switch.md // https://github.com/p4lang/behavioral-model/blob/main/docs/simple_switch.md#table-match-kinds-supported // -std::vector> SortEntries( - const ir::Table &table, const std::vector &entries) { +std::vector SortEntries(const ir::Table &table, + const std::vector &entries) { if (entries.empty()) return {}; // Find which *definition* of priority we should use by looking at the @@ -130,44 +131,34 @@ std::vector> SortEntries( } // The output array. - std::vector> sorted_entries; - sorted_entries.reserve(entries.size()); - for (int i = 0; i < entries.size(); i++) { - sorted_entries.push_back(std::make_pair(i, entries.at(i))); - } + std::vector sorted_entries(entries); // The sort comparator depends on the match types. - std::function &, - const std::pair &)> - comparator; + std::function comparator; if (has_ternary_or_optional) { // Sort by explicit priority. // Entries with numerically larger priority precede others. - comparator = [](const std::pair &entry1, - const std::pair &entry2) { - return GetConcreteOrSymbolicPdpiIrTableEntry(entry1.second).priority() > - GetConcreteOrSymbolicPdpiIrTableEntry(entry2.second).priority(); + comparator = [](const TableEntry &entry1, const TableEntry &entry2) { + return entry1.GetPdpiIrTableEntry().priority() > + entry2.GetPdpiIrTableEntry().priority(); }; } else if (lpm_match_name.has_value()) { // Sort by prefix length. // Entries with numerically larger prefix length precede others. - comparator = [&lpm_match_name]( - const std::pair &entry1, - const std::pair &entry2) { + comparator = [&lpm_match_name](const TableEntry &entry1, + const TableEntry &entry2) { auto is_lpm_match = [&lpm_match_name](const pdpi::IrMatch &match) -> bool { return match.name() == *lpm_match_name; }; - auto get_prefix_length = - [&is_lpm_match](const ir::TableEntry &entry) -> int { - auto &matches = GetConcreteOrSymbolicPdpiIrTableEntry(entry).matches(); + auto get_prefix_length = [&is_lpm_match](const TableEntry &entry) -> int { + auto &matches = entry.GetPdpiIrTableEntry().matches(); auto it = std::find_if(matches.begin(), matches.end(), is_lpm_match); return it == matches.end() ? 0 : it->lpm().prefix_length(); }; - return get_prefix_length(entry1.second) > - get_prefix_length(entry2.second); + return get_prefix_length(entry1) > get_prefix_length(entry2); }; } else { return sorted_entries; @@ -184,8 +175,7 @@ std::vector> SortEntries( absl::StatusOr EvaluateSingleMatch( const p4::config::v1::MatchField &match_definition, const std::string &field_name, const z3::expr &field_expression, - const pdpi::IrMatch &match, values::P4RuntimeTranslator *translator, - z3::context &z3_context) { + const pdpi::IrMatch &match, SolverState &state) { if (match_definition.match_case() != p4::config::v1::MatchField::kMatchType) { // Arch-specific match type. return absl::InvalidArgumentError( @@ -202,9 +192,10 @@ absl::StatusOr EvaluateSingleMatch( auto GetZ3Value = [&](const pdpi::IrValue &value) -> absl::StatusOr { - return values::FormatP4RTValue(z3_context, field_name, + return values::FormatP4RTValue(field_name, match_definition.type_name().name(), value, - match_definition.bitwidth(), translator); + match_definition.bitwidth(), + *state.context.z3_context, state.translator); }; switch (match_definition.match_type()) { @@ -257,13 +248,12 @@ absl::StatusOr EvaluateSingleMatch( // 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, - const SymbolicPerPacketState &state, - values::P4RuntimeTranslator *translator, z3::context &z3_context) { + const ir::Table &table, const pdpi::IrTableEntry &entry, SolverState &state, + const SymbolicPerPacketState &headers) { const std::string &table_name = table.table_definition().preamble().name(); // Construct the match condition expression. - z3::expr condition_expression = z3_context.bool_val(true); + 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(); @@ -300,12 +290,11 @@ absl::StatusOr EvaluateTableEntryCondition( 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 match_field_expr, - action::EvaluateFieldValue(match_field, state)); - ASSIGN_OR_RETURN( - z3::expr match_expression, - EvaluateSingleMatch(match_definition, field_name, match_field_expr, - match, translator, z3_context)); + 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)); } @@ -316,52 +305,53 @@ absl::StatusOr EvaluateTableEntryCondition( absl::Status EvaluateSingeTableEntryAction( const pdpi::IrActionInvocation &action, const google::protobuf::Map &actions, - SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, - z3::context &z3_context, const z3::expr &guard) { + SolverState &state, SymbolicPerPacketState *headers, + const z3::expr &guard) { // Check that the action invoked by entry exists. if (actions.count(action.name()) != 1) { return gutil::InvalidArgumentErrorBuilder() << "unknown action '" << action.name() << "'"; } return action::EvaluateAction(actions.at(action.name()), action.params(), - state, translator, z3_context, guard); + state, headers, guard); } // Constructs a symbolic expressions that represents the action invocation // corresponding to this entry. absl::Status EvaluateTableEntryAction( - const ir::Table &table, const pdpi::IrTableEntry &entry, int entry_index, + const ir::Table &table, const TableEntry &entry, const google::protobuf::Map &actions, - SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, - z3::context &z3_context, const z3::expr &guard) { - switch (entry.type_case()) { + 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(entry.action(), actions, - state, translator, - z3_context, guard)) + RETURN_IF_ERROR(EvaluateSingeTableEntryAction(ir_entry.action(), actions, + state, headers, guard)) .SetPrepend() - << "In table entry '" << entry.ShortDebugString() << "':"; + << "In table entry '" << ir_entry.ShortDebugString() << "':"; return absl::OkStatus(); case pdpi::IrTableEntry::kActionSet: { - auto &action_set = entry.action_set().actions(); + 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 // approximation, action i is executed iff `selector == i`. std::string selector_name = absl::StrFormat("action selector for entry #%d of table '%s'", - entry_index, entry.table_name()); - z3::expr selector = z3_context.int_const(selector_name.c_str()); - z3::expr unselected = z3_context.bool_val(true); + entry.GetIndex(), ir_entry.table_name()); + z3::expr selector = + state.context.z3_context->int_const(selector_name.c_str()); + z3::expr unselected = state.context.z3_context->bool_val(true); for (int i = 0; i < action_set.size(); ++i) { auto &action = action_set.at(i).action(); 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, - translator, z3_context, - guard && selected)) + RETURN_IF_ERROR(EvaluateSingeTableEntryAction( + action, actions, state, headers, guard && selected)) .SetPrepend() - << "In table entry '" << entry.ShortDebugString() << "':"; + << "In table entry '" << ir_entry.ShortDebugString() << "':"; } return absl::OkStatus(); } @@ -370,20 +360,22 @@ absl::Status EvaluateTableEntryAction( } return gutil::InvalidArgumentErrorBuilder() << "unexpected or missing action in table entry: " - << entry.DebugString(); + << ir_entry.DebugString(); } } // namespace absl::StatusOr EvaluateTable( - const ir::Dataplane &data_plane, const ir::Table &table, - const std::vector &entries, SymbolicPerPacketState *state, - values::P4RuntimeTranslator *translator, z3::context &z3_context, + 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 = - SortEntries(table, entries); + std::vector sorted_entries; + if (auto it = state.context.table_entries.find(table_name); + it != state.context.table_entries.end()) { + sorted_entries = SortEntries(table, it->second); + } + // The table semantically is just a bunch of if conditions, one per // table entry, we construct this big if-elseif-...-else symbolically. // @@ -423,17 +415,17 @@ absl::StatusOr EvaluateTable( // Find all entries match conditions. std::vector entries_matches; - for (const auto &[_, entry] : sorted_entries) { - if (!entry.has_concrete_entry()) { + 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.concrete_entry(), - *state, translator, z3_context)); + ASSIGN_OR_RETURN(z3::expr entry_match, + EvaluateTableEntryCondition( + table, entry.GetPdpiIrTableEntry(), state, *headers)); entries_matches.push_back(entry_match); } @@ -462,30 +454,31 @@ absl::StatusOr EvaluateTable( } // Build a TableEntry object for the default entry. - ir::TableEntry default_entry; - default_entry.mutable_concrete_entry()->mutable_action()->set_name( + ir::TableEntry ir_default_entry; + ir_default_entry.mutable_concrete_entry()->mutable_action()->set_name( table.table_implementation().default_action()); for (const std::string ¶meter_value : table.table_implementation().default_action_parameters()) { - ASSIGN_OR_RETURN(*(default_entry.mutable_concrete_entry() + ASSIGN_OR_RETURN(*(ir_default_entry.mutable_concrete_entry() ->mutable_action() ->add_params() ->mutable_value()), values::ParseIrValue(parameter_value)); } + TableEntry default_entry(kDefaultActionEntryIndex, + std::move(ir_default_entry)); // Start with the default entry - z3::expr match_index = z3_context.int_val(kDefaultActionEntryIndex); - RETURN_IF_ERROR(EvaluateTableEntryAction( - table, default_entry.concrete_entry(), kDefaultActionEntryIndex, - data_plane.program.actions(), state, translator, z3_context, - default_entry_assignment_guard)); + 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)); // Continue evaluating each table entry in reverse priority for (int row = sorted_entries.size() - 1; row >= 0; row--) { - int old_index = sorted_entries.at(row).first; - const ir::TableEntry &entry = sorted_entries.at(row).second; - z3::expr row_symbol = z3_context.int_val(old_index); + const TableEntry &entry = sorted_entries.at(row); + z3::expr row_symbol = state.context.z3_context->int_val(entry.GetIndex()); // The condition used in the big if_else_then construct. ASSIGN_OR_RETURN(z3::expr entry_match, @@ -495,9 +488,9 @@ 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.concrete_entry(), old_index, data_plane.program.actions(), - state, translator, z3_context, entry_assignment_guard)); + RETURN_IF_ERROR(EvaluateTableEntryAction(table, entry, + state.program.actions(), state, + headers, entry_assignment_guard)); } const std::string &merge_point = table.table_implementation() @@ -523,12 +516,12 @@ absl::StatusOr EvaluateTable( ? (match_index != kDefaultActionEntryIndex) : (match_index == kDefaultActionEntryIndex); ASSIGN_OR_RETURN(SymbolicTableMatches branch_matches, - control::EvaluateControl(data_plane, next_control, - state, translator, z3_context, + control::EvaluateControl(next_control, state, headers, guard && branch_condition)); - ASSIGN_OR_RETURN(merged_matches, util::MergeMatchesOnCondition( - branch_condition, branch_matches, - merged_matches, z3_context)); + ASSIGN_OR_RETURN(merged_matches, + util::MergeMatchesOnCondition( + branch_condition, branch_matches, merged_matches, + *state.context.z3_context)); } else { return absl::UnimplementedError( absl::Substitute("Conditional on executed table action is not " @@ -545,9 +538,9 @@ absl::StatusOr EvaluateTable( : ir::EndOfPipeline(); // Evaluate the next control. - ASSIGN_OR_RETURN(SymbolicTableMatches result, - control::EvaluateControl(data_plane, continuation, state, - translator, z3_context, guard)); + ASSIGN_OR_RETURN( + SymbolicTableMatches result, + control::EvaluateControl(continuation, state, headers, guard)); // Merge the result of execution from the merge point with the result of // execution from action_to_next_control (up to the merge point). ASSIGN_OR_RETURN(result, diff --git a/p4_symbolic/symbolic/table.h b/p4_symbolic/symbolic/table.h index f7916c62..2f9ee2b1 100644 --- a/p4_symbolic/symbolic/table.h +++ b/p4_symbolic/symbolic/table.h @@ -21,13 +21,10 @@ #ifndef P4_SYMBOLIC_SYMBOLIC_TABLE_H_ #define P4_SYMBOLIC_SYMBOLIC_TABLE_H_ -#include - #include "absl/status/statusor.h" -#include "p4_symbolic/ir/ir.h" #include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/symbolic/context.h" -#include "p4_symbolic/symbolic/values.h" +#include "p4_symbolic/symbolic/symbolic.h" #include "z3++.h" namespace p4_symbolic { @@ -38,9 +35,7 @@ namespace table { constexpr int kDefaultActionEntryIndex = -1; absl::StatusOr EvaluateTable( - const ir::Dataplane &data_plane, const ir::Table &table, - const std::vector &entries, SymbolicPerPacketState *state, - values::P4RuntimeTranslator *translator, z3::context &z3_context, + const ir::Table &table, SolverState &state, SymbolicPerPacketState *headers, const z3::expr &guard); } // namespace table diff --git a/p4_symbolic/symbolic/table_entry_test.cc b/p4_symbolic/symbolic/table_entry_test.cc new file mode 100644 index 00000000..cf14e18f --- /dev/null +++ b/p4_symbolic/symbolic/table_entry_test.cc @@ -0,0 +1,417 @@ +// Copyright 2023 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#include "p4_symbolic/symbolic/table_entry.h" + +#include +#include +#include +#include +#include + +#include "absl/status/status.h" +#include "absl/status/statusor.h" +#include "absl/strings/str_cat.h" +#include "absl/strings/string_view.h" +#include "gmock/gmock.h" +#include "google/protobuf/util/message_differencer.h" +#include "gtest/gtest.h" +#include "gutil/status.h" +#include "gutil/status_matchers.h" +#include "p4/config/v1/p4info.pb.h" +#include "p4/v1/p4runtime.pb.h" +#include "p4_pdpi/ir.pb.h" +#include "p4_symbolic/ir/ir.h" +#include "p4_symbolic/ir/ir.pb.h" +#include "p4_symbolic/ir/parser.h" +#include "p4_symbolic/ir/table_entries.h" +#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/test_util.h" +#include "z3++.h" + +namespace p4_symbolic::symbolic { +namespace { + +using MatchType = p4::config::v1::MatchField::MatchType; +using gutil::StatusIs; + +// P4 source: p4_symbolic/testdata/ipv4-routing/basic.p4 +// Table "MyIngress.ipv4_lpm" has exactly one LPM match. +class IPv4RoutingTableEntriesTest : public testing::Test { + public: + void SetUp() override { + constexpr absl::string_view bmv2_json_path = + "p4_symbolic/testdata/ipv4-routing/" + "basic.config.json"; + constexpr absl::string_view p4info_path = + "p4_symbolic/testdata/ipv4-routing/" + "basic.p4info.pb.txt"; + constexpr absl::string_view entries_path = + "p4_symbolic/testdata/ipv4-routing/" + "entries.pb.txt"; + ASSERT_OK_AND_ASSIGN( + p4::v1::ForwardingPipelineConfig config, + ParseToForwardingPipelineConfig(bmv2_json_path, p4info_path)); + ASSERT_OK_AND_ASSIGN( + std::vector pi_entries, + GetPiTableEntriesFromPiUpdatesProtoTextFile(entries_path)); + ASSERT_OK_AND_ASSIGN(ir::Dataplane dataplane, + ir::ParseToIr(config, pi_entries)); + state_ = std::make_unique(dataplane.program); + ir_entries_ = std::move(dataplane.entries); + } + + absl::StatusOr CreateSymbolicEntry(int entry_index, + int prefix_length) const { + // The P4 program should have exactly one table. + if (state_->program.tables_size() != 1) { + return gutil::InternalErrorBuilder() + << "The program must have exactly 1 table. Found " + << state_->program.tables_size() << " tables."; + } + + const std::string &table_name = state_->program.tables().begin()->first; + const ir::Table &table = state_->program.tables().begin()->second; + + // The table should have exactly one LPM match. + if (table.table_definition().match_fields_by_name_size() != 1) { + return gutil::InternalErrorBuilder() + << "The table '" << table_name + << "' must have exactly 1 match. Found: " + << table.table_definition().DebugString(); + } + + const std::string &match_name = + table.table_definition().match_fields_by_name().begin()->first; + const p4::config::v1::MatchField &pi_match = table.table_definition() + .match_fields_by_name() + .begin() + ->second.match_field(); + + // The match should be an LPM match. + if (pi_match.match_type() != MatchType::MatchField_MatchType_LPM) { + return gutil::InternalErrorBuilder() + << "The match '" << match_name + << "' must be an LPM match. Found: " << pi_match.DebugString(); + } + + // Construct the symbolic table entry in P4-Symbolic IR. + ir::TableEntry ir_entry; + pdpi::IrTableEntry &sketch = + *ir_entry.mutable_symbolic_entry()->mutable_sketch(); + sketch.set_table_name(table_name); + pdpi::IrMatch &ir_match = *sketch.add_matches(); + ir_match.set_name(match_name); + ir_match.mutable_lpm()->set_prefix_length(prefix_length); + sketch.set_priority(0); + + // Build and return the symbolic table entry object. + return TableEntry(entry_index, ir_entry); + } + + protected: + std::unique_ptr state_; + ir::TableEntries ir_entries_; +}; + +TEST_F(IPv4RoutingTableEntriesTest, SymbolicEntryWithGetterFunctions) { + constexpr int entry_index = 0; + constexpr int prefix_length = 16; + + // Construct a symbolic table entry. + ASSERT_OK_AND_ASSIGN(TableEntry entry, + CreateSymbolicEntry(entry_index, prefix_length)); + + // Test all basic getter functions. + EXPECT_EQ(entry.GetIndex(), entry_index); + EXPECT_FALSE(entry.IsConcrete()); + EXPECT_TRUE(entry.IsSymbolic()); + EXPECT_EQ(entry.GetTableName(), "MyIngress.ipv4_lpm"); + EXPECT_TRUE(google::protobuf::util::MessageDifferencer::Equals( + entry.GetP4SymbolicIrTableEntry().symbolic_entry().sketch(), + entry.GetPdpiIrTableEntry())); + EXPECT_EQ(entry.GetPdpiIrTableEntry().matches_size(), 1); + EXPECT_TRUE(entry.GetPdpiIrTableEntry().matches(0).has_lpm()); + EXPECT_EQ(entry.GetPdpiIrTableEntry().matches(0).lpm().prefix_length(), + prefix_length); +} + +TEST_F(IPv4RoutingTableEntriesTest, MatchVariablesOfSymbolicEntry) { + constexpr int entry_index = 0; + constexpr int prefix_length = 16; + + // Construct a symbolic table entry. + ASSERT_OK_AND_ASSIGN(TableEntry entry, + CreateSymbolicEntry(entry_index, prefix_length)); + + // Test the symbolic variables of the symbolic LPM match. + ASSERT_EQ(state_->program.tables_size(), 1); + const ir::Table &table = state_->program.tables().begin()->second; + const std::string &match_name = entry.GetPdpiIrTableEntry().matches(0).name(); + int bitwidth = table.table_definition() + .match_fields_by_name() + .begin() + ->second.match_field() + .bitwidth(); + constexpr absl::string_view variable_prefix = + "MyIngress.ipv4_lpm_entry_0_hdr.ipv4.dstAddr_lpm_"; + ASSERT_OK_AND_ASSIGN(SymbolicMatchVariables match_variables, + entry.GetMatchValues(match_name, table, state_->program, + *state_->context.z3_context)); + EXPECT_EQ(match_variables.match_type, MatchType::MatchField_MatchType_LPM); + z3::expr expected_value_expr = state_->context.z3_context->bv_const( + absl::StrCat(variable_prefix, "value").c_str(), bitwidth); + z3::expr expected_mask_expr = state_->context.z3_context->bv_const( + absl::StrCat(variable_prefix, "mask").c_str(), bitwidth); + EXPECT_TRUE(z3::eq(match_variables.value, expected_value_expr)); + EXPECT_TRUE(z3::eq(match_variables.mask, expected_mask_expr)); +} + +TEST_F(IPv4RoutingTableEntriesTest, ActionInvocationVariablesOfSymbolicEntry) { + constexpr int entry_index = 0; + constexpr int prefix_length = 16; + + // Construct a symbolic table entry. + ASSERT_OK_AND_ASSIGN(TableEntry entry, + CreateSymbolicEntry(entry_index, prefix_length)); + + // Test the symbolic variables of the symbolic action invocations. + ASSERT_EQ(state_->program.tables_size(), 1); + const ir::Table &table = state_->program.tables().begin()->second; + for (const auto &action_ref : table.table_definition().entry_actions()) { + const std::string &action_name = action_ref.action().preamble().name(); + ASSERT_OK_AND_ASSIGN(z3::expr action_invocation, + entry.GetActionInvocation( + action_name, table, *state_->context.z3_context)); + z3::expr expected_action_invocation = + state_->context.z3_context->bool_const( + absl::StrCat("MyIngress.ipv4_lpm_entry_0_", action_name, + "_$chosen$") + .c_str()); + EXPECT_TRUE(z3::eq(action_invocation, expected_action_invocation)); + } +} + +TEST_F(IPv4RoutingTableEntriesTest, ActionParameterVariablesOfSymbolicEntry) { + constexpr int entry_index = 0; + constexpr int prefix_length = 16; + + // Construct a symbolic table entry. + ASSERT_OK_AND_ASSIGN(TableEntry entry, + CreateSymbolicEntry(entry_index, prefix_length)); + + // Test the symbolic variables of the symbolic action parameters. + ASSERT_EQ(state_->program.tables_size(), 1); + const ir::Table &table = state_->program.tables().begin()->second; + for (const auto &action_ref : table.table_definition().entry_actions()) { + const std::string &action_name = action_ref.action().preamble().name(); + ASSERT_TRUE(state_->program.actions().contains(action_name)); + const ir::Action &action = state_->program.actions().at(action_name); + + for (const auto &[param_name, param_definition] : + action_ref.action().params_by_name()) { + ASSERT_OK_AND_ASSIGN(z3::expr param, entry.GetActionParameter( + param_name, action, table, + *state_->context.z3_context)); + z3::expr expected_param = state_->context.z3_context->bv_const( + absl::StrCat("MyIngress.ipv4_lpm_entry_0_", action_name, "_", + param_name) + .c_str(), + param_definition.param().bitwidth()); + EXPECT_TRUE(z3::eq(param, expected_param)); + } + } +} + +TEST_F(IPv4RoutingTableEntriesTest, ErrorWithNonExistentMatch) { + constexpr int entry_index = 0; + constexpr int prefix_length = 16; + + // Construct a symbolic table entry. + ASSERT_OK_AND_ASSIGN(TableEntry entry, + CreateSymbolicEntry(entry_index, prefix_length)); + + // Test getting the symbolic variables of a non-existent match. + ASSERT_EQ(state_->program.tables_size(), 1); + const ir::Table &table = state_->program.tables().begin()->second; + constexpr absl::string_view non_existent_match_name = "non_existent_match"; + EXPECT_THAT( + entry.GetMatchValues(non_existent_match_name, table, state_->program, + *state_->context.z3_context), + StatusIs(absl::StatusCode::kNotFound, + "Match 'non_existent_match' not found in table " + "'MyIngress.ipv4_lpm'")); +} + +TEST_F(IPv4RoutingTableEntriesTest, ErrorWithWildcardMatch) { + constexpr int entry_index = 0; + constexpr int prefix_length = 16; + + // Construct a symbolic table entry with all wildcard matches. + ASSERT_OK_AND_ASSIGN(TableEntry non_wildcard_entry, + CreateSymbolicEntry(entry_index, prefix_length)); + ir::TableEntry ir_entry = non_wildcard_entry.GetP4SymbolicIrTableEntry(); + ir_entry.mutable_symbolic_entry()->mutable_sketch()->clear_matches(); + TableEntry entry(entry_index, ir_entry); + + // Test getting the symbolic variables of an all-wildcard symbolic entry. + ASSERT_EQ(state_->program.tables_size(), 1); + const ir::Table &table = state_->program.tables().begin()->second; + constexpr absl::string_view match_name = "hdr.ipv4.dstAddr"; + EXPECT_THAT( + entry.GetMatchValues(match_name, table, state_->program, + *state_->context.z3_context), + StatusIs(absl::StatusCode::kInvalidArgument, + testing::StartsWith(absl::StrCat( + "Match '", match_name, "' is an explicit wildcard.")))); +} + +TEST_F(IPv4RoutingTableEntriesTest, ErrorWithNonExistentAction) { + constexpr int entry_index = 0; + constexpr int prefix_length = 16; + + // Construct a symbolic table entry. + ASSERT_OK_AND_ASSIGN(TableEntry entry, + CreateSymbolicEntry(entry_index, prefix_length)); + + // Test getting the symbolic variables of a non-existent action. + ASSERT_EQ(state_->program.tables_size(), 1); + const ir::Table &table = state_->program.tables().begin()->second; + constexpr absl::string_view non_existent_action_name = "non_existent_action"; + EXPECT_THAT(entry.GetActionInvocation(non_existent_action_name, table, + *state_->context.z3_context), + StatusIs(absl::StatusCode::kNotFound, + "Action 'non_existent_action' not found in table " + "'MyIngress.ipv4_lpm'")); + + constexpr absl::string_view param_name = "dstAddr"; + const std::string &valid_action_name = table.table_definition() + .entry_actions() + .begin() + ->action() + .preamble() + .name(); + ASSERT_TRUE(state_->program.actions().contains(valid_action_name)); + const ir::Action &valid_action = + state_->program.actions().at(valid_action_name); + ir::Action non_existent_action = valid_action; + non_existent_action.mutable_action_definition()->mutable_preamble()->set_name( + non_existent_action_name); + EXPECT_THAT(entry.GetActionParameter(param_name, non_existent_action, table, + *state_->context.z3_context), + StatusIs(absl::StatusCode::kNotFound, + "Action 'non_existent_action' not found in table " + "'MyIngress.ipv4_lpm'")); +} + +TEST_F(IPv4RoutingTableEntriesTest, ErrorWithNonExistentActionParameter) { + constexpr int entry_index = 0; + constexpr int prefix_length = 16; + + // Construct a symbolic table entry. + ASSERT_OK_AND_ASSIGN(TableEntry entry, + CreateSymbolicEntry(entry_index, prefix_length)); + + // Test getting the symbolic variables of a non-existent action parameter. + ASSERT_EQ(state_->program.tables_size(), 1); + const ir::Table &table = state_->program.tables().begin()->second; + constexpr absl::string_view non_existent_param_name = "non_existent_param"; + for (const auto &action_ref : table.table_definition().entry_actions()) { + const std::string &action_name = action_ref.action().preamble().name(); + ASSERT_TRUE(state_->program.actions().contains(action_name)); + const ir::Action &action = state_->program.actions().at(action_name); + EXPECT_THAT( + entry.GetActionParameter(non_existent_param_name, action, table, + *state_->context.z3_context), + StatusIs(absl::StatusCode::kNotFound, + absl::StrCat("Action parameter 'non_existent_param' not found " + "in implementation of action '", + action_name, "'"))); + } +} + +TEST_F(IPv4RoutingTableEntriesTest, ConcreteEntriesWithGetterFunctions) { + for (const auto &[table_name, per_table_ir_entries] : ir_entries_) { + for (size_t index = 0; index < per_table_ir_entries.size(); ++index) { + // For each concrete IR entry, create a table entry object. + const ir::TableEntry &ir_entry = per_table_ir_entries[index]; + TableEntry entry(index, ir_entry); + + // Test all basic getter functions. + EXPECT_EQ(entry.GetIndex(), index); + EXPECT_TRUE(entry.IsConcrete()); + EXPECT_FALSE(entry.IsSymbolic()); + EXPECT_EQ(entry.GetTableName(), table_name); + EXPECT_EQ(entry.GetTableName(), "MyIngress.ipv4_lpm"); + EXPECT_TRUE(google::protobuf::util::MessageDifferencer::Equals( + entry.GetP4SymbolicIrTableEntry().concrete_entry(), + entry.GetPdpiIrTableEntry())); + EXPECT_TRUE(google::protobuf::util::MessageDifferencer::Equals( + entry.GetP4SymbolicIrTableEntry(), ir_entry)); + EXPECT_EQ(entry.GetPdpiIrTableEntry().matches_size(), 1); + EXPECT_TRUE(entry.GetPdpiIrTableEntry().matches(0).has_lpm()); + } + } +} + +TEST_F(IPv4RoutingTableEntriesTest, + ErrorGettingSymbolicVariablesWithConcreteEntries) { + for (const auto &[table_name, per_table_ir_entries] : ir_entries_) { + for (size_t index = 0; index < per_table_ir_entries.size(); ++index) { + // For each concrete IR entry, create a table entry object. + const ir::TableEntry &ir_entry = per_table_ir_entries[index]; + TableEntry entry(index, ir_entry); + + // Test getting the symbolic variables of a concrete entry. + ASSERT_EQ(state_->program.tables_size(), 1); + const ir::Table &table = state_->program.tables().begin()->second; + ASSERT_EQ(entry.GetPdpiIrTableEntry().matches_size(), 1); + const std::string &match_name = + entry.GetPdpiIrTableEntry().matches(0).name(); + ASSERT_TRUE(entry.GetPdpiIrTableEntry().has_action()); + const std::string &action_name = + entry.GetPdpiIrTableEntry().action().name(); + ASSERT_TRUE(state_->program.actions().contains(action_name)); + const ir::Action &action = state_->program.actions().at(action_name); + + EXPECT_THAT( + entry.GetMatchValues(match_name, table, state_->program, + *state_->context.z3_context), + StatusIs( + absl::StatusCode::kInvalidArgument, + absl::StrCat("Entry ", index, + " of table 'MyIngress.ipv4_lpm' is not symbolic."))); + EXPECT_THAT( + entry.GetActionInvocation(action_name, table, + *state_->context.z3_context), + StatusIs( + absl::StatusCode::kInvalidArgument, + absl::StrCat("Entry ", index, + " of table 'MyIngress.ipv4_lpm' is not symbolic."))); + + for (const auto ¶m : entry.GetPdpiIrTableEntry().action().params()) { + EXPECT_THAT( + entry.GetActionParameter(param.name(), action, table, + *state_->context.z3_context), + StatusIs(absl::StatusCode::kInvalidArgument, + absl::StrCat( + "Entry ", index, + " of table 'MyIngress.ipv4_lpm' is not symbolic."))); + } + } + } +} + +} // namespace +} // namespace p4_symbolic::symbolic diff --git a/p4_symbolic/symbolic/v1model.cc b/p4_symbolic/symbolic/v1model.cc index 5f8d7b93..5bfe5efc 100644 --- a/p4_symbolic/symbolic/v1model.cc +++ b/p4_symbolic/symbolic/v1model.cc @@ -16,15 +16,20 @@ #include #include +#include #include #include "absl/status/status.h" +#include "absl/status/statusor.h" #include "absl/strings/str_format.h" +#include "absl/strings/string_view.h" #include "absl/strings/substitute.h" #include "gutil/status.h" #include "p4_pdpi/internal/ordered_map.h" #include "p4_symbolic/ir/ir.pb.h" +#include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/control.h" +#include "p4_symbolic/symbolic/guarded_map.h" #include "p4_symbolic/symbolic/operators.h" #include "p4_symbolic/symbolic/parser.h" #include "p4_symbolic/symbolic/symbolic.h" @@ -167,10 +172,10 @@ absl::Status InitializeIngressHeaders(const ir::P4Program &program, return absl::OkStatus(); } -absl::Status EvaluateV1model(const ir::Dataplane &data_plane, - const std::vector &physical_ports, - SymbolicContext &context, - values::P4RuntimeTranslator &translator) { +absl::Status EvaluateV1model(SolverState &state, + const std::vector &physical_ports) { + SymbolicContext &context = state.context; + // Check input physical ports. RETURN_IF_ERROR(CheckPhysicalPortsConformanceToV1Model(physical_ports)); @@ -179,10 +184,10 @@ absl::Status EvaluateV1model(const ir::Dataplane &data_plane, // variable for each header field. ASSIGN_OR_RETURN(context.ingress_headers, SymbolicGuardedMap::CreateSymbolicGuardedMap( - *context.z3_context, data_plane.program.headers())); + *context.z3_context, state.program.headers())); // Initialize the symbolic ingress packet before evaluation. RETURN_IF_ERROR(InitializeIngressHeaders( - data_plane.program, context.ingress_headers, *context.z3_context)); + state.program, context.ingress_headers, *context.z3_context)); // Evaluate all parsers in the P4 program. // If a parser error occurs, the `standard_metadata.parser_error` field will @@ -191,12 +196,12 @@ absl::Status EvaluateV1model(const ir::Dataplane &data_plane, // will only yield 2 kinds of parser error, NoError and NoMatch. ASSIGN_OR_RETURN( context.parsed_headers, - parser::EvaluateParsers(data_plane.program, context.ingress_headers, + parser::EvaluateParsers(state.program, context.ingress_headers, *context.z3_context)); // Update the ingress_headers' valid fields to be parsed_headers' extracted // fields. - for (const auto &[header_name, _] : Ordered(data_plane.program.headers())) { + for (const auto &[header_name, _] : Ordered(state.program.headers())) { ASSIGN_OR_RETURN( z3::expr extracted, context.parsed_headers.Get(header_name, kExtractedPseudoField)); @@ -216,8 +221,7 @@ absl::Status EvaluateV1model(const ir::Dataplane &data_plane, // 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(data_plane, "ingress", &context.egress_headers, - &translator, *context.z3_context, + 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)); @@ -233,8 +237,7 @@ absl::Status EvaluateV1model(const ir::Dataplane &data_plane, // Evaluate the egress pipeline. ASSIGN_OR_RETURN( SymbolicTableMatches egress_matches, - control::EvaluatePipeline(data_plane, "egress", &context.egress_headers, - &translator, *context.z3_context, + control::EvaluatePipeline("egress", state, &context.egress_headers, /*guard=*/!dropped)); matches.merge(std::move(egress_matches)); diff --git a/p4_symbolic/symbolic/v1model.h b/p4_symbolic/symbolic/v1model.h index f0849526..341adf75 100644 --- a/p4_symbolic/symbolic/v1model.h +++ b/p4_symbolic/symbolic/v1model.h @@ -17,9 +17,11 @@ #include -#include "p4_symbolic/ir/ir.h" +#include "absl/status/status.h" +#include "absl/strings/string_view.h" +#include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/symbolic/context.h" -#include "p4_symbolic/symbolic/values.h" +#include "p4_symbolic/symbolic/symbolic.h" #include "z3++.h" namespace p4_symbolic { @@ -52,10 +54,8 @@ absl::Status InitializeIngressHeaders(const ir::P4Program &program, // Symbolically evaluates the parser, ingress, and egress pipelines of the given // P4 program with the given entries, assuming the program is written against V1 // model. -absl::Status EvaluateV1model(const ir::Dataplane &data_plane, - const std::vector &physical_ports, - SymbolicContext &context, - values::P4RuntimeTranslator &translator); +absl::Status EvaluateV1model(SolverState &state, + const std::vector &physical_ports); } // namespace v1model } // namespace symbolic diff --git a/p4_symbolic/symbolic/values.cc b/p4_symbolic/symbolic/values.cc index b41af2f9..50063172 100644 --- a/p4_symbolic/symbolic/values.cc +++ b/p4_symbolic/symbolic/values.cc @@ -20,12 +20,11 @@ #include "p4_symbolic/symbolic/values.h" -#include -#include -#include -#include +#include +#include #include "absl/status/status.h" +#include "absl/status/statusor.h" #include "absl/strings/match.h" #include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" @@ -44,6 +43,7 @@ #include "p4_symbolic/symbolic/operators.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/z3_util.h" +#include "z3++.h" namespace p4_symbolic { namespace symbolic { @@ -75,18 +75,17 @@ absl::StatusOr ParseIrValue(const std::string &value) { } } -absl::StatusOr FormatP4RTValue(z3::context &context, - const std::string &field_name, +absl::StatusOr FormatP4RTValue(const std::string &field_name, const std::string &type_name, const pdpi::IrValue &value, - int bitwidth, - P4RuntimeTranslator *translator) { + int bitwidth, z3::context &context, + P4RuntimeTranslator &translator) { switch (value.format_case()) { case pdpi::IrValue::kStr: { // Mark that this field is a string translatable field, and map it // to its custom type name (e.g. vrf_id => vrf_t). if (!field_name.empty()) { - translator->fields_p4runtime_type[field_name] = type_name; + translator.fields_p4runtime_type[field_name] = type_name; } // Must translate the string into a bitvector according to the field type. @@ -94,13 +93,13 @@ absl::StatusOr FormatP4RTValue(z3::context &context, // If there is no IdAllocator for the given type (implying no static // mapping was provided), create a new dynamic IdAllocator. - translator->p4runtime_translation_allocators.try_emplace( + translator.p4runtime_translation_allocators.try_emplace( type_name, IdAllocator(TranslationData{ .static_mapping = {}, .dynamic_translation = true, })); IdAllocator &allocator = - translator->p4runtime_translation_allocators.at(type_name); + translator.p4runtime_translation_allocators.at(type_name); ASSIGN_OR_RETURN(uint64_t int_value, allocator.AllocateId(string_value)); if (bitwidth == 0) { @@ -114,7 +113,7 @@ absl::StatusOr FormatP4RTValue(z3::context &context, return context.bv_val(int_value, bitwidth); } default: { - if (translator->fields_p4runtime_type.count(field_name)) { + if (translator.fields_p4runtime_type.count(field_name)) { return absl::InvalidArgumentError(absl::StrCat( "A table entry provides a non-string value ", value.DebugString(), "to a string translated field", field_name)); diff --git a/p4_symbolic/symbolic/values.h b/p4_symbolic/symbolic/values.h index 26e8629a..92f37549 100644 --- a/p4_symbolic/symbolic/values.h +++ b/p4_symbolic/symbolic/values.h @@ -114,10 +114,11 @@ absl::StatusOr ParseIrValue(const std::string &value); // translated values (i.e. string IrValues) the bitwidth MUST be 0, in which // case we use the minimum number of bits to encode the resulting translated // value. -absl::StatusOr -FormatP4RTValue(z3::context &context, const std::string &field_name, - const std::string &type_name, const pdpi::IrValue &value, - int bitwidth, P4RuntimeTranslator *translator); +absl::StatusOr FormatP4RTValue(const std::string &field_name, + const std::string &type_name, + const pdpi::IrValue &value, + int bitwidth, z3::context &context, + P4RuntimeTranslator &translator); // Reverse translation: operates opposite to FormatP4RTValue(). // If the given field was not detected to be translatable (perhaps it is indeed diff --git a/p4_symbolic/symbolic/values_test.cc b/p4_symbolic/symbolic/values_test.cc index 4fc95c71..4b1c9eeb 100644 --- a/p4_symbolic/symbolic/values_test.cc +++ b/p4_symbolic/symbolic/values_test.cc @@ -1,12 +1,16 @@ #include "p4_symbolic/symbolic/values.h" +#include +#include + #include "absl/container/flat_hash_map.h" +#include "absl/status/status.h" #include "absl/strings/str_cat.h" #include "absl/strings/string_view.h" #include "gmock/gmock.h" #include "gtest/gtest.h" +#include "gutil/proto.h" #include "gutil/status_matchers.h" -#include "gutil/testing.h" #include "p4_pdpi/ir.pb.h" #include "p4_symbolic/z3_util.h" #include "z3++.h" @@ -31,9 +35,8 @@ TEST(TranslateValueToP4RT, ReverseTranslatedValuesAreEqualToTheOriginalOnes) { pdpi::IrValue ir_value; ir_value.set_str(id); ASSERT_OK_AND_ASSIGN( - z3::expr expr, - FormatP4RTValue(z3_context, kFieldName, kFieldType, ir_value, - /*bitwidth=*/0, &translator)); + z3::expr expr, FormatP4RTValue(kFieldName, kFieldType, ir_value, + /*bitwidth=*/0, z3_context, translator)); z3_value_to_id[expr.to_string()] = id; } @@ -55,8 +58,8 @@ TEST(FormatP4RTValue, WorksFor64BitIPv6) { R"pb(ipv6: "0000:ffff:ffff:ffff::")pb")); ASSERT_OK_AND_ASSIGN( z3::expr z3_expr, - FormatP4RTValue(z3_context, kFieldName, kFieldType, ir_value, - /*bitwidth=*/64, &translator)); + FormatP4RTValue(kFieldName, kFieldType, ir_value, + /*bitwidth=*/64, z3_context, translator)); ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x0000'ffff'ffff'ffffULL); } @@ -67,8 +70,8 @@ TEST(FormatP4RTValue, WorksForIpv4) { R"pb(ipv4: "127.0.0.1")pb")); ASSERT_OK_AND_ASSIGN( z3::expr z3_expr, - FormatP4RTValue(z3_context, kFieldName, kFieldType, ir_value, - /*bitwidth=*/32, &translator)); + FormatP4RTValue(kFieldName, kFieldType, ir_value, + /*bitwidth=*/32, z3_context, translator)); ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x7f000001); } @@ -79,8 +82,8 @@ TEST(FormatP4RTValue, WorksForMac) { R"pb(mac: "01:02:03:04:05:06")pb")); ASSERT_OK_AND_ASSIGN( z3::expr z3_expr, - FormatP4RTValue(z3_context, kFieldName, kFieldType, ir_value, - /*bitwidth=*/48, &translator)); + FormatP4RTValue(kFieldName, kFieldType, ir_value, + /*bitwidth=*/48, z3_context, translator)); ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x01'02'03'04'05'06ULL); } @@ -91,8 +94,8 @@ TEST(FormatP4RTValue, WorksForHexString) { R"pb(hex_str: "0xabcd")pb")); ASSERT_OK_AND_ASSIGN( z3::expr z3_expr, - FormatP4RTValue(z3_context, kFieldName, kFieldType, ir_value, - /*bitwidth=*/16, &translator)); + FormatP4RTValue(kFieldName, kFieldType, ir_value, + /*bitwidth=*/16, z3_context, translator)); ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0xabcd); } @@ -101,8 +104,8 @@ TEST(FormatP4RTValue, FailsForStringWithNonZeroBitwidth) { z3::context z3_context; ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto( R"pb(str: "dummy_value")pb")); - ASSERT_THAT(FormatP4RTValue(z3_context, kFieldName, kFieldType, ir_value, - /*bitwidth=*/16, &translator), + ASSERT_THAT(FormatP4RTValue(kFieldName, kFieldType, ir_value, + /*bitwidth=*/16, z3_context, translator), StatusIs(absl::StatusCode::kInvalidArgument)); } diff --git a/p4_symbolic/tests/BUILD.bazel b/p4_symbolic/tests/BUILD.bazel index d83c2c24..72ed6659 100644 --- a/p4_symbolic/tests/BUILD.bazel +++ b/p4_symbolic/tests/BUILD.bazel @@ -18,9 +18,14 @@ cc_test( "//p4_symbolic/symbolic", "//sai_p4/instantiations/google:sai_nonstandard_platforms_cc", "//sai_p4/instantiations/google:sai_pd_cc_proto", - "//sai_p4/instantiations/google:instantiations", - "//thinkit:bazel_test_environment", + "//thinkit:bazel_test_environment", + "//thinkit:test_environment", + "@com_github_google_glog//:glog", "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", + "@com_github_z3prover_z3//:api", + "@com_google_absl//absl/memory", + "@com_google_absl//absl/status", + "@com_google_absl//absl/status:statusor", "@com_google_absl//absl/strings", "@com_google_absl//absl/time", "@com_google_absl//absl/types:optional",