Merge branch 'main' into fuzzer_19

gutil/io.cc

@@ -1,4 +1,4 @@
-// Copyright 2020 Google LLC
+// Copyright 2024 Google LLC
 //
 // Licensed under the Apache License, Version 2.0 (the "License");
 // you may not use this file except in compliance with the License.

gutil/io.h

@@ -1,4 +1,4 @@
-// Copyright 2020 Google LLC
+// Copyright 2024 Google LLC
 //
 // Licensed under the Apache License, Version 2.0 (the "License");
 // you may not use this file except in compliance with the License.

p4_fuzzer/fuzzer_tests.cc

@@ -151,12 +151,13 @@ TEST_P(FuzzTest, P4rtWriteAndCheckNoInternalErrors) {
           ASSERT_OK_AND_ASSIGN(
               const pdpi::IrTableDefinition& table,
               gutil::FindOrStatus(info.tables_by_id(), table_id));
-          // TODO: acl_lookup_table has a resource limit problem.
+          // TODO: acl_pre_ingress_table has a resource limit
+          // problem.
           // TODO: router_interface_table, ipv4_table and
           // ipv6_table all have resource limit problems.
           // TODO: wcmp_group_table has a resource limit problem.
           if (!(mask_known_failures &&
-                (table.preamble().alias() == "acl_lookup_table" ||
+                (table.preamble().alias() == "acl_pre_ingress_table" ||
                  table.preamble().alias() == "router_interface_table" ||
                  table.preamble().alias() == "ipv4_table" ||
                  table.preamble().alias() == "ipv6_table" ||

p4_symbolic/BUILD.bazel

@@ -26,11 +26,11 @@ cc_binary(
     ],
     deps = [
         ":parser",
+        "//gutil:io",
         "//gutil:status",
         "//p4_symbolic/bmv2",
         "//p4_symbolic/sai:parser",
         "//p4_symbolic/symbolic",
-        "//p4_symbolic/util",
         "@com_google_absl//absl/flags:flag",
         "@com_google_absl//absl/flags:parse",
         "@com_google_absl//absl/flags:usage",
@@ -45,15 +45,15 @@ cc_library(
     srcs = ["parser.cc"],
     hdrs = ["parser.h"],
     deps = [
-	"//gutil:proto",
+        "//gutil:io",
+        "//gutil:proto",
         "//gutil:status",
 	"//p4_pdpi:ir_cc_proto",
         "//p4_symbolic/bmv2",
         "//p4_symbolic/ir",
         "//p4_symbolic/ir:ir_cc_proto",
         "//p4_symbolic/ir:pdpi_driver",
         "//p4_symbolic/symbolic",
-	"//p4_symbolic/util",
         "@com_google_absl//absl/types:span",
     ],
 )
@@ -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",
+    ],
+)

p4_symbolic/bmv2/BUILD.bazel

@@ -44,8 +44,8 @@ cc_library(
     ],
     deps = [
         ":bmv2_cc_proto",
+        "//gutil:io",
         "//gutil:status",
-        "//p4_symbolic/util",
         "@com_google_protobuf//:protobuf",
     ],
 )
@@ -55,8 +55,8 @@ cc_binary(
     srcs = ["test.cc"],
     deps = [
         ":bmv2",
+        "//gutil:io",
         "//gutil:status",
-        "//p4_symbolic/util",
         "@com_google_absl//absl/flags:flag",
         "@com_google_absl//absl/flags:parse",
         "@com_google_absl//absl/flags:usage",

p4_symbolic/bmv2/bmv2.cc

@@ -17,14 +17,14 @@
 #include <string>
 
 #include "google/protobuf/util/json_util.h"
+#include "gutil/io.h"
 #include "gutil/status.h"
-#include "p4_symbolic/util/io.h"
 
 namespace p4_symbolic {
 namespace bmv2 {
 
 absl::StatusOr<P4Program> ParseBmv2JsonFile(const std::string &json_path) {
-  ASSIGN_OR_RETURN(std::string json, util::ReadFile(json_path));
+  ASSIGN_OR_RETURN(std::string json, gutil::ReadFile(json_path));
   return ParseBmv2JsonString(json);
 }
 

p4_symbolic/bmv2/test.cc

@@ -30,9 +30,9 @@
 #include "absl/strings/str_format.h"
 #include "google/protobuf/text_format.h"
 #include "google/protobuf/util/json_util.h"
+#include "gutil/io.h"
 #include "gutil/status.h"
 #include "p4_symbolic/bmv2/bmv2.h"
-#include "p4_symbolic/util/io.h"
 
 ABSL_FLAG(std::string, bmv2, "", "The path to the bmv2 json file (required)");
 ABSL_FLAG(std::string, protobuf, "",
@@ -55,8 +55,7 @@ absl::Status Test() {
                    p4_symbolic::bmv2::ParseBmv2JsonFile(bmv2_path.c_str()));
 
   // Dumping protobuf.
-  RETURN_IF_ERROR(
-      p4_symbolic::util::WriteFile(bmv2.DebugString(), protobuf_path.c_str()));
+  RETURN_IF_ERROR(gutil::WriteFile(bmv2.DebugString(), protobuf_path.c_str()));
 
   // Dumping JSON.
   google::protobuf::util::JsonPrintOptions dumping_options;
@@ -68,8 +67,7 @@ absl::Status Test() {
   RETURN_IF_ERROR(
       gutil::ToAbslStatus(google::protobuf::util::MessageToJsonString(
           bmv2, &json_output_str, dumping_options)));
-  RETURN_IF_ERROR(
-      p4_symbolic::util::WriteFile(json_output_str, json_path.c_str()));
+  RETURN_IF_ERROR(gutil::WriteFile(json_output_str, json_path.c_str()));
 
   return absl::OkStatus();
 }

p4_symbolic/ir/BUILD.bazel

@@ -59,10 +59,10 @@ cc_library(
     ],
     deps = [
         ":ir_cc_proto",
+        "//gutil:io",
         "//gutil:status",
         "//p4_pdpi:ir",
         "//p4_pdpi:ir_cc_proto",
-        "//p4_symbolic/util",
         "@com_github_p4lang_p4runtime//:p4runtime_cc_proto",
         "@com_google_absl//absl/status",
         "@com_google_absl//absl/strings",

p4_symbolic/ir/ir.proto

@@ -25,7 +25,7 @@
 // Additionally, some types of expressions and statements are unsupported, these
 // are described in the relevant sections of this file.
 // See the bmv2 JSON format reference for more information:
-// https://github.com/p4lang/behavioral-model/blob/master/docs/JSON_format.md
+// https://github.com/p4lang/behavioral-model/blob/main/docs/JSON_format.md
 
 syntax = "proto3";
 
@@ -51,7 +51,7 @@ message P4Program {
 
   // TODO: If needed in the future, action calls can be added here, for
   // action calls that are not wrapped in other control constructs.
-  // https://github.com/p4lang/behavioral-model/blob/master/docs/JSON_format.md#pipelines
+  // https://github.com/p4lang/behavioral-model/blob/main/docs/JSON_format.md#pipelines
 }
 
 // A header type definition.

p4_symbolic/ir/table_entries.cc

@@ -18,11 +18,11 @@
 #include "absl/strings/str_cat.h"
 #include "absl/strings/str_format.h"
 #include "absl/strings/str_split.h"
+#include "gutil/io.h"
 #include "gutil/status.h"
 #include "p4/v1/p4runtime.pb.h"
 #include "p4_pdpi/ir.h"
 #include "p4_pdpi/ir.pb.h"
-#include "p4_symbolic/util/io.h"
 
 namespace p4_symbolic {
 namespace ir {

p4_symbolic/main.cc

@@ -27,12 +27,12 @@
 #include "absl/status/status.h"
 #include "absl/strings/str_cat.h"
 #include "absl/strings/str_format.h"
+#include "gutil/io.h"
 #include "gutil/status.h"
 #include "p4_symbolic/bmv2/bmv2.h"
 #include "p4_symbolic/parser.h"
 #include "p4_symbolic/sai/parser.h"
 #include "p4_symbolic/symbolic/symbolic.h"
-#include "p4_symbolic/util/io.h"
 
 ABSL_FLAG(std::string, p4info, "",
           "The path to the p4info protobuf file (required)");
@@ -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;
       }
@@ -160,8 +173,7 @@ absl::Status ParseAndEvaluate() {
 
   // Debugging.
   if (!debug_path.empty()) {
-    RETURN_IF_ERROR(
-        p4_symbolic::util::WriteFile(debug_smt_formula, debug_path));
+    RETURN_IF_ERROR(gutil::WriteFile(debug_smt_formula, debug_path));
   }
 
   return absl::OkStatus();

p4_symbolic/parser.cc

@@ -14,11 +14,11 @@
 
 #include "p4_symbolic/parser.h"
 
+#include "gutil/io.h"
 #include "gutil/proto.h"
 #include "p4_symbolic/bmv2/bmv2.h"
 #include "p4_symbolic/ir/ir.h"
 #include "p4_symbolic/ir/pdpi_driver.h"
-#include "p4_symbolic/util/io.h"
 
 namespace p4_symbolic {
 
@@ -58,7 +58,7 @@ absl::StatusOr<symbolic::Dataplane> ParseToIr(
     const std::string &bmv2_json_path, const std::string &p4info_path,
     absl::Span<const p4::v1::TableEntry> table_entries) {
   // Parse bmv2 json file into our initial bmv2 protobuf.
-  ASSIGN_OR_RETURN(std::string bmv2_json, util::ReadFile(bmv2_json_path));
+  ASSIGN_OR_RETURN(std::string bmv2_json, gutil::ReadFile(bmv2_json_path));
 
   // Parse p4info file into pdpi format.
   ASSIGN_OR_RETURN(pdpi::IrP4Info p4info,

p4_symbolic/sai/fields.cc

@@ -100,6 +100,11 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
       .admit_to_l3 = get_metadata_field("admit_to_l3"),
       .vrf_id = get_metadata_field("vrf_id"),
       .mirror_session_id_valid = get_metadata_field("mirror_session_id_valid"),
+      .ingress_port = get_metadata_field("ingress_port"),
+      .route_metadata = get_metadata_field("route_metadata"),
+  };
+  auto standard_metadata = V1ModelStandardMetadata{
+      .ingress_port = get_field("standard_metadata.ingress_port"),
   };
 
   if (!errors.empty()) {

p4_symbolic/sai/fields.h

@@ -63,8 +63,14 @@ struct SaiLocalMetadata {
   z3::expr vrf_id;
   // TODO: add `packet_rewrites` fields.
   z3::expr mirror_session_id_valid;
-  // TODO: add `mirror*` fields.
-  // TODO: Add `color` field.
+  z3::expr ingress_port;
+  z3::expr route_metadata;
+};
+
+// Symbolic version of `struct standard_metadata_t` in v1model.p4
+// TODO: Add missing fields, as needed.
+struct V1ModelStandardMetadata {
+  z3::expr ingress_port;
 };
 
 struct SaiFields {

p4_symbolic/symbolic/BUILD.bazel

@@ -27,7 +27,6 @@ cc_library(
         "control.cc",
         "guarded_map.cc",
         "operators.cc",
-        "packet.cc",
         "symbolic.cc",
         "table.cc",
         "util.cc",
@@ -39,7 +38,6 @@ cc_library(
         "control.h",
         "guarded_map.h",
         "operators.h",
-        "packet.h",
         "symbolic.h",
         "table.h",
         "util.h",
@@ -48,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",
@@ -59,10 +58,7 @@ cc_library(
         "@com_github_p4lang_p4runtime//:p4info_cc_proto",
         "@com_github_z3prover_z3//:api",
         "@com_gnu_gmp//:gmp",
-        "@com_google_absl//absl/algorithm:container",
         "@com_google_absl//absl/cleanup",
-        "@com_google_absl//absl/container:btree",
-        "@com_google_absl//absl/memory",
         "@com_google_absl//absl/status",
         "@com_google_absl//absl/strings",
         "@com_google_absl//absl/strings:str_format",
@@ -103,3 +99,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",
+    ],
+)