[P4Symbolic] Add support for string formatted optional matches.

PiperOrigin-RevId: 428140974
sonic-net · Oct 15, 2024 · a7335c6 · a7335c6
1 parent 658a984
commit a7335c6
Show file tree

Hide file tree

Showing 17 changed files with 1,580 additions and 47 deletions.
diff --git a/p4_symbolic/BUILD.bazel b/p4_symbolic/BUILD.bazel
@@ -72,3 +72,12 @@ cc_library(
         "@com_google_absl//absl/strings",
     ],
 )
+
+cc_test(
+    name = "z3_util_test",
+    srcs = ["z3_util_test.cc"],
+    deps = [
+        ":z3_util",
+        "@com_google_googletest//:gtest_main",
+    ],
+)
diff --git a/p4_symbolic/main.cc b/p4_symbolic/main.cc
@@ -42,6 +42,7 @@ ABSL_FLAG(std::string, entries, "",
           "if the input p4 program contains no (explicit) tables for which "
           "entries are needed.");
 ABSL_FLAG(std::string, debug, "", "Dump the SMT program for debugging");
+ABSL_FLAG(int, port_count, 2, "Number of used ports (numbered 0 to N-1)");
 ABSL_FLAG(bool, hardcoded_parser, true,
           "Use the hardcoded parser during symbolic evaluation");
 
@@ -53,6 +54,7 @@ absl::Status ParseAndEvaluate() {
   const std::string &bmv2_path = absl::GetFlag(FLAGS_bmv2);
   const std::string &entries_path = absl::GetFlag(FLAGS_entries);
   const std::string &debug_path = absl::GetFlag(FLAGS_debug);
+  const int port_count = absl::GetFlag(FLAGS_port_count);
   bool hardcoded_parser = absl::GetFlag(FLAGS_hardcoded_parser);
 
   RET_CHECK(!p4info_path.empty());
@@ -63,11 +65,14 @@ absl::Status ParseAndEvaluate() {
       p4_symbolic::symbolic::Dataplane dataplane,
       p4_symbolic::ParseToIr(bmv2_path, p4info_path, entries_path));
 
+  // Generate port list.
+  std::vector<int> physical_ports(port_count);
+  for (int i = 0; i < port_count; i++) physical_ports[i] = i;
+
   // Evaluate program symbolically.
   ASSIGN_OR_RETURN(
       const std::unique_ptr<p4_symbolic::symbolic::SolverState> &solver_state,
-      p4_symbolic::symbolic::EvaluateP4Pipeline(dataplane,
-                                                std::vector<int>{0, 1}));
+      p4_symbolic::symbolic::EvaluateP4Pipeline(dataplane, physical_ports));
   // Add constraints for parser.
   if (hardcoded_parser) {
     ASSIGN_OR_RETURN(
@@ -151,6 +156,14 @@ absl::Status ParseAndEvaluate() {
                            "scalars.userMetadata.vrf_is_valid")
                     << std::endl;
         }
+        // Custom metadata field defined in testdata/string-optional/program.p4
+        if (packet_option.value().egress_headers.contains(
+                "scalars.userMetadata.string_field")) {
+          std::cout << "\tscalars.userMetadata.string_field = "
+                    << packet_option.value().egress_headers.at(
+                           "scalars.userMetadata.string_field")
+                    << std::endl;
+        }
       } else {
         std::cout << "Cannot find solution!" << std::endl;
       }

diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel
@@ -103,3 +103,26 @@ end_to_end_test(
     smt_golden_file = "expected/basic.smt2",
     table_entries = "//p4_symbolic/testdata:ipv4-routing/entries.pb.txt",
 )
+
+end_to_end_test(
+    name = "string_optional_test",
+    output_golden_file = "expected/string_optional.txt",
+    p4_program = "//p4_symbolic/testdata:string-optional/program.p4",
+    port_count = 3,
+    smt_golden_file = "expected/string_optional.smt2",
+    table_entries = "//p4_symbolic/testdata:string-optional/entries.pb.txt",
+)
+
+cc_test(
+    name = "values_test",
+    srcs = ["values_test.cc"],
+    deps = [
+        ":symbolic",
+        "//gutil:status_matchers",
+        "//gutil:testing",
+        "//p4_pdpi:ir_cc_proto",
+        "@com_google_absl//absl/container:flat_hash_map",
+        "@com_google_absl//absl/strings",
+        "@com_google_googletest//:gtest_main",
+    ],
+)
diff --git a/p4_symbolic/symbolic/expected/string_optional.smt2 b/p4_symbolic/symbolic/expected/string_optional.smt2
diff --git a/p4_symbolic/symbolic/expected/string_optional.txt b/p4_symbolic/symbolic/expected/string_optional.txt
@@ -0,0 +1,42 @@
+Finding packet for table MyIngress.optional_match and row -1
+Cannot find solution!
+
+Finding packet for table MyIngress.optional_match and row 0
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+	scalars.userMetadata.string_field = VALUE-0
+
+Finding packet for table MyIngress.optional_match and row 1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000010
+	standard_metadata.egress_spec = #b000000001
+	scalars.userMetadata.string_field = VALUE-2
+
+Finding packet for table MyIngress.set_field_table and row -1
+Cannot find solution!
+
+Finding packet for table MyIngress.set_field_table and row 0
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000000
+	standard_metadata.egress_spec = #b000000000
+	scalars.userMetadata.string_field = VALUE-0
+
+Finding packet for table MyIngress.set_field_table and row 1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000001
+	standard_metadata.egress_spec = #b000000001
+	scalars.userMetadata.string_field = VALUE-1
+
+Finding packet for table MyIngress.set_field_table and row 2
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000010
+	standard_metadata.egress_spec = #b000000001
+	scalars.userMetadata.string_field = VALUE-2
+
+Finding packet for table tbl_program92 and row -1
+	Dropped = 0
+	standard_metadata.ingress_port = #b000000010
+	standard_metadata.egress_spec = #b000000001
+	scalars.userMetadata.string_field = VALUE-2
+