[P4_Symbolic] Output concrete solutions to a file instead of standard…

… output. (#920) * [P4-Symbolic] Use generic deparser to extract input/output packets * [P4-Symbolic] Use p4-symbolic's test data instead of SAI P4 for deparser tests. * [P4-Symbolic] Move IR parser to `ir/`. Simplify IR parser API. Remove unused IR pdpi_driver. Remove hard-coded SAI parser. Remove EvaluateSaiPipeline. Refactor SAI-specific code. * [P4-Symbolic] Remove dependencies on SAI fields. * [P4-Symbolic] Add non-SAI tests for the generic deparser. Output concrete solutions to a file instead of standard output. --------- Co-authored-by: kishanps <[email protected]>
sonic-net · Jan 7, 2025 · 6051add · 6051add
1 parent 548e089
commit 6051add
Show file tree

Hide file tree

Showing 9 changed files with 296 additions and 117 deletions.
diff --git a/p4_symbolic/BUILD.bazel b/p4_symbolic/BUILD.bazel
@@ -27,7 +27,9 @@ cc_binary(
     deps = [
         ":test_util",
         "//gutil:io",
+        "//p4_pdpi/internal:ordered_map",
         "//p4_symbolic/symbolic",
+        "@com_github_google_glog//:glog",
         "@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
         "@com_google_absl//absl/flags:flag",
         "@com_google_absl//absl/flags:parse",
@@ -79,21 +81,24 @@ cc_library(
         "@com_github_p4lang_p4runtime//:p4info_cc_proto",
         "@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
         "@com_google_absl//absl/status:statusor",
+        "@com_google_absl//absl/strings",
     ],
 )
 
 cc_test(
     name = "deparser_test",
     srcs = ["deparser_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",
         "//p4_symbolic/testdata:parser/sai_parser.config.json",
         "//p4_symbolic/testdata:parser/sai_parser.p4info.pb.txt",
     ],
     deps = [
         ":deparser",
+        ":test_util",
         ":z3_util",
-        "//gutil:io",
-        "//gutil:proto",
         "//gutil:status_matchers",
         "//p4_pdpi/packetlib",
         "//p4_pdpi/packetlib:packetlib_cc_proto",

diff --git a/p4_symbolic/deparser_test.cc b/p4_symbolic/deparser_test.cc
@@ -15,19 +15,20 @@
 #include "p4_symbolic/deparser.h"
 
 #include <memory>
+#include <vector>
 
 #include "absl/status/statusor.h"
+#include "absl/strings/match.h"
 #include "absl/strings/string_view.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
-#include "gutil/io.h"
-#include "gutil/proto.h"
 #include "gutil/status_matchers.h"
 #include "p4/v1/p4runtime.pb.h"
 #include "p4_pdpi/packetlib/packetlib.h"
 #include "p4_pdpi/packetlib/packetlib.pb.h"
 #include "p4_symbolic/symbolic/symbolic.h"
 #include "p4_symbolic/symbolic/util.h"
+#include "p4_symbolic/test_util.h"
 #include "p4_symbolic/z3_util.h"
 #include "z3++.h"
 
@@ -36,20 +37,149 @@ namespace {
 
 using ::p4_symbolic::symbolic::util::GetHeaderValidityFieldName;
 
+class IPv4RoutingBasicTest : 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<p4::v1::TableEntry> entries,
+        GetPiTableEntriesFromPiUpdatesProtoTextFile(entries_path));
+    Z3Context(/*renew=*/true);
+    ASSERT_OK_AND_ASSIGN(state_, symbolic::EvaluateP4Program(config, entries));
+  }
+
+ protected:
+  std::unique_ptr<symbolic::SolverState> state_;
+};
+
+TEST_F(IPv4RoutingBasicTest, DeparseIngressAndEgressHeadersWithoutConstraints) {
+  ASSERT_EQ(state_->solver->check(), z3::check_result::sat);
+  auto model = state_->solver->get_model();
+  EXPECT_OK(DeparseIngressPacket(*state_, model).status());
+  EXPECT_OK(DeparseEgressPacket(*state_, model).status());
+}
+
+TEST_F(IPv4RoutingBasicTest, DeparseIngressHeaders1) {
+  // Add constraints.
+  {
+    ASSERT_OK_AND_ASSIGN(
+        z3::expr eth_dst_addr,
+        state_->context.egress_headers.Get("ethernet.dstAddr"));
+    state_->solver->add(eth_dst_addr == Z3Context().bv_val(0, 48));
+    state_->solver->add(state_->context.egress_port ==
+                        Z3Context().bv_val(1, 9));
+
+    ASSERT_OK_AND_ASSIGN(
+        z3::expr ipv4_valid,
+        state_->context.ingress_headers.Get(
+            symbolic::util::GetHeaderValidityFieldName("ipv4")));
+    state_->solver->add(ipv4_valid);
+  }
+
+  // Solve and deparse.
+  ASSERT_EQ(state_->solver->check(), z3::check_result::sat);
+  auto model = state_->solver->get_model();
+  ASSERT_OK_AND_ASSIGN(std::string raw_packet,
+                       DeparseIngressPacket(*state_, model));
+
+  // Check that we got an IPv4 packet with destination address 10.10.0.0.
+  packetlib::Packet packet = packetlib::ParsePacket(raw_packet);
+  LOG(INFO) << "Z3-generated packet = " << packet.DebugString();
+  ASSERT_GE(packet.headers_size(), 2);
+  EXPECT_TRUE(packet.headers(0).has_ethernet_header());
+  EXPECT_TRUE(packet.headers(1).has_ipv4_header());
+  EXPECT_EQ(packet.headers(1).ipv4_header().ipv4_destination(), "10.10.0.0");
+}
+
+TEST_F(IPv4RoutingBasicTest, DeparseIngressHeaders2) {
+  // Add constraints.
+  {
+    ASSERT_OK_AND_ASSIGN(
+        z3::expr eth_dst_addr,
+        state_->context.egress_headers.Get("ethernet.dstAddr"));
+    state_->solver->add(eth_dst_addr ==
+                        Z3Context().bv_val((22UL << 40) + 22, 48));
+    state_->solver->add(state_->context.egress_port ==
+                        Z3Context().bv_val(1, 9));
+
+    ASSERT_OK_AND_ASSIGN(
+        z3::expr ipv4_valid,
+        state_->context.ingress_headers.Get(
+            symbolic::util::GetHeaderValidityFieldName("ipv4")));
+    state_->solver->add(ipv4_valid);
+  }
+
+  // Solve and deparse.
+  ASSERT_EQ(state_->solver->check(), z3::check_result::sat);
+  auto model = state_->solver->get_model();
+  ASSERT_OK_AND_ASSIGN(std::string raw_packet,
+                       DeparseIngressPacket(*state_, model));
+
+  // Check that we got an IPv4 packet with destination within 20.20.0.0/16.
+  packetlib::Packet packet = packetlib::ParsePacket(raw_packet);
+  LOG(INFO) << "Z3-generated packet = " << packet.DebugString();
+  ASSERT_GE(packet.headers_size(), 2);
+  EXPECT_TRUE(packet.headers(0).has_ethernet_header());
+  EXPECT_TRUE(packet.headers(1).has_ipv4_header());
+  EXPECT_TRUE(absl::StartsWith(
+      packet.headers(1).ipv4_header().ipv4_destination(), "20.20."));
+}
+
+TEST_F(IPv4RoutingBasicTest, DeparseEgressHeaders) {
+  // Add constraints.
+  {
+    ASSERT_OK_AND_ASSIGN(z3::expr ipv4_dst_addr,
+                         state_->context.ingress_headers.Get("ipv4.dstAddr"));
+    state_->solver->add(ipv4_dst_addr ==
+                        Z3Context().bv_val((10UL << 24) + 1, 32));
+
+    ASSERT_OK_AND_ASSIGN(
+        z3::expr ipv4_valid,
+        state_->context.ingress_headers.Get(
+            symbolic::util::GetHeaderValidityFieldName("ipv4")));
+    state_->solver->add(ipv4_valid);
+  }
+
+  // Solve and deparse.
+  ASSERT_EQ(state_->solver->check(), z3::check_result::sat);
+  auto model = state_->solver->get_model();
+  ASSERT_OK_AND_ASSIGN(std::string raw_packet,
+                       DeparseEgressPacket(*state_, model));
+
+  // Check that we got an IPv4 packet with destination MAC 00:00:00:00:00:0a.
+  packetlib::Packet packet = packetlib::ParsePacket(raw_packet);
+  LOG(INFO) << "Z3-generated packet = " << packet.DebugString();
+  ASSERT_GE(packet.headers_size(), 2);
+  EXPECT_TRUE(packet.headers(0).has_ethernet_header());
+  EXPECT_TRUE(packet.headers(1).has_ipv4_header());
+  EXPECT_EQ(packet.headers(0).ethernet_header().ethernet_destination(),
+            "00:00:00:00:00:0a");
+  EXPECT_EQ(packet.headers(1).ipv4_header().ipv4_destination(), "10.0.0.1");
+}
+
 class SaiDeparserTest : public testing::Test {
  public:
   void SetUp() override {
+    constexpr absl::string_view bmv2_json_path =
+        "p4_symbolic/testdata/parser/"
+        "sai_parser.config.json";
     constexpr absl::string_view p4info_path =
         "p4_symbolic/testdata/parser/"
         "sai_parser.p4info.pb.txt";
-    constexpr absl::string_view p4_config_path =
-        "p4_symbolic/testdata/parser/"
-        "sai_parser.config.json";
-    p4::v1::ForwardingPipelineConfig config;
-    ASSERT_OK(gutil::ReadProtoFromFile(p4info_path, config.mutable_p4info()));
-    ASSERT_OK_AND_ASSIGN(*config.mutable_p4_device_config(),
-                         gutil::ReadFile(std::string(p4_config_path)));
-
+    ASSERT_OK_AND_ASSIGN(
+        p4::v1::ForwardingPipelineConfig config,
+        ParseToForwardingPipelineConfig(bmv2_json_path, p4info_path));
     Z3Context(/*renew=*/true);
     ASSERT_OK_AND_ASSIGN(state_,
                          symbolic::EvaluateP4Program(config, /*entries=*/{}));

diff --git a/p4_symbolic/ir/test.bzl b/p4_symbolic/ir/test.bzl
@@ -25,8 +25,7 @@ load("@com_github_p4lang_p4c//:bazel/p4_library.bzl", "p4_library")
 load("//p4_pdpi/testing:diff_test.bzl", "diff_test")
 
 def ir_parsing_test(name, p4_program, golden_file, table_entries = None, p4_deps = []):
-    """Macro that defines exact diff IR testing rules for a given p4 program
-    with all their dependent rules.
+    """Macro that defines exact diff IR testing rules for a given p4 program.
 
     The macro defines these rules in order:
     1. A rule for producing bmv2 json and p4info files from a .p4 file using p4c.
@@ -36,6 +35,13 @@ def ir_parsing_test(name, p4_program, golden_file, table_entries = None, p4_deps
        specified expected file.
     Use the p4_deps list to specify dependent files that p4_program input fle
     depends on (e.g. by including them).
+
+    Args:
+      name: Test name.
+      p4_program: Input P4 program.
+      golden_file: File containing the expected IR output.
+      table_entries: File containing the table entries as input in protobuf text.
+      p4_deps: List of targets that the P4 program depends on (e.g., included files)
     """
     bmv2_file = "tmp/%s.bmv2.json" % name
     p4info_file = "tmp/%s.p4info.pb.txt" % name
@@ -76,10 +82,11 @@ def ir_parsing_test(name, p4_program, golden_file, table_entries = None, p4_deps
             ("--entries=$(location %s)" % table_entries if table_entries else ""),
             ("--output=$(location %s)" % test_output_file),
             "|| true",
-            # The following line makes sure hexstrings are lowercase in the protobuf file.
-            # This is needed because the hexstring representation of boost::multiprecision::cpp_int
-            # seems to behave differently accross different versions of boost (although the root
-            # cause has not been fully investigated).
+            # The following line makes sure hexstrings are lowercase in the
+            # protobuf file. This is needed because the hexstring representation
+            # of boost::multiprecision::cpp_int seems to behave differently
+            # across different versions of boost (although the root cause has
+            # not been fully investigated).
             "&& sed -i 's/0x[0-9A-F]\\+/\\L&/g' $(location %s)" % test_output_file,
         ]),
     )

diff --git a/p4_symbolic/ir/test.cc b/p4_symbolic/ir/test.cc
@@ -54,8 +54,9 @@ absl::Status Test() {
   ASSIGN_OR_RETURN(
       p4::v1::ForwardingPipelineConfig config,
       p4_symbolic::ParseToForwardingPipelineConfig(bmv2_path, p4info_path));
-  ASSIGN_OR_RETURN(std::vector<p4::v1::TableEntry> table_entries,
-                   p4_symbolic::ParseToPiTableEntries(entries_path));
+  ASSIGN_OR_RETURN(
+      std::vector<p4::v1::TableEntry> table_entries,
+      p4_symbolic::GetPiTableEntriesFromPiUpdatesProtoTextFile(entries_path));
   ASSIGN_OR_RETURN(p4_symbolic::ir::Dataplane dataplane,
                    p4_symbolic::ir::ParseToIr(config, table_entries));