From 93f57a1083b99d9569d95a4d37f989af5830ff78 Mon Sep 17 00:00:00 2001 From: VSuryaprasad-HCL Date: Wed, 6 Nov 2024 15:38:15 +0530 Subject: [PATCH 1/3] [P4_Symbolic] Adding util files to p4_symbolic/packet_synthesizer/ --- p4_symbolic/packet_synthesizer/BUILD.bazel | 30 +++ p4_symbolic/packet_synthesizer/util.cc | 269 ++++++++++++++++++++ p4_symbolic/packet_synthesizer/util.h | 70 +++++ p4_symbolic/packet_synthesizer/util_test.cc | 92 +++++++ 4 files changed, 461 insertions(+) create mode 100644 p4_symbolic/packet_synthesizer/util.cc create mode 100644 p4_symbolic/packet_synthesizer/util.h create mode 100644 p4_symbolic/packet_synthesizer/util_test.cc diff --git a/p4_symbolic/packet_synthesizer/BUILD.bazel b/p4_symbolic/packet_synthesizer/BUILD.bazel index d2d10557..753e3531 100644 --- a/p4_symbolic/packet_synthesizer/BUILD.bazel +++ b/p4_symbolic/packet_synthesizer/BUILD.bazel @@ -18,6 +18,36 @@ package( licenses = ["notice"], ) +cc_library( + name = "util", + srcs = ["util.cc"], + hdrs = ["util.h"], + deps = [ + "//gutil:status", + "//p4_pdpi/netaddr:ipv6_address", + "//p4_pdpi/string_encodings:decimal_string", + "//p4_pdpi/utils:ir", + "//p4_symbolic:z3_util", + "//p4_symbolic/sai:fields", + "//p4_symbolic/symbolic", + "@com_google_absl//absl/status", + "@com_google_absl//absl/strings", + ], +) + +cc_test( + name = "util_test", + srcs = ["util_test.cc"], + deps = [ + ":util", + "//gutil:status_matchers", + "//gutil:testing", + "//p4_symbolic/ir:ir_cc_proto", + "@com_google_absl//absl/status", + "@com_google_googletest//:gtest_main", + ], +) + proto_library( name = "packet_synthesizer_proto", srcs = ["packet_synthesizer.proto"], diff --git a/p4_symbolic/packet_synthesizer/util.cc b/p4_symbolic/packet_synthesizer/util.cc new file mode 100644 index 00000000..0019ab22 --- /dev/null +++ b/p4_symbolic/packet_synthesizer/util.cc @@ -0,0 +1,269 @@ +// Copyright 2024 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#include "p4_symbolic/packet_synthesizer/util.h" + +#include "absl/strings/string_view.h" +#include "absl/strings/substitute.h" +#include "gutil/status.h" +#include "p4_pdpi/netaddr/ipv6_address.h" +#include "p4_pdpi/string_encodings/decimal_string.h" +#include "p4_pdpi/utils/ir.h" +#include "p4_symbolic/sai/fields.h" +#include "p4_symbolic/symbolic/operators.h" +#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/z3_util.h" + +namespace p4_symbolic { +namespace packet_synthesizer { +using ::p4_symbolic::ir::P4Program; +using ::p4_symbolic::symbolic::operators::BitAnd; +using ::p4_symbolic::symbolic::operators::Eq; +using ::p4_symbolic::symbolic::operators::PrefixEq; + +namespace { + +// Creates Z3 bitvector of the given width and value. +// The use of a template here is a hack to improve readability. +// TODO: Move to p4-symbolic utility library. +template +inline z3::expr Bitvector(uint64_t value) { + return p4_symbolic::Z3Context().bv_val(value, num_bits); +} + +// TODO: Move to netaddr. +struct Ipv6Range { + netaddr::Ipv6Address value; + int prefix_length = 0; +}; + +// TODO: Move to netaddr. +absl::StatusOr ParseIpv6Range(absl::string_view ipv6_range) { + std::vector parts = absl::StrSplit(ipv6_range, '/'); + if (parts.size() != 2) { + return gutil::InvalidArgumentErrorBuilder() + << "invalid IPv6 range: " << ipv6_range; + } + ASSIGN_OR_RETURN(auto ipv6, netaddr::Ipv6Address::OfString(parts[0]), + _ << " while trying to parse Ipv6 range: " << ipv6_range); + ASSIGN_OR_RETURN(int prefix_length, pdpi::DecimalStringToUint32(parts[1]), + _ << " while trying to parse Ipv6 range: " << ipv6_range); + return Ipv6Range{ + .value = ipv6, + .prefix_length = prefix_length, + }; +} + +// https://www.iana.org/assignments/ipv6-address-space/ipv6-address-space.xhtml +absl::StatusOr> GetUnicastIpv6Ranges() { + std::vector result; + // Global Unicast (RFC 4291). + ASSIGN_OR_RETURN(result.emplace_back(), ParseIpv6Range("2000::/3")); + // Unique Local Unicast (RFC 4193). + ASSIGN_OR_RETURN(result.emplace_back(), ParseIpv6Range("fe80::/10")); + return result; +} + +// TODO: Move to p4-symbolic utility library and add unit tests. +absl::StatusOr Ipv6PrefixLengthToZ3Mask(int prefix_length) { + if (prefix_length < 0 || prefix_length > 128) { + return gutil::InvalidArgumentErrorBuilder() + << "invalid IPv6 prefix length: " << prefix_length; + } + if (prefix_length > 64) { + return Bitvector<128>(0xFFFF'FFFF'FFFF'FFFFu).rotate_left(64) | + Bitvector<128>(0xFFFF'FFFF'FFFF'FFFFu << (128 - prefix_length)); + } else { + return Bitvector<128>(0xFFFF'FFFF'FFFF'FFFFu << (64 - prefix_length)) + .rotate_left(64); + } +} + +// TODO: Move to p4-symbolic utility library. +absl::StatusOr Ipv6AddressToZ3Bitvector( + const netaddr::Ipv6Address& ipv6) { + std::bitset<128> bits = ipv6.ToBitset(); + uint64_t upper = (bits >> 64).to_ullong(); + uint64_t lower = + (bits & std::bitset<128>(0xFFFF'FFFF'FFFF'FFFFu)).to_ullong(); + return Bitvector<128>(upper).rotate_left(64) | Bitvector<128>(lower); +} + +absl::StatusOr IsIpv6UnicastAddress(z3::expr ipv6_address) { + z3::expr result = p4_symbolic::Z3Context().bool_val(false); + ASSIGN_OR_RETURN(std::vector ranges, GetUnicastIpv6Ranges()); + for (auto& range : ranges) { + ASSIGN_OR_RETURN(z3::expr value, Ipv6AddressToZ3Bitvector(range.value)); + ASSIGN_OR_RETURN(z3::expr mask, + Ipv6PrefixLengthToZ3Mask(range.prefix_length)); + result = result || ((ipv6_address & mask) == value); + } + return result; +} +} // namespace + +// TODO: We need extra constraints to avoid generating packets +// the switch deams invalid and drops, such as "martian" packets. +// Ideally this switch behavior would be fully modeled in P4 instead, and this +// function would disappear. +absl::Status AddSanePacketConstraints( + p4_symbolic::symbolic::SolverState& state) { + ASSIGN_OR_RETURN(p4_symbolic::SaiFields ingress_fields, + p4_symbolic::GetSaiFields(state.context.ingress_headers)); + auto& ethernet = ingress_fields.headers.ethernet; + auto& ipv4 = ingress_fields.headers.ipv4; + auto& ipv6 = ingress_fields.headers.ipv6; + + // ======Ethernet constraints====== + // Use "locally administered", "individual" MAC addresses + // (U/L bit = 1, I/G bit = 0). + // TODO: A multicast MAC address is not a legal src_mac, but it + // is a legal dst_mac, thus applying the constraint only to the src_mac. If + // applied to dst_mac, the constraint would make some of the NDV6_PUNTFLOWs + // and VARIOUS_L3ADMIT_PUNTFLOWs unsatisfiable. Actually, the packets with + // multicast dst_mac addresses are indeed marked to drop in l3_admit, however + // such packets still continue to hit the acl_ingress table and some of the + // entries cause such packets to get punted. So we should not disallow the + // generation of such packets. + state.solver->add((ethernet.src_addr & Bitvector<48>(0x03'00'00'00'00'00)) == + Bitvector<48>(0x02'00'00'00'00'00)); + + for (auto& mac_address : {ethernet.src_addr, ethernet.dst_addr}) { + // Require key parts of the address to be nonzero to avoid corner cases. + auto nonzero_masks = std::vector({ + Bitvector<48>(0x00'FF'FF'00'00'00), // OUI + }); + for (auto& nonzero_mask : nonzero_masks) { + state.solver->add((mac_address & nonzero_mask) != 0); + } + } + // Require source MAC and destination MAC to differ. + state.solver->add(ethernet.src_addr != ethernet.dst_addr); + + // ======IPv4 constraints====== + // Avoid martian IP addresses. + // https://tools.ietf.org/html/rfc1122#section-3.2.1.3 + state.solver->add((ipv4.src_addr & Bitvector<32>(0xFF'00'00'00)) != 0); + // Src IP address cannot be 255.255.255.255 (broadcast). + state.solver->add(ipv4.src_addr != Bitvector<32>(0xFF'FF'FF'FF)); + // Neither src nor dst IPv4 addresses can be 0. + state.solver->add(ipv4.src_addr != Bitvector<32>(0)); + state.solver->add(ipv4.dst_addr != Bitvector<32>(0)); + // Neither src nor dst IPv4 addresses can be 127.0.0.1 (loopback). + state.solver->add(ipv4.src_addr != Bitvector<32>(0x7F'00'00'01)); + state.solver->add(ipv4.dst_addr != Bitvector<32>(0x7F'00'00'01)); + + // ======Ipv6 constraints====== + // Src IP address should be a unicast address. + { + ASSIGN_OR_RETURN(z3::expr constraint, IsIpv6UnicastAddress(ipv6.src_addr)); + state.solver->add(constraint); + } + // Neither src nor dst IPv6 addresses can be 0. + state.solver->add(ipv6.src_addr != Bitvector<128>(0)); + state.solver->add(ipv6.dst_addr != Bitvector<128>(0)); + // Neither src nor dst IPv4 addresses can be ::1 (loopback). + state.solver->add(ipv6.src_addr != Bitvector<128>(1)); + state.solver->add(ipv6.dst_addr != Bitvector<128>(1)); + + return absl::OkStatus(); +} + +absl::StatusOr IrValueToZ3Bitvector(const pdpi::IrValue& value, + int bitwidth) { + ASSIGN_OR_RETURN(const std::string bytes, + pdpi::IrValueToNormalizedByteString(value, bitwidth)); + const std::string hex_string = pdpi::ByteStringToHexString(bytes); + return HexStringToZ3Bitvector(hex_string, bitwidth); +} + +// The following functions return Z3 constraints corresponding to `field` +// matching the given pdpi::IrMatch value. +absl::StatusOr GetFieldMatchConstraints(z3::expr field, int bitwidth, + const pdpi::IrValue& match) { + ASSIGN_OR_RETURN(z3::expr value, IrValueToZ3Bitvector(match, bitwidth)); + return Eq(field, value); +} +absl::StatusOr GetFieldMatchConstraints( + z3::expr field, int bitwidth, const pdpi::IrMatch::IrLpmMatch& match) { + ASSIGN_OR_RETURN(z3::expr value, + IrValueToZ3Bitvector(match.value(), bitwidth)); + return PrefixEq(field, value, + static_cast(match.prefix_length())); +} +absl::StatusOr GetFieldMatchConstraints( + z3::expr field, int bitwidth, const pdpi::IrMatch::IrTernaryMatch& match) { + ASSIGN_OR_RETURN(z3::expr value, + IrValueToZ3Bitvector(match.value(), bitwidth)); + ASSIGN_OR_RETURN(z3::expr mask, IrValueToZ3Bitvector(match.mask(), bitwidth)); + ASSIGN_OR_RETURN(z3::expr masked_field, BitAnd(field, mask)); + return Eq(masked_field, value); +} +absl::StatusOr GetFieldMatchConstraints(z3::expr field, int bitwidth, + const pdpi::IrMatch& match) { + switch (match.match_value_case()) { + case pdpi::IrMatch::kExact: + return GetFieldMatchConstraints(field, bitwidth, match.exact()); + case pdpi::IrMatch::kLpm: + return GetFieldMatchConstraints(field, bitwidth, match.lpm()); + case pdpi::IrMatch::kTernary: + return GetFieldMatchConstraints(field, bitwidth, match.ternary()); + default: + return gutil::InvalidArgumentErrorBuilder() + << "Unsupported IR match type in " << match.ShortDebugString(); + } +} + +// Extract the header field defition of a `field_ref` from the given P4 +// `program`. +absl::StatusOr GetFieldDefinition( + const P4Program& program, absl::string_view field_ref) { + // Split the field reference into header and field names. + std::vector split = absl::StrSplit(field_ref, '.'); + if (split.size() != 2) { + return absl::InvalidArgumentError( + absl::Substitute("Expected
. got '$0'", field_ref)); + } + const std::string& header_name = split[0]; + const std::string& field_name = split[1]; + + // Extract the header definition from the program. + if (!program.headers().contains(header_name)) { + return absl::InvalidArgumentError( + absl::Substitute("Unexpected header instance'$0'", header_name)); + } + const p4_symbolic::ir::HeaderType& header_def = + program.headers().at(header_name); + + // Extract the field definition from the header definition. + if (!header_def.fields().contains(field_name)) { + return absl::InvalidArgumentError(absl::Substitute( + "Unexpected field'$0' in header '$1'", field_name, header_name)); + } + return header_def.fields().at(field_name); +} + +absl::StatusOr GetFieldBitwidth( + absl::string_view field_name, const p4_symbolic::ir::P4Program& program) { + if (absl::EndsWith(field_name, ".$valid$")) { + return 1; + } else { + ASSIGN_OR_RETURN(const p4_symbolic::ir::HeaderField field_definition, + GetFieldDefinition(program, field_name)); + return field_definition.bitwidth(); + } +} + +} // namespace packet_synthesizer +} // namespace p4_symbolic diff --git a/p4_symbolic/packet_synthesizer/util.h b/p4_symbolic/packet_synthesizer/util.h new file mode 100644 index 00000000..f864c607 --- /dev/null +++ b/p4_symbolic/packet_synthesizer/util.h @@ -0,0 +1,70 @@ +// Copyright 2024 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#ifndef PINS_P4_SYMBOLIC_PACKET_SYNTHESIZER_UTIL_H_ +#define PINS_P4_SYMBOLIC_PACKET_SYNTHESIZER_UTIL_H_ + +#include "absl/status/status.h" +#include "p4_symbolic/symbolic/symbolic.h" + +// This file contains varrious utility functions and classes used by packet +// synthesizer. + +namespace p4_symbolic::packet_synthesizer { + +// TODO: We need extra constraints to avoid generating packets +// the switch deams invalid and drops, such as "martian" packets. +// Ideally this switch behavior would be fully modeled in P4 instead, and this +// function would disappear. +absl::Status AddSanePacketConstraints( + p4_symbolic::symbolic::SolverState& state); + +// A simple timer implementation. +// TODO: Move this to third_party/pins_infra/gutil/timer +class Timer { + public: + // Returns the duration between the current time and the last reset (or + // initialization). + absl::Duration GetDuration() { return absl::Now() - start_time_; } + // Same as GetDuration. Resets the timer as well. + absl::Duration GetDurationAndReset() { + auto duration = GetDuration(); + Reset(); + return duration; + } + // Subsequent calls to GetDuration will measure the duration between the last + // call to Reset and those calls. + void Reset() { start_time_ = absl::Now(); } + + private: + absl::Time start_time_ = absl::Now(); +}; + +// Turns a given IrValue into equivalent Z3 bitvector with length `bitwidth`. +absl::StatusOr IrValueToZ3Bitvector(const pdpi::IrValue& value, + int bitwidth); + +// Return Z3 constraints corresponding to `field` matching the given +// pdpi::IrMatch value assuming the field's size is `bitwidth`. +absl::StatusOr GetFieldMatchConstraints(z3::expr field, int bitwidth, + const pdpi::IrMatch& match); + +// Extracts the bitwidth of the field with name `field_name` in the given +// `program`. +absl::StatusOr GetFieldBitwidth(absl::string_view field_name, + const p4_symbolic::ir::P4Program& program); + +} // namespace p4_symbolic::packet_synthesizer + +#endif // PINS_P4_SYMBOLIC_PACKET_SYNTHESIZER_UTIL_H_ diff --git a/p4_symbolic/packet_synthesizer/util_test.cc b/p4_symbolic/packet_synthesizer/util_test.cc new file mode 100644 index 00000000..cfdff94f --- /dev/null +++ b/p4_symbolic/packet_synthesizer/util_test.cc @@ -0,0 +1,92 @@ +// Copyright 2024 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#include "p4_symbolic/packet_synthesizer/util.h" + +#include "absl/status/status.h" +#include "gmock/gmock.h" +#include "gtest/gtest.h" +#include "gutil/status_matchers.h" +#include "gutil/testing.h" +#include "p4_symbolic/ir/ir.pb.h" + +namespace p4_symbolic::packet_synthesizer { +namespace { + +using ::testing::Gt; +using ::testing::Lt; + +TEST(TimerTest, GetDurationReturnsApproximatelyCorrectDuration) { + Timer timer; + absl::SleepFor(absl::Milliseconds(1001)); + ASSERT_THAT(timer.GetDuration(), Gt(absl::Milliseconds(1000))); +} + +TEST(TimerTest, GetDurationAfterResetReturnsApproximatelyCorrectDuration) { + Timer timer; + absl::SleepFor(absl::Milliseconds(1000)); + timer.Reset(); + absl::SleepFor(absl::Milliseconds(1001)); + auto duration = timer.GetDuration(); + ASSERT_THAT(duration, Gt(absl::Milliseconds(1000))); + ASSERT_THAT(duration, Lt(absl::Milliseconds(2000))); +} + +TEST(TimerTest, + GetDurationAndResetReturnsApproximatelyCorrectDurationAndResets) { + Timer timer; + absl::SleepFor(absl::Milliseconds(1001)); + ASSERT_THAT(timer.GetDurationAndReset(), Gt(absl::Milliseconds(1000))); + absl::SleepFor(absl::Milliseconds(1001)); + auto duration = timer.GetDuration(); + ASSERT_THAT(duration, Gt(absl::Milliseconds(1000))); + ASSERT_THAT(duration, Lt(absl::Milliseconds(2000))); +} + +TEST(GetFieldBitwidthTest, FailsForSyntacticallyIncorrectInput) { + ir::P4Program program; + ASSERT_THAT(GetFieldBitwidth("a.b.c.d", program), + gutil::StatusIs(absl::StatusCode::kInvalidArgument)); +} + +TEST(GetFieldBitwidthTest, FailsForNonExistingHeader) { + ir::P4Program program; + ASSERT_THAT(GetFieldBitwidth("dummy_header.dummy_field", program), + gutil::StatusIs(absl::StatusCode::kInvalidArgument)); +} + +TEST(GetFieldBitwidthTest, FailsForNonExistingField) { + ir::P4Program program; + (*program.mutable_headers())["dummy_header"] = ir::HeaderType(); + ASSERT_THAT(GetFieldBitwidth("dummy_header.dummy_field", program), + gutil::StatusIs(absl::StatusCode::kInvalidArgument)); +} + +TEST(GetFieldBitwidthTest, YieldCorrectFieldBitwidth) { + auto program = gutil::ParseProtoOrDie(R"pb( + headers { + key: "dummy_header" + value { + fields { + key: "dummy_field" + value { bitwidth: 10 } + } + } + })pb"); + ASSERT_THAT(GetFieldBitwidth("dummy_header.dummy_field", program), + gutil::IsOkAndHolds(testing::Eq(10))); +} + +} // namespace +} // namespace p4_symbolic::packet_synthesizer From 9efd5890f6aaf1efc57bae450644db983bdf23c9 Mon Sep 17 00:00:00 2001 From: VSuryaprasad-HCL Date: Wed, 6 Nov 2024 18:30:46 +0530 Subject: [PATCH 2/3] [P4_Symbolic] Adding p4_symbolic/packet_synthesizer/packet_synthesis_criteria files --- p4_symbolic/packet_synthesizer/BUILD.bazel | 35 ++++++ .../packet_synthesis_criteria.cc | 78 ++++++++++++ .../packet_synthesis_criteria.h | 40 ++++++ .../packet_synthesis_criteria.proto | 84 +++++++++++++ .../packet_synthesis_criteria_test.cc | 117 ++++++++++++++++++ 5 files changed, 354 insertions(+) create mode 100644 p4_symbolic/packet_synthesizer/packet_synthesis_criteria.cc create mode 100644 p4_symbolic/packet_synthesizer/packet_synthesis_criteria.h create mode 100644 p4_symbolic/packet_synthesizer/packet_synthesis_criteria.proto create mode 100644 p4_symbolic/packet_synthesizer/packet_synthesis_criteria_test.cc diff --git a/p4_symbolic/packet_synthesizer/BUILD.bazel b/p4_symbolic/packet_synthesizer/BUILD.bazel index 753e3531..17df1cbf 100644 --- a/p4_symbolic/packet_synthesizer/BUILD.bazel +++ b/p4_symbolic/packet_synthesizer/BUILD.bazel @@ -48,6 +48,17 @@ cc_test( ], ) +proto_library( + name = "packet_synthesis_criteria_proto", + srcs = ["packet_synthesis_criteria.proto"], + deps = ["//p4_pdpi:ir_proto"], +) + +cc_proto_library( + name = "packet_synthesis_criteria_cc_proto", + deps = [":packet_synthesis_criteria_proto"], +) + proto_library( name = "packet_synthesizer_proto", srcs = ["packet_synthesizer.proto"], @@ -62,3 +73,27 @@ cc_proto_library( deps = [":packet_synthesizer_proto"], ) +cc_library( + name = "packet_synthesis_criteria", + srcs = ["packet_synthesis_criteria.cc"], + hdrs = ["packet_synthesis_criteria.h"], + deps = [ + ":packet_synthesis_criteria_cc_proto", + "//gutil:status", + "@com_google_absl//absl/status:statusor", + "@com_google_protobuf//:protobuf", + ], +) + +cc_test( + name = "packet_synthesis_criteria_test", + srcs = ["packet_synthesis_criteria_test.cc"], + deps = [ + ":packet_synthesis_criteria", + ":packet_synthesis_criteria_cc_proto", + "//gutil:proto_matchers", + "//gutil:status_matchers", + "//gutil:testing", + "@com_google_googletest//:gtest_main", + ], +) diff --git a/p4_symbolic/packet_synthesizer/packet_synthesis_criteria.cc b/p4_symbolic/packet_synthesizer/packet_synthesis_criteria.cc new file mode 100644 index 00000000..fd736480 --- /dev/null +++ b/p4_symbolic/packet_synthesizer/packet_synthesis_criteria.cc @@ -0,0 +1,78 @@ +// Copyright 2024 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#include "p4_symbolic/packet_synthesizer/packet_synthesis_criteria.h" + +#include "google/protobuf/util/message_differencer.h" +#include "gutil/status.h" + +namespace p4_symbolic::packet_synthesizer { + +bool Equals(const CriteriaVariant& lhs, const CriteriaVariant& rhs) { + return google::protobuf::util::MessageDifferencer::Equals(lhs, rhs); +} + +absl::StatusOr GetCriteriaVariant( + const PacketSynthesisCriteria& criteria, + CriteriaVariant::CriteriaCase criteria_case) { + CriteriaVariant criteria_variant; + switch (criteria_case) { + case CriteriaVariant::kOutputCriteria: + if (criteria.has_output_criteria()) { + *criteria_variant.mutable_output_criteria() = + criteria.output_criteria(); + } + break; + case CriteriaVariant::kInputPacketHeaderCriteria: + if (criteria.has_input_packet_header_criteria()) { + *criteria_variant.mutable_input_packet_header_criteria() = + criteria.input_packet_header_criteria(); + } + break; + case CriteriaVariant::kTableReachabilityCriteria: + if (criteria.has_table_reachability_criteria()) { + *criteria_variant.mutable_table_reachability_criteria() = + criteria.table_reachability_criteria(); + } + break; + case CriteriaVariant::kTableEntryReachabilityCriteria: + if (criteria.has_table_entry_reachability_criteria()) { + *criteria_variant.mutable_table_entry_reachability_criteria() = + criteria.table_entry_reachability_criteria(); + } + break; + case CriteriaVariant::kPayloadCriteria: + if (criteria.has_payload_criteria()) { + *criteria_variant.mutable_payload_criteria() = + criteria.payload_criteria(); + } + break; + default: + return gutil::InvalidArgumentErrorBuilder() + << "Unexpected criteria case " << criteria_case; + } + return criteria_variant; +} + +absl::StatusOr HaveEqualCriteriaVariants( + const PacketSynthesisCriteria& lhs, const PacketSynthesisCriteria& rhs, + CriteriaVariant::CriteriaCase criteria_case) { + ASSIGN_OR_RETURN(const auto lhs_variant, + GetCriteriaVariant(lhs, criteria_case)); + ASSIGN_OR_RETURN(const auto rhs_variant, + GetCriteriaVariant(rhs, criteria_case)); + return Equals(lhs_variant, rhs_variant); +} + +} // namespace p4_symbolic::packet_synthesizer diff --git a/p4_symbolic/packet_synthesizer/packet_synthesis_criteria.h b/p4_symbolic/packet_synthesizer/packet_synthesis_criteria.h new file mode 100644 index 00000000..6b3c3b02 --- /dev/null +++ b/p4_symbolic/packet_synthesizer/packet_synthesis_criteria.h @@ -0,0 +1,40 @@ +// Copyright 2024 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#ifndef PINS_P4_SYMBOLIC_PACKET_SYNTHESIZER_PACKET_SYNTHESIS_CRITERIA_H_ +#define PINS_P4_SYMBOLIC_PACKET_SYNTHESIZER_PACKET_SYNTHESIS_CRITERIA_H_ + +#include "absl/status/statusor.h" +#include "p4_symbolic/packet_synthesizer/packet_synthesis_criteria.pb.h" + +namespace p4_symbolic::packet_synthesizer { + +// Returns whether two CriteriaVariants are considered equal. +bool Equals(const CriteriaVariant& lhs, const CriteriaVariant& rhs); + +// Get a single CriteriaVariant corresponding to the given `criteria_case` in +// the given `criteria`. +absl::StatusOr GetCriteriaVariant( + const PacketSynthesisCriteria& criteria, + CriteriaVariant::CriteriaCase criteria_case); + +// Checks whether `lhs` and `rhs` have equal criteria variants corresponding +// to the given `criteria_case`. +absl::StatusOr HaveEqualCriteriaVariants( + const PacketSynthesisCriteria& lhs, const PacketSynthesisCriteria& rhs, + CriteriaVariant::CriteriaCase criteria_case); + +} // namespace p4_symbolic::packet_synthesizer + +#endif // PINS_P4_SYMBOLIC_PACKET_SYNTHESIZER_PACKET_SYNTHESIS_CRITERIA_H_ diff --git a/p4_symbolic/packet_synthesizer/packet_synthesis_criteria.proto b/p4_symbolic/packet_synthesizer/packet_synthesis_criteria.proto new file mode 100644 index 00000000..a32ff1cd --- /dev/null +++ b/p4_symbolic/packet_synthesizer/packet_synthesis_criteria.proto @@ -0,0 +1,84 @@ +// Copyright 2024 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +syntax = "proto3"; + +package p4_symbolic.packet_synthesizer; + +import "p4_pdpi/ir.proto"; + +// Criteria stating the synthesized packet must reach and match a certain table +// entry. +message TableEntryReachabilityCriteria { + // The table containing the entry that must be matched. + string table_name = 1; + // The index of the entry (in descending order of priority, starting from 0) + // that must match the packet. -1 indicates default action (i.e. no match). + int32 match_index = 2; +} + +// Criteria stateing the synthesized packet must reach a certain table. +message TableReachabilityCriteria { + // The table that must be reachable. + string table_name = 1; +} + +// Criteria for the output behavior for the synthesized packet. +message OutputCriteria { + // Whether the packet must get dropped. + bool drop_expected = 1; +} + +// Criteria on fields of a packet's header. +message HeaderCriteria { + // Constraint for a single header field. + message FieldCriterion { + // Constraint in form of a match on a header field. + pdpi.IrMatch field_match = 1; + // Whether the constraint should be negated. + bool negated = 2; + } + // List of constraints on header fields. They must all be satisfied (i.e. the + // resulting criteria is the conjunction of individual constraints). + repeated FieldCriterion field_criteria = 1; +} + +// Criteria on the paypload of the synthesized packet. +// TODO: Set the payload in the client side. +message PayloadCriteria { + // The payload to be attached to the synthesized packet. + string payload = 1; +} + +// The coverage criteria for (single) packet synthesis. All fields are optional. +// If a criterion is not provided, no constraints for that criterion will be +// added. +message PacketSynthesisCriteria { + OutputCriteria output_criteria = 1; + HeaderCriteria input_packet_header_criteria = 2; + TableReachabilityCriteria table_reachability_criteria = 3; + TableEntryReachabilityCriteria table_entry_reachability_criteria = 4; + PayloadCriteria payload_criteria = 5; +} + +// Contains a single (type of) criteria. +message CriteriaVariant { + oneof criteria { + OutputCriteria output_criteria = 1; + HeaderCriteria input_packet_header_criteria = 2; + TableReachabilityCriteria table_reachability_criteria = 3; + TableEntryReachabilityCriteria table_entry_reachability_criteria = 4; + PayloadCriteria payload_criteria = 5; + } +} diff --git a/p4_symbolic/packet_synthesizer/packet_synthesis_criteria_test.cc b/p4_symbolic/packet_synthesizer/packet_synthesis_criteria_test.cc new file mode 100644 index 00000000..de3baf2f --- /dev/null +++ b/p4_symbolic/packet_synthesizer/packet_synthesis_criteria_test.cc @@ -0,0 +1,117 @@ +#include "p4_symbolic/packet_synthesizer/packet_synthesis_criteria.h" + +#include "gmock/gmock.h" +#include "gtest/gtest.h" +#include "gutil/proto_matchers.h" +#include "gutil/status_matchers.h" +#include "gutil/testing.h" +#include "p4_symbolic/packet_synthesizer/packet_synthesis_criteria.pb.h" + +namespace p4_symbolic::packet_synthesizer { +namespace { +using ::gutil::EqualsProto; +using ::gutil::IsOkAndHolds; + +TEST(GetCriteriaVariantTest, EmptyCriteriaYieldsEmptyVariant) { + PacketSynthesisCriteria criteria; + CriteriaVariant variant; + + for (const auto criteria_case : { + CriteriaVariant::kTableEntryReachabilityCriteria, + CriteriaVariant::kTableReachabilityCriteria, + CriteriaVariant::kOutputCriteria, + CriteriaVariant::kInputPacketHeaderCriteria, + CriteriaVariant::kPayloadCriteria, + }) { + ASSERT_THAT(GetCriteriaVariant(criteria, criteria_case), + IsOkAndHolds(EqualsProto(variant))); + } +} + +TEST(GetCriteriaVariantTest, + YieldsCorrectVariantForTableEntryReachabilityCriteria) { + auto table_entry_reachablity_criteria = + gutil::ParseProtoOrDie( + R"pb(table_name: "dummy" match_index: 10)pb"); + + PacketSynthesisCriteria criteria; + *criteria.mutable_table_entry_reachability_criteria() = + table_entry_reachablity_criteria; + + CriteriaVariant expected_variant; + *expected_variant.mutable_table_entry_reachability_criteria() = + table_entry_reachablity_criteria; + + ASSERT_THAT(GetCriteriaVariant( + criteria, CriteriaVariant::kTableEntryReachabilityCriteria), + IsOkAndHolds(EqualsProto(expected_variant))); +} + +TEST(GetCriteriaVariantTest, YieldsCorrectVariantForTableReachabilityCriteria) { + auto table_reachablity_criteria = + gutil::ParseProtoOrDie( + R"pb(table_name: "dummy")pb"); + + PacketSynthesisCriteria criteria; + *criteria.mutable_table_reachability_criteria() = table_reachablity_criteria; + + CriteriaVariant expected_variant; + *expected_variant.mutable_table_reachability_criteria() = + table_reachablity_criteria; + + ASSERT_THAT( + GetCriteriaVariant(criteria, CriteriaVariant::kTableReachabilityCriteria), + IsOkAndHolds(EqualsProto(expected_variant))); +} + +TEST(GetCriteriaVariantTest, YieldsCorrectVariantForOutputCriteria) { + auto output_criteria = + gutil::ParseProtoOrDie(R"pb(drop_expected: true)pb"); + + PacketSynthesisCriteria criteria; + *criteria.mutable_output_criteria() = output_criteria; + + CriteriaVariant expected_variant; + *expected_variant.mutable_output_criteria() = output_criteria; + + ASSERT_THAT(GetCriteriaVariant(criteria, CriteriaVariant::kOutputCriteria), + IsOkAndHolds(EqualsProto(expected_variant))); +} + +TEST(GetCriteriaVariantTest, YieldsCorrectVariantForInputPacketHeaderCriteria) { + auto input_header_criteria = + gutil::ParseProtoOrDie(R"pb(field_criteria { + field_match { + name: "dummy.field" + exact { str: "dummy" } + } + })pb"); + + PacketSynthesisCriteria criteria; + *criteria.mutable_input_packet_header_criteria() = input_header_criteria; + + CriteriaVariant expected_variant; + *expected_variant.mutable_input_packet_header_criteria() = + input_header_criteria; + + ASSERT_THAT( + GetCriteriaVariant(criteria, CriteriaVariant::kInputPacketHeaderCriteria), + IsOkAndHolds(EqualsProto(expected_variant))); +} + +TEST(GetCriteriaVariantTest, YieldsCorrectVariantForPayloadCriteria) { + auto payload_cretia = + gutil::ParseProtoOrDie(R"pb(payload: "dummy")pb"); + + PacketSynthesisCriteria criteria; + *criteria.mutable_payload_criteria() = payload_cretia; + + CriteriaVariant expected_variant; + *expected_variant.mutable_payload_criteria() = payload_cretia; + + ASSERT_THAT(GetCriteriaVariant(criteria, CriteriaVariant::kPayloadCriteria), + IsOkAndHolds(EqualsProto(expected_variant))); +} + +} // namespace +} // namespace p4_symbolic::packet_synthesizer From ba328c326e407ce0998bc57564246c29ac06d7a4 Mon Sep 17 00:00:00 2001 From: VSuryaprasad-HCL Date: Thu, 7 Nov 2024 12:41:55 +0530 Subject: [PATCH 3/3] [P4_Symbolic] Add packet_synthesizer. --- .../packet_synthesizer/packet_synthesizer.cc | 374 ++++++++++++++++++ .../packet_synthesizer/packet_synthesizer.h | 147 +++++++ 2 files changed, 521 insertions(+) create mode 100644 p4_symbolic/packet_synthesizer/packet_synthesizer.cc create mode 100644 p4_symbolic/packet_synthesizer/packet_synthesizer.h diff --git a/p4_symbolic/packet_synthesizer/packet_synthesizer.cc b/p4_symbolic/packet_synthesizer/packet_synthesizer.cc new file mode 100644 index 00000000..6b272b37 --- /dev/null +++ b/p4_symbolic/packet_synthesizer/packet_synthesizer.cc @@ -0,0 +1,374 @@ +// Copyright 2024 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#include "p4_symbolic/packet_synthesizer/packet_synthesizer.h" + +#include +#include +#include +#include +#include +#include + +#include "absl/base/log_severity.h" +#include "absl/status/status.h" +#include "absl/status/statusor.h" +#include "absl/strings/match.h" +#include "absl/strings/str_split.h" +#include "absl/strings/string_view.h" +#include "absl/strings/substitute.h" +#include "absl/time/time.h" +#include "gutil/status.h" +#include "p4/v1/p4runtime.pb.h" +#include "p4_pdpi/ir.pb.h" +#include "p4_pdpi/packetlib/packetlib.h" +#include "p4_symbolic/ir/ir.pb.h" +#include "p4_symbolic/packet_synthesizer/packet_synthesis_criteria.h" +#include "p4_symbolic/packet_synthesizer/util.h" +#include "p4_symbolic/sai/deparser.h" +#include "p4_symbolic/sai/sai.h" +#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/z3_util.h" + +namespace p4_symbolic::packet_synthesizer { + +namespace { +using ::p4_symbolic::symbolic::SolverState; + +// Given a Z3 model, prepares a SynthesizedPacket by extracting the relevant +// fields from the model. The packet payload will be set to the contents of +// `packet_payload` parameter. +absl::StatusOr SynthesizePacketFromZ3Model( + const p4_symbolic::symbolic::SolverState& solver_state, + absl::string_view packet_payload, bool should_be_dropped) { + z3::model model = solver_state.solver->get_model(); + ASSIGN_OR_RETURN( + std::string raw_packet, + p4_symbolic::SaiDeparser(solver_state.context.ingress_headers, model)); + packetlib::Packet packet = packetlib::ParsePacket(raw_packet); + ASSIGN_OR_RETURN( + const bool dropped, + p4_symbolic::EvalZ3Bool(solver_state.context.trace.dropped, model)); + if (dropped != should_be_dropped) { + return absl::FailedPreconditionError(absl::Substitute( + "Z3 model's drop prediction ($0) is inconsistent with the expectation " + "($1)", + dropped ? "drop" : "no drop", should_be_dropped ? "drop" : "no drop")); + } + ASSIGN_OR_RETURN( + const bool got_cloned, + p4_symbolic::EvalZ3Bool(solver_state.context.trace.got_cloned, model)); + ASSIGN_OR_RETURN( + p4_symbolic::SaiFields egress_fields, + p4_symbolic::GetSaiFields(solver_state.context.egress_headers)); + ASSIGN_OR_RETURN( + const bool mirrored, + p4_symbolic::EvalZ3Bool( + egress_fields.local_metadata.mirror_session_id_valid == 1, model)); + + // Get ingress port from the model. + ASSIGN_OR_RETURN( + std::string local_metadata_ingress_port, + p4_symbolic::ExtractLocalMetadataIngressPortFromModel(solver_state)); + + // TODO: p4-symbolic might miss that + // local_metadata.ingress_port is p4runtime_translated. In such cases, + // p4-symbolic returns the raw Z3 bitvector value. As a hacky workaround, + // we assign the empty string ("") as the ingress port for such cases, + // signaling that no port is picked by the test generator. Note + // that we currently assume that local_metadata.ingress_port is a + // decimal string in normal cases. + if (absl::StartsWith(local_metadata_ingress_port, "#")) { + // Z3 raw value is detected. + local_metadata_ingress_port = ""; + } + + // Set packet payload. + // TODO: Move this logic to the client. + RET_CHECK(packet.payload().empty()) + << "where packet = " << packet.DebugString(); + *packet.mutable_payload() = packet_payload; + + // Avoid using bad next_header that causes packet to be dropped. + // TODO: Move this logic to the client. + RET_CHECK(packet.headers_size() > 0) + << "where packet = " << packet.DebugString(); + auto& last_header = *packet.mutable_headers(packet.headers_size() - 1); + if (last_header.ipv6_header().next_header() == "0x00") { + // Use protocol number reserved for experimentation/testing (RFC3692). + last_header.mutable_ipv6_header()->set_next_header( + packetlib::IpNextHeader(253)); + } else if (last_header.ipv4_header().protocol() == "0x00") { + // Use protocol number reserved for experimentation/testing (RFC3692). + last_header.mutable_ipv4_header()->set_protocol(packetlib::IpProtocol(253)); + } + + SynthesizedPacket synthesized_packet; + *synthesized_packet.mutable_packet() = packet; + // Note that we get local_metadata.ingress_port as opposed to + // standard_metadata.ingress_port because the former is how the + // controller views the ports. Refer to + // third_party/pins_infra/sai_p4/fixed/metadata.p4 for more info. + synthesized_packet.set_ingress_port(local_metadata_ingress_port); + // Currently, p4-symbolic has no generic, built-in support for + // prediciting whether a packet gets dropped and/or punted to the + // controller. As a workaround, we hard-code some program-specific + // predictions here; they may break in the future when the program + // changes. + // + // The hard-coded predictions work as follows: + // - We predict that a packet gets dropped iff (i) it got + // `mark_to_drop`'ed in the P4 program and (ii) it did not get + // mirrored. Criterion (ii) is needed because mirrored packets are + // not considered dropped, for the purposes of dataplane test. + // - We predict that a packet gets punted iff (i) it got cloned in + // the P4 program and (ii) it did not get mirrored. Criterion (ii) + // is needed because mirroring is implemented through cloning, but + // mirrored packets are not considered "punted" (as they are + // forwarded in the dataplane). Luckily we know that mirrored + // packets never get punted, so the prediction should be sound. + // + // TODO: these hard-coded predictions are major tech debt + // that has led to hard-to-debug problems in the past; replacing + // them with sound, generic predictions is high priority. + synthesized_packet.set_drop_expected(dropped && !mirrored); + synthesized_packet.set_punt_expected(got_cloned && !mirrored); + synthesized_packet.set_mirror_expected(mirrored); + + return synthesized_packet; +} + +// Adds logical assertions corresponding to the given `criteria` (for packet +// input header) to `solver_state`. +absl::Status AddConstraintsForInputPacketHeader(const HeaderCriteria& criteria, + SolverState& solver_state) { + // Loop over the list of field criteria, adding the constraints for each + // criteria to the frame. The overall constraint for `criteria` will + // effectively be the conjunction of the constraints for each + // `field_criterion`). + for (const HeaderCriteria::FieldCriterion& field_criterion : + criteria.field_criteria()) { + const pdpi::IrMatch& field_match = field_criterion.field_match(); + + // Get the symbolic expression representing the input packet header value of + // the field in the given field match. + ASSIGN_OR_RETURN(z3::expr field, solver_state.context.ingress_headers.Get( + field_match.name())); + + // Generate the constraint corresponding to the given field match. + ASSIGN_OR_RETURN( + const int bitwidth, + GetFieldBitwidth(field_match.name(), solver_state.program)); + ASSIGN_OR_RETURN(z3::expr constraint, + GetFieldMatchConstraints(field, bitwidth, field_match)); + + // Negate the constraint if needed. + if (field_criterion.negated()) { + constraint = !constraint; + } + // Add the constraint to the frame. + solver_state.solver->add(constraint); + } + return absl::OkStatus(); +} + +// The following functions add logical assertions to the current solver state +// corresponding to the given `criteria`. +absl::Status AddConstraints(const OutputCriteria& criteria, + SolverState& solver_state) { + solver_state.solver->add(criteria.drop_expected() + ? solver_state.context.trace.dropped + : !solver_state.context.trace.dropped); + return absl::OkStatus(); +} +absl::Status AddConstraints(const TableReachabilityCriteria& criteria, + SolverState& solver_state) { + const auto& table_name = criteria.table_name(); + const auto& match = solver_state.context.trace.matched_entries.at(table_name); + solver_state.solver->add(match.matched); + return absl::OkStatus(); +} +absl::Status AddConstraints(const TableEntryReachabilityCriteria& criteria, + SolverState& solver_state) { + const auto& table_name = criteria.table_name(); + auto& match = solver_state.context.trace.matched_entries.at(table_name); + solver_state.solver->add(match.entry_index == criteria.match_index()); + + return absl::OkStatus(); +} + +} // namespace + +absl::StatusOr> PacketSynthesizer::Create( + const PacketSynthesisParams& params) { + Timer timer; + + // Extract data from params. + const p4::v1::ForwardingPipelineConfig& config = params.pipeline_config(); + std::vector entries(params.pi_entries().begin(), + params.pi_entries().end()); + std::vector physical_ports(params.physical_port().begin(), + params.physical_port().end()); + p4_symbolic::symbolic::TranslationPerType translation_per_type; + for (const auto& [type_name, data] : params.translation_per_type()) { + p4_symbolic::symbolic::values::TranslationData translation; + translation.dynamic_translation = data.dynamic_translation(); + for (const auto& mapping : data.static_mapping()) { + translation.static_mapping.push_back( + {mapping.string_value(), mapping.integer_value()}); + } + translation_per_type.insert({type_name, translation}); + } + + // Evaluate P4 pipeline to get solver_state. + ASSIGN_OR_RETURN(auto solver_state, + p4_symbolic::EvaluateSaiPipeline( + config, entries, physical_ports, translation_per_type)); + + // TODO: Avoid generating packets that are always dropped. + RETURN_IF_ERROR(AddSanePacketConstraints(*solver_state)); + + LOG(INFO) << "Generated the SMT formula in " << timer.GetDuration(); + + // The p4-symbolic's solver_state contains the symbolic variables and the + // SMT formula corresponding to the inputs (P4 program, entries, etc.) passed + // to Create. + return absl::WrapUnique(new PacketSynthesizer(std::move(*solver_state))); +} + +absl::StatusOr PacketSynthesizer::SynthesizePacket( + const PacketSynthesisCriteria& criteria) { + PacketSynthesisResult result; + Timer timer; + + // Add synthesized packet criterion as Z3 assertions. Modify the incremental + // solver stack accordingly. + RETURN_IF_ERROR(PrepareZ3SolverStack(criteria)); + + // Solve the constraints and generate the packet if satisfiable. + if (solver_state_.solver->check() == z3::check_result::sat) { + ASSIGN_OR_RETURN(*result.mutable_synthesized_packet(), + SynthesizePacketFromZ3Model( + solver_state_, criteria.payload_criteria().payload(), + criteria.output_criteria().drop_expected())); + } + + VLOG(1) << absl::Substitute("SynthesizePacket finished in $0 for\n$1", + absl::FormatDuration(timer.GetDuration()), + criteria.ShortDebugString()); + return result; +} + +absl::Status PacketSynthesizer::PushSolverFrame() { + if (solver_frame_stack_size_ >= kSolverFrameStackOrder.size()) { + return absl::InternalError("Cannot push a new frame to full solver stack"); + } + solver_state_.solver->push(); + ++solver_frame_stack_size_; + + return absl::OkStatus(); +} + +absl::Status PacketSynthesizer::PopSolverFrames(int n) { + if (n < 1) { + return absl::InvalidArgumentError( + absl::StrCat("Expected positive number of frames, got ", n)); + } + + for (int i = 0; i < n; i++) { + if (solver_frame_stack_size_ == 0) { + return absl::InternalError("Cannot pop from empty solver stack"); + } + solver_state_.solver->pop(); + --solver_frame_stack_size_; + } + + return absl::OkStatus(); +} + +absl::Status PacketSynthesizer::AddFrameForCriteria( + CriteriaVariant::CriteriaCase criteria_case, + const PacketSynthesisCriteria& criteria) { + // Add a new frame. + RETURN_IF_ERROR(PushSolverFrame()); + + // Add the constraints for the given `criteria_case`. If the input + // `criteria` does not contain the corresponding criteria case, we add no + // constraints to the frame. + switch (criteria_case) { + case CriteriaVariant::kOutputCriteria: + if (criteria.has_output_criteria()) + return AddConstraints(criteria.output_criteria(), solver_state_); + break; + case CriteriaVariant::kInputPacketHeaderCriteria: + if (criteria.has_input_packet_header_criteria()) { + return AddConstraintsForInputPacketHeader( + criteria.input_packet_header_criteria(), solver_state_); + } + break; + case CriteriaVariant::kTableReachabilityCriteria: + if (criteria.has_table_reachability_criteria()) + return AddConstraints(criteria.table_reachability_criteria(), + solver_state_); + break; + case CriteriaVariant::kTableEntryReachabilityCriteria: + if (criteria.has_table_reachability_criteria()) + return AddConstraints(criteria.table_entry_reachability_criteria(), + solver_state_); + break; + default: + return gutil::InvalidArgumentErrorBuilder() + << "Unsupported criteria case " << criteria.ShortDebugString(); + } + + return absl::OkStatus(); +} + +absl::Status PacketSynthesizer::PrepareZ3SolverStack( + const PacketSynthesisCriteria& criteria) { + // Find the first index from which the stack needs to be poped. This is + // essentially the first index in which the currently encoded criteria is + // different from the requested criteria. + int pop_index = 0; + for (; pop_index < kSolverFrameStackOrder.size(); pop_index++) { + const CriteriaVariant::CriteriaCase criteria_case = + kSolverFrameStackOrder[pop_index]; + ASSIGN_OR_RETURN( + bool equal_variants, + HaveEqualCriteriaVariants(criteria, current_criteria_, criteria_case)); + if (!equal_variants) break; + } + + VLOG(1) << "Frame stack pop index is " << pop_index; + + // Pop the frames on top of pop_index (including itself). + RETURN_IF_ERROR(PopSolverFrames(kSolverFrameStackOrder.size() - pop_index)); + + // Push new frames. + while (solver_frame_stack_size_ < kSolverFrameStackOrder.size()) { + RETURN_IF_ERROR(AddFrameForCriteria( + kSolverFrameStackOrder[solver_frame_stack_size_], criteria)); + } + + if (solver_frame_stack_size_ != kSolverFrameStackOrder.size()) { + return absl::InternalError(absl::Substitute( + "Expected frame size of $0, got $1", kSolverFrameStackOrder.size(), + solver_frame_stack_size_)); + } + + current_criteria_ = criteria; + + return absl::OkStatus(); +} +} // namespace p4_symbolic::packet_synthesizer diff --git a/p4_symbolic/packet_synthesizer/packet_synthesizer.h b/p4_symbolic/packet_synthesizer/packet_synthesizer.h new file mode 100644 index 00000000..8f88c13b --- /dev/null +++ b/p4_symbolic/packet_synthesizer/packet_synthesizer.h @@ -0,0 +1,147 @@ +// Copyright 2024 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +#ifndef PINS_P4_SYMBOLIC_PACKET_SYNTHESIZER_PACKET_SYNTHESIZER_H_ +#define PINS_P4_SYMBOLIC_PACKET_SYNTHESIZER_PACKET_SYNTHESIZER_H_ + +#include +#include +#include +#include + +#include "p4/v1/p4runtime.pb.h" +#include "p4_symbolic/packet_synthesizer/packet_synthesis_criteria.pb.h" +#include "p4_symbolic/packet_synthesizer/packet_synthesizer.pb.h" +#include "p4_symbolic/symbolic/symbolic.h" + +namespace p4_symbolic::packet_synthesizer { + +// A high-level, stateful interface to packet synthesis via p4-symbolic. +// A PacketSynthesizer object can only be created through a call to `Create` +// with appropriate inputs (P4 program, table entries, etc.). +// Given an instance, one may call `SynthesizePacket` multiple times to +// synthesize packets satisfying the given input criteria (if possible). +// +// Example usage: +// ASSIGN_OR_RETURN(std::unique_ptr synthesizer, +// PacketSynthesizer::Create(config, entries, ports, translation); +// ASSIGN_OR_RETURN(PacketSynthesisResult result_1, +// synthesizer->SynthesizePacket(criteria_1)); +// ASSIGN_OR_RETURN(PacketSynthesisResult result_2, +// synthesizer->SynthesizePacket(criteria_2)); +// if (result_1.has_synthesized_packet()) {...} +// +// This class is NOT thread safe. Clients must serialize calls to +// `SynthesizePacket`. +// TODO: Due to p4-symbolic's use of a single global Z3 context, it +// is currently not safe to have more than once instance of this class per +// process. +class PacketSynthesizer { + public: + // Creates and initializes an instance of PacketSynthesizer given the + // input (the P4 program, table entries, etc.). Returns a unique pointer to + // the created object on success. The returned object keeps a state + // corresponding to the input of this function. + // + // This static function is the only way to create an instance of + // PacketSynthesizer. + static absl::StatusOr> Create( + const PacketSynthesisParams& params); + + // Attempts to synthesize and return a packet (if any) for the given + // `criteria`. + absl::StatusOr SynthesizePacket( + const PacketSynthesisCriteria& criteria); + + // Disallow copy and move. + PacketSynthesizer(const PacketSynthesizer&) = delete; + PacketSynthesizer(PacketSynthesizer&&) = delete; + PacketSynthesizer& operator=(const PacketSynthesizer&) = delete; + PacketSynthesizer& operator=(PacketSynthesizer&&) = delete; + + // The order of Z3 frames corresponding to different types of criteria. The + // criteria type in lower index will be lower in the stack. See + // `PrepareZ3SolverStack` for more details about the use of Z3 frames. The + // order is chosen based on empirical results and intuition. For example, we + // expect the client to change the drop_expectation less frequently than the + // table frame across the sequence of calls to SynthesizePackets because in + // the client the loop that iterates over tables is kept inside the loop that + // iterates over drop_expectations. This is because we have empirically + // observed that doing so (as opposed to the other way around) leads to better + // performance. + // Note that some types of criteria (e.g. PayloadCriteria) do not require Z3 + // constraints. Such criteria excluded from the stack and therefore the order. + // In the future, it might make sense for the client to specify the order. + const std::vector kSolverFrameStackOrder = { + CriteriaVariant::kOutputCriteria, + CriteriaVariant::kInputPacketHeaderCriteria, + CriteriaVariant::kTableReachabilityCriteria, + CriteriaVariant::kTableEntryReachabilityCriteria, + }; + + private: + // A PacketSynthesizer object may only be created through a (successful) call + // to Create. + explicit PacketSynthesizer(p4_symbolic::symbolic::SolverState&& solver_state) + : solver_state_(std::move(solver_state)) { + // Prepare the solver frame stack. + for (int i = 0; i < kSolverFrameStackOrder.size(); i++) { + solver_state_.solver->push(); + } + solver_frame_stack_size_ = kSolverFrameStackOrder.size(); + current_criteria_ = PacketSynthesisCriteria(); + } + + // The solver state. + p4_symbolic::symbolic::SolverState solver_state_; + + // The current criteria encoded in solver state (through the use of Z3 + // frames). + // Invariant: must truly reflect the constraints encoded in Z3. i.e. + // CriteriaToZ3Stack(current_criteria_) == solver.z3.current_stack. Empty + // criteria variants correspond to Z3 frames with no assertion. + PacketSynthesisCriteria current_criteria_; + // The number of Z3 frames pushed to the solver state. + // Invariant 1: must truly reflect the number of Z3 frames. + // Invariant 2: must be equal to kSolverFrameStackOrder.size() at the + // end of any (successful) call to `Create` and `SynthesizePacket`. This is + // because we push a frame (even if empty) for each member of + // kSolverFrameStackOrder. + int solver_frame_stack_size_ = 0; + + // Pushes a new (Z3) frame to the solver state. + absl::Status PushSolverFrame(); + // Pops `n` (Z3) frames from the solver state. Returns error if there aren't + // enough frames to pop. + absl::Status PopSolverFrames(int n = 1); + + // Adds a new (Z3) frame to the solver state, then adds logical assertions + // corresponding to the given `criteria_case` of the input `criteria`. + absl::Status AddFrameForCriteria(CriteriaVariant::CriteriaCase criteria_case, + const PacketSynthesisCriteria& criteria); + + // To use Z3's incremental solver and gain better performance, we keep logical + // constraints corresponding to different types of criteria in separate Z3 + // frames (the order of which is determined by kSolverFrameStackOrder). Across + // calls to SynthesizePacket, we adjust the frame stack only if needed. This + // function adjusts Z3's frame stack based on the previous and new values for + // packet synthesis criteria. If a part of the criteria is changed, the frames + // from the lowest changing criteria upward get popped and frames (and + // constraints) corresponding to the new values get pushed. + absl::Status PrepareZ3SolverStack(const PacketSynthesisCriteria& criteria); +}; + +} // namespace p4_symbolic::packet_synthesizer + +#endif // PINS_P4_SYMBOLIC_PACKET_SYNTHESIZER_PACKET_SYNTHESIZER_H_