diff --git a/gutil/io.cc b/gutil/io.cc index 3d1b7542..6508f4c3 100644 --- a/gutil/io.cc +++ b/gutil/io.cc @@ -1,4 +1,4 @@ -// Copyright 2020 Google LLC +// 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. diff --git a/gutil/io.h b/gutil/io.h index 34f0f117..b14e23c6 100644 --- a/gutil/io.h +++ b/gutil/io.h @@ -1,4 +1,4 @@ -// Copyright 2020 Google LLC +// 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. diff --git a/p4_fuzzer/fuzzer_tests.cc b/p4_fuzzer/fuzzer_tests.cc index 62254465..9defc445 100644 --- a/p4_fuzzer/fuzzer_tests.cc +++ b/p4_fuzzer/fuzzer_tests.cc @@ -151,12 +151,13 @@ TEST_P(FuzzTest, P4rtWriteAndCheckNoInternalErrors) { ASSERT_OK_AND_ASSIGN( const pdpi::IrTableDefinition& table, gutil::FindOrStatus(info.tables_by_id(), table_id)); - // TODO: acl_lookup_table has a resource limit problem. + // TODO: acl_pre_ingress_table has a resource limit + // problem. // TODO: router_interface_table, ipv4_table and // ipv6_table all have resource limit problems. // TODO: wcmp_group_table has a resource limit problem. if (!(mask_known_failures && - (table.preamble().alias() == "acl_lookup_table" || + (table.preamble().alias() == "acl_pre_ingress_table" || table.preamble().alias() == "router_interface_table" || table.preamble().alias() == "ipv4_table" || table.preamble().alias() == "ipv6_table" || diff --git a/p4_symbolic/BUILD.bazel b/p4_symbolic/BUILD.bazel index cd5432f8..6c044033 100644 --- a/p4_symbolic/BUILD.bazel +++ b/p4_symbolic/BUILD.bazel @@ -26,11 +26,11 @@ cc_binary( ], deps = [ ":parser", + "//gutil:io", "//gutil:status", "//p4_symbolic/bmv2", "//p4_symbolic/sai:parser", "//p4_symbolic/symbolic", - "//p4_symbolic/util", "@com_google_absl//absl/flags:flag", "@com_google_absl//absl/flags:parse", "@com_google_absl//absl/flags:usage", @@ -45,7 +45,8 @@ cc_library( srcs = ["parser.cc"], hdrs = ["parser.h"], deps = [ - "//gutil:proto", + "//gutil:io", + "//gutil:proto", "//gutil:status", "//p4_pdpi:ir_cc_proto", "//p4_symbolic/bmv2", @@ -53,7 +54,6 @@ cc_library( "//p4_symbolic/ir:ir_cc_proto", "//p4_symbolic/ir:pdpi_driver", "//p4_symbolic/symbolic", - "//p4_symbolic/util", "@com_google_absl//absl/types:span", ], ) diff --git a/p4_symbolic/bmv2/BUILD.bazel b/p4_symbolic/bmv2/BUILD.bazel index f80130ff..c2aaf3f0 100644 --- a/p4_symbolic/bmv2/BUILD.bazel +++ b/p4_symbolic/bmv2/BUILD.bazel @@ -44,8 +44,8 @@ cc_library( ], deps = [ ":bmv2_cc_proto", + "//gutil:io", "//gutil:status", - "//p4_symbolic/util", "@com_google_protobuf//:protobuf", ], ) @@ -55,8 +55,8 @@ cc_binary( srcs = ["test.cc"], deps = [ ":bmv2", + "//gutil:io", "//gutil:status", - "//p4_symbolic/util", "@com_google_absl//absl/flags:flag", "@com_google_absl//absl/flags:parse", "@com_google_absl//absl/flags:usage", diff --git a/p4_symbolic/bmv2/bmv2.cc b/p4_symbolic/bmv2/bmv2.cc index 0c5623da..08dec256 100644 --- a/p4_symbolic/bmv2/bmv2.cc +++ b/p4_symbolic/bmv2/bmv2.cc @@ -17,14 +17,14 @@ #include #include "google/protobuf/util/json_util.h" +#include "gutil/io.h" #include "gutil/status.h" -#include "p4_symbolic/util/io.h" namespace p4_symbolic { namespace bmv2 { absl::StatusOr ParseBmv2JsonFile(const std::string &json_path) { - ASSIGN_OR_RETURN(std::string json, util::ReadFile(json_path)); + ASSIGN_OR_RETURN(std::string json, gutil::ReadFile(json_path)); return ParseBmv2JsonString(json); } diff --git a/p4_symbolic/bmv2/test.cc b/p4_symbolic/bmv2/test.cc index 99dd4d14..0de25489 100644 --- a/p4_symbolic/bmv2/test.cc +++ b/p4_symbolic/bmv2/test.cc @@ -30,9 +30,9 @@ #include "absl/strings/str_format.h" #include "google/protobuf/text_format.h" #include "google/protobuf/util/json_util.h" +#include "gutil/io.h" #include "gutil/status.h" #include "p4_symbolic/bmv2/bmv2.h" -#include "p4_symbolic/util/io.h" ABSL_FLAG(std::string, bmv2, "", "The path to the bmv2 json file (required)"); ABSL_FLAG(std::string, protobuf, "", @@ -55,8 +55,7 @@ absl::Status Test() { p4_symbolic::bmv2::ParseBmv2JsonFile(bmv2_path.c_str())); // Dumping protobuf. - RETURN_IF_ERROR( - p4_symbolic::util::WriteFile(bmv2.DebugString(), protobuf_path.c_str())); + RETURN_IF_ERROR(gutil::WriteFile(bmv2.DebugString(), protobuf_path.c_str())); // Dumping JSON. google::protobuf::util::JsonPrintOptions dumping_options; @@ -68,8 +67,7 @@ absl::Status Test() { RETURN_IF_ERROR( gutil::ToAbslStatus(google::protobuf::util::MessageToJsonString( bmv2, &json_output_str, dumping_options))); - RETURN_IF_ERROR( - p4_symbolic::util::WriteFile(json_output_str, json_path.c_str())); + RETURN_IF_ERROR(gutil::WriteFile(json_output_str, json_path.c_str())); return absl::OkStatus(); } diff --git a/p4_symbolic/ir/BUILD.bazel b/p4_symbolic/ir/BUILD.bazel index be4ec3e5..14674ca3 100644 --- a/p4_symbolic/ir/BUILD.bazel +++ b/p4_symbolic/ir/BUILD.bazel @@ -59,10 +59,10 @@ cc_library( ], deps = [ ":ir_cc_proto", + "//gutil:io", "//gutil:status", "//p4_pdpi:ir", "//p4_pdpi:ir_cc_proto", - "//p4_symbolic/util", "@com_github_p4lang_p4runtime//:p4runtime_cc_proto", "@com_google_absl//absl/status", "@com_google_absl//absl/strings", diff --git a/p4_symbolic/ir/ir.proto b/p4_symbolic/ir/ir.proto index 72d6ce15..590bd0b7 100644 --- a/p4_symbolic/ir/ir.proto +++ b/p4_symbolic/ir/ir.proto @@ -25,7 +25,7 @@ // Additionally, some types of expressions and statements are unsupported, these // are described in the relevant sections of this file. // See the bmv2 JSON format reference for more information: -// https://github.com/p4lang/behavioral-model/blob/master/docs/JSON_format.md +// https://github.com/p4lang/behavioral-model/blob/main/docs/JSON_format.md syntax = "proto3"; @@ -51,7 +51,7 @@ message P4Program { // TODO: If needed in the future, action calls can be added here, for // action calls that are not wrapped in other control constructs. - // https://github.com/p4lang/behavioral-model/blob/master/docs/JSON_format.md#pipelines + // https://github.com/p4lang/behavioral-model/blob/main/docs/JSON_format.md#pipelines } // A header type definition. diff --git a/p4_symbolic/ir/table_entries.cc b/p4_symbolic/ir/table_entries.cc index 714b9266..331ecfb5 100644 --- a/p4_symbolic/ir/table_entries.cc +++ b/p4_symbolic/ir/table_entries.cc @@ -18,11 +18,11 @@ #include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" #include "absl/strings/str_split.h" +#include "gutil/io.h" #include "gutil/status.h" #include "p4/v1/p4runtime.pb.h" #include "p4_pdpi/ir.h" #include "p4_pdpi/ir.pb.h" -#include "p4_symbolic/util/io.h" namespace p4_symbolic { namespace ir { diff --git a/p4_symbolic/main.cc b/p4_symbolic/main.cc index ccf635b1..8451f0ec 100644 --- a/p4_symbolic/main.cc +++ b/p4_symbolic/main.cc @@ -27,12 +27,12 @@ #include "absl/status/status.h" #include "absl/strings/str_cat.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_symbolic/symbolic/symbolic.h" -#include "p4_symbolic/util/io.h" ABSL_FLAG(std::string, p4info, "", "The path to the p4info protobuf file (required)"); @@ -173,8 +173,7 @@ absl::Status ParseAndEvaluate() { // Debugging. if (!debug_path.empty()) { - RETURN_IF_ERROR( - p4_symbolic::util::WriteFile(debug_smt_formula, debug_path)); + RETURN_IF_ERROR(gutil::WriteFile(debug_smt_formula, debug_path)); } return absl::OkStatus(); diff --git a/p4_symbolic/parser.cc b/p4_symbolic/parser.cc index 6d58d91b..bf167715 100644 --- a/p4_symbolic/parser.cc +++ b/p4_symbolic/parser.cc @@ -14,11 +14,11 @@ #include "p4_symbolic/parser.h" +#include "gutil/io.h" #include "gutil/proto.h" #include "p4_symbolic/bmv2/bmv2.h" #include "p4_symbolic/ir/ir.h" #include "p4_symbolic/ir/pdpi_driver.h" -#include "p4_symbolic/util/io.h" namespace p4_symbolic { @@ -58,7 +58,7 @@ 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, util::ReadFile(bmv2_json_path)); + ASSIGN_OR_RETURN(std::string bmv2_json, gutil::ReadFile(bmv2_json_path)); // Parse p4info file into pdpi format. ASSIGN_OR_RETURN(pdpi::IrP4Info p4info, diff --git a/p4_symbolic/sai/fields.cc b/p4_symbolic/sai/fields.cc index 02145369..99f20165 100644 --- a/p4_symbolic/sai/fields.cc +++ b/p4_symbolic/sai/fields.cc @@ -100,6 +100,11 @@ absl::StatusOr GetSaiFields(const SymbolicPerPacketState& state) { .admit_to_l3 = get_metadata_field("admit_to_l3"), .vrf_id = get_metadata_field("vrf_id"), .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"), + }; + auto standard_metadata = V1ModelStandardMetadata{ + .ingress_port = get_field("standard_metadata.ingress_port"), }; if (!errors.empty()) { diff --git a/p4_symbolic/sai/fields.h b/p4_symbolic/sai/fields.h index 103c2982..25dd70ef 100644 --- a/p4_symbolic/sai/fields.h +++ b/p4_symbolic/sai/fields.h @@ -63,8 +63,14 @@ struct SaiLocalMetadata { z3::expr vrf_id; // TODO: add `packet_rewrites` fields. z3::expr mirror_session_id_valid; - // TODO: add `mirror*` fields. - // TODO: Add `color` field. + z3::expr ingress_port; + z3::expr route_metadata; +}; + +// Symbolic version of `struct standard_metadata_t` in v1model.p4 +// TODO: Add missing fields, as needed. +struct V1ModelStandardMetadata { + z3::expr ingress_port; }; struct SaiFields { diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel index 608ae6ec..b601b1f2 100644 --- a/p4_symbolic/symbolic/BUILD.bazel +++ b/p4_symbolic/symbolic/BUILD.bazel @@ -27,7 +27,6 @@ cc_library( "control.cc", "guarded_map.cc", "operators.cc", - "packet.cc", "symbolic.cc", "table.cc", "util.cc", @@ -39,7 +38,6 @@ cc_library( "control.h", "guarded_map.h", "operators.h", - "packet.h", "symbolic.h", "table.h", "util.h", @@ -59,10 +57,7 @@ cc_library( "@com_github_p4lang_p4runtime//:p4info_cc_proto", "@com_github_z3prover_z3//:api", "@com_gnu_gmp//:gmp", - "@com_google_absl//absl/algorithm:container", "@com_google_absl//absl/cleanup", - "@com_google_absl//absl/container:btree", - "@com_google_absl//absl/memory", "@com_google_absl//absl/status", "@com_google_absl//absl/strings", "@com_google_absl//absl/strings:str_format", diff --git a/p4_symbolic/symbolic/packet.cc b/p4_symbolic/symbolic/packet.cc deleted file mode 100644 index 12c75a74..00000000 --- a/p4_symbolic/symbolic/packet.cc +++ /dev/null @@ -1,76 +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. - -// Contains helpers for creating, extracting, and managing concerete and -// symbolic packet structs. - -#include "p4_symbolic/symbolic/packet.h" - -#include - -namespace p4_symbolic { -namespace symbolic { -namespace packet { - -namespace { - -// Get the symbolic field value from state or return a default value -// of the given size. -z3::expr GetOrDefault(SymbolicPerPacketState state, const std::string &field, - unsigned int default_value_bit_size) { - if (state.ContainsKey(field)) { - return state.Get(field).value(); - } -} - -} // namespace - -SymbolicPacket ExtractSymbolicPacket(SymbolicPerPacketState state) { - z3::expr ipv6_src = GetOrDefault(state, "ipv6.src_addr", 128); - z3::expr ipv6_dst = GetOrDefault(state, "ipv6.dst_addr", 128); - - return SymbolicPacket{GetOrDefault(state, "ethernet.src_addr", 48), - GetOrDefault(state, "ethernet.dst_addr", 48), - GetOrDefault(state, "ethernet.ether_type", 16), - - GetOrDefault(state, "ipv4.src_addr", 32), - GetOrDefault(state, "ipv4.dst_addr", 32), - ipv6_dst.extract(127, 64), - ipv6_dst.extract(63, 0), - GetOrDefault(state, "ipv4.protocol", 8), - GetOrDefault(state, "ipv4.dscp", 6), - GetOrDefault(state, "ipv4.ttl", 8), - - GetOrDefault(state, "icmp.type", 8)}; -} - -ConcretePacket ExtractConcretePacket(SymbolicPacket packet, z3::model model) { - return {model.eval(packet.eth_src, true).to_string(), - model.eval(packet.eth_dst, true).to_string(), - model.eval(packet.eth_type, true).to_string(), - - model.eval(packet.ipv4_src, true).to_string(), - model.eval(packet.ipv4_dst, true).to_string(), - model.eval(packet.ipv6_dst_upper, true).to_string(), - model.eval(packet.ipv6_dst_lower, true).to_string(), - model.eval(packet.protocol, true).to_string(), - model.eval(packet.dscp, true).to_string(), - model.eval(packet.ttl, true).to_string(), - - model.eval(packet.icmp_type, true).to_string()}; -} - -} // namespace packet -} // namespace symbolic -} // namespace p4_symbolic diff --git a/p4_symbolic/symbolic/packet.h b/p4_symbolic/symbolic/packet.h deleted file mode 100644 index bd18674a..00000000 --- a/p4_symbolic/symbolic/packet.h +++ /dev/null @@ -1,40 +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. - -// Contains helpers for creating, extracting, and managing concerete and -// symbolic packet structs. - -#ifndef P4_SYMBOLIC_SYMBOLIC_PACKET_H_ -#define P4_SYMBOLIC_SYMBOLIC_PACKET_H_ - -#include "gutil/status.h" -#include "p4_symbolic/symbolic/symbolic.h" -#include "z3++.h" - -namespace p4_symbolic { -namespace symbolic { -namespace packet { - -// Extract the packet fields from their p4 program counterparts. -SymbolicPacket ExtractSymbolicPacket(SymbolicPerPacketState state); - -// Extract a concrete packet by evaluating every field's corresponding -// expression in the model. -ConcretePacket ExtractConcretePacket(SymbolicPacket packet, z3::model model); - -} // namespace packet -} // namespace symbolic -} // namespace p4_symbolic - -#endif // P4_SYMBOLIC_SYMBOLIC_PACKET_H_ diff --git a/p4_symbolic/symbolic/symbolic.cc b/p4_symbolic/symbolic/symbolic.cc index bee51063..03df3933 100644 --- a/p4_symbolic/symbolic/symbolic.cc +++ b/p4_symbolic/symbolic/symbolic.cc @@ -16,15 +16,12 @@ #include -#include "absl/algorithm/container.h" #include "absl/cleanup/cleanup.h" -#include "absl/memory/memory.h" #include "absl/types/optional.h" #include "glog/logging.h" #include "gutil/status.h" #include "p4_symbolic/symbolic/control.h" #include "p4_symbolic/symbolic/operators.h" -#include "p4_symbolic/symbolic/packet.h" #include "p4_symbolic/symbolic/util.h" #include "p4_symbolic/z3_util.h" @@ -132,11 +129,11 @@ absl::StatusOr> Solve( solver_state->solver->push(); solver_state->solver->add(constraint); + auto pop = absl::Cleanup([&] { solver_state->solver->pop(); }); z3::check_result check_result = solver_state->solver->check(); switch (check_result) { case z3::unsat: case z3::unknown: - solver_state->solver->pop(); return absl::nullopt; case z3::sat: @@ -145,7 +142,6 @@ absl::StatusOr> Solve( ConcreteContext result, util::ExtractFromModel(solver_state->context, packet_model, solver_state->translator)); - solver_state->solver->pop(); return result; } LOG(DFATAL) << "invalid Z3 check() result: " diff --git a/p4_symbolic/symbolic/symbolic.h b/p4_symbolic/symbolic/symbolic.h index 6b46f93b..2ecf3b72 100644 --- a/p4_symbolic/symbolic/symbolic.h +++ b/p4_symbolic/symbolic/symbolic.h @@ -110,7 +110,7 @@ struct ConcreteTrace { absl::StrAppend(&result, "dropped = ", dropped, "\n"); absl::StrAppend(&result, "got cloned = ", got_cloned, "\n"); for (const auto &[table, match] : matched_entries) { - result = absl::StrCat(result, "\n", table, " => ", match.to_string()); + absl::StrAppend(&result, "\n", table, " => ", match.to_string()); } return result; } @@ -126,87 +126,31 @@ struct SymbolicTrace { z3::expr got_cloned; }; -// Specifies the concrete data inside a packet. -// This is a friendly helper struct, all information in this struct -// is extracted from ConcretePerPacketState. -struct ConcretePacket { - std::string eth_src; - std::string eth_dst; - std::string eth_type; - - std::string ipv4_src; - std::string ipv4_dst; - std::string ipv6_dst_upper; - std::string ipv6_dst_lower; - std::string protocol; - std::string dscp; - std::string ttl; - - std::string icmp_type; - - std::string to_string() const { - return absl::StrCat("eth_src = ", eth_src, "\n", "eth_dst = ", eth_dst, - "\n", "eth_type = ", eth_type, "\n", - "ipv4_src = ", ipv4_src, "\n", "ipv4_dst = ", ipv4_dst, - "\n", "ipv6_dst_upper = ", ipv6_dst_upper, "\n", - "ipv6_dst_lower = ", ipv6_dst_lower, "\n", - "protocol = ", protocol, "\n", "dscp = ", dscp, "\n", - "ttl = ", ttl, "\n", "icmp_type = ", icmp_type); - } -}; - -// A helper struct containing symbolic expressions for every field in a packet. -// All expressions in this struct are extracted from SymbolicPerPacketState. -// We explicitly give these fields name in this struct to simplify how the -// client code can impose constraints on them in assertions. -struct SymbolicPacket { - z3::expr eth_src; // 48 bit. - z3::expr eth_dst; // 48 bit. - z3::expr eth_type; // 16 bit. - - z3::expr ipv4_src; // 32 bit, valid if eth_type = 0x0800 - z3::expr ipv4_dst; // 32 bit, valid if eth_type = 0x0800 - z3::expr ipv6_dst_upper; // 64 bit, valid if eth_type = 0x86dd - z3::expr ipv6_dst_lower; // 64 bit, valid if eth_type = 0x86dd - z3::expr protocol; // 8 bit, valid if eth_type is ip - z3::expr dscp; // 6 bit, valid if eth_type is ip - z3::expr ttl; // 8 bit, valid if eth_type is ip - - z3::expr icmp_type; // 8 bit, valid if eth_type is ip -}; - // 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; - ConcretePacket ingress_packet; // Input packet into the program/switch. - ConcretePacket egress_packet; // Expected output packet. ConcretePerPacketState ingress_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\n", "ingress_packet:\n", ingress_packet.to_string(), "\n\n", - "egress_packet:\n", egress_packet.to_string(), "\n\n", "trace:\n", - trace.to_string()); + 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 egress_string = absl::StrCat("egress_headers", ":"); for (const auto &[name, ingress_value] : ingress_headers) { - ingress_string = - absl::StrCat(ingress_string, "\n", name, " = ", ingress_value); + absl::StrAppend(&ingress_string, "\n", name, " = ", ingress_value); } for (const auto &[name, egress_value] : egress_headers) { - egress_string = - absl::StrCat(egress_string, "\n", name, " = ", egress_value); + absl::StrAppend(&egress_string, "\n", name, " = ", egress_value); } - result = - absl::StrCat(result, "\n\n", ingress_string, "\n\n", egress_string); + absl::StrAppend(&result, "\n\n", ingress_string, "\n\n", egress_string); } return result; } diff --git a/p4_symbolic/tests/BUILD.bazel b/p4_symbolic/tests/BUILD.bazel index 013dcdcc..9bf1f6c3 100644 --- a/p4_symbolic/tests/BUILD.bazel +++ b/p4_symbolic/tests/BUILD.bazel @@ -13,6 +13,7 @@ cc_test( "//p4_pdpi:ir_cc_proto", "//p4_pdpi:pd", "//p4_symbolic:parser", + "//p4_symbolic:z3_util", "//p4_symbolic/sai:parser", "//p4_symbolic/symbolic", "//sai_p4/instantiations/google:sai_nonstandard_platforms_cc", diff --git a/p4_symbolic/tests/sai_p4_component_test.cc b/p4_symbolic/tests/sai_p4_component_test.cc index 14944e0c..4e973433 100644 --- a/p4_symbolic/tests/sai_p4_component_test.cc +++ b/p4_symbolic/tests/sai_p4_component_test.cc @@ -15,9 +15,10 @@ #include "p4_symbolic/parser.h" #include "p4_symbolic/sai/parser.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 "sai_p4/instantiations/google/sai_pd.pb.h" -#include "sai_p4/instantiations/google/instantiations.h" #include "thinkit/bazel_test_environment.h" namespace p4_symbolic { @@ -30,7 +31,7 @@ using ::testing::Not; constexpr absl::string_view kTableEntries = R"pb( entries { - acl_pre_ingress_table_entry { + acl_pre_ingress_table_entry { match { src_mac { value: "22:22:22:11:11:11" mask: "ff:ff:ff:ff:ff:ff" } dst_ip { value: "10.0.10.0" mask: "255.255.255.255" } diff --git a/p4_symbolic/util/BUILD.bazel b/p4_symbolic/util/BUILD.bazel deleted file mode 100644 index d9f9a016..00000000 --- a/p4_symbolic/util/BUILD.bazel +++ /dev/null @@ -1,37 +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. - -package( - default_visibility = ["//visibility:public"], - licenses = ["notice"], -) - -cc_library( - name = "util", - srcs = [ - "io.cc", - # "status.cc", - ], - hdrs = [ - "io.h", - # TODO: clean up. - # "status.h", - ], - deps = [ - "//gutil:status", - "@com_google_absl//absl/status", - "@com_google_absl//absl/strings", - "@com_google_absl//absl/strings:str_format", - ], -) diff --git a/p4_symbolic/util/io.cc b/p4_symbolic/util/io.cc deleted file mode 100644 index 000b8a7c..00000000 --- a/p4_symbolic/util/io.cc +++ /dev/null @@ -1,75 +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/util/io.h" - -#include -#include -#include -#include - -#include "absl/strings/str_format.h" -#include "gutil/status.h" - -namespace p4_symbolic { -namespace util { - -namespace { - -absl::Status ErrorNoToAbsl(const char *operation, const std::string &path) { - switch (errno) { - case EACCES: - case ENOENT: - return absl::NotFoundError( - absl::StrFormat("%s: %s", strerror(errno), path)); - default: - return absl::UnknownError(absl::StrFormat("Cannot %s file %s, errno = %d", - operation, path, errno)); - } -} - -} // namespace - -absl::StatusOr ReadFile(const std::string &path) { - std::ifstream f; - f.open(path.c_str()); - if (f.fail()) { - return ErrorNoToAbsl("open", path); - } - f >> std::noskipws; // Read whitespaces. - std::string result(std::istreambuf_iterator(f), - (std::istreambuf_iterator())); - if (f.bad()) { - return ErrorNoToAbsl("read", path); - } - f.close(); - return result; -} - -absl::Status WriteFile(const std::string &content, const std::string &path) { - std::ofstream f; - f.open(path.c_str()); - if (f.fail()) { - return ErrorNoToAbsl("open", path); - } - f << content; - f.close(); - if (f.bad()) { - return ErrorNoToAbsl("write", path); - } - return absl::OkStatus(); -} - -} // namespace util -} // namespace p4_symbolic diff --git a/p4_symbolic/util/io.h b/p4_symbolic/util/io.h deleted file mode 100644 index a105b072..00000000 --- a/p4_symbolic/util/io.h +++ /dev/null @@ -1,36 +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_UTIL_IO_H_ -#define P4_SYMBOLIC_UTIL_IO_H_ - -#include - -#include "absl/status/status.h" -#include "absl/strings/string_view.h" -#include "gutil/status.h" - -namespace p4_symbolic { -namespace util { - -// Reads the entire content of the file and returns it (or an error status). -absl::StatusOr ReadFile(const std::string &path); - -// Writes the content of the string to the file. -absl::Status WriteFile(const std::string &content, const std::string &path); - -} // namespace util -} // namespace p4_symbolic - -#endif // P4_SYMBOLIC_UTIL_IO_H_