[P4_Symbolic] Expose the ability to specify dynamically growing stati…

…c mapping for translated types to P4Symbolic's clients. (sonic-net#705)



Co-authored-by: kheradmandG <kheradmand@google.com>
Co-authored-by: kishanps <kishanps@google.com>

p4_symbolic/sai/sai.cc

@@ -44,7 +44,7 @@ absl::Status CheckPhysicalPortAndPortIdTypeValueConsistency(
   absl::flat_hash_set<uint64_t> 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);
   }
 

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 <memory>
+#include <vector>
+
+#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<std::unique_ptr<symbolic::SolverState>> 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<std::unique_ptr<symbolic::SolverState>> 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<sai::TableEntries>(
+      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<p4::v1::TableEntry> 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<std::unique_ptr<symbolic::SolverState>> 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

p4_symbolic/symbolic/symbolic.cc

@@ -14,15 +14,19 @@
 
 #include "p4_symbolic/symbolic/symbolic.h"
 
+#include <memory>
 #include <utility>
 
 #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,15 +52,50 @@ absl::StatusOr<z3::expr> GotCloned(const SymbolicPerPacketState &state) {
   return state.Get(std::string(kGotClonedPseudoField));
 }
 
+absl::Status CheckPhysicalPortsConformanceToV1Model(
+    const std::vector<int> &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<std::unique_ptr<SolverState>> EvaluateP4Pipeline(
-    const Dataplane &data_plane, const std::vector<int> &physical_ports) {
+    const Dataplane &data_plane, const std::vector<int> &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> z3_solver =
       std::make_unique<z3::solver>(Z3Context());
 
   // 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<std::unique_ptr<SolverState>> 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<int>(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));

p4_symbolic/symbolic/symbolic.h

@@ -24,7 +24,6 @@
 #include <utility>
 #include <vector>
 
-#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<z3::expr(const SymbolicContext &)>;
 
+// 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<std::string, values::TranslationData>;
+
 // 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<std::unique_ptr<SolverState>> EvaluateP4Pipeline(
-    const Dataplane &data_plane, const std::vector<int> &physical_ports);
+    const Dataplane &data_plane, const std::vector<int> &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.

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<z3::expr> 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<std::string> 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<uint64_t> 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<std::string> IdAllocator::IdToString(uint64_t value) const {
@@ -168,8 +198,8 @@ absl::StatusOr<std::string> 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