From 8bb7b076afd98e25a44831da40e62b718dc33d46 Mon Sep 17 00:00:00 2001 From: smolkaj Date: Tue, 20 Jul 2021 10:00:49 -0700 Subject: [PATCH] [p4-symbolic] Eliminate extremely long variable names for action selector variables. Eliminate bug in detecting unsupported scenario (conditional on table match result) Eliminate non-determinism in EvaluateTableEntryCondition. Add test for output determinism.Update hard-coded SAI parser constraint to reflect the updated P4 code.Decrease the number of runs for determinism check. Define kDefaultActionEntryIndex. Fix typo. --- p4_symbolic/symbolic/BUILD.bazel | 3 +- p4_symbolic/symbolic/table.cc | 60 ++++++++++++++++++-------------- p4_symbolic/symbolic/table.h | 3 ++ p4_symbolic/z3_util.cc | 8 ++++- p4_symbolic/z3_util.h | 8 +++-- 5 files changed, 50 insertions(+), 32 deletions(-) diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel index b601b1f2..81fa9701 100644 --- a/p4_symbolic/symbolic/BUILD.bazel +++ b/p4_symbolic/symbolic/BUILD.bazel @@ -46,7 +46,8 @@ cc_library( deps = [ "//gutil:status", "//p4_pdpi:ir_cc_proto", - "//p4_pdpi/netaddr:ipv4_address", + "//p4_pdpi/internal:ordered_map", + "//p4_pdpi/netaddr:ipv4_address", "//p4_pdpi/netaddr:ipv6_address", "//p4_pdpi/netaddr:mac_address", "//p4_pdpi/utils:ir", diff --git a/p4_symbolic/symbolic/table.cc b/p4_symbolic/symbolic/table.cc index effe5f8d..66e36000 100644 --- a/p4_symbolic/symbolic/table.cc +++ b/p4_symbolic/symbolic/table.cc @@ -30,6 +30,7 @@ #include "absl/types/span.h" #include "gutil/status.h" #include "p4/config/v1/p4info.pb.h" +#include "p4_pdpi/internal/ordered_map.h" #include "p4_pdpi/ir.pb.h" #include "p4_symbolic/symbolic/action.h" #include "p4_symbolic/symbolic/operators.h" @@ -77,7 +78,7 @@ int FindMatchWithName(const pdpi::IrTableEntry &entry, // We return the old index so that Symbolic and Concrete TableMatches are // set up against the indices as they appear in the input table entries array, // and not the sorted array. -std::vector> SortEntries( +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 @@ -106,27 +107,26 @@ std::vector> SortEntries( } // The output array. - std::vector> sorted_entries; - for (size_t i = 0; i < entries.size(); i++) { + std::vector> sorted_entries; + for (int i = 0; i < entries.size(); i++) { const pdpi::IrTableEntry &entry = entries.at(i); sorted_entries.push_back(std::make_pair(i, entry)); } // The sort comparator depends on the match types. - std::function &, - const std::pair &)> + std::function &, + const std::pair &)> comparator; if (has_ternary) { // Sort by explicit priority. - comparator = [](const std::pair &entry1, - const std::pair &entry2) { + comparator = [](const std::pair &entry1, + const std::pair &entry2) { return entry1.second.priority() > entry2.second.priority(); }; } else if (lpm_key.has_value()) { // Sort by prefix length. - comparator = [lpm_key]( - const std::pair &entry1, - const std::pair &entry2) { + comparator = [lpm_key](const std::pair &entry1, + const std::pair &entry2) { auto is_lpm_match = [=](const pdpi::IrMatch &match) -> bool { return match.name() == *lpm_key; }; @@ -235,8 +235,13 @@ absl::StatusOr EvaluateTableEntryCondition( z3::expr condition_expression = Z3Context().bool_val(true); const google::protobuf::Map &match_to_fields = table.table_implementation().match_name_to_field(); - for (const auto &[name, match_fields] : - table.table_definition().match_fields_by_name()) { + + // It is desirable for P4Symbolic to produce deterministic outputs. Therefore, + // all containers need to be traversed in a deterministic order. + const auto sorted_match_fields_by_name = + Ordered(table.table_definition().match_fields_by_name()); + + for (const auto &[name, match_fields] : sorted_match_fields_by_name) { p4::config::v1::MatchField match_definition = match_fields.match_field(); int match_field_index = FindMatchWithName(entry, name); @@ -295,7 +300,7 @@ absl::Status EvaluateSingeTableEntryAction( // Constructs a symbolic expressions that represents the action invocation // corresponding to this entry. absl::Status EvaluateTableEntryAction( - const ir::Table &table, const pdpi::IrTableEntry &entry, + const ir::Table &table, const pdpi::IrTableEntry &entry, int entry_index, const google::protobuf::Map &actions, SymbolicPerPacketState *state, values::P4RuntimeTranslator *translator, const z3::expr &guard) { @@ -312,7 +317,8 @@ absl::Status EvaluateTableEntryAction( // whose value determines which action is executed: to a first // approximation, action i is executed iff `selector == i`. std::string selector_name = - absl::StrCat("action selector for ", entry.DebugString()); + absl::StrFormat("action selector for entry #%d of table '%s'", + entry_index, entry.table_name()); z3::expr selector = Z3Context().int_const(selector_name.c_str()); z3::expr unselected = Z3Context().bool_val(true); for (int i = 0; i < action_set.size(); ++i) { @@ -345,7 +351,7 @@ absl::StatusOr EvaluateTable( 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 = + std::vector> sorted_entries = SortEntries(table, entries); // The table semantically is just a bunch of if conditions, one per // table entry, we construct this big if-elseif-...-else symbolically. @@ -431,16 +437,17 @@ absl::StatusOr EvaluateTable( } // Start with the default entry - z3::expr match_index = Z3Context().int_val(-1); - RETURN_IF_ERROR(EvaluateTableEntryAction( - table, default_entry, data_plane.program.actions(), state, translator, - default_entry_assignment_guard)); + z3::expr match_index = Z3Context().int_val(kDefaultActionEntryIndex); + RETURN_IF_ERROR( + EvaluateTableEntryAction(table, default_entry, kDefaultActionEntryIndex, + data_plane.program.actions(), state, translator, + default_entry_assignment_guard)); // Continue evaluating each table entry in reverse priority for (int row = sorted_entries.size() - 1; row >= 0; row--) { - size_t old_index = sorted_entries.at(row).first; + int old_index = sorted_entries.at(row).first; const pdpi::IrTableEntry &entry = sorted_entries.at(row).second; - z3::expr row_symbol = Z3Context().int_val(static_cast(old_index)); + z3::expr row_symbol = Z3Context().int_val(old_index); // The condition used in the big if_else_then construct. ASSIGN_OR_RETURN(z3::expr entry_match, @@ -450,9 +457,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, data_plane.program.actions(), - state, translator, entry_assignment_guard)); + RETURN_IF_ERROR(EvaluateTableEntryAction( + table, entry, old_index, data_plane.program.actions(), state, + translator, entry_assignment_guard)); } // This table has been completely evaluated, the result of the evaluation @@ -476,9 +483,8 @@ absl::StatusOr EvaluateTable( table.table_implementation().action_to_next_control()) { if (first) { next_control = control; - continue; - } - if (next_control != control) { + first = false; + } else if (next_control != control) { return absl::UnimplementedError(absl::StrCat( "Table \"", table_name, "\" invokes different control constructs based on matched actions.")); diff --git a/p4_symbolic/symbolic/table.h b/p4_symbolic/symbolic/table.h index 94b27423..09def04b 100644 --- a/p4_symbolic/symbolic/table.h +++ b/p4_symbolic/symbolic/table.h @@ -36,6 +36,9 @@ namespace p4_symbolic { namespace symbolic { namespace table { +// P4-Symbolic models the default action as an entry with index -1. +constexpr int kDefaultActionEntryIndex = -1; + absl::StatusOr EvaluateTable( const Dataplane &data_plane, const ir::Table &table, const std::vector &entries, diff --git a/p4_symbolic/z3_util.cc b/p4_symbolic/z3_util.cc index 391627a7..cccb0174 100644 --- a/p4_symbolic/z3_util.cc +++ b/p4_symbolic/z3_util.cc @@ -8,8 +8,14 @@ namespace p4_symbolic { -z3::context& Z3Context() { +z3::context& Z3Context(bool renew) { static z3::context* z3_context = new z3::context(); + + if (renew) { + delete z3_context; + z3_context = new z3::context(); + } + return *z3_context; } diff --git a/p4_symbolic/z3_util.h b/p4_symbolic/z3_util.h index 16a2179b..59a8d1c9 100644 --- a/p4_symbolic/z3_util.h +++ b/p4_symbolic/z3_util.h @@ -11,9 +11,11 @@ namespace p4_symbolic { -// Global z3::context used for creating symbolic expressions during symbolic -// evaluation. -z3::context& Z3Context(); +// Returns the global z3::context used for creating symbolic expressions during +// symbolic evaluation. If parameter `renew` is set to true, it deletes the +// older context and returns a new one. +// TODO: `renew` is a workaround for using a global context. +z3::context& Z3Context(bool renew = false); // -- Evaluation ---------------------------------------------------------------