[P4_Symbolic] Extend reverse P4Runtime translation for symbolic entri…

…es. Remove unneeded function. (sonic-net#954) * [P4-Symbolic] Create symbolic variables and add constraints for symbolic table entries. * [P4-Symbolic] Extend z3_util to evaluate bitvectors to unsigned integers. * [P4_Symbolic] Use absl numeric bit_width instead of custom implementation.Evaluate symbolic table entries with symbolic headers. * [P4_Symbolic] Extend reverse P4Runtime translation for symbolic entries. Remove unneeded function. --------- Co-authored-by: kishanps <[email protected]>
divyagayathri-hcl · Jan 22, 2025 · 484717e · 484717e
1 parent f9424a4
commit 484717e
Show file tree

Hide file tree

Showing 13 changed files with 186 additions and 111 deletions.
diff --git a/p4_symbolic/sai/BUILD.bazel b/p4_symbolic/sai/BUILD.bazel
@@ -24,6 +24,7 @@ cc_library(
     deps = [
         "//gutil:status",
         "//p4_symbolic/symbolic",
+        "@com_github_z3prover_z3//:api",
         "@com_google_absl//absl/container:flat_hash_set",
         "@com_google_absl//absl/status",
         "@com_google_absl//absl/status:statusor",

diff --git a/p4_symbolic/sai/sai.cc b/p4_symbolic/sai/sai.cc
@@ -14,21 +14,26 @@
 
 #include "p4_symbolic/sai/sai.h"
 
+#include <cstdint>
+#include <optional>
 #include <string>
 #include <type_traits>
 #include <unordered_set>
 #include <vector>
 
 #include "absl/container/flat_hash_set.h"
 #include "absl/status/status.h"
+#include "absl/status/statusor.h"
 #include "absl/strings/ascii.h"
 #include "absl/strings/match.h"
 #include "absl/strings/str_cat.h"
 #include "absl/strings/str_join.h"
 #include "absl/strings/string_view.h"
 #include "gutil/status.h"
+#include "p4_symbolic/symbolic/context.h"
 #include "p4_symbolic/symbolic/symbolic.h"
 #include "p4_symbolic/symbolic/values.h"
+#include "z3++.h"
 
 namespace p4_symbolic {
 
@@ -133,12 +138,14 @@ absl::StatusOr<std::string> GetLocalMetadataIngressPortFromModel(
   ASSIGN_OR_RETURN(
       z3::expr ingress_port_expr,
       solver_state.context.parsed_headers.Get(ingress_port_field_name));
-  return symbolic::values::TranslateValueToP4RT(
-      ingress_port_field_name,
-      solver_state.solver->get_model()
-          .eval(ingress_port_expr, true)
-          .to_string(),
-      solver_state.translator);
+  ASSIGN_OR_RETURN(auto translated_value,
+                   symbolic::values::TranslateZ3ValueStringToP4RT(
+                       solver_state.solver->get_model()
+                           .eval(ingress_port_expr, true)
+                           .to_string(),
+                       ingress_port_field_name,
+                       /*type_name=*/std::nullopt, solver_state.translator));
+  return translated_value.first;
 }
 
 }  // namespace p4_symbolic
diff --git a/p4_symbolic/symbolic/BUILD.bazel b/p4_symbolic/symbolic/BUILD.bazel
@@ -57,10 +57,7 @@ cc_library(
         "//gutil:status",
         "//p4_pdpi:ir_cc_proto",
         "//p4_pdpi/internal:ordered_map",
-        "//p4_pdpi/netaddr:ipv4_address",
-        "//p4_pdpi/netaddr:ipv6_address",
-        "//p4_pdpi/netaddr:mac_address",
-        "//p4_pdpi/string_encodings:byte_string",
+        "//p4_pdpi/string_encodings:bit_string",
         "//p4_pdpi/utils:ir",
         "//p4_symbolic:z3_util",
         "//p4_symbolic/ir",

diff --git a/p4_symbolic/symbolic/action.cc b/p4_symbolic/symbolic/action.cc
@@ -14,6 +14,7 @@
 
 #include "p4_symbolic/symbolic/action.h"
 
+#include <optional>
 #include <string>
 #include <vector>
 
@@ -346,10 +347,10 @@ absl::Status EvaluateConcreteAction(
                      gutil::FindPtrOrStatus(parameters, arg_name));
     ASSIGN_OR_RETURN(
         z3::expr parameter_value,
-        values::FormatP4RTValue(
-            /*field_name=*/"", param_definition->param().type_name().name(),
-            arg.value(), param_definition->param().bitwidth(),
-            *state.context.z3_context, state.translator));
+        values::FormatP4RTValue(arg.value(), /*field_name=*/std::nullopt,
+                                param_definition->param().type_name().name(),
+                                param_definition->param().bitwidth(),
+                                *state.context.z3_context, state.translator));
     context.scope.insert({param_definition->param().name(), parameter_value});
   }
 

diff --git a/p4_symbolic/symbolic/context.cc b/p4_symbolic/symbolic/context.cc
@@ -38,10 +38,6 @@ std::string ConcreteTrace::to_string() const {
   return result;
 }
 
-std::string ConcreteContext::to_string() const {
-  return to_string(/*verbose=*/false);
-}
-
 std::string ConcreteContext::to_string(bool verbose) const {
   auto result = absl::StrCat("ingress_port = ", ingress_port, "\n",
                              "egress_port = ", egress_port, "\n", "trace:\n",

diff --git a/p4_symbolic/symbolic/context.h b/p4_symbolic/symbolic/context.h
@@ -105,8 +105,7 @@ struct ConcreteContext {
   ConcretePerPacketState egress_headers;
   ConcreteTrace trace;  // Expected trace in the program.
 
-  std::string to_string() const;
-  std::string to_string(bool verbose) const;
+  std::string to_string(bool verbose = false) const;
 };
 
 // The symbolic context within our analysis.

diff --git a/p4_symbolic/symbolic/symbolic.cc b/p4_symbolic/symbolic/symbolic.cc
@@ -119,35 +119,6 @@ absl::Status InitializeTableEntries(SolverState &state,
     }
   }
 
-  // For each symbolic table entry object in each table, create respective
-  // symbolic variables and add corresponding constraints as Z3 assertions.
-  for (auto &[table_name, table_entries] : state.context.table_entries) {
-    ASSIGN_OR_RETURN(const ir::Table *table,
-                     GetIrTable(state.program, table_name));
-
-    for (TableEntry &entry : table_entries) {
-      // Skip concrete table entries.
-      if (entry.IsConcrete()) continue;
-
-      // Initialize the symbolic match fields of the current entry.
-      RETURN_IF_ERROR(InitializeSymbolicMatches(
-          entry, *table, state.program, *state.context.z3_context,
-          *state.solver, state.translator));
-
-      // Entries with symbolic action sets are not supported for now.
-      if (table->table_definition().has_action_profile_id()) {
-        return gutil::UnimplementedErrorBuilder()
-               << "Table entries with symbolic action sets are not supported "
-                  "at the moment.";
-      }
-
-      // Initialize the symbolic actions of the current entry.
-      RETURN_IF_ERROR(InitializeSymbolicActions(
-          entry, *table, state.program, *state.context.z3_context,
-          *state.solver, state.translator));
-    }
-  }
-
   return absl::OkStatus();
 }
 

diff --git a/p4_symbolic/symbolic/table.cc b/p4_symbolic/symbolic/table.cc
@@ -188,9 +188,9 @@ absl::StatusOr<z3::expr> EvaluateConcreteMatch(
   auto GetZ3Value =
       [&field_name, &pi_match,
        &state](const pdpi::IrValue &value) -> absl::StatusOr<z3::expr> {
-    return values::FormatP4RTValue(field_name, pi_match.type_name().name(),
-                                   value, pi_match.bitwidth(),
-                                   *state.context.z3_context, state.translator);
+    return values::FormatP4RTValue(
+        value, field_name, pi_match.type_name().name(), pi_match.bitwidth(),
+        *state.context.z3_context, state.translator);
   };
 
   absl::Status mismatch =

diff --git a/p4_symbolic/symbolic/table_entry.cc b/p4_symbolic/symbolic/table_entry.cc
@@ -71,7 +71,7 @@ absl::StatusOr<z3::expr> GetZ3Value(const pdpi::IrValue &value,
   const ir::FieldValue &matched_field = it->second;
   std::string field_name = absl::StrFormat("%s.%s", matched_field.header_name(),
                                            matched_field.field_name());
-  return values::FormatP4RTValue(field_name, match.type_name().name(), value,
+  return values::FormatP4RTValue(value, field_name, match.type_name().name(),
                                  match.bitwidth(), z3_context, translator);
 }
 
@@ -319,10 +319,10 @@ absl::Status AddConstraintsForConcretePartsOfSymbolicAction(
                                             param.name()));
     ASSIGN_OR_RETURN(
         z3::expr concrete_param_value,
-        values::FormatP4RTValue(
-            /*field_name=*/"", param_definition->param().type_name().name(),
-            param.value(), param_definition->param().bitwidth(), z3_context,
-            translator));
+        values::FormatP4RTValue(param.value(), /*field_name=*/std::nullopt,
+                                param_definition->param().type_name().name(),
+                                param_definition->param().bitwidth(),
+                                z3_context, translator));
     ASSIGN_OR_RETURN(z3::expr param_constraint,
                      operators::Eq(action_param, concrete_param_value));
     solver.add(param_constraint);

diff --git a/p4_symbolic/symbolic/util.cc b/p4_symbolic/symbolic/util.cc
@@ -16,7 +16,9 @@
 
 #include "p4_symbolic/symbolic/util.h"
 
+#include <optional>
 #include <string>
+#include <utility>
 #include <vector>
 
 #include "absl/container/btree_map.h"
@@ -128,21 +130,27 @@ absl::StatusOr<ConcreteContext> ExtractFromModel(
   // Extract the ingress, parsed, and egress headers.
   ConcretePerPacketState ingress_headers;
   for (const auto &[name, expr] : context.ingress_headers) {
-    ASSIGN_OR_RETURN(ingress_headers[name],
-                     values::TranslateValueToP4RT(
-                         name, model.eval(expr, true).to_string(), translator));
+    ASSIGN_OR_RETURN(auto translated_value,
+                     values::TranslateZ3ValueStringToP4RT(
+                         model.eval(expr, true).to_string(), name,
+                         /*type_name=*/std::nullopt, translator));
+    ingress_headers[name] = std::move(translated_value.first);
   }
   ConcretePerPacketState parsed_headers;
   for (const auto &[name, expr] : context.parsed_headers) {
-    ASSIGN_OR_RETURN(parsed_headers[name],
-                     values::TranslateValueToP4RT(
-                         name, model.eval(expr, true).to_string(), translator));
+    ASSIGN_OR_RETURN(auto translated_value,
+                     values::TranslateZ3ValueStringToP4RT(
+                         model.eval(expr, true).to_string(), name,
+                         /*type_name=*/std::nullopt, translator));
+    parsed_headers[name] = std::move(translated_value.first);
   }
   ConcretePerPacketState egress_headers;
   for (const auto &[name, expr] : context.egress_headers) {
-    ASSIGN_OR_RETURN(egress_headers[name],
-                     values::TranslateValueToP4RT(
-                         name, model.eval(expr, true).to_string(), translator));
+    ASSIGN_OR_RETURN(auto translated_value,
+                     values::TranslateZ3ValueStringToP4RT(
+                         model.eval(expr, true).to_string(), name,
+                         /*type_name=*/std::nullopt, translator));
+    egress_headers[name] = std::move(translated_value.first);
   }
 
   // Extract the trace (matches on every table).