[P4_Symbolic] Add support for VLAN header. Fix SAI VLAN header existe…

…nce check. (sonic-net#905) Co-authored-by: kheradmandG <[email protected]> Co-authored-by: kishanps <[email protected]>
divyagayathri-hcl · Dec 31, 2024 · dc824c3 · dc824c3
1 parent a115348
commit dc824c3
Show file tree

Hide file tree

Showing 7 changed files with 142 additions and 14 deletions.
diff --git a/p4_symbolic/packet_synthesizer/util.cc b/p4_symbolic/packet_synthesizer/util.cc
@@ -123,6 +123,7 @@ absl::Status AddSanePacketConstraints(
   auto& ethernet = ingress_fields.headers.ethernet;
   auto& ipv4 = ingress_fields.headers.ipv4;
   auto& ipv6 = ingress_fields.headers.ipv6;
+  auto& vlan = ingress_fields.headers.vlan;
 
   // ======Ethernet constraints======
   // Use "locally administered", "individual" MAC addresses
@@ -176,6 +177,16 @@ absl::Status AddSanePacketConstraints(
   state.solver->add(ipv6.src_addr != Bitvector<128>(1));
   state.solver->add(ipv6.dst_addr != Bitvector<128>(1));
 
+  // ======VLAN constraints==========
+  // TODO: Make unconditional when we no longer need
+  // backwards-compatibility.
+  if (vlan.has_value()) {
+    // TODO: Consider testing the following VIDs when PacketIO is
+    // properly modeled.
+    state.solver->add(vlan->vlan_id != Bitvector<12>(0xFFF));
+    state.solver->add(vlan->vlan_id != Bitvector<12>(0x001));
+  }
+
   return absl::OkStatus();
 }
 

diff --git a/p4_symbolic/sai/BUILD.bazel b/p4_symbolic/sai/BUILD.bazel
@@ -41,5 +41,8 @@ cc_library(
         "//p4_symbolic/symbolic",
         "@com_github_z3prover_z3//:api",
         "@com_google_absl//absl/status",
+        "@com_google_absl//absl/status:statusor",
+        "@com_google_absl//absl/strings",
     ],
 )
+
diff --git a/p4_symbolic/sai/deparser.cc b/p4_symbolic/sai/deparser.cc
@@ -72,6 +72,18 @@ absl::Status Deparse(const SaiEthernet& header, const z3::model& model,
   return absl::OkStatus();
 }
 
+absl::Status Deparse(const SaiVlan& header, const z3::model& model,
+                     pdpi::BitString& result) {
+  ASSIGN_OR_RETURN(bool valid, EvalZ3Bool(header.valid, model));
+  if (valid) {
+    RETURN_IF_ERROR(Deparse<3>(header.priority_code_point, model, result));
+    RETURN_IF_ERROR(Deparse<1>(header.drop_eligible_indicator, model, result));
+    RETURN_IF_ERROR(Deparse<12>(header.vlan_id, model, result));
+    RETURN_IF_ERROR(Deparse<16>(header.ether_type, model, result));
+  }
+  return absl::OkStatus();
+}
+
 absl::Status Deparse(const SaiIpv4& header, const z3::model& model,
                      pdpi::BitString& result) {
   ASSIGN_OR_RETURN(bool valid, EvalZ3Bool(header.valid, model));
@@ -222,6 +234,11 @@ absl::StatusOr<std::string> SaiDeparser(const SaiFields& packet,
   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));
+  // TODO: Make unconditional when we no longer need
+  // backwards-compatibility.
+  if (packet.headers.vlan.has_value()) {
+    RETURN_IF_ERROR(Deparse(*packet.headers.vlan, model, result));
+  }
   RETURN_IF_ERROR(Deparse(packet.headers.tunnel_encap_ipv6, model, result));
   RETURN_IF_ERROR(Deparse(packet.headers.tunnel_encap_gre, model, result));
   RETURN_IF_ERROR(Deparse(packet.headers.ipv4, model, result));

diff --git a/p4_symbolic/sai/deparser_test.cc b/p4_symbolic/sai/deparser_test.cc
@@ -69,6 +69,35 @@ TEST_P(SaiDeparserTest, DeparseIngressAndEgressHeadersWithoutConstraints) {
   }
 }
 
+TEST_P(SaiDeparserTest, VlanPacketParserIntegrationTest) {
+  // Add parse constraints.
+  {
+    ASSERT_OK_AND_ASSIGN(auto parse_constraints,
+                         EvaluateSaiParser(state_->context.ingress_headers));
+    for (auto& constraint : parse_constraints) state_->solver->add(constraint);
+  }
+
+  // Add VLAN constraint.
+  {
+    ASSERT_OK_AND_ASSIGN(SaiFields fields,
+                         GetSaiFields(state_->context.ingress_headers));
+    state_->solver->add(fields.headers.vlan->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,
+                       SaiDeparser(state_->context.ingress_headers, model));
+
+  // Check we indeed got a VLAN packet.
+  packetlib::Packet packet = packetlib::ParsePacket(raw_packet);
+  LOG(INFO) << "Z3-generated packet = " << packet.DebugString();
+  ASSERT_GE(packet.headers_size(), 2);
+  ASSERT_TRUE(packet.headers(0).has_ethernet_header());
+  ASSERT_TRUE(packet.headers(1).has_vlan_header());
+}
+
 TEST_P(SaiDeparserTest, Ipv4UdpPacketParserIntegrationTest) {
   // Add parse constraints.
   {
@@ -77,12 +106,14 @@ TEST_P(SaiDeparserTest, Ipv4UdpPacketParserIntegrationTest) {
     for (auto& constraint : parse_constraints) state_->solver->add(constraint);
   }
 
-  // Add IPv4 + UDP constraint.
+  // Add IPv4 + UDP (+ no VLAN) constraint.
   {
     ASSERT_OK_AND_ASSIGN(SaiFields fields,
                          GetSaiFields(state_->context.ingress_headers));
     state_->solver->add(fields.headers.ipv4.valid);
     state_->solver->add(fields.headers.udp.valid);
+
+    state_->solver->add(!fields.headers.vlan->valid);
   }
 
   // Solve and deparse.
@@ -109,14 +140,15 @@ TEST_P(SaiDeparserTest, Ipv6TcpPacketParserIntegrationTest) {
     for (auto& constraint : parse_constraints) state_->solver->add(constraint);
   }
 
-  // Add IPv6 + UDP constraint.
+  // Add IPv6 + TCP (+ no VLAN) constraint.
   {
     ASSERT_OK_AND_ASSIGN(SaiFields fields,
                          GetSaiFields(state_->context.ingress_headers));
     state_->solver->add(!fields.headers.ipv4.valid);
     state_->solver->add(fields.headers.tcp.valid);
     // The only way to have a TCP packet that is not an IPv4 packet is to have
     // an IPv6 packet.
+    state_->solver->add(!fields.headers.vlan->valid);
   }
 
   // Solve and deparse.
@@ -143,11 +175,12 @@ TEST_P(SaiDeparserTest, ArpPacketParserIntegrationTest) {
     for (auto& constraint : parse_constraints) state_->solver->add(constraint);
   }
 
-  // Add ARP constraint.
+  // Add ARP (+ no VLAN) constraint.
   {
     ASSERT_OK_AND_ASSIGN(SaiFields fields,
                          GetSaiFields(state_->context.ingress_headers));
     state_->solver->add(fields.headers.arp.valid);
+    state_->solver->add(!fields.headers.vlan->valid);
   }
 
   // Solve and deparse.
@@ -173,11 +206,12 @@ TEST_P(SaiDeparserTest, IcmpPacketParserIntegrationTest) {
     for (auto& constraint : parse_constraints) state_->solver->add(constraint);
   }
 
-  // Add ICMP constraint.
+  // Add ICMP (+ no VLAN) constraint.
   {
     ASSERT_OK_AND_ASSIGN(SaiFields fields,
                          GetSaiFields(state_->context.ingress_headers));
     state_->solver->add(fields.headers.icmp.valid);
+    state_->solver->add(!fields.headers.vlan->valid);
   }
 
   // Solve and deparse.

diff --git a/p4_symbolic/sai/fields.cc b/p4_symbolic/sai/fields.cc
@@ -116,7 +116,7 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
   };
 
   // TODO: Make unconditional when we no longer need
-  // backwards-compatability.
+  // backwards-compatibility.
   auto packet_in =
       state.ContainsKey("packet_in_header.$valid$")
           ? std::make_optional(SaiPacketIn{
@@ -181,6 +181,19 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
       .src_addr = get_field("ethernet.src_addr"),
       .ether_type = get_field("ethernet.ether_type"),
   };
+  // TODO: Make unconditional when we no longer need
+  // backwards-compatibility.
+  auto vlan =
+      state.ContainsKey("vlan.$valid$")
+          ? std::make_optional(SaiVlan{
+                .valid = get_field("vlan.$valid$"),
+                .priority_code_point = get_field("vlan.priority_code_point"),
+                .drop_eligible_indicator =
+                    get_field("vlan.drop_eligible_indicator"),
+                .vlan_id = get_field("vlan.vlan_id"),
+                .ether_type = get_field("vlan.ether_type"),
+            })
+          : std::nullopt;
   auto tunnel_encap_ipv6 = SaiIpv6{
       .valid = get_field("tunnel_encap_ipv6.$valid$"),
       .version = get_field("tunnel_encap_ipv6.version"),
@@ -276,6 +289,15 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
       .target_proto_addr = get_field("arp.target_proto_addr"),
   };
   auto local_metadata = SaiLocalMetadata{
+      // TODO: Make unconditional when we no longer need
+      // backwards-compatibility.
+      .vlan_id = GetUserMetadata("vlan_id", state).ok()
+                     ? std::make_optional(get_metadata_field("vlan_id"))
+                     : std::nullopt,
+      .vlan_id_valid =
+          GetUserMetadata("vlan_id_valid", state).ok()
+              ? std::make_optional(get_metadata_field("vlan_id_valid"))
+              : std::nullopt,
       .admit_to_l3 = get_metadata_field("admit_to_l3"),
       .vrf_id = get_metadata_field("vrf_id"),
       .l4_src_port = get_metadata_field("l4_src_port"),
@@ -284,7 +306,7 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
       .ingress_port = get_metadata_field("ingress_port"),
       .route_metadata = get_metadata_field("route_metadata"),
       // TODO: Make unconditional when we no longer need
-      // backwards-compatability.
+      // backwards-compatibility.
       .bypass_ingress =
           GetUserMetadata("bypass_ingress", state).ok()
               ? std::make_optional(get_metadata_field("bypass_ingress"))
@@ -311,6 +333,7 @@ absl::StatusOr<SaiFields> GetSaiFields(const SymbolicPerPacketState& state) {
               .erspan_ipv4 = erspan_ipv4,
               .erspan_gre = erspan_gre,
               .ethernet = ethernet,
+              .vlan = vlan,
               .tunnel_encap_ipv6 = tunnel_encap_ipv6,
               .tunnel_encap_gre = tunnel_encap_gre,
               .ipv4 = ipv4,

diff --git a/p4_symbolic/sai/fields.h b/p4_symbolic/sai/fields.h
@@ -50,6 +50,15 @@ struct SaiEthernet {
   z3::expr ether_type;
 };
 
+// Symbolic version of `struct vlan_t` in headers.p4.
+struct SaiVlan {
+  z3::expr valid;
+  z3::expr priority_code_point;
+  z3::expr drop_eligible_indicator;
+  z3::expr vlan_id;
+  z3::expr ether_type;
+};
+
 // Symbolic version of `struct ipv4_t` in headers.p4.
 struct SaiIpv4 {
   z3::expr valid;
@@ -147,15 +156,18 @@ struct SaiGre {
 
 // Symbolic version of `struct headers_t` in metadata.p4.
 struct SaiHeaders {
-  // TODO: Make non-optional when we no longer need
-  // backwards-compatability.
+  // TODO: Make unconditional when we no longer need
+  // backwards-compatibility.
   std::optional<SaiPacketIn> packet_in;
   std::optional<SaiPacketOut> packet_out;
 
   SaiEthernet erspan_ethernet;
   SaiIpv4 erspan_ipv4;
   SaiGre erspan_gre;
   SaiEthernet ethernet;
+  // TODO: Make unconditional when we no longer need
+  // backwards-compatibility.
+  std::optional<SaiVlan> vlan;
 
   // Not extracted during parsing.
   SaiIpv6 tunnel_encap_ipv6;
@@ -172,15 +184,19 @@ struct SaiHeaders {
 // Symbolic version of `struct local_metadata_t` in metadata.p4.
 // TODO: add missing fields.
 struct SaiLocalMetadata {
+  // TODO: Make unconditional when we no longer need
+  // backwards-compatibility.
+  std::optional<z3::expr> vlan_id;
+  std::optional<z3::expr> vlan_id_valid;
   z3::expr admit_to_l3;
   z3::expr vrf_id;
   z3::expr l4_src_port;
   z3::expr l4_dst_port;
   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.
+  // TODO: Make unconditional when we no longer need
+  // backwards-compatibility.
   std::optional<z3::expr> bypass_ingress;
 };
 

diff --git a/p4_symbolic/sai/parser.cc b/p4_symbolic/sai/parser.cc
@@ -14,6 +14,12 @@
 
 #include "p4_symbolic/sai/parser.h"
 
+#include <optional>
+#include <type_traits>
+#include <vector>
+
+#include "absl/status/statusor.h"
+#include "absl/strings/match.h"
 #include "gutil/status.h"
 #include "p4_symbolic/sai/fields.h"
 #include "p4_symbolic/symbolic/operators.h"
@@ -38,6 +44,9 @@ absl::StatusOr<std::vector<z3::expr>> EvaluateSaiParser(
   SaiIpv4& erspan_ipv4 = fields.headers.erspan_ipv4;
   SaiGre& erspan_gre = fields.headers.erspan_gre;
   SaiEthernet& ethernet = fields.headers.ethernet;
+  // TODO: Make non-optional when we no longer need
+  // backwards-compatibility.
+  std::optional<SaiVlan>& vlan = fields.headers.vlan;
   SaiIpv6& tunnel_encap_ipv6 = fields.headers.tunnel_encap_ipv6;
   SaiGre& tunnel_encap_gre = fields.headers.tunnel_encap_gre;
   SaiIpv4& ipv4 = fields.headers.ipv4;
@@ -57,6 +66,14 @@ absl::StatusOr<std::vector<z3::expr>> EvaluateSaiParser(
   constraints.push_back(!erspan_gre.valid);
   constraints.push_back(!tunnel_encap_ipv6.valid);
   constraints.push_back(!tunnel_encap_gre.valid);
+  // TODO: Make unconditional when we no longer need
+  // backwards-compatibility.
+  if (local_metadata.vlan_id.has_value()) {
+    constraints.push_back(*local_metadata.vlan_id == 0);
+  }
+  if (local_metadata.vlan_id_valid.has_value()) {
+    constraints.push_back(*local_metadata.vlan_id_valid == bv_false);
+  }
   constraints.push_back(local_metadata.admit_to_l3 == bv_false);
   constraints.push_back(local_metadata.vrf_id == 0);
   constraints.push_back(local_metadata.mirror_session_id_valid == bv_false);
@@ -83,11 +100,18 @@ absl::StatusOr<std::vector<z3::expr>> EvaluateSaiParser(
         (standard_metadata.ingress_port == symbolic::kCpuPort));
   }
 
-  // `parse_ethernet` state.
+  // `parse_ethernet` state and `parse_8021q_vlan` state.
   constraints.push_back(ethernet.valid == Z3Context().bool_val(true));
-  constraints.push_back(ipv4.valid == (ethernet.ether_type == 0x0800));
-  constraints.push_back(ipv6.valid == (ethernet.ether_type == 0x86dd));
-  constraints.push_back(arp.valid == (ethernet.ether_type == 0x0806));
+  // TODO: Make unconditional when we no longer need
+  // backwards-compatibility.
+  z3::expr ether_type = ethernet.ether_type;
+  if (vlan.has_value()) {
+    constraints.push_back(vlan->valid == (ethernet.ether_type == 0x8100));
+    ether_type = z3::ite(vlan->valid, vlan->ether_type, ethernet.ether_type);
+  }
+  constraints.push_back(ipv4.valid == (ether_type == 0x0800));
+  constraints.push_back(ipv6.valid == (ether_type == 0x86dd));
+  constraints.push_back(arp.valid == (ether_type == 0x0806));
 
   // `parse_ipv{4,6}` states.
   constraints.push_back(icmp.valid == (ipv4.valid && ipv4.protocol == 0x01 ||