From 9d065b3b5119503d588975dbabe6a81e5300d2d2 Mon Sep 17 00:00:00 2001 From: smolkaj Date: Tue, 6 Dec 2022 22:51:17 -0800 Subject: [PATCH] [P4-Symbolic] Extend SAI module with packet-out headers and metadata. Add GetHeaderValidityFieldRef. --- p4_symbolic/sai/fields.cc | 24 ++++++++++++++++++++++++ p4_symbolic/sai/fields.h | 25 +++++++++++++++++++++++++ p4_symbolic/sai/parser.cc | 17 +++++++++++++++++ 3 files changed, 66 insertions(+) diff --git a/p4_symbolic/sai/fields.cc b/p4_symbolic/sai/fields.cc index a35821ce..a947a6d1 100644 --- a/p4_symbolic/sai/fields.cc +++ b/p4_symbolic/sai/fields.cc @@ -15,6 +15,7 @@ #include "p4_symbolic/sai/fields.h" #include +#include #include #include @@ -79,6 +80,10 @@ absl::StatusOr GetUserMetadataFieldName( << absl::StrJoin(mangled_candidates, "\n- "); } +std::string GetHeaderValidityFieldRef(absl::string_view header) { + return absl::StrCat(header, ".$valid$"); +} + namespace { // The p4c compiler mangles field names from the local_metadata struct. @@ -110,6 +115,18 @@ absl::StatusOr GetSaiFields(const SymbolicPerPacketState& state) { return z3::expr(Z3Context()); }; + // TODO: Make unconditional when we no longer need + // backwards-compatability. + auto packet_out = + state.ContainsKey("packet_out_header.$valid$") + ? std::make_optional(SaiPacketOut{ + .valid = get_field("packet_out_header.$valid$"), + .egress_port = get_field("packet_out_header.egress_port"), + .submit_to_ingress = + get_field("packet_out_header.submit_to_ingress"), + .unused_pad = get_field("packet_out_header.unused_pad"), + }) + : std::nullopt; auto erspan_ethernet = SaiEthernet{ .valid = get_field("erspan_ethernet.$valid$"), .dst_addr = get_field("erspan_ethernet.dst_addr"), @@ -256,6 +273,12 @@ absl::StatusOr GetSaiFields(const SymbolicPerPacketState& state) { .mirror_session_id_valid = get_metadata_field("mirror_session_id_valid"), .ingress_port = get_metadata_field("ingress_port"), .route_metadata = get_metadata_field("route_metadata"), + // TODO: Make unconditional when we no longer need + // backwards-compatability. + .bypass_ingress = + GetUserMetadata("bypass_ingress", state).ok() + ? std::make_optional(get_metadata_field("bypass_ingress")) + : std::nullopt, }; auto standard_metadata = V1ModelStandardMetadata{ .ingress_port = get_field("standard_metadata.ingress_port"), @@ -272,6 +295,7 @@ absl::StatusOr GetSaiFields(const SymbolicPerPacketState& state) { return SaiFields{ .headers = SaiHeaders{ + .packet_out = packet_out, .erspan_ethernet = erspan_ethernet, .erspan_ipv4 = erspan_ipv4, .erspan_gre = erspan_gre, diff --git a/p4_symbolic/sai/fields.h b/p4_symbolic/sai/fields.h index b70568f2..f14a1854 100644 --- a/p4_symbolic/sai/fields.h +++ b/p4_symbolic/sai/fields.h @@ -18,11 +18,22 @@ #ifndef PINS_P4_SYMBOLIC_SAI_FIELDS_H_ #define PINS_P4_SYMBOLIC_SAI_FIELDS_H_ +#include + +#include "absl/status/statusor.h" #include "p4_symbolic/symbolic/symbolic.h" #include "z3++.h" namespace p4_symbolic { +// Symbolic version of `packet_out_header_t` in metadata.p4. +struct SaiPacketOut { + z3::expr valid; + z3::expr egress_port; + z3::expr submit_to_ingress; + z3::expr unused_pad; +}; + // Symbolic version of `struct ethernet_t` in headers.p4. struct SaiEthernet { z3::expr valid; @@ -128,6 +139,10 @@ struct SaiGre { // Symbolic version of `struct headers_t` in metadata.p4. struct SaiHeaders { + // TODO: Make non-optional when we no longer need + // backwards-compatability. + std::optional packet_out; + SaiEthernet erspan_ethernet; SaiIpv4 erspan_ipv4; SaiGre erspan_gre; @@ -155,6 +170,9 @@ struct SaiLocalMetadata { 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. + std::optional bypass_ingress; }; // Symbolic version of `struct standard_metadata_t` in v1model.p4 @@ -179,6 +197,13 @@ absl::StatusOr GetSaiFields( absl::StatusOr GetUserMetadataFieldName( const std::string& field, const symbolic::SymbolicPerPacketState& state); +// The p4c compiler adds a special field ("$valid$") to each header +// corresponding to its validity. This function returns a field reference (in +// form of
.) to the p4c generated validity field of the given +// `header`. +// Note: This function does NOT check if the given header exists. +std::string GetHeaderValidityFieldRef(absl::string_view header); + } // namespace p4_symbolic #endif // PINS_P4_SYMBOLIC_SAI_FIELDS_H_ diff --git a/p4_symbolic/sai/parser.cc b/p4_symbolic/sai/parser.cc index ee8e6a57..daa7fc88 100644 --- a/p4_symbolic/sai/parser.cc +++ b/p4_symbolic/sai/parser.cc @@ -30,6 +30,9 @@ absl::StatusOr> EvaluateSaiParser( std::vector constraints; ASSIGN_OR_RETURN(SaiFields fields, GetSaiFields(state)); + // TODO: Make non-optional when we no longer need + // backwards-compatability. + std::optional& packet_out = fields.headers.packet_out; SaiEthernet& erspan_ethernet = fields.headers.erspan_ethernet; SaiIpv4& erspan_ipv4 = fields.headers.erspan_ipv4; SaiGre& erspan_gre = fields.headers.erspan_gre; @@ -59,6 +62,20 @@ absl::StatusOr> EvaluateSaiParser( constraints.push_back(local_metadata.ingress_port == standard_metadata.ingress_port); constraints.push_back(local_metadata.route_metadata == 0); + if (local_metadata.bypass_ingress.has_value()) { + // TODO: Make unconditional when we no longer need + // backwards-compatability. + constraints.push_back(*local_metadata.bypass_ingress == false); + } + + // `parse_packet_out` state. + if (packet_out.has_value()) { + // TODO: Make unconditional when we no longer need + // backwards-compatability. + constraints.push_back( + packet_out->valid == + (standard_metadata.ingress_port == symbolic::kCpuPort)); + } // `parse_ethernet` state. constraints.push_back(ethernet.valid == Z3Context().bool_val(true));