[P4_Symbolic] Remove and modify outdated comments. Make the order of …

…creating symbolic header fields deterministic.Initialize standard metadata fields to 0.

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

p4_symbolic/symbolic/util.cc

@@ -74,19 +74,19 @@ absl::StatusOr<absl::btree_map<std::string, z3::expr>> FreeSymbolicHeaders(
   // variable for every field in every header instance.
   absl::btree_map<std::string, z3::expr> symbolic_headers;
   for (const auto &[header_name, header_type] : Ordered(headers)) {
-    // Pseudo fields used in P4-Symbolic indicating the state of the header.
+    // Pseudo fields (`$valid$`, `$extracted$`) in P4-Symbolic indicate the
+    // state of the header. Here we initialize the pseudo fields of each header
+    // to symbolic variables.
     for (const auto &pseudo_field_name :
          {kValidPseudoField, kExtractedPseudoField}) {
       std::string field_name =
           absl::StrFormat("%s.%s", header_name, pseudo_field_name);
-      // TODO: Set these fields to false while removing SAI parser
-      // code.
-      z3::expr free_expr = z3_context.bool_const(field_name.c_str());
-      symbolic_headers.insert({field_name, free_expr});
+      z3::expr free_variable = z3_context.bool_const(field_name.c_str());
+      symbolic_headers.insert({field_name, free_variable});
     }
 
     // Regular fields defined in the p4 program or v1model.
-    for (const auto &[field_name, field] : header_type.fields()) {
+    for (const auto &[field_name, field] : Ordered(header_type.fields())) {
       if (field.signed_()) {
         return absl::UnimplementedError(
             "Negative header fields are not supported");
@@ -100,7 +100,7 @@ absl::StatusOr<absl::btree_map<std::string, z3::expr>> FreeSymbolicHeaders(
     }
   }
 
-  // Initialize pseudo header fields.
+  // Initialize packet-wide pseudo fields to false.
   symbolic_headers.insert({
       std::string(kGotClonedPseudoField),
       z3_context.bool_val(false),

p4_symbolic/symbolic/v1model.cc

@@ -14,13 +14,21 @@
 
 #include "p4_symbolic/symbolic/v1model.h"
 
+#include <array>
+#include <string>
+#include <vector>
+
+#include "absl/status/status.h"
+#include "absl/strings/str_format.h"
 #include "absl/strings/substitute.h"
 #include "gutil/status.h"
 #include "p4_pdpi/internal/ordered_map.h"
+#include "p4_symbolic/ir/ir.pb.h"
 #include "p4_symbolic/symbolic/control.h"
 #include "p4_symbolic/symbolic/operators.h"
 #include "p4_symbolic/symbolic/parser.h"
 #include "p4_symbolic/symbolic/symbolic.h"
+#include "p4_symbolic/symbolic/v1model_intrinsic.h"
 #include "z3++.h"
 
 namespace p4_symbolic {
@@ -29,6 +37,68 @@ namespace v1model {
 
 namespace {
 
+// Initializes standard metadata fields to zero, except for `ingress_port`,
+// `egress_port`, and `packet_length`.
+absl::Status InitializeStandardMetadata(const ir::P4Program &program,
+                                        SymbolicPerPacketState &headers,
+                                        z3::context &z3_context) {
+  // Check if the standard metadata header exists.
+  auto it = program.headers().find(kStandardMetadataHeaderName);
+  if (it == program.headers().end()) {
+    return gutil::InternalErrorBuilder()
+           << "Header '" << kStandardMetadataHeaderName
+           << "' not found in P4 program.";
+  }
+
+  const google::protobuf::Map<std::string, ir::HeaderField>
+      &standard_metadata_fields = it->second.fields();
+
+  // List of standard metadata fields to be initialized to zero. See
+  // https://github.com/p4lang/p4c/blob/main/p4include/v1model.p4 for the full
+  // list of fields.
+  static constexpr std::array kFieldsToBeInitialized = {
+      // The ingress port should not be fixed.
+      // "ingress_port",
+      "egress_spec",
+      // TODO: Whenever `egress_port` is initialized to zero,
+      // `packet_util_production_test` fails. It would be helpful to understand
+      // why that's the case.
+      // "egress_port",
+      "instance_type",
+      // TODO: Packet length depends on the validity of headers.
+      // "packet_length",
+      "enq_timestamp",
+      "enq_qdepth",
+      "deq_timedelta",
+      "deq_qdepth",
+      "ingress_global_timestamp",
+      "egress_global_timestamp",
+      "mcast_grp",
+      "egress_rid",
+      "checksum_error",
+      "parser_error",
+      "priority",
+  };
+
+  // Initialize the listed standard metadata fields to zero.
+  for (const absl::string_view field_name : kFieldsToBeInitialized) {
+    auto it = standard_metadata_fields.find(field_name);
+    if (it == standard_metadata_fields.end()) {
+      return gutil::InternalErrorBuilder()
+             << "Field '" << field_name << "' not found in standard metadata.";
+    }
+
+    std::string field_full_name =
+        absl::StrFormat("%s.%s", kStandardMetadataHeaderName, field_name);
+    z3::expr zero = z3_context.bv_val(
+        (field_name == "instance_type" ? PKT_INSTANCE_TYPE_NORMAL : 0),
+        it->second.bitwidth());
+    RETURN_IF_ERROR(headers.UnguardedSet(field_full_name, zero));
+  }
+
+  return absl::OkStatus();
+}
+
 absl::Status CheckPhysicalPortsConformanceToV1Model(
     const std::vector<int> &physical_ports) {
   for (const int port : physical_ports) {
@@ -82,7 +152,8 @@ z3::expr EgressSpecDroppedValue(z3::context &z3_context) {
 absl::Status InitializeIngressHeaders(const ir::P4Program &program,
                                       SymbolicPerPacketState &ingress_headers,
                                       z3::context &z3_context) {
-  // TODO: Consider initializing all metadata fields to 0.
+  RETURN_IF_ERROR(
+      InitializeStandardMetadata(program, ingress_headers, z3_context));
 
   // Set the `$valid$` and `$extracted$` fields of all headers to false.
   const z3::expr false_expr = z3_context.bool_val(false);
@@ -93,11 +164,6 @@ absl::Status InitializeIngressHeaders(const ir::P4Program &program,
         header_name, kExtractedPseudoField, false_expr));
   }
 
-  // Set the `standard_metadata.parser_error` field to error.NoError.
-  ASSIGN_OR_RETURN(z3::expr no_error, parser::GetErrorCodeExpression(
-                                          program, "NoError", z3_context));
-  RETURN_IF_ERROR(ingress_headers.UnguardedSet(kParserErrorField, no_error));
-
   return absl::OkStatus();
 }