From 1e5d8dcb0435375d6986a8840de8debd7cfb5301 Mon Sep 17 00:00:00 2001 From: kishanps Date: Fri, 23 Jun 2023 23:00:49 -0700 Subject: [PATCH 1/7] [P4-Symbolic] Use generic deparser to extract input/output packets --- p4_symbolic/BUILD.bazel | 17 ++ p4_symbolic/deparser.cc | 93 +++++++ p4_symbolic/{sai => }/deparser.h | 31 ++- p4_symbolic/{sai => }/deparser_test.cc | 162 ++--------- .../packet_synthesizer/packet_synthesizer.cc | 11 +- .../packet_synthesizer/packet_synthesizer.h | 3 - p4_symbolic/sai/deparser.cc | 254 ------------------ p4_symbolic/z3_util.cc | 118 ++++++++ p4_symbolic/z3_util.h | 35 +-- tests/sflow/sflow_test.cc | 89 ------ 10 files changed, 282 insertions(+), 531 deletions(-) create mode 100644 p4_symbolic/deparser.cc rename p4_symbolic/{sai => }/deparser.h (52%) rename p4_symbolic/{sai => }/deparser_test.cc (51%) delete mode 100644 p4_symbolic/sai/deparser.cc diff --git a/p4_symbolic/BUILD.bazel b/p4_symbolic/BUILD.bazel index b5898c29..4d097cce 100644 --- a/p4_symbolic/BUILD.bazel +++ b/p4_symbolic/BUILD.bazel @@ -63,6 +63,7 @@ cc_library( hdrs = ["z3_util.h"], deps = [ "//gutil:status", + "//p4_pdpi/string_encodings:bit_string", "//p4_pdpi/string_encodings:hex_string", "@com_github_z3prover_z3//:api", "@com_gnu_gmp//:gmp", @@ -71,6 +72,22 @@ cc_library( ], ) +cc_library( + name = "deparser", + srcs = ["deparser.cc"], + hdrs = ["deparser.h"], + deps = [ + ":z3_util", + "//gutil:status", + "//p4_pdpi/string_encodings:bit_string", + "//p4_symbolic/ir:ir_cc_proto", + "//p4_symbolic/symbolic", + "@com_github_z3prover_z3//:api", + "@com_google_absl//absl/status:statusor", + "@com_google_protobuf//:protobuf", + ], +) + cc_test( name = "z3_util_test", srcs = ["z3_util_test.cc"], diff --git a/p4_symbolic/deparser.cc b/p4_symbolic/deparser.cc new file mode 100644 index 00000000..c5d0ffad --- /dev/null +++ b/p4_symbolic/deparser.cc @@ -0,0 +1,93 @@ +// Copyright 2023 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/deparser.h" + +#include "google/protobuf/repeated_ptr_field.h" +#include "gutil/status.h" +#include "p4_pdpi/string_encodings/bit_string.h" +#include "p4_symbolic/ir/ir.pb.h" +#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/z3_util.h" + +namespace p4_symbolic { + +namespace { + +// Deparses the given symbolic `packet` into a byte string, using values +// according to the given `model`, with the given `header_order`. +absl::StatusOr Deparse( + const symbolic::SymbolicPerPacketState& packet, const z3::model& model, + const ::google::protobuf::RepeatedPtrField& header_order, + const ::google::protobuf::Map& headers) { + pdpi::BitString result; + + // Serialize each header to the bit-string from the outermost one to the + // innermost one. + for (const std::string& header_name : header_order) { + // The header specified in the header order must exist in the program. + auto it = headers.find(header_name); + if (it == headers.end()) { + return gutil::NotFoundErrorBuilder() + << "Header not found during deparsing: " << header_name; + } + + // Obtain the valid field of the header. Skip serializing the header if it's + // not valid. + ASSIGN_OR_RETURN(z3::expr valid_expr, + packet.Get(header_name, symbolic::kValidPseudoField)); + ASSIGN_OR_RETURN(bool valid, EvalZ3Bool(valid_expr, model)); + if (!valid) continue; + + const ir::HeaderType& header_type = it->second; + + // Serialize each field within the header to the bit-string. + for (const std::string& field_name : header_type.ordered_fields_list()) { + ASSIGN_OR_RETURN(z3::expr field_expr, + packet.Get(header_name, field_name)); + if (!field_expr.is_bv()) { + return gutil::InvalidArgumentErrorBuilder() + << "Header field '" << header_name << "." << field_name + << "' is not a bit-vector: " << field_expr; + } + + // Evaluate the concrete value of the field given the model. + RETURN_IF_ERROR( + EvalAndAppendZ3BitvectorToBitString(result, field_expr, model)); + } + } + + return result.ToByteString(); +} + +} // namespace + +absl::StatusOr DeparseIngressPacket( + const symbolic::SolverState& state, const z3::model& model) { + // TODO: We are using the deparser header order to serialize + // ingress packet for now. In the future, we may want to infer parser header + // order and use that for ingress packets. + const ir::Deparser& deparser = state.program.deparsers().begin()->second; + return Deparse(state.context.ingress_headers, model, deparser.header_order(), + state.program.headers()); +} + +absl::StatusOr DeparseEgressPacket( + const symbolic::SolverState& state, const z3::model& model) { + const ir::Deparser& deparser = state.program.deparsers().begin()->second; + return Deparse(state.context.egress_headers, model, deparser.header_order(), + state.program.headers()); +} + +} // namespace p4_symbolic diff --git a/p4_symbolic/sai/deparser.h b/p4_symbolic/deparser.h similarity index 52% rename from p4_symbolic/sai/deparser.h rename to p4_symbolic/deparser.h index 88c43f37..c16486e3 100644 --- a/p4_symbolic/sai/deparser.h +++ b/p4_symbolic/deparser.h @@ -11,25 +11,28 @@ // 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_SAI_DEPARSER_H_ -#define PINS_P4_SYMBOLIC_SAI_DEPARSER_H_ + +#ifndef P4_SYMBOLIC_DEPARSER_H_ +#define P4_SYMBOLIC_DEPARSER_H_ + +#include #include "absl/status/statusor.h" -#include "gutil/status.h" -#include "p4_pdpi/string_encodings/bit_string.h" -#include "p4_symbolic/sai/fields.h" #include "p4_symbolic/symbolic/symbolic.h" #include "z3++.h" namespace p4_symbolic { -// Deparses the given packet into a byte string, using values according to the -// given model. -absl::StatusOr -SaiDeparser(const symbolic::SymbolicPerPacketState &packet, - const z3::model &model); -absl::StatusOr SaiDeparser(const SaiFields &packet, - const z3::model &model); +// Deparses the ingress packet from the given symbolic solver `state` into a +// byte string, using values according to the given `model`. +absl::StatusOr DeparseIngressPacket( + const symbolic::SolverState& state, const z3::model& model); + +// Deparses the egress packet from the given symbolic solver `state` into a byte +// string, using values according to the given `model`. +absl::StatusOr DeparseEgressPacket( + const symbolic::SolverState& state, const z3::model& model); + +} // namespace p4_symbolic -} // namespace p4_symbolic -#endif // PINS_P4_SYMBOLIC_SAI_DEPARSER_H_ +#endif // P4_SYMBOLIC_DEPARSER_H_ diff --git a/p4_symbolic/sai/deparser_test.cc b/p4_symbolic/deparser_test.cc similarity index 51% rename from p4_symbolic/sai/deparser_test.cc rename to p4_symbolic/deparser_test.cc index a271f438..2fc166fb 100644 --- a/p4_symbolic/sai/deparser_test.cc +++ b/p4_symbolic/deparser_test.cc @@ -11,32 +11,20 @@ // 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/sai/deparser.h" + +#include "p4_symbolic/deparser.h" #include -#include -#include -#include -#include "absl/status/statusor.h" -#include "absl/strings/str_format.h" -#include "glog/logging.h" #include "gmock/gmock.h" #include "gtest/gtest.h" -#include "gutil/proto_matchers.h" -#include "gutil/status.h" #include "gutil/status_matchers.h" #include "p4/v1/p4runtime.pb.h" #include "p4_pdpi/packetlib/packetlib.h" #include "p4_pdpi/packetlib/packetlib.pb.h" -#include "p4_pdpi/string_encodings/bit_string.h" -#include "p4_pdpi/string_encodings/hex_string.h" -#include "p4_symbolic/parser.h" #include "p4_symbolic/sai/fields.h" -#include "p4_symbolic/sai/parser.h" #include "p4_symbolic/sai/sai.h" #include "p4_symbolic/symbolic/symbolic.h" -#include "p4_symbolic/z3_util.h" #include "sai_p4/instantiations/google/instantiations.h" #include "sai_p4/instantiations/google/sai_nonstandard_platforms.h" #include "z3++.h" @@ -44,8 +32,6 @@ namespace p4_symbolic { namespace { -using ::testing::IsEmpty; - class SaiDeparserTest : public testing::TestWithParam { public: void SetUp() override { @@ -63,20 +49,11 @@ class SaiDeparserTest : public testing::TestWithParam { TEST_P(SaiDeparserTest, DeparseIngressAndEgressHeadersWithoutConstraints) { ASSERT_EQ(state_->solver->check(), z3::check_result::sat); auto model = state_->solver->get_model(); - for (auto& packet : - {state_->context.ingress_headers, state_->context.egress_headers}) { - EXPECT_OK(SaiDeparser(packet, model).status()); - } + EXPECT_OK(DeparseIngressPacket(*state_, model).status()); + EXPECT_OK(DeparseEgressPacket(*state_, model).status()); } TEST_P(SaiDeparserTest, VlanPacketParserIntegrationTest) { - // Add parse constraints. - { - ASSERT_OK_AND_ASSIGN(auto parse_constraints, - EvaluateSaiParser(state_->context.ingress_headers)); - for (auto& constraint : parse_constraints) state_->solver->add(constraint); - } - // Add VLAN constraint. { ASSERT_OK_AND_ASSIGN(SaiFields fields, @@ -88,31 +65,23 @@ TEST_P(SaiDeparserTest, VlanPacketParserIntegrationTest) { ASSERT_EQ(state_->solver->check(), z3::check_result::sat); auto model = state_->solver->get_model(); ASSERT_OK_AND_ASSIGN(std::string raw_packet, - SaiDeparser(state_->context.ingress_headers, model)); + DeparseIngressPacket(*state_, model)); // Check we indeed got a VLAN packet. packetlib::Packet packet = packetlib::ParsePacket(raw_packet); LOG(INFO) << "Z3-generated packet = " << packet.DebugString(); ASSERT_GE(packet.headers_size(), 2); - ASSERT_TRUE(packet.headers(0).has_ethernet_header()); - ASSERT_TRUE(packet.headers(1).has_vlan_header()); + EXPECT_TRUE(packet.headers(0).has_ethernet_header()); + EXPECT_TRUE(packet.headers(1).has_vlan_header()); } TEST_P(SaiDeparserTest, Ipv4UdpPacketParserIntegrationTest) { - // Add parse constraints. - { - ASSERT_OK_AND_ASSIGN(auto parse_constraints, - EvaluateSaiParser(state_->context.ingress_headers)); - for (auto& constraint : parse_constraints) state_->solver->add(constraint); - } - // Add IPv4 + UDP (+ no VLAN) constraint. { ASSERT_OK_AND_ASSIGN(SaiFields fields, GetSaiFields(state_->context.ingress_headers)); state_->solver->add(fields.headers.ipv4.valid); state_->solver->add(fields.headers.udp.valid); - state_->solver->add(!fields.headers.vlan->valid); } @@ -120,26 +89,19 @@ TEST_P(SaiDeparserTest, Ipv4UdpPacketParserIntegrationTest) { ASSERT_EQ(state_->solver->check(), z3::check_result::sat); auto model = state_->solver->get_model(); ASSERT_OK_AND_ASSIGN(std::string raw_packet, - SaiDeparser(state_->context.ingress_headers, model)); + DeparseIngressPacket(*state_, model)); // Check we indeed got an IPv4 UDP packet. packetlib::Packet packet = packetlib::ParsePacket(raw_packet); LOG(INFO) << "Z3-generated packet = " << packet.DebugString(); ASSERT_GE(packet.headers_size(), 3); - ASSERT_TRUE(packet.headers(0).has_ethernet_header()); - ASSERT_TRUE(packet.headers(1).has_ipv4_header()); - ASSERT_TRUE(packet.headers(2).has_udp_header()); - ASSERT_THAT(packet.payload(), IsEmpty()); + EXPECT_TRUE(packet.headers(0).has_ethernet_header()); + EXPECT_TRUE(packet.headers(1).has_ipv4_header()); + EXPECT_TRUE(packet.headers(2).has_udp_header()); + EXPECT_THAT(packet.payload(), testing::IsEmpty()); } TEST_P(SaiDeparserTest, Ipv6TcpPacketParserIntegrationTest) { - // Add parse constraints. - { - ASSERT_OK_AND_ASSIGN(auto parse_constraints, - EvaluateSaiParser(state_->context.ingress_headers)); - for (auto& constraint : parse_constraints) state_->solver->add(constraint); - } - // Add IPv6 + TCP (+ no VLAN) constraint. { ASSERT_OK_AND_ASSIGN(SaiFields fields, @@ -155,26 +117,19 @@ TEST_P(SaiDeparserTest, Ipv6TcpPacketParserIntegrationTest) { ASSERT_EQ(state_->solver->check(), z3::check_result::sat); auto model = state_->solver->get_model(); ASSERT_OK_AND_ASSIGN(std::string raw_packet, - SaiDeparser(state_->context.ingress_headers, model)); + DeparseIngressPacket(*state_, model)); // Check we indeed got an IPv6 TCP packet. packetlib::Packet packet = packetlib::ParsePacket(raw_packet); LOG(INFO) << "Z3-generated packet = " << packet.DebugString(); ASSERT_GE(packet.headers_size(), 3); - ASSERT_TRUE(packet.headers(0).has_ethernet_header()); - ASSERT_TRUE(packet.headers(1).has_ipv6_header()); - ASSERT_TRUE(packet.headers(2).has_tcp_header()); - ASSERT_THAT(packet.payload(), IsEmpty()); + EXPECT_TRUE(packet.headers(0).has_ethernet_header()); + EXPECT_TRUE(packet.headers(1).has_ipv6_header()); + EXPECT_TRUE(packet.headers(2).has_tcp_header()); + EXPECT_THAT(packet.payload(), testing::IsEmpty()); } TEST_P(SaiDeparserTest, ArpPacketParserIntegrationTest) { - // Add parse constraints. - { - ASSERT_OK_AND_ASSIGN(auto parse_constraints, - EvaluateSaiParser(state_->context.ingress_headers)); - for (auto& constraint : parse_constraints) state_->solver->add(constraint); - } - // Add ARP (+ no VLAN) constraint. { ASSERT_OK_AND_ASSIGN(SaiFields fields, @@ -187,25 +142,18 @@ TEST_P(SaiDeparserTest, ArpPacketParserIntegrationTest) { ASSERT_EQ(state_->solver->check(), z3::check_result::sat); auto model = state_->solver->get_model(); ASSERT_OK_AND_ASSIGN(std::string raw_packet, - SaiDeparser(state_->context.ingress_headers, model)); + DeparseIngressPacket(*state_, model)); // Check we indeed got an ARP packet. packetlib::Packet packet = packetlib::ParsePacket(raw_packet); LOG(INFO) << "Z3-generated packet = " << packet.DebugString(); ASSERT_GE(packet.headers_size(), 2); - ASSERT_TRUE(packet.headers(0).has_ethernet_header()); - ASSERT_TRUE(packet.headers(1).has_arp_header()); - ASSERT_THAT(packet.payload(), IsEmpty()); + EXPECT_TRUE(packet.headers(0).has_ethernet_header()); + EXPECT_TRUE(packet.headers(1).has_arp_header()); + EXPECT_THAT(packet.payload(), testing::IsEmpty()); } TEST_P(SaiDeparserTest, IcmpPacketParserIntegrationTest) { - // Add parse constraints. - { - ASSERT_OK_AND_ASSIGN(auto parse_constraints, - EvaluateSaiParser(state_->context.ingress_headers)); - for (auto& constraint : parse_constraints) state_->solver->add(constraint); - } - // Add ICMP (+ no VLAN) constraint. { ASSERT_OK_AND_ASSIGN(SaiFields fields, @@ -218,27 +166,20 @@ TEST_P(SaiDeparserTest, IcmpPacketParserIntegrationTest) { ASSERT_EQ(state_->solver->check(), z3::check_result::sat); auto model = state_->solver->get_model(); ASSERT_OK_AND_ASSIGN(std::string raw_packet, - SaiDeparser(state_->context.ingress_headers, model)); + DeparseIngressPacket(*state_, model)); // Check we indeed got an ARP packet. packetlib::Packet packet = packetlib::ParsePacket(raw_packet); LOG(INFO) << "Z3-generated packet = " << packet.DebugString(); ASSERT_GE(packet.headers_size(), 3); - ASSERT_TRUE(packet.headers(0).has_ethernet_header()); - ASSERT_TRUE(packet.headers(1).has_ipv4_header() || + EXPECT_TRUE(packet.headers(0).has_ethernet_header()); + EXPECT_TRUE(packet.headers(1).has_ipv4_header() || packet.headers(1).has_ipv6_header()); - ASSERT_TRUE(packet.headers(2).has_icmp_header()); - ASSERT_THAT(packet.payload(), IsEmpty()); + EXPECT_TRUE(packet.headers(2).has_icmp_header()); + EXPECT_THAT(packet.payload(), testing::IsEmpty()); } TEST_P(SaiDeparserTest, PacketInHeaderIsNeverParsedIntegrationTest) { - // Add parse constraints. - { - ASSERT_OK_AND_ASSIGN(auto parse_constraints, - EvaluateSaiParser(state_->context.ingress_headers)); - for (auto& constraint : parse_constraints) state_->solver->add(constraint); - } - // Add packet_in constraint. { ASSERT_OK_AND_ASSIGN(SaiFields fields, @@ -248,60 +189,11 @@ TEST_P(SaiDeparserTest, PacketInHeaderIsNeverParsedIntegrationTest) { } // Should be unsatisfiable, because we never parse a packet-in header. - ASSERT_EQ(state_->solver->check(), z3::check_result::unsat); -} - -using SimpleSaiDeparserTest = testing::TestWithParam; - -TEST_P(SimpleSaiDeparserTest, PacketInHeaderDeparsingIsCorrect) { - // Set up. - z3::solver solver = z3::solver(Z3Context()); - const auto config = sai::GetNonstandardForwardingPipelineConfig( - /*instantiation=*/GetParam(), sai::NonstandardPlatform::kP4Symbolic); - ASSERT_OK_AND_ASSIGN(ir::Dataplane dataplane, - ParseToIr(config, /*entries=*/{})); - ASSERT_OK_AND_ASSIGN(auto headers, - symbolic::SymbolicGuardedMap::CreateSymbolicGuardedMap( - dataplane.program.headers())); - ASSERT_OK_AND_ASSIGN(SaiFields fields, GetSaiFields(headers)); - - // Add packet_in constraints. - EXPECT_TRUE(fields.headers.packet_in.has_value()); - solver.add(fields.headers.packet_in->valid); - constexpr int kIngressPort = 42; - constexpr int kTargetEgpressPort = 17; - constexpr int kUnusedPad = 0; - solver.add(fields.headers.packet_in->ingress_port == kIngressPort); - solver.add(fields.headers.packet_in->target_egress_port == - kTargetEgpressPort); - solver.add(fields.headers.packet_in->unused_pad == kUnusedPad); - packetlib::Header expected_header; - packetlib::SaiP4BMv2PacketInHeader& packet_in_header = - *expected_header.mutable_sai_p4_bmv2_packet_in_header(); - packet_in_header.set_ingress_port(pdpi::BitsetToHexString<9>(kIngressPort)); - packet_in_header.set_target_egress_port( - pdpi::BitsetToHexString<9>(kTargetEgpressPort)); - packet_in_header.set_unused_pad(pdpi::BitsetToHexString<6>(kUnusedPad)); - - // Solve and deparse. - ASSERT_EQ(solver.check(), z3::check_result::sat); - auto model = solver.get_model(); - ASSERT_OK_AND_ASSIGN(std::string raw_packet, SaiDeparser(headers, model)); - - // Check we indeed got a packet_in packet with the correct fields. - packetlib::Packet packet = packetlib::ParsePacket( - raw_packet, - /*first_header=*/packetlib::Header::kSaiP4Bmv2PacketInHeader); - LOG(INFO) << "Z3-generated packet = " << packet.DebugString(); - ASSERT_GT(packet.headers_size(), 0); - ASSERT_THAT(packet.headers(0), gutil::EqualsProto(expected_header)); + EXPECT_EQ(state_->solver->check(), z3::check_result::unsat); } INSTANTIATE_TEST_SUITE_P(SaiDeparserTest, SaiDeparserTest, testing::ValuesIn(sai::AllSaiInstantiations())); -INSTANTIATE_TEST_SUITE_P(SimpleSaiDeparserTest, SimpleSaiDeparserTest, - testing::ValuesIn(sai::AllSaiInstantiations())); - } // namespace } // namespace p4_symbolic diff --git a/p4_symbolic/packet_synthesizer/packet_synthesizer.cc b/p4_symbolic/packet_synthesizer/packet_synthesizer.cc index bb1827c2..62089343 100644 --- a/p4_symbolic/packet_synthesizer/packet_synthesizer.cc +++ b/p4_symbolic/packet_synthesizer/packet_synthesizer.cc @@ -33,10 +33,11 @@ #include "p4/v1/p4runtime.pb.h" #include "p4_pdpi/ir.pb.h" #include "p4_pdpi/packetlib/packetlib.h" +#include "p4_symbolic/deparser.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/fields.h" #include "p4_symbolic/sai/sai.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/symbolic/util.h" @@ -54,10 +55,8 @@ 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(std::string packet, + p4_symbolic::DeparseIngressPacket(solver_state, model)); ASSIGN_OR_RETURN( const bool dropped, p4_symbolic::EvalZ3Bool(solver_state.context.trace.dropped, model)); @@ -123,7 +122,7 @@ absl::StatusOr SynthesizePacketFromZ3Model( // 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 + // predicting 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. diff --git a/p4_symbolic/packet_synthesizer/packet_synthesizer.h b/p4_symbolic/packet_synthesizer/packet_synthesizer.h index 23f4ed74..600bd56f 100644 --- a/p4_symbolic/packet_synthesizer/packet_synthesizer.h +++ b/p4_symbolic/packet_synthesizer/packet_synthesizer.h @@ -16,11 +16,8 @@ #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" diff --git a/p4_symbolic/sai/deparser.cc b/p4_symbolic/sai/deparser.cc deleted file mode 100644 index 6d89f19f..00000000 --- a/p4_symbolic/sai/deparser.cc +++ /dev/null @@ -1,254 +0,0 @@ -// 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/sai/deparser.h" - -#include - -#include -#include - -#include "absl/status/status.h" -#include "absl/status/statusor.h" -#include "gutil/status.h" -#include "p4_pdpi/string_encodings/bit_string.h" -#include "p4_symbolic/sai/fields.h" -#include "p4_symbolic/symbolic/symbolic.h" -#include "p4_symbolic/z3_util.h" -#include "z3++.h" - -namespace p4_symbolic { - -namespace { - -template -absl::StatusOr> EvalBitvector(const z3::expr& bv_expr, - const z3::model& model) { - if (!bv_expr.is_bv() || bv_expr.get_sort().bv_size() != num_bits) { - return gutil::InvalidArgumentErrorBuilder() - << "expected bitvector of " << num_bits << " bits, but got " - << bv_expr.get_sort() << ": " << bv_expr; - } - - std::string value_with_prefix = model.eval(bv_expr, true).to_string(); - absl::string_view value = value_with_prefix; - if (absl::ConsumePrefix(&value, "#x")) { - return pdpi::HexStringToBitset(absl::StrCat("0x", value)); - } - if (absl::ConsumePrefix(&value, "#b")) { - return std::bitset(std::string(value)); - } - return gutil::InvalidArgumentErrorBuilder() - << "invalid Z3 bitvector value '" << value_with_prefix << "'"; -} - -template -absl::Status Deparse(const z3::expr& field, const z3::model& model, - pdpi::BitString& result) { - ASSIGN_OR_RETURN(std::bitset bits, - EvalZ3Bitvector(field, model)); - result.AppendBits(bits); - return absl::OkStatus(); -} - -absl::Status Deparse(const SaiEthernet& header, const z3::model& model, - pdpi::BitString& result) { - ASSIGN_OR_RETURN(bool valid, EvalZ3Bool(header.valid, model)); - if (valid) { - RETURN_IF_ERROR(Deparse<48>(header.dst_addr, model, result)); - RETURN_IF_ERROR(Deparse<48>(header.src_addr, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.ether_type, model, result)); - } - return absl::OkStatus(); -} - -absl::Status Deparse(const SaiVlan& header, const z3::model& model, - pdpi::BitString& result) { - ASSIGN_OR_RETURN(bool valid, EvalZ3Bool(header.valid, model)); - if (valid) { - RETURN_IF_ERROR(Deparse<3>(header.priority_code_point, model, result)); - RETURN_IF_ERROR(Deparse<1>(header.drop_eligible_indicator, model, result)); - RETURN_IF_ERROR(Deparse<12>(header.vlan_id, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.ether_type, model, result)); - } - return absl::OkStatus(); -} - -absl::Status Deparse(const SaiIpv4& header, const z3::model& model, - pdpi::BitString& result) { - ASSIGN_OR_RETURN(bool valid, EvalZ3Bool(header.valid, model)); - if (valid) { - RETURN_IF_ERROR(Deparse<4>(header.version, model, result)); - RETURN_IF_ERROR(Deparse<4>(header.ihl, model, result)); - RETURN_IF_ERROR(Deparse<6>(header.dscp, model, result)); - RETURN_IF_ERROR(Deparse<2>(header.ecn, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.total_len, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.identification, model, result)); - RETURN_IF_ERROR(Deparse<1>(header.reserved, model, result)); - RETURN_IF_ERROR(Deparse<1>(header.do_not_fragment, model, result)); - RETURN_IF_ERROR(Deparse<1>(header.more_fragments, model, result)); - RETURN_IF_ERROR(Deparse<13>(header.frag_offset, model, result)); - RETURN_IF_ERROR(Deparse<8>(header.ttl, model, result)); - RETURN_IF_ERROR(Deparse<8>(header.protocol, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.header_checksum, model, result)); - RETURN_IF_ERROR(Deparse<32>(header.src_addr, model, result)); - RETURN_IF_ERROR(Deparse<32>(header.dst_addr, model, result)); - } - return absl::OkStatus(); -} - -absl::Status Deparse(const SaiIpv6& header, const z3::model& model, - pdpi::BitString& result) { - ASSIGN_OR_RETURN(bool valid, EvalZ3Bool(header.valid, model)); - if (valid) { - RETURN_IF_ERROR(Deparse<4>(header.version, model, result)); - RETURN_IF_ERROR(Deparse<6>(header.dscp, model, result)); - RETURN_IF_ERROR(Deparse<2>(header.ecn, model, result)); - RETURN_IF_ERROR(Deparse<20>(header.flow_label, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.payload_length, model, result)); - RETURN_IF_ERROR(Deparse<8>(header.next_header, model, result)); - RETURN_IF_ERROR(Deparse<8>(header.hop_limit, model, result)); - RETURN_IF_ERROR(Deparse<128>(header.src_addr, model, result)); - RETURN_IF_ERROR(Deparse<128>(header.dst_addr, model, result)); - } - return absl::OkStatus(); -} - -absl::Status Deparse(const SaiUdp& header, const z3::model& model, - pdpi::BitString& result) { - ASSIGN_OR_RETURN(bool valid, EvalZ3Bool(header.valid, model)); - if (valid) { - RETURN_IF_ERROR(Deparse<16>(header.src_port, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.dst_port, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.hdr_length, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.checksum, model, result)); - } - return absl::OkStatus(); -} - -absl::Status Deparse(const SaiTcp& header, const z3::model& model, - pdpi::BitString& result) { - ASSIGN_OR_RETURN(bool valid, EvalZ3Bool(header.valid, model)); - if (valid) { - RETURN_IF_ERROR(Deparse<16>(header.src_port, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.dst_port, model, result)); - RETURN_IF_ERROR(Deparse<32>(header.seq_no, model, result)); - RETURN_IF_ERROR(Deparse<32>(header.ack_no, model, result)); - RETURN_IF_ERROR(Deparse<4>(header.data_offset, model, result)); - RETURN_IF_ERROR(Deparse<4>(header.res, model, result)); - RETURN_IF_ERROR(Deparse<8>(header.flags, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.window, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.checksum, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.urgent_ptr, model, result)); - } - return absl::OkStatus(); -} - -absl::Status Deparse(const SaiIcmp& header, const z3::model& model, - pdpi::BitString& result) { - ASSIGN_OR_RETURN(bool valid, EvalZ3Bool(header.valid, model)); - if (valid) { - RETURN_IF_ERROR(Deparse<8>(header.type, model, result)); - RETURN_IF_ERROR(Deparse<8>(header.code, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.checksum, model, result)); - // Rest of header. Not parsed by P4 SAI, so the best we can do is to always - // set it to zero. - result.AppendBits(std::bitset<32>(0)); - } - return absl::OkStatus(); -} - -absl::Status Deparse(const SaiArp& header, const z3::model& model, - pdpi::BitString& result) { - ASSIGN_OR_RETURN(bool valid, EvalZ3Bool(header.valid, model)); - if (valid) { - RETURN_IF_ERROR(Deparse<16>(header.hw_type, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.proto_type, model, result)); - RETURN_IF_ERROR(Deparse<8>(header.hw_addr_len, model, result)); - RETURN_IF_ERROR(Deparse<8>(header.proto_addr_len, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.opcode, model, result)); - RETURN_IF_ERROR(Deparse<48>(header.sender_hw_addr, model, result)); - RETURN_IF_ERROR(Deparse<32>(header.sender_proto_addr, model, result)); - RETURN_IF_ERROR(Deparse<48>(header.target_hw_addr, model, result)); - RETURN_IF_ERROR(Deparse<32>(header.target_proto_addr, model, result)); - } - return absl::OkStatus(); -} - -absl::Status Deparse(const SaiGre& header, const z3::model& model, - pdpi::BitString& result) { - ASSIGN_OR_RETURN(bool valid, EvalZ3Bool(header.valid, model)); - if (valid) { - RETURN_IF_ERROR(Deparse<1>(header.checksum_present, model, result)); - RETURN_IF_ERROR(Deparse<1>(header.routing_present, model, result)); - RETURN_IF_ERROR(Deparse<1>(header.key_present, model, result)); - RETURN_IF_ERROR(Deparse<1>(header.sequence_present, model, result)); - RETURN_IF_ERROR(Deparse<1>(header.strict_source_route, model, result)); - RETURN_IF_ERROR(Deparse<3>(header.recursion_control, model, result)); - RETURN_IF_ERROR(Deparse<1>(header.acknowledgement_present, model, result)); - RETURN_IF_ERROR(Deparse<4>(header.flags, model, result)); - RETURN_IF_ERROR(Deparse<3>(header.version, model, result)); - RETURN_IF_ERROR(Deparse<16>(header.protocol, model, result)); - } - return absl::OkStatus(); -} - -absl::Status Deparse(const SaiPacketIn& header, const z3::model& model, - pdpi::BitString& result) { - ASSIGN_OR_RETURN(bool valid, EvalZ3Bool(header.valid, model)); - if (valid) { - RETURN_IF_ERROR(Deparse<9>(header.ingress_port, model, result)); - RETURN_IF_ERROR(Deparse<9>(header.target_egress_port, model, result)); - RETURN_IF_ERROR(Deparse<6>(header.unused_pad, model, result)); - } - return absl::OkStatus(); -} - -} // namespace - -absl::StatusOr SaiDeparser( - const symbolic::SymbolicPerPacketState& packet, const z3::model& model) { - ASSIGN_OR_RETURN(SaiFields fields, GetSaiFields(packet)); - return SaiDeparser(fields, model); -} - -absl::StatusOr SaiDeparser(const SaiFields& packet, - const z3::model& model) { - pdpi::BitString result; - // TODO: Make unconditional when we no longer need - // backwards-compatibility. - if (packet.headers.packet_in.has_value()) { - RETURN_IF_ERROR(Deparse(packet.headers.packet_in.value(), model, result)); - } - RETURN_IF_ERROR(Deparse(packet.headers.erspan_ethernet, model, result)); - RETURN_IF_ERROR(Deparse(packet.headers.erspan_ipv4, model, result)); - RETURN_IF_ERROR(Deparse(packet.headers.erspan_gre, model, result)); - RETURN_IF_ERROR(Deparse(packet.headers.ethernet, model, result)); - // TODO: Make unconditional when we no longer need - // backwards-compatibility. - if (packet.headers.vlan.has_value()) { - RETURN_IF_ERROR(Deparse(*packet.headers.vlan, model, result)); - } - RETURN_IF_ERROR(Deparse(packet.headers.tunnel_encap_ipv6, model, result)); - RETURN_IF_ERROR(Deparse(packet.headers.tunnel_encap_gre, model, result)); - RETURN_IF_ERROR(Deparse(packet.headers.ipv4, model, result)); - RETURN_IF_ERROR(Deparse(packet.headers.ipv6, model, result)); - RETURN_IF_ERROR(Deparse(packet.headers.udp, model, result)); - RETURN_IF_ERROR(Deparse(packet.headers.tcp, model, result)); - RETURN_IF_ERROR(Deparse(packet.headers.icmp, model, result)); - RETURN_IF_ERROR(Deparse(packet.headers.arp, model, result)); - ASSIGN_OR_RETURN(std::string bytes, result.ToByteString()); - return bytes; -} - -} // namespace p4_symbolic diff --git a/p4_symbolic/z3_util.cc b/p4_symbolic/z3_util.cc index 9adebee2..62ee5b55 100644 --- a/p4_symbolic/z3_util.cc +++ b/p4_symbolic/z3_util.cc @@ -11,14 +11,106 @@ // 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/z3_util.h" #include "absl/status/statusor.h" +#include "absl/strings/strip.h" #include "gmpxx.h" +#include "gutil/status.h" +#include "p4_pdpi/string_encodings/hex_string.h" #include "z3++.h" namespace p4_symbolic { +namespace { + +// Appends exactly `num_bits` bits to the `result` PDPI bit string from the +// given `bit_char_string`. Returns an error if the bit-width of the +// `bit_char_string` exceeds `num_bits`. If the bit-width of the +// `bit_char_string` is less than `num_bits`, pads leading zero bits before +// appending `bit_char_string`. +// Note that we assume network (big) endianness for all bit strings and packet +// fields. When interpreted to integers, preceding bits are more significant. +absl::Status AppendBitCharStringToPDPIBitString( + pdpi::BitString& result, const absl::string_view& bit_char_string, + size_t num_bits) { + // The bit string length should not exceed the specified number of bits. + if (bit_char_string.size() > num_bits) { + return gutil::InvalidArgumentErrorBuilder() + << "Bit string length exceeds the specified size (" << num_bits + << " bits): '" << bit_char_string << "'"; + } + + // Pad leading 0s if the bit string is shorter than the specified size. + for (size_t i = 0; i < num_bits - bit_char_string.size(); ++i) { + result.AppendBit(0); + } + + // Append the bits to the result bit string based on the given value. + for (const char& c : bit_char_string) { + switch (c) { + case '1': { + result.AppendBit(1); + break; + } + case '0': { + result.AppendBit(0); + break; + } + default: { + return gutil::InvalidArgumentErrorBuilder() + << "Bit string must contain either 1s or 0s. Found: " + << bit_char_string; + } + } + } + + return absl::OkStatus(); +} + +// Appends exactly `num_bits` bits to the `result` PDPI bit string from the +// given `hex_char_string`. Returns an error if the bit-width of the +// `hex_char_string` exceeds `num_bits`. If the bit-width of the +// `hex_char_string` is less than `num_bits`, pads leading zero bits before +// appending `hex_char_string`. +// Note that we assume network (big) endianness for all bit strings and packet +// fields. When interpreted to integers, preceding bits are more significant. +absl::Status AppendHexCharStringToPDPIBitString( + pdpi::BitString& result, const absl::string_view& hex_char_string, + size_t num_bits) { + // The hex string length should not exceed the specified number of bits. + if (hex_char_string.size() * 4 > num_bits) { + return gutil::InvalidArgumentErrorBuilder() + << "Hex string length exceeds the specified size (" << num_bits + << " bits): '" << hex_char_string << "'"; + } + + // Pad leading 0s if the hex string is shorter than the specified size. + for (size_t i = 0; i < num_bits - hex_char_string.size() * 4; ++i) { + result.AppendBit(0); + } + + std::string hex_string = std::string(hex_char_string); + + // If the hex string has an uneven length, convert the first hex character and + // then convert the rest of the hex string with an even length. + if (hex_string.size() % 2 == 1) { + // Convert the first hex character and append to the result bit string. + ASSIGN_OR_RETURN(const int digit, pdpi::HexCharToDigit(hex_string.at(0))); + for (int i = 3; i >= 0; --i) { + result.AppendBit((digit >> i) % 2); + } + + // Remove the appended hex character to form an even hex string. + hex_string = hex_string.substr(1); + } + + return result.AppendHexString(absl::StrCat("0x", hex_string)); +} + +} // namespace + z3::context& Z3Context(bool renew) { static z3::context* z3_context = new z3::context(); @@ -53,6 +145,32 @@ absl::StatusOr EvalZ3Int(const z3::expr& int_expr, return model.eval(int_expr, true).get_numeral_int(); } +absl::Status EvalAndAppendZ3BitvectorToBitString(pdpi::BitString& output, + const z3::expr& bv_expr, + const z3::model& model) { + if (!bv_expr.is_bv()) { + return gutil::InvalidArgumentErrorBuilder() + << "Expected a bitvector, found '" << bv_expr << "'"; + } + + const std::string field_value = + model.eval(bv_expr, /*model_completion=*/true).to_string(); + absl::string_view field_value_view = field_value; + + if (absl::ConsumePrefix(&field_value_view, "#x")) { + RETURN_IF_ERROR(AppendHexCharStringToPDPIBitString( + output, field_value_view, bv_expr.get_sort().bv_size())); + } else if (absl::ConsumePrefix(&field_value_view, "#b")) { + RETURN_IF_ERROR(AppendBitCharStringToPDPIBitString( + output, field_value_view, bv_expr.get_sort().bv_size())); + } else { + return gutil::InvalidArgumentErrorBuilder() + << "Invalid Z3 bitvector value '" << field_value << "'"; + } + + return absl::OkStatus(); +} + absl::StatusOr HexStringToZ3Bitvector(z3::context& context, const std::string& hex_string, absl::optional bitwidth) { diff --git a/p4_symbolic/z3_util.h b/p4_symbolic/z3_util.h index 0d9b3c29..9f6e5d29 100644 --- a/p4_symbolic/z3_util.h +++ b/p4_symbolic/z3_util.h @@ -14,12 +14,8 @@ #ifndef PINS_P4_SYMBOLIC_Z3_UTIL_H_ #define PINS_P4_SYMBOLIC_Z3_UTIL_H_ -#include - #include "absl/status/statusor.h" -#include "absl/strings/strip.h" -#include "gutil/status.h" -#include "p4_pdpi/string_encodings/hex_string.h" +#include "p4_pdpi/string_encodings/bit_string.h" #include "z3++.h" namespace p4_symbolic { @@ -37,9 +33,9 @@ absl::StatusOr EvalZ3Bool(const z3::expr &bool_expr, absl::StatusOr EvalZ3Int(const z3::expr &int_expr, const z3::model &model); -template -absl::StatusOr> EvalZ3Bitvector(const z3::expr &bv_expr, - const z3::model &model); +absl::Status EvalAndAppendZ3BitvectorToBitString(pdpi::BitString& output, + const z3::expr& bv_expr, + const z3::model& model); // -- Constructing Z3 expressions ---------------------------------------------- @@ -62,27 +58,6 @@ uint64_t Z3ValueStringToInt(const std::string &value); // == END OF PUBLIC INTERFACE ================================================== -template -absl::StatusOr> EvalZ3Bitvector(const z3::expr &bv_expr, - const z3::model &model) { - if (!bv_expr.is_bv() || bv_expr.get_sort().bv_size() != num_bits) { - return gutil::InvalidArgumentErrorBuilder() - << "expected bitvector of " << num_bits << " bits, but got " - << bv_expr.get_sort() << ": " << bv_expr; - } - - std::string value_with_prefix = model.eval(bv_expr, true).to_string(); - absl::string_view value = value_with_prefix; - if (absl::ConsumePrefix(&value, "#x")) { - return pdpi::HexStringToBitset(absl::StrCat("0x", value)); - } - if (absl::ConsumePrefix(&value, "#b")) { - return std::bitset(std::string(value)); - } - return gutil::InvalidArgumentErrorBuilder() - << "invalid Z3 bitvector value '" << value_with_prefix << "'"; -} - -} // namespace p4_symbolic +} // namespace p4_symbolic #endif // PINS_P4_SYMBOLIC_Z3_UTIL_H_ diff --git a/tests/sflow/sflow_test.cc b/tests/sflow/sflow_test.cc index 79445da5..2764da24 100644 --- a/tests/sflow/sflow_test.cc +++ b/tests/sflow/sflow_test.cc @@ -2626,93 +2626,4 @@ TEST_P(SflowMirrorTestFixture, TestIp2MePacketsAreSampledAndPunted) { EXPECT_TRUE(HasSampleForProtocol(sflow_result, /*ip_protocol=*/58)); } -// 1. Set sFlow config on SUT for one interface. -// 2. Set SUT sFlow collector as kLocalLoopbackIpv6. -// 3. Send ICMP traffic from control switch to SUT on this interface. -// 4. Validate the packets get punted and sFlowtool has expected result. -// TODO: Enable Ip2Me test with correct expectation on CPU counter -TEST_P(SflowMirrorTestFixture, DISABLED_TestIp2MePacketsAreSampledAndPunted) { - thinkit::MirrorTestbed& testbed = - GetParam().testbed_interface->GetMirrorTestbed(); - const int packets_num = 3000; - // Use 100 for traffic speed since we want to verify the punted packets number - // and we don't want the punted packets to get discarded. - const int traffic_speed = 100; - - ASSERT_OK_AND_ASSIGN(Port traffic_port, - GetUnusedUpPort(*sut_gnmi_stub_, /*used_port=*/"")); - ASSERT_OK_AND_ASSIGN( - auto port_id_per_port_name, - pins_test::GetAllUpInterfacePortIdsByName(*sut_gnmi_stub_)); - ASSERT_GE(port_id_per_port_name.size(), 0) << "No up interfaces."; - absl::flat_hash_set sflow_enabled_interfaces; - for (const auto& [interface_name, unused] : port_id_per_port_name) { - sflow_enabled_interfaces.insert(interface_name); - } - - std::vector> collector_address_and_port{ - {kLocalLoopbackIpv6, 6343}}; - ASSERT_OK_AND_ASSIGN( - auto sut_gnmi_config_with_sflow, - UpdateSflowConfig(GetParam().sut_gnmi_config, agent_address_, - collector_address_and_port, sflow_enabled_interfaces, - kInbandSamplingRate, kSampleHeaderSize)); - ASSERT_OK(testbed.Environment().StoreTestArtifact( - "sut_gnmi_config_with_sflow.txt", - json_yang::FormatJsonBestEffort(sut_gnmi_config_with_sflow))); - ASSERT_OK( - pins_test::PushGnmiConfig(testbed.Sut(), sut_gnmi_config_with_sflow)); - - // Wait until all sFLow gNMI states are converged. - ASSERT_OK(pins_test::WaitForCondition( - VerifySflowStatesConverged, absl::Seconds(30), sut_gnmi_stub_.get(), - agent_address_, kInbandSamplingRate, kSampleHeaderSize, - collector_address_and_port, sflow_enabled_interfaces)); - - // Start sflowtool on peer switch. - std::string sflow_result; - { - ASSERT_OK_AND_ASSIGN( - std::thread sflow_tool_thread, - RunSflowCollectorForNSecs( - *GetParam().ssh_client, testbed.Sut().ChassisName(), - kSflowtoolLineFormatTemplate, - /*sflowtool_runtime=*/ - packets_num / traffic_speed + 20, sflow_result)); - - ASSERT_OK_AND_ASSIGN(auto initial_cpu_counter, - ReadCounters("CPU", sut_gnmi_stub_.get())); - absl::Time start_time = absl::Now(); - - // Wait for sflowtool to finish and read counter data. - absl::Cleanup clean_up([this, initial_cpu_counter, packets_num, start_time, - &sflow_tool_thread] { - if (sflow_tool_thread.joinable()) { - sflow_tool_thread.join(); - } - - // Display the difference for CPU counter during test dev. - ASSERT_OK_AND_ASSIGN(auto final_cpu_counter, - ReadCounters("CPU", sut_gnmi_stub_.get())); - auto delta = DeltaCounters(initial_cpu_counter, final_cpu_counter); - EXPECT_EQ(delta.in_discards, 0); - EXPECT_GT(delta.in_pkts, packets_num); - LOG(INFO) << "Ingress Deltas (CPU):\n total time: " - << (absl::Now() - start_time); - ShowCounters(delta); - }); - - ASSERT_OK(SendNIcmpPacketsFromSwitch( - packets_num, traffic_speed, traffic_port, agent_address_, GetIrP4Info(), - *control_p4_session_, testbed.Environment())); - } - - EXPECT_OK(testbed.Environment().StoreTestArtifact("sflow_result.txt", - sflow_result)); - std::vector sflow_samples = absl::StrSplit(sflow_result, '\n'); - LOG(INFO) << "Received " << sflow_samples.size() << " samples"; - // Check ICMP pkts. ICMP for IPv6 protocol number is 58. - EXPECT_TRUE(HasSampleForProtocol(sflow_result, /*ip_protocol=*/58)); -} - } // namespace pins From 4eab3b2aac009f147249d49fcc0c869844b0ca21 Mon Sep 17 00:00:00 2001 From: kishanps Date: Wed, 28 Jun 2023 13:11:57 -0700 Subject: [PATCH 2/7] [P4-Symbolic] Use p4-symbolic's test data instead of SAI P4 for deparser tests. --- p4_symbolic/BUILD.bazel | 24 +++ p4_symbolic/deparser_test.cc | 47 +++--- p4_symbolic/ir/BUILD.bazel | 14 +- p4_symbolic/ir/expected/sai_parser.txt | 192 +++++++++++++++++++++- p4_symbolic/testdata/BUILD.bazel | 22 ++- p4_symbolic/testdata/common/bitwidths.p4 | 48 ++++++ p4_symbolic/testdata/common/headers.p4 | 146 +++++++++++----- p4_symbolic/testdata/common/sai_ids.p4 | 110 +++++++++++++ p4_symbolic/testdata/p4c.bzl | 39 +++++ p4_symbolic/testdata/parser/sai_parser.p4 | 57 ++++++- 10 files changed, 623 insertions(+), 76 deletions(-) create mode 100644 p4_symbolic/testdata/common/bitwidths.p4 create mode 100644 p4_symbolic/testdata/common/sai_ids.p4 create mode 100644 p4_symbolic/testdata/p4c.bzl diff --git a/p4_symbolic/BUILD.bazel b/p4_symbolic/BUILD.bazel index 4d097cce..07271179 100644 --- a/p4_symbolic/BUILD.bazel +++ b/p4_symbolic/BUILD.bazel @@ -88,6 +88,30 @@ cc_library( ], ) +cc_test( + name = "deparser_test", + srcs = ["deparser_test.cc"], + data = [ + "//p4_symbolic/testdata:parser/sai_parser.config.json", + "//p4_symbolic/testdata:parser/sai_parser.p4info.pb.txt", + ], + deps = [ + ":deparser", + ":parser", + ":z3_util", + "//gutil:io", + "//gutil:proto", + "//gutil:status_matchers", + "//p4_pdpi/packetlib", + "//p4_pdpi/packetlib:packetlib_cc_proto", + "//p4_symbolic/sai:fields", + "//p4_symbolic/symbolic", + "@com_github_z3prover_z3//:api", + "@com_google_absl//absl/strings", + "@com_google_googletest//:gtest_main", + ], +) + cc_test( name = "z3_util_test", srcs = ["z3_util_test.cc"], diff --git a/p4_symbolic/deparser_test.cc b/p4_symbolic/deparser_test.cc index 2fc166fb..ec930edf 100644 --- a/p4_symbolic/deparser_test.cc +++ b/p4_symbolic/deparser_test.cc @@ -16,44 +16,56 @@ #include +#include "absl/strings/string_view.h" #include "gmock/gmock.h" #include "gtest/gtest.h" +#include "gutil/io.h" +#include "gutil/proto.h" #include "gutil/status_matchers.h" #include "p4/v1/p4runtime.pb.h" #include "p4_pdpi/packetlib/packetlib.h" #include "p4_pdpi/packetlib/packetlib.pb.h" +#include "p4_symbolic/parser.h" #include "p4_symbolic/sai/fields.h" -#include "p4_symbolic/sai/sai.h" #include "p4_symbolic/symbolic/symbolic.h" -#include "sai_p4/instantiations/google/instantiations.h" -#include "sai_p4/instantiations/google/sai_nonstandard_platforms.h" +#include "p4_symbolic/z3_util.h" #include "z3++.h" namespace p4_symbolic { namespace { -class SaiDeparserTest : public testing::TestWithParam { +class SaiDeparserTest : public testing::Test { public: void SetUp() override { - testing::TestWithParam::SetUp(); - const auto config = sai::GetNonstandardForwardingPipelineConfig( - /*instantiation=*/GetParam(), sai::NonstandardPlatform::kP4Symbolic); - ASSERT_OK_AND_ASSIGN( - state_, EvaluateSaiPipeline(config, /*entries=*/{}, /*ports=*/{})); + constexpr absl::string_view p4info_path = + "p4_symbolic/testdata/parser/" + "sai_parser.p4info.pb.txt"; + constexpr absl::string_view p4_config_path = + "p4_symbolic/testdata/parser/" + "sai_parser.config.json"; + p4::v1::ForwardingPipelineConfig config; + ASSERT_OK(gutil::ReadProtoFromFile(p4info_path, config.mutable_p4info())); + ASSERT_OK_AND_ASSIGN(*config.mutable_p4_device_config(), + gutil::ReadFile(std::string(p4_config_path))); + + Z3Context(/*renew=*/true); + ASSERT_OK_AND_ASSIGN(ir::Dataplane dataplane, + ParseToIr(config, /*table_entries=*/{})); + ASSERT_OK_AND_ASSIGN(state_, symbolic::EvaluateP4Program(dataplane)); } protected: std::unique_ptr state_; }; -TEST_P(SaiDeparserTest, DeparseIngressAndEgressHeadersWithoutConstraints) { +TEST_F(SaiDeparserTest, DeparseIngressAndEgressHeadersWithoutConstraints) { ASSERT_EQ(state_->solver->check(), z3::check_result::sat); auto model = state_->solver->get_model(); EXPECT_OK(DeparseIngressPacket(*state_, model).status()); EXPECT_OK(DeparseEgressPacket(*state_, model).status()); } -TEST_P(SaiDeparserTest, VlanPacketParserIntegrationTest) { +TEST_F(SaiDeparserTest, VlanPacketParserIntegrationTest) { // Add VLAN constraint. { ASSERT_OK_AND_ASSIGN(SaiFields fields, @@ -75,7 +87,7 @@ TEST_P(SaiDeparserTest, VlanPacketParserIntegrationTest) { EXPECT_TRUE(packet.headers(1).has_vlan_header()); } -TEST_P(SaiDeparserTest, Ipv4UdpPacketParserIntegrationTest) { +TEST_F(SaiDeparserTest, Ipv4UdpPacketParserIntegrationTest) { // Add IPv4 + UDP (+ no VLAN) constraint. { ASSERT_OK_AND_ASSIGN(SaiFields fields, @@ -101,7 +113,7 @@ TEST_P(SaiDeparserTest, Ipv4UdpPacketParserIntegrationTest) { EXPECT_THAT(packet.payload(), testing::IsEmpty()); } -TEST_P(SaiDeparserTest, Ipv6TcpPacketParserIntegrationTest) { +TEST_F(SaiDeparserTest, Ipv6TcpPacketParserIntegrationTest) { // Add IPv6 + TCP (+ no VLAN) constraint. { ASSERT_OK_AND_ASSIGN(SaiFields fields, @@ -129,7 +141,7 @@ TEST_P(SaiDeparserTest, Ipv6TcpPacketParserIntegrationTest) { EXPECT_THAT(packet.payload(), testing::IsEmpty()); } -TEST_P(SaiDeparserTest, ArpPacketParserIntegrationTest) { +TEST_F(SaiDeparserTest, ArpPacketParserIntegrationTest) { // Add ARP (+ no VLAN) constraint. { ASSERT_OK_AND_ASSIGN(SaiFields fields, @@ -153,7 +165,7 @@ TEST_P(SaiDeparserTest, ArpPacketParserIntegrationTest) { EXPECT_THAT(packet.payload(), testing::IsEmpty()); } -TEST_P(SaiDeparserTest, IcmpPacketParserIntegrationTest) { +TEST_F(SaiDeparserTest, IcmpPacketParserIntegrationTest) { // Add ICMP (+ no VLAN) constraint. { ASSERT_OK_AND_ASSIGN(SaiFields fields, @@ -179,7 +191,7 @@ TEST_P(SaiDeparserTest, IcmpPacketParserIntegrationTest) { EXPECT_THAT(packet.payload(), testing::IsEmpty()); } -TEST_P(SaiDeparserTest, PacketInHeaderIsNeverParsedIntegrationTest) { +TEST_F(SaiDeparserTest, PacketInHeaderIsNeverParsedIntegrationTest) { // Add packet_in constraint. { ASSERT_OK_AND_ASSIGN(SaiFields fields, @@ -192,8 +204,5 @@ TEST_P(SaiDeparserTest, PacketInHeaderIsNeverParsedIntegrationTest) { EXPECT_EQ(state_->solver->check(), z3::check_result::unsat); } -INSTANTIATE_TEST_SUITE_P(SaiDeparserTest, SaiDeparserTest, - testing::ValuesIn(sai::AllSaiInstantiations())); - } // namespace } // namespace p4_symbolic diff --git a/p4_symbolic/ir/BUILD.bazel b/p4_symbolic/ir/BUILD.bazel index cdaec7d5..d61b5f1a 100644 --- a/p4_symbolic/ir/BUILD.bazel +++ b/p4_symbolic/ir/BUILD.bazel @@ -209,49 +209,49 @@ ir_parsing_test( ir_parsing_test( name = "sai_parser_test", golden_file = "expected/sai_parser.txt", - p4_deps = ["//p4_symbolic/testdata:common/headers.p4"], + p4_deps = ["//p4_symbolic/testdata:common_p4_includes"], p4_program = "//p4_symbolic/testdata:parser/sai_parser.p4", ) ir_parsing_test( name = "extract_parser_operation_test", golden_file = "expected/extract_parser_operation.txt", - p4_deps = ["//p4_symbolic/testdata:common/headers.p4"], + p4_deps = ["//p4_symbolic/testdata:common_p4_includes"], p4_program = "//p4_symbolic/testdata:parser/extract_parser_operation.p4", ) ir_parsing_test( name = "set_parser_operation_test", golden_file = "expected/set_parser_operation.txt", - p4_deps = ["//p4_symbolic/testdata:common/headers.p4"], + p4_deps = ["//p4_symbolic/testdata:common_p4_includes"], p4_program = "//p4_symbolic/testdata:parser/set_parser_operation.p4", ) ir_parsing_test( name = "primitive_parser_operation_test", golden_file = "expected/primitive_parser_operation.txt", - p4_deps = ["//p4_symbolic/testdata:common/headers.p4"], + p4_deps = ["//p4_symbolic/testdata:common_p4_includes"], p4_program = "//p4_symbolic/testdata:parser/primitive_parser_operation.p4", ) ir_parsing_test( name = "default_transition_test", golden_file = "expected/default_transition.txt", - p4_deps = ["//p4_symbolic/testdata:common/headers.p4"], + p4_deps = ["//p4_symbolic/testdata:common_p4_includes"], p4_program = "//p4_symbolic/testdata:parser/default_transition.p4", ) ir_parsing_test( name = "hex_string_transition_test", golden_file = "expected/hex_string_transition.txt", - p4_deps = ["//p4_symbolic/testdata:common/headers.p4"], + p4_deps = ["//p4_symbolic/testdata:common_p4_includes"], p4_program = "//p4_symbolic/testdata:parser/hex_string_transition.p4", ) ir_parsing_test( name = "fall_through_transition_test", golden_file = "expected/fall_through_transition.txt", - p4_deps = ["//p4_symbolic/testdata:common/headers.p4"], + p4_deps = ["//p4_symbolic/testdata:common_p4_includes"], p4_program = "//p4_symbolic/testdata:parser/fall_through_transition.p4", ) diff --git a/p4_symbolic/ir/expected/sai_parser.txt b/p4_symbolic/ir/expected/sai_parser.txt index faca0518..59f40f2f 100644 --- a/p4_symbolic/ir/expected/sai_parser.txt +++ b/p4_symbolic/ir/expected/sai_parser.txt @@ -617,8 +617,16 @@ headers { bitwidth: 16 } } + fields { + key: "unused_pad" + value { + name: "unused_pad" + bitwidth: 8 + } + } ordered_fields_list: "ingress_port" ordered_fields_list: "target_egress_port" + ordered_fields_list: "unused_pad" } } headers { @@ -660,7 +668,14 @@ headers { key: "_padding_0" value { name: "_padding_0" - bitwidth: 1 + bitwidth: 6 + } + } + fields { + key: "local_metadata_t._acl_metadata25" + value { + name: "local_metadata_t._acl_metadata25" + bitwidth: 8 } } fields { @@ -677,6 +692,27 @@ headers { bitwidth: 1 } } + fields { + key: "local_metadata_t._bypass_ingress26" + value { + name: "local_metadata_t._bypass_ingress26" + bitwidth: 1 + } + } + fields { + key: "local_metadata_t._color22" + value { + name: "local_metadata_t._color22" + bitwidth: 2 + } + } + fields { + key: "local_metadata_t._ingress_port23" + value { + name: "local_metadata_t._ingress_port23" + bitwidth: 9 + } + } fields { key: "local_metadata_t._l4_dst_port7" value { @@ -692,16 +728,72 @@ headers { } } fields { - key: "local_metadata_t._packet_in_ingress_port12" + key: "local_metadata_t._mirror_session_id_valid12" + value { + name: "local_metadata_t._mirror_session_id_valid12" + bitwidth: 1 + } + } + fields { + key: "local_metadata_t._mirror_session_id_value13" + value { + name: "local_metadata_t._mirror_session_id_value13" + bitwidth: 16 + } + } + fields { + key: "local_metadata_t._mirroring_dst_ip15" + value { + name: "local_metadata_t._mirroring_dst_ip15" + bitwidth: 32 + } + } + fields { + key: "local_metadata_t._mirroring_dst_mac17" + value { + name: "local_metadata_t._mirroring_dst_mac17" + bitwidth: 48 + } + } + fields { + key: "local_metadata_t._mirroring_src_ip14" + value { + name: "local_metadata_t._mirroring_src_ip14" + bitwidth: 32 + } + } + fields { + key: "local_metadata_t._mirroring_src_mac16" + value { + name: "local_metadata_t._mirroring_src_mac16" + bitwidth: 48 + } + } + fields { + key: "local_metadata_t._mirroring_tos19" + value { + name: "local_metadata_t._mirroring_tos19" + bitwidth: 8 + } + } + fields { + key: "local_metadata_t._mirroring_ttl18" + value { + name: "local_metadata_t._mirroring_ttl18" + bitwidth: 8 + } + } + fields { + key: "local_metadata_t._packet_in_ingress_port20" value { - name: "local_metadata_t._packet_in_ingress_port12" + name: "local_metadata_t._packet_in_ingress_port20" bitwidth: 16 } } fields { - key: "local_metadata_t._packet_in_target_egress_port13" + key: "local_metadata_t._packet_in_target_egress_port21" value { - name: "local_metadata_t._packet_in_target_egress_port13" + name: "local_metadata_t._packet_in_target_egress_port21" bitwidth: 16 } } @@ -719,6 +811,13 @@ headers { bitwidth: 48 } } + fields { + key: "local_metadata_t._route_metadata24" + value { + name: "local_metadata_t._route_metadata24" + bitwidth: 6 + } + } fields { key: "local_metadata_t._tunnel_encap_dst_ipv611" value { @@ -773,8 +872,21 @@ headers { ordered_fields_list: "local_metadata_t._apply_tunnel_encap_at_egress9" ordered_fields_list: "local_metadata_t._tunnel_encap_src_ipv610" ordered_fields_list: "local_metadata_t._tunnel_encap_dst_ipv611" - ordered_fields_list: "local_metadata_t._packet_in_ingress_port12" - ordered_fields_list: "local_metadata_t._packet_in_target_egress_port13" + ordered_fields_list: "local_metadata_t._mirror_session_id_valid12" + ordered_fields_list: "local_metadata_t._mirror_session_id_value13" + ordered_fields_list: "local_metadata_t._mirroring_src_ip14" + ordered_fields_list: "local_metadata_t._mirroring_dst_ip15" + ordered_fields_list: "local_metadata_t._mirroring_src_mac16" + ordered_fields_list: "local_metadata_t._mirroring_dst_mac17" + ordered_fields_list: "local_metadata_t._mirroring_ttl18" + ordered_fields_list: "local_metadata_t._mirroring_tos19" + ordered_fields_list: "local_metadata_t._packet_in_ingress_port20" + ordered_fields_list: "local_metadata_t._packet_in_target_egress_port21" + ordered_fields_list: "local_metadata_t._color22" + ordered_fields_list: "local_metadata_t._ingress_port23" + ordered_fields_list: "local_metadata_t._route_metadata24" + ordered_fields_list: "local_metadata_t._acl_metadata25" + ordered_fields_list: "local_metadata_t._bypass_ingress26" ordered_fields_list: "_padding_0" } } @@ -1776,6 +1888,72 @@ parsers { } } } + parser_ops { + set { + lvalue { + header_name: "scalars" + field_name: "local_metadata_t._mirror_session_id_valid12" + } + expression_rvalue { + builtin_expression { + arguments { + bool_value { + } + } + } + } + } + } + parser_ops { + set { + lvalue { + header_name: "scalars" + field_name: "local_metadata_t._color22" + } + hexstr_rvalue { + value: "0x00" + } + } + } + parser_ops { + set { + lvalue { + header_name: "scalars" + field_name: "local_metadata_t._ingress_port23" + } + field_rvalue { + header_name: "standard_metadata" + field_name: "ingress_port" + } + } + } + parser_ops { + set { + lvalue { + header_name: "scalars" + field_name: "local_metadata_t._route_metadata24" + } + hexstr_rvalue { + value: "0x00" + } + } + } + parser_ops { + set { + lvalue { + header_name: "scalars" + field_name: "local_metadata_t._bypass_ingress26" + } + expression_rvalue { + builtin_expression { + arguments { + bool_value { + } + } + } + } + } + } transition_key_fields { field { header_name: "standard_metadata" diff --git a/p4_symbolic/testdata/BUILD.bazel b/p4_symbolic/testdata/BUILD.bazel index 52e61f67..3fdd35a5 100644 --- a/p4_symbolic/testdata/BUILD.bazel +++ b/p4_symbolic/testdata/BUILD.bazel @@ -12,7 +12,12 @@ # See the License for the specific language governing permissions and # limitations under the License. -package(default_visibility = ["//visibility:public"]) +load("//p4_symbolic/testdata:p4c.bzl", "p4_config_and_p4info_files") + +package( + default_visibility = ["//visibility:public"], + licenses = ["notice"], +) # Make sure programs under p4-samples are visible to other # bazel packages. @@ -21,5 +26,18 @@ exports_files( "**/*.p4", "**/*.txt", ]), - licenses = ["notice"], +) + +filegroup( + name = "common_p4_includes", + srcs = glob(["common/*.p4"]), +) + +p4_config_and_p4info_files( + name = "p4c_outputs", + srcs = glob( + include = ["**/*.p4"], + exclude = ["common/*.p4"], + ), + deps = [":common_p4_includes"], ) diff --git a/p4_symbolic/testdata/common/bitwidths.p4 b/p4_symbolic/testdata/common/bitwidths.p4 new file mode 100644 index 00000000..34b40491 --- /dev/null +++ b/p4_symbolic/testdata/common/bitwidths.p4 @@ -0,0 +1,48 @@ +#ifndef P4_SYMBOLIC_TESTDATA_COMMON_SAI_BITWIDTHS_P4_ +#define P4_SYMBOLIC_TESTDATA_COMMON_SAI_BITWIDTHS_P4_ + +#ifndef PORT_BITWIDTH +#define PORT_BITWIDTH 16 +#endif + +#ifndef VRF_BITWIDTH +#define VRF_BITWIDTH 16 +#endif + +#ifndef NEXTHOP_ID_BITWIDTH +#define NEXTHOP_ID_BITWIDTH 16 +#endif + +#ifndef ROUTER_INTERFACE_ID_BITWIDTH +#define ROUTER_INTERFACE_ID_BITWIDTH 16 +#endif + +#ifndef WCMP_GROUP_ID_BITWIDTH +#define WCMP_GROUP_ID_BITWIDTH 16 +#endif + +#ifndef MIRROR_SESSION_ID_BITWIDTH +#define MIRROR_SESSION_ID_BITWIDTH 16 +#endif + +#ifndef QOS_QUEUE_BITWIDTH +#define QOS_QUEUE_BITWIDTH 16 +#endif + +#ifndef WCMP_SELECTOR_INPUT_BITWIDTH +#define WCMP_SELECTOR_INPUT_BITWIDTH 16 +#endif + +#ifndef ROUTE_METADATA_BITWIDTH +#define ROUTE_METADATA_BITWIDTH 6 +#endif + +#ifndef ACL_METADATA_BITWIDTH +#define ACL_METADATA_BITWIDTH 8 +#endif + +#ifndef TUNNEL_ID_BITWIDTH +#define TUNNEL_ID_BITWIDTH 16 +#endif + +#endif // P4_SYMBOLIC_TESTDATA_COMMON_SAI_BITWIDTHS_P4_ diff --git a/p4_symbolic/testdata/common/headers.p4 b/p4_symbolic/testdata/common/headers.p4 index 762103d4..e1766e6a 100644 --- a/p4_symbolic/testdata/common/headers.p4 +++ b/p4_symbolic/testdata/common/headers.p4 @@ -1,6 +1,9 @@ #ifndef P4_SYMBOLIC_TESTDATA_COMMON_HEADERS_P4_ #define P4_SYMBOLIC_TESTDATA_COMMON_HEADERS_P4_ +#include "bitwidths.p4" +#include "sai_ids.p4" + #define ETHERTYPE_IPV4 0x0800 #define ETHERTYPE_IPV6 0x86dd #define ETHERTYPE_ARP 0x0806 @@ -41,26 +44,6 @@ const vlan_id_t NO_VLAN_ID = 0x000; // documentation of `mark_to_drop`. #define SAI_P4_DROP_PORT 511 -// -- Translated Types --------------------------------------------------------- - -// BMv2 does not support @p4runtime_translation. - -#ifndef PLATFORM_BMV2 -@p4runtime_translation("", string) -@p4runtime_translation_mappings({ - // The "default VRF", 0, corresponds to the empty string, "", in P4Runtime. - {"", 0}, -}) -#endif -type bit<16> vrf_id_t; - -const vrf_id_t kDefaultVrf = 0; - -#ifndef PLATFORM_BMV2 -@p4runtime_translation("", string) -#endif -type bit<16> port_id_t; - // -- Protocol headers --------------------------------------------------------- #define ETHERNET_HEADER_BYTES 14 @@ -172,45 +155,132 @@ header gre_t { bit<16> protocol; } +// -- Preserved Field Lists ---------------------------------------------------- + +// The field list numbers used in @field_list annotations to identify the fields +// that need to be preserved during clone/recirculation/etc. operations. +enum bit<8> PreservedFieldList { + CLONE_I2E_MIRRORING = 8w1, + // We implement packet-in in SAI P4 by using the replication engine to make a + // clone of the punted packet and then send the clone to the controller. But + // the standard metadata of the packet clone will be empty, that's a problem + // because the controller needs to know the ingress port and expected egress + // port of the punted packet. To solve this problem, we save the targeted + // egress port and ingress port of the punted packet in local metadata and use + // clone_preserving_field_list to preserve these local metadata fields when + // cloning the punted packet. + CLONE_I2E_PACKET_IN = 8w2 +}; + +// -- Translated Types --------------------------------------------------------- + +// BMv2 does not support @p4runtime_translation. + +#ifndef PLATFORM_BMV2 +@p4runtime_translation("", string) +#endif +type bit nexthop_id_t; + +#ifndef PLATFORM_BMV2 +@p4runtime_translation("", string) +#endif +type bit tunnel_id_t; + +#ifndef PLATFORM_BMV2 +@p4runtime_translation("", string) +#endif +type bit wcmp_group_id_t; + + +#ifndef PLATFORM_BMV2 +@p4runtime_translation("", string) +// TODO: The following annotation is not yet standard, and not yet +// understood by p4-symbolic. Work with the P4Runtime WG to standardize the +// annotation (or a similar annotation), and teach it to p4-symbolic. +@p4runtime_translation_mappings({ + // The "default VRF", 0, corresponds to the empty string, "", in P4Runtime. + {"", 0}, +}) +#endif +type bit vrf_id_t; + +const vrf_id_t kDefaultVrf = 0; + +#ifndef PLATFORM_BMV2 +@p4runtime_translation("", string) +#endif +type bit router_interface_id_t; + +#ifndef PLATFORM_BMV2 +@p4runtime_translation("", string) +#endif +type bit port_id_t; + +#ifndef PLATFORM_BMV2 +@p4runtime_translation("", string) +#endif +type bit mirror_session_id_t; + +#ifndef PLATFORM_BMV2 +@p4runtime_translation("", string) +#endif +type bit qos_queue_t; + +// -- Untranslated Types ------------------------------------------------------- + +typedef bit route_metadata_t; +typedef bit acl_metadata_t; + +// -- Meters ------------------------------------------------------------------- + +enum bit<2> MeterColor_t { + GREEN = 0, + YELLOW = 1, + RED = 2 +}; + // -- Packet IO headers -------------------------------------------------------- @controller_header("packet_in") header packet_in_header_t { // The port the packet ingressed on. + @id(PACKET_IN_INGRESS_PORT_ID) port_id_t ingress_port; // The initial intended egress port decided for the packet by the pipeline. + @id(PACKET_IN_TARGET_EGRESS_PORT_ID) port_id_t target_egress_port; + // Padding field to align the header to 8-bit multiple, as required by BMv2. + // Carries no information. + // + // Contrary to the corresponding field in the `packet_out` header, we include + // this field only on BMv2, as clients will generally ignore this field anyhow + // and thus not observe this minor API deviation. + // TODO: Handle packet-in uniformly for all platforms. +#if defined(PLATFORM_BMV2) || defined(PLATFORM_P4SYMBOLIC) + @id(PACKET_IN_UNUSED_PAD_ID) + @padding + bit<8> unused_pad; +#endif } @controller_header("packet_out") header packet_out_header_t { // The port this packet should egress out of when `submit_to_ingress == 0`. // Meaningless when `submit_to_ingress == 1`. + @id(PACKET_OUT_EGRESS_PORT_ID) port_id_t egress_port; // Indicates if the packet should go through the ingress pipeline like a // dataplane packet, or be sent straight out of the given `egress_port`. + @id(PACKET_OUT_SUBMIT_TO_INGRESS_ID) bit<1> submit_to_ingress; // Padding field to align the header to 8-bit multiple, as required by BMv2. // Carries no information. + // + // Technically this makes sense only for BMv2, but we include it on all + // platforms so clients don't have to make a distinction in packet-out + // requests. + @id(PACKET_OUT_UNUSED_PAD_ID) @padding bit<7> unused_pad; } - -// -- Preserved Field Lists ---------------------------------------------------- - -// The field list numbers used in @field_list annotations to identify the fields -// that need to be preserved during clone/recirculation/etc. operations. -enum bit<8> PreservedFieldList { - CLONE_I2E_MIRRORING = 8w1, - // We implement packet-in in SAI P4 by using the replication engine to make a - // clone of the punted packet and then send the clone to the controller. But - // the standard metadata of the packet clone will be empty, that's a problem - // because the controller needs to know the ingress port and expected egress - // port of the punted packet. To solve this problem, we save the targeted - // egress port and ingress port of the punted packet in local metadata and use - // clone_preserving_field_list to preserve these local metadata fields when - // cloning the punted packet. - CLONE_I2E_PACKET_IN = 8w2 -}; - #endif // P4_SYMBOLIC_TESTDATA_COMMON_HEADERS_P4_ diff --git a/p4_symbolic/testdata/common/sai_ids.p4 b/p4_symbolic/testdata/common/sai_ids.p4 new file mode 100644 index 00000000..ff4f2721 --- /dev/null +++ b/p4_symbolic/testdata/common/sai_ids.p4 @@ -0,0 +1,110 @@ +#ifndef P4_SYMBOLIC_TESTDATA_COMMON_SAI_IDS_P4_ +#define P4_SYMBOLIC_TESTDATA_COMMON_SAI_IDS_P4_ + +// All declarations (tables, actions, action profiles, meters, counters) have a +// stable ID. This list will evolve as new declarations are added. IDs cannot be +// reused. If a declaration is removed, its ID macro is kept and marked reserved +// to avoid the ID being reused. +// +// The IDs are classified using the 8 most significant bits to be compatible +// with "6.3. ID Allocation for P4Info Objects" in the P4Runtime specification. + +// --- Tables ------------------------------------------------------------------ + +// IDs of fixed SAI tables (8 most significant bits = 0x02). +#define ROUTING_NEIGHBOR_TABLE_ID 0x02000040 // 33554496 +#define ROUTING_ROUTER_INTERFACE_TABLE_ID 0x02000041 // 33554497 +#define ROUTING_NEXTHOP_TABLE_ID 0x02000042 // 33554498 +#define ROUTING_WCMP_GROUP_TABLE_ID 0x02000043 // 33554499 +#define ROUTING_IPV4_TABLE_ID 0x02000044 // 33554500 +#define ROUTING_IPV6_TABLE_ID 0x02000045 // 33554501 +#define ROUTING_VRF_TABLE_ID 0x0200004A // 33554506 +#define MIRROR_SESSION_TABLE_ID 0x02000046 // 33554502 +#define L3_ADMIT_TABLE_ID 0x02000047 // 33554503 +#define MIRROR_PORT_TO_PRE_SESSION_TABLE_ID 0x02000048 // 33554504 +#define ECMP_HASHING_TABLE_ID 0x02000049 // 33554505 +#define ROUTING_TUNNEL_TABLE_ID 0x02000050 // 33554506 + +// --- Actions ----------------------------------------------------------------- + +// IDs of fixed SAI actions (8 most significant bits = 0x01). +#define ROUTING_SET_DST_MAC_ACTION_ID 0x01000001 // 16777217 +#define ROUTING_SET_PORT_AND_SRC_MAC_ACTION_ID 0x01000002 // 16777218 +#define ROUTING_SET_NEXTHOP_ACTION_ID 0x01000003 // 16777219 +#define ROUTING_SET_IP_NEXTHOP_ACTION_ID 0x01000014 // 16777236 +#define ROUTING_SET_WCMP_GROUP_ID_ACTION_ID 0x01000004 // 16777220 +#define ROUTING_SET_WCMP_GROUP_ID_AND_METADATA_ACTION_ID 0x01000011 // 16777233 +#define ROUTING_SET_NEXTHOP_ID_ACTION_ID 0x01000005 // 16777221 +#define ROUTING_SET_NEXTHOP_ID_AND_METADATA_ACTION_ID 0x01000010 // 16777232 +#define ROUTING_DROP_ACTION_ID 0x01000006 // 16777222 +#define ROUTING_SET_P2P_TUNNEL_ENCAP_NEXTHOP_ACTION_ID 0x01000012 // 16777234 +#define ROUTING_MARK_FOR_P2P_TUNNEL_ENCAP_ACTION_ID 0x01000013 // 16777235 +#define MIRRORING_MIRROR_AS_IPV4_ERSPAN_ACTION_ID 0x01000007 // 16777223 +#define L3_ADMIT_ACTION_ID 0x01000008 // 16777224 +#define MIRRORING_SET_PRE_SESSION_ACTION_ID 0x01000009 // 16777225 +#define SELECT_ECMP_HASH_ALGORITHM_ACTION_ID 0x010000A // 16777226 +#define COMPUTE_ECMP_HASH_IPV4_ACTION_ID 0x0100000B // 16777227 +#define COMPUTE_ECMP_HASH_IPV6_ACTION_ID 0x0100000C // 16777228 +#define COMPUTE_LAG_HASH_IPV4_ACTION_ID 0x0100000D // 16777229 +#define COMPUTE_LAG_HASH_IPV6_ACTION_ID 0x0100000E // 16777230 +#define ROUTING_SET_METADATA_AND_DROP_ACTION_ID 0x01000015 // 16777237 +// Next available action id: 0x01000016 (16777238) + +// --- Action Profiles and Selectors (8 most significant bits = 0x11) ---------- +// This value should ideally be 0x11000001, but we currently have this value for +// legacy reasons. +#define ROUTING_WCMP_GROUP_SELECTOR_ACTION_PROFILE_ID 0x11DC4EC8 // 299650760 + +// --- Intrinsic ports --------------------------------------------------------- + +// Port used for PacketIO. Packets sent to this port go to the CPU. +// Packets received on this port come from the CPU. +// TODO For simplicity, we went with 510/511 as CPU/drop port to +// begin with, which are the values used by BMv2 by default, and the values +// hard-coded in p4-symbolic. We should revisit these arbitrary values. +#define SAI_P4_CPU_PORT 510 + +// The port used by `mark_to_drop` from v1model.p4. For details, see the +// documentation of `mark_to_drop`. +#define SAI_P4_DROP_PORT 511 + +// --- Copy to CPU session ----------------------------------------------------- + +// The COPY_TO_CPU_SESSION_ID must be programmed in the target using P4Runtime: +// +// type: INSERT +// entity { +// packet_replication_engine_entry { +// clone_session_entry { +// session_id: COPY_TO_CPU_SESSION_ID +// replicas { +// egress_port: SAI_P4_CPU_PORT +// instance: CLONE_REPLICA_INSTANCE_PACKET_IN +// } +// } +// } +// } +// +#define COPY_TO_CPU_SESSION_ID 255 + +// --- Packet-IO --------------------------------------------------------------- + +#define PACKET_IN_INGRESS_PORT_ID 1 +#define PACKET_IN_TARGET_EGRESS_PORT_ID 2 +#define PACKET_IN_UNUSED_PAD_ID 3 + +#define PACKET_OUT_EGRESS_PORT_ID 1 +#define PACKET_OUT_SUBMIT_TO_INGRESS_ID 2 +#define PACKET_OUT_UNUSED_PAD_ID 3 + +//--- Packet Replication Engine Instances -------------------------------------- + +// Egress instance type definitions. +// The egress instance is a 32-bit standard metadata set by the packet +// replication engine (PRE) in the V1Model architecture. However, the values are +// not defined by the P4 specification. Here we define our own values; these may +// be changed when we adopt another architecture. +#define CLONE_REPLICA_INSTANCE_PACKET_IN 1 +#define CLONE_REPLICA_INSTANCE_MIRRORING 2 + +#endif // P4_SYMBOLIC_TESTDATA_COMMON_SAI_IDS_P4_ diff --git a/p4_symbolic/testdata/p4c.bzl b/p4_symbolic/testdata/p4c.bzl new file mode 100644 index 00000000..10423070 --- /dev/null +++ b/p4_symbolic/testdata/p4c.bzl @@ -0,0 +1,39 @@ +# Copyright 2023 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. + +"""This file includes macros for compiling P4 programs.""" + +load("@com_github_p4lang_p4c//:bazel/p4_library.bzl", "p4_library") + +def p4_config_and_p4info_files(name, srcs, deps): + """ + Macro that defines the compilation rules for provided P4 programs. + + Args: + name: Name of the macro. + srcs: List of P4 program sources. + deps: List of P4 dependencies (included files). + """ + for p4_src_path in srcs: + p4c_name = p4_src_path.removesuffix(".p4") + config_path = "%s.config.json" % p4c_name + p4info_path = "%s.p4info.pb.txt" % p4c_name + p4_library( + name = p4c_name, + src = p4_src_path, + p4info_out = p4info_path, + target = "bmv2", + target_out = config_path, + deps = deps, + ) diff --git a/p4_symbolic/testdata/parser/sai_parser.p4 b/p4_symbolic/testdata/parser/sai_parser.p4 index 70de9cc2..0f98c1f5 100644 --- a/p4_symbolic/testdata/parser/sai_parser.p4 +++ b/p4_symbolic/testdata/parser/sai_parser.p4 @@ -1,10 +1,15 @@ +#define PLATFORM_P4SYMBOLIC #include #include "../common/headers.p4" struct headers_t { +// TODO: Clean up once we have better solution to handle packet-in +// across platforms. +#if defined(PLATFORM_BMV2) || defined(PLATFORM_P4SYMBOLIC) // Never extracted during parsing, but serialized during deparsing for packets // punted to the controller. packet_in_header_t packet_in_header; +#endif // PacketOut header; extracted only for packets received from the controller. packet_out_header_t packet_out_header; @@ -47,11 +52,27 @@ struct local_metadata_t { packet_rewrites_t packet_rewrites; bit<16> l4_src_port; bit<16> l4_dst_port; - bit<16> wcmp_selector_input; + bit wcmp_selector_input; // GRE tunnel encap related fields. bool apply_tunnel_encap_at_egress; ipv6_addr_t tunnel_encap_src_ipv6; ipv6_addr_t tunnel_encap_dst_ipv6; + // mirroring data, we can't group them into a struct, because BMv2 doesn't + // support passing structs in clone3. + bool mirror_session_id_valid; + mirror_session_id_t mirror_session_id_value; + @field_list(PreservedFieldList.CLONE_I2E_MIRRORING) + ipv4_addr_t mirroring_src_ip; + @field_list(PreservedFieldList.CLONE_I2E_MIRRORING) + ipv4_addr_t mirroring_dst_ip; + @field_list(PreservedFieldList.CLONE_I2E_MIRRORING) + ethernet_addr_t mirroring_src_mac; + @field_list(PreservedFieldList.CLONE_I2E_MIRRORING) + ethernet_addr_t mirroring_dst_mac; + @field_list(PreservedFieldList.CLONE_I2E_MIRRORING) + bit<8> mirroring_ttl; + @field_list(PreservedFieldList.CLONE_I2E_MIRRORING) + bit<8> mirroring_tos; // Packet-in related fields, which we can't group into a struct, because BMv2 // doesn't support passing structs in clone3. @@ -59,11 +80,32 @@ struct local_metadata_t { // The value to be copied into the `ingress_port` field of packet_in_header on // punted packets. @field_list(PreservedFieldList.CLONE_I2E_PACKET_IN) - port_id_t packet_in_ingress_port; + bit packet_in_ingress_port; // The value to be copied into the `target_egress_port` field of // packet_in_header on punted packets. @field_list(PreservedFieldList.CLONE_I2E_PACKET_IN) - port_id_t packet_in_target_egress_port; + bit packet_in_target_egress_port; + + MeterColor_t color; + // We consistently use local_metadata.ingress_port instead of + // standard_metadata.ingress_port in the P4 tables to ensure that the P4Info + // has port_id_t as the type for all fields that match on ports. This allows + // tools to treat ports specially (e.g. a fuzzer). + bit<9> ingress_port; + // The following field corresponds to SAI_ROUTE_ENTRY_ATTR_META_DATA/ + // SAI_ACL_TABLE_ATTR_FIELD_ROUTE_DST_USER_META. + route_metadata_t route_metadata; + // ACL metadata can be set with SAI_ACL_ACTION_TYPE_SET_ACL_META_DATA, and + // read from SAI_ACL_TABLE_ATTR_FIELD_ACL_USER_META. + acl_metadata_t acl_metadata; + // When controller sends a packet-out packet, the packet will be submitted to + // the ingress pipleine by default. But sometimes we want to skip the ingress + // pipeline for packet-out, and we cannot skip using the 'exit' statement as + // it is not supported in p4-symbolic yet: b/184062335. So we use this field + // as a workaround. + // TODO: Clean up this workaround after 'exit' is supported in + // p4-symbolic. + bool bypass_ingress; } parser packet_parser(packet_in packet, out headers_t headers, @@ -80,6 +122,11 @@ parser packet_parser(packet_in packet, out headers_t headers, local_metadata.l4_src_port = 0; local_metadata.l4_dst_port = 0; local_metadata.wcmp_selector_input = 0; + local_metadata.mirror_session_id_valid = false; + local_metadata.color = MeterColor_t.GREEN; + local_metadata.ingress_port = standard_metadata.ingress_port; + local_metadata.route_metadata = 0; + local_metadata.bypass_ingress = false; transition select(standard_metadata.ingress_port) { SAI_P4_CPU_PORT: parse_packet_out_header; @@ -240,7 +287,11 @@ control packet_deparser(packet_out packet, in headers_t headers) { // We always expect the packet_out_header to be invalid at the end of the // pipeline, so this line has no effect on the output packet. packet.emit(headers.packet_out_header); +// TODO: Clean up once we have better solution to handle packet-in +// across platforms. +#if defined(PLATFORM_BMV2) || defined(PLATFORM_P4SYMBOLIC) packet.emit(headers.packet_in_header); +#endif packet.emit(headers.erspan_ethernet); packet.emit(headers.erspan_ipv4); packet.emit(headers.erspan_gre); From 27b65f120f23e814d28e4bd01c35da9ad036df52 Mon Sep 17 00:00:00 2001 From: kishanps Date: Thu, 29 Jun 2023 12:40:09 -0700 Subject: [PATCH 3/7] [P4-Symbolic] Move IR parser to `ir/`. Simplify IR parser API. Remove unused IR pdpi_driver. Remove hard-coded SAI parser. Remove EvaluateSaiPipeline. Refactor SAI-specific code. --- p4_symbolic/BUILD.bazel | 39 ++--- p4_symbolic/deparser_test.cc | 6 +- p4_symbolic/ir/BUILD.bazel | 34 ++--- p4_symbolic/ir/parser.cc | 39 +++++ p4_symbolic/{ => ir}/parser.h | 26 +--- p4_symbolic/ir/pdpi_driver.cc | 32 ---- p4_symbolic/ir/pdpi_driver.h | 35 ----- p4_symbolic/ir/test.cc | 11 +- p4_symbolic/main.cc | 44 ++---- .../packet_synthesizer/packet_synthesizer.cc | 7 +- p4_symbolic/parser.cc | 94 ------------ p4_symbolic/sai/BUILD.bazel | 17 +-- p4_symbolic/sai/fields.h | 7 +- p4_symbolic/sai/fields_test.cc | 9 +- p4_symbolic/sai/parser.cc | 139 ------------------ p4_symbolic/sai/parser.h | 39 ----- p4_symbolic/sai/sai.cc | 40 +---- p4_symbolic/sai/sai.h | 50 ++++--- p4_symbolic/sai/sai_test.cc | 139 +++++++++--------- p4_symbolic/symbolic/BUILD.bazel | 2 + p4_symbolic/symbolic/symbolic.cc | 14 +- p4_symbolic/symbolic/symbolic.h | 9 +- p4_symbolic/symbolic/test.bzl | 1 - p4_symbolic/test_util.cc | 60 ++++++++ p4_symbolic/test_util.h | 21 +++ p4_symbolic/tests/BUILD.bazel | 2 - p4_symbolic/tests/sai_p4_component_test.cc | 6 - p4_symbolic/z3_util.h | 4 +- 28 files changed, 313 insertions(+), 613 deletions(-) create mode 100644 p4_symbolic/ir/parser.cc rename p4_symbolic/{ => ir}/parser.h (55%) delete mode 100644 p4_symbolic/ir/pdpi_driver.cc delete mode 100644 p4_symbolic/ir/pdpi_driver.h delete mode 100644 p4_symbolic/parser.cc delete mode 100644 p4_symbolic/sai/parser.cc delete mode 100644 p4_symbolic/sai/parser.h create mode 100644 p4_symbolic/test_util.cc create mode 100644 p4_symbolic/test_util.h diff --git a/p4_symbolic/BUILD.bazel b/p4_symbolic/BUILD.bazel index 07271179..e731dc8b 100644 --- a/p4_symbolic/BUILD.bazel +++ b/p4_symbolic/BUILD.bazel @@ -25,12 +25,10 @@ cc_binary( "main.cc", ], deps = [ - ":parser", + ":test_util", "//gutil:io", - "//gutil:status", - "//p4_symbolic/bmv2", - "//p4_symbolic/sai:parser", "//p4_symbolic/symbolic", + "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", "@com_google_absl//absl/flags:flag", "@com_google_absl//absl/flags:parse", "@com_google_absl//absl/flags:usage", @@ -39,24 +37,6 @@ cc_binary( ], ) -cc_library( - name = "parser", - srcs = ["parser.cc"], - hdrs = ["parser.h"], - deps = [ - "//gutil:io", - "//gutil:proto", - "//p4_pdpi:ir", - "//p4_pdpi:ir_cc_proto", - "//p4_symbolic/bmv2", - "//p4_symbolic/ir", - "//p4_symbolic/ir:ir_cc_proto", - "//p4_symbolic/ir:pdpi_driver", - "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", - "@com_google_absl//absl/types:span", - ], -) - cc_library( name = "z3_util", srcs = ["z3_util.cc"], @@ -88,6 +68,20 @@ cc_library( ], ) +cc_library( + name = "test_util", + testonly = False, + srcs = ["test_util.cc"], + hdrs = ["test_util.h"], + deps = [ + "//gutil:io", + "//gutil:proto", + "@com_github_p4lang_p4runtime//:p4info_cc_proto", + "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", + "@com_google_absl//absl/status:statusor", + ], +) + cc_test( name = "deparser_test", srcs = ["deparser_test.cc"], @@ -97,7 +91,6 @@ cc_test( ], deps = [ ":deparser", - ":parser", ":z3_util", "//gutil:io", "//gutil:proto", diff --git a/p4_symbolic/deparser_test.cc b/p4_symbolic/deparser_test.cc index ec930edf..544fab25 100644 --- a/p4_symbolic/deparser_test.cc +++ b/p4_symbolic/deparser_test.cc @@ -25,7 +25,6 @@ #include "p4/v1/p4runtime.pb.h" #include "p4_pdpi/packetlib/packetlib.h" #include "p4_pdpi/packetlib/packetlib.pb.h" -#include "p4_symbolic/parser.h" #include "p4_symbolic/sai/fields.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/z3_util.h" @@ -49,9 +48,8 @@ class SaiDeparserTest : public testing::Test { gutil::ReadFile(std::string(p4_config_path))); Z3Context(/*renew=*/true); - ASSERT_OK_AND_ASSIGN(ir::Dataplane dataplane, - ParseToIr(config, /*table_entries=*/{})); - ASSERT_OK_AND_ASSIGN(state_, symbolic::EvaluateP4Program(dataplane)); + ASSERT_OK_AND_ASSIGN(state_, + symbolic::EvaluateP4Program(config, /*entries=*/{})); } protected: diff --git a/p4_symbolic/ir/BUILD.bazel b/p4_symbolic/ir/BUILD.bazel index d61b5f1a..cf7f1797 100644 --- a/p4_symbolic/ir/BUILD.bazel +++ b/p4_symbolic/ir/BUILD.bazel @@ -33,22 +33,6 @@ proto_library( ], ) -cc_library( - name = "pdpi_driver", - srcs = [ - "pdpi_driver.cc", - ], - hdrs = [ - "pdpi_driver.h", - ], - deps = [ - "//gutil:proto", - "//gutil:status", - "//p4_pdpi:ir", - "//p4_pdpi:ir_cc_proto", - ], -) - cc_library( name = "table_entries", srcs = [ @@ -116,6 +100,21 @@ cc_library( ], ) +cc_library( + name = "parser", + srcs = ["parser.cc"], + hdrs = ["parser.h"], + deps = [ + ":ir", + "//p4_pdpi:ir", + "//p4_pdpi:ir_cc_proto", + "//p4_symbolic/bmv2", + "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", + "@com_google_absl//absl/status:statusor", + "@com_google_absl//absl/types:span", + ], +) + cc_test( name = "cfg_test", srcs = ["cfg_test.cc"], @@ -138,9 +137,10 @@ cc_binary( "test.cc", ], deps = [ + ":parser", "//gutil:io", "//gutil:proto", - "//p4_symbolic:parser", + "//p4_symbolic:test_util", "@com_google_absl//absl/flags:flag", "@com_google_absl//absl/flags:parse", "@com_google_absl//absl/flags:usage", diff --git a/p4_symbolic/ir/parser.cc b/p4_symbolic/ir/parser.cc new file mode 100644 index 00000000..d84277c5 --- /dev/null +++ b/p4_symbolic/ir/parser.cc @@ -0,0 +1,39 @@ +// 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/ir/parser.h" + +#include "p4/v1/p4runtime.pb.h" +#include "p4_pdpi/ir.h" +#include "p4_pdpi/ir.pb.h" +#include "p4_symbolic/bmv2/bmv2.h" +#include "p4_symbolic/ir/ir.h" + +namespace p4_symbolic::ir { + +absl::StatusOr ParseToIr( + const p4::v1::ForwardingPipelineConfig &config, + absl::Span table_entries) { + ASSIGN_OR_RETURN(bmv2::P4Program bmv2, + bmv2::ParseBmv2JsonString(config.p4_device_config()), + _.SetPrepend() << "While trying to parse BMv2 JSON: "); + ASSIGN_OR_RETURN(const pdpi::IrP4Info ir_p4info, + pdpi::CreateIrP4Info(config.p4info())); + ASSIGN_OR_RETURN(P4Program program, Bmv2AndP4infoToIr(bmv2, ir_p4info)); + ASSIGN_OR_RETURN(TableEntries ir_table_entries, + ParseTableEntries(ir_p4info, table_entries)); + return Dataplane{program, ir_table_entries}; +} + +} // namespace p4_symbolic::ir diff --git a/p4_symbolic/parser.h b/p4_symbolic/ir/parser.h similarity index 55% rename from p4_symbolic/parser.h rename to p4_symbolic/ir/parser.h index 3de42959..88a9c994 100644 --- a/p4_symbolic/parser.h +++ b/p4_symbolic/ir/parser.h @@ -15,34 +15,20 @@ // This file defines the main API entry point for parsing input files // into our IR representation. -#ifndef P4_SYMBOLIC_PARSER_H_ -#define P4_SYMBOLIC_PARSER_H_ - -#include +#ifndef P4_SYMBOLIC_IR_PARSER_H_ +#define P4_SYMBOLIC_IR_PARSER_H_ +#include "absl/status/statusor.h" #include "absl/types/span.h" #include "p4/v1/p4runtime.pb.h" -#include "p4_pdpi/ir.pb.h" #include "p4_symbolic/ir/ir.h" -namespace p4_symbolic { - -absl::StatusOr ParseToIr(const std::string &bmv2_json_path, - const std::string &p4info_path, - const std::string &table_entries_path); - -absl::StatusOr ParseToIr( - const std::string &bmv2_json_path, const std::string &p4info_path, - absl::Span table_entries); - -absl::StatusOr ParseToIr( - const std::string &bmv2_json, const pdpi::IrP4Info &p4info, - absl::Span table_entries); +namespace p4_symbolic::ir { -absl::StatusOr ParseToIr( +absl::StatusOr ParseToIr( const p4::v1::ForwardingPipelineConfig &config, absl::Span table_entries); -} // namespace p4_symbolic +} // namespace p4_symbolic::ir #endif // P4_SYMBOLIC_PARSER_H_ diff --git a/p4_symbolic/ir/pdpi_driver.cc b/p4_symbolic/ir/pdpi_driver.cc deleted file mode 100644 index 0142c3de..00000000 --- a/p4_symbolic/ir/pdpi_driver.cc +++ /dev/null @@ -1,32 +0,0 @@ -// 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/ir/pdpi_driver.h" - -#include - -#include "gutil/proto.h" -#include "p4_pdpi/ir.h" - -namespace p4_symbolic { -namespace ir { - -absl::StatusOr ParseP4InfoFile(const std::string &p4info_path) { - p4::config::v1::P4Info p4info; - RETURN_IF_ERROR(gutil::ReadProtoFromFile(p4info_path.c_str(), &p4info)); - return pdpi::CreateIrP4Info(p4info); -} - -} // namespace ir -} // namespace p4_symbolic diff --git a/p4_symbolic/ir/pdpi_driver.h b/p4_symbolic/ir/pdpi_driver.h deleted file mode 100644 index a394e997..00000000 --- a/p4_symbolic/ir/pdpi_driver.h +++ /dev/null @@ -1,35 +0,0 @@ -// 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 P4_SYMBOLIC_IR_PDPI_DRIVER_H_ -#define P4_SYMBOLIC_IR_PDPI_DRIVER_H_ - -#include - -#include "gutil/status.h" -#include "p4_pdpi/ir.pb.h" - -namespace p4_symbolic { -namespace ir { - -// Parses the p4info file given by "p4info_path" into a pdpi:IrP4Info -// instance. -// Returns the parsed IrP4Info instance, or an appropriate failure status -// in case of a badly formatted input file, or if the file does not exist. -absl::StatusOr ParseP4InfoFile(const std::string &p4info_path); - -} // namespace ir -} // namespace p4_symbolic - -#endif // P4_SYMBOLIC_IR_PDPI_DRIVER_H_ diff --git a/p4_symbolic/ir/test.cc b/p4_symbolic/ir/test.cc index 695eca48..e44d2aa8 100644 --- a/p4_symbolic/ir/test.cc +++ b/p4_symbolic/ir/test.cc @@ -24,7 +24,8 @@ #include "absl/strings/str_format.h" #include "gutil/io.h" #include "gutil/proto.h" -#include "p4_symbolic/parser.h" +#include "p4_symbolic/ir/parser.h" +#include "p4_symbolic/test_util.h" ABSL_FLAG(std::string, p4info, "", "The path to the p4info protobuf file (required)"); @@ -51,8 +52,12 @@ absl::Status Test() { // Transform to IR and print. ASSIGN_OR_RETURN( - p4_symbolic::ir::Dataplane dataplane, - p4_symbolic::ParseToIr(bmv2_path, p4info_path, entries_path)); + p4::v1::ForwardingPipelineConfig config, + p4_symbolic::ParseToForwardingPipelineConfig(bmv2_path, p4info_path)); + ASSIGN_OR_RETURN(std::vector table_entries, + p4_symbolic::ParseToPiTableEntries(entries_path)); + ASSIGN_OR_RETURN(p4_symbolic::ir::Dataplane dataplane, + p4_symbolic::ir::ParseToIr(config, table_entries)); // Dump string representation to the output file. std::ostringstream output; diff --git a/p4_symbolic/main.cc b/p4_symbolic/main.cc index 6c5398c0..b8518097 100644 --- a/p4_symbolic/main.cc +++ b/p4_symbolic/main.cc @@ -27,11 +27,9 @@ #include "absl/status/status.h" #include "absl/strings/str_format.h" #include "gutil/io.h" -#include "gutil/status.h" -#include "p4_symbolic/bmv2/bmv2.h" -#include "p4_symbolic/parser.h" -#include "p4_symbolic/sai/parser.h" +#include "p4/v1/p4runtime.pb.h" #include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/test_util.h" ABSL_FLAG(std::string, p4info, "", "The path to the p4info protobuf file (required)"); @@ -42,8 +40,6 @@ ABSL_FLAG(std::string, entries, "", "entries are needed."); ABSL_FLAG(std::string, smt, "", "Dump the SMT program for debugging"); ABSL_FLAG(int, port_count, 2, "Number of used ports (numbered 0 to N-1)"); -ABSL_FLAG(bool, hardcoded_parser, true, - "Use the hardcoded parser during symbolic evaluation"); namespace { @@ -55,15 +51,15 @@ absl::Status ParseAndEvaluate() { const std::string &entries_path = absl::GetFlag(FLAGS_entries); const std::string &smt_path = absl::GetFlag(FLAGS_smt); const int port_count = absl::GetFlag(FLAGS_port_count); - bool hardcoded_parser = absl::GetFlag(FLAGS_hardcoded_parser); RET_CHECK(!p4info_path.empty()); RET_CHECK(!bmv2_path.empty()); - // Transform to IR. ASSIGN_OR_RETURN( - p4_symbolic::ir::Dataplane dataplane, - p4_symbolic::ParseToIr(bmv2_path, p4info_path, entries_path)); + p4::v1::ForwardingPipelineConfig config, + p4_symbolic::ParseToForwardingPipelineConfig(bmv2_path, p4info_path)); + ASSIGN_OR_RETURN(std::vector table_entries, + p4_symbolic::ParseToPiTableEntries(entries_path)); // Generate port list. std::vector physical_ports(port_count); @@ -72,17 +68,8 @@ absl::Status ParseAndEvaluate() { // Evaluate program symbolically. ASSIGN_OR_RETURN( std::unique_ptr solver_state, - p4_symbolic::symbolic::EvaluateP4Program(dataplane, physical_ports)); - - // Add constraints for parser. - if (hardcoded_parser) { - ASSIGN_OR_RETURN( - std::vector parser_constraints, - p4_symbolic::EvaluateSaiParser(solver_state->context.ingress_headers)); - for (auto &constraint : parser_constraints) { - solver_state->solver->add(constraint); - } - } + p4_symbolic::symbolic::EvaluateP4Program(config, table_entries, + physical_ports)); // Output SMT formula. if (!smt_path.empty()) { @@ -94,11 +81,12 @@ absl::Status ParseAndEvaluate() { // Loop over tables in a deterministic order for output consistency // (important for ci tests). auto ordered_tables = absl::btree_map( - dataplane.program.tables().cbegin(), dataplane.program.tables().cend()); + solver_state->program.tables().cbegin(), + solver_state->program.tables().cend()); constexpr int kColumnSize = 80; for (const auto &[name, table] : ordered_tables) { - int row_count = static_cast(dataplane.entries[name].size()); + int row_count = static_cast(solver_state->entries[name].size()); for (int i = -1; i < row_count; i++) { std::string banner = "Finding packet for table " + name + " and row " + std::to_string(i); @@ -137,11 +125,11 @@ int main(int argc, char *argv[]) { // Verify link and compile versions are the same. // GOOGLE_PROTOBUF_VERIFY_VERSION; - // Command line arugments and help message. - absl::SetProgramUsageMessage(absl::StrFormat( - "usage: %s %s", argv[0], - "--bmv2=path/to/bmv2.json --p4info=path/to/p4info.pb.txt " - "[--entries=path/to/table_entries.txt] [--hardcoded_parser=false]")); + // Command line arguments and help message. + absl::SetProgramUsageMessage( + absl::StrFormat("usage: %s %s", argv[0], + "--bmv2=path/to/bmv2.json --p4info=path/to/p4info.pb.txt " + "[--entries=path/to/table_entries.txt]")); absl::ParseCommandLine(argc, argv); // Run code diff --git a/p4_symbolic/packet_synthesizer/packet_synthesizer.cc b/p4_symbolic/packet_synthesizer/packet_synthesizer.cc index 62089343..f93a3fa7 100644 --- a/p4_symbolic/packet_synthesizer/packet_synthesizer.cc +++ b/p4_symbolic/packet_synthesizer/packet_synthesizer.cc @@ -78,9 +78,8 @@ absl::StatusOr SynthesizePacketFromZ3Model( 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)); + ASSIGN_OR_RETURN(std::string local_metadata_ingress_port, + GetLocalMetadataIngressPortFromModel(solver_state)); // TODO: p4-symbolic might miss that // local_metadata.ingress_port is p4runtime_translated. In such cases, @@ -233,7 +232,7 @@ absl::StatusOr> PacketSynthesizer::Create( // Evaluate P4 pipeline to get solver_state. ASSIGN_OR_RETURN(auto solver_state, - p4_symbolic::EvaluateSaiPipeline( + p4_symbolic::symbolic::EvaluateP4Program( config, entries, physical_ports, translation_per_type)); // TODO: Avoid generating packets that are always dropped. diff --git a/p4_symbolic/parser.cc b/p4_symbolic/parser.cc deleted file mode 100644 index d0a74949..00000000 --- a/p4_symbolic/parser.cc +++ /dev/null @@ -1,94 +0,0 @@ -// 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/parser.h" - -#include "gutil/io.h" -#include "gutil/proto.h" -#include "p4/v1/p4runtime.pb.h" -#include "p4_pdpi/ir.h" -#include "p4_symbolic/bmv2/bmv2.h" -#include "p4_symbolic/ir/ir.h" -#include "p4_symbolic/ir/pdpi_driver.h" - -namespace p4_symbolic { - -absl::StatusOr ParseToIr(const std::string &bmv2_json_path, - const std::string &p4info_path, - const std::string &table_entries_path) { - // Parse table entries. - p4::v1::WriteRequest write_request; - if (!table_entries_path.empty()) { - RETURN_IF_ERROR( - gutil::ReadProtoFromFile(table_entries_path.c_str(), &write_request)) - .SetPrepend() - << "While trying to parse table entry file '" << table_entries_path - << "': "; - } - std::vector table_entries; - for (const auto &update : write_request.updates()) { - // Make sure update is of type insert. - if (update.type() != p4::v1::Update::INSERT) { - return absl::InvalidArgumentError( - absl::StrCat("Table entries file contains a non-insert update ", - update.DebugString())); - } - - // Make sure the entity is a table entry. - const p4::v1::Entity &entity = update.entity(); - if (entity.entity_case() != p4::v1::Entity::kTableEntry) { - return absl::InvalidArgumentError( - absl::StrCat("Table entries file contains a non-table entry entity ", - entity.DebugString())); - } - table_entries.push_back(std::move(entity.table_entry())); - } - - return ParseToIr(bmv2_json_path, p4info_path, table_entries); -} - -absl::StatusOr ParseToIr( - const std::string &bmv2_json_path, const std::string &p4info_path, - absl::Span table_entries) { - // Parse bmv2 json file into our initial bmv2 protobuf. - ASSIGN_OR_RETURN(std::string bmv2_json, gutil::ReadFile(bmv2_json_path)); - - // Parse p4info file into pdpi format. - ASSIGN_OR_RETURN(pdpi::IrP4Info p4info, - p4_symbolic::ir::ParseP4InfoFile(p4info_path), - _.SetPrepend() << "While trying to parse p4info file '" - << p4info_path << "': "); - return ParseToIr(bmv2_json, p4info, table_entries); -} - -absl::StatusOr ParseToIr( - const std::string &bmv2_json, const pdpi::IrP4Info &p4info, - absl::Span table_entries) { - ASSIGN_OR_RETURN(bmv2::P4Program bmv2, bmv2::ParseBmv2JsonString(bmv2_json), - _.SetPrepend() << "While trying to parse BMv2 JSON: "); - ASSIGN_OR_RETURN(ir::P4Program program, ir::Bmv2AndP4infoToIr(bmv2, p4info)); - ASSIGN_OR_RETURN(ir::TableEntries ir_table_entries, - ir::ParseTableEntries(p4info, table_entries)); - return ir::Dataplane{program, ir_table_entries}; -} - -absl::StatusOr ParseToIr( - const p4::v1::ForwardingPipelineConfig &config, - absl::Span table_entries) { - ASSIGN_OR_RETURN(const pdpi::IrP4Info ir_p4info, - pdpi::CreateIrP4Info(config.p4info())); - return ParseToIr(config.p4_device_config(), ir_p4info, table_entries); -} - -} // namespace p4_symbolic diff --git a/p4_symbolic/sai/BUILD.bazel b/p4_symbolic/sai/BUILD.bazel index 23a65ad5..091e22bd 100644 --- a/p4_symbolic/sai/BUILD.bazel +++ b/p4_symbolic/sai/BUILD.bazel @@ -26,23 +26,8 @@ cc_library( "//p4_symbolic:z3_util", "//p4_symbolic/symbolic", "@com_github_z3prover_z3//:api", - "@com_google_absl//absl/strings", - ], -) - -cc_library( - name = "parser", - srcs = ["parser.cc"], - hdrs = ["parser.h"], - deps = [ - ":fields", - "//gutil:status", - "//p4_symbolic:z3_util", - "//p4_symbolic/symbolic", - "@com_github_z3prover_z3//:api", - "@com_google_absl//absl/status", + "@com_google_absl//absl/status", "@com_google_absl//absl/status:statusor", "@com_google_absl//absl/strings", ], ) - diff --git a/p4_symbolic/sai/fields.h b/p4_symbolic/sai/fields.h index ec685644..bf286d5d 100644 --- a/p4_symbolic/sai/fields.h +++ b/p4_symbolic/sai/fields.h @@ -223,10 +223,9 @@ 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`. +// P4-Symbolic adds a special field ("$valid$") to each header corresponding to +// its validity. This function returns a field reference (in form of +//
.) to the validity field of the given `header`. // Note: This function does NOT check if the given header exists. std::string GetHeaderValidityFieldRef(absl::string_view header); diff --git a/p4_symbolic/sai/fields_test.cc b/p4_symbolic/sai/fields_test.cc index c0915b94..fb3cc669 100644 --- a/p4_symbolic/sai/fields_test.cc +++ b/p4_symbolic/sai/fields_test.cc @@ -20,7 +20,6 @@ #include "gmock/gmock.h" #include "gtest/gtest.h" #include "gutil/status_matchers.h" -#include "p4_symbolic/sai/sai.h" #include "p4_symbolic/symbolic/symbolic.h" #include "sai_p4/instantiations/google/instantiations.h" #include "sai_p4/instantiations/google/sai_nonstandard_platforms.h" @@ -32,8 +31,8 @@ TEST(GetSaiFields, CanGetIngressAndEgressFieldsForAllInstantiations) { for (auto instantiation : sai::AllSaiInstantiations()) { const auto config = sai::GetNonstandardForwardingPipelineConfig( instantiation, sai::NonstandardPlatform::kP4Symbolic); - ASSERT_OK_AND_ASSIGN( - auto state, EvaluateSaiPipeline(config, /*entries=*/{}, /*ports=*/{})); + ASSERT_OK_AND_ASSIGN(auto state, symbolic::EvaluateP4Program( + config, /*entries=*/{}, /*ports=*/{})); for (auto& headers : {state->context.ingress_headers, state->context.egress_headers}) { EXPECT_OK(GetSaiFields(headers).status()); @@ -44,8 +43,8 @@ TEST(GetSaiFields, CanGetIngressAndEgressFieldsForAllInstantiations) { TEST(GetUserMetadataFieldNameTest, FailsForNonExistingFields) { const auto config = sai::GetNonstandardForwardingPipelineConfig( sai::Instantiation::kMiddleblock, sai::NonstandardPlatform::kP4Symbolic); - ASSERT_OK_AND_ASSIGN( - auto state, EvaluateSaiPipeline(config, /*entries=*/{}, /*ports=*/{})); + ASSERT_OK_AND_ASSIGN(auto state, symbolic::EvaluateP4Program( + config, /*entries=*/{}, /*ports=*/{})); ASSERT_THAT(GetUserMetadataFieldName("dummy_nonexisting_field", state->context.ingress_headers), gutil::StatusIs(absl::StatusCode::kInternal)); diff --git a/p4_symbolic/sai/parser.cc b/p4_symbolic/sai/parser.cc deleted file mode 100644 index 3ee30ca8..00000000 --- a/p4_symbolic/sai/parser.cc +++ /dev/null @@ -1,139 +0,0 @@ -// 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/sai/parser.h" - -#include -#include -#include - -#include "absl/status/statusor.h" -#include "absl/strings/match.h" -#include "gutil/status.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" -#include "z3++.h" - -namespace p4_symbolic { - -using ::p4_symbolic::symbolic::SymbolicPerPacketState; - -absl::StatusOr> EvaluateSaiParser( - const SymbolicPerPacketState& state) { - std::vector constraints; - - ASSIGN_OR_RETURN(SaiFields fields, GetSaiFields(state)); - // TODO: Make non-optional when we no longer need - // backwards-compatibility. - std::optional& packet_in = fields.headers.packet_in; - 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; - SaiEthernet& ethernet = fields.headers.ethernet; - // TODO: Make non-optional when we no longer need - // backwards-compatibility. - std::optional& vlan = fields.headers.vlan; - SaiIpv6& tunnel_encap_ipv6 = fields.headers.tunnel_encap_ipv6; - SaiGre& tunnel_encap_gre = fields.headers.tunnel_encap_gre; - SaiIpv4& ipv4 = fields.headers.ipv4; - SaiIpv6& ipv6 = fields.headers.ipv6; - SaiUdp& udp = fields.headers.udp; - SaiTcp& tcp = fields.headers.tcp; - SaiIcmp& icmp = fields.headers.icmp; - SaiArp& arp = fields.headers.arp; - SaiLocalMetadata& local_metadata = fields.local_metadata; - V1ModelStandardMetadata& standard_metadata = fields.standard_metadata; - z3::expr bv_true = Z3Context().bv_val(1, 1); - z3::expr bv_false = Z3Context().bv_val(0, 1); - - // `start` state. - constraints.push_back(!erspan_ethernet.valid); - constraints.push_back(!erspan_ipv4.valid); - constraints.push_back(!erspan_gre.valid); - constraints.push_back(!tunnel_encap_ipv6.valid); - constraints.push_back(!tunnel_encap_gre.valid); - // TODO: Make unconditional when we no longer need - // backwards-compatibility. - if (local_metadata.vlan_id.has_value()) { - constraints.push_back(*local_metadata.vlan_id == 0); - } - if (local_metadata.vlan_id_valid.has_value()) { - constraints.push_back(*local_metadata.vlan_id_valid == bv_false); - } - constraints.push_back(local_metadata.admit_to_l3 == bv_false); - constraints.push_back(local_metadata.vrf_id == 0); - constraints.push_back(local_metadata.mirror_session_id_valid == bv_false); - 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-compatibility. - constraints.push_back(*local_metadata.bypass_ingress == false); - } - if (packet_in.has_value()) { - // TODO: Make unconditional when we no longer need - // backwards-compatibility. - constraints.push_back(!packet_in->valid); - } - - // `parse_packet_out` state. - if (packet_out.has_value()) { - // TODO: Make unconditional when we no longer need - // backwards-compatibility. - constraints.push_back( - packet_out->valid == - (standard_metadata.ingress_port == symbolic::kCpuPort)); - } - - // `parse_ethernet` state and `parse_8021q_vlan` state. - constraints.push_back(ethernet.valid == Z3Context().bool_val(true)); - // TODO: Make unconditional when we no longer need - // backwards-compatibility. - z3::expr ether_type = ethernet.ether_type; - if (vlan.has_value()) { - constraints.push_back(vlan->valid == (ethernet.ether_type == 0x8100)); - ether_type = z3::ite(vlan->valid, vlan->ether_type, ethernet.ether_type); - } - constraints.push_back(ipv4.valid == (ether_type == 0x0800)); - constraints.push_back(ipv6.valid == (ether_type == 0x86dd)); - constraints.push_back(arp.valid == (ether_type == 0x0806)); - - // `parse_ipv{4,6}` states. - constraints.push_back(icmp.valid == (ipv4.valid && ipv4.protocol == 0x01 || - ipv6.valid && ipv6.next_header == 0x3a)); - constraints.push_back(tcp.valid == (ipv4.valid && ipv4.protocol == 0x06 || - ipv6.valid && ipv6.next_header == 0x06)); - constraints.push_back(udp.valid == (ipv4.valid && ipv4.protocol == 0x11 || - ipv6.valid && ipv6.next_header == 0x11)); - - // `parse_tcp` state. - // We use `!a || b` to express `a implies b`. - constraints.push_back(!tcp.valid || - (local_metadata.l4_src_port == tcp.src_port && - local_metadata.l4_dst_port == tcp.dst_port)); - - // `parse_udp` state. - // We use `!a || b` ito express `a implies b`. - constraints.push_back(!udp.valid || - (local_metadata.l4_src_port == udp.src_port && - local_metadata.l4_dst_port == udp.dst_port)); - - return constraints; -} - -} // namespace p4_symbolic diff --git a/p4_symbolic/sai/parser.h b/p4_symbolic/sai/parser.h deleted file mode 100644 index 89b6ccf8..00000000 --- a/p4_symbolic/sai/parser.h +++ /dev/null @@ -1,39 +0,0 @@ -// 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. - -// Hardcodes the behavior of an interesting p4 parser that is part -// of the p4 program we are interested in. -// The hardcoded behavior sets the validity of certain header fields -// based on the fields in the packet, and sets the default values -// for local_metadata fields. - -#ifndef GOOGLE_P4_SYMBOLIC_SAI_PARSER_H_ -#define GOOGLE_P4_SYMBOLIC_SAI_PARSER_H_ - -#include - -#include "gutil/status.h" -#include "p4_symbolic/symbolic/symbolic.h" - -namespace p4_symbolic { - -// Generates constraints encoding the behavior of the SAI parser. -// NOTE: The parser logic is currently hard-coded and not parsed from the -// program. -absl::StatusOr> -EvaluateSaiParser(const symbolic::SymbolicPerPacketState &state); - -} // namespace p4_symbolic - -#endif // GOOGLE_P4_SYMBOLIC_SAI_PARSER_H_ diff --git a/p4_symbolic/sai/sai.cc b/p4_symbolic/sai/sai.cc index 57c9d7a9..cd5adcee 100644 --- a/p4_symbolic/sai/sai.cc +++ b/p4_symbolic/sai/sai.cc @@ -11,6 +11,7 @@ // 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/sai/sai.h" #include @@ -23,20 +24,12 @@ #include "absl/status/status.h" #include "absl/strings/str_cat.h" #include "gutil/status.h" -#include "p4/config/v1/p4info.pb.h" -#include "p4/v1/p4runtime.pb.h" -#include "p4_pdpi/ir.h" -#include "p4_pdpi/ir.pb.h" -#include "p4_symbolic/parser.h" #include "p4_symbolic/sai/fields.h" -#include "p4_symbolic/sai/parser.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/symbolic/values.h" namespace p4_symbolic { -// Checks if the set of physical ports is the same as the set of numeric IDs -// passed as the static mapping for "port_id_t". absl::Status CheckPhysicalPortAndPortIdTypeValueConsistency( const std::vector& physical_ports, const symbolic::TranslationPerType& translation_per_type) { @@ -58,7 +51,6 @@ absl::Status CheckPhysicalPortAndPortIdTypeValueConsistency( return absl::OkStatus(); } -// Adds partially static mapping for "vrf_id_t". absl::Status AddVrfIdTypeTranslation( symbolic::TranslationPerType& translation_per_type) { if (translation_per_type.contains(kVrfIdTypeName)) { @@ -76,40 +68,20 @@ absl::Status AddVrfIdTypeTranslation( return absl::OkStatus(); } -absl::StatusOr> EvaluateSaiPipeline( - const p4::v1::ForwardingPipelineConfig& config, - const std::vector& entries, - const std::vector& physical_ports, - symbolic::TranslationPerType translation_per_type) { - // Check inputs for consistency. - RETURN_IF_ERROR(CheckPhysicalPortAndPortIdTypeValueConsistency( - physical_ports, translation_per_type)); - - // Add translation for vrf_id_t. - RETURN_IF_ERROR(AddVrfIdTypeTranslation(translation_per_type)); - - ASSIGN_OR_RETURN(ir::Dataplane dataplane, ParseToIr(config, entries)); - ASSIGN_OR_RETURN(std::unique_ptr state, - symbolic::EvaluateP4Program(dataplane, physical_ports, - translation_per_type)); - return state; -} - -absl::StatusOr ExtractLocalMetadataIngressPortFromModel( +absl::StatusOr GetLocalMetadataIngressPortFromModel( const symbolic::SolverState& solver_state) { // We are interested in the value after parsing because the parser sets // `local_metadata.ingress_port = standard_metadata.ingress_port`. Also, // according to P4-16 spec, the metadata of the ingress packet may contain // arbitrary value before being initialized. - ASSIGN_OR_RETURN( - p4_symbolic::SaiFields parsed_fields, - p4_symbolic::GetSaiFields(solver_state.context.parsed_headers)); + ASSIGN_OR_RETURN(SaiFields parsed_fields, + GetSaiFields(solver_state.context.parsed_headers)); ASSIGN_OR_RETURN(const std::string local_metadata_ingress_port_field_name, - p4_symbolic::GetUserMetadataFieldName( + GetUserMetadataFieldName( "ingress_port", solver_state.context.parsed_headers)); // Note: Do NOT directly use "local_metadata.ingress_port" as the field name // (see p4_symbolic::GetUserMetadataFieldName). - return TranslateValueToP4RT( + return symbolic::values::TranslateValueToP4RT( local_metadata_ingress_port_field_name, solver_state.solver->get_model() .eval(parsed_fields.local_metadata.ingress_port, true) diff --git a/p4_symbolic/sai/sai.h b/p4_symbolic/sai/sai.h index 67ae1376..ba60770c 100644 --- a/p4_symbolic/sai/sai.h +++ b/p4_symbolic/sai/sai.h @@ -11,38 +11,40 @@ // 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_SAI_TEST_UTIL_H_ -#define PINS_P4_SYMBOLIC_SAI_TEST_UTIL_H_ -#include +#ifndef PINS_P4_SYMBOLIC_SAI_SAI_H_ +#define PINS_P4_SYMBOLIC_SAI_SAI_H_ + +#include #include +#include "absl/status/status.h" #include "absl/status/statusor.h" -#include "p4/v1/p4runtime.pb.h" +#include "absl/strings/string_view.h" #include "p4_symbolic/symbolic/symbolic.h" namespace p4_symbolic { -constexpr char kPortIdTypeName[] = "port_id_t"; -constexpr char kVrfIdTypeName[] = "vrf_id_t"; - -// Symbolically evaluates the SAI P4 program for the given forwarding pipeline -// config with the given table entries. If `physical_ports` is non-empty, any -// solution is guaranteed to only use ports from the list. Note that the set of -// `physical_ports` should be consistent with the numeric values used in the -// static translation of "port_id_t" in `translation_per_type`, otherwise -// returns an error. Also adds the partially static mapping for "vrf_id_t" and -// expects such mapping to not be present in `translation_per_type`. Otherwise, -// returns an error. -absl::StatusOr> -EvaluateSaiPipeline(const p4::v1::ForwardingPipelineConfig &config, - const std::vector &entries, - const std::vector &physical_ports = {}, - symbolic::TranslationPerType translation_per_type = {}); - -absl::StatusOr ExtractLocalMetadataIngressPortFromModel( - const symbolic::SolverState &solver_state); +// SAI-specific type names. +constexpr absl::string_view kPortIdTypeName = "port_id_t"; +constexpr absl::string_view kVrfIdTypeName = "vrf_id_t"; + +// Checks if the set of physical ports is the same as the set of numeric IDs +// passed as the static mapping for "port_id_t". +absl::Status CheckPhysicalPortAndPortIdTypeValueConsistency( + const std::vector& physical_ports, + const symbolic::TranslationPerType& translation_per_type); + +// Adds the partially static mapping for "vrf_id_t" if such mapping is not +// present in `translation_per_type`. +absl::Status AddVrfIdTypeTranslation( + symbolic::TranslationPerType& translation_per_type); + +// Returns the concrete value of the field `local_metadata.ingress_port` right +// after parser processing based on the given model. +absl::StatusOr GetLocalMetadataIngressPortFromModel( + const symbolic::SolverState& solver_state); } // namespace p4_symbolic -#endif // PINS_P4_SYMBOLIC_SAI_TEST_UTIL_H_ +#endif // PINS_INFRA_P4_SYMBOLIC_SAI_SAI_H_ diff --git a/p4_symbolic/sai/sai_test.cc b/p4_symbolic/sai/sai_test.cc index cdbe283c..60f19d74 100644 --- a/p4_symbolic/sai/sai_test.cc +++ b/p4_symbolic/sai/sai_test.cc @@ -17,13 +17,13 @@ #include #include "absl/status/status.h" -#include "absl/status/statusor.h" #include "absl/strings/string_view.h" #include "gmock/gmock.h" #include "gtest/gtest.h" #include "gutil/status_matchers.h" #include "gutil/testing.h" #include "p4/v1/p4runtime.pb.h" +#include "p4_pdpi/ir.h" #include "p4_pdpi/pd.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/symbolic/values.h" @@ -34,102 +34,95 @@ namespace p4_symbolic { namespace { -TEST(EvaluateSaiPipeline, - SatisfiableForAllInstantiationsWithEmptyEntriesAndPorts) { - for (auto instantiation : sai::AllSaiInstantiations()) { - const auto config = sai::GetNonstandardForwardingPipelineConfig( - instantiation, sai::NonstandardPlatform::kP4Symbolic); - ASSERT_OK_AND_ASSIGN( - auto state, EvaluateSaiPipeline(config, /*entries=*/{}, /*ports=*/{})); - EXPECT_EQ(state->solver->check(), z3::check_result::sat); - } +TEST(SaiTranslationChecks, NoErrorWithEmptyPortsAndTranslation) { + EXPECT_OK(CheckPhysicalPortAndPortIdTypeValueConsistency( + /*physical_ports=*/{}, + /*translation_per_type=*/{})); + + symbolic::TranslationPerType translations; + EXPECT_OK(AddVrfIdTypeTranslation(translations)); + EXPECT_EQ(translations.size(), 1); + ASSERT_TRUE(translations.contains(kVrfIdTypeName)); + std::vector> expected_static_mapping{ + {"", 0}}; + EXPECT_EQ(translations.at(kVrfIdTypeName).static_mapping, + expected_static_mapping); + EXPECT_TRUE(translations.at(kVrfIdTypeName).dynamic_translation); } -TEST(EvaluateSaiPipeline, FailsForInconsistentPortAndPortIdTypeTranslation) { - const auto config = sai::GetNonstandardForwardingPipelineConfig( - sai::Instantiation::kFabricBorderRouter, - sai::NonstandardPlatform::kP4Symbolic); +TEST(SaiTranslationChecks, FailsForInconsistentPortAndPortIdTypeTranslation) { + std::vector ports{1, 2, 3}; symbolic::TranslationPerType translations; translations[kPortIdTypeName] = symbolic::values::TranslationData{ .static_mapping = {{"a", 1}, {"b", 2}}, .dynamic_translation = false, }; - absl::StatusOr> state = - EvaluateSaiPipeline(config, /*entries=*/{}, /*ports=*/{1, 2, 3}, - translations); - ASSERT_THAT(state.status(), - gutil::StatusIs(absl::StatusCode::kInvalidArgument)); + EXPECT_THAT( + CheckPhysicalPortAndPortIdTypeValueConsistency(ports, translations), + gutil::StatusIs(absl::StatusCode::kInvalidArgument)); } -TEST(EvaluateSaiPipeline, PassForConsistentPortAndPortIdTypeTranslation) { - const auto config = sai::GetNonstandardForwardingPipelineConfig( - sai::Instantiation::kFabricBorderRouter, - sai::NonstandardPlatform::kP4Symbolic); +TEST(SaiTranslationChecks, PassForConsistentPortAndPortIdTypeTranslation) { + std::vector ports{1, 2}; symbolic::TranslationPerType translations; translations[kPortIdTypeName] = symbolic::values::TranslationData{ .static_mapping = {{"a", 1}, {"b", 2}}, .dynamic_translation = false, }; - absl::StatusOr> state = - EvaluateSaiPipeline(config, /*entries=*/{}, /*ports=*/{1, 2}, - translations); - ASSERT_OK(state.status()); - EXPECT_EQ((*state)->solver->check(), z3::check_result::sat); + EXPECT_OK( + CheckPhysicalPortAndPortIdTypeValueConsistency(ports, translations)); } -TEST(EvaluateSaiPipeline, FailsIfInputContainsTranslationForVrfIdType) { - const auto config = sai::GetNonstandardForwardingPipelineConfig( - sai::Instantiation::kFabricBorderRouter, - sai::NonstandardPlatform::kP4Symbolic); +TEST(SaiTranslationChecks, FailsIfInputContainsTranslationForVrfIdType) { symbolic::TranslationPerType translations; translations[kVrfIdTypeName] = symbolic::values::TranslationData{}; - absl::StatusOr> state = - EvaluateSaiPipeline(config, /*entries=*/{}, /*ports=*/{}, translations); - ASSERT_THAT(state.status(), + EXPECT_THAT(AddVrfIdTypeTranslation(translations), gutil::StatusIs(absl::StatusCode::kInvalidArgument)); } -TEST(EvaluateSaiPipeline, IngressPortIsAmongPassedValues) { - // Get config. - const auto config = sai::GetNonstandardForwardingPipelineConfig( - sai::Instantiation::kFabricBorderRouter, - sai::NonstandardPlatform::kP4Symbolic); - ASSERT_OK_AND_ASSIGN(const pdpi::IrP4Info ir_p4info, - pdpi::CreateIrP4Info(config.p4info())); +TEST(GetLocalMetadataIngressPortFromModel, IngressPortIsAmongPassedValues) { + for (auto instantiation : sai::AllSaiInstantiations()) { + // Get config. + const auto config = sai::GetNonstandardForwardingPipelineConfig( + instantiation, sai::NonstandardPlatform::kP4Symbolic); + ASSERT_OK_AND_ASSIGN(const pdpi::IrP4Info ir_p4info, + pdpi::CreateIrP4Info(config.p4info())); - // Note: We need to install a table entry with the given translated field (in - // this case, local_metadata.ingress_port) for P4Symbolic to understand that - // the field is a translated type. - auto pd_entries = gutil::ParseProtoOrDie( - R"pb(entries { - acl_pre_ingress_table_entry { - match { in_port { value: "b" } } - action { set_vrf { vrf_id: "vrf-80" } } - priority: 1 - } - })pb"); - std::vector pi_entries; - for (auto& pd_entry : pd_entries.entries()) { - ASSERT_OK_AND_ASSIGN(pi_entries.emplace_back(), - pdpi::PartialPdTableEntryToPiTableEntry(ir_p4info, pd_entry)); - } + // Note: We need to install a table entry with the given translated field + // (in this case, local_metadata.ingress_port) for P4Symbolic to understand + // that the field is a translated type. + auto pd_entries = gutil::ParseProtoOrDie( + R"pb(entries { + acl_pre_ingress_table_entry { + match { in_port { value: "b" } } + action { set_vrf { vrf_id: "vrf-80" } } + priority: 1 + } + })pb"); + std::vector pi_entries; + for (auto& pd_entry : pd_entries.entries()) { + ASSERT_OK_AND_ASSIGN(pi_entries.emplace_back(), + pdpi::PartialPdTableEntryToPiTableEntry(ir_p4info, pd_entry)); + } + symbolic::TranslationPerType translations; + translations[kPortIdTypeName] = symbolic::values::TranslationData{ + .static_mapping = {{"a", 1}, {"b", 2}}, + .dynamic_translation = false, + }; - // Evaluate the SAI pipeline. - symbolic::TranslationPerType translations; - translations[kPortIdTypeName] = symbolic::values::TranslationData{ - .static_mapping = {{"a", 1}, {"b", 2}}, - .dynamic_translation = false, - }; - absl::StatusOr> state = - EvaluateSaiPipeline(config, pi_entries, /*ports=*/{1, 2}, translations); - ASSERT_OK(state.status()); + // Evaluate the SAI pipeline. + ASSERT_OK_AND_ASSIGN( + std::unique_ptr state, + symbolic::EvaluateP4Program(config, pi_entries, /*ports=*/{1, 2}, + translations)); - // Check local_metadata.ingress_port value. - EXPECT_EQ((*state)->solver->check(), z3::check_result::sat); - ASSERT_OK_AND_ASSIGN(const std::string local_metadata_ingress_port, - ExtractLocalMetadataIngressPortFromModel(**state)); - ASSERT_THAT(local_metadata_ingress_port, - testing::AnyOf(testing::Eq("a"), testing::Eq("b"))); + // Check local_metadata.ingress_port value. + EXPECT_EQ(state->solver->check(), z3::check_result::sat); + ASSERT_OK_AND_ASSIGN(const std::string local_metadata_ingress_port, + GetLocalMetadataIngressPortFromModel(*state)); + EXPECT_THAT(local_metadata_ingress_port, + testing::AnyOf(testing::Eq("a"), testing::Eq("b"))); + } } } // namespace diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel index 94be8908..0df696a4 100644 --- a/p4_symbolic/symbolic/BUILD.bazel +++ b/p4_symbolic/symbolic/BUILD.bazel @@ -61,9 +61,11 @@ cc_library( "//p4_symbolic/ir", "//p4_symbolic/ir:cfg", "//p4_symbolic/ir:ir_cc_proto", + "//p4_symbolic/ir:parser", "//p4_symbolic/ir:table_entries", "@com_github_google_glog//:glog", "@com_github_p4lang_p4runtime//:p4info_cc_proto", + "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", "@com_github_z3prover_z3//:api", "@com_gnu_gmp//:gmp", "@com_google_absl//absl/base:core_headers", diff --git a/p4_symbolic/symbolic/symbolic.cc b/p4_symbolic/symbolic/symbolic.cc index 2df96f88..147dfacf 100644 --- a/p4_symbolic/symbolic/symbolic.cc +++ b/p4_symbolic/symbolic/symbolic.cc @@ -23,6 +23,7 @@ #include "absl/types/optional.h" #include "glog/logging.h" #include "p4_pdpi/internal/ordered_map.h" +#include "p4_symbolic/ir/parser.h" #include "p4_symbolic/symbolic/util.h" #include "p4_symbolic/symbolic/v1model.h" #include "p4_symbolic/symbolic/values.h" @@ -58,9 +59,14 @@ z3::expr EgressSpecDroppedValue() { return Z3Context().bv_val(kDropPort, kPortBitwidth); } -absl::StatusOr> EvaluateP4Program( - const ir::Dataplane &data_plane, const std::vector &physical_ports, +absl::StatusOr> EvaluateP4Program( + const p4::v1::ForwardingPipelineConfig &config, + const std::vector &entries, + const std::vector &physical_ports, const TranslationPerType &translation_per_type) { + // Parse the P4 config and entries into the P4-symbolic IR. + ASSIGN_OR_RETURN(ir::Dataplane dataplane, ir::ParseToIr(config, entries)); + // Use global context to define a solver. std::unique_ptr z3_solver = std::make_unique(Z3Context()); @@ -77,7 +83,7 @@ absl::StatusOr> EvaluateP4Program( // Evaluate the main program, assuming it conforms to V1 model. ASSIGN_OR_RETURN( SymbolicContext context, - v1model::EvaluateV1model(data_plane, physical_ports, translator)); + v1model::EvaluateV1model(dataplane, physical_ports, translator)); // Restrict the value of all fields with (purely static, i.e. // dynamic_translation = false) P4RT translated types to what has been used in @@ -118,7 +124,7 @@ absl::StatusOr> EvaluateP4Program( } // Assemble and return result. - return std::make_unique(data_plane.program, data_plane.entries, + return std::make_unique(dataplane.program, dataplane.entries, std::move(context), std::move(z3_solver), std::move(translator)); } diff --git a/p4_symbolic/symbolic/symbolic.h b/p4_symbolic/symbolic/symbolic.h index c610be87..782e0020 100644 --- a/p4_symbolic/symbolic/symbolic.h +++ b/p4_symbolic/symbolic/symbolic.h @@ -28,7 +28,7 @@ #include "absl/base/macros.h" #include "absl/strings/str_cat.h" #include "absl/strings/string_view.h" -#include "p4_symbolic/ir/ir.h" +#include "p4/v1/p4runtime.pb.h" #include "p4_symbolic/ir/table_entries.h" #include "p4_symbolic/symbolic/guarded_map.h" #include "p4_symbolic/symbolic/values.h" @@ -265,13 +265,14 @@ using TranslationPerType = absl::btree_map; // Symbolically evaluates/interprets the given program against the given -// entries for every table in that program, and the available physical ports +// entries for every table in the program, and the available physical ports // on the switch. Optionally, for types that have @p4runtime_translate(_, // string) annotation, a static mapping between the P4RT values and the // underlying bitvector values may be provided. Otherwise, a mapping is // inferred dynamically for such types. -absl::StatusOr> EvaluateP4Program( - const ir::Dataplane &data_plane, +absl::StatusOr> EvaluateP4Program( + const p4::v1::ForwardingPipelineConfig &config, + const std::vector &entries, const std::vector &physical_ports = {}, const TranslationPerType &translation_per_type = {}); diff --git a/p4_symbolic/symbolic/test.bzl b/p4_symbolic/symbolic/test.bzl index 5e9d7b86..5be09d31 100644 --- a/p4_symbolic/symbolic/test.bzl +++ b/p4_symbolic/symbolic/test.bzl @@ -103,7 +103,6 @@ def end_to_end_test( tools = ["//p4_symbolic:main"], cmd = " ".join([ "$(location //p4_symbolic:main)", - "--hardcoded_parser=false", ("--bmv2=$(location %s)" % bmv2_file), ("--p4info=$(location %s)" % p4info_file), ("--entries=$(location %s)" % table_entries if table_entries else ""), diff --git a/p4_symbolic/test_util.cc b/p4_symbolic/test_util.cc new file mode 100644 index 00000000..4239689d --- /dev/null +++ b/p4_symbolic/test_util.cc @@ -0,0 +1,60 @@ +#include "p4_symbolic/test_util.h" + +#include "gutil/io.h" +#include "gutil/proto.h" +#include "p4/config/v1/p4info.pb.h" +#include "p4/v1/p4runtime.pb.h" + +namespace p4_symbolic { + +absl::StatusOr +ParseToForwardingPipelineConfig(const std::string &bmv2_json_path, + const std::string &p4info_path) { + // Read BMv2 json file into a string. + ASSIGN_OR_RETURN(std::string bmv2_json, gutil::ReadFile(bmv2_json_path)); + + // Parse p4info file into protobuf. + p4::config::v1::P4Info p4info; + RETURN_IF_ERROR(gutil::ReadProtoFromFile(p4info_path, &p4info)); + + p4::v1::ForwardingPipelineConfig config; + *config.mutable_p4_device_config() = std::move(bmv2_json); + *config.mutable_p4info() = std::move(p4info); + return config; +} + +absl::StatusOr> ParseToPiTableEntries( + const std::string &table_entries_path) { + // Parse table entries. + p4::v1::WriteRequest write_request; + if (!table_entries_path.empty()) { + RETURN_IF_ERROR( + gutil::ReadProtoFromFile(table_entries_path, &write_request)) + .SetPrepend() + << "While trying to parse table entry file '" << table_entries_path + << "': "; + } + + std::vector table_entries; + for (const auto &update : write_request.updates()) { + // Make sure update is of type insert. + if (update.type() != p4::v1::Update::INSERT) { + return absl::InvalidArgumentError( + absl::StrCat("Table entries file contains a non-insert update ", + update.DebugString())); + } + + // Make sure the entity is a table entry. + const p4::v1::Entity &entity = update.entity(); + if (entity.entity_case() != p4::v1::Entity::kTableEntry) { + return absl::InvalidArgumentError( + absl::StrCat("Table entries file contains a non-table entry entity ", + entity.DebugString())); + } + table_entries.push_back(std::move(entity.table_entry())); + } + + return table_entries; +} + +} // namespace p4_symbolic diff --git a/p4_symbolic/test_util.h b/p4_symbolic/test_util.h new file mode 100644 index 00000000..e940b17b --- /dev/null +++ b/p4_symbolic/test_util.h @@ -0,0 +1,21 @@ +#ifndef PINS_P4_SYMBOLIC_TEST_UTIL_H_ +#define PINS_P4_SYMBOLIC_TEST_UTIL_H_ + +#include +#include + +#include "absl/status/statusor.h" +#include "p4/v1/p4runtime.pb.h" + +namespace p4_symbolic { + +absl::StatusOr +ParseToForwardingPipelineConfig(const std::string &bmv2_json_path, + const std::string &p4info_path); + +absl::StatusOr> ParseToPiTableEntries( + const std::string &table_entries_path); + +} // namespace p4_symbolic + +#endif // PINS_P4_SYMBOLIC_TEST_UTIL_H_ diff --git a/p4_symbolic/tests/BUILD.bazel b/p4_symbolic/tests/BUILD.bazel index 79e0288f..c4190359 100644 --- a/p4_symbolic/tests/BUILD.bazel +++ b/p4_symbolic/tests/BUILD.bazel @@ -13,7 +13,6 @@ cc_test( "//p4_pdpi:ir", "//p4_pdpi:ir_cc_proto", "//p4_pdpi:pd", - "//p4_symbolic:parser", "//p4_symbolic:z3_util", "//p4_symbolic/symbolic", "//sai_p4/instantiations/google:sai_nonstandard_platforms_cc", @@ -24,7 +23,6 @@ cc_test( "@com_google_absl//absl/strings", "@com_google_absl//absl/time", "@com_google_absl//absl/types:optional", - "@com_google_absl//absl/types:span", "@com_google_googletest//:gtest_main", ], ) diff --git a/p4_symbolic/tests/sai_p4_component_test.cc b/p4_symbolic/tests/sai_p4_component_test.cc index fb10ea12..6fe6d80d 100644 --- a/p4_symbolic/tests/sai_p4_component_test.cc +++ b/p4_symbolic/tests/sai_p4_component_test.cc @@ -16,7 +16,6 @@ #include "absl/strings/string_view.h" #include "absl/time/clock.h" #include "absl/types/optional.h" -#include "absl/types/span.h" #include "gmock/gmock.h" #include "gtest/gtest.h" #include "gutil/status_matchers.h" @@ -25,7 +24,6 @@ #include "p4_pdpi/ir.h" #include "p4_pdpi/ir.pb.h" #include "p4_pdpi/pd.h" -#include "p4_symbolic/parser.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/z3_util.h" #include "sai_p4/instantiations/google/instantiations.h" @@ -127,10 +125,6 @@ TEST(P4SymbolicComponentTest, CanGenerateTestPacketsForSimpleSaiP4Entries) { pdpi::PartialPdTableEntryToPiTableEntry(ir_p4info, pd_entry)); } - // Prepare p4-symbolic. - ASSERT_OK_AND_ASSIGN( - ir::Dataplane dataplane, - ParseToIr(config.p4_device_config(), ir_p4info, pi_entries)); std::vector ports = {1, 2, 3, 4, 5}; LOG(INFO) << "building model (this may take a while) ..."; absl::Time start_time = absl::Now(); diff --git a/p4_symbolic/z3_util.h b/p4_symbolic/z3_util.h index 9f6e5d29..652fc4bd 100644 --- a/p4_symbolic/z3_util.h +++ b/p4_symbolic/z3_util.h @@ -50,8 +50,8 @@ HexStringToZ3Bitvector(z3::context &context, const std::string &hex_string, // Turns the given z3 extracted value (as a string) to a uint64_t. // Z3 returns an extracted value as either a binary, hex, or decimal strings -// dependening on the size of the value and the formatting flags it is -// initialized with. +// depending on the size of the value and the formatting flags it is initialized +// with. // Note: This function assumes that the input is well-formatted and the result // fits in uint64_t (otherwise an exception will be thrown). uint64_t Z3ValueStringToInt(const std::string &value); From 218b2c425a5476aaeea6004e6fbe9d0732eb69d6 Mon Sep 17 00:00:00 2001 From: kishanps Date: Thu, 29 Jun 2023 17:50:41 -0700 Subject: [PATCH 4/7] [P4-Symbolic] Remove dependencies on SAI fields. --- p4_symbolic/BUILD.bazel | 3 +- p4_symbolic/deparser_test.cc | 78 ++-- p4_symbolic/packet_synthesizer/BUILD.bazel | 2 +- .../packet_synthesizer/criteria_generator.cc | 4 +- .../packet_synthesizer/packet_synthesizer.cc | 46 +-- p4_symbolic/packet_synthesizer/util.cc | 62 ++-- p4_symbolic/sai/BUILD.bazel | 31 +- p4_symbolic/sai/fields.cc | 351 ------------------ p4_symbolic/sai/fields.h | 234 ------------ p4_symbolic/sai/fields_test.cc | 54 --- p4_symbolic/sai/sai.cc | 87 ++++- p4_symbolic/sai/sai.h | 13 +- p4_symbolic/symbolic/util.cc | 4 + p4_symbolic/symbolic/util.h | 9 +- 14 files changed, 234 insertions(+), 744 deletions(-) delete mode 100644 p4_symbolic/sai/fields.cc delete mode 100644 p4_symbolic/sai/fields.h delete mode 100644 p4_symbolic/sai/fields_test.cc diff --git a/p4_symbolic/BUILD.bazel b/p4_symbolic/BUILD.bazel index e731dc8b..2a8484fa 100644 --- a/p4_symbolic/BUILD.bazel +++ b/p4_symbolic/BUILD.bazel @@ -97,9 +97,10 @@ cc_test( "//gutil:status_matchers", "//p4_pdpi/packetlib", "//p4_pdpi/packetlib:packetlib_cc_proto", - "//p4_symbolic/sai:fields", "//p4_symbolic/symbolic", + "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", "@com_github_z3prover_z3//:api", + "@com_google_absl//absl/status:statusor", "@com_google_absl//absl/strings", "@com_google_googletest//:gtest_main", ], diff --git a/p4_symbolic/deparser_test.cc b/p4_symbolic/deparser_test.cc index 544fab25..4b985a45 100644 --- a/p4_symbolic/deparser_test.cc +++ b/p4_symbolic/deparser_test.cc @@ -16,6 +16,7 @@ #include +#include "absl/status/statusor.h" #include "absl/strings/string_view.h" #include "gmock/gmock.h" #include "gtest/gtest.h" @@ -25,14 +26,16 @@ #include "p4/v1/p4runtime.pb.h" #include "p4_pdpi/packetlib/packetlib.h" #include "p4_pdpi/packetlib/packetlib.pb.h" -#include "p4_symbolic/sai/fields.h" #include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/util.h" #include "p4_symbolic/z3_util.h" #include "z3++.h" namespace p4_symbolic { namespace { +using ::p4_symbolic::symbolic::util::GetHeaderValidityFieldName; + class SaiDeparserTest : public testing::Test { public: void SetUp() override { @@ -66,9 +69,10 @@ TEST_F(SaiDeparserTest, DeparseIngressAndEgressHeadersWithoutConstraints) { TEST_F(SaiDeparserTest, VlanPacketParserIntegrationTest) { // Add VLAN constraint. { - ASSERT_OK_AND_ASSIGN(SaiFields fields, - GetSaiFields(state_->context.ingress_headers)); - state_->solver->add(fields.headers.vlan->valid); + ASSERT_OK_AND_ASSIGN(z3::expr vlan_valid, + state_->context.ingress_headers.Get( + GetHeaderValidityFieldName("vlan"))); + state_->solver->add(vlan_valid); } // Solve and deparse. @@ -88,11 +92,18 @@ TEST_F(SaiDeparserTest, VlanPacketParserIntegrationTest) { TEST_F(SaiDeparserTest, Ipv4UdpPacketParserIntegrationTest) { // Add IPv4 + UDP (+ no VLAN) constraint. { - ASSERT_OK_AND_ASSIGN(SaiFields fields, - GetSaiFields(state_->context.ingress_headers)); - state_->solver->add(fields.headers.ipv4.valid); - state_->solver->add(fields.headers.udp.valid); - state_->solver->add(!fields.headers.vlan->valid); + ASSERT_OK_AND_ASSIGN(z3::expr ipv4_valid, + state_->context.ingress_headers.Get( + GetHeaderValidityFieldName("ipv4"))); + ASSERT_OK_AND_ASSIGN( + z3::expr udp_valid, + state_->context.ingress_headers.Get(GetHeaderValidityFieldName("udp"))); + ASSERT_OK_AND_ASSIGN(z3::expr vlan_valid, + state_->context.ingress_headers.Get( + GetHeaderValidityFieldName("vlan"))); + state_->solver->add(ipv4_valid); + state_->solver->add(udp_valid); + state_->solver->add(!vlan_valid); } // Solve and deparse. @@ -114,13 +125,20 @@ TEST_F(SaiDeparserTest, Ipv4UdpPacketParserIntegrationTest) { TEST_F(SaiDeparserTest, Ipv6TcpPacketParserIntegrationTest) { // Add IPv6 + TCP (+ no VLAN) constraint. { - ASSERT_OK_AND_ASSIGN(SaiFields fields, - GetSaiFields(state_->context.ingress_headers)); - state_->solver->add(!fields.headers.ipv4.valid); - state_->solver->add(fields.headers.tcp.valid); + ASSERT_OK_AND_ASSIGN(z3::expr ipv4_valid, + state_->context.ingress_headers.Get( + GetHeaderValidityFieldName("ipv4"))); + ASSERT_OK_AND_ASSIGN( + z3::expr tcp_valid, + state_->context.ingress_headers.Get(GetHeaderValidityFieldName("tcp"))); + ASSERT_OK_AND_ASSIGN(z3::expr vlan_valid, + state_->context.ingress_headers.Get( + GetHeaderValidityFieldName("vlan"))); + state_->solver->add(!ipv4_valid); + state_->solver->add(tcp_valid); // The only way to have a TCP packet that is not an IPv4 packet is to have // an IPv6 packet. - state_->solver->add(!fields.headers.vlan->valid); + state_->solver->add(!vlan_valid); } // Solve and deparse. @@ -142,10 +160,14 @@ TEST_F(SaiDeparserTest, Ipv6TcpPacketParserIntegrationTest) { TEST_F(SaiDeparserTest, ArpPacketParserIntegrationTest) { // Add ARP (+ no VLAN) constraint. { - ASSERT_OK_AND_ASSIGN(SaiFields fields, - GetSaiFields(state_->context.ingress_headers)); - state_->solver->add(fields.headers.arp.valid); - state_->solver->add(!fields.headers.vlan->valid); + ASSERT_OK_AND_ASSIGN( + z3::expr arp_valid, + state_->context.ingress_headers.Get(GetHeaderValidityFieldName("arp"))); + ASSERT_OK_AND_ASSIGN(z3::expr vlan_valid, + state_->context.ingress_headers.Get( + GetHeaderValidityFieldName("vlan"))); + state_->solver->add(arp_valid); + state_->solver->add(!vlan_valid); } // Solve and deparse. @@ -166,10 +188,14 @@ TEST_F(SaiDeparserTest, ArpPacketParserIntegrationTest) { TEST_F(SaiDeparserTest, IcmpPacketParserIntegrationTest) { // Add ICMP (+ no VLAN) constraint. { - ASSERT_OK_AND_ASSIGN(SaiFields fields, - GetSaiFields(state_->context.ingress_headers)); - state_->solver->add(fields.headers.icmp.valid); - state_->solver->add(!fields.headers.vlan->valid); + ASSERT_OK_AND_ASSIGN(z3::expr icmp_valid, + state_->context.ingress_headers.Get( + GetHeaderValidityFieldName("icmp"))); + ASSERT_OK_AND_ASSIGN(z3::expr vlan_valid, + state_->context.ingress_headers.Get( + GetHeaderValidityFieldName("vlan"))); + state_->solver->add(icmp_valid); + state_->solver->add(!vlan_valid); } // Solve and deparse. @@ -192,10 +218,10 @@ TEST_F(SaiDeparserTest, IcmpPacketParserIntegrationTest) { TEST_F(SaiDeparserTest, PacketInHeaderIsNeverParsedIntegrationTest) { // Add packet_in constraint. { - ASSERT_OK_AND_ASSIGN(SaiFields fields, - GetSaiFields(state_->context.ingress_headers)); - EXPECT_TRUE(fields.headers.packet_in.has_value()); - state_->solver->add(fields.headers.packet_in->valid); + ASSERT_OK_AND_ASSIGN(z3::expr packet_in_valid, + state_->context.ingress_headers.Get( + GetHeaderValidityFieldName("packet_in_header"))); + state_->solver->add(packet_in_valid); } // Should be unsatisfiable, because we never parse a packet-in header. diff --git a/p4_symbolic/packet_synthesizer/BUILD.bazel b/p4_symbolic/packet_synthesizer/BUILD.bazel index e368f8b1..32cc4d90 100644 --- a/p4_symbolic/packet_synthesizer/BUILD.bazel +++ b/p4_symbolic/packet_synthesizer/BUILD.bazel @@ -28,8 +28,8 @@ cc_library( "//p4_pdpi/string_encodings:decimal_string", "//p4_pdpi/utils:ir", "//p4_symbolic:z3_util", - "//p4_symbolic/sai:fields", "//p4_symbolic/symbolic", + "@com_github_z3prover_z3//:api", "@com_google_absl//absl/status", "@com_google_absl//absl/strings", ], diff --git a/p4_symbolic/packet_synthesizer/criteria_generator.cc b/p4_symbolic/packet_synthesizer/criteria_generator.cc index d063a688..c86174c5 100644 --- a/p4_symbolic/packet_synthesizer/criteria_generator.cc +++ b/p4_symbolic/packet_synthesizer/criteria_generator.cc @@ -21,7 +21,6 @@ #include "absl/strings/match.h" #include "absl/strings/str_cat.h" #include "absl/strings/string_view.h" -#include "gutil/status.h" #include "p4_pdpi/ir.pb.h" #include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/packet_synthesizer/coverage_goal.pb.h" @@ -29,6 +28,7 @@ #include "p4_symbolic/packet_synthesizer/packet_synthesis_criteria.pb.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/symbolic/table.h" +#include "p4_symbolic/symbolic/util.h" namespace p4_symbolic::packet_synthesizer { namespace { @@ -146,7 +146,7 @@ HeaderCriteria::FieldCriterion MakeHeaderValidityCriterion( absl::string_view header_name, bool valid) { HeaderCriteria::FieldCriterion field_criterion; field_criterion.mutable_field_match()->set_name( - absl::StrCat(header_name, ".$valid$")); + symbolic::util::GetHeaderValidityFieldName(header_name)); field_criterion.mutable_field_match()->mutable_exact()->set_hex_str( valid ? "0x1" : "0x0"); return field_criterion; diff --git a/p4_symbolic/packet_synthesizer/packet_synthesizer.cc b/p4_symbolic/packet_synthesizer/packet_synthesizer.cc index f93a3fa7..61e93832 100644 --- a/p4_symbolic/packet_synthesizer/packet_synthesizer.cc +++ b/p4_symbolic/packet_synthesizer/packet_synthesizer.cc @@ -37,7 +37,6 @@ #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/fields.h" #include "p4_symbolic/sai/sai.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/symbolic/util.h" @@ -52,30 +51,32 @@ using ::p4_symbolic::symbolic::SolverState; // 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) { + const SolverState& solver_state, absl::string_view packet_payload, + std::optional should_be_dropped) { z3::model model = solver_state.solver->get_model(); ASSIGN_OR_RETURN(std::string packet, - p4_symbolic::DeparseIngressPacket(solver_state, model)); - ASSIGN_OR_RETURN( - const bool dropped, - p4_symbolic::EvalZ3Bool(solver_state.context.trace.dropped, model)); - if (dropped != should_be_dropped) { + DeparseIngressPacket(solver_state, model)); + ASSIGN_OR_RETURN(const bool dropped, + EvalZ3Bool(solver_state.context.trace.dropped, model)); + if (should_be_dropped.has_value() && 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, + EvalZ3Bool(solver_state.context.trace.got_cloned, model)); + + // Get mirrored from the model. 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)); + std::string mirror_session_id_valid_field_name, + GetUserMetadataFieldName("mirror_session_id_valid", + solver_state.context.egress_headers)); + ASSIGN_OR_RETURN(z3::expr mirror_session_id_valid, + solver_state.context.egress_headers.Get( + mirror_session_id_valid_field_name)); + ASSIGN_OR_RETURN(const bool mirrored, + EvalZ3Bool(mirror_session_id_valid == 1, model)); // Get ingress port from the model. ASSIGN_OR_RETURN(std::string local_metadata_ingress_port, @@ -219,9 +220,9 @@ absl::StatusOr> PacketSynthesizer::Create( params.pi_entries().end()); std::vector physical_ports(params.physical_port().begin(), params.physical_port().end()); - p4_symbolic::symbolic::TranslationPerType translation_per_type; + symbolic::TranslationPerType translation_per_type; for (const auto& [type_name, data] : params.translation_per_type()) { - p4_symbolic::symbolic::values::TranslationData translation; + symbolic::values::TranslationData translation; translation.dynamic_translation = data.dynamic_translation(); for (const auto& mapping : data.static_mapping()) { translation.static_mapping.push_back( @@ -232,8 +233,8 @@ absl::StatusOr> PacketSynthesizer::Create( // Evaluate P4 pipeline to get solver_state. ASSIGN_OR_RETURN(auto solver_state, - p4_symbolic::symbolic::EvaluateP4Program( - config, entries, physical_ports, translation_per_type)); + symbolic::EvaluateP4Program(config, entries, physical_ports, + translation_per_type)); // TODO: Avoid generating packets that are always dropped. RETURN_IF_ERROR(AddSanePacketConstraints(*solver_state)); @@ -370,4 +371,7 @@ absl::Status PacketSynthesizer::PrepareZ3SolverStack( return absl::OkStatus(); } + +const SolverState& PacketSynthesizer::SolverState() { return solver_state_; } + } // namespace p4_symbolic::packet_synthesizer diff --git a/p4_symbolic/packet_synthesizer/util.cc b/p4_symbolic/packet_synthesizer/util.cc index 041a6a8b..9c99f889 100644 --- a/p4_symbolic/packet_synthesizer/util.cc +++ b/p4_symbolic/packet_synthesizer/util.cc @@ -20,10 +20,11 @@ #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/symbolic/util.h" #include "p4_symbolic/z3_util.h" +#include "z3++.h" namespace p4_symbolic { namespace packet_synthesizer { @@ -118,14 +119,11 @@ absl::StatusOr IsIpv6UnicastAddress(z3::expr ipv6_address) { // 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; - auto& vlan = ingress_fields.headers.vlan; - // ======Ethernet constraints====== + ASSIGN_OR_RETURN(z3::expr ethernet_src_addr, + state.context.ingress_headers.Get("ethernet.src_addr")); + ASSIGN_OR_RETURN(z3::expr ethernet_dst_addr, + state.context.ingress_headers.Get("ethernet.dst_addr")); // 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 @@ -136,10 +134,10 @@ absl::Status AddSanePacketConstraints( // 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)) == + 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}) { + 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 @@ -149,42 +147,54 @@ absl::Status AddSanePacketConstraints( } } // Require source MAC and destination MAC to differ. - state.solver->add(ethernet.src_addr != ethernet.dst_addr); + state.solver->add(ethernet_src_addr != ethernet_dst_addr); // ======IPv4 constraints====== + ASSIGN_OR_RETURN(z3::expr ipv4_src_addr, + state.context.ingress_headers.Get("ipv4.src_addr")); + ASSIGN_OR_RETURN(z3::expr ipv4_dst_addr, + state.context.ingress_headers.Get("ipv4.dst_addr")); // 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); + 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)); + 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)); + 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)); + 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====== + ASSIGN_OR_RETURN(z3::expr ipv6_src_addr, + state.context.ingress_headers.Get("ipv6.src_addr")); + ASSIGN_OR_RETURN(z3::expr ipv6_dst_addr, + state.context.ingress_headers.Get("ipv6.dst_addr")); // Src IP address should be a unicast address. { - ASSIGN_OR_RETURN(z3::expr constraint, IsIpv6UnicastAddress(ipv6.src_addr)); + 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)); + state.solver->add(ipv6_src_addr != Bitvector<128>(0)); + state.solver->add(ipv6_dst_addr != Bitvector<128>(0)); + // Neither src nor dst IPv6 addresses can be ::1 (loopback). + state.solver->add(ipv6_src_addr != Bitvector<128>(1)); + state.solver->add(ipv6_dst_addr != Bitvector<128>(1)); // ======VLAN constraints========== // TODO: Make unconditional when we no longer need // backwards-compatibility. - if (vlan.has_value()) { + bool vlan = state.context.ingress_headers.ContainsKey( + symbolic::util::GetHeaderValidityFieldName("vlan")); + if (vlan) { + ASSIGN_OR_RETURN(z3::expr vlan_id, + state.context.ingress_headers.Get("vlan.vlan_id")); // TODO: Consider testing the following VIDs when PacketIO is // properly modeled. - state.solver->add(vlan->vlan_id != Bitvector<12>(0xFFF)); - state.solver->add(vlan->vlan_id != Bitvector<12>(0x001)); + state.solver->add(vlan_id != Bitvector<12>(0xFFF)); + state.solver->add(vlan_id != Bitvector<12>(0x001)); } return absl::OkStatus(); diff --git a/p4_symbolic/sai/BUILD.bazel b/p4_symbolic/sai/BUILD.bazel index 091e22bd..118219ef 100644 --- a/p4_symbolic/sai/BUILD.bazel +++ b/p4_symbolic/sai/BUILD.bazel @@ -18,16 +18,35 @@ package( ) cc_library( - name = "fields", - srcs = ["fields.cc"], - hdrs = ["fields.h"], + name = "sai", + srcs = ["sai.cc"], + hdrs = ["sai.h"], deps = [ "//gutil:status", - "//p4_symbolic:z3_util", "//p4_symbolic/symbolic", - "@com_github_z3prover_z3//:api", - "@com_google_absl//absl/status", + "@com_google_absl//absl/container:flat_hash_set", + "@com_google_absl//absl/status", "@com_google_absl//absl/status:statusor", "@com_google_absl//absl/strings", ], ) + +cc_test( + name = "sai_test", + srcs = ["sai_test.cc"], + deps = [ + ":sai", + "//gutil:status_matchers", + "//gutil:testing", + "//p4_pdpi:ir", + "//p4_pdpi:pd", + "//p4_symbolic/symbolic", + "//sai_p4/instantiations/google:instantiations", + "//sai_p4/instantiations/google:sai_nonstandard_platforms_cc", + "//sai_p4/instantiations/google:sai_pd_cc_proto", + "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", + "@com_google_absl//absl/status", + "@com_google_absl//absl/strings", + "@com_google_googletest//:gtest_main", + ], +) diff --git a/p4_symbolic/sai/fields.cc b/p4_symbolic/sai/fields.cc deleted file mode 100644 index ef34c6c2..00000000 --- a/p4_symbolic/sai/fields.cc +++ /dev/null @@ -1,351 +0,0 @@ -// 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/sai/fields.h" - -#include -#include -#include -#include - -#include "absl/status/status.h" -#include "absl/status/statusor.h" -#include "absl/strings/ascii.h" -#include "absl/strings/match.h" -#include "absl/strings/str_join.h" -#include "absl/strings/string_view.h" -#include "gutil/status.h" -#include "p4_symbolic/symbolic/symbolic.h" -#include "p4_symbolic/z3_util.h" -#include "z3++.h" - -namespace p4_symbolic { - -using ::p4_symbolic::symbolic::SymbolicPerPacketState; - -absl::StatusOr GetUserMetadataFieldName( - const std::string& field, const SymbolicPerPacketState& state) { - // Compute set of mangled field names that match the given field name. - std::vector mangled_candidates; - - // p4c seems to use the following template to name user metadata fields: - // - // - Until ~ 2022-11-01: - // "scalars.userMetadata._" - // - // - After ~ 2022-11-01: - // "scalars.._", where - // is "local_metadata_t" in SAI P4. - // - // We look for names that match these templates. - // TODO: Remove `old_prefix` eventually when we no longer - // need backward compatibility. - const std::string old_prefix = absl::StrCat("scalars.userMetadata._", field); - const std::string new_prefix = - absl::StrCat("scalars.local_metadata_t._", field); - for (const auto& [key, _] : state) { - for (absl::string_view prefix : {old_prefix, new_prefix}) { - if (absl::StartsWith(key, prefix) && key.length() > prefix.length() && - absl::ascii_isdigit(key.at(prefix.length()))) { - mangled_candidates.push_back(key); - } - } - } - - if (mangled_candidates.size() == 1) { - return mangled_candidates.back(); - } - - auto error = gutil::InternalErrorBuilder() - << "unable to disambiguate metadata field '" << field << "': "; - if (mangled_candidates.empty()) { - return error << "no matching fields found in config: " - << absl::StrJoin(state, "\n - ", - [](std::string* out, const auto& key_value) { - absl::StrAppend(out, key_value.first); - }); - } - return error << "several mangled fields in the config match:\n- " - << 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. -// As a workaround, we unmangle the names, best effort. -absl::StatusOr GetUserMetadata(const std::string& field, - const SymbolicPerPacketState& state) { - ASSIGN_OR_RETURN(const std::string mangled_name, - GetUserMetadataFieldName(field, state)); - return state.Get(mangled_name); -} - -} // namespace - -absl::StatusOr GetSaiFields(const SymbolicPerPacketState& state) { - // Helpers to extract fields. - std::vector errors; - auto get_field = [&](const std::string& field) -> z3::expr { - auto result = state.Get(field); - if (result.ok()) return *result; - errors.push_back(result.status()); - // Return dummy. - return z3::expr(Z3Context()); - }; - auto get_metadata_field = [&](const std::string& field) -> z3::expr { - auto result = GetUserMetadata(field, state); - if (result.ok()) return *result; - errors.push_back(result.status()); - // Return dummy. - return z3::expr(Z3Context()); - }; - - // TODO: Make unconditional when we no longer need - // backwards-compatibility. - auto packet_in = - state.ContainsKey("packet_in_header.$valid$") - ? std::make_optional(SaiPacketIn{ - .valid = get_field("packet_in_header.$valid$"), - .ingress_port = get_field("packet_in_header.ingress_port"), - .target_egress_port = - get_field("packet_in_header.target_egress_port"), - .unused_pad = get_field("packet_in_header.unused_pad"), - }) - : std::nullopt; - 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"), - .src_addr = get_field("erspan_ethernet.src_addr"), - .ether_type = get_field("erspan_ethernet.ether_type"), - }; - auto erspan_ipv4 = SaiIpv4{ - .valid = get_field("erspan_ipv4.$valid$"), - .version = get_field("erspan_ipv4.version"), - .ihl = get_field("erspan_ipv4.ihl"), - .dscp = get_field("erspan_ipv4.dscp"), - .ecn = get_field("erspan_ipv4.ecn"), - .total_len = get_field("erspan_ipv4.total_len"), - .identification = get_field("erspan_ipv4.identification"), - .reserved = get_field("erspan_ipv4.reserved"), - .do_not_fragment = get_field("erspan_ipv4.do_not_fragment"), - .more_fragments = get_field("erspan_ipv4.more_fragments"), - .frag_offset = get_field("erspan_ipv4.frag_offset"), - .ttl = get_field("erspan_ipv4.ttl"), - .protocol = get_field("erspan_ipv4.protocol"), - .header_checksum = get_field("erspan_ipv4.header_checksum"), - .src_addr = get_field("erspan_ipv4.src_addr"), - .dst_addr = get_field("erspan_ipv4.dst_addr"), - }; - auto erspan_gre = SaiGre{ - .valid = get_field("erspan_gre.$valid$"), - .checksum_present = get_field("erspan_gre.checksum_present"), - .routing_present = get_field("erspan_gre.routing_present"), - .key_present = get_field("erspan_gre.key_present"), - .sequence_present = get_field("erspan_gre.sequence_present"), - .strict_source_route = get_field("erspan_gre.strict_source_route"), - .recursion_control = get_field("erspan_gre.recursion_control"), - .acknowledgement_present = - get_field("erspan_gre.acknowledgement_present"), - .flags = get_field("erspan_gre.flags"), - .version = get_field("erspan_gre.version"), - .protocol = get_field("erspan_gre.protocol"), - }; - auto ethernet = SaiEthernet{ - .valid = get_field("ethernet.$valid$"), - .dst_addr = get_field("ethernet.dst_addr"), - .src_addr = get_field("ethernet.src_addr"), - .ether_type = get_field("ethernet.ether_type"), - }; - // TODO: Make unconditional when we no longer need - // backwards-compatibility. - auto vlan = - state.ContainsKey("vlan.$valid$") - ? std::make_optional(SaiVlan{ - .valid = get_field("vlan.$valid$"), - .priority_code_point = get_field("vlan.priority_code_point"), - .drop_eligible_indicator = - get_field("vlan.drop_eligible_indicator"), - .vlan_id = get_field("vlan.vlan_id"), - .ether_type = get_field("vlan.ether_type"), - }) - : std::nullopt; - auto tunnel_encap_ipv6 = SaiIpv6{ - .valid = get_field("tunnel_encap_ipv6.$valid$"), - .version = get_field("tunnel_encap_ipv6.version"), - .dscp = get_field("tunnel_encap_ipv6.dscp"), - .ecn = get_field("tunnel_encap_ipv6.ecn"), - .flow_label = get_field("tunnel_encap_ipv6.flow_label"), - .payload_length = get_field("tunnel_encap_ipv6.payload_length"), - .next_header = get_field("tunnel_encap_ipv6.next_header"), - .hop_limit = get_field("tunnel_encap_ipv6.hop_limit"), - .src_addr = get_field("tunnel_encap_ipv6.src_addr"), - .dst_addr = get_field("tunnel_encap_ipv6.dst_addr"), - }; - auto tunnel_encap_gre = SaiGre{ - .valid = get_field("tunnel_encap_gre.$valid$"), - .checksum_present = get_field("tunnel_encap_gre.checksum_present"), - .routing_present = get_field("tunnel_encap_gre.routing_present"), - .key_present = get_field("tunnel_encap_gre.key_present"), - .sequence_present = get_field("tunnel_encap_gre.sequence_present"), - .strict_source_route = get_field("tunnel_encap_gre.strict_source_route"), - .recursion_control = get_field("tunnel_encap_gre.recursion_control"), - .acknowledgement_present = - get_field("tunnel_encap_gre.acknowledgement_present"), - .flags = get_field("tunnel_encap_gre.flags"), - .version = get_field("tunnel_encap_gre.version"), - .protocol = get_field("tunnel_encap_gre.protocol"), - }; - auto ipv4 = SaiIpv4{ - .valid = get_field("ipv4.$valid$"), - .version = get_field("ipv4.version"), - .ihl = get_field("ipv4.ihl"), - .dscp = get_field("ipv4.dscp"), - .ecn = get_field("ipv4.ecn"), - .total_len = get_field("ipv4.total_len"), - .identification = get_field("ipv4.identification"), - .reserved = get_field("ipv4.reserved"), - .do_not_fragment = get_field("ipv4.do_not_fragment"), - .more_fragments = get_field("ipv4.more_fragments"), - .frag_offset = get_field("ipv4.frag_offset"), - .ttl = get_field("ipv4.ttl"), - .protocol = get_field("ipv4.protocol"), - .header_checksum = get_field("ipv4.header_checksum"), - .src_addr = get_field("ipv4.src_addr"), - .dst_addr = get_field("ipv4.dst_addr"), - }; - auto ipv6 = SaiIpv6{ - .valid = get_field("ipv6.$valid$"), - .version = get_field("ipv6.version"), - .dscp = get_field("ipv6.dscp"), - .ecn = get_field("ipv6.ecn"), - .flow_label = get_field("ipv6.flow_label"), - .payload_length = get_field("ipv6.payload_length"), - .next_header = get_field("ipv6.next_header"), - .hop_limit = get_field("ipv6.hop_limit"), - .src_addr = get_field("ipv6.src_addr"), - .dst_addr = get_field("ipv6.dst_addr"), - }; - auto udp = SaiUdp{ - .valid = get_field("udp.$valid$"), - .src_port = get_field("udp.src_port"), - .dst_port = get_field("udp.dst_port"), - .hdr_length = get_field("udp.hdr_length"), - .checksum = get_field("udp.checksum"), - }; - auto tcp = SaiTcp{ - .valid = get_field("tcp.$valid$"), - .src_port = get_field("tcp.src_port"), - .dst_port = get_field("tcp.dst_port"), - .seq_no = get_field("tcp.seq_no"), - .ack_no = get_field("tcp.ack_no"), - .data_offset = get_field("tcp.data_offset"), - .res = get_field("tcp.res"), - .flags = get_field("tcp.flags"), - .window = get_field("tcp.window"), - .checksum = get_field("tcp.checksum"), - .urgent_ptr = get_field("tcp.urgent_ptr"), - }; - auto icmp = SaiIcmp{ - .valid = get_field("icmp.$valid$"), - .type = get_field("icmp.type"), - .code = get_field("icmp.code"), - .checksum = get_field("icmp.checksum"), - }; - auto arp = SaiArp{ - .valid = get_field("arp.$valid$"), - .hw_type = get_field("arp.hw_type"), - .proto_type = get_field("arp.proto_type"), - .hw_addr_len = get_field("arp.hw_addr_len"), - .proto_addr_len = get_field("arp.proto_addr_len"), - .opcode = get_field("arp.opcode"), - .sender_hw_addr = get_field("arp.sender_hw_addr"), - .sender_proto_addr = get_field("arp.sender_proto_addr"), - .target_hw_addr = get_field("arp.target_hw_addr"), - .target_proto_addr = get_field("arp.target_proto_addr"), - }; - auto local_metadata = SaiLocalMetadata{ - // TODO: Make unconditional when we no longer need - // backwards-compatibility. - .vlan_id = GetUserMetadata("vlan_id", state).ok() - ? std::make_optional(get_metadata_field("vlan_id")) - : std::nullopt, - .vlan_id_valid = - GetUserMetadata("vlan_id_valid", state).ok() - ? std::make_optional(get_metadata_field("vlan_id_valid")) - : std::nullopt, - .admit_to_l3 = get_metadata_field("admit_to_l3"), - .vrf_id = get_metadata_field("vrf_id"), - .l4_src_port = get_metadata_field("l4_src_port"), - .l4_dst_port = get_metadata_field("l4_dst_port"), - .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-compatibility. - .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"), - }; - - if (!errors.empty()) { - return gutil::InternalErrorBuilder() - << "Errors while trying to extract hard coded fields:\n- " - << absl::StrJoin(errors, "\n- ", - [](std::string* out, const absl::Status& error) { - absl::StrAppend(out, error.ToString()); - }); - } - return SaiFields{ - .headers = - SaiHeaders{ - .packet_in = packet_in, - .packet_out = packet_out, - .erspan_ethernet = erspan_ethernet, - .erspan_ipv4 = erspan_ipv4, - .erspan_gre = erspan_gre, - .ethernet = ethernet, - .vlan = vlan, - .tunnel_encap_ipv6 = tunnel_encap_ipv6, - .tunnel_encap_gre = tunnel_encap_gre, - .ipv4 = ipv4, - .ipv6 = ipv6, - .udp = udp, - .tcp = tcp, - .icmp = icmp, - .arp = arp, - }, - .local_metadata = local_metadata, - .standard_metadata = standard_metadata, - }; -} - -} // namespace p4_symbolic diff --git a/p4_symbolic/sai/fields.h b/p4_symbolic/sai/fields.h deleted file mode 100644 index bf286d5d..00000000 --- a/p4_symbolic/sai/fields.h +++ /dev/null @@ -1,234 +0,0 @@ -// 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. - -// This file exposes the SAI header/metadata fields as Z3 expressions, making it -// easy to formulate constraints on these fields. - -#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_in_header_t` in metadata.p4. -struct SaiPacketIn { - z3::expr valid; - z3::expr ingress_port; - z3::expr target_egress_port; - z3::expr unused_pad; -}; - -// 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; - z3::expr dst_addr; - z3::expr src_addr; - z3::expr ether_type; -}; - -// Symbolic version of `struct vlan_t` in headers.p4. -struct SaiVlan { - z3::expr valid; - z3::expr priority_code_point; - z3::expr drop_eligible_indicator; - z3::expr vlan_id; - z3::expr ether_type; -}; - -// Symbolic version of `struct ipv4_t` in headers.p4. -struct SaiIpv4 { - z3::expr valid; - z3::expr version; - z3::expr ihl; - z3::expr dscp; - z3::expr ecn; - z3::expr total_len; - z3::expr identification; - z3::expr reserved; - z3::expr do_not_fragment; - z3::expr more_fragments; - z3::expr frag_offset; - z3::expr ttl; - z3::expr protocol; - z3::expr header_checksum; - z3::expr src_addr; - z3::expr dst_addr; -}; - -// Symbolic version of `struct ipv6_t` in headers.p4. -struct SaiIpv6 { - z3::expr valid; - z3::expr version; - z3::expr dscp; - z3::expr ecn; - z3::expr flow_label; - z3::expr payload_length; - z3::expr next_header; - z3::expr hop_limit; - z3::expr src_addr; - z3::expr dst_addr; -}; - -// Symbolic version of `struct udp_t` in headers.p4. -struct SaiUdp { - z3::expr valid; - z3::expr src_port; - z3::expr dst_port; - z3::expr hdr_length; - z3::expr checksum; -}; - -// Symbolic version of `struct tcp_t` in headers.p4. -struct SaiTcp { - z3::expr valid; - z3::expr src_port; - z3::expr dst_port; - z3::expr seq_no; - z3::expr ack_no; - z3::expr data_offset; - z3::expr res; - z3::expr flags; - z3::expr window; - z3::expr checksum; - z3::expr urgent_ptr; -}; - -// Symbolic version of `struct icmp_t` in headers.p4. -struct SaiIcmp { - z3::expr valid; - z3::expr type; - z3::expr code; - z3::expr checksum; -}; - -// Symbolic version of `struct arp_t` in headers.p4. -struct SaiArp { - z3::expr valid; - z3::expr hw_type; - z3::expr proto_type; - z3::expr hw_addr_len; - z3::expr proto_addr_len; - z3::expr opcode; - z3::expr sender_hw_addr; - z3::expr sender_proto_addr; - z3::expr target_hw_addr; - z3::expr target_proto_addr; -}; - -// Symbolic version of `struct gre_t` in headers.p4. -struct SaiGre { - z3::expr valid; - z3::expr checksum_present; - z3::expr routing_present; - z3::expr key_present; - z3::expr sequence_present; - z3::expr strict_source_route; - z3::expr recursion_control; - z3::expr acknowledgement_present; - z3::expr flags; - z3::expr version; - z3::expr protocol; -}; - -// Symbolic version of `struct headers_t` in metadata.p4. -struct SaiHeaders { - // TODO: Make unconditional when we no longer need - // backwards-compatibility. - std::optional packet_in; - std::optional packet_out; - - SaiEthernet erspan_ethernet; - SaiIpv4 erspan_ipv4; - SaiGre erspan_gre; - SaiEthernet ethernet; - // TODO: Make unconditional when we no longer need - // backwards-compatibility. - std::optional vlan; - - // Not extracted during parsing. - SaiIpv6 tunnel_encap_ipv6; - SaiGre tunnel_encap_gre; - - SaiIpv4 ipv4; - SaiIpv6 ipv6; - SaiUdp udp; - SaiTcp tcp; - SaiIcmp icmp; - SaiArp arp; -}; - -// Symbolic version of `struct local_metadata_t` in metadata.p4. -// TODO: add missing fields. -struct SaiLocalMetadata { - // TODO: Make unconditional when we no longer need - // backwards-compatibility. - std::optional vlan_id; - std::optional vlan_id_valid; - z3::expr admit_to_l3; - z3::expr vrf_id; - z3::expr l4_src_port; - z3::expr l4_dst_port; - z3::expr mirror_session_id_valid; - z3::expr ingress_port; - z3::expr route_metadata; - // TODO: Make unconditional when we no longer need - // backwards-compatibility. - std::optional bypass_ingress; -}; - -// Symbolic version of `struct standard_metadata_t` in v1model.p4 -// TODO: Add missing fields, as needed. -struct V1ModelStandardMetadata { - z3::expr ingress_port; -}; - -struct SaiFields { - SaiHeaders headers; - SaiLocalMetadata local_metadata; - V1ModelStandardMetadata standard_metadata; -}; - -absl::StatusOr -GetSaiFields(const symbolic::SymbolicPerPacketState &state); - -// The p4c compiler "mangles" field names of user defined metadata and the -// mangled name is used in some places in p4-symbolic. This function returns -// the mangled name of a given user defined metadata field. Note that this is a -// workaround and done in a best effort fashion. -absl::StatusOr -GetUserMetadataFieldName(const std::string &field, - const symbolic::SymbolicPerPacketState &state); - -// P4-Symbolic adds a special field ("$valid$") to each header corresponding to -// its validity. This function returns a field reference (in form of -//
.) to the 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/fields_test.cc b/p4_symbolic/sai/fields_test.cc deleted file mode 100644 index fb3cc669..00000000 --- a/p4_symbolic/sai/fields_test.cc +++ /dev/null @@ -1,54 +0,0 @@ -// 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/sai/fields.h" - -#include -#include - -#include "absl/status/statusor.h" -#include "gmock/gmock.h" -#include "gtest/gtest.h" -#include "gutil/status_matchers.h" -#include "p4_symbolic/symbolic/symbolic.h" -#include "sai_p4/instantiations/google/instantiations.h" -#include "sai_p4/instantiations/google/sai_nonstandard_platforms.h" - -namespace p4_symbolic { -namespace { - -TEST(GetSaiFields, CanGetIngressAndEgressFieldsForAllInstantiations) { - for (auto instantiation : sai::AllSaiInstantiations()) { - const auto config = sai::GetNonstandardForwardingPipelineConfig( - instantiation, sai::NonstandardPlatform::kP4Symbolic); - ASSERT_OK_AND_ASSIGN(auto state, symbolic::EvaluateP4Program( - config, /*entries=*/{}, /*ports=*/{})); - for (auto& headers : - {state->context.ingress_headers, state->context.egress_headers}) { - EXPECT_OK(GetSaiFields(headers).status()); - } - } -} - -TEST(GetUserMetadataFieldNameTest, FailsForNonExistingFields) { - const auto config = sai::GetNonstandardForwardingPipelineConfig( - sai::Instantiation::kMiddleblock, sai::NonstandardPlatform::kP4Symbolic); - ASSERT_OK_AND_ASSIGN(auto state, symbolic::EvaluateP4Program( - config, /*entries=*/{}, /*ports=*/{})); - ASSERT_THAT(GetUserMetadataFieldName("dummy_nonexisting_field", - state->context.ingress_headers), - gutil::StatusIs(absl::StatusCode::kInternal)); -} - -} // namespace -} // namespace p4_symbolic diff --git a/p4_symbolic/sai/sai.cc b/p4_symbolic/sai/sai.cc index cd5adcee..44951248 100644 --- a/p4_symbolic/sai/sai.cc +++ b/p4_symbolic/sai/sai.cc @@ -22,23 +22,26 @@ #include "absl/container/flat_hash_set.h" #include "absl/status/status.h" +#include "absl/strings/ascii.h" +#include "absl/strings/match.h" #include "absl/strings/str_cat.h" +#include "absl/strings/str_join.h" +#include "absl/strings/string_view.h" #include "gutil/status.h" -#include "p4_symbolic/sai/fields.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/symbolic/values.h" namespace p4_symbolic { absl::Status CheckPhysicalPortAndPortIdTypeValueConsistency( - const std::vector& physical_ports, - const symbolic::TranslationPerType& translation_per_type) { + const std::vector &physical_ports, + const symbolic::TranslationPerType &translation_per_type) { absl::flat_hash_set physical_port_set(physical_ports.begin(), physical_ports.end()); absl::flat_hash_set numeric_value_set; if (auto it = translation_per_type.find(kPortIdTypeName); it != translation_per_type.end()) { - for (const auto& [_, numeric_value] : it->second.static_mapping) + for (const auto &[_, numeric_value] : it->second.static_mapping) numeric_value_set.insert(numeric_value); } @@ -52,7 +55,7 @@ absl::Status CheckPhysicalPortAndPortIdTypeValueConsistency( } absl::Status AddVrfIdTypeTranslation( - symbolic::TranslationPerType& translation_per_type) { + symbolic::TranslationPerType &translation_per_type) { if (translation_per_type.contains(kVrfIdTypeName)) { return absl::InvalidArgumentError(absl::StrCat( "Did not expect user defined translation for ", kVrfIdTypeName)); @@ -68,23 +71,73 @@ absl::Status AddVrfIdTypeTranslation( return absl::OkStatus(); } +absl::StatusOr GetUserMetadataFieldName( + absl::string_view field_name, + const symbolic::SymbolicPerPacketState &state) { + // Compute set of mangled field names that match the given field name. + std::vector mangled_candidates; + + // p4c seems to use the following template to name user metadata fields: + // + // - Until ~ 2022-11-01: + // "scalars.userMetadata._" + // + // - After ~ 2022-11-01: + // "scalars.._", where + // is the header type name of the given + // `header_name`. + // + // We look for names that match these templates. + // TODO: Remove the old prefix eventually when we no + // longer need backward compatibility. + std::vector fully_qualified_field_prefixes; + fully_qualified_field_prefixes.reserve(2); + // Old prefix. + fully_qualified_field_prefixes.push_back( + absl::StrCat("scalars.userMetadata._", field_name)); + // New prefix. Note that this is SAI-specific. + fully_qualified_field_prefixes.push_back( + absl::StrCat("scalars.local_metadata_t._", field_name)); + + for (const auto &[key, _] : state) { + for (absl::string_view prefix : fully_qualified_field_prefixes) { + if (absl::StartsWith(key, prefix) && key.length() > prefix.length() && + absl::ascii_isdigit(key.at(prefix.length()))) { + mangled_candidates.push_back(key); + } + } + } + + if (mangled_candidates.size() == 1) { + return mangled_candidates.back(); + } + + auto error = gutil::InternalErrorBuilder() + << "unable to disambiguate metadata field '" << field_name + << "': "; + if (mangled_candidates.empty()) { + return error << "no matching fields found in config: " + << absl::StrJoin(state, "\n - ", + [](std::string *out, const auto &key_value) { + absl::StrAppend(out, key_value.first); + }); + } + return error << "several mangled fields in the config match:\n- " + << absl::StrJoin(mangled_candidates, "\n- "); +} + absl::StatusOr GetLocalMetadataIngressPortFromModel( - const symbolic::SolverState& solver_state) { - // We are interested in the value after parsing because the parser sets - // `local_metadata.ingress_port = standard_metadata.ingress_port`. Also, - // according to P4-16 spec, the metadata of the ingress packet may contain - // arbitrary value before being initialized. - ASSIGN_OR_RETURN(SaiFields parsed_fields, - GetSaiFields(solver_state.context.parsed_headers)); - ASSIGN_OR_RETURN(const std::string local_metadata_ingress_port_field_name, + const symbolic::SolverState &solver_state) { + ASSIGN_OR_RETURN(std::string ingress_port_field_name, GetUserMetadataFieldName( "ingress_port", solver_state.context.parsed_headers)); - // Note: Do NOT directly use "local_metadata.ingress_port" as the field name - // (see p4_symbolic::GetUserMetadataFieldName). + ASSIGN_OR_RETURN( + z3::expr ingress_port_expr, + solver_state.context.parsed_headers.Get(ingress_port_field_name)); return symbolic::values::TranslateValueToP4RT( - local_metadata_ingress_port_field_name, + ingress_port_field_name, solver_state.solver->get_model() - .eval(parsed_fields.local_metadata.ingress_port, true) + .eval(ingress_port_expr, true) .to_string(), solver_state.translator); } diff --git a/p4_symbolic/sai/sai.h b/p4_symbolic/sai/sai.h index ba60770c..2a061ad5 100644 --- a/p4_symbolic/sai/sai.h +++ b/p4_symbolic/sai/sai.h @@ -40,8 +40,17 @@ absl::Status CheckPhysicalPortAndPortIdTypeValueConsistency( absl::Status AddVrfIdTypeTranslation( symbolic::TranslationPerType& translation_per_type); -// Returns the concrete value of the field `local_metadata.ingress_port` right -// after parser processing based on the given model. +// Returns the mangled user metadata field name of the given `header_name` and +// `field_name`. Note that this function is specific to SAI because it assumes +// the local metadata header type name to be `local_metadata_t`. +absl::StatusOr GetUserMetadataFieldName( + absl::string_view field_name, + const symbolic::SymbolicPerPacketState& state); + +// Returns the concrete value of `local_metadata.ingress_port` given the +// `solver_state`. Note that this function is specific to SAI because it assumes +// the existence of `local_metadata_t` header type and that the header type has +// a field called `ingress_port`. absl::StatusOr GetLocalMetadataIngressPortFromModel( const symbolic::SolverState& solver_state); diff --git a/p4_symbolic/symbolic/util.cc b/p4_symbolic/symbolic/util.cc index b86134e3..0a861a2e 100644 --- a/p4_symbolic/symbolic/util.cc +++ b/p4_symbolic/symbolic/util.cc @@ -249,6 +249,10 @@ absl::StatusOr GetFieldBitwidth(absl::string_view field_name, } } +std::string GetHeaderValidityFieldName(absl::string_view header_name) { + return absl::StrCat(header_name, ".", kValidPseudoField); +} + } // namespace util } // namespace symbolic } // namespace p4_symbolic diff --git a/p4_symbolic/symbolic/util.h b/p4_symbolic/symbolic/util.h index 06ab1232..c07a9d31 100644 --- a/p4_symbolic/symbolic/util.h +++ b/p4_symbolic/symbolic/util.h @@ -68,8 +68,11 @@ MergeDisjointTableMatches(const SymbolicTableMatches &lhs, absl::StatusOr GetFieldBitwidth(absl::string_view field_name, const ir::P4Program &program); -} // namespace util -} // namespace symbolic -} // namespace p4_symbolic +// Returns the full valid field name of the given header. +std::string GetHeaderValidityFieldName(absl::string_view header_name); + +} // namespace util +} // namespace symbolic +} // namespace p4_symbolic #endif // P4_SYMBOLIC_SYMBOLIC_UTIL_H_ From b88cc32c15ce1e4b3b252d5bcb8672c2e62f30db Mon Sep 17 00:00:00 2001 From: kishanps Date: Thu, 29 Jun 2023 21:28:41 -0700 Subject: [PATCH 5/7] [P4-Symbolic] Add non-SAI tests for the generic deparser. Output concrete solutions to a file instead of standard output. --- p4_symbolic/BUILD.bazel | 9 +- p4_symbolic/deparser_test.cc | 150 ++++++++++++++++++++++++++++--- p4_symbolic/ir/test.bzl | 19 ++-- p4_symbolic/ir/test.cc | 5 +- p4_symbolic/main.cc | 114 +++++++++++++---------- p4_symbolic/symbolic/BUILD.bazel | 12 +-- p4_symbolic/symbolic/test.bzl | 23 +++-- p4_symbolic/test_util.cc | 70 +++++++++------ p4_symbolic/test_util.h | 11 +-- 9 files changed, 296 insertions(+), 117 deletions(-) diff --git a/p4_symbolic/BUILD.bazel b/p4_symbolic/BUILD.bazel index 2a8484fa..d3f2cd24 100644 --- a/p4_symbolic/BUILD.bazel +++ b/p4_symbolic/BUILD.bazel @@ -27,7 +27,9 @@ cc_binary( deps = [ ":test_util", "//gutil:io", + "//p4_pdpi/internal:ordered_map", "//p4_symbolic/symbolic", + "@com_github_google_glog//:glog", "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", "@com_google_absl//absl/flags:flag", "@com_google_absl//absl/flags:parse", @@ -79,6 +81,7 @@ cc_library( "@com_github_p4lang_p4runtime//:p4info_cc_proto", "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", "@com_google_absl//absl/status:statusor", + "@com_google_absl//absl/strings", ], ) @@ -86,14 +89,16 @@ cc_test( name = "deparser_test", srcs = ["deparser_test.cc"], data = [ + "//p4_symbolic/testdata:ipv4-routing/basic.config.json", + "//p4_symbolic/testdata:ipv4-routing/basic.p4info.pb.txt", + "//p4_symbolic/testdata:ipv4-routing/entries.pb.txt", "//p4_symbolic/testdata:parser/sai_parser.config.json", "//p4_symbolic/testdata:parser/sai_parser.p4info.pb.txt", ], deps = [ ":deparser", + ":test_util", ":z3_util", - "//gutil:io", - "//gutil:proto", "//gutil:status_matchers", "//p4_pdpi/packetlib", "//p4_pdpi/packetlib:packetlib_cc_proto", diff --git a/p4_symbolic/deparser_test.cc b/p4_symbolic/deparser_test.cc index 4b985a45..50ad2400 100644 --- a/p4_symbolic/deparser_test.cc +++ b/p4_symbolic/deparser_test.cc @@ -15,19 +15,20 @@ #include "p4_symbolic/deparser.h" #include +#include #include "absl/status/statusor.h" +#include "absl/strings/match.h" #include "absl/strings/string_view.h" #include "gmock/gmock.h" #include "gtest/gtest.h" -#include "gutil/io.h" -#include "gutil/proto.h" #include "gutil/status_matchers.h" #include "p4/v1/p4runtime.pb.h" #include "p4_pdpi/packetlib/packetlib.h" #include "p4_pdpi/packetlib/packetlib.pb.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/symbolic/util.h" +#include "p4_symbolic/test_util.h" #include "p4_symbolic/z3_util.h" #include "z3++.h" @@ -36,20 +37,149 @@ namespace { using ::p4_symbolic::symbolic::util::GetHeaderValidityFieldName; +class IPv4RoutingBasicTest : public testing::Test { + public: + void SetUp() override { + constexpr absl::string_view bmv2_json_path = + "p4_symbolic/testdata/ipv4-routing/" + "basic.config.json"; + constexpr absl::string_view p4info_path = + "p4_symbolic/testdata/ipv4-routing/" + "basic.p4info.pb.txt"; + constexpr absl::string_view entries_path = + "p4_symbolic/testdata/ipv4-routing/" + "entries.pb.txt"; + ASSERT_OK_AND_ASSIGN( + p4::v1::ForwardingPipelineConfig config, + ParseToForwardingPipelineConfig(bmv2_json_path, p4info_path)); + ASSERT_OK_AND_ASSIGN( + std::vector entries, + GetPiTableEntriesFromPiUpdatesProtoTextFile(entries_path)); + Z3Context(/*renew=*/true); + ASSERT_OK_AND_ASSIGN(state_, symbolic::EvaluateP4Program(config, entries)); + } + + protected: + std::unique_ptr state_; +}; + +TEST_F(IPv4RoutingBasicTest, DeparseIngressAndEgressHeadersWithoutConstraints) { + ASSERT_EQ(state_->solver->check(), z3::check_result::sat); + auto model = state_->solver->get_model(); + EXPECT_OK(DeparseIngressPacket(*state_, model).status()); + EXPECT_OK(DeparseEgressPacket(*state_, model).status()); +} + +TEST_F(IPv4RoutingBasicTest, DeparseIngressHeaders1) { + // Add constraints. + { + ASSERT_OK_AND_ASSIGN( + z3::expr eth_dst_addr, + state_->context.egress_headers.Get("ethernet.dstAddr")); + state_->solver->add(eth_dst_addr == Z3Context().bv_val(0, 48)); + state_->solver->add(state_->context.egress_port == + Z3Context().bv_val(1, 9)); + + ASSERT_OK_AND_ASSIGN( + z3::expr ipv4_valid, + state_->context.ingress_headers.Get( + symbolic::util::GetHeaderValidityFieldName("ipv4"))); + state_->solver->add(ipv4_valid); + } + + // Solve and deparse. + ASSERT_EQ(state_->solver->check(), z3::check_result::sat); + auto model = state_->solver->get_model(); + ASSERT_OK_AND_ASSIGN(std::string raw_packet, + DeparseIngressPacket(*state_, model)); + + // Check that we got an IPv4 packet with destination address 10.10.0.0. + packetlib::Packet packet = packetlib::ParsePacket(raw_packet); + LOG(INFO) << "Z3-generated packet = " << packet.DebugString(); + ASSERT_GE(packet.headers_size(), 2); + EXPECT_TRUE(packet.headers(0).has_ethernet_header()); + EXPECT_TRUE(packet.headers(1).has_ipv4_header()); + EXPECT_EQ(packet.headers(1).ipv4_header().ipv4_destination(), "10.10.0.0"); +} + +TEST_F(IPv4RoutingBasicTest, DeparseIngressHeaders2) { + // Add constraints. + { + ASSERT_OK_AND_ASSIGN( + z3::expr eth_dst_addr, + state_->context.egress_headers.Get("ethernet.dstAddr")); + state_->solver->add(eth_dst_addr == + Z3Context().bv_val((22UL << 40) + 22, 48)); + state_->solver->add(state_->context.egress_port == + Z3Context().bv_val(1, 9)); + + ASSERT_OK_AND_ASSIGN( + z3::expr ipv4_valid, + state_->context.ingress_headers.Get( + symbolic::util::GetHeaderValidityFieldName("ipv4"))); + state_->solver->add(ipv4_valid); + } + + // Solve and deparse. + ASSERT_EQ(state_->solver->check(), z3::check_result::sat); + auto model = state_->solver->get_model(); + ASSERT_OK_AND_ASSIGN(std::string raw_packet, + DeparseIngressPacket(*state_, model)); + + // Check that we got an IPv4 packet with destination within 20.20.0.0/16. + packetlib::Packet packet = packetlib::ParsePacket(raw_packet); + LOG(INFO) << "Z3-generated packet = " << packet.DebugString(); + ASSERT_GE(packet.headers_size(), 2); + EXPECT_TRUE(packet.headers(0).has_ethernet_header()); + EXPECT_TRUE(packet.headers(1).has_ipv4_header()); + EXPECT_TRUE(absl::StartsWith( + packet.headers(1).ipv4_header().ipv4_destination(), "20.20.")); +} + +TEST_F(IPv4RoutingBasicTest, DeparseEgressHeaders) { + // Add constraints. + { + ASSERT_OK_AND_ASSIGN(z3::expr ipv4_dst_addr, + state_->context.ingress_headers.Get("ipv4.dstAddr")); + state_->solver->add(ipv4_dst_addr == + Z3Context().bv_val((10UL << 24) + 1, 32)); + + ASSERT_OK_AND_ASSIGN( + z3::expr ipv4_valid, + state_->context.ingress_headers.Get( + symbolic::util::GetHeaderValidityFieldName("ipv4"))); + state_->solver->add(ipv4_valid); + } + + // Solve and deparse. + ASSERT_EQ(state_->solver->check(), z3::check_result::sat); + auto model = state_->solver->get_model(); + ASSERT_OK_AND_ASSIGN(std::string raw_packet, + DeparseEgressPacket(*state_, model)); + + // Check that we got an IPv4 packet with destination MAC 00:00:00:00:00:0a. + packetlib::Packet packet = packetlib::ParsePacket(raw_packet); + LOG(INFO) << "Z3-generated packet = " << packet.DebugString(); + ASSERT_GE(packet.headers_size(), 2); + EXPECT_TRUE(packet.headers(0).has_ethernet_header()); + EXPECT_TRUE(packet.headers(1).has_ipv4_header()); + EXPECT_EQ(packet.headers(0).ethernet_header().ethernet_destination(), + "00:00:00:00:00:0a"); + EXPECT_EQ(packet.headers(1).ipv4_header().ipv4_destination(), "10.0.0.1"); +} + class SaiDeparserTest : public testing::Test { public: void SetUp() override { + constexpr absl::string_view bmv2_json_path = + "p4_symbolic/testdata/parser/" + "sai_parser.config.json"; constexpr absl::string_view p4info_path = "p4_symbolic/testdata/parser/" "sai_parser.p4info.pb.txt"; - constexpr absl::string_view p4_config_path = - "p4_symbolic/testdata/parser/" - "sai_parser.config.json"; - p4::v1::ForwardingPipelineConfig config; - ASSERT_OK(gutil::ReadProtoFromFile(p4info_path, config.mutable_p4info())); - ASSERT_OK_AND_ASSIGN(*config.mutable_p4_device_config(), - gutil::ReadFile(std::string(p4_config_path))); - + ASSERT_OK_AND_ASSIGN( + p4::v1::ForwardingPipelineConfig config, + ParseToForwardingPipelineConfig(bmv2_json_path, p4info_path)); Z3Context(/*renew=*/true); ASSERT_OK_AND_ASSIGN(state_, symbolic::EvaluateP4Program(config, /*entries=*/{})); diff --git a/p4_symbolic/ir/test.bzl b/p4_symbolic/ir/test.bzl index d3d85255..82a3e210 100644 --- a/p4_symbolic/ir/test.bzl +++ b/p4_symbolic/ir/test.bzl @@ -25,8 +25,7 @@ load("@com_github_p4lang_p4c//:bazel/p4_library.bzl", "p4_library") load("//p4_pdpi/testing:diff_test.bzl", "diff_test") def ir_parsing_test(name, p4_program, golden_file, table_entries = None, p4_deps = []): - """Macro that defines exact diff IR testing rules for a given p4 program - with all their dependent rules. + """Macro that defines exact diff IR testing rules for a given p4 program. The macro defines these rules in order: 1. A rule for producing bmv2 json and p4info files from a .p4 file using p4c. @@ -36,6 +35,13 @@ def ir_parsing_test(name, p4_program, golden_file, table_entries = None, p4_deps specified expected file. Use the p4_deps list to specify dependent files that p4_program input fle depends on (e.g. by including them). + + Args: + name: Test name. + p4_program: Input P4 program. + golden_file: File containing the expected IR output. + table_entries: File containing the table entries as input in protobuf text. + p4_deps: List of targets that the P4 program depends on (e.g., included files) """ bmv2_file = "tmp/%s.bmv2.json" % name p4info_file = "tmp/%s.p4info.pb.txt" % name @@ -76,10 +82,11 @@ def ir_parsing_test(name, p4_program, golden_file, table_entries = None, p4_deps ("--entries=$(location %s)" % table_entries if table_entries else ""), ("--output=$(location %s)" % test_output_file), "|| true", - # The following line makes sure hexstrings are lowercase in the protobuf file. - # This is needed because the hexstring representation of boost::multiprecision::cpp_int - # seems to behave differently accross different versions of boost (although the root - # cause has not been fully investigated). + # The following line makes sure hexstrings are lowercase in the + # protobuf file. This is needed because the hexstring representation + # of boost::multiprecision::cpp_int seems to behave differently + # across different versions of boost (although the root cause has + # not been fully investigated). "&& sed -i 's/0x[0-9A-F]\\+/\\L&/g' $(location %s)" % test_output_file, ]), ) diff --git a/p4_symbolic/ir/test.cc b/p4_symbolic/ir/test.cc index e44d2aa8..24dfb54d 100644 --- a/p4_symbolic/ir/test.cc +++ b/p4_symbolic/ir/test.cc @@ -54,8 +54,9 @@ absl::Status Test() { ASSIGN_OR_RETURN( p4::v1::ForwardingPipelineConfig config, p4_symbolic::ParseToForwardingPipelineConfig(bmv2_path, p4info_path)); - ASSIGN_OR_RETURN(std::vector table_entries, - p4_symbolic::ParseToPiTableEntries(entries_path)); + ASSIGN_OR_RETURN( + std::vector table_entries, + p4_symbolic::GetPiTableEntriesFromPiUpdatesProtoTextFile(entries_path)); ASSIGN_OR_RETURN(p4_symbolic::ir::Dataplane dataplane, p4_symbolic::ir::ParseToIr(config, table_entries)); diff --git a/p4_symbolic/main.cc b/p4_symbolic/main.cc index b8518097..d449908e 100644 --- a/p4_symbolic/main.cc +++ b/p4_symbolic/main.cc @@ -26,8 +26,10 @@ #include "absl/flags/usage.h" #include "absl/status/status.h" #include "absl/strings/str_format.h" +#include "glog/logging.h" #include "gutil/io.h" #include "p4/v1/p4runtime.pb.h" +#include "p4_pdpi/internal/ordered_map.h" #include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/test_util.h" @@ -38,17 +40,64 @@ ABSL_FLAG(std::string, entries, "", "The path to the table entries txt file (optional), leave this empty " "if the input p4 program contains no (explicit) tables for which " "entries are needed."); -ABSL_FLAG(std::string, smt, "", "Dump the SMT program for debugging"); +ABSL_FLAG(std::string, packets, "", "The concrete packets output file"); +ABSL_FLAG(std::string, smt, "", "The SMT program output file"); ABSL_FLAG(int, port_count, 2, "Number of used ports (numbered 0 to N-1)"); namespace { -// Parse input P4 program, analyze it symbolically -// and generate test pakcets. +// Finds a packet matching every table entry. +absl::StatusOr GetConcretePacketsCoveringAllTableEntries( + p4_symbolic::symbolic::SolverState &solver_state) { + constexpr int kColumnSize = 80; + std::ostringstream result; + + // Loop over tables in a deterministic order for output consistency + // (important for CI tests). + for (const auto &[name, table] : Ordered(solver_state.program.tables())) { + int row_count = 0; + if (solver_state.entries.count(name) > 0) { + row_count = static_cast(solver_state.entries.at(name).size()); + } + + for (int i = -1; i < row_count; i++) { + std::string banner = + "Finding packet for table " + name + " and row " + std::to_string(i); + result << std::string(kColumnSize, '=') << std::endl + << banner << std::endl + << std::string(kColumnSize, '=') << std::endl; + + p4_symbolic::symbolic::Assertion table_entry_assertion = + [name = name, + i](const p4_symbolic::symbolic::SymbolicContext &symbolic_context) { + const p4_symbolic::symbolic::SymbolicTableMatch &match = + symbolic_context.trace.matched_entries.at(name); + return (!symbolic_context.trace.dropped && match.matched && + match.entry_index == static_cast(i)); + }; + + ASSIGN_OR_RETURN( + std::optional concrete_packet, + p4_symbolic::symbolic::Solve(solver_state, table_entry_assertion)); + + if (concrete_packet) { + result << concrete_packet->to_string(/*verbose=*/true) << std::endl; + } else { + result << "Cannot find solution!" << std::endl; + } + result << std::string(kColumnSize, '_') << std::endl << std::endl; + } + } + + return result.str(); +} + +// Parses input P4 program, analyzes it symbolically and generates test packets. absl::Status ParseAndEvaluate() { const std::string &p4info_path = absl::GetFlag(FLAGS_p4info); const std::string &bmv2_path = absl::GetFlag(FLAGS_bmv2); const std::string &entries_path = absl::GetFlag(FLAGS_entries); + const std::string &packets_path = absl::GetFlag(FLAGS_packets); const std::string &smt_path = absl::GetFlag(FLAGS_smt); const int port_count = absl::GetFlag(FLAGS_port_count); @@ -58,8 +107,9 @@ absl::Status ParseAndEvaluate() { ASSIGN_OR_RETURN( p4::v1::ForwardingPipelineConfig config, p4_symbolic::ParseToForwardingPipelineConfig(bmv2_path, p4info_path)); - ASSIGN_OR_RETURN(std::vector table_entries, - p4_symbolic::ParseToPiTableEntries(entries_path)); + ASSIGN_OR_RETURN( + std::vector table_entries, + p4_symbolic::GetPiTableEntriesFromPiUpdatesProtoTextFile(entries_path)); // Generate port list. std::vector physical_ports(port_count); @@ -77,43 +127,14 @@ absl::Status ParseAndEvaluate() { solver_state->GetHeadersAndSolverConstraintsSMT(), smt_path)); } - // Find a packet matching every entry of every table. - // Loop over tables in a deterministic order for output consistency - // (important for ci tests). - auto ordered_tables = absl::btree_map( - solver_state->program.tables().cbegin(), - solver_state->program.tables().cend()); - constexpr int kColumnSize = 80; - - for (const auto &[name, table] : ordered_tables) { - int row_count = static_cast(solver_state->entries[name].size()); - for (int i = -1; i < row_count; i++) { - std::string banner = - "Finding packet for table " + name + " and row " + std::to_string(i); - std::cout << std::string(kColumnSize, '=') << std::endl - << banner << std::endl - << std::string(kColumnSize, '=') << std::endl; - - p4_symbolic::symbolic::Assertion table_entry_assertion = - [name = name, - i](const p4_symbolic::symbolic::SymbolicContext &symbolic_context) { - const p4_symbolic::symbolic::SymbolicTableMatch &match = - symbolic_context.trace.matched_entries.at(name); - return (!symbolic_context.trace.dropped && match.matched && - match.entry_index == static_cast(i)); - }; - - ASSIGN_OR_RETURN( - std::optional concrete_packet, - p4_symbolic::symbolic::Solve(*solver_state, table_entry_assertion)); - - if (concrete_packet) { - std::cout << concrete_packet->to_string(/*verbose=*/true) << std::endl; - } else { - std::cout << "Cannot find solution!" << std::endl; - } - std::cout << std::string(kColumnSize, '_') << std::endl << std::endl; - } + // Solve and output a concrete packet for each table entry. + if (packets_path.empty()) { + LOG(WARNING) << "No output path is provided for concrete packets. Consider " + "using --packets=path/to/packets.txt option."; + } else { + ASSIGN_OR_RETURN(std::string concrete_packets, + GetConcretePacketsCoveringAllTableEntries(*solver_state)); + RETURN_IF_ERROR(gutil::WriteFile(concrete_packets, packets_path)); } return absl::OkStatus(); @@ -126,10 +147,11 @@ int main(int argc, char *argv[]) { // GOOGLE_PROTOBUF_VERIFY_VERSION; // Command line arguments and help message. - absl::SetProgramUsageMessage( - absl::StrFormat("usage: %s %s", argv[0], - "--bmv2=path/to/bmv2.json --p4info=path/to/p4info.pb.txt " - "[--entries=path/to/table_entries.txt]")); + absl::SetProgramUsageMessage(absl::StrFormat( + "usage: %s %s", argv[0], + "--bmv2=path/to/bmv2.json --p4info=path/to/p4info.pb.txt " + "[--entries=path/to/table_entries.txt] [--packets=path/to/packets.txt] " + "[--smt=path/to/formulas.smt2] [--port_count=N]")); absl::ParseCommandLine(argc, argv); // Run code diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel index 0df696a4..0a9fb6d7 100644 --- a/p4_symbolic/symbolic/BUILD.bazel +++ b/p4_symbolic/symbolic/BUILD.bazel @@ -84,30 +84,30 @@ cc_library( # program generated by p4_symbolic/symbolic/symbolic.cc. end_to_end_test( name = "port_table_test", - output_golden_file = "expected/table.txt", p4_program = "//p4_symbolic/testdata:port-table/table.p4", + packets_golden_file = "expected/table.txt", smt_golden_file = "expected/table.smt2", table_entries = "//p4_symbolic/testdata:port-table/entries.pb.txt", ) end_to_end_test( name = "port_hardcoded_test", - output_golden_file = "expected/hardcoded.txt", p4_program = "//p4_symbolic/testdata:hardcoded/hardcoded.p4", + packets_golden_file = "expected/hardcoded.txt", smt_golden_file = "expected/hardcoded.smt2", ) end_to_end_test( name = "reflector_test", - output_golden_file = "expected/reflector.txt", p4_program = "//p4_symbolic/testdata:reflector/reflector.p4", + packets_golden_file = "expected/reflector.txt", smt_golden_file = "expected/reflector.smt2", ) end_to_end_test( name = "ipv4_routing_test", - output_golden_file = "expected/basic.txt", p4_program = "//p4_symbolic/testdata:ipv4-routing/basic.p4", + packets_golden_file = "expected/basic.txt", smt_golden_file = "expected/basic.smt2", table_entries = "//p4_symbolic/testdata:ipv4-routing/entries.pb.txt", ) @@ -118,16 +118,16 @@ end_to_end_test( # smaller SMT formulas, hence better constraint solving performance. end_to_end_test( name = "condtional_test", - output_golden_file = "expected/conditional.txt", p4_program = "//p4_symbolic/testdata:conditional/conditional.p4", + packets_golden_file = "expected/conditional.txt", smt_golden_file = "expected/conditional.smt2", table_entries = "//p4_symbolic/testdata:conditional/conditional_entries.pb.txt", ) end_to_end_test( name = "conditional_sequence_test", - output_golden_file = "expected/conditional_sequence.txt", p4_program = "//p4_symbolic/testdata:conditional/conditional_sequence.p4", + packets_golden_file = "expected/conditional_sequence.txt", smt_golden_file = "expected/conditional_sequence.smt2", table_entries = "//p4_symbolic/testdata:conditional/conditional_sequence_entries.pb.txt", ) diff --git a/p4_symbolic/symbolic/test.bzl b/p4_symbolic/symbolic/test.bzl index 5be09d31..25a2375a 100644 --- a/p4_symbolic/symbolic/test.bzl +++ b/p4_symbolic/symbolic/test.bzl @@ -28,7 +28,7 @@ load("//p4_pdpi/testing:diff_test.bzl", "diff_test") def end_to_end_test( name, p4_program, - output_golden_file, + packets_golden_file, smt_golden_file, table_entries = None, port_count = 2, @@ -55,7 +55,7 @@ def end_to_end_test( Args: name: Test name. p4_program: Input P4 program. - output_golden_file: File containing the expected output. + packets_golden_file: File containing the expected concrete packets. smt_golden_file: File containing the expected SMT formulae. table_entries: File containing the table entries as input in protobuf text. port_count: Number of ports. @@ -63,12 +63,11 @@ def end_to_end_test( """ p4c_name = "%s_p4c" % name p4info_file = "%s_bazel-p4c-tmp-output/p4info.pb.txt" % p4c_name - output_test_name = "%s_output" % name + packets_test_name = "%s_packets" % name smt_test_name = "%s_smt" % name bmv2_file = "tmp/%s.bmv2.json" % name p4info_file = "tmp/%s.p4info.pb.txt" % name - test_output_file = "tmp/%s_output" % name # Run p4c to get bmv2 JSON and p4info.pb.txt files. tmp_bmv2_file = "%s.tmp" % bmv2_file @@ -91,7 +90,7 @@ def end_to_end_test( # Use p4_symbolic/main.cc to run our tool on the p4 program # and produce a debugging smt file and an output file with # interesting testing packets. - test_output_file = "generated/%s.txt" % name + packets_output_file = "generated/%s.txt" % name smt_output_file = "generated/%s.smt2" % name native.genrule( name = "%s_test_runner" % name, @@ -99,26 +98,24 @@ def end_to_end_test( bmv2_file, p4info_file, ] + ([table_entries] if table_entries else []), - outs = [test_output_file, smt_output_file], + outs = [packets_output_file, smt_output_file], tools = ["//p4_symbolic:main"], cmd = " ".join([ "$(location //p4_symbolic:main)", ("--bmv2=$(location %s)" % bmv2_file), ("--p4info=$(location %s)" % p4info_file), ("--entries=$(location %s)" % table_entries if table_entries else ""), + ("--packets=$(location %s)" % packets_output_file), ("--smt=$(location %s)" % smt_output_file), ("--port_count=%d" % port_count), - # Use `tee` to simultaneously capture output in file yet still print it to stdout, to - # ease debugging. - ("| tee $(location %s)" % test_output_file), ]), ) # Exact diff test for the packet output file. diff_test( - name = output_test_name, - actual = test_output_file, - expected = output_golden_file, + name = packets_test_name, + actual = packets_output_file, + expected = packets_golden_file, ) # Group tests into a test_suite with the given name. @@ -126,6 +123,6 @@ def end_to_end_test( native.test_suite( name = name, tests = [ - (":%s" % output_test_name), + (":%s" % packets_test_name), ], ) diff --git a/p4_symbolic/test_util.cc b/p4_symbolic/test_util.cc index 4239689d..eb118d18 100644 --- a/p4_symbolic/test_util.cc +++ b/p4_symbolic/test_util.cc @@ -1,5 +1,11 @@ #include "p4_symbolic/test_util.h" +#include +#include + +#include "absl/status/statusor.h" +#include "absl/strings/str_cat.h" +#include "absl/strings/string_view.h" #include "gutil/io.h" #include "gutil/proto.h" #include "p4/config/v1/p4info.pb.h" @@ -7,35 +13,12 @@ namespace p4_symbolic { -absl::StatusOr -ParseToForwardingPipelineConfig(const std::string &bmv2_json_path, - const std::string &p4info_path) { - // Read BMv2 json file into a string. - ASSIGN_OR_RETURN(std::string bmv2_json, gutil::ReadFile(bmv2_json_path)); - - // Parse p4info file into protobuf. - p4::config::v1::P4Info p4info; - RETURN_IF_ERROR(gutil::ReadProtoFromFile(p4info_path, &p4info)); - - p4::v1::ForwardingPipelineConfig config; - *config.mutable_p4_device_config() = std::move(bmv2_json); - *config.mutable_p4info() = std::move(p4info); - return config; -} - -absl::StatusOr> ParseToPiTableEntries( - const std::string &table_entries_path) { - // Parse table entries. - p4::v1::WriteRequest write_request; - if (!table_entries_path.empty()) { - RETURN_IF_ERROR( - gutil::ReadProtoFromFile(table_entries_path, &write_request)) - .SetPrepend() - << "While trying to parse table entry file '" << table_entries_path - << "': "; - } +namespace { +absl::StatusOr> +ParseWriteRequestToPiTableEntries(const p4::v1::WriteRequest &write_request) { std::vector table_entries; + for (const auto &update : write_request.updates()) { // Make sure update is of type insert. if (update.type() != p4::v1::Update::INSERT) { @@ -57,4 +40,37 @@ absl::StatusOr> ParseToPiTableEntries( return table_entries; } +} // namespace + +absl::StatusOr +ParseToForwardingPipelineConfig(absl::string_view bmv2_json_path, + absl::string_view p4info_path) { + // Read BMv2 json file into a string. + ASSIGN_OR_RETURN(std::string bmv2_json, + gutil::ReadFile(std::string(bmv2_json_path))); + + // Parse p4info file into protobuf. + p4::config::v1::P4Info p4info; + RETURN_IF_ERROR(gutil::ReadProtoFromFile(p4info_path, &p4info)); + + p4::v1::ForwardingPipelineConfig config; + *config.mutable_p4_device_config() = std::move(bmv2_json); + *config.mutable_p4info() = std::move(p4info); + return config; +} + +absl::StatusOr> +GetPiTableEntriesFromPiUpdatesProtoTextFile( + absl::string_view table_entries_path) { + p4::v1::WriteRequest write_request; + if (!table_entries_path.empty()) { + RETURN_IF_ERROR( + gutil::ReadProtoFromFile(table_entries_path, &write_request)) + .SetPrepend() + << "While trying to parse table entry file '" << table_entries_path + << "': "; + } + return ParseWriteRequestToPiTableEntries(write_request); +} + } // namespace p4_symbolic diff --git a/p4_symbolic/test_util.h b/p4_symbolic/test_util.h index e940b17b..69cab0ed 100644 --- a/p4_symbolic/test_util.h +++ b/p4_symbolic/test_util.h @@ -1,20 +1,21 @@ #ifndef PINS_P4_SYMBOLIC_TEST_UTIL_H_ #define PINS_P4_SYMBOLIC_TEST_UTIL_H_ -#include #include #include "absl/status/statusor.h" +#include "absl/strings/string_view.h" #include "p4/v1/p4runtime.pb.h" namespace p4_symbolic { absl::StatusOr -ParseToForwardingPipelineConfig(const std::string &bmv2_json_path, - const std::string &p4info_path); +ParseToForwardingPipelineConfig(absl::string_view bmv2_json_path, + absl::string_view p4info_path); -absl::StatusOr> ParseToPiTableEntries( - const std::string &table_entries_path); +absl::StatusOr> +GetPiTableEntriesFromPiUpdatesProtoTextFile( + absl::string_view table_entries_path); } // namespace p4_symbolic From 357a8e1541c60da1e701a320dfd544c4347b4542 Mon Sep 17 00:00:00 2001 From: kishanps Date: Tue, 25 Jul 2023 11:52:35 -0700 Subject: [PATCH 6/7] [Comb] Rename PD->IR/PI to set up for deprecation. --- p4_symbolic/sai/criteria_generator_test.cc | 3 +- p4_symbolic/sai/packet_synthesizer_test.cc | 303 +++++++++++++++++++++ p4_symbolic/sai/sai_test.cc | 5 +- p4_symbolic/tests/BUILD.bazel | 1 + 4 files changed, 309 insertions(+), 3 deletions(-) create mode 100644 p4_symbolic/sai/packet_synthesizer_test.cc diff --git a/p4_symbolic/sai/criteria_generator_test.cc b/p4_symbolic/sai/criteria_generator_test.cc index de30b3f5..1cea6881 100644 --- a/p4_symbolic/sai/criteria_generator_test.cc +++ b/p4_symbolic/sai/criteria_generator_test.cc @@ -68,7 +68,8 @@ PacketSynthesisParams GetParams( ->mutable_match() ->mutable_in_port() ->set_value(*in_port_match); - const auto pi_entry = pdpi::PdTableEntryToPi(ir_p4info, pd_entry); + const auto pi_entry = + pdpi::PartialPdTableEntryToPiTableEntry(ir_p4info, pd_entry); CHECK_OK(pi_entry.status()); *params.mutable_pi_entries()->Add() = *pi_entry; diff --git a/p4_symbolic/sai/packet_synthesizer_test.cc b/p4_symbolic/sai/packet_synthesizer_test.cc new file mode 100644 index 00000000..86d66769 --- /dev/null +++ b/p4_symbolic/sai/packet_synthesizer_test.cc @@ -0,0 +1,303 @@ +// 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 "absl/strings/match.h" +#include "absl/strings/str_cat.h" +#include "gmock/gmock.h" +#include "gtest/gtest.h" +#include "gutil/status_matchers.h" +#include "gutil/testing.h" +#include "p4_pdpi/packetlib/packetlib.h" +#include "p4_pdpi/packetlib/packetlib.pb.h" +#include "p4_pdpi/pd.h" +#include "p4_symbolic/packet_synthesizer/packet_synthesizer.pb.h" +#include "p4_symbolic/sai/sai.h" +#include "sai_p4/instantiations/google/instantiations.h" +#include "sai_p4/instantiations/google/sai_nonstandard_platforms.h" +#include "sai_p4/instantiations/google/sai_p4info.h" +#include "sai_p4/instantiations/google/sai_pd.pb.h" + +namespace p4_symbolic::packet_synthesizer { +namespace { + +// Returns packet synthesis parameters with the pipeline config for FBR and a +// simple table entry. +// If `in_port_match` is not null, the added entry matches on the provided +// ingress port. +PacketSynthesisParams GetParams( + std::optional in_port_match = std::nullopt) { + const sai::Instantiation instantiation = + sai::Instantiation::kFabricBorderRouter; + const pdpi::IrP4Info ir_p4info = sai::GetIrP4Info(instantiation); + const p4::v1::ForwardingPipelineConfig pipeline_config = + sai::GetNonstandardForwardingPipelineConfig( + instantiation, sai::NonstandardPlatform::kP4Symbolic); + + PacketSynthesisParams params; + *params.mutable_pipeline_config() = pipeline_config; + auto pd_entry = gutil::ParseProtoOrDie(R"pb( + acl_pre_ingress_table_entry { + match {} + action { set_vrf { vrf_id: "vrf-80" } } + priority: 1 + })pb"); + if (in_port_match.has_value()) + pd_entry.mutable_acl_pre_ingress_table_entry() + ->mutable_match() + ->mutable_in_port() + ->set_value(*in_port_match); + const auto pi_entry = + pdpi::PartialPdTableEntryToPiTableEntry(ir_p4info, pd_entry); + + CHECK_OK(pi_entry.status()); + *params.mutable_pi_entries()->Add() = *pi_entry; + + return params; +} + +TEST(PacketSynthesizerTest, SynthesizePacketSatisfiableCriteriaYieldsAPacket) { + // Get a packet synthesizer object. + ASSERT_OK_AND_ASSIGN(auto synthesizer, + PacketSynthesizer::Create(GetParams())); + + // Synthesize Packet. + ASSERT_OK_AND_ASSIGN( + const PacketSynthesisResult result, + synthesizer->SynthesizePacket( + gutil::ParseProtoOrDie( + R"pb( + output_criteria { drop_expected: True } + table_reachability_criteria { + table_name: "ingress.acl_pre_ingress.acl_pre_ingress_table" + } + table_entry_reachability_criteria { + table_name: "ingress.acl_pre_ingress.acl_pre_ingress_table" + match_index: 0 + } + )pb"))); + + // Check the synthesized packet. + ASSERT_TRUE(result.has_synthesized_packet()); +} + +TEST(PacketSynthesizerTest, + SynthesizePacketWithUnsatisfiableCriteriaDoesNotYieldAPacket) { + // Get a packet synthesizer object. + ASSERT_OK_AND_ASSIGN(auto synthesizer, + PacketSynthesizer::Create(GetParams())); + + // Synthesize Packet. + ASSERT_OK_AND_ASSIGN( + const PacketSynthesisResult result, + synthesizer->SynthesizePacket( + gutil::ParseProtoOrDie( + R"pb( + table_reachability_criteria { + table_name: "ingress.acl_pre_ingress.acl_pre_ingress_table" + } + table_entry_reachability_criteria { + table_name: "ingress.acl_pre_ingress.acl_pre_ingress_table" + match_index: -1 + } + )pb"))); + + // Check the synthesized packet. + ASSERT_FALSE(result.has_synthesized_packet()); +} + +TEST(PacketSynthesizerTest, + SynthesizePacketWithIpv4ValidCriteriaYieldsIpv4Packet) { + // Get a packet synthesizer object. + ASSERT_OK_AND_ASSIGN(auto synthesizer, + PacketSynthesizer::Create(GetParams())); + + // Synthesize Packet. + ASSERT_OK_AND_ASSIGN(const PacketSynthesisResult result, + synthesizer->SynthesizePacket( + gutil::ParseProtoOrDie( + R"pb( + output_criteria { drop_expected: True } + input_packet_header_criteria { + field_criteria { + field_match { + name: "ipv4.$valid$" + exact { hex_str: "0x1" } + } + } + # No VLAN header + field_criteria { + field_match { + name: "vlan.$valid$" + exact { hex_str: "0x0" } + } + } + } + )pb"))); + + // Check the synthesized packet. + ASSERT_TRUE(result.has_synthesized_packet()); + const auto& synthesized_packet = result.synthesized_packet(); + LOG(INFO) << synthesized_packet.DebugString(); + ASSERT_TRUE(packetlib::ParsePacket(synthesized_packet.packet()) + .headers(1) + .has_ipv4_header()); +} + +TEST(PacketSynthesizerTest, + SynthesizePacketWithIpv4DstAddrCriteriaYieldsProperPacket) { + // Get a packet synthesizer object. + ASSERT_OK_AND_ASSIGN(auto synthesizer, + PacketSynthesizer::Create(GetParams())); + + // Synthesize Packet. + ASSERT_OK_AND_ASSIGN(const PacketSynthesisResult result, + synthesizer->SynthesizePacket( + gutil::ParseProtoOrDie( + R"pb( + output_criteria { drop_expected: True } + input_packet_header_criteria { + field_criteria { + field_match { + name: "ipv4.$valid$" + exact { hex_str: "0x1" } + } + } + field_criteria { + field_match { + name: "ipv4.dst_addr" + lpm { + value { ipv4: "10.0.0.0" } + prefix_length: 8 + } + } + } + # No VLAN header + field_criteria { + field_match { + name: "vlan.$valid$" + exact { hex_str: "0x0" } + } + } + } + )pb"))); + + // Check the synthesized packet. + ASSERT_TRUE(result.has_synthesized_packet()); + const auto& synthesized_packet = result.synthesized_packet(); + LOG(INFO) << synthesized_packet.DebugString(); + packetlib::Packet packet = + packetlib::ParsePacket(synthesized_packet.packet()); + const auto& second_header = packet.headers(1); + ASSERT_TRUE(second_header.has_ipv4_header()); + ASSERT_TRUE( + absl::StartsWith(second_header.ipv4_header().ipv4_destination(), "10.")); +} + +TEST(PacketSynthesizerTest, + SynthesizePacketWithTernaryIpv4DstAddrCriteriaYieldsProperPacket) { + // Get a packet synthesizer object. + ASSERT_OK_AND_ASSIGN(auto synthesizer, + PacketSynthesizer::Create(GetParams())); + + // Synthesize Packet. + ASSERT_OK_AND_ASSIGN(const PacketSynthesisResult result, + synthesizer->SynthesizePacket( + gutil::ParseProtoOrDie( + R"pb( + output_criteria { drop_expected: True } + input_packet_header_criteria { + field_criteria { + field_match { + name: "ipv4.$valid$" + exact { hex_str: "0x1" } + } + } + field_criteria { + field_match { + name: "ipv4.dst_addr" + ternary { + value { ipv4: "10.0.0.0" } + mask { ipv4: "255.0.0.0" } + } + } + } + # No VLAN header + field_criteria { + field_match { + name: "vlan.$valid$" + exact { hex_str: "0x0" } + } + } + } + )pb"))); + + // Check the synthesized packet. + ASSERT_TRUE(result.has_synthesized_packet()); + const auto& synthesized_packet = result.synthesized_packet(); + LOG(INFO) << synthesized_packet.DebugString(); + packetlib::Packet packet = + packetlib::ParsePacket(synthesized_packet.packet()); + const auto& second_header = packet.headers(1); + ASSERT_TRUE(second_header.has_ipv4_header()); + ASSERT_TRUE( + absl::StartsWith(second_header.ipv4_header().ipv4_destination(), "10.")); +} + +TEST(PacketSynthesizerTest, + SynthesizePacketWithIngressPortCriteriaYieldsProperPacket) { + constexpr int kPortCount = 10; + + // Get basic parameters to create packet synthesizer object. + // TODO: If no entry matches on ingress port, P4-Symbolic misses + // that local_metadata.ingress_port is p4runtime_translated. In such cases, + // the synthesizer will return empty string ("") as the ingress port. Here we + // add a match on in_port to prevent such a scenario. + PacketSynthesisParams params = GetParams(/*in_port_match=*/"7"); + + // Prepare v1model ports and P4RT <-> v1model port translation. + TranslationData& port_translation = + (*params.mutable_translation_per_type())[p4_symbolic::kPortIdTypeName]; + for (int port = 1; port <= kPortCount; port++) { + params.add_physical_port(port); + TranslationData::StaticMapping& static_mapping = + *port_translation.add_static_mapping(); + static_mapping.set_string_value(absl::StrCat(port)); + static_mapping.set_integer_value(port); + } + + // Get a packet synthesizer object. + ASSERT_OK_AND_ASSIGN(auto synthesizer, PacketSynthesizer::Create(params)); + + // Synthesize Packet. + ASSERT_OK_AND_ASSIGN(const PacketSynthesisResult result, + synthesizer->SynthesizePacket( + gutil::ParseProtoOrDie( + R"pb( + output_criteria { drop_expected: True } + ingress_port_criteria { v1model_port: 5 } + )pb"))); + + // Check the synthesized packet's port. + ASSERT_TRUE(result.has_synthesized_packet()); + const auto& synthesized_packet = result.synthesized_packet(); + LOG(INFO) << synthesized_packet.DebugString(); + ASSERT_EQ(synthesized_packet.ingress_port(), "5"); +} + +} // namespace +} // namespace p4_symbolic::packet_synthesizer diff --git a/p4_symbolic/sai/sai_test.cc b/p4_symbolic/sai/sai_test.cc index 60f19d74..aa513d3b 100644 --- a/p4_symbolic/sai/sai_test.cc +++ b/p4_symbolic/sai/sai_test.cc @@ -101,8 +101,9 @@ TEST(GetLocalMetadataIngressPortFromModel, IngressPortIsAmongPassedValues) { })pb"); std::vector pi_entries; for (auto& pd_entry : pd_entries.entries()) { - ASSERT_OK_AND_ASSIGN(pi_entries.emplace_back(), - pdpi::PartialPdTableEntryToPiTableEntry(ir_p4info, pd_entry)); + ASSERT_OK_AND_ASSIGN( + pi_entries.emplace_back(), + pdpi::PartialPdTableEntryToPiTableEntry(ir_p4info, pd_entry)); } symbolic::TranslationPerType translations; translations[kPortIdTypeName] = symbolic::values::TranslationData{ diff --git a/p4_symbolic/tests/BUILD.bazel b/p4_symbolic/tests/BUILD.bazel index c4190359..d83c2c24 100644 --- a/p4_symbolic/tests/BUILD.bazel +++ b/p4_symbolic/tests/BUILD.bazel @@ -14,6 +14,7 @@ cc_test( "//p4_pdpi:ir_cc_proto", "//p4_pdpi:pd", "//p4_symbolic:z3_util", + "//p4_symbolic/sai", "//p4_symbolic/symbolic", "//sai_p4/instantiations/google:sai_nonstandard_platforms_cc", "//sai_p4/instantiations/google:sai_pd_cc_proto", From e08722fd8df130c9b6db0a2ee4e83a0c6503642f Mon Sep 17 00:00:00 2001 From: kishanps Date: Wed, 26 Jul 2023 21:12:16 -0700 Subject: [PATCH 7/7] [P4-Symbolic] Move symbolic/concrete context to context.{cc,h} separated from symbolic.{cc,h}, and make the context-related objects constructed along with the solver state and then passed along the symbolic evaluation. --- p4_symbolic/sai/sai.cc | 1 - p4_symbolic/symbolic/BUILD.bazel | 2 + p4_symbolic/symbolic/action.h | 2 +- p4_symbolic/symbolic/conditional.h | 2 +- p4_symbolic/symbolic/context.cc | 69 ++++++++++++ p4_symbolic/symbolic/context.h | 129 +++++++++++++++++++++++ p4_symbolic/symbolic/control.cc | 2 +- p4_symbolic/symbolic/control.h | 2 +- p4_symbolic/symbolic/guarded_map.h | 44 ++++---- p4_symbolic/symbolic/symbolic.cc | 37 +++---- p4_symbolic/symbolic/symbolic.h | 158 ++-------------------------- p4_symbolic/symbolic/table.cc | 1 - p4_symbolic/symbolic/table.h | 2 +- p4_symbolic/symbolic/v1model.cc | 82 +++++++-------- p4_symbolic/symbolic/v1model.h | 10 +- p4_symbolic/symbolic/values.h | 5 +- p4_symbolic/symbolic/values_test.cc | 20 ++-- 17 files changed, 308 insertions(+), 260 deletions(-) create mode 100644 p4_symbolic/symbolic/context.cc create mode 100644 p4_symbolic/symbolic/context.h diff --git a/p4_symbolic/sai/sai.cc b/p4_symbolic/sai/sai.cc index 44951248..85a410b2 100644 --- a/p4_symbolic/sai/sai.cc +++ b/p4_symbolic/sai/sai.cc @@ -14,7 +14,6 @@ #include "p4_symbolic/sai/sai.h" -#include #include #include #include diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel index 0a9fb6d7..30ed2f47 100644 --- a/p4_symbolic/symbolic/BUILD.bazel +++ b/p4_symbolic/symbolic/BUILD.bazel @@ -24,6 +24,7 @@ cc_library( srcs = [ "action.cc", "conditional.cc", + "context.cc", "control.cc", "guarded_map.cc", "operators.cc", @@ -37,6 +38,7 @@ cc_library( hdrs = [ "action.h", "conditional.h", + "context.h", "control.h", "guarded_map.h", "operators.h", diff --git a/p4_symbolic/symbolic/action.h b/p4_symbolic/symbolic/action.h index d7022a6f..64da0027 100644 --- a/p4_symbolic/symbolic/action.h +++ b/p4_symbolic/symbolic/action.h @@ -25,7 +25,7 @@ #include "google/protobuf/repeated_ptr_field.h" #include "p4_pdpi/ir.pb.h" #include "p4_symbolic/ir/ir.pb.h" -#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/values.h" #include "z3++.h" diff --git a/p4_symbolic/symbolic/conditional.h b/p4_symbolic/symbolic/conditional.h index af461187..c9b9febf 100644 --- a/p4_symbolic/symbolic/conditional.h +++ b/p4_symbolic/symbolic/conditional.h @@ -20,7 +20,7 @@ #include "p4_symbolic/ir/ir.h" #include "p4_symbolic/ir/ir.pb.h" -#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/values.h" #include "z3++.h" diff --git a/p4_symbolic/symbolic/context.cc b/p4_symbolic/symbolic/context.cc new file mode 100644 index 00000000..0459a1e4 --- /dev/null +++ b/p4_symbolic/symbolic/context.cc @@ -0,0 +1,69 @@ +// 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/symbolic/context.h" + +#include + +#include "absl/strings/str_cat.h" + +namespace p4_symbolic { +namespace symbolic { + +std::string ConcreteTableMatch::to_string() const { + if (!matched) { + return "was not matched!"; + } + return absl::StrCat("was matched on entry ", entry_index); +} + +std::string ConcreteTrace::to_string() const { + std::string result; + absl::StrAppend(&result, "dropped = ", dropped, "\n"); + absl::StrAppend(&result, "got cloned = ", got_cloned); + for (const auto &[table, match] : matched_entries) { + absl::StrAppend(&result, "\n", table, " => ", match.to_string()); + } + return result; +} + +std::string ConcreteContext::to_string() const { + return to_string(/*verbose=*/false); +} + +std::string ConcreteContext::to_string(bool verbose) const { + auto result = absl::StrCat("ingress_port = ", ingress_port, "\n", + "egress_port = ", egress_port, "\n", "trace:\n", + trace.to_string()); + if (verbose) { + auto ingress_string = absl::StrCat("ingress_headers", ":"); + auto parsed_string = absl::StrCat("parsed_headers", ":"); + auto egress_string = absl::StrCat("egress_headers", ":"); + for (const auto &[name, ingress_value] : ingress_headers) { + absl::StrAppend(&ingress_string, "\n", name, " = ", ingress_value); + } + for (const auto &[name, parsed_value] : parsed_headers) { + absl::StrAppend(&parsed_string, "\n", name, " = ", parsed_value); + } + for (const auto &[name, egress_value] : egress_headers) { + absl::StrAppend(&egress_string, "\n", name, " = ", egress_value); + } + absl::StrAppend(&result, "\n\n", ingress_string, "\n\n", parsed_string, + "\n\n", egress_string); + } + return result; +} + +} // namespace symbolic +} // namespace p4_symbolic diff --git a/p4_symbolic/symbolic/context.h b/p4_symbolic/symbolic/context.h new file mode 100644 index 00000000..4ec76c96 --- /dev/null +++ b/p4_symbolic/symbolic/context.h @@ -0,0 +1,129 @@ +// 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_SYMBOLIC_CONTEXT_H_ +#define PINS_P4_SYMBOLIC_SYMBOLIC_CONTEXT_H_ + +#include + +#include "absl/container/btree_map.h" +#include "p4_symbolic/symbolic/guarded_map.h" +#include "p4_symbolic/z3_util.h" +#include "z3++.h" + +namespace p4_symbolic { +namespace symbolic { + +// Maps the name of a header field in the p4 program to its concrete value. +using ConcretePerPacketState = absl::btree_map; + +// The symbolic counterpart of ConcretePerPacketState. +// Maps the name of a header field in the p4 program to its symbolic value. +// This can be used to constrain p4 program fields inside assertions. +// This is automatically constructed from the header type definitions +// the p4 program has. +// Assume the p4 program has a header instance named "standard_metadata" of type +// "standard_metadata_t", which has field "ingress_port" of type "bit<9>" in it. +// Then, we will have: +// SymbolicMetadata["standard_metadata.ingress_port"] = +// +// An instance of this type is passed around and mutated by the functions +// responsible for symbolically evaluating the program. +using SymbolicPerPacketState = SymbolicGuardedMap; + +// Expresses a concrete match for a corresponding concrete packet with a +// table in the program. +struct ConcreteTableMatch { + bool matched; // false if no entry in this table was matched, true otherwise. + // If matched is false, this is set to -1. + // If matched is true, this is the index of the matched table entry, or -1 if + // the default entry was matched. + int entry_index; + std::string to_string() const; +}; + +// Exposes a symbolic handle for a match between the symbolic packet and +// a symbolic table. +// This allows encoding of constraints on which (if any) entries are matched, +// and the value of the match. +// e.g. for some table "": +// (.entry_index == i) iff +// [][i] was matched/hit. +struct SymbolicTableMatch { + z3::expr matched; + z3::expr entry_index; +}; + +// `SymbolicTableMatch`es by table name. +using SymbolicTableMatches = absl::btree_map; + +// Specifies the expected trace in the program that the corresponding +// concrete packet is expected to take. +struct ConcreteTrace { + absl::btree_map matched_entries; + // Can be extended more in the future to include useful + // flags about dropping the packet, taking specific code (e.g. if) + // branches, vrf, other interesting events, etc. + bool dropped; // true if the packet was dropped. + bool got_cloned; // true if the packet got cloned. + std::string to_string() const; +}; + +// Provides symbolic handles for the trace the symbolic packet is constrained +// to take in the program. +struct SymbolicTrace { + SymbolicTrace() : dropped(Z3Context()), got_cloned(Z3Context()) {} + + // Full table name to its symbolic match. + // TODO: Rename to matches_by_table_name. + SymbolicTableMatches matched_entries; + z3::expr dropped; + z3::expr got_cloned; +}; + +// The result of solving with some assertion. +// This contains an input test packet with its predicted flow in the program, +// and the predicted output. +struct ConcreteContext { + std::string ingress_port; + std::string egress_port; + ConcretePerPacketState ingress_headers; + ConcretePerPacketState parsed_headers; + ConcretePerPacketState egress_headers; + ConcreteTrace trace; // Expected trace in the program. + + std::string to_string() const; + std::string to_string(bool verbose) const; +}; + +// The symbolic context within our analysis. +// Exposes symbolic handles for the fields of the input packet, +// and its trace in the program. +// Assertions are defined on a symbolic context. +class SymbolicContext { + public: + SymbolicContext() : ingress_port(Z3Context()), egress_port(Z3Context()) {} + + z3::expr ingress_port; + z3::expr egress_port; + SymbolicPerPacketState ingress_headers; + SymbolicPerPacketState parsed_headers; + SymbolicPerPacketState egress_headers; + SymbolicTrace trace; +}; + +} // namespace symbolic +} // namespace p4_symbolic + +#endif // PINS_P4_SYMBOLIC_SYMBOLIC_CONTEXT_H_ diff --git a/p4_symbolic/symbolic/control.cc b/p4_symbolic/symbolic/control.cc index e60deeb0..4a5c0ba0 100644 --- a/p4_symbolic/symbolic/control.cc +++ b/p4_symbolic/symbolic/control.cc @@ -28,7 +28,7 @@ #include "p4_symbolic/ir/ir.h" #include "p4_symbolic/ir/ir.pb.h" #include "p4_symbolic/symbolic/conditional.h" -#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/table.h" namespace p4_symbolic::symbolic::control { diff --git a/p4_symbolic/symbolic/control.h b/p4_symbolic/symbolic/control.h index 71c7e158..8fe5b974 100644 --- a/p4_symbolic/symbolic/control.h +++ b/p4_symbolic/symbolic/control.h @@ -60,7 +60,7 @@ #include #include "p4_symbolic/ir/ir.h" -#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/values.h" #include "z3++.h" diff --git a/p4_symbolic/symbolic/guarded_map.h b/p4_symbolic/symbolic/guarded_map.h index 5a1d5183..0ec28dcc 100644 --- a/p4_symbolic/symbolic/guarded_map.h +++ b/p4_symbolic/symbolic/guarded_map.h @@ -22,7 +22,6 @@ #include "absl/container/btree_map.h" #include "absl/status/status.h" #include "google/protobuf/map.h" -#include "gutil/status.h" #include "p4_symbolic/ir/ir.pb.h" #include "z3++.h" @@ -31,17 +30,22 @@ namespace symbolic { // This class wraps around an internal absl::btree_map instance, // while enforcing the following: -// 1. This class can only be instantiated with an instance of the IR -// header definitions. The resulting instance will be initialized -// to have exactly the same keys as the fields defined in those header -// definitions. These keys are initially mapped to free symbolic variables, -// with the same sort (including bitsize) described in the definitions. -// 2. This class supports a const reference .Get(), which returns -// an absl error if the key is not found in the map. -// 3. This class allows mutation via .Set(, , ), which -// sets the value of the key to z3::ite(, , ), -// after checking that the sort of matches the sort of -// modulo padding. +// 1. When instantiated with an instance of the IR header definitions. The +// resulting instance will be initialized to have exactly the same keys as +// the fields defined in those header definitions. These keys are initially +// mapped to free symbolic variables, with the same sort (including bitsize) +// described in the definitions. +// 2. This class supports const references .Get() and .Get(, +// ), which returns an absl error if the key is not found in the +// map. +// 3. This class allows mutation via .Set(, , ) and +// .Set(, , , ), which set the value +// of the key to z3::ite(, , ), after checking that +// the sort of matches the sort of modulo padding. +// 4. Special mutation methods are supported via .UnguardedSet(, ) +// and .UnguardedSet(, , ), which +// unconditionally overwrite the old values in the map and are mainly used +// for initializing certain architecture- or target-specific values. // // As such, this class provides the following safety properties: // 1. Once initialized, the class has a fixed set of keys. @@ -49,19 +53,17 @@ namespace symbolic { // 3. A value can only be assigned to a key given a guard. // class SymbolicGuardedMap { -public: - // Constructor requires passing the headers definition and will fill the map - // with a free symbolic variable per header field. + public: + // By passing the headers definition, the constructor will fill the map with a + // free symbolic variable per header field. static absl::StatusOr CreateSymbolicGuardedMap( const google::protobuf::Map &headers); - // Explicitly copyable and movable! + SymbolicGuardedMap() = default; SymbolicGuardedMap(const SymbolicGuardedMap &other) = default; SymbolicGuardedMap(SymbolicGuardedMap &&other) = default; - - // Not assignable. - SymbolicGuardedMap &operator=(const SymbolicGuardedMap &other) = delete; - SymbolicGuardedMap &operator=(SymbolicGuardedMap &&other) = delete; + SymbolicGuardedMap &operator=(const SymbolicGuardedMap &other) = default; + SymbolicGuardedMap &operator=(SymbolicGuardedMap &&other) = default; // Getters. bool ContainsKey(absl::string_view key) const; @@ -96,7 +98,7 @@ class SymbolicGuardedMap { // Private constructor used by factory. explicit SymbolicGuardedMap(absl::btree_map map) - : map_(map) {} + : map_(std::move(map)) {} }; } // namespace symbolic diff --git a/p4_symbolic/symbolic/symbolic.cc b/p4_symbolic/symbolic/symbolic.cc index 147dfacf..75815607 100644 --- a/p4_symbolic/symbolic/symbolic.cc +++ b/p4_symbolic/symbolic/symbolic.cc @@ -33,12 +33,12 @@ namespace p4_symbolic { namespace symbolic { -std::string SolverState::GetSolverSMT() const { +std::string SolverState::GetSolverSMT() { if (!solver) return ""; return solver->to_smt2(); } -std::string SolverState::GetHeadersAndSolverConstraintsSMT() const { +std::string SolverState::GetHeadersAndSolverConstraintsSMT() { std::ostringstream result; for (const auto &[field_name, expression] : context.ingress_headers) { result << "(ingress) " << field_name << ": " << expression << std::endl; @@ -67,23 +67,20 @@ absl::StatusOr> EvaluateP4Program( // Parse the P4 config and entries into the P4-symbolic IR. ASSIGN_OR_RETURN(ir::Dataplane dataplane, ir::ParseToIr(config, entries)); - // Use global context to define a solver. - std::unique_ptr z3_solver = - std::make_unique(Z3Context()); + auto solver_state = + std::make_unique(dataplane.program, dataplane.entries); + SymbolicContext &context = solver_state->context; + values::P4RuntimeTranslator &translator = solver_state->translator; - // Initially, the p4runtime translator has empty state. - values::P4RuntimeTranslator translator; - - // Initiate the p4runtime translator with statically translated types. + // Initialize the p4runtime translator with statically translated types. for (const auto &[type, translation] : translation_per_type) { translator.p4runtime_translation_allocators.emplace( type, values::IdAllocator(translation)); } // Evaluate the main program, assuming it conforms to V1 model. - ASSIGN_OR_RETURN( - SymbolicContext context, - v1model::EvaluateV1model(dataplane, physical_ports, translator)); + RETURN_IF_ERROR( + v1model::EvaluateV1model(dataplane, physical_ports, context, translator)); // Restrict the value of all fields with (purely static, i.e. // dynamic_translation = false) P4RT translated types to what has been used in @@ -99,15 +96,15 @@ absl::StatusOr> EvaluateP4Program( constraint = constraint || (field_expr == static_cast(numeric_value)); } - z3_solver->add(constraint); + solver_state->solver->add(constraint); } } // Restrict ports to the available physical ports. // TODO: Support generating packet-out packets from the CPU port. if (physical_ports.empty()) { - z3_solver->add(context.ingress_port != kCpuPort); - z3_solver->add(context.ingress_port != kDropPort); + solver_state->solver->add(context.ingress_port != kCpuPort); + solver_state->solver->add(context.ingress_port != kDropPort); } else { z3::expr ingress_port_is_physical = Z3Context().bool_val(false); z3::expr egress_port_is_physical = Z3Context().bool_val(false); @@ -117,20 +114,18 @@ absl::StatusOr> EvaluateP4Program( egress_port_is_physical = egress_port_is_physical || context.egress_port == port; } - z3_solver->add(ingress_port_is_physical); + solver_state->solver->add(ingress_port_is_physical); // TODO: Lift this constraint, it should not be necessary and // prevents generation of packet-ins. - z3_solver->add(context.trace.dropped || egress_port_is_physical); + solver_state->solver->add(context.trace.dropped || egress_port_is_physical); } // Assemble and return result. - return std::make_unique(dataplane.program, dataplane.entries, - std::move(context), std::move(z3_solver), - std::move(translator)); + return solver_state; } absl::StatusOr> Solve( - const SolverState &solver_state) { + SolverState &solver_state) { z3::check_result check_result = solver_state.solver->check(); switch (check_result) { case z3::unsat: diff --git a/p4_symbolic/symbolic/symbolic.h b/p4_symbolic/symbolic/symbolic.h index 782e0020..270c4f60 100644 --- a/p4_symbolic/symbolic/symbolic.h +++ b/p4_symbolic/symbolic/symbolic.h @@ -24,14 +24,12 @@ #include #include -#include "absl/base/attributes.h" -#include "absl/base/macros.h" -#include "absl/strings/str_cat.h" #include "absl/strings/string_view.h" #include "p4/v1/p4runtime.pb.h" #include "p4_symbolic/ir/table_entries.h" -#include "p4_symbolic/symbolic/guarded_map.h" +#include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/values.h" +#include "p4_symbolic/z3_util.h" #include "z3++.h" namespace p4_symbolic { @@ -65,138 +63,11 @@ constexpr absl::string_view kGotClonedPseudoField = "$got_cloned$"; constexpr absl::string_view kParserErrorField = "standard_metadata.parser_error"; -// Maps the name of a header field in the p4 program to its concrete value. -using ConcretePerPacketState = absl::btree_map; - -// The symbolic counterpart of ConcretePerPacketState. -// Maps the name of a header field in the p4 program to its symbolic value. -// This can be used to constrain p4 program fields inside assertions. -// This is automatically constructred from the header type definitions -// the p4 program has. -// Assume the p4 program has a header instance named "standard_metadata" of type -// "standard_metadata_t", which has field "ingress_port" of type "bit<9>" in it. -// Then, we will have: -// SymbolicMetadata["standard_metadata.ingress_port"] = -// -// An instance of this type is passed around and mutated by the functions -// responsible for symbolically evaluating the program. -using SymbolicPerPacketState = SymbolicGuardedMap; - // V1model's `mark_to_drop` primitive sets the `egress_spec` field to this // value to indicate the packet should be dropped at the end of ingress/egress // processing. See v1model.p4 for details. z3::expr EgressSpecDroppedValue(); -// Expresses a concrete match for a corresponding concrete packet with a -// table in the program. -struct ConcreteTableMatch { - bool matched; // false if no entry in this table was matched, true otherwise. - // If matched is false, this is set to -1. - // If matched is true, this is the index of the matched table entry, or -1 if - // the default entry was matched. - int entry_index; - std::string to_string() const { - if (!matched) { - return "was not matched!"; - } - return absl::StrCat("was matched on entry ", entry_index); - } -}; - -// Exposes a symbolic handle for a match between the symbolic packet and -// a symbolic table. -// This allows encoding of constraints on which (if any) entries are matched, -// and the value of the match. -// e.g. for some table "": -// (.entry_index == i) iff -// [][i] was matched/hit. -struct SymbolicTableMatch { - z3::expr matched; - z3::expr entry_index; -}; - -// `SymbolicTableMatch`es by table name. -using SymbolicTableMatches = absl::btree_map; - -// Specifies the expected trace in the program that the corresponding -// concrete packet is expected to take. -struct ConcreteTrace { - absl::btree_map matched_entries; - // Can be extended more in the future to include useful - // flags about dropping the packet, taking specific code (e.g. if) - // branches, vrf, other interesting events, etc. - bool dropped; // true if the packet was dropped. - bool got_cloned; // true if the packet got cloned. - std::string to_string() const { - std::string result; - absl::StrAppend(&result, "dropped = ", dropped, "\n"); - absl::StrAppend(&result, "got cloned = ", got_cloned); - for (const auto &[table, match] : matched_entries) { - absl::StrAppend(&result, "\n", table, " => ", match.to_string()); - } - return result; - } -}; - -// Provides symbolic handles for the trace the symbolic packet is constrained -// to take in the program. -struct SymbolicTrace { - // Full table name to its symbolic match. - // TODO: Rename to matches_by_table_name. - SymbolicTableMatches matched_entries; - z3::expr dropped; - z3::expr got_cloned; -}; - -// The result of solving with some assertion. -// This contains an input test packet with its predicted flow in the program, -// and the predicted output. -struct ConcreteContext { - std::string ingress_port; - std::string egress_port; - ConcretePerPacketState ingress_headers; - ConcretePerPacketState parsed_headers; - ConcretePerPacketState egress_headers; - ConcreteTrace trace; // Expected trace in the program. - - std::string to_string() const { return to_string(false); } - std::string to_string(bool verbose) const { - auto result = absl::StrCat("ingress_port = ", ingress_port, "\n", - "egress_port = ", egress_port, "\n", "trace:\n", - trace.to_string()); - if (verbose) { - auto ingress_string = absl::StrCat("ingress_headers", ":"); - auto parsed_string = absl::StrCat("parsed_headers", ":"); - auto egress_string = absl::StrCat("egress_headers", ":"); - for (const auto &[name, ingress_value] : ingress_headers) { - absl::StrAppend(&ingress_string, "\n", name, " = ", ingress_value); - } - for (const auto &[name, parsed_value] : parsed_headers) { - absl::StrAppend(&parsed_string, "\n", name, " = ", parsed_value); - } - for (const auto &[name, egress_value] : egress_headers) { - absl::StrAppend(&egress_string, "\n", name, " = ", egress_value); - } - absl::StrAppend(&result, "\n\n", ingress_string, "\n\n", parsed_string, - "\n\n", egress_string); - } - return result; - } -}; - -// The symbolic context within our analysis. -// Exposes symbolic handles for the fields of the input packet, -// and its trace in the program. -// Assertions are defined on a symbolic context. -struct SymbolicContext { - z3::expr ingress_port; - z3::expr egress_port; - SymbolicPerPacketState ingress_headers; - SymbolicPerPacketState parsed_headers; - SymbolicPerPacketState egress_headers; - SymbolicTrace trace; -}; - // The overall state of our symbolic solver/interpreter. // This is returned by our main analysis/interpration function, and is used // to find concrete test packets and for debugging. @@ -207,14 +78,10 @@ struct SymbolicContext { // many times. class SolverState { public: - SolverState(ir::P4Program program, ir::TableEntries entries, - SymbolicContext context, std::unique_ptr solver, - values::P4RuntimeTranslator translator) + SolverState(ir::P4Program program, ir::TableEntries entries) : program(std::move(program)), entries(std::move(entries)), - context(std::move(context)), - solver(std::move(solver)), - translator(std::move(translator)) {} + solver(std::make_unique(Z3Context())) {} SolverState(const SolverState &) = delete; SolverState(SolverState &&) = default; ~SolverState() { @@ -227,10 +94,10 @@ class SolverState { } // Returns the SMT formulae of all assertions in the solver. - std::string GetSolverSMT() const; + std::string GetSolverSMT(); // Returns the SMT formulae of all ingress, parsed, and egress headers and // solver constraints. - std::string GetHeadersAndSolverConstraintsSMT() const; + std::string GetHeadersAndSolverConstraintsSMT(); // The IR of the p4 program being analyzed. ir::P4Program program; @@ -278,16 +145,9 @@ absl::StatusOr> EvaluateP4Program( // Finds a concrete packet and flow in the program that satisfies the given // assertion and meets the structure constrained by solver_state. -absl::StatusOr> -Solve(SolverState &solver_state, const Assertion &assertion); -absl::StatusOr> -Solve(const SolverState &solver_state); - -ABSL_DEPRECATED( - "Use the overload Solve(SolverState&, const Assertion&) instead.") -absl::StatusOr> -Solve(const std::unique_ptr &solver_state, - const Assertion &assertion); +absl::StatusOr> Solve(SolverState &solver_state); +absl::StatusOr> Solve( + SolverState &solver_state, const Assertion &assertion); // Dumps the underlying SMT program for debugging. std::string DebugSMT(const std::unique_ptr &solver_state, diff --git a/p4_symbolic/symbolic/table.cc b/p4_symbolic/symbolic/table.cc index 4485b3c8..83d199d7 100644 --- a/p4_symbolic/symbolic/table.cc +++ b/p4_symbolic/symbolic/table.cc @@ -40,7 +40,6 @@ #include "p4_symbolic/symbolic/action.h" #include "p4_symbolic/symbolic/control.h" #include "p4_symbolic/symbolic/operators.h" -#include "p4_symbolic/symbolic/symbolic.h" #include "p4_symbolic/symbolic/util.h" #include "p4_symbolic/symbolic/values.h" #include "p4_symbolic/z3_util.h" diff --git a/p4_symbolic/symbolic/table.h b/p4_symbolic/symbolic/table.h index becffb7a..27d0fb27 100644 --- a/p4_symbolic/symbolic/table.h +++ b/p4_symbolic/symbolic/table.h @@ -26,7 +26,7 @@ #include "absl/status/statusor.h" #include "p4_symbolic/ir/ir.h" #include "p4_symbolic/ir/ir.pb.h" -#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/values.h" #include "z3++.h" diff --git a/p4_symbolic/symbolic/v1model.cc b/p4_symbolic/symbolic/v1model.cc index c91b8e5f..51f7bfb8 100644 --- a/p4_symbolic/symbolic/v1model.cc +++ b/p4_symbolic/symbolic/v1model.cc @@ -95,21 +95,22 @@ absl::Status InitializeIngressHeaders(const ir::P4Program &program, return absl::OkStatus(); } -absl::StatusOr EvaluateV1model( - const ir::Dataplane &data_plane, const std::vector &physical_ports, - values::P4RuntimeTranslator &translator) { +absl::Status EvaluateV1model(const ir::Dataplane &data_plane, + const std::vector &physical_ports, + SymbolicContext &context, + values::P4RuntimeTranslator &translator) { // Check input physical ports. RETURN_IF_ERROR(CheckPhysicalPortsConformanceToV1Model(physical_ports)); // The ingress headers represent the symbolic ingress packet before entering // the parsers or the pipelines. It contains an unconstrained symbolic // variable for each header field. - ASSIGN_OR_RETURN(SymbolicPerPacketState ingress_headers, + ASSIGN_OR_RETURN(context.ingress_headers, SymbolicGuardedMap::CreateSymbolicGuardedMap( data_plane.program.headers())); // Initialize the symbolic ingress packet before evaluation. RETURN_IF_ERROR( - InitializeIngressHeaders(data_plane.program, ingress_headers)); + InitializeIngressHeaders(data_plane.program, context.ingress_headers)); // Evaluate all parsers in the P4 program. // If a parser error occurs, the `standard_metadata.parser_error` field will @@ -117,69 +118,60 @@ absl::StatusOr EvaluateV1model( // directly to the ingress pipeline. The current implementation of P4-Symbolic // will only yield 2 kinds of parser error, NoError and NoMatch. ASSIGN_OR_RETURN( - SymbolicPerPacketState parsed_headers, - parser::EvaluateParsers(data_plane.program, ingress_headers)); + context.parsed_headers, + parser::EvaluateParsers(data_plane.program, context.ingress_headers)); // Update the ingress_headers' valid fields to be parsed_headers' extracted // fields. for (const auto &[header_name, _] : Ordered(data_plane.program.headers())) { - ASSIGN_OR_RETURN(z3::expr extracted, - parsed_headers.Get(header_name, kExtractedPseudoField)); - RETURN_IF_ERROR(ingress_headers.UnguardedSet(header_name, kValidPseudoField, - extracted)); + ASSIGN_OR_RETURN( + z3::expr extracted, + context.parsed_headers.Get(header_name, kExtractedPseudoField)); + RETURN_IF_ERROR(context.ingress_headers.UnguardedSet( + header_name, kValidPseudoField, extracted)); } // Duplicate the symbolic headers for evaluating pipelines. This is to // preserve the symbolic state after evaluating the parsers but before // evaluating the pipelines. - SymbolicPerPacketState egress_headers = parsed_headers; + context.egress_headers = context.parsed_headers; // Evaluate the ingress pipeline. // TODO: This is a simplification that omits a lot of features, e.g. // cloning, digests, resubmit, and multicast. The full semantics we should // implement is documented here: // https://github.com/p4lang/behavioral-model/blob/main/docs/simple_switch.md#pseudocode-for-what-happens-at-the-end-of-ingress-and-egress-processing - ASSIGN_OR_RETURN(SymbolicTableMatches matches, - control::EvaluatePipeline( - data_plane, "ingress", &egress_headers, &translator, - /*guard=*/Z3Context().bool_val(true))); - ASSIGN_OR_RETURN(z3::expr dropped, IsDropped(egress_headers)); + ASSIGN_OR_RETURN( + SymbolicTableMatches matches, + control::EvaluatePipeline(data_plane, "ingress", &context.egress_headers, + &translator, + /*guard=*/Z3Context().bool_val(true))); + ASSIGN_OR_RETURN(z3::expr dropped, IsDropped(context.egress_headers)); // Constrain egress_port to be equal to egress_spec. ASSIGN_OR_RETURN(z3::expr egress_spec, - egress_headers.Get("standard_metadata.egress_spec")); - RETURN_IF_ERROR(egress_headers.Set("standard_metadata.egress_port", - egress_spec, - /*guard=*/Z3Context().bool_val(true))); + context.egress_headers.Get("standard_metadata.egress_spec")); + RETURN_IF_ERROR( + context.egress_headers.Set("standard_metadata.egress_port", egress_spec, + /*guard=*/Z3Context().bool_val(true))); // Evaluate the egress pipeline. - ASSIGN_OR_RETURN(SymbolicTableMatches egress_matches, - control::EvaluatePipeline(data_plane, "egress", - &egress_headers, &translator, - /*guard=*/!dropped)); + ASSIGN_OR_RETURN( + SymbolicTableMatches egress_matches, + control::EvaluatePipeline(data_plane, "egress", &context.egress_headers, + &translator, + /*guard=*/!dropped)); matches.merge(std::move(egress_matches)); // Populate and build the symbolic context. - ASSIGN_OR_RETURN(dropped, IsDropped(egress_headers)); - ASSIGN_OR_RETURN(z3::expr got_cloned, GotCloned(egress_headers)); - ASSIGN_OR_RETURN(z3::expr ingress_port, - ingress_headers.Get("standard_metadata.ingress_port")); - ASSIGN_OR_RETURN(z3::expr egress_port, - egress_headers.Get("standard_metadata.egress_spec")); - - return SymbolicContext{ - .ingress_port = std::move(ingress_port), - .egress_port = std::move(egress_port), - .ingress_headers = std::move(ingress_headers), - .parsed_headers = std::move(parsed_headers), - .egress_headers = std::move(egress_headers), - .trace = - { - .matched_entries = std::move(matches), - .dropped = std::move(dropped), - .got_cloned = std::move(got_cloned), - }, - }; + context.trace.matched_entries = std::move(matches); + ASSIGN_OR_RETURN(context.trace.dropped, IsDropped(context.egress_headers)); + ASSIGN_OR_RETURN(context.trace.got_cloned, GotCloned(context.egress_headers)); + ASSIGN_OR_RETURN(context.ingress_port, context.ingress_headers.Get( + "standard_metadata.ingress_port")); + ASSIGN_OR_RETURN(context.egress_port, + context.egress_headers.Get("standard_metadata.egress_spec")); + return absl::OkStatus(); } } // namespace v1model diff --git a/p4_symbolic/symbolic/v1model.h b/p4_symbolic/symbolic/v1model.h index b0dc9371..f437d848 100644 --- a/p4_symbolic/symbolic/v1model.h +++ b/p4_symbolic/symbolic/v1model.h @@ -17,9 +17,8 @@ #include -#include "absl/status/statusor.h" #include "p4_symbolic/ir/ir.h" -#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/context.h" #include "p4_symbolic/symbolic/values.h" namespace p4_symbolic { @@ -33,9 +32,10 @@ absl::Status InitializeIngressHeaders(const ir::P4Program &program, // Symbolically evaluates the parser, ingress, and egress pipelines of the given // P4 program with the given entries, assuming the program is written against V1 // model. -absl::StatusOr EvaluateV1model( - const ir::Dataplane &data_plane, const std::vector &physical_ports, - values::P4RuntimeTranslator &translator); +absl::Status EvaluateV1model(const ir::Dataplane &data_plane, + const std::vector &physical_ports, + SymbolicContext &context, + values::P4RuntimeTranslator &translator); } // namespace v1model } // namespace symbolic diff --git a/p4_symbolic/symbolic/values.h b/p4_symbolic/symbolic/values.h index 92d61917..26e8629a 100644 --- a/p4_symbolic/symbolic/values.h +++ b/p4_symbolic/symbolic/values.h @@ -22,11 +22,12 @@ #define P4_SYMBOLIC_SYMBOLIC_VALUES_H_ #include -#include #include #include +#include +#include -#include "gutil/status.h" +#include "absl/status/statusor.h" #include "p4_pdpi/ir.pb.h" #include "z3++.h" diff --git a/p4_symbolic/symbolic/values_test.cc b/p4_symbolic/symbolic/values_test.cc index 9eb02c04..93277d91 100644 --- a/p4_symbolic/symbolic/values_test.cc +++ b/p4_symbolic/symbolic/values_test.cc @@ -46,56 +46,56 @@ TEST(TranslateValueToP4RT, ReverseTranslatedValuesAreEqualToTheOriginalOnes) { // Make sure the code conforms to the peculiarities of PDPI's value conversion. TEST(FormatP4RTValue, WorksFor64BitIPv6) { - P4RuntimeTranslator trasnlator; + P4RuntimeTranslator translator; ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto( R"pb(ipv6: "0000:ffff:ffff:ffff::")pb")); ASSERT_OK_AND_ASSIGN( z3::expr z3_expr, FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value, - /*bitwidth=*/64, &trasnlator)); + /*bitwidth=*/64, &translator)); ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x0000'ffff'ffff'ffffULL); } TEST(FormatP4RTValue, WorksForIpv4) { - P4RuntimeTranslator trasnlator; + P4RuntimeTranslator translator; ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto( R"pb(ipv4: "127.0.0.1")pb")); ASSERT_OK_AND_ASSIGN( z3::expr z3_expr, FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value, - /*bitwidth=*/32, &trasnlator)); + /*bitwidth=*/32, &translator)); ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x7f000001); } TEST(FormatP4RTValue, WorksForMac) { - P4RuntimeTranslator trasnlator; + P4RuntimeTranslator translator; ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto( R"pb(mac: "01:02:03:04:05:06")pb")); ASSERT_OK_AND_ASSIGN( z3::expr z3_expr, FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value, - /*bitwidth=*/48, &trasnlator)); + /*bitwidth=*/48, &translator)); ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x01'02'03'04'05'06ULL); } TEST(FormatP4RTValue, WorksForHexString) { - P4RuntimeTranslator trasnlator; + P4RuntimeTranslator translator; ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto( R"pb(hex_str: "0xabcd")pb")); ASSERT_OK_AND_ASSIGN( z3::expr z3_expr, FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value, - /*bitwidth=*/16, &trasnlator)); + /*bitwidth=*/16, &translator)); ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0xabcd); } TEST(FormatP4RTValue, FailsForStringWithNonZeroBitwidth) { - P4RuntimeTranslator trasnlator; + P4RuntimeTranslator translator; ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto( R"pb(str: "dummy_value")pb")); ASSERT_THAT(FormatP4RTValue(Z3Context(), kFieldName, kFieldType, ir_value, - /*bitwidth=*/16, &trasnlator), + /*bitwidth=*/16, &translator), StatusIs(absl::StatusCode::kInvalidArgument)); }