[P4_Symbolic] Create a class for symbolic table entries. (#940)

* [P4_Symbolic] Remove and modify outdated comments. Make the order of creating symbolic header fields deterministic.Initialize standard metadata fields to 0. * [P4-Symbolic] Overload `GetFieldBitwidth` to accept separate header and field names as parameters. * [P4-Symbolic] Create a class for symbolic table entries. --------- Co-authored-by: kishanps <[email protected]>
sonic-net · Jan 22, 2025 · a3f6b42 · a3f6b42
1 parent f770f30
commit a3f6b42
Show file tree

Hide file tree

Showing 26 changed files with 854 additions and 321 deletions.
diff --git 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
@@ -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
@@ -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
@@ -19,9 +19,9 @@
 #define P4_SYMBOLIC_IR_TABLE_ENTRIES_H_
 
 #include <string>
-#include <unordered_map>
 #include <vector>
 
+#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<std::string, std::vector<TableEntry>>;
+// 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<std::string, std::vector<TableEntry>>;
 
 // Returns table entries in P4-Symbolic IR, keyed by table name.
 absl::StatusOr<TableEntries> ParseTableEntries(

diff --git a/p4_symbolic/main.cc b/p4_symbolic/main.cc
@@ -18,18 +18,24 @@
 // Produces test packets that hit every row in the P4 program tables.
 
 #include <iostream>
-#include <map>
+#include <memory>
+#include <optional>
+#include <sstream>
 #include <string>
+#include <vector>
 
 #include "absl/flags/flag.h"
 #include "absl/flags/parse.h"
 #include "absl/flags/usage.h"
 #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<std::string> 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<int>(solver_state.entries.at(name).size());
+    if (solver_state.context.table_entries.count(table_name) > 0) {
+      row_count = static_cast<int>(
+          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
@@ -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<ir::TableEntry>& entries = it->second;
+    auto it = solver_state.context.table_entries.find(table_name);
+    if (it != solver_state.context.table_entries.end()) {
+      const std::vector<symbolic::TableEntry>& 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
@@ -31,6 +31,7 @@ cc_library(
         "parser.cc",
         "symbolic.cc",
         "table.cc",
+        "table_entry.cc",
         "util.cc",
         "v1model.cc",
         "values.cc",
@@ -45,6 +46,7 @@ cc_library(
         "parser.h",
         "symbolic.h",
         "table.h",
+        "table_entry.h",
         "util.h",
         "v1model.h",
         "v1model_intrinsic.h",
@@ -73,6 +75,8 @@ cc_library(
         "@com_gnu_gmp//:gmp",
         "@com_google_absl//absl/base:core_headers",
         "@com_google_absl//absl/cleanup",
+        "@com_google_absl//absl/container:btree",
+        "@com_google_absl//absl/container:flat_hash_map",
         "@com_google_absl//absl/status",
         "@com_google_absl//absl/status:statusor",
         "@com_google_absl//absl/strings",
@@ -132,12 +136,13 @@ cc_test(
     srcs = ["values_test.cc"],
     deps = [
         ":symbolic",
+        "//gutil:proto",
         "//gutil:status_matchers",
-        "//gutil:testing",
         "//p4_pdpi:ir_cc_proto",
         "//p4_symbolic:z3_util",
         "@com_github_z3prover_z3//:api",
         "@com_google_absl//absl/container:flat_hash_map",
+        "@com_google_absl//absl/status",
         "@com_google_absl//absl/strings",
         "@com_google_googletest//:gtest_main",
     ],
@@ -172,3 +177,32 @@ cc_test(
         "@com_google_googletest//:gtest_main",
     ],
 )
+
+cc_test(
+    name = "table_entry_test",
+    srcs = ["table_entry_test.cc"],
+    data = [
+        "//p4_symbolic/testdata:ipv4-routing/basic.config.json",
+        "//p4_symbolic/testdata:ipv4-routing/basic.p4info.pb.txt",
+        "//p4_symbolic/testdata:ipv4-routing/entries.pb.txt",
+    ],
+    deps = [
+        ":symbolic",
+        "//gutil:status",
+        "//gutil:status_matchers",
+        "//p4_pdpi:ir_cc_proto",
+        "//p4_symbolic:test_util",
+        "//p4_symbolic/ir",
+        "//p4_symbolic/ir:ir_cc_proto",
+        "//p4_symbolic/ir:parser",
+        "//p4_symbolic/ir:table_entries",
+        "@com_github_p4lang_p4runtime//:p4info_cc_proto",
+        "@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
+        "@com_github_z3prover_z3//:api",
+        "@com_google_absl//absl/status",
+        "@com_google_absl//absl/status:statusor",
+        "@com_google_absl//absl/strings",
+        "@com_google_googletest//:gtest_main",
+        "@com_google_protobuf//:protobuf",
+    ],
+)
diff --git a/p4_symbolic/symbolic/action.cc b/p4_symbolic/symbolic/action.cc
@@ -14,18 +14,27 @@
 
 #include "p4_symbolic/symbolic/action.h"
 
+#include <string>
 #include <vector>
 
 #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<z3::expr> 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
@@ -22,11 +22,13 @@
 #include <string>
 #include <unordered_map>
 
+#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
@@ -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 <string>
+
+#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<SymbolicTableMatches> 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<SymbolicTableMatches> 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<SymbolicTableMatches> 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.