[P4-Symbolic] Extend SAI module with packet-out headers and metadata.…

… Add GetHeaderValidityFieldRef.

p4_symbolic/sai/fields.cc

@@ -15,6 +15,7 @@
 #include "p4_symbolic/sai/fields.h"
 
 #include <array>
+#include <optional>
 #include <string>
 #include <vector>
 
@@ -79,6 +80,10 @@ absl::StatusOr<std::string> GetUserMetadataFieldName(
                << absl::StrJoin(mangled_candidates, "\n- ");
 }
 
+std::string GetHeaderValidityFieldRef(absl::string_view header) {
+  return absl::StrCat(header, ".$valid$");
+}
+
 namespace {
 
 // The p4c compiler mangles field names from the local_metadata struct.
@@ -110,6 +115,18 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
     return z3::expr(Z3Context());
   };
 
+  // TODO: Make unconditional when we no longer need
+  // backwards-compatability.
+  auto packet_out =
+      state.ContainsKey("packet_out_header.$valid$")
+          ? std::make_optional(SaiPacketOut{
+                .valid = get_field("packet_out_header.$valid$"),
+                .egress_port = get_field("packet_out_header.egress_port"),
+                .submit_to_ingress =
+                    get_field("packet_out_header.submit_to_ingress"),
+                .unused_pad = get_field("packet_out_header.unused_pad"),
+            })
+          : std::nullopt;
   auto erspan_ethernet = SaiEthernet{
       .valid = get_field("erspan_ethernet.$valid$"),
       .dst_addr = get_field("erspan_ethernet.dst_addr"),
@@ -256,6 +273,12 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
       .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"),
+      // TODO: Make unconditional when we no longer need
+      // backwards-compatability.
+      .bypass_ingress =
+          GetUserMetadata("bypass_ingress", state).ok()
+              ? std::make_optional(get_metadata_field("bypass_ingress"))
+              : std::nullopt,
   };
   auto standard_metadata = V1ModelStandardMetadata{
       .ingress_port = get_field("standard_metadata.ingress_port"),
@@ -272,6 +295,7 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
   return SaiFields{
       .headers =
           SaiHeaders{
+              .packet_out = packet_out,
               .erspan_ethernet = erspan_ethernet,
               .erspan_ipv4 = erspan_ipv4,
               .erspan_gre = erspan_gre,

p4_symbolic/sai/fields.h

@@ -18,11 +18,22 @@
 #ifndef PINS_P4_SYMBOLIC_SAI_FIELDS_H_
 #define PINS_P4_SYMBOLIC_SAI_FIELDS_H_
 
+#include <optional>
+
+#include "absl/status/statusor.h"
 #include "p4_symbolic/symbolic/symbolic.h"
 #include "z3++.h"
 
 namespace p4_symbolic {
 
+// Symbolic version of `packet_out_header_t` in metadata.p4.
+struct SaiPacketOut {
+  z3::expr valid;
+  z3::expr egress_port;
+  z3::expr submit_to_ingress;
+  z3::expr unused_pad;
+};
+
 // Symbolic version of `struct ethernet_t` in headers.p4.
 struct SaiEthernet {
   z3::expr valid;
@@ -128,6 +139,10 @@ struct SaiGre {
 
 // Symbolic version of `struct headers_t` in metadata.p4.
 struct SaiHeaders {
+  // TODO: Make non-optional when we no longer need
+  // backwards-compatability.
+  std::optional<SaiPacketOut> packet_out;
+
   SaiEthernet erspan_ethernet;
   SaiIpv4 erspan_ipv4;
   SaiGre erspan_gre;
@@ -155,6 +170,9 @@ struct SaiLocalMetadata {
   z3::expr mirror_session_id_valid;
   z3::expr ingress_port;
   z3::expr route_metadata;
+  // TODO: Make non-optional when we no longer need
+  // backwards-compatability.
+  std::optional<z3::expr> bypass_ingress;
 };
 
 // Symbolic version of `struct standard_metadata_t` in v1model.p4
@@ -179,6 +197,13 @@ absl::StatusOr<SaiFields> GetSaiFields(
 absl::StatusOr<std::string> GetUserMetadataFieldName(
     const std::string& field, const symbolic::SymbolicPerPacketState& state);
 
+// The p4c compiler adds a special field ("$valid$") to each header
+// corresponding to its validity. This function returns a field reference (in
+// form of <header>.<field>) to the p4c generated validity field of the given
+// `header`.
+// Note: This function does NOT check if the given header exists.
+std::string GetHeaderValidityFieldRef(absl::string_view header);
+
 }  // namespace p4_symbolic
 
 #endif  // PINS_P4_SYMBOLIC_SAI_FIELDS_H_

p4_symbolic/sai/parser.cc

@@ -30,6 +30,9 @@ absl::StatusOr<std::vector<z3::expr>> EvaluateSaiParser(
   std::vector<z3::expr> constraints;
 
   ASSIGN_OR_RETURN(SaiFields fields, GetSaiFields(state));
+  // TODO: Make non-optional when we no longer need
+  // backwards-compatability.
+  std::optional<SaiPacketOut>& packet_out = fields.headers.packet_out;
   SaiEthernet& erspan_ethernet = fields.headers.erspan_ethernet;
   SaiIpv4& erspan_ipv4 = fields.headers.erspan_ipv4;
   SaiGre& erspan_gre = fields.headers.erspan_gre;
@@ -59,6 +62,20 @@ absl::StatusOr<std::vector<z3::expr>> EvaluateSaiParser(
   constraints.push_back(local_metadata.ingress_port ==
                         standard_metadata.ingress_port);
   constraints.push_back(local_metadata.route_metadata == 0);
+  if (local_metadata.bypass_ingress.has_value()) {
+    // TODO: Make unconditional when we no longer need
+    // backwards-compatability.
+    constraints.push_back(*local_metadata.bypass_ingress == false);
+  }
+
+  // `parse_packet_out` state.
+  if (packet_out.has_value()) {
+    // TODO: Make unconditional when we no longer need
+    // backwards-compatability.
+    constraints.push_back(
+        packet_out->valid ==
+        (standard_metadata.ingress_port == symbolic::kCpuPort));
+  }
 
   // `parse_ethernet` state.
   constraints.push_back(ethernet.valid == Z3Context().bool_val(true));