diff --git a/p4_symbolic/sai/sai.cc b/p4_symbolic/sai/sai.cc index bb2b084d..4f4ba146 100644 --- a/p4_symbolic/sai/sai.cc +++ b/p4_symbolic/sai/sai.cc @@ -44,7 +44,7 @@ absl::Status CheckPhysicalPortAndPortIdTypeValueConsistency( 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) + for (const auto& [_, numeric_value] : it->second.static_mapping) numeric_value_set.insert(numeric_value); } diff --git a/p4_symbolic/sai/sai_test.cc b/p4_symbolic/sai/sai_test.cc new file mode 100644 index 00000000..54fb144a --- /dev/null +++ b/p4_symbolic/sai/sai_test.cc @@ -0,0 +1,124 @@ +// 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/sai.h" + +#include +#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/pd.h" +#include "p4_symbolic/symbolic/symbolic.h" +#include "p4_symbolic/symbolic/values.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" + +namespace p4_symbolic { +namespace { + +TEST(EvaluateSaiPipeline, + SatisfiableForAllInstantiationsWithEmptyEntriesAndPorts) { + for (auto instantiation : sai::AllInstantiations()) { + 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(EvaluateSaiPipeline, FailsForInconsistentPortAndPortIdTypeTranslation) { + const auto config = sai::GetNonstandardForwardingPipelineConfig( + sai::Instantiation::kFabricBorderRouter, + sai::NonstandardPlatform::kP4Symbolic); + symbolic::StaticTranslationPerType 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)); +} + +TEST(EvaluateSaiPipeline, PassForConsistentPortAndPortIdTypeTranslation) { + const auto config = sai::GetNonstandardForwardingPipelineConfig( + sai::Instantiation::kFabricBorderRouter, + sai::NonstandardPlatform::kP4Symbolic); + symbolic::StaticTranslationPerType 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); +} + +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())); + + // 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::PdTableEntryToPi(ir_p4info, pd_entry)); + } + + // Evaluate the SAI pipeline. + symbolic::StaticTranslationPerType 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()); + + // 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"))); +} + +} // namespace +} // namespace p4_symbolic diff --git a/p4_symbolic/symbolic/symbolic.cc b/p4_symbolic/symbolic/symbolic.cc index 03df3933..f4f912c8 100644 --- a/p4_symbolic/symbolic/symbolic.cc +++ b/p4_symbolic/symbolic/symbolic.cc @@ -14,15 +14,19 @@ #include "p4_symbolic/symbolic/symbolic.h" +#include #include #include "absl/cleanup/cleanup.h" +#include "absl/status/status.h" +#include "absl/strings/substitute.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/util.h" +#include "p4_symbolic/symbolic/values.h" #include "p4_symbolic/z3_util.h" namespace p4_symbolic { @@ -48,8 +52,37 @@ absl::StatusOr GotCloned(const SymbolicPerPacketState &state) { return state.Get(std::string(kGotClonedPseudoField)); } +absl::Status CheckPhysicalPortsConformanceToV1Model( + const std::vector &physical_ports) { + for (const int port : physical_ports) { + if (port == kDropPort) { + return gutil::InvalidArgumentErrorBuilder() + << "cannot use physical port " << kDropPort + << " as p4-symbolic reserves it to encode dropping a packet; see " + "the documentation of `mark_to_drop` in v1mode1.p4 for details"; + } + if (port < 0 || port >= 512) { + return absl::InvalidArgumentError(absl::Substitute( + "Cannot use the value $0 as a physical port as the value does not " + "fit into PortId_t (bit<9>), the type of " + "standard_metadata.{ingress/egress}_port in v1model.p4", + port)); + } + } + + return absl::OkStatus(); +} + absl::StatusOr> EvaluateP4Pipeline( - const Dataplane &data_plane, const std::vector &physical_ports) { + const Dataplane &data_plane, const std::vector &physical_ports, + const StaticTranslationPerType &translation_per_type) { + // Check input physical ports. + if (absl::Status status = + CheckPhysicalPortsConformanceToV1Model(physical_ports); + !status.ok()) { + return status; + } + // Use global context to define a solver. std::unique_ptr z3_solver = std::make_unique(Z3Context()); @@ -57,6 +90,12 @@ absl::StatusOr> EvaluateP4Pipeline( // Initially, the p4runtime translator has empty state. values::P4RuntimeTranslator translator; + // Initiate the p4runtime translator with statically translated types. + for (const auto &[type, translation] : translation_per_type) { + translator.p4runtime_translation_allocators.emplace( + type, values::IdAllocator(translation)); + } + // "Accumulator"-style p4 program headers. // This is used to evaluate the P4 program. // Initially free/unconstrained and contains symbolic variables for @@ -71,6 +110,25 @@ absl::StatusOr> EvaluateP4Pipeline( SymbolicTableMatches matched_entries, control::EvaluateV1model(data_plane, &egress_headers, &translator)); + // Restrict the value of all fields with (purely static, i.e. + // dynamic_translation = false) P4RT translated types to what has been used in + // StaticTranslationPerType. This should be done after the symbolic execution + // since P4Symbolic does not initially know which fields have translated + // types. + for (const auto &[field, type] : translator.fields_p4runtime_type) { + if (auto it = translation_per_type.find(type); + it != translation_per_type.end() && !it->second.dynamic_translation) { + ASSIGN_OR_RETURN(z3::expr field_expr, ingress_headers.Get(field)); + z3::expr constraint = Z3Context().bool_val(false); + for (const auto &[string_value, numeric_value] : + it->second.static_mapping) { + constraint = + constraint || (field_expr == static_cast(numeric_value)); + } + z3_solver->add(constraint); + } + } + // Alias the event that the packet is dropped for ease of use in assertions ASSIGN_OR_RETURN(z3::expr dropped, IsDropped(egress_headers)); ASSIGN_OR_RETURN(z3::expr got_cloned, GotCloned(egress_headers)); diff --git a/p4_symbolic/symbolic/symbolic.h b/p4_symbolic/symbolic/symbolic.h index 2ecf3b72..25b773b3 100644 --- a/p4_symbolic/symbolic/symbolic.h +++ b/p4_symbolic/symbolic/symbolic.h @@ -24,7 +24,6 @@ #include #include -#include "absl/container/btree_map.h" #include "absl/strings/str_cat.h" #include "absl/strings/string_view.h" #include "gutil/status.h" @@ -208,11 +207,23 @@ struct SolverState { // } using Assertion = std::function; +// User provided TranslationData for P4 types. This is a partial +// map. For any P4 type included in this map, the statically provided +// TranslationData is used. For other types, if runtime translated (i.e. have +// @p4runtime_translation("", string) annotation), +// TranslationData{.static_mapping = {}, .dynamic_translation = true} is used. +using StaticTranslationPerType = + absl::btree_map; + // Symbolically evaluates/interprets the given program against the given // entries for every table in that program, and the available physical ports -// on the switch. +// 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> EvaluateP4Pipeline( - const Dataplane &data_plane, const std::vector &physical_ports); + const Dataplane &data_plane, const std::vector &physical_ports = {}, + const StaticTranslationPerType &translation_per_type = {}); // Finds a concrete packet and flow in the program that satisfies the given // assertion and meets the structure constrained by solver_state. diff --git a/p4_symbolic/symbolic/values.cc b/p4_symbolic/symbolic/values.cc index 69e2131b..bfdf6666 100644 --- a/p4_symbolic/symbolic/values.cc +++ b/p4_symbolic/symbolic/values.cc @@ -34,6 +34,7 @@ #include "absl/strings/strip.h" #include "absl/strings/substitute.h" #include "gmpxx.h" +#include "gutil/status.h" #include "p4_pdpi/ir.pb.h" #include "p4_pdpi/netaddr/ipv4_address.h" #include "p4_pdpi/netaddr/ipv6_address.h" @@ -89,10 +90,18 @@ absl::StatusOr FormatP4RTValue(const std::string &field_name, // Must translate the string into a bitvector according to the field type. const std::string &string_value = value.str(); + + // If there is no IdAllocator for the given type (implying no static + // mapping was provided), create a new dynamic IdAllocator. + translator->p4runtime_translation_allocators.try_emplace( + type_name, IdAllocator(TranslationData{ + .static_mapping = {}, + .dynamic_translation = true, + })); IdAllocator &allocator = - translator->p4runtime_translation_allocators[type_name]; - uint64_t int_value = allocator.AllocateId(string_value); + translator->p4runtime_translation_allocators.at(type_name); + ASSIGN_OR_RETURN(uint64_t int_value, allocator.AllocateId(string_value)); if (bitwidth == 0) { bitwidth = FindBitsize(int_value); } else { @@ -147,18 +156,39 @@ absl::StatusOr TranslateValueToP4RT( return p4rt_value; } -// IdAllocator Implementation. +IdAllocator::IdAllocator(const TranslationData &translation_data) + : translation_data_(translation_data) { + for (const auto &[string_value, id] : translation_data_.static_mapping) { + string_to_id_map_[string_value] = id; + id_to_string_map_[id] = string_value; + } +} -uint64_t IdAllocator::AllocateId(const std::string &string_value) { +absl::StatusOr IdAllocator::AllocateId( + const std::string &string_value) { // If previously allocated, return the same bitvector value. if (this->string_to_id_map_.count(string_value)) { return this->string_to_id_map_.at(string_value); } - // Allocate new bitvector value and store it in mapping. - uint64_t int_value = this->counter_++; - this->string_to_id_map_.insert({string_value, int_value}); - this->id_to_string_map_.insert({int_value, string_value}); - return int_value; + + if (translation_data_.dynamic_translation) { + // If dynamic allocation is enabled, allocate new bitvector value and store + // it in mapping. + + // Get the next unused ID value. + while (id_to_string_map_.find(next_id_) != id_to_string_map_.end()) { + ++next_id_; + } + + // Allocate it for the string value. + string_to_id_map_[string_value] = next_id_; + id_to_string_map_[next_id_] = string_value; + return next_id_; + } else { + return absl::InvalidArgumentError( + absl::StrCat("Cannot translate string value '", string_value, + "' to a bitvector with the given static mapping.")); + } } absl::StatusOr IdAllocator::IdToString(uint64_t value) const { @@ -168,8 +198,8 @@ absl::StatusOr IdAllocator::IdToString(uint64_t value) const { } // Could not find the bitvector in reverse map! - return absl::InvalidArgumentError( - absl::StrCat("Cannot translate bitvector ", value, " to a string value")); + return absl::InvalidArgumentError(absl::StrCat( + "Cannot translate bitvector '", value, "' to a string value.")); } } // namespace values diff --git a/p4_symbolic/symbolic/values.h b/p4_symbolic/symbolic/values.h index 857dbf40..d064fdd9 100644 --- a/p4_symbolic/symbolic/values.h +++ b/p4_symbolic/symbolic/values.h @@ -34,6 +34,19 @@ namespace p4_symbolic { namespace symbolic { namespace values { +// Translation data for a certain (P4RT translated) P4 type. +struct TranslationData { + // Static mapping between string values and ids. + std::vector> static_mapping; + // Indicates if the allocator should dynamically assign new Ids to new string + // values (i.e. values not present in the static mapping). + // Note: If a translation is purely static (i.e. dynamic_translation = false), + // the domain of the possible values for any variable with that type is + // restricted to to values static_mapping (see symbolic.cc). In the future, we + // might want to add a parameter to make this configurable by the user. + bool dynamic_translation = false; +}; + // This class is responsible for translating string values into consistent // numberic ids, that can then be used to create bitvector values to use in // z3. @@ -41,10 +54,16 @@ namespace values { // their corresponding string value. class IdAllocator { public: - // Allocates an arbitrary integer id to this string identifier. - // The Id is guaranteed to be consistent (the same bitvector is - // allocated to equal strings), and unique per instance of this class. - uint64_t AllocateId(const std::string &string_value); + IdAllocator(const TranslationData &translation_data); + + // Allocates an integer ID to this string identifier. If a static mapping is + // provided, the value from that mapping is used. If there is no static + // mapping for the string value and dynamic allocation is enabled, an + // arbitrary ID is used. Otherwise, returns an error. In case of dynamic + // allocation, the chosen ID is guaranteed to be consistent (the same + // bitvector is allocated to equal strings), and unique per instance of this + // class. + absl::StatusOr AllocateId(const std::string &string_value); // Reverse translation of an allocated bit vector to the string value for // which it was allocated. @@ -57,8 +76,9 @@ class IdAllocator { // A mapping from bitvector values to string values. std::unordered_map id_to_string_map_; - // Counter used to come up with new values per new allocation. - uint64_t counter_ = 0; + TranslationData translation_data_; + // Used to come up with new values per new allocation. + uint64_t next_id_ = 0; }; // This struct stores all the state that is required to translate string values diff --git a/p4_symbolic/symbolic/values_test.cc b/p4_symbolic/symbolic/values_test.cc index 0d3e2e86..e1ab49ac 100644 --- a/p4_symbolic/symbolic/values_test.cc +++ b/p4_symbolic/symbolic/values_test.cc @@ -94,5 +94,59 @@ TEST(FormatP4RTValue, FailsForStringWithNonZeroBitwidth) { StatusIs(absl::StatusCode::kInvalidArgument)); } +constexpr char kDummyString1[] = "a"; +constexpr char kDummyString2[] = "b"; +constexpr int kDummyId1 = 10; + +TEST(IdAllocatorTest, AssignedIdsAreUnique) { + IdAllocator allocator(TranslationData{.dynamic_translation = true}); + ASSERT_OK_AND_ASSIGN(const uint64_t id_1, + allocator.AllocateId(kDummyString1)); + ASSERT_OK_AND_ASSIGN(const uint64_t id_2, + allocator.AllocateId(kDummyString2)); + ASSERT_NE(id_1, id_2); +} + +TEST(IdAllocatorTest, ReverseTranslationYieldsOriginalString) { + IdAllocator allocator(TranslationData{.dynamic_translation = true}); + ASSERT_OK_AND_ASSIGN(const uint64_t id_1, + allocator.AllocateId(kDummyString1)); + ASSERT_OK_AND_ASSIGN(const std::string string_1, allocator.IdToString(id_1)); + ASSERT_EQ(string_1, kDummyString1); +} + +TEST(IdAllocatorTest, StaticMappingWorksForExistingString) { + IdAllocator allocator(TranslationData{ + .static_mapping = {{kDummyString1, kDummyId1}}, + .dynamic_translation = true, + }); + ASSERT_OK_AND_ASSIGN(const std::string string_1, + allocator.IdToString(kDummyId1)); + ASSERT_EQ(string_1, kDummyString1); + ASSERT_OK_AND_ASSIGN(const uint64_t id, allocator.AllocateId(kDummyString1)); + ASSERT_EQ(id, kDummyId1); +} + +TEST(IdAllocatorTest, StaticMappingWithDynamicAllocationWorksForNewString) { + IdAllocator allocator(TranslationData{ + .static_mapping = {{kDummyString1, kDummyId1}}, + .dynamic_translation = true, + }); + ASSERT_OK_AND_ASSIGN(const uint64_t id_2, + allocator.AllocateId(kDummyString2)); + ASSERT_NE(id_2, kDummyId1); + ASSERT_OK_AND_ASSIGN(const std::string string_2, allocator.IdToString(id_2)); + ASSERT_EQ(string_2, kDummyString2); +} + +TEST(IdAllocatorTest, StaticMappingWithoutDynamicAllocationFailForNewString) { + IdAllocator allocator(TranslationData{ + .static_mapping = {{kDummyString1, kDummyId1}}, + .dynamic_translation = false, + }); + ASSERT_THAT(allocator.AllocateId(kDummyString2), + gutil::StatusIs(absl::StatusCode::kInvalidArgument)); +} + } // namespace } // namespace p4_symbolic::symbolic::values