[P4-Symbolic] Add ERSPAN support to hard-coded SAI fields/parser/deparser.

p4_symbolic/sai/deparser.cc

@@ -193,6 +193,24 @@ absl::Status Deparse(const SaiArp& header, const z3::model& model,
   return absl::OkStatus();
 }
 
+absl::Status Deparse(const SaiGre& header, const z3::model& model,
+                     pdpi::BitString& result) {
+  ASSIGN_OR_RETURN(bool valid, EvalBool(header.valid, model));
+  if (valid) {
+    RETURN_IF_ERROR(Deparse<1>(header.checksum_present, model, result));
+    RETURN_IF_ERROR(Deparse<1>(header.routing_present, model, result));
+    RETURN_IF_ERROR(Deparse<1>(header.key_present, model, result));
+    RETURN_IF_ERROR(Deparse<1>(header.sequence_present, model, result));
+    RETURN_IF_ERROR(Deparse<1>(header.strict_source_route, model, result));
+    RETURN_IF_ERROR(Deparse<3>(header.recursion_control, model, result));
+    RETURN_IF_ERROR(Deparse<1>(header.acknowledgement_present, model, result));
+    RETURN_IF_ERROR(Deparse<4>(header.flags, model, result));
+    RETURN_IF_ERROR(Deparse<3>(header.version, model, result));
+    RETURN_IF_ERROR(Deparse<16>(header.protocol, model, result));
+  }
+  return absl::OkStatus();
+}
+
 }  // namespace
 
 absl::StatusOr<std::string> SaiDeparser(
@@ -204,6 +222,9 @@ absl::StatusOr<std::string> SaiDeparser(
 absl::StatusOr<std::string> SaiDeparser(const SaiFields& packet,
                                         const z3::model& model) {
   pdpi::BitString result;
+  RETURN_IF_ERROR(Deparse(packet.headers.erspan_ethernet, model, result));
+  RETURN_IF_ERROR(Deparse(packet.headers.erspan_ipv4, model, result));
+  RETURN_IF_ERROR(Deparse(packet.headers.erspan_gre, model, result));
   RETURN_IF_ERROR(Deparse(packet.headers.ethernet, model, result));
   RETURN_IF_ERROR(Deparse(packet.headers.ipv4, model, result));
   RETURN_IF_ERROR(Deparse(packet.headers.ipv6, model, result));

p4_symbolic/sai/fields.cc

@@ -110,6 +110,44 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
     return z3::expr(Z3Context());
   };
 
+  auto erspan_ethernet = SaiEthernet{
+      .valid = get_field("erspan_ethernet.$valid$"),
+      .dst_addr = get_field("erspan_ethernet.dst_addr"),
+      .src_addr = get_field("erspan_ethernet.src_addr"),
+      .ether_type = get_field("erspan_ethernet.ether_type"),
+  };
+  auto erspan_ipv4 = SaiIpv4{
+      .valid = get_field("erspan_ipv4.$valid$"),
+      .version = get_field("erspan_ipv4.version"),
+      .ihl = get_field("erspan_ipv4.ihl"),
+      .dscp = get_field("erspan_ipv4.dscp"),
+      .ecn = get_field("erspan_ipv4.ecn"),
+      .total_len = get_field("erspan_ipv4.total_len"),
+      .identification = get_field("erspan_ipv4.identification"),
+      .reserved = get_field("erspan_ipv4.reserved"),
+      .do_not_fragment = get_field("erspan_ipv4.do_not_fragment"),
+      .more_fragments = get_field("erspan_ipv4.more_fragments"),
+      .frag_offset = get_field("erspan_ipv4.frag_offset"),
+      .ttl = get_field("erspan_ipv4.ttl"),
+      .protocol = get_field("erspan_ipv4.protocol"),
+      .header_checksum = get_field("erspan_ipv4.header_checksum"),
+      .src_addr = get_field("erspan_ipv4.src_addr"),
+      .dst_addr = get_field("erspan_ipv4.dst_addr"),
+  };
+  auto erspan_gre = SaiGre{
+      .valid = get_field("erspan_gre.$valid$"),
+      .checksum_present = get_field("erspan_gre.checksum_present"),
+      .routing_present = get_field("erspan_gre.routing_present"),
+      .key_present = get_field("erspan_gre.key_present"),
+      .sequence_present = get_field("erspan_gre.sequence_present"),
+      .strict_source_route = get_field("erspan_gre.strict_source_route"),
+      .recursion_control = get_field("erspan_gre.recursion_control"),
+      .acknowledgement_present =
+          get_field("erspan_gre.acknowledgement_present"),
+      .flags = get_field("erspan_gre.flags"),
+      .version = get_field("erspan_gre.version"),
+      .protocol = get_field("erspan_gre.protocol"),
+  };
   auto ethernet = SaiEthernet{
       .valid = get_field("ethernet.$valid$"),
       .dst_addr = get_field("ethernet.dst_addr"),
@@ -205,13 +243,19 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
                             });
   }
   return SaiFields{
-      .headers = SaiHeaders{.ethernet = ethernet,
-                            .ipv4 = ipv4,
-                            .ipv6 = ipv6,
-                            .udp = udp,
-                            .tcp = tcp,
-                            .icmp = icmp,
-                            .arp = arp},
+      .headers =
+          SaiHeaders{
+              .erspan_ethernet = erspan_ethernet,
+              .erspan_ipv4 = erspan_ipv4,
+              .erspan_gre = erspan_gre,
+              .ethernet = ethernet,
+              .ipv4 = ipv4,
+              .ipv6 = ipv6,
+              .udp = udp,
+              .tcp = tcp,
+              .icmp = icmp,
+              .arp = arp,
+          },
       .local_metadata = local_metadata,
       .standard_metadata = standard_metadata,
   };

p4_symbolic/sai/fields.h

@@ -111,8 +111,27 @@ struct SaiArp {
   z3::expr target_proto_addr;
 };
 
+// Symbolic version of `struct gre_t` in headers.p4.
+struct SaiGre {
+  z3::expr valid;
+  z3::expr checksum_present;
+  z3::expr routing_present;
+  z3::expr key_present;
+  z3::expr sequence_present;
+  z3::expr strict_source_route;
+  z3::expr recursion_control;
+  z3::expr acknowledgement_present;
+  z3::expr flags;
+  z3::expr version;
+  z3::expr protocol;
+};
+
 // Symbolic version of `struct headers_t` in metadata.p4.
 struct SaiHeaders {
+  SaiEthernet erspan_ethernet;
+  SaiIpv4 erspan_ipv4;
+  SaiGre erspan_gre;
+
   SaiEthernet ethernet;
   SaiIpv4 ipv4;
   SaiIpv6 ipv6;

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));
+  SaiEthernet& erspan_ethernet = fields.headers.erspan_ethernet;
+  SaiIpv4& erspan_ipv4 = fields.headers.erspan_ipv4;
+  SaiGre& erspan_gre = fields.headers.erspan_gre;
   SaiEthernet& ethernet = fields.headers.ethernet;
   SaiIpv4& ipv4 = fields.headers.ipv4;
   SaiIpv6& ipv6 = fields.headers.ipv6;
@@ -43,6 +46,9 @@ absl::StatusOr<std::vector<z3::expr>> EvaluateSaiParser(
   z3::expr bv_false = Z3Context().bv_val(0, 1);
 
   // `start` state.
+  constraints.push_back(!erspan_ethernet.valid);
+  constraints.push_back(!erspan_ipv4.valid);
+  constraints.push_back(!erspan_gre.valid);
   constraints.push_back(local_metadata.admit_to_l3 == bv_true);
   constraints.push_back(local_metadata.vrf_id == 0);
   constraints.push_back(local_metadata.mirror_session_id_valid == bv_false);