From d3b98dc6a659f841a37a053a72ec1cecb6de17ce Mon Sep 17 00:00:00 2001 From: kishanps Date: Wed, 26 Jul 2023 21:40:20 -0700 Subject: [PATCH] [P4_Symbolic] Remove and modify outdated comments. Make the order of creating symbolic header fields deterministic.Initialize standard metadata fields to 0. --- .../expected/conditional_sequence.txt | 6 +- p4_symbolic/symbolic/parser.cc | 5 +- p4_symbolic/symbolic/parser_test.cc | 102 +++++++++++++++++- p4_symbolic/symbolic/symbolic.h | 14 +-- p4_symbolic/symbolic/util.cc | 14 +-- p4_symbolic/symbolic/v1model.cc | 78 ++++++++++++-- p4_symbolic/symbolic/v1model.h | 12 +++ 7 files changed, 204 insertions(+), 27 deletions(-) diff --git a/p4_symbolic/symbolic/expected/conditional_sequence.txt b/p4_symbolic/symbolic/expected/conditional_sequence.txt index fc912d21..63975d8b 100644 --- a/p4_symbolic/symbolic/expected/conditional_sequence.txt +++ b/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 diff --git a/p4_symbolic/symbolic/parser.cc b/p4_symbolic/symbolic/parser.cc index 5e3bc24f..db5fe9b7 100644 --- a/p4_symbolic/symbolic/parser.cc +++ b/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 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); } diff --git a/p4_symbolic/symbolic/parser_test.cc b/p4_symbolic/symbolic/parser_test.cc index 6033b8c4..d4fca492 100644 --- a/p4_symbolic/symbolic/parser_test.cc +++ b/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,6 +155,21 @@ 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 { @@ -160,10 +177,91 @@ constexpr absl::string_view kHeaders = R"pb( 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 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))}, diff --git a/p4_symbolic/symbolic/symbolic.h b/p4_symbolic/symbolic/symbolic.h index b247c768..4f0b44e4 100644 --- a/p4_symbolic/symbolic/symbolic.h +++ b/p4_symbolic/symbolic/symbolic.h @@ -37,15 +37,19 @@ 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 @@ -53,14 +57,10 @@ constexpr absl::string_view kValidPseudoField = "$valid$"; // 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 diff --git a/p4_symbolic/symbolic/util.cc b/p4_symbolic/symbolic/util.cc index 94fc2f86..ddb7f665 100644 --- a/p4_symbolic/symbolic/util.cc +++ b/p4_symbolic/symbolic/util.cc @@ -74,19 +74,19 @@ absl::StatusOr> FreeSymbolicHeaders( // variable for every field in every header instance. absl::btree_map 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> FreeSymbolicHeaders( } } - // Initialize pseudo header fields. + // Initialize packet-wide pseudo fields to false. symbolic_headers.insert({ std::string(kGotClonedPseudoField), z3_context.bool_val(false), diff --git a/p4_symbolic/symbolic/v1model.cc b/p4_symbolic/symbolic/v1model.cc index 94015842..5f8d7b93 100644 --- a/p4_symbolic/symbolic/v1model.cc +++ b/p4_symbolic/symbolic/v1model.cc @@ -14,13 +14,21 @@ #include "p4_symbolic/symbolic/v1model.h" +#include +#include +#include + +#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 + &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 &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(); } diff --git a/p4_symbolic/symbolic/v1model.h b/p4_symbolic/symbolic/v1model.h index 237a3ad7..c3cf1783 100644 --- a/p4_symbolic/symbolic/v1model.h +++ b/p4_symbolic/symbolic/v1model.h @@ -26,12 +26,24 @@ namespace p4_symbolic { namespace symbolic { namespace v1model { +// Standard metadata header name. +constexpr absl::string_view kStandardMetadataHeaderName = "standard_metadata"; + +// 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"; + // V1model's `mark_to_drop` primitive sets the `egress_spec` field to // `kDropPort` to indicate the packet should be dropped at the end of // ingress/egress processing. See v1model.p4 for details. z3::expr EgressSpecDroppedValue(z3::context &z3_context); // Initializes the ingress headers to appropriate values. +// Here we initialize all standard metadata fields to zero for the ingress +// packet. Local (user) metadata fields are intentionally left uninitialized +// to align with the standard. absl::Status InitializeIngressHeaders(const ir::P4Program &program, SymbolicPerPacketState &ingress_headers, z3::context &z3_context);