From ae9158fa75b901f0c524be688840b84587d8a221 Mon Sep 17 00:00:00 2001 From: VSuryaprasad-hcl <159443973+VSuryaprasad-HCL@users.noreply.github.com> Date: Sat, 4 Jan 2025 01:02:11 +0000 Subject: [PATCH] [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. (#917) Co-authored-by: kishanps --- 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);