[P4_Symbolic] Create symbolic variables and add constraints for symbolic table entries.

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",
     ],
 )
 

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",

p4_symbolic/ir/ir.proto

@@ -512,6 +512,9 @@ message SymbolicTableEntry {
   //     https://p4.org/p4-spec/p4runtime/v1.3.0/P4Runtime-Spec.html#sec-match-format
   //   - To specify a symbolic match, provide a concrete match name without any
   //     values.
+  //   - For the prefix lengths in symbolic LPM matches, any negative value
+  //     denotes a symbolic prefix length and a non-negative value represents a
+  //     concrete prefix length value.
   //   - The `priority` must be concrete. It must be strictly positive if there
   //     are range, ternary, or optional matches, and must be zero if there are
   //     only LPM or exact matches.
@@ -522,6 +525,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.

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(

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);

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(

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",
+    ],
+)

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();

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