Merge branch 'main' of https://github.com/divyagayathri-hcl/sonic-pins …

…into tests_88

p4_symbolic/symbolic/expected/conditional_sequence.txt

@@ -28,7 +28,7 @@ ingress_headers:
 $got_cloned$ = false
 h1.$extracted$ = false
 h1.$valid$ = true
-h1.f1 = #x01
+h1.f1 = #x02
 h1.f2 = #x00
 h1.f3 = #x00
 h1.f4 = #x00
@@ -64,7 +64,7 @@ parsed_headers:
 $got_cloned$ = false
 h1.$extracted$ = true
 h1.$valid$ = true
-h1.f1 = #x01
+h1.f1 = #x02
 h1.f2 = #x00
 h1.f3 = #x00
 h1.f4 = #x00
@@ -100,7 +100,7 @@ egress_headers:
 $got_cloned$ = false
 h1.$extracted$ = true
 h1.$valid$ = true
-h1.f1 = #x01
+h1.f1 = #x02
 h1.f2 = #x00
 h1.f3 = #x00
 h1.f4 = #x00

p4_symbolic/symbolic/parser.cc

@@ -27,6 +27,7 @@
 #include "p4_symbolic/symbolic/operators.h"
 #include "p4_symbolic/symbolic/symbolic.h"
 #include "p4_symbolic/symbolic/util.h"
+#include "p4_symbolic/symbolic/v1model.h"
 #include "z3++.h"
 
 namespace p4_symbolic::symbolic::parser {
@@ -361,7 +362,7 @@ absl::Status SetParserError(const ir::P4Program &program,
                             const z3::expr &guard) {
   ASSIGN_OR_RETURN(z3::expr error_code,
                    GetErrorCodeExpression(program, error_name, z3_context));
-  return state.Set(kParserErrorField, std::move(error_code), guard);
+  return state.Set(v1model::kParserErrorField, std::move(error_code), guard);
 }
 
 // Evaluates the parse state with the given `state_name` in the given parser.
@@ -486,7 +487,7 @@ absl::StatusOr<z3::expr> GetErrorCodeExpression(const ir::P4Program &program,
 
   // Obtain the bitwidth of the `parser_error` field
   ASSIGN_OR_RETURN(unsigned int bitwidth,
-                   util::GetFieldBitwidth(kParserErrorField, program));
+                   util::GetFieldBitwidth(v1model::kParserErrorField, program));
 
   return z3_context.bv_val(error_code, bitwidth);
 }

p4_symbolic/symbolic/parser_test.cc

@@ -28,7 +28,6 @@
 #include "gutil/status_matchers.h"
 #include "p4_symbolic/ir/ir.h"
 #include "p4_symbolic/ir/ir.pb.h"
-#include "p4_symbolic/symbolic/symbolic.h"
 #include "p4_symbolic/symbolic/v1model.h"
 #include "z3++.h"
 
@@ -86,6 +85,9 @@ constexpr absl::string_view kHeaders = R"pb(
         key: "src_addr"
         value { name: "src_addr" bitwidth: 48 }
       }
+      ordered_fields_list: "dst_addr"
+      ordered_fields_list: "src_addr"
+      ordered_fields_list: "ether_type"
     }
   }
   headers {
@@ -153,17 +155,113 @@ constexpr absl::string_view kHeaders = R"pb(
         key: "version"
         value { name: "version" bitwidth: 4 }
       }
+      ordered_fields_list: "version"
+      ordered_fields_list: "ihl"
+      ordered_fields_list: "dscp"
+      ordered_fields_list: "ecn"
+      ordered_fields_list: "total_len"
+      ordered_fields_list: "identification"
+      ordered_fields_list: "reserved"
+      ordered_fields_list: "do_not_fragment"
+      ordered_fields_list: "more_fragments"
+      ordered_fields_list: "frag_offset"
+      ordered_fields_list: "ttl"
+      ordered_fields_list: "protocol"
+      ordered_fields_list: "header_checksum"
+      ordered_fields_list: "src_addr"
+      ordered_fields_list: "dst_addr"
     }
   }
   headers {
     key: "standard_metadata"
     value {
       name: "standard_metadata"
       id: 1
+      fields {
+        key: "_padding"
+        value { name: "_padding" bitwidth: 3 }
+      }
+      fields {
+        key: "checksum_error"
+        value { name: "checksum_error" bitwidth: 1 }
+      }
+      fields {
+        key: "deq_qdepth"
+        value { name: "deq_qdepth" bitwidth: 19 }
+      }
+      fields {
+        key: "deq_timedelta"
+        value { name: "deq_timedelta" bitwidth: 32 }
+      }
+      fields {
+        key: "egress_global_timestamp"
+        value { name: "egress_global_timestamp" bitwidth: 48 }
+      }
+      fields {
+        key: "egress_port"
+        value { name: "egress_port" bitwidth: 9 }
+      }
+      fields {
+        key: "egress_rid"
+        value { name: "egress_rid" bitwidth: 16 }
+      }
+      fields {
+        key: "egress_spec"
+        value { name: "egress_spec" bitwidth: 9 }
+      }
+      fields {
+        key: "enq_qdepth"
+        value { name: "enq_qdepth" bitwidth: 19 }
+      }
+      fields {
+        key: "enq_timestamp"
+        value { name: "enq_timestamp" bitwidth: 32 }
+      }
+      fields {
+        key: "ingress_global_timestamp"
+        value { name: "ingress_global_timestamp" bitwidth: 48 }
+      }
+      fields {
+        key: "ingress_port"
+        value { name: "ingress_port" bitwidth: 9 }
+      }
+      fields {
+        key: "instance_type"
+        value { name: "instance_type" bitwidth: 32 }
+      }
+      fields {
+        key: "mcast_grp"
+        value { name: "mcast_grp" bitwidth: 16 }
+      }
+      fields {
+        key: "packet_length"
+        value { name: "packet_length" bitwidth: 32 }
+      }
       fields {
         key: "parser_error"
         value { name: "parser_error" bitwidth: 32 }
       }
+      fields {
+        key: "priority"
+        value { name: "priority" bitwidth: 3 }
+      }
+      ordered_fields_list: "ingress_port"
+      ordered_fields_list: "egress_spec"
+      ordered_fields_list: "egress_port"
+      ordered_fields_list: "instance_type"
+      ordered_fields_list: "packet_length"
+      ordered_fields_list: "enq_timestamp"
+      ordered_fields_list: "enq_qdepth"
+      ordered_fields_list: "deq_timedelta"
+      ordered_fields_list: "deq_qdepth"
+      ordered_fields_list: "ingress_global_timestamp"
+      ordered_fields_list: "egress_global_timestamp"
+      ordered_fields_list: "mcast_grp"
+      ordered_fields_list: "egress_rid"
+      ordered_fields_list: "checksum_error"
+      ordered_fields_list: "parser_error"
+      ordered_fields_list: "priority"
+      ordered_fields_list: "_padding"
     }
   }
 )pb";
@@ -943,7 +1041,7 @@ std::vector<ParserTestParam> GetParserTestInstances() {
                                   ctx.bv_val(0x0800, 16))},
                 {"ipv4.$extracted$", (ctx.bv_const("ethernet.ether_type", 16) ==
                                       ctx.bv_val(0x0800, 16))},
-                {std::string(kParserErrorField),
+                {std::string(v1model::kParserErrorField),
                  z3::ite((ctx.bv_const("ethernet.ether_type", 16) !=
                           ctx.bv_val(0x0800, 16)),
                          ctx.bv_val(2, 32), ctx.bv_val(0, 32))},

p4_symbolic/symbolic/symbolic.h

@@ -37,30 +37,30 @@ namespace symbolic {
 // A port reserved to encode dropping packets.
 // The value is arbitrary; we choose the same value as BMv2:
 // https://github.com/p4lang/behavioral-model/blob/main/docs/simple_switch.md#standard-metadata
-constexpr int kDropPort = 511; // 2^9 - 1.
+constexpr int kDropPort = 511;  // 2^9 - 1.
+
 // An arbitrary port we reserve for the CPU port (for PacketIO packets).
-constexpr int kCpuPort = 510; // 2^9 - 2.
+constexpr int kCpuPort = 510;  // 2^9 - 2.
+
+// Bit-width of port numbers.
 constexpr int kPortBitwidth = 9;
 
 // Boolean pseudo header field that is initialized to false, set to true when
 // the header is extracted, and set to true/false when `setValid`/`setInvalid`
 // is called, respectively.
 constexpr absl::string_view kValidPseudoField = "$valid$";
+
 // Boolean pseudo header field denoting that the header has been extracted by
 // the parser. It is initialized to false and set to true when the header is
 // extracted. This is necessary to distinguish between headers extracted and
 // headers set to valid in the parsers via the `setValid` primitives. For
 // example, a `packet_in` header may be set to valid but should never be
 // extracted from the input packet.
 constexpr absl::string_view kExtractedPseudoField = "$extracted$";
+
 // Boolean pseudo header field that is set to true by p4-symbolic if the packet
 // gets cloned. Not an actual header field, but convenient for analysis.
 constexpr absl::string_view kGotClonedPseudoField = "$got_cloned$";
-// 32-bit bit-vector field in standard metadata indicating whether there is a
-// parser error. The error code is defined in core.p4 and can be extended by the
-// P4 program. 0 means no error.
-constexpr absl::string_view kParserErrorField =
-    "standard_metadata.parser_error";
 
 // The overall state of our symbolic solver/interpreter.
 // This is returned by our main analysis/interpration function, and is used