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 4c32efab..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,8 +46,10 @@ cc_library( "parser.h", "symbolic.h", "table.h", + "table_entry.h", "util.h", "v1model.h", + "v1model_intrinsic.h", "values.h", ], deps = [ @@ -72,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", @@ -106,14 +111,6 @@ end_to_end_test( smt_golden_file = "expected/reflector.smt2", ) -end_to_end_test( - name = "ipv4_routing_test", - p4_program = "//p4_symbolic/testdata:ipv4-routing/basic.p4", - packets_golden_file = "expected/basic.txt", - smt_golden_file = "expected/basic.smt2", - table_entries = "//p4_symbolic/testdata:ipv4-routing/entries.pb.txt", -) - # Checks the behavior of symbolic execution when there is a table application after a conditional. # Before go/optimized-symbolic-execution, p4-symbolic was executing t3 twice (once from the if # branch and once from the else branch). Now it executed each table exactly once, leading to @@ -139,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", ], @@ -179,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/expected/basic.smt2 b/p4_symbolic/symbolic/expected/basic.smt2 index 90b94d3e..110c975b 100644 --- a/p4_symbolic/symbolic/expected/basic.smt2 +++ b/p4_symbolic/symbolic/expected/basic.smt2 @@ -23,22 +23,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) ethernet.$extracted$: (ite true true false) @@ -65,26 +65,26 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (let ((a!1 (and true (not (= (concat #x0 #x800) ethernet.etherType)) (not true))) (a!2 (ite (and true (= (concat #x0 #x800) ethernet.etherType) (not true)) #x00000002 #x00000000))) (ite a!1 #x00000002 a!2)) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) ethernet.$extracted$: (ite true true false) @@ -203,10 +203,10 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (ite (and true (= (concat #x0 #x800) ethernet.etherType)) true false)) (a!3 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) @@ -237,12 +237,12 @@ #b000000001 (ite (and (and true a!1) (and a!4 a!6) a!8) #b111111111 - standard_metadata.egress_spec)))) + #b000000000)))) (let ((a!10 (ite (and (and true a!1) (and true (= ipv4.dstAddr #x0a0a0000))) #b000000001 (ite a!2 #b000000000 (ite a!5 #b000000001 a!9))))) (ite (not (= a!10 #b111111111)) a!10 standard_metadata.egress_port)))))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (ite (and true (= (concat #x0 #x800) ethernet.etherType)) true false)) (a!3 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) @@ -273,55 +273,54 @@ #b000000001 (ite (and (and true a!1) (and a!4 a!6) a!8) #b111111111 - standard_metadata.egress_spec)))) + #b000000000)))) (ite (and (and true a!1) (and true (= ipv4.dstAddr #x0a0a0000))) #b000000001 (ite a!2 #b000000000 (ite a!5 #b000000001 a!9))))))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (let ((a!1 (and true (not (= (concat #x0 #x800) ethernet.etherType)) (not true))) (a!2 (ite (and true (= (concat #x0 #x800) ethernet.etherType) (not true)) #x00000002 #x00000000))) (ite a!1 #x00000002 a!2)) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun ethernet.etherType () (_ BitVec 16)) (assert - (let (($x137 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x137))) + (let (($x129 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x129))) (assert - (let (($x56 (= ipv4.dstAddr (_ bv168427520 32)))) - (let (($x57 (and true $x56))) - (let (($x72 (not $x57))) - (let (($x76 (and $x72 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))))))) - (let (($x80 (and $x76 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))))))) - (let (($x84 (and $x80 (not (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))))))) + (let (($x50 (= ipv4.dstAddr (_ bv168427520 32)))) + (let (($x51 (and true $x50))) + (let (($x66 (not $x51))) + (let (($x70 (and $x66 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))))))) + (let (($x74 (and $x70 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))))))) + (let (($x78 (and $x74 (not (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))))))) (let (($x11 (= (concat (_ bv0 4) (_ bv2048 12)) ethernet.etherType))) (let (($x10 (and true $x11))) - (let (($x48 (ite $x10 true false))) - (let (($x53 (and true $x48))) - (let (($x70 (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))))) - (let (($x82 (and (and $x53 $x80) $x70))) - (let ((?x94 (ite $x82 (_ bv1 9) (ite (and $x53 $x84) (_ bv511 9) standard_metadata.egress_spec)))) - (let (($x65 (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))))) - (let (($x78 (and (and $x53 $x76) $x65))) - (let (($x61 (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))))) - (let (($x74 (and (and $x53 $x72) $x61))) - (let (($x71 (and $x53 $x57))) - (let ((?x124 (ite $x71 (_ bv1 9) (ite $x74 (_ bv0 9) (ite $x78 (_ bv1 9) ?x94))))) - (let (($x140 (or (or false (= ?x124 (_ bv0 9))) (= ?x124 (_ bv1 9))))) - (let (($x45 (= ?x124 (_ bv511 9)))) - (or $x45 $x140))))))))))))))))))))))) + (let (($x38 (ite $x10 true false))) + (let (($x47 (and true $x38))) + (let (($x64 (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))))) + (let (($x76 (and (and $x47 $x74) $x64))) + (let (($x59 (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))))) + (let (($x72 (and (and $x47 $x70) $x59))) + (let (($x55 (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))))) + (let (($x68 (and (and $x47 $x66) $x55))) + (let ((?x108 (ite $x68 (_ bv0 9) (ite $x72 (_ bv1 9) (ite $x76 (_ bv1 9) (ite (and $x47 $x78) (_ bv511 9) (_ bv0 9))))))) + (let (($x65 (and $x47 $x51))) + (let ((?x116 (ite $x65 (_ bv1 9) ?x108))) + (let (($x132 (or (or false (= ?x116 (_ bv0 9))) (= ?x116 (_ bv1 9))))) + (let (($x44 (= ?x116 (_ bv511 9)))) + (or $x44 $x132))))))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/basic.txt b/p4_symbolic/symbolic/expected/basic.txt index d265e27e..27d6f6ba 100644 --- a/p4_symbolic/symbolic/expected/basic.txt +++ b/p4_symbolic/symbolic/expected/basic.txt @@ -7,7 +7,7 @@ ________________________________________________________________________________ ================================================================================ Finding packet for table MyIngress.ipv4_lpm and row 0 ================================================================================ -ingress_port = #b000000000 +ingress_port = #b000000001 egress_port = #b000000000 trace: dropped = 0 @@ -50,7 +50,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -93,7 +93,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -136,7 +136,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -147,7 +147,7 @@ ________________________________________________________________________________ ================================================================================ Finding packet for table MyIngress.ipv4_lpm and row 1 ================================================================================ -ingress_port = #b000000000 +ingress_port = #b000000001 egress_port = #b000000001 trace: dropped = 0 @@ -190,7 +190,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -233,7 +233,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -276,7 +276,7 @@ standard_metadata.egress_spec = #b000000001 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -287,7 +287,7 @@ ________________________________________________________________________________ ================================================================================ Finding packet for table MyIngress.ipv4_lpm and row 2 ================================================================================ -ingress_port = #b000000000 +ingress_port = #b000000001 egress_port = #b000000001 trace: dropped = 0 @@ -330,7 +330,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -373,7 +373,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -416,7 +416,7 @@ standard_metadata.egress_spec = #b000000001 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -427,7 +427,7 @@ ________________________________________________________________________________ ================================================================================ Finding packet for table MyIngress.ipv4_lpm and row 3 ================================================================================ -ingress_port = #b000000000 +ingress_port = #b000000001 egress_port = #b000000001 trace: dropped = 0 @@ -470,7 +470,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -513,7 +513,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -556,7 +556,7 @@ standard_metadata.egress_spec = #b000000001 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000000001 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 diff --git a/p4_symbolic/symbolic/expected/conditional.smt2 b/p4_symbolic/symbolic/expected/conditional.smt2 index fbd2ecf9..91689af0 100644 --- a/p4_symbolic/symbolic/expected/conditional.smt2 +++ b/p4_symbolic/symbolic/expected/conditional.smt2 @@ -9,22 +9,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) ethernet.$extracted$: (ite true true false) @@ -37,22 +37,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) ethernet.$extracted$: (ite true true false) @@ -67,57 +67,56 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (and true (not (and true (= ethernet.dst_addr #x000000000001))))) (a!2 (and true (not (= standard_metadata.ingress_port (concat #x00 #b0))))) (a!3 (ite (and true (= standard_metadata.ingress_port (concat #x00 #b0))) #b111111111 - standard_metadata.egress_spec))) + #b000000000))) (let ((a!4 (ite (and true (and true (= ethernet.dst_addr #x000000000001))) #b000000001 (ite a!1 #b111111111 (ite a!2 #b111111111 a!3))))) (ite (not (= a!4 #b111111111)) a!4 standard_metadata.egress_port))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (and true (= ethernet.dst_addr #x000000000001))))) (a!2 (and true (not (= standard_metadata.ingress_port (concat #x00 #b0))))) (a!3 (ite (and true (= standard_metadata.ingress_port (concat #x00 #b0))) #b111111111 - standard_metadata.egress_spec))) + #b000000000))) (ite (and true (and true (= ethernet.dst_addr #x000000000001))) #b000000001 (ite a!1 #b111111111 (ite a!2 #b111111111 a!3)))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun ethernet.dst_addr () (_ BitVec 48)) (assert - (let (($x64 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x64))) + (let (($x56 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x56))) (assert - (let (($x33 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))) - (let (($x35 (and true $x33))) - (let (($x36 (and true (not $x33)))) - (let ((?x49 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x36 (_ bv511 9) (ite $x35 (_ bv511 9) standard_metadata.egress_spec))))) - (let (($x44 (= ethernet.dst_addr (_ bv1 48)))) - (let (($x45 (and true $x44))) - (let (($x46 (and true $x45))) - (let ((?x54 (ite $x46 (_ bv1 9) ?x49))) - (let (($x67 (or (or false (= ?x54 (_ bv0 9))) (= ?x54 (_ bv1 9))))) - (let (($x56 (= ?x54 (_ bv511 9)))) - (or $x56 $x67)))))))))))) + (let (($x12 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1))))) + (let (($x24 (and true $x12))) + (let (($x17 (and true (not $x12)))) + (let ((?x42 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x17 (_ bv511 9) (ite $x24 (_ bv511 9) (_ bv0 9)))))) + (let (($x37 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x38 (and true $x37))) + (let (($x39 (and true $x38))) + (let ((?x47 (ite $x39 (_ bv1 9) ?x42))) + (let (($x59 (or (or false (= ?x47 (_ bv0 9))) (= ?x47 (_ bv1 9))))) + (let (($x49 (= ?x47 (_ bv511 9)))) + (or $x49 $x59)))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 b/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 index 14bdd98e..e2060054 100644 --- a/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 +++ b/p4_symbolic/symbolic/expected/conditional_nonlattice.smt2 @@ -9,22 +9,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) ethernet.$extracted$: (ite true true false) @@ -37,22 +37,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) ethernet.$extracted$: (ite true true false) @@ -67,10 +67,10 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (and true (not (and true (= ethernet.dst_addr #x000000000001))))) (a!2 (and true (not (bvugt standard_metadata.ingress_port (concat #b00000 #xa))))) @@ -87,14 +87,12 @@ (bvugt standard_metadata.ingress_port (concat #b000000 #b101))) #b111111111 - (ite a!4 - #b111111111 - (ite a!5 #b111111111 standard_metadata.egress_spec))))) + (ite a!4 #b111111111 (ite a!5 #b111111111 #b000000000))))) (let ((a!7 (ite (and true (and true (= ethernet.dst_addr #x000000000001))) #b000000001 (ite a!1 #b111111111 (ite a!3 #b111111111 a!6))))) (ite (not (= a!7 #b111111111)) a!7 standard_metadata.egress_port)))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (and true (= ethernet.dst_addr #x000000000001))))) (a!2 (and true (not (bvugt standard_metadata.ingress_port (concat #b00000 #xa))))) @@ -111,73 +109,69 @@ (bvugt standard_metadata.ingress_port (concat #b000000 #b101))) #b111111111 - (ite a!4 - #b111111111 - (ite a!5 #b111111111 standard_metadata.egress_spec))))) + (ite a!4 #b111111111 (ite a!5 #b111111111 #b000000000))))) (ite (and true (and true (= ethernet.dst_addr #x000000000001))) #b000000001 (ite a!1 #b111111111 (ite a!3 #b111111111 a!6))))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun ethernet.dst_addr () (_ BitVec 48)) (assert - (let (($x173 (= standard_metadata.ingress_port (_ bv19 9)))) - (let (($x168 (= standard_metadata.ingress_port (_ bv18 9)))) - (let (($x163 (= standard_metadata.ingress_port (_ bv17 9)))) - (let (($x158 (= standard_metadata.ingress_port (_ bv16 9)))) - (let (($x153 (= standard_metadata.ingress_port (_ bv15 9)))) - (let (($x148 (= standard_metadata.ingress_port (_ bv14 9)))) - (let (($x143 (= standard_metadata.ingress_port (_ bv13 9)))) - (let (($x138 (= standard_metadata.ingress_port (_ bv12 9)))) - (let (($x133 (= standard_metadata.ingress_port (_ bv11 9)))) - (let (($x128 (= standard_metadata.ingress_port (_ bv10 9)))) - (let (($x123 (= standard_metadata.ingress_port (_ bv9 9)))) - (let (($x118 (= standard_metadata.ingress_port (_ bv8 9)))) - (let (($x113 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x108 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x103 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x98 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x93 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x88 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x83 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x89 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x83) $x88))) - (let (($x124 (or (or (or (or (or (or (or $x89 $x93) $x98) $x103) $x108) $x113) $x118) $x123))) - (let (($x159 (or (or (or (or (or (or (or $x124 $x128) $x133) $x138) $x143) $x148) $x153) $x158))) - (or (or (or $x159 $x163) $x168) $x173)))))))))))))))))))))))) + (let (($x166 (= standard_metadata.ingress_port (_ bv19 9)))) + (let (($x161 (= standard_metadata.ingress_port (_ bv18 9)))) + (let (($x156 (= standard_metadata.ingress_port (_ bv17 9)))) + (let (($x151 (= standard_metadata.ingress_port (_ bv16 9)))) + (let (($x146 (= standard_metadata.ingress_port (_ bv15 9)))) + (let (($x141 (= standard_metadata.ingress_port (_ bv14 9)))) + (let (($x136 (= standard_metadata.ingress_port (_ bv13 9)))) + (let (($x131 (= standard_metadata.ingress_port (_ bv12 9)))) + (let (($x126 (= standard_metadata.ingress_port (_ bv11 9)))) + (let (($x121 (= standard_metadata.ingress_port (_ bv10 9)))) + (let (($x116 (= standard_metadata.ingress_port (_ bv9 9)))) + (let (($x111 (= standard_metadata.ingress_port (_ bv8 9)))) + (let (($x106 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x101 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x96 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x91 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x86 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x81 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x76 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x82 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x76) $x81))) + (let (($x117 (or (or (or (or (or (or (or $x82 $x86) $x91) $x96) $x101) $x106) $x111) $x116))) + (let (($x152 (or (or (or (or (or (or (or $x117 $x121) $x126) $x131) $x136) $x141) $x146) $x151))) + (or (or (or $x152 $x156) $x161) $x166)))))))))))))))))))))))) (assert - (let (($x39 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))) - (let (($x33 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))) - (let (($x35 (and true $x33))) - (let (($x41 (and $x35 $x39))) - (let (($x42 (and $x35 (not $x39)))) - (let (($x52 (bvugt standard_metadata.ingress_port (concat (_ bv0 6) (_ bv5 3))))) - (let (($x36 (and true (not $x33)))) - (let (($x54 (and $x36 $x52))) - (let ((?x56 (ite $x54 (_ bv511 9) (ite $x42 (_ bv511 9) (ite $x41 (_ bv511 9) standard_metadata.egress_spec))))) - (let (($x55 (and $x36 (not $x52)))) - (let ((?x68 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x55 (_ bv511 9) ?x56)))) - (let (($x63 (= ethernet.dst_addr (_ bv1 48)))) - (let (($x64 (and true $x63))) - (let (($x65 (and true $x64))) - (let ((?x73 (ite $x65 (_ bv1 9) ?x68))) - (let (($x96 (or (or (or (or false (= ?x73 (_ bv0 9))) (= ?x73 (_ bv1 9))) (= ?x73 (_ bv2 9))) (= ?x73 (_ bv3 9))))) - (let (($x116 (or (or (or (or $x96 (= ?x73 (_ bv4 9))) (= ?x73 (_ bv5 9))) (= ?x73 (_ bv6 9))) (= ?x73 (_ bv7 9))))) - (let (($x136 (or (or (or (or $x116 (= ?x73 (_ bv8 9))) (= ?x73 (_ bv9 9))) (= ?x73 (_ bv10 9))) (= ?x73 (_ bv11 9))))) - (let (($x156 (or (or (or (or $x136 (= ?x73 (_ bv12 9))) (= ?x73 (_ bv13 9))) (= ?x73 (_ bv14 9))) (= ?x73 (_ bv15 9))))) - (let (($x176 (or (or (or (or $x156 (= ?x73 (_ bv16 9))) (= ?x73 (_ bv17 9))) (= ?x73 (_ bv18 9))) (= ?x73 (_ bv19 9))))) - (let (($x75 (= ?x73 (_ bv511 9)))) - (or $x75 $x176))))))))))))))))))))))) + (let (($x33 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv15 4))))) + (let (($x27 (bvugt standard_metadata.ingress_port (concat (_ bv0 5) (_ bv10 4))))) + (let (($x17 (and true $x27))) + (let (($x35 (and $x17 $x33))) + (let (($x36 (and $x17 (not $x33)))) + (let (($x46 (bvugt standard_metadata.ingress_port (concat (_ bv0 6) (_ bv5 3))))) + (let (($x22 (and true (not $x27)))) + (let (($x48 (and $x22 $x46))) + (let (($x49 (and $x22 (not $x46)))) + (let ((?x62 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x49 (_ bv511 9) (ite $x48 (_ bv511 9) (ite $x36 (_ bv511 9) (ite $x35 (_ bv511 9) (_ bv0 9)))))))) + (let (($x57 (= ethernet.dst_addr (_ bv1 48)))) + (let (($x58 (and true $x57))) + (let (($x59 (and true $x58))) + (let ((?x67 (ite $x59 (_ bv1 9) ?x62))) + (let (($x89 (or (or (or (or false (= ?x67 (_ bv0 9))) (= ?x67 (_ bv1 9))) (= ?x67 (_ bv2 9))) (= ?x67 (_ bv3 9))))) + (let (($x109 (or (or (or (or $x89 (= ?x67 (_ bv4 9))) (= ?x67 (_ bv5 9))) (= ?x67 (_ bv6 9))) (= ?x67 (_ bv7 9))))) + (let (($x129 (or (or (or (or $x109 (= ?x67 (_ bv8 9))) (= ?x67 (_ bv9 9))) (= ?x67 (_ bv10 9))) (= ?x67 (_ bv11 9))))) + (let (($x149 (or (or (or (or $x129 (= ?x67 (_ bv12 9))) (= ?x67 (_ bv13 9))) (= ?x67 (_ bv14 9))) (= ?x67 (_ bv15 9))))) + (let (($x169 (or (or (or (or $x149 (= ?x67 (_ bv16 9))) (= ?x67 (_ bv17 9))) (= ?x67 (_ bv18 9))) (= ?x67 (_ bv19 9))))) + (let (($x69 (= ?x67 (_ bv511 9)))) + (or $x69 $x169)))))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/conditional_nonlattice.txt b/p4_symbolic/symbolic/expected/conditional_nonlattice.txt index 39b32a5b..a1f18593 100644 --- a/p4_symbolic/symbolic/expected/conditional_nonlattice.txt +++ b/p4_symbolic/symbolic/expected/conditional_nonlattice.txt @@ -101,7 +101,7 @@ ________________________________________________________________________________ ================================================================================ Finding packet for table MyIngress.t_2 and row -1 ================================================================================ -ingress_port = #b000000000 +ingress_port = #b000001100 egress_port = #b000000001 trace: dropped = 0 @@ -132,7 +132,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000001100 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -161,7 +161,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000001100 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -190,7 +190,7 @@ standard_metadata.egress_spec = #b000000001 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000001100 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -207,7 +207,7 @@ ________________________________________________________________________________ ================================================================================ Finding packet for table MyIngress.t_3 and row 0 ================================================================================ -ingress_port = #b000000000 +ingress_port = #b000001100 egress_port = #b000000001 trace: dropped = 0 @@ -238,7 +238,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000001100 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -267,7 +267,7 @@ standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000001100 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 @@ -296,7 +296,7 @@ standard_metadata.egress_spec = #b000000001 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 -standard_metadata.ingress_port = #b000000000 +standard_metadata.ingress_port = #b000001100 standard_metadata.instance_type = #x00000000 standard_metadata.mcast_grp = #x0000 standard_metadata.packet_length = #x00000000 diff --git a/p4_symbolic/symbolic/expected/conditional_sequence.smt2 b/p4_symbolic/symbolic/expected/conditional_sequence.smt2 index fc3a5fe9..334097a3 100644 --- a/p4_symbolic/symbolic/expected/conditional_sequence.smt2 +++ b/p4_symbolic/symbolic/expected/conditional_sequence.smt2 @@ -16,22 +16,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) h1.$extracted$: (ite true true false) @@ -51,22 +51,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) h1.$extracted$: (ite true true false) @@ -86,38 +86,36 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp -(egress) standard_metadata.egress_port: (ite (not (= standard_metadata.egress_spec #b111111111)) - standard_metadata.egress_spec +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 +(egress) standard_metadata.egress_port: (ite (not (= #b000000000 #b111111111)) + #b000000000 (ite (and true true (= h1.fr #xff)) #b000000001 standard_metadata.egress_port)) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid -(egress) standard_metadata.egress_spec: standard_metadata.egress_spec -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.egress_rid: #x0000 +(egress) standard_metadata.egress_spec: #b000000000 +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (assert - (let (($x109 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x109))) + (let (($x101 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x101))) (assert - (let (($x111 (= standard_metadata.egress_spec (_ bv1 9)))) - (let (($x112 (or (or false (= standard_metadata.egress_spec (_ bv0 9))) $x111))) - (let (($x94 (= standard_metadata.egress_spec (_ bv511 9)))) - (or $x94 $x112))))) + (let (($x104 (or (or false (= (_ bv0 9) (_ bv0 9))) (= (_ bv0 9) (_ bv1 9))))) + (let (($x87 (= (_ bv0 9) (_ bv511 9)))) + (or $x87 $x104)))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/conditional_sequence.txt b/p4_symbolic/symbolic/expected/conditional_sequence.txt index fc912d21..63975d8b 100644 --- a/p4_symbolic/symbolic/expected/conditional_sequence.txt +++ b/p4_symbolic/symbolic/expected/conditional_sequence.txt @@ -28,7 +28,7 @@ ingress_headers: $got_cloned$ = false h1.$extracted$ = false h1.$valid$ = true -h1.f1 = #x01 +h1.f1 = #x02 h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 @@ -64,7 +64,7 @@ parsed_headers: $got_cloned$ = false h1.$extracted$ = true h1.$valid$ = true -h1.f1 = #x01 +h1.f1 = #x02 h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 @@ -100,7 +100,7 @@ egress_headers: $got_cloned$ = false h1.$extracted$ = true h1.$valid$ = true -h1.f1 = #x01 +h1.f1 = #x02 h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 diff --git a/p4_symbolic/symbolic/expected/hardcoded.smt2 b/p4_symbolic/symbolic/expected/hardcoded.smt2 index 4b835ef2..1c4dee64 100644 --- a/p4_symbolic/symbolic/expected/hardcoded.smt2 +++ b/p4_symbolic/symbolic/expected/hardcoded.smt2 @@ -4,22 +4,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) scalars.$extracted$: false @@ -27,22 +27,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) scalars.$extracted$: false @@ -50,47 +50,46 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (and true (not (= standard_metadata.ingress_port (concat #x00 #b0))))) (a!2 (ite (and true (= standard_metadata.ingress_port (concat #x00 #b0))) (concat #x00 #b1) - standard_metadata.egress_spec))) + #b000000000))) (let ((a!3 (not (= (ite a!1 (concat #x00 #b0) a!2) #b111111111)))) (ite a!3 (ite a!1 (concat #x00 #b0) a!2) standard_metadata.egress_port))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (= standard_metadata.ingress_port (concat #x00 #b0))))) (a!2 (ite (and true (= standard_metadata.ingress_port (concat #x00 #b0))) (concat #x00 #b1) - standard_metadata.egress_spec))) + #b000000000))) (ite a!1 (concat #x00 #b0) a!2)) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (assert - (let (($x50 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x50))) + (let (($x42 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x42))) (assert - (let ((?x28 (concat (_ bv0 8) (_ bv0 1)))) - (let (($x29 (= standard_metadata.ingress_port ?x28))) - (let (($x31 (and true $x29))) - (let (($x32 (and true (not $x29)))) - (let ((?x37 (ite $x32 ?x28 (ite $x31 (concat (_ bv0 8) (_ bv1 1)) standard_metadata.egress_spec)))) - (let (($x53 (or (or false (= ?x37 (_ bv0 9))) (= ?x37 (_ bv1 9))))) - (let (($x41 (= ?x37 (_ bv511 9)))) - (or $x41 $x53))))))))) + (let ((?x22 (concat (_ bv0 8) (_ bv0 1)))) + (let (($x8 (= standard_metadata.ingress_port ?x22))) + (let (($x12 (and true $x8))) + (let (($x17 (and true (not $x8)))) + (let ((?x30 (ite $x17 ?x22 (ite $x12 (concat (_ bv0 8) (_ bv1 1)) (_ bv0 9))))) + (let (($x45 (or (or false (= ?x30 (_ bv0 9))) (= ?x30 (_ bv1 9))))) + (let (($x34 (= ?x30 (_ bv511 9)))) + (or $x34 $x45))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/reflector.smt2 b/p4_symbolic/symbolic/expected/reflector.smt2 index 9c5ba037..fc64a14a 100644 --- a/p4_symbolic/symbolic/expected/reflector.smt2 +++ b/p4_symbolic/symbolic/expected/reflector.smt2 @@ -4,22 +4,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) scalars.$extracted$: false @@ -27,22 +27,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) scalars.$extracted$: false @@ -50,39 +50,35 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp -(egress) standard_metadata.egress_port: (ite (not (= (ite true - standard_metadata.ingress_port - standard_metadata.egress_spec) - #b111111111)) - (ite true standard_metadata.ingress_port standard_metadata.egress_spec) +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 +(egress) standard_metadata.egress_port: (ite (not (= (ite true standard_metadata.ingress_port #b000000000) #b111111111)) + (ite true standard_metadata.ingress_port #b000000000) standard_metadata.egress_port) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid -(egress) standard_metadata.egress_spec: (ite true standard_metadata.ingress_port standard_metadata.egress_spec) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.egress_rid: #x0000 +(egress) standard_metadata.egress_spec: (ite true standard_metadata.ingress_port #b000000000) +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (assert - (let (($x38 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x38))) + (let (($x31 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x31))) (assert - (let ((?x27 (ite true standard_metadata.ingress_port standard_metadata.egress_spec))) - (let (($x41 (or (or false (= ?x27 (_ bv0 9))) (= ?x27 (_ bv1 9))))) - (let (($x29 (= ?x27 (_ bv511 9)))) - (or $x29 $x41))))) + (let (($x34 (or (or false (= (ite true standard_metadata.ingress_port (_ bv0 9)) (_ bv0 9))) (= (ite true standard_metadata.ingress_port (_ bv0 9)) (_ bv1 9))))) + (let ((?x10 (ite true standard_metadata.ingress_port (_ bv0 9)))) + (let (($x19 (= ?x10 (_ bv511 9)))) + (or $x19 $x34))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/string_optional.smt2 b/p4_symbolic/symbolic/expected/string_optional.smt2 index 0210e513..efaf665c 100644 --- a/p4_symbolic/symbolic/expected/string_optional.smt2 +++ b/p4_symbolic/symbolic/expected/string_optional.smt2 @@ -6,22 +6,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) scalars.$extracted$: false @@ -31,22 +31,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) scalars.$extracted$: false @@ -71,10 +71,10 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (and true (not (and true (= standard_metadata.ingress_port #b000000000))) (and true (= standard_metadata.ingress_port #b000000001)))) @@ -96,11 +96,9 @@ (a!6 (not (and true (= a!4 (concat #b0000000 #b10)))))) (let ((a!7 (ite a!5 #b000000000 - (ite (and true a!6 true) - #b000000001 - standard_metadata.egress_spec)))) + (ite (and true a!6 true) #b000000001 #b000000000)))) (ite (not (= a!7 #b111111111)) a!7 standard_metadata.egress_port)))))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (and true (not (and true (= standard_metadata.ingress_port #b000000000))) (and true (= standard_metadata.ingress_port #b000000001)))) @@ -120,48 +118,44 @@ a!3))) (let ((a!5 (and true (and true (= a!4 (concat #b0000000 #b10))))) (a!6 (not (and true (= a!4 (concat #b0000000 #b10)))))) - (ite a!5 - #b000000000 - (ite (and true a!6 true) #b000000001 standard_metadata.egress_spec)))))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp + (ite a!5 #b000000000 (ite (and true a!6 true) #b000000001 #b000000000)))))) +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun scalars.metadata.string_field () (_ BitVec 9)) (assert - (let (($x40 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x37 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x37) $x40)))) + (let (($x32 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x29 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x29) $x32)))) (assert - (let ((?x67 (concat (_ bv0 7) (_ bv2 2)))) - (let ((?x31 (concat (_ bv0 8) (_ bv0 1)))) - (let (($x40 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x41 (and true $x40))) - (let (($x34 (= standard_metadata.ingress_port (_ bv0 9)))) - (let (($x35 (and true $x34))) - (let (($x43 (not $x35))) - (let (($x48 (and true (and $x43 (not (and true (= standard_metadata.ingress_port (_ bv1 9)))))))) - (let ((?x56 (ite (and $x48 $x41) ?x31 (ite true ?x31 scalars.metadata.string_field)))) - (let (($x37 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x38 (and true $x37))) - (let (($x42 (and true $x35))) - (let ((?x68 (ite $x42 ?x67 (ite (and (and true $x43) $x38) (concat (_ bv0 8) (_ bv1 1)) ?x56)))) - (let (($x70 (and true (= ?x68 ?x67)))) - (let ((?x79 (ite (and (and true (not $x70)) true) (_ bv1 9) standard_metadata.egress_spec))) - (let (($x71 (and true $x70))) - (let ((?x81 (ite $x71 (_ bv0 9) ?x79))) - (let (($x89 (or (or (or false (= ?x81 (_ bv0 9))) (= ?x81 (_ bv1 9))) (= ?x81 (_ bv2 9))))) - (let (($x51 (= ?x81 (_ bv511 9)))) - (or $x51 $x89))))))))))))))))))))) + (let ((?x59 (concat (_ bv0 7) (_ bv2 2)))) + (let ((?x24 (concat (_ bv0 8) (_ bv0 1)))) + (let (($x32 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x33 (and true $x32))) + (let (($x14 (= standard_metadata.ingress_port (_ bv0 9)))) + (let (($x19 (and true $x14))) + (let (($x35 (not $x19))) + (let (($x40 (and true (and $x35 (not (and true (= standard_metadata.ingress_port (_ bv1 9)))))))) + (let ((?x48 (ite (and $x40 $x33) ?x24 (ite true ?x24 scalars.metadata.string_field)))) + (let (($x29 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x30 (and true $x29))) + (let (($x34 (and true $x19))) + (let ((?x60 (ite $x34 ?x59 (ite (and (and true $x35) $x30) (concat (_ bv0 8) (_ bv1 1)) ?x48)))) + (let (($x62 (and true (= ?x60 ?x59)))) + (let (($x63 (and true $x62))) + (let ((?x73 (ite $x63 (_ bv0 9) (ite (and (and true (not $x62)) true) (_ bv1 9) (_ bv0 9))))) + (let (($x81 (or (or (or false (= ?x73 (_ bv0 9))) (= ?x73 (_ bv1 9))) (= ?x73 (_ bv2 9))))) + (let (($x43 (= ?x73 (_ bv511 9)))) + (or $x43 $x81)))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/table.smt2 b/p4_symbolic/symbolic/expected/table.smt2 index f6ae7815..92278526 100644 --- a/p4_symbolic/symbolic/expected/table.smt2 +++ b/p4_symbolic/symbolic/expected/table.smt2 @@ -4,22 +4,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) scalars.$extracted$: false @@ -27,22 +27,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) scalars.$extracted$: false @@ -50,54 +50,48 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp -(egress) standard_metadata.egress_port: (let ((a!1 (and true - (not (and true (= standard_metadata.ingress_port #b000000000))) - true - (= standard_metadata.ingress_port #b000000001)))) -(let ((a!2 (ite (and true - (and true (= standard_metadata.ingress_port #b000000000))) - #b000000001 - (ite a!1 #b000000000 standard_metadata.egress_spec)))) - (ite (not (= a!2 #b111111111)) a!2 standard_metadata.egress_port))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid -(egress) standard_metadata.egress_spec: (let ((a!1 (and true - (not (and true (= standard_metadata.ingress_port #b000000000))) - true - (= standard_metadata.ingress_port #b000000001)))) - (ite (and true (and true (= standard_metadata.ingress_port #b000000000))) - #b000000001 - (ite a!1 #b000000000 standard_metadata.egress_spec))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 +(egress) standard_metadata.egress_port: (let ((a!1 (= (ite (and true + true + (= standard_metadata.ingress_port #b000000000)) + #b000000001 + #b000000000) + #b111111111))) + (ite (not a!1) + (ite (and true true (= standard_metadata.ingress_port #b000000000)) + #b000000001 + #b000000000) + standard_metadata.egress_port)) +(egress) standard_metadata.egress_rid: #x0000 +(egress) standard_metadata.egress_spec: (ite (and true true (= standard_metadata.ingress_port #b000000000)) + #b000000001 + #b000000000) +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (assert - (let (($x30 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x30))) + (let (($x19 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x19))) (assert - (let (($x30 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x31 (and true $x30))) - (let (($x34 (and true (not (and true (= standard_metadata.ingress_port (_ bv0 9))))))) - (let (($x27 (= standard_metadata.ingress_port (_ bv0 9)))) - (let (($x28 (and true $x27))) - (let (($x32 (and true $x28))) - (let ((?x46 (ite $x32 (_ bv1 9) (ite (and $x34 $x31) (_ bv0 9) standard_metadata.egress_spec)))) - (let (($x53 (or (or false (= ?x46 (_ bv0 9))) (= ?x46 (_ bv1 9))))) - (let (($x37 (= ?x46 (_ bv511 9)))) - (or $x37 $x53))))))))))) + (let (($x10 (= standard_metadata.ingress_port (_ bv0 9)))) + (let (($x22 (and true $x10))) + (let (($x17 (and true $x22))) + (let ((?x38 (ite $x17 (_ bv1 9) (_ bv0 9)))) + (let (($x42 (or (or false (= ?x38 (_ bv0 9))) (= ?x38 (_ bv1 9))))) + (let (($x29 (= ?x38 (_ bv511 9)))) + (or $x29 $x42)))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/table_hit_1.smt2 b/p4_symbolic/symbolic/expected/table_hit_1.smt2 index 7ffdff09..aa8b2da1 100644 --- a/p4_symbolic/symbolic/expected/table_hit_1.smt2 +++ b/p4_symbolic/symbolic/expected/table_hit_1.smt2 @@ -9,22 +9,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) ethernet.$extracted$: (ite true true false) @@ -37,22 +37,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) ethernet.$extracted$: (ite true true false) @@ -73,15 +73,15 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (ite (and true (and true (= ethernet.ether_type #x0010))) 0 (- 1))) (a!2 (and true (not (and true (= ethernet.ether_type #x0010)))))) (let ((a!3 (ite (and true (and true (= ethernet.ether_type #x0010))) #b000000010 - (ite a!2 #b111111111 standard_metadata.egress_spec)))) + (ite a!2 #b111111111 #b000000000)))) (let ((a!4 (ite (and true (distinct a!1 (- 1)) true @@ -89,54 +89,53 @@ #b000000011 a!3))) (ite (not (= a!4 #b111111111)) a!4 standard_metadata.egress_port)))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (ite (and true (and true (= ethernet.ether_type #x0010))) 0 (- 1))) (a!2 (and true (not (and true (= ethernet.ether_type #x0010)))))) (let ((a!3 (ite (and true (and true (= ethernet.ether_type #x0010))) #b000000010 - (ite a!2 #b111111111 standard_metadata.egress_spec)))) + (ite a!2 #b111111111 #b000000000)))) (ite (and true (distinct a!1 (- 1)) true (= ethernet.src_addr #x000000000100)) #b000000011 a!3))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun ethernet.ether_type () (_ BitVec 16)) (declare-fun ethernet.src_addr () (_ BitVec 48)) (assert - (let (($x95 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x90 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x85 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x80 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x75 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x71 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x67 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x72 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x67) $x71))) - (or (or (or (or (or $x72 $x75) $x80) $x85) $x90) $x95)))))))))) + (let (($x88 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x83 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x78 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x73 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x68 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x64 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x60 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x65 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x60) $x64))) + (or (or (or (or (or $x65 $x68) $x73) $x78) $x83) $x88)))))))))) (assert - (let ((?x38 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) standard_metadata.egress_spec))) - (let (($x31 (= ethernet.ether_type (_ bv16 16)))) - (let (($x32 (and true $x31))) - (let (($x33 (and true $x32))) - (let ((?x40 (ite $x33 0 (- 1)))) - (let (($x45 (and (distinct ?x40 (- 1)) true))) - (let (($x46 (and true $x45))) - (let (($x50 (and $x46 (and true (= ethernet.src_addr (_ bv256 48)))))) - (let ((?x56 (ite $x50 (_ bv3 9) (ite $x33 (_ bv2 9) ?x38)))) - (let (($x78 (or (or (or (or false (= ?x56 (_ bv0 9))) (= ?x56 (_ bv1 9))) (= ?x56 (_ bv2 9))) (= ?x56 (_ bv3 9))))) - (let (($x98 (or (or (or (or $x78 (= ?x56 (_ bv4 9))) (= ?x56 (_ bv5 9))) (= ?x56 (_ bv6 9))) (= ?x56 (_ bv7 9))))) - (let (($x58 (= ?x56 (_ bv511 9)))) - (or $x58 $x98)))))))))))))) + (let ((?x32 (ite (and true (not (and true (= ethernet.ether_type (_ bv16 16))))) (_ bv511 9) (_ bv0 9)))) + (let (($x30 (= ethernet.ether_type (_ bv16 16)))) + (let (($x15 (and true $x30))) + (let (($x27 (and true $x15))) + (let ((?x34 (ite $x27 0 (- 1)))) + (let (($x39 (and (distinct ?x34 (- 1)) true))) + (let (($x40 (and true $x39))) + (let (($x44 (and $x40 (and true (= ethernet.src_addr (_ bv256 48)))))) + (let ((?x50 (ite $x44 (_ bv3 9) (ite $x27 (_ bv2 9) ?x32)))) + (let (($x71 (or (or (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9))) (= ?x50 (_ bv2 9))) (= ?x50 (_ bv3 9))))) + (let (($x91 (or (or (or (or $x71 (= ?x50 (_ bv4 9))) (= ?x50 (_ bv5 9))) (= ?x50 (_ bv6 9))) (= ?x50 (_ bv7 9))))) + (let (($x52 (= ?x50 (_ bv511 9)))) + (or $x52 $x91)))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/table_hit_2.smt2 b/p4_symbolic/symbolic/expected/table_hit_2.smt2 index 38eb57aa..0ee87309 100644 --- a/p4_symbolic/symbolic/expected/table_hit_2.smt2 +++ b/p4_symbolic/symbolic/expected/table_hit_2.smt2 @@ -10,22 +10,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) h1.$extracted$: (ite true true false) @@ -39,22 +39,22 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) h1.$extracted$: (ite true true false) @@ -68,71 +68,69 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (= (ite (and true true (= h1.f1 #xff)) 0 (- 1)) (- 1))) (a!2 (distinct (ite (and true true (= h1.f1 #xff)) 0 (- 1)) (- 1)))) (let ((a!3 (ite (and true a!2 true (= h1.f2 #xff)) #b000000010 (ite (and true true (= h1.f1 #xff)) #b000000001 - (ite true (concat #x00 #b0) standard_metadata.egress_spec))))) + (ite true (concat #x00 #b0) #b000000000))))) (let ((a!4 (ite (and true a!1 true (= h1.f3 #xff)) #b000000011 a!3))) (ite (not (= a!4 #b111111111)) a!4 standard_metadata.egress_port)))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (= (ite (and true true (= h1.f1 #xff)) 0 (- 1)) (- 1))) (a!2 (distinct (ite (and true true (= h1.f1 #xff)) 0 (- 1)) (- 1)))) (let ((a!3 (ite (and true a!2 true (= h1.f2 #xff)) #b000000010 (ite (and true true (= h1.f1 #xff)) #b000000001 - (ite true (concat #x00 #b0) standard_metadata.egress_spec))))) + (ite true (concat #x00 #b0) #b000000000))))) (ite (and true a!1 true (= h1.f3 #xff)) #b000000011 a!3))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (ite (and true (not true)) #x00000002 #x00000000) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun h1.f1 () (_ BitVec 8)) (declare-fun h1.f2 () (_ BitVec 8)) (declare-fun h1.f3 () (_ BitVec 8)) (assert - (let (($x103 (= standard_metadata.ingress_port (_ bv7 9)))) - (let (($x98 (= standard_metadata.ingress_port (_ bv6 9)))) - (let (($x93 (= standard_metadata.ingress_port (_ bv5 9)))) - (let (($x88 (= standard_metadata.ingress_port (_ bv4 9)))) - (let (($x83 (= standard_metadata.ingress_port (_ bv3 9)))) - (let (($x79 (= standard_metadata.ingress_port (_ bv2 9)))) - (let (($x75 (= standard_metadata.ingress_port (_ bv1 9)))) - (let (($x80 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x75) $x79))) - (or (or (or (or (or $x80 $x83) $x88) $x93) $x98) $x103)))))))))) + (let (($x95 (= standard_metadata.ingress_port (_ bv7 9)))) + (let (($x90 (= standard_metadata.ingress_port (_ bv6 9)))) + (let (($x85 (= standard_metadata.ingress_port (_ bv5 9)))) + (let (($x80 (= standard_metadata.ingress_port (_ bv4 9)))) + (let (($x75 (= standard_metadata.ingress_port (_ bv3 9)))) + (let (($x71 (= standard_metadata.ingress_port (_ bv2 9)))) + (let (($x67 (= standard_metadata.ingress_port (_ bv1 9)))) + (let (($x72 (or (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x67) $x71))) + (or (or (or (or (or $x72 $x75) $x80) $x85) $x90) $x95)))))))))) (assert - (let (($x37 (= h1.f1 (_ bv255 8)))) - (let (($x38 (and true $x37))) - (let (($x39 (and true $x38))) - (let ((?x45 (ite $x39 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) standard_metadata.egress_spec)))) - (let ((?x43 (ite $x39 0 (- 1)))) - (let (($x46 (and (distinct ?x43 (- 1)) true))) - (let (($x47 (and true $x46))) - (let (($x50 (and $x47 (and true (= h1.f2 (_ bv255 8)))))) - (let (($x56 (= ?x43 (- 1)))) - (let (($x57 (and true $x56))) - (let (($x60 (and $x57 (and true (= h1.f3 (_ bv255 8)))))) - (let ((?x65 (ite $x60 (_ bv3 9) (ite $x50 (_ bv2 9) ?x45)))) - (let (($x86 (or (or (or (or false (= ?x65 (_ bv0 9))) (= ?x65 (_ bv1 9))) (= ?x65 (_ bv2 9))) (= ?x65 (_ bv3 9))))) - (let (($x106 (or (or (or (or $x86 (= ?x65 (_ bv4 9))) (= ?x65 (_ bv5 9))) (= ?x65 (_ bv6 9))) (= ?x65 (_ bv7 9))))) - (let (($x41 (= ?x65 (_ bv511 9)))) - (or $x41 $x106))))))))))))))))) + (let (($x18 (= h1.f1 (_ bv255 8)))) + (let (($x23 (and true $x18))) + (let (($x27 (and true $x23))) + (let ((?x36 (ite $x27 0 (- 1)))) + (let (($x39 (and (distinct ?x36 (- 1)) true))) + (let (($x40 (and true $x39))) + (let (($x43 (and $x40 (and true (= h1.f2 (_ bv255 8)))))) + (let (($x49 (= ?x36 (- 1)))) + (let (($x50 (and true $x49))) + (let (($x53 (and $x50 (and true (= h1.f3 (_ bv255 8)))))) + (let ((?x58 (ite $x53 (_ bv3 9) (ite $x43 (_ bv2 9) (ite $x27 (_ bv1 9) (ite true (concat (_ bv0 8) (_ bv0 1)) (_ bv0 9))))))) + (let (($x78 (or (or (or (or false (= ?x58 (_ bv0 9))) (= ?x58 (_ bv1 9))) (= ?x58 (_ bv2 9))) (= ?x58 (_ bv3 9))))) + (let (($x98 (or (or (or (or $x78 (= ?x58 (_ bv4 9))) (= ?x58 (_ bv5 9))) (= ?x58 (_ bv6 9))) (= ?x58 (_ bv7 9))))) + (let (($x34 (= ?x58 (_ bv511 9)))) + (or $x34 $x98)))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/table_hit_2.txt b/p4_symbolic/symbolic/expected/table_hit_2.txt index 859f6a36..399ab984 100644 --- a/p4_symbolic/symbolic/expected/table_hit_2.txt +++ b/p4_symbolic/symbolic/expected/table_hit_2.txt @@ -107,12 +107,12 @@ ________________________________________________________________________________ Finding packet for table MyIngress.t1 and row 0 ================================================================================ ingress_port = #b000000000 -egress_port = #b000000010 +egress_port = #b000000001 trace: dropped = 0 got cloned = 0 MyIngress.t1 => was matched on entry 0 -MyIngress.t2 => was matched on entry 0 +MyIngress.t2 => was matched on entry -1 MyIngress.t3 => was not matched! MyIngress.t4 => was matched on entry -1 tbl_table_hit_2l83 => was matched on entry -1 @@ -122,7 +122,7 @@ $got_cloned$ = false h1.$extracted$ = false h1.$valid$ = true h1.f1 = #xff -h1.f2 = #xff +h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 scalars.$extracted$ = false @@ -152,7 +152,7 @@ $got_cloned$ = false h1.$extracted$ = true h1.$valid$ = true h1.f1 = #xff -h1.f2 = #xff +h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 scalars.$extracted$ = false @@ -182,7 +182,7 @@ $got_cloned$ = false h1.$extracted$ = true h1.$valid$ = true h1.f1 = #xff -h1.f2 = #xff +h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 scalars.$extracted$ = false @@ -194,9 +194,9 @@ standard_metadata.checksum_error = #b0 standard_metadata.deq_qdepth = #b0000000000000000000 standard_metadata.deq_timedelta = #x00000000 standard_metadata.egress_global_timestamp = #x000000000000 -standard_metadata.egress_port = #b000000010 +standard_metadata.egress_port = #b000000001 standard_metadata.egress_rid = #x0000 -standard_metadata.egress_spec = #b000000010 +standard_metadata.egress_spec = #b000000001 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 @@ -227,7 +227,7 @@ $got_cloned$ = false h1.$extracted$ = false h1.$valid$ = true h1.f1 = #xff -h1.f2 = #x7f +h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 scalars.$extracted$ = false @@ -257,7 +257,7 @@ $got_cloned$ = false h1.$extracted$ = true h1.$valid$ = true h1.f1 = #xff -h1.f2 = #x7f +h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 scalars.$extracted$ = false @@ -287,7 +287,7 @@ $got_cloned$ = false h1.$extracted$ = true h1.$valid$ = true h1.f1 = #xff -h1.f2 = #x7f +h1.f2 = #x00 h1.f3 = #x00 h1.f4 = #x00 scalars.$extracted$ = false diff --git a/p4_symbolic/symbolic/expected/vrf.smt2 b/p4_symbolic/symbolic/expected/vrf.smt2 index 0f876256..f77a53f4 100644 --- a/p4_symbolic/symbolic/expected/vrf.smt2 +++ b/p4_symbolic/symbolic/expected/vrf.smt2 @@ -26,22 +26,22 @@ (ingress) standard_metadata.$extracted$: false (ingress) standard_metadata.$valid$: false (ingress) standard_metadata._padding: standard_metadata._padding -(ingress) standard_metadata.checksum_error: standard_metadata.checksum_error -(ingress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(ingress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(ingress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(ingress) standard_metadata.checksum_error: #b0 +(ingress) standard_metadata.deq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.deq_timedelta: #x00000000 +(ingress) standard_metadata.egress_global_timestamp: #x000000000000 (ingress) standard_metadata.egress_port: standard_metadata.egress_port -(ingress) standard_metadata.egress_rid: standard_metadata.egress_rid -(ingress) standard_metadata.egress_spec: standard_metadata.egress_spec -(ingress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(ingress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(ingress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(ingress) standard_metadata.egress_rid: #x0000 +(ingress) standard_metadata.egress_spec: #b000000000 +(ingress) standard_metadata.enq_qdepth: #b0000000000000000000 +(ingress) standard_metadata.enq_timestamp: #x00000000 +(ingress) standard_metadata.ingress_global_timestamp: #x000000000000 (ingress) standard_metadata.ingress_port: standard_metadata.ingress_port -(ingress) standard_metadata.instance_type: standard_metadata.instance_type -(ingress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(ingress) standard_metadata.instance_type: #x00000000 +(ingress) standard_metadata.mcast_grp: #x0000 (ingress) standard_metadata.packet_length: standard_metadata.packet_length (ingress) standard_metadata.parser_error: #x00000000 -(ingress) standard_metadata.priority: standard_metadata.priority +(ingress) standard_metadata.priority: #b000 (parsed) $got_cloned$: false (parsed) ethernet.$extracted$: (ite true true false) @@ -71,26 +71,26 @@ (parsed) standard_metadata.$extracted$: false (parsed) standard_metadata.$valid$: false (parsed) standard_metadata._padding: standard_metadata._padding -(parsed) standard_metadata.checksum_error: standard_metadata.checksum_error -(parsed) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(parsed) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(parsed) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(parsed) standard_metadata.checksum_error: #b0 +(parsed) standard_metadata.deq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.deq_timedelta: #x00000000 +(parsed) standard_metadata.egress_global_timestamp: #x000000000000 (parsed) standard_metadata.egress_port: standard_metadata.egress_port -(parsed) standard_metadata.egress_rid: standard_metadata.egress_rid -(parsed) standard_metadata.egress_spec: standard_metadata.egress_spec -(parsed) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(parsed) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(parsed) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(parsed) standard_metadata.egress_rid: #x0000 +(parsed) standard_metadata.egress_spec: #b000000000 +(parsed) standard_metadata.enq_qdepth: #b0000000000000000000 +(parsed) standard_metadata.enq_timestamp: #x00000000 +(parsed) standard_metadata.ingress_global_timestamp: #x000000000000 (parsed) standard_metadata.ingress_port: standard_metadata.ingress_port -(parsed) standard_metadata.instance_type: standard_metadata.instance_type -(parsed) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(parsed) standard_metadata.instance_type: #x00000000 +(parsed) standard_metadata.mcast_grp: #x0000 (parsed) standard_metadata.packet_length: standard_metadata.packet_length (parsed) standard_metadata.parser_error: (let ((a!1 (and true (not (= (concat #x0 #x800) ethernet.eth_type)) (not true))) (a!2 (ite (and true (= (concat #x0 #x800) ethernet.eth_type) (not true)) #x00000002 #x00000000))) (ite a!1 #x00000002 a!2)) -(parsed) standard_metadata.priority: standard_metadata.priority +(parsed) standard_metadata.priority: #b000 (egress) $got_cloned$: false (egress) ethernet.$extracted$: (ite true true false) @@ -296,10 +296,10 @@ (egress) standard_metadata.$extracted$: false (egress) standard_metadata.$valid$: false (egress) standard_metadata._padding: standard_metadata._padding -(egress) standard_metadata.checksum_error: standard_metadata.checksum_error -(egress) standard_metadata.deq_qdepth: standard_metadata.deq_qdepth -(egress) standard_metadata.deq_timedelta: standard_metadata.deq_timedelta -(egress) standard_metadata.egress_global_timestamp: standard_metadata.egress_global_timestamp +(egress) standard_metadata.checksum_error: #b0 +(egress) standard_metadata.deq_qdepth: #b0000000000000000000 +(egress) standard_metadata.deq_timedelta: #x00000000 +(egress) standard_metadata.egress_global_timestamp: #x000000000000 (egress) standard_metadata.egress_port: (let ((a!1 (ite (and true (= (concat #x0 #x800) ethernet.eth_type)) true false)) (a!3 (not (and true (= (bvand ipv4.srcAddr #x09210909) #x00210100))))) (let ((a!2 (and (and true a!1) @@ -347,9 +347,7 @@ (and (not a!7) (not a!8)) a!9) #b000000001 - (ite a!11 - #b000000001 - (ite a!12 #b111111111 standard_metadata.egress_spec))))) + (ite a!11 #b000000001 (ite a!12 #b111111111 #b000000000))))) (let ((a!14 (ite (and (and (and true a!1) (bvuge a!5 #b1)) (not a!7) a!8) #b000000000 a!13))) @@ -357,7 +355,7 @@ #b000000001 a!14))) (ite (not (= a!15 #b111111111)) a!15 standard_metadata.egress_port))))))))) -(egress) standard_metadata.egress_rid: standard_metadata.egress_rid +(egress) standard_metadata.egress_rid: #x0000 (egress) standard_metadata.egress_spec: (let ((a!1 (ite (and true (= (concat #x0 #x800) ethernet.eth_type)) true false)) (a!3 (not (and true (= (bvand ipv4.srcAddr #x09210909) #x00210100))))) (let ((a!2 (and (and true a!1) @@ -405,72 +403,69 @@ (and (not a!7) (not a!8)) a!9) #b000000001 - (ite a!11 - #b000000001 - (ite a!12 #b111111111 standard_metadata.egress_spec))))) + (ite a!11 #b000000001 (ite a!12 #b111111111 #b000000000))))) (let ((a!14 (ite (and (and (and true a!1) (bvuge a!5 #b1)) (not a!7) a!8) #b000000000 a!13))) (ite (and (and (and true a!1) (bvuge a!5 #b1)) a!7) #b000000001 a!14)))))))) -(egress) standard_metadata.enq_qdepth: standard_metadata.enq_qdepth -(egress) standard_metadata.enq_timestamp: standard_metadata.enq_timestamp -(egress) standard_metadata.ingress_global_timestamp: standard_metadata.ingress_global_timestamp +(egress) standard_metadata.enq_qdepth: #b0000000000000000000 +(egress) standard_metadata.enq_timestamp: #x00000000 +(egress) standard_metadata.ingress_global_timestamp: #x000000000000 (egress) standard_metadata.ingress_port: standard_metadata.ingress_port -(egress) standard_metadata.instance_type: standard_metadata.instance_type -(egress) standard_metadata.mcast_grp: standard_metadata.mcast_grp +(egress) standard_metadata.instance_type: #x00000000 +(egress) standard_metadata.mcast_grp: #x0000 (egress) standard_metadata.packet_length: standard_metadata.packet_length (egress) standard_metadata.parser_error: (let ((a!1 (and true (not (= (concat #x0 #x800) ethernet.eth_type)) (not true))) (a!2 (ite (and true (= (concat #x0 #x800) ethernet.eth_type) (not true)) #x00000002 #x00000000))) (ite a!1 #x00000002 a!2)) -(egress) standard_metadata.priority: standard_metadata.priority +(egress) standard_metadata.priority: #b000 (solver constraints) ; (set-info :status unknown) (declare-fun standard_metadata.ingress_port () (_ BitVec 9)) -(declare-fun standard_metadata.egress_spec () (_ BitVec 9)) (declare-fun scalars.local_metadata_t.vrf () (_ BitVec 10)) (declare-fun ipv4.srcAddr () (_ BitVec 32)) (declare-fun ethernet.eth_type () (_ BitVec 16)) (declare-fun ipv4.dstAddr () (_ BitVec 32)) (declare-fun scalars.local_metadata_t.vrf_is_valid () (_ BitVec 1)) (assert - (let (($x181 (= standard_metadata.ingress_port (_ bv1 9)))) - (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x181))) + (let (($x172 (= standard_metadata.ingress_port (_ bv1 9)))) + (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x172))) (assert - (let ((?x61 (concat (_ bv0 9) (_ bv0 1)))) - (let (($x75 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) + (let ((?x53 (concat (_ bv0 9) (_ bv0 1)))) + (let (($x67 (and true (= (bvand ipv4.srcAddr (_ bv555813129 32)) (_ bv555810816 32))))) (let (($x11 (= (concat (_ bv0 4) (_ bv2048 12)) ethernet.eth_type))) (let (($x10 (and true $x11))) - (let (($x51 (ite $x10 true false))) - (let (($x64 (and true $x51))) - (let (($x79 (and (and $x64 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x75))) - (let ((?x91 (concat (_ bv0 9) (_ bv1 1)))) - (let (($x70 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) - (let (($x76 (and $x64 $x70))) - (let ((?x92 (ite $x76 ?x91 (ite $x79 ?x61 (ite true ?x61 scalars.local_metadata_t.vrf))))) - (let (($x101 (= ?x92 ?x61))) - (let (($x119 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x101))) - (let (($x113 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x92 ?x91)))) - (let (($x107 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x101))) - (let (($x102 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x101))) - (let (($x121 (not $x102))) - (let (($x125 (and $x121 (not $x107)))) - (let (($x129 (and $x125 (not $x113)))) - (let ((?x58 (ite false (_ bv1 1) (_ bv0 1)))) - (let ((?x87 (ite true (_ bv1 1) (_ bv0 1)))) - (let ((?x93 (ite $x76 ?x87 (ite $x79 ?x87 (ite true ?x58 scalars.local_metadata_t.vrf_is_valid))))) - (let (($x94 (bvuge ?x93 (_ bv1 1)))) - (let (($x96 (and $x64 $x94))) - (let ((?x136 (ite (and $x96 (and $x129 (not $x119))) (_ bv511 9) standard_metadata.egress_spec))) - (let (($x131 (and (and $x96 $x129) $x119))) - (let (($x127 (and (and $x96 $x125) $x113))) - (let (($x123 (and (and $x96 $x121) $x107))) - (let (($x120 (and $x96 $x102))) - (let ((?x169 (ite $x120 (_ bv1 9) (ite $x123 (_ bv0 9) (ite $x127 (_ bv1 9) (ite $x131 (_ bv1 9) ?x136)))))) - (let (($x184 (or (or false (= ?x169 (_ bv0 9))) (= ?x169 (_ bv1 9))))) - (let (($x63 (= ?x169 (_ bv511 9)))) - (or $x63 $x184)))))))))))))))))))))))))))))))))) + (let (($x41 (ite $x10 true false))) + (let (($x56 (and true $x41))) + (let (($x71 (and (and $x56 (not (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) $x67))) + (let ((?x83 (concat (_ bv0 9) (_ bv1 1)))) + (let (($x62 (and true (= (bvand ipv4.srcAddr (_ bv153159945 32)) (_ bv2162944 32))))) + (let (($x68 (and $x56 $x62))) + (let ((?x84 (ite $x68 ?x83 (ite $x71 ?x53 (ite true ?x53 scalars.local_metadata_t.vrf))))) + (let (($x93 (= ?x84 ?x53))) + (let (($x111 (and (and true (= ((_ extract 31 24) ipv4.dstAddr) ((_ extract 31 24) (_ bv167772160 32)))) $x93))) + (let (($x105 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32)))) (= ?x84 ?x83)))) + (let (($x99 (and (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32)))) $x93))) + (let (($x94 (and (and true (= ipv4.dstAddr (_ bv168427520 32))) $x93))) + (let (($x113 (not $x94))) + (let (($x117 (and $x113 (not $x99)))) + (let (($x121 (and $x117 (not $x105)))) + (let ((?x51 (ite false (_ bv1 1) (_ bv0 1)))) + (let ((?x79 (ite true (_ bv1 1) (_ bv0 1)))) + (let ((?x85 (ite $x68 ?x79 (ite $x71 ?x79 (ite true ?x51 scalars.local_metadata_t.vrf_is_valid))))) + (let (($x86 (bvuge ?x85 (_ bv1 1)))) + (let (($x88 (and $x56 $x86))) + (let (($x123 (and (and $x88 $x121) $x111))) + (let (($x119 (and (and $x88 $x117) $x105))) + (let ((?x145 (ite $x119 (_ bv1 9) (ite $x123 (_ bv1 9) (ite (and $x88 (and $x121 (not $x111))) (_ bv511 9) (_ bv0 9)))))) + (let (($x115 (and (and $x88 $x113) $x99))) + (let (($x112 (and $x88 $x94))) + (let ((?x160 (ite $x112 (_ bv1 9) (ite $x115 (_ bv0 9) ?x145)))) + (let (($x175 (or (or false (= ?x160 (_ bv0 9))) (= ?x160 (_ bv1 9))))) + (let (($x55 (= ?x160 (_ bv511 9)))) + (or $x55 $x175)))))))))))))))))))))))))))))))))) (check-sat) diff --git a/p4_symbolic/symbolic/expected/vrf.txt b/p4_symbolic/symbolic/expected/vrf.txt index 1294c897..09ad9f68 100644 --- a/p4_symbolic/symbolic/expected/vrf.txt +++ b/p4_symbolic/symbolic/expected/vrf.txt @@ -26,7 +26,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = false ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0010 +ipv4.dstAddr = #x0a0a0004 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -72,7 +72,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0010 +ipv4.dstAddr = #x0a0a0004 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -118,7 +118,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0010 +ipv4.dstAddr = #x0a0a0004 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -630,7 +630,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = false ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x00000000 +ipv4.dstAddr = #x0a000000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -676,7 +676,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x00000000 +ipv4.dstAddr = #x0a000000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -722,7 +722,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x00000000 +ipv4.dstAddr = #x0a000000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -918,7 +918,7 @@ egress_port = #b000000001 trace: dropped = 0 got cloned = 0 -packet_ingress.ipv4_lpm_table => was matched on entry 1 +packet_ingress.ipv4_lpm_table => was matched on entry 2 packet_ingress.set_vrf_table => was matched on entry 1 tbl_vrf133 => was matched on entry -1 @@ -932,7 +932,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = false ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0000 +ipv4.dstAddr = #x0a140000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -978,7 +978,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0000 +ipv4.dstAddr = #x0a140000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -1018,13 +1018,13 @@ egress_headers: $got_cloned$ = false ethernet.$extracted$ = true ethernet.$valid$ = true -ethernet.dstAddr = #x000000000000 +ethernet.dstAddr = #x00000000000a ethernet.eth_type = #x0800 ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0000 +ipv4.dstAddr = #x0a140000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -1069,7 +1069,7 @@ egress_port = #b000000001 trace: dropped = 0 got cloned = 0 -packet_ingress.ipv4_lpm_table => was matched on entry 1 +packet_ingress.ipv4_lpm_table => was matched on entry 2 packet_ingress.set_vrf_table => was matched on entry 1 tbl_vrf133 => was matched on entry -1 @@ -1083,7 +1083,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = false ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0000 +ipv4.dstAddr = #x0a140000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -1108,7 +1108,7 @@ standard_metadata.deq_timedelta = #x00000000 standard_metadata.egress_global_timestamp = #x000000000000 standard_metadata.egress_port = #b000000000 standard_metadata.egress_rid = #x0000 -standard_metadata.egress_spec = #b000100000 +standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 @@ -1129,7 +1129,7 @@ ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0000 +ipv4.dstAddr = #x0a140000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 @@ -1154,7 +1154,7 @@ standard_metadata.deq_timedelta = #x00000000 standard_metadata.egress_global_timestamp = #x000000000000 standard_metadata.egress_port = #b000000000 standard_metadata.egress_rid = #x0000 -standard_metadata.egress_spec = #b000100000 +standard_metadata.egress_spec = #b000000000 standard_metadata.enq_qdepth = #b0000000000000000000 standard_metadata.enq_timestamp = #x00000000 standard_metadata.ingress_global_timestamp = #x000000000000 @@ -1169,13 +1169,13 @@ egress_headers: $got_cloned$ = false ethernet.$extracted$ = true ethernet.$valid$ = true -ethernet.dstAddr = #x000000000000 +ethernet.dstAddr = #x00000000000a ethernet.eth_type = #x0800 ethernet.srcAddr = #x000000000000 ipv4.$extracted$ = true ipv4.$valid$ = true ipv4.diffserv = #x00 -ipv4.dstAddr = #x0a0a0000 +ipv4.dstAddr = #x0a140000 ipv4.flags = #b000 ipv4.fragOffset = #b0000000000000 ipv4.hdrChecksum = #x0000 diff --git a/p4_symbolic/symbolic/parser.cc b/p4_symbolic/symbolic/parser.cc index 5e3bc24f..0b604988 100644 --- a/p4_symbolic/symbolic/parser.cc +++ b/p4_symbolic/symbolic/parser.cc @@ -14,19 +14,25 @@ #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" +#include "p4_symbolic/symbolic/v1model.h" #include "z3++.h" namespace p4_symbolic::symbolic::parser { @@ -42,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(); @@ -52,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())) { @@ -77,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); @@ -91,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: { @@ -104,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() @@ -142,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: { @@ -204,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); @@ -221,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)); } @@ -356,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(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. @@ -404,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); @@ -424,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])); } } @@ -452,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 @@ -465,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(); @@ -486,7 +493,7 @@ absl::StatusOr GetErrorCodeExpression(const ir::P4Program &program, // Obtain the bitwidth of the `parser_error` field ASSIGN_OR_RETURN(unsigned int bitwidth, - util::GetFieldBitwidth(kParserErrorField, program)); + util::GetFieldBitwidth(v1model::kParserErrorField, program)); return z3_context.bv_val(error_code, bitwidth); } diff --git a/p4_symbolic/symbolic/parser_test.cc b/p4_symbolic/symbolic/parser_test.cc index 6033b8c4..d4fca492 100644 --- a/p4_symbolic/symbolic/parser_test.cc +++ b/p4_symbolic/symbolic/parser_test.cc @@ -28,7 +28,6 @@ #include "gutil/status_matchers.h" #include "p4_symbolic/ir/ir.h" #include "p4_symbolic/ir/ir.pb.h" -#include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/symbolic/v1model.h" #include "z3++.h" @@ -86,6 +85,9 @@ constexpr absl::string_view kHeaders = R"pb( key: "src_addr" value { name: "src_addr" bitwidth: 48 } } + ordered_fields_list: "dst_addr" + ordered_fields_list: "src_addr" + ordered_fields_list: "ether_type" } } headers { @@ -153,6 +155,21 @@ constexpr absl::string_view kHeaders = R"pb( key: "version" value { name: "version" bitwidth: 4 } } + ordered_fields_list: "version" + ordered_fields_list: "ihl" + ordered_fields_list: "dscp" + ordered_fields_list: "ecn" + ordered_fields_list: "total_len" + ordered_fields_list: "identification" + ordered_fields_list: "reserved" + ordered_fields_list: "do_not_fragment" + ordered_fields_list: "more_fragments" + ordered_fields_list: "frag_offset" + ordered_fields_list: "ttl" + ordered_fields_list: "protocol" + ordered_fields_list: "header_checksum" + ordered_fields_list: "src_addr" + ordered_fields_list: "dst_addr" } } headers { @@ -160,10 +177,91 @@ constexpr absl::string_view kHeaders = R"pb( value { name: "standard_metadata" id: 1 + fields { + key: "_padding" + value { name: "_padding" bitwidth: 3 } + } + fields { + key: "checksum_error" + value { name: "checksum_error" bitwidth: 1 } + } + fields { + key: "deq_qdepth" + value { name: "deq_qdepth" bitwidth: 19 } + } + fields { + key: "deq_timedelta" + value { name: "deq_timedelta" bitwidth: 32 } + } + fields { + key: "egress_global_timestamp" + value { name: "egress_global_timestamp" bitwidth: 48 } + } + fields { + key: "egress_port" + value { name: "egress_port" bitwidth: 9 } + } + fields { + key: "egress_rid" + value { name: "egress_rid" bitwidth: 16 } + } + fields { + key: "egress_spec" + value { name: "egress_spec" bitwidth: 9 } + } + fields { + key: "enq_qdepth" + value { name: "enq_qdepth" bitwidth: 19 } + } + fields { + key: "enq_timestamp" + value { name: "enq_timestamp" bitwidth: 32 } + } + fields { + key: "ingress_global_timestamp" + value { name: "ingress_global_timestamp" bitwidth: 48 } + } + fields { + key: "ingress_port" + value { name: "ingress_port" bitwidth: 9 } + } + fields { + key: "instance_type" + value { name: "instance_type" bitwidth: 32 } + } + fields { + key: "mcast_grp" + value { name: "mcast_grp" bitwidth: 16 } + } + fields { + key: "packet_length" + value { name: "packet_length" bitwidth: 32 } + } fields { key: "parser_error" value { name: "parser_error" bitwidth: 32 } } + fields { + key: "priority" + value { name: "priority" bitwidth: 3 } + } + ordered_fields_list: "ingress_port" + ordered_fields_list: "egress_spec" + ordered_fields_list: "egress_port" + ordered_fields_list: "instance_type" + ordered_fields_list: "packet_length" + ordered_fields_list: "enq_timestamp" + ordered_fields_list: "enq_qdepth" + ordered_fields_list: "deq_timedelta" + ordered_fields_list: "deq_qdepth" + ordered_fields_list: "ingress_global_timestamp" + ordered_fields_list: "egress_global_timestamp" + ordered_fields_list: "mcast_grp" + ordered_fields_list: "egress_rid" + ordered_fields_list: "checksum_error" + ordered_fields_list: "parser_error" + ordered_fields_list: "priority" + ordered_fields_list: "_padding" } } )pb"; @@ -943,7 +1041,7 @@ std::vector GetParserTestInstances() { ctx.bv_val(0x0800, 16))}, {"ipv4.$extracted$", (ctx.bv_const("ethernet.ether_type", 16) == ctx.bv_val(0x0800, 16))}, - {std::string(kParserErrorField), + {std::string(v1model::kParserErrorField), z3::ite((ctx.bv_const("ethernet.ether_type", 16) != ctx.bv_val(0x0800, 16)), ctx.bv_val(2, 32), ctx.bv_val(0, 32))}, 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 b247c768..87146f65 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" @@ -37,15 +42,19 @@ namespace symbolic { // A port reserved to encode dropping packets. // The value is arbitrary; we choose the same value as BMv2: // https://github.com/p4lang/behavioral-model/blob/main/docs/simple_switch.md#standard-metadata -constexpr int kDropPort = 511; // 2^9 - 1. +constexpr int kDropPort = 511; // 2^9 - 1. + // An arbitrary port we reserve for the CPU port (for PacketIO packets). -constexpr int kCpuPort = 510; // 2^9 - 2. +constexpr int kCpuPort = 510; // 2^9 - 2. + +// Bit-width of port numbers. constexpr int kPortBitwidth = 9; // Boolean pseudo header field that is initialized to false, set to true when // the header is extracted, and set to true/false when `setValid`/`setInvalid` // is called, respectively. constexpr absl::string_view kValidPseudoField = "$valid$"; + // Boolean pseudo header field denoting that the header has been extracted by // the parser. It is initialized to false and set to true when the header is // extracted. This is necessary to distinguish between headers extracted and @@ -53,14 +62,10 @@ constexpr absl::string_view kValidPseudoField = "$valid$"; // example, a `packet_in` header may be set to valid but should never be // extracted from the input packet. constexpr absl::string_view kExtractedPseudoField = "$extracted$"; + // Boolean pseudo header field that is set to true by p4-symbolic if the packet // gets cloned. Not an actual header field, but convenient for analysis. constexpr absl::string_view kGotClonedPseudoField = "$got_cloned$"; -// 32-bit bit-vector field in standard metadata indicating whether there is a -// parser error. The error code is defined in core.p4 and can be extended by the -// P4 program. 0 means no error. -constexpr absl::string_view kParserErrorField = - "standard_metadata.parser_error"; // The overall state of our symbolic solver/interpreter. // This is returned by our main analysis/interpration function, and is used @@ -72,9 +77,8 @@ constexpr absl::string_view kParserErrorField = // 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 @@ -134,7 +136,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 +156,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.cc b/p4_symbolic/symbolic/table_entry.cc new file mode 100644 index 00000000..7f662553 --- /dev/null +++ b/p4_symbolic/symbolic/table_entry.cc @@ -0,0 +1,312 @@ +// Copyright 2024 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 "absl/container/flat_hash_map.h" +#include "absl/status/statusor.h" +#include "absl/strings/str_cat.h" +#include "absl/strings/string_view.h" +#include "gutil/status.h" +#include "p4/config/v1/p4info.pb.h" +#include "p4_pdpi/ir.pb.h" +#include "p4_symbolic/ir/ir.pb.h" +#include "p4_symbolic/symbolic/util.h" +#include "z3++.h" + +namespace p4_symbolic::symbolic { + +using MatchType = p4::config::v1::MatchField::MatchType; + +namespace { + +// A static mapping between the PI match type to the type string. +const absl::flat_hash_map match_type_to_str = { + {MatchType::MatchField_MatchType_EXACT, "exact"}, + {MatchType::MatchField_MatchType_LPM, "lpm"}, + {MatchType::MatchField_MatchType_TERNARY, "ternary"}, + {MatchType::MatchField_MatchType_OPTIONAL, "optional"}, +}; + +} // namespace + +TableEntry::TableEntry(int index, ir::TableEntry ir_entry) + : index_(index), ir_entry_(std::move(ir_entry)) {} + +int TableEntry::GetIndex() const { return index_; } +bool TableEntry::IsConcrete() const { return ir_entry_.has_concrete_entry(); } +bool TableEntry::IsSymbolic() const { return ir_entry_.has_symbolic_entry(); } + +const std::string &TableEntry::GetTableName() const { + return GetPdpiIrTableEntry().table_name(); +} + +const ir::TableEntry &TableEntry::GetP4SymbolicIrTableEntry() const { + return ir_entry_; +} + +const pdpi::IrTableEntry &TableEntry::GetPdpiIrTableEntry() const { + if (IsConcrete()) return ir_entry_.concrete_entry(); + return ir_entry_.symbolic_entry().sketch(); +} + +absl::StatusOr TableEntry::GetSymbolicMatchInfo( + absl::string_view match_name, const ir::Table &table, + const ir::P4Program &program) const { + // Check if the match exists in the table definition. + if (!table.table_definition().match_fields_by_name().contains(match_name)) { + return gutil::NotFoundErrorBuilder() + << "Match '" << match_name << "' not found in table '" + << GetTableName() << "'"; + } + + const p4::config::v1::MatchField &pi_match_field = table.table_definition() + .match_fields_by_name() + .at(match_name) + .match_field(); + + // Check if the match type is specified and supported. + if (!pi_match_field.has_match_type() || + !match_type_to_str.contains(pi_match_field.match_type())) { + return gutil::InvalidArgumentErrorBuilder() + << "Match type must be one of [exact, lpm, ternary, optional]. " + "Found match: " + << pi_match_field.DebugString(); + } + + // Return an error if this is a fully concrete entry. + if (IsConcrete()) { + return gutil::InvalidArgumentErrorBuilder() + << "Entry " << GetIndex() << " of table '" << GetTableName() + << "' is not symbolic."; + } + + // If the specified match of this entry is an explicit wildcard, return an + // error and no symbolic variable should be created. + const auto &entry_matches = GetPdpiIrTableEntry().matches(); + auto ir_match_it = + std::find_if(entry_matches.begin(), entry_matches.end(), + [&match_name](const pdpi::IrMatch &match) -> bool { + return match.name() == match_name; + }); + if (ir_match_it == entry_matches.end()) { + return gutil::InvalidArgumentErrorBuilder() + << "Match '" << match_name + << "' is an explicit wildcard. The match is omitted in the IR table" + " entry. To specify a symbolic match, please set the match name" + " while leaving other fields unset."; + } + + // Use the matched header field to get the match bit-width. + auto it = table.table_implementation().match_name_to_field().find(match_name); + if (it == table.table_implementation().match_name_to_field().end()) { + return gutil::NotFoundErrorBuilder() + << "Match '" << match_name + << "' not found in implementation of table '" << GetTableName() + << "'. Found: " << table.DebugString(); + } + ASSIGN_OR_RETURN(int bitwidth, + util::GetFieldBitwidth(it->second.header_name(), + it->second.field_name(), program)); + + // If the table definition has the match bit-width, make sure it is consistent + // with the one in the table implementation. + if (pi_match_field.bitwidth() != 0 && pi_match_field.bitwidth() != bitwidth) { + return gutil::InternalErrorBuilder() + << "Bit-width of match '" << match_name << "' in table '" + << GetTableName() + << "' is inconsistent between the definition and implementation."; + } + + // Construct and return the variable names with the following template: + // "_entry____(value|mask)" + const auto &match_type = pi_match_field.match_type(); + std::string name_prefix = + absl::StrCat(GetTableName(), "_entry_", GetIndex(), "_", match_name, "_", + match_type_to_str.at(match_type), "_"); + return SymbolicMatchInfo{ + .match_type = match_type, + .bitwidth = bitwidth, + .value_variable_name = absl::StrCat(name_prefix, "value"), + .mask_variable_name = absl::StrCat(name_prefix, "mask"), + }; +} + +absl::StatusOr TableEntry::GetActionChoiceSymbolicVariableName( + absl::string_view action_name, const ir::Table &table) const { + // Check if the action exists in the table definition based on the given + // `action_name`. + auto action_ref_it = std::find_if( + table.table_definition().entry_actions().begin(), + table.table_definition().entry_actions().end(), + [&action_name](const pdpi::IrActionReference &action_ref) -> bool { + return action_ref.action().preamble().name() == action_name; + }); + + if (action_ref_it == table.table_definition().entry_actions().end()) { + return gutil::NotFoundErrorBuilder() + << "Action '" << action_name << "' not found in table '" + << GetTableName() << "'"; + } + + // Return an error if this is a fully concrete entry. + if (IsConcrete()) { + return gutil::InvalidArgumentErrorBuilder() + << "Entry " << GetIndex() << " of table '" << GetTableName() + << "' is not symbolic."; + } + + // Construct and return the variable name with the following template: + // "_entry___$chosen$" + return absl::StrCat(GetTableName(), "_entry_", GetIndex(), "_", action_name, + "_$chosen$"); +} + +absl::StatusOr +TableEntry::GetSymbolicActionParameterInfo(absl::string_view param_name, + const ir::Action &action, + const ir::Table &table) const { + const absl::string_view action_name = + action.action_definition().preamble().name(); + + // Check if the action with the given `action_name` exists in the table + // definition. + auto action_ref_it = std::find_if( + table.table_definition().entry_actions().begin(), + table.table_definition().entry_actions().end(), + [&action_name](const pdpi::IrActionReference &action_ref) -> bool { + return action_ref.action().preamble().name() == action_name; + }); + + if (action_ref_it == table.table_definition().entry_actions().end()) { + return gutil::NotFoundErrorBuilder() + << "Action '" << action_name << "' not found in table '" + << GetTableName() << "'"; + } + + // Return an error if this is a fully concrete entry. + if (IsConcrete()) { + return gutil::InvalidArgumentErrorBuilder() + << "Entry " << GetIndex() << " of table '" << GetTableName() + << "' is not symbolic."; + } + + // Check if the parameter with the given `param_name` exists in the action + // implementation. + auto param_bitwidth_it = + action.action_implementation().parameter_to_bitwidth().find(param_name); + if (param_bitwidth_it == + action.action_implementation().parameter_to_bitwidth().end()) { + return gutil::NotFoundErrorBuilder() + << "Action parameter '" << param_name + << "' not found in implementation of action '" << action_name << "'"; + } + int bitwidth = param_bitwidth_it->second; + + // Check if the parameter with the given `param_name` exists in the action + // definition. + auto param_it = action.action_definition().params_by_name().find(param_name); + if (param_it == action.action_definition().params_by_name().end()) { + return gutil::NotFoundErrorBuilder() + << "Action parameter '" << param_name + << "' not found in definition of action '" << action_name << "'"; + } + + // If the action definition has the parameter bit-width, make sure it is + // consistent with the one in the action implementation. + if (param_it->second.param().bitwidth() != 0 && + param_it->second.param().bitwidth() != bitwidth) { + return gutil::InternalErrorBuilder() + << "Bit-width of parameter '" << param_name << "' in action '" + << action_name + << "' is inconsistent between the definition and implementation."; + } + + // Construct and return the variable name and its bit-width with the following + // template: + // "_entry___" + std::string variable_name = absl::StrCat( + GetTableName(), "_entry_", GetIndex(), "_", action_name, "_", param_name); + return SymbolicActionParameterInfo{ + .variable_name = variable_name, + .bitwidth = bitwidth, + }; +} + +absl::StatusOr TableEntry::GetMatchValues( + absl::string_view match_name, const ir::Table &table, + const ir::P4Program &program, z3::context &z3_context) const { + // Return an error if this is a fully concrete entry. + if (IsConcrete()) { + return gutil::InvalidArgumentErrorBuilder() + << "Entry " << GetIndex() << " of table '" << GetTableName() + << "' is not symbolic."; + } + + // Get symbolic variable names. + ASSIGN_OR_RETURN(SymbolicMatchInfo match, + GetSymbolicMatchInfo(match_name, table, program)); + + // Construct and return the symbolic variables as Z3 expressions. + return SymbolicMatchVariables{ + .match_type = match.match_type, + .value = z3_context.bv_const(match.value_variable_name.c_str(), + match.bitwidth), + .mask = + z3_context.bv_const(match.mask_variable_name.c_str(), match.bitwidth), + }; +} + +absl::StatusOr TableEntry::GetActionInvocation( + absl::string_view action_name, const ir::Table &table, + z3::context &z3_context) const { + // Return an error if this is a fully concrete entry. + if (IsConcrete()) { + return gutil::InvalidArgumentErrorBuilder() + << "Entry " << GetIndex() << " of table '" << GetTableName() + << "' is not symbolic."; + } + + // Get symbolic variable names. + ASSIGN_OR_RETURN(std::string variable_name, + GetActionChoiceSymbolicVariableName(action_name, table)); + + // Construct and return the symbolic variable as a Z3 expression. + return z3_context.bool_const(variable_name.c_str()); +} + +absl::StatusOr TableEntry::GetActionParameter( + absl::string_view param_name, const ir::Action &action, + const ir::Table &table, z3::context &z3_context) const { + // Return an error if this is a fully concrete entry. + if (IsConcrete()) { + return gutil::InvalidArgumentErrorBuilder() + << "Entry " << GetIndex() << " of table '" << GetTableName() + << "' is not symbolic."; + } + + // Get symbolic variable names. + ASSIGN_OR_RETURN(auto action_param, + GetSymbolicActionParameterInfo(param_name, action, table)); + + // Construct and return the symbolic variable as a Z3 expression. + return z3_context.bv_const(action_param.variable_name.c_str(), + action_param.bitwidth); +} + +} // namespace p4_symbolic::symbolic diff --git a/p4_symbolic/symbolic/table_entry.h b/p4_symbolic/symbolic/table_entry.h new file mode 100644 index 00000000..8eb8a98c --- /dev/null +++ b/p4_symbolic/symbolic/table_entry.h @@ -0,0 +1,129 @@ +// Copyright 2024 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. + +#ifndef PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_ +#define PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_ + +#include +#include + +#include "absl/container/btree_map.h" +#include "absl/status/statusor.h" +#include "absl/strings/string_view.h" +#include "p4/config/v1/p4info.pb.h" +#include "p4_pdpi/ir.pb.h" +#include "p4_symbolic/ir/ir.pb.h" +#include "z3++.h" + +namespace p4_symbolic::symbolic { + +// Contains the symbolic variables of a symbolic match of a table entry. +struct SymbolicMatchVariables { + p4::config::v1::MatchField::MatchType match_type; + z3::expr value; + z3::expr mask; +}; + +// Contains the symbolic variable names and bit-width of the symbolic match of a +// table entry. +struct SymbolicMatchInfo { + p4::config::v1::MatchField::MatchType match_type; + int bitwidth; + // Value variable name of the symbolic match. It looks like + // "_entry____value". + std::string value_variable_name; + // Value variable name of the symbolic match. It looks like + // "_entry____mask". + std::string mask_variable_name; +}; + +// Contains the symbolic variable name and bit-width of the symbolic action +// parameter of a table entry. +struct SymbolicActionParameterInfo { + // Variable name of the symbolic action parameter. It looks like + // "_entry___". + std::string variable_name; + int bitwidth; +}; + +class TableEntry { + public: + // Constructs a table entry object, where the `index` is the original index of + // the entry in the table and the `ir_entry` is the entry in P4-Symbolic IR. + TableEntry(int index, ir::TableEntry ir_entry); + + // Returns the original index of the entry as installed in the table. + int GetIndex() const; + // Returns true if the IR entry has a concrete entry. + bool IsConcrete() const; + // Returns true if the IR entry has a symbolic entry. + bool IsSymbolic() const; + // Returns the table name of the table to which the entry belongs. + const std::string &GetTableName() const; + // Returns the P4-Symbolic IR table entry. + const ir::TableEntry &GetP4SymbolicIrTableEntry() const; + // Returns the PDPI IR table entry, which may represent a concrete entry or + // the skeleton for a symbolic entry. + // Note: If symbolic, the returned entry may not be a well-formed PDPI IR + // entry. See p4_symbolic/ir/ir.proto for details. + const pdpi::IrTableEntry &GetPdpiIrTableEntry() const; + + // Returns the symbolic variables of the symbolic match with the given + // `match_name`. Returns an error if this is not a symbolic entry. + absl::StatusOr GetMatchValues( + absl::string_view match_name, const ir::Table &table, + const ir::P4Program &program, z3::context &z3_context) const; + // Returns the symbolic variable of the action invocation with the given + // `action_name`. Returns an error if this is not a symbolic entry. + absl::StatusOr GetActionInvocation(absl::string_view action_name, + const ir::Table &table, + z3::context &z3_context) const; + // Returns the symbolic variable of the action parameter with the given + // `param_name` in the `action`. Returns an error if this is not a symbolic + // entry. + absl::StatusOr GetActionParameter(absl::string_view param_name, + const ir::Action &action, + const ir::Table &table, + z3::context &z3_context) const; + + private: + int index_; // The original index of the entry in the table. + ir::TableEntry ir_entry_; // Entry in P4-Symbolic IR. + + // Returns the symbolic variable names, the bit-width, and the match type of + // the symbolic match with the given `match_name`. An error is returned if + // this is not a symbolic entry, or if the given `match_name` is not found in + // the table definition. + absl::StatusOr GetSymbolicMatchInfo( + absl::string_view match_name, const ir::Table &table, + const ir::P4Program &program) const; + // Returns the symbolic variable name of the action invocation with the given + // `action_name`. An error is returned if this is not a symbolic entry, or if + // the given `action_name` is not found in the table definition. + absl::StatusOr GetActionChoiceSymbolicVariableName( + absl::string_view action_name, const ir::Table &table) const; + // Returns the symbolic variable name and the bit-width of the action + // parameter with the given `action_name` and `param_name`. An error is + // returned if this is not a symbolic entry, or if the given `action_name` and + // `param_name` are not found in the table and action definition. + absl::StatusOr GetSymbolicActionParameterInfo( + absl::string_view param_name, const ir::Action &action, + const ir::Table &table) const; +}; + +using TableEntries = absl::btree_map>; + +} // namespace p4_symbolic::symbolic + +#endif // PINS_P4_SYMBOLIC_SYMBOLIC_TABLE_ENTRY_H_ diff --git a/p4_symbolic/symbolic/table_entry_test.cc b/p4_symbolic/symbolic/table_entry_test.cc new file mode 100644 index 00000000..89614811 --- /dev/null +++ b/p4_symbolic/symbolic/table_entry_test.cc @@ -0,0 +1,417 @@ +// Copyright 2024 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/util.cc b/p4_symbolic/symbolic/util.cc index 94fc2f86..63c5ca70 100644 --- a/p4_symbolic/symbolic/util.cc +++ b/p4_symbolic/symbolic/util.cc @@ -17,17 +17,25 @@ #include "p4_symbolic/symbolic/util.h" #include +#include +#include "absl/container/btree_map.h" #include "absl/status/status.h" +#include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" #include "absl/strings/str_split.h" #include "absl/strings/string_view.h" #include "absl/strings/substitute.h" #include "glog/logging.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/operators.h" #include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/values.h" #include "p4_symbolic/z3_util.h" +#include "z3++.h" namespace p4_symbolic { namespace symbolic { @@ -35,33 +43,27 @@ namespace util { namespace { -// Extract the header field definition of a `field_ref` from the given P4 -// `program`. +// Extracts the header field definition based on the given `header_name` and +// `field_name` from the given P4 `program`. absl::StatusOr GetFieldDefinition( - const ir::P4Program &program, absl::string_view field_ref) { - // Split the field reference into header and field names. - std::vector split = absl::StrSplit(field_ref, '.'); - if (split.size() != 2) { - return absl::InvalidArgumentError( - absl::Substitute("Expected
. got '$0'", field_ref)); - } - const std::string &header_name = split[0]; - const std::string &field_name = split[1]; - + const ir::P4Program &program, absl::string_view header_name, + absl::string_view field_name) { // Extract the header definition from the program. - if (!program.headers().contains(header_name)) { - return absl::InvalidArgumentError( - absl::Substitute("Unexpected header instance'$0'", header_name)); + auto header_it = program.headers().find(header_name); + if (header_it == program.headers().end()) { + return gutil::InvalidArgumentErrorBuilder() + << "Unexpected header instance '" << header_name << "'"; } - const p4_symbolic::ir::HeaderType &header_def = - program.headers().at(header_name); + const p4_symbolic::ir::HeaderType &header = header_it->second; // Extract the field definition from the header definition. - if (!header_def.fields().contains(field_name)) { - return absl::InvalidArgumentError(absl::Substitute( - "Unexpected field'$0' in header '$1'", field_name, header_name)); + auto field_it = header.fields().find(field_name); + if (field_it == header.fields().end()) { + return gutil::InvalidArgumentErrorBuilder() + << "Unexpected field '" << field_name << "' in header '" + << header_name << "'"; } - return header_def.fields().at(field_name); + return field_it->second; } } // namespace @@ -74,19 +76,19 @@ absl::StatusOr> FreeSymbolicHeaders( // variable for every field in every header instance. absl::btree_map symbolic_headers; for (const auto &[header_name, header_type] : Ordered(headers)) { - // Pseudo fields used in P4-Symbolic indicating the state of the header. + // Pseudo fields (`$valid$`, `$extracted$`) in P4-Symbolic indicate the + // state of the header. Here we initialize the pseudo fields of each header + // to symbolic variables. for (const auto &pseudo_field_name : {kValidPseudoField, kExtractedPseudoField}) { std::string field_name = absl::StrFormat("%s.%s", header_name, pseudo_field_name); - // TODO: Set these fields to false while removing SAI parser - // code. - z3::expr free_expr = z3_context.bool_const(field_name.c_str()); - symbolic_headers.insert({field_name, free_expr}); + z3::expr free_variable = z3_context.bool_const(field_name.c_str()); + symbolic_headers.insert({field_name, free_variable}); } // Regular fields defined in the p4 program or v1model. - for (const auto &[field_name, field] : header_type.fields()) { + for (const auto &[field_name, field] : Ordered(header_type.fields())) { if (field.signed_()) { return absl::UnimplementedError( "Negative header fields are not supported"); @@ -100,7 +102,7 @@ absl::StatusOr> FreeSymbolicHeaders( } } - // Initialize pseudo header fields. + // Initialize packet-wide pseudo fields to false. symbolic_headers.insert({ std::string(kGotClonedPseudoField), z3_context.bool_val(false), @@ -238,14 +240,27 @@ absl::StatusOr MergeDisjointTableMatches( return merged; } -absl::StatusOr GetFieldBitwidth(absl::string_view field_name, +absl::StatusOr GetFieldBitwidth(absl::string_view qualified_field_name, + const ir::P4Program &program) { + // Split the fully qualified field name into header and field names. + std::vector split = absl::StrSplit(qualified_field_name, '.'); + if (split.size() != 2) { + return absl::InvalidArgumentError(absl::Substitute( + "Expected
. got '$0'", qualified_field_name)); + } + return GetFieldBitwidth(/*header_name=*/split[0], /*field_name=*/split[1], + program); +} + +absl::StatusOr GetFieldBitwidth(absl::string_view header_name, + absl::string_view field_name, const ir::P4Program &program) { - if (absl::EndsWith(field_name, symbolic::kValidPseudoField) || - absl::EndsWith(field_name, symbolic::kExtractedPseudoField)) { + if (field_name == symbolic::kValidPseudoField || + field_name == symbolic::kExtractedPseudoField) { return 1; } else { ASSIGN_OR_RETURN(const ir::HeaderField field_definition, - GetFieldDefinition(program, field_name)); + GetFieldDefinition(program, header_name, field_name)); return field_definition.bitwidth(); } } diff --git a/p4_symbolic/symbolic/util.h b/p4_symbolic/symbolic/util.h index 2dd6b661..fdf42cbb 100644 --- a/p4_symbolic/symbolic/util.h +++ b/p4_symbolic/symbolic/util.h @@ -63,9 +63,15 @@ absl::StatusOr MergeDisjointTableMatches(const SymbolicTableMatches &lhs, const SymbolicTableMatches &rhs); -// Extracts the bit-width of the field with name `field_name` in the given -// `program`. -absl::StatusOr GetFieldBitwidth(absl::string_view field_name, +// Extracts the bit-width of the field with the `qualified_field_name` (i.e., +// `
.`) in the given `program`. +absl::StatusOr GetFieldBitwidth(absl::string_view qualified_field_name, + const ir::P4Program &program); + +// Extracts the bit-width of the field with the name `field_name` of header +// `header_name` in the given `program`. +absl::StatusOr GetFieldBitwidth(absl::string_view header_name, + absl::string_view field_name, const ir::P4Program &program); // Returns the full valid field name of the given header. diff --git a/p4_symbolic/symbolic/v1model.cc b/p4_symbolic/symbolic/v1model.cc index 94015842..5bfe5efc 100644 --- a/p4_symbolic/symbolic/v1model.cc +++ b/p4_symbolic/symbolic/v1model.cc @@ -14,13 +14,26 @@ #include "p4_symbolic/symbolic/v1model.h" +#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" +#include "p4_symbolic/symbolic/v1model_intrinsic.h" #include "z3++.h" namespace p4_symbolic { @@ -29,6 +42,68 @@ namespace v1model { namespace { +// Initializes standard metadata fields to zero, except for `ingress_port`, +// `egress_port`, and `packet_length`. +absl::Status InitializeStandardMetadata(const ir::P4Program &program, + SymbolicPerPacketState &headers, + z3::context &z3_context) { + // Check if the standard metadata header exists. + auto it = program.headers().find(kStandardMetadataHeaderName); + if (it == program.headers().end()) { + return gutil::InternalErrorBuilder() + << "Header '" << kStandardMetadataHeaderName + << "' not found in P4 program."; + } + + const google::protobuf::Map + &standard_metadata_fields = it->second.fields(); + + // List of standard metadata fields to be initialized to zero. See + // https://github.com/p4lang/p4c/blob/main/p4include/v1model.p4 for the full + // list of fields. + static constexpr std::array kFieldsToBeInitialized = { + // The ingress port should not be fixed. + // "ingress_port", + "egress_spec", + // TODO: Whenever `egress_port` is initialized to zero, + // `packet_util_production_test` fails. It would be helpful to understand + // why that's the case. + // "egress_port", + "instance_type", + // TODO: Packet length depends on the validity of headers. + // "packet_length", + "enq_timestamp", + "enq_qdepth", + "deq_timedelta", + "deq_qdepth", + "ingress_global_timestamp", + "egress_global_timestamp", + "mcast_grp", + "egress_rid", + "checksum_error", + "parser_error", + "priority", + }; + + // Initialize the listed standard metadata fields to zero. + for (const absl::string_view field_name : kFieldsToBeInitialized) { + auto it = standard_metadata_fields.find(field_name); + if (it == standard_metadata_fields.end()) { + return gutil::InternalErrorBuilder() + << "Field '" << field_name << "' not found in standard metadata."; + } + + std::string field_full_name = + absl::StrFormat("%s.%s", kStandardMetadataHeaderName, field_name); + z3::expr zero = z3_context.bv_val( + (field_name == "instance_type" ? PKT_INSTANCE_TYPE_NORMAL : 0), + it->second.bitwidth()); + RETURN_IF_ERROR(headers.UnguardedSet(field_full_name, zero)); + } + + return absl::OkStatus(); +} + absl::Status CheckPhysicalPortsConformanceToV1Model( const std::vector &physical_ports) { for (const int port : physical_ports) { @@ -82,7 +157,8 @@ z3::expr EgressSpecDroppedValue(z3::context &z3_context) { absl::Status InitializeIngressHeaders(const ir::P4Program &program, SymbolicPerPacketState &ingress_headers, z3::context &z3_context) { - // TODO: Consider initializing all metadata fields to 0. + RETURN_IF_ERROR( + InitializeStandardMetadata(program, ingress_headers, z3_context)); // Set the `$valid$` and `$extracted$` fields of all headers to false. const z3::expr false_expr = z3_context.bool_val(false); @@ -93,18 +169,13 @@ absl::Status InitializeIngressHeaders(const ir::P4Program &program, header_name, kExtractedPseudoField, false_expr)); } - // Set the `standard_metadata.parser_error` field to error.NoError. - ASSIGN_OR_RETURN(z3::expr no_error, parser::GetErrorCodeExpression( - program, "NoError", z3_context)); - RETURN_IF_ERROR(ingress_headers.UnguardedSet(kParserErrorField, no_error)); - 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)); @@ -113,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 @@ -125,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)); @@ -150,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)); @@ -167,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 237a3ad7..46d9cdf1 100644 --- a/p4_symbolic/symbolic/v1model.h +++ b/p4_symbolic/symbolic/v1model.h @@ -17,21 +17,35 @@ #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 { namespace symbolic { namespace v1model { +// Standard metadata header name. +constexpr absl::string_view kStandardMetadataHeaderName = "standard_metadata"; + +// 32-bit bit-vector field in standard metadata indicating whether there is a +// parser error. The error code is defined in core.p4 and can be extended by the +// P4 program. 0 means no error. +constexpr absl::string_view kParserErrorField = + "standard_metadata.parser_error"; + // V1model's `mark_to_drop` primitive sets the `egress_spec` field to // `kDropPort` to indicate the packet should be dropped at the end of // ingress/egress processing. See v1model.p4 for details. z3::expr EgressSpecDroppedValue(z3::context &z3_context); // Initializes the ingress headers to appropriate values. +// Here we initialize all standard metadata fields to zero for the ingress +// packet. Local (user) metadata fields are intentionally left uninitialized +// to align with the standard. absl::Status InitializeIngressHeaders(const ir::P4Program &program, SymbolicPerPacketState &ingress_headers, z3::context &z3_context); @@ -39,10 +53,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/v1model_intrinsic.h b/p4_symbolic/symbolic/v1model_intrinsic.h new file mode 100644 index 00000000..ee88c185 --- /dev/null +++ b/p4_symbolic/symbolic/v1model_intrinsic.h @@ -0,0 +1,33 @@ +// Copyright 2024 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. + +#ifndef P4_SYMBOLIC_SYMBOLIC_V1MODEL_INTRINSIC_H_ +#define P4_SYMBOLIC_SYMBOLIC_V1MODEL_INTRINSIC_H_ + +namespace p4_symbolic::symbolic::v1model { + +// Possible values of the v1model `standard_metadata_t` field `instance_type` in +// BMv2. The semantics of these values is explained here: +// https://github.com/p4lang/behavioral-model/blob/main/docs/simple_switch.md +#define PKT_INSTANCE_TYPE_NORMAL 0 +#define PKT_INSTANCE_TYPE_INGRESS_CLONE 1 +#define PKT_INSTANCE_TYPE_EGRESS_CLONE 2 +#define PKT_INSTANCE_TYPE_COALESCED 3 +#define PKT_INSTANCE_TYPE_INGRESS_RECIRC 4 +#define PKT_INSTANCE_TYPE_REPLICATION 5 +#define PKT_INSTANCE_TYPE_RESUBMIT 6 + +} // namespace p4_symbolic::symbolic::v1model + +#endif // PINS_P4_SYMBOLIC_SYMBOLIC_V1MODEL_INTRINSIC_H_ 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", diff --git a/tests/integration/system/alpm_miss_counter_tests.cc b/tests/integration/system/alpm_miss_counter_tests.cc index 3dd087d0..252bb41c 100644 --- a/tests/integration/system/alpm_miss_counter_tests.cc +++ b/tests/integration/system/alpm_miss_counter_tests.cc @@ -266,7 +266,7 @@ absl::StatusOr GetAlpmMissStat(gnmi::gNMI::StubInterface& gnmi_stub) { return GetGnmiStats(gnmi_stub, state_path, resp_parse_str); } -absl::StatusOr IsPlatformTypeBrixia( +absl::StatusOr IsPlatformTypeExperimental( gnmi::gNMI::StubInterface& gnmi_stub) { std::string state_path = "components/component[name=chassis]/chassis/state/platform"; @@ -276,7 +276,7 @@ absl::StatusOr IsPlatformTypeBrixia( std::string state_response, GetGnmiStatePathInfo(&gnmi_stub, state_path, resp_parse_str)); - return absl::StrContains(state_response, "BRIXIA"); + return absl::StrContains(state_response, "Experimental"); } // Control switch sends packets to SUT. @@ -352,10 +352,10 @@ TEST_P(AlpmMissCountersTest, Ipv4AlpmRouteHit) { ASSERT_NO_FATAL_FAILURE( InitializeTestEnvironment("d9716769-9ca5-477b-b53b-1b96fce60e13")); - ASSERT_OK_AND_ASSIGN(bool is_sut_brixia, - IsPlatformTypeBrixia(*sut_gnmi_stub_)); - if (!is_sut_brixia) { - GTEST_SKIP() << "Test is not supported on non-Brixia SUT."; + ASSERT_OK_AND_ASSIGN(bool is_sut_Experimental, + IsPlatformTypeExperimental(*sut_gnmi_stub_)); + if (!is_sut_Experimental) { + GTEST_SKIP() << "Test is not supported on non-Experimental SUT."; } if (!generic_testbed_->ControlDevice().SupportsSendPacket()) { GTEST_SKIP() << "Control device does not support SendPacket"; @@ -418,10 +418,10 @@ TEST_P(AlpmMissCountersTest, Ipv4AlpmRouteMiss) { ASSERT_NO_FATAL_FAILURE( InitializeTestEnvironment("07dda215-ad21-4c25-b89e-1128b3806c27")); - ASSERT_OK_AND_ASSIGN(bool is_sut_brixia, - IsPlatformTypeBrixia(*sut_gnmi_stub_)); - if (!is_sut_brixia) { - GTEST_SKIP() << "Test is not supported on non-Brixia SUT."; + ASSERT_OK_AND_ASSIGN(bool is_sut_Experimental, + IsPlatformTypeExperimental(*sut_gnmi_stub_)); + if (!is_sut_Experimental) { + GTEST_SKIP() << "Test is not supported on non-Experimental SUT."; } if (!generic_testbed_->ControlDevice().SupportsSendPacket()) { GTEST_SKIP() << "Control device does not support SendPacket"; @@ -486,10 +486,10 @@ TEST_P(AlpmMissCountersTest, Ipv6AlpmRouteHit) { ASSERT_NO_FATAL_FAILURE( InitializeTestEnvironment("552ebd5d-fa98-4298-b4ef-efab286bcc89")); - ASSERT_OK_AND_ASSIGN(bool is_sut_brixia, - IsPlatformTypeBrixia(*sut_gnmi_stub_)); - if (!is_sut_brixia) { - GTEST_SKIP() << "Test is not supported on non-Brixia SUT."; + ASSERT_OK_AND_ASSIGN(bool is_sut_Experimental, + IsPlatformTypeExperimental(*sut_gnmi_stub_)); + if (!is_sut_Experimental) { + GTEST_SKIP() << "Test is not supported on non-Experimental SUT."; } if (!generic_testbed_->ControlDevice().SupportsSendPacket()) { GTEST_SKIP() << "Control device does not support SendPacket"; @@ -552,10 +552,10 @@ TEST_P(AlpmMissCountersTest, Ipv6AlpmRouteMiss) { ASSERT_NO_FATAL_FAILURE( InitializeTestEnvironment("b8c1ba7f-a8ca-429b-bb8b-9fc479fc7e71")); - ASSERT_OK_AND_ASSIGN(bool is_sut_brixia, - IsPlatformTypeBrixia(*sut_gnmi_stub_)); - if (!is_sut_brixia) { - GTEST_SKIP() << "Test is not supported on non-Brixia SUT."; + ASSERT_OK_AND_ASSIGN(bool is_sut_Experimental, + IsPlatformTypeExperimental(*sut_gnmi_stub_)); + if (!is_sut_Experimental) { + GTEST_SKIP() << "Test is not supported on non-Experimental SUT."; } if (!generic_testbed_->ControlDevice().SupportsSendPacket()) { GTEST_SKIP() << "Control device does not support SendPacket";