[P4_Symbolic] Extend reverse P4Runtime translation for symbolic entri…

…es. Remove unneeded function.

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",

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

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",

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});
   }
 

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",

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.

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 =

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);

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).

p4_symbolic/symbolic/values.cc

@@ -21,7 +21,9 @@
 #include "p4_symbolic/symbolic/values.h"
 
 #include <cstdint>
+#include <optional>
 #include <string>
+#include <utility>
 
 #include "absl/numeric/bits.h"
 #include "absl/status/status.h"
@@ -36,10 +38,7 @@
 #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"
-#include "p4_pdpi/netaddr/mac_address.h"
-#include "p4_pdpi/string_encodings/byte_string.h"
+#include "p4_pdpi/string_encodings/bit_string.h"
 #include "p4_pdpi/utils/ir.h"
 #include "p4_symbolic/symbolic/operators.h"
 #include "p4_symbolic/symbolic/symbolic.h"
@@ -61,17 +60,16 @@ absl::StatusOr<pdpi::IrValue> ParseIrValue(const std::string &value) {
   }
 }
 
-absl::StatusOr<z3::expr> FormatP4RTValue(const std::string &field_name,
-                                         const std::string &type_name,
-                                         const pdpi::IrValue &value,
-                                         int bitwidth, z3::context &context,
-                                         P4RuntimeTranslator &translator) {
+absl::StatusOr<z3::expr> FormatP4RTValue(
+    const pdpi::IrValue &value, const std::optional<std::string> &field_name,
+    const std::string &type_name, int bitwidth, z3::context &context,
+    P4RuntimeTranslator &translator) {
   switch (value.format_case()) {
     case pdpi::IrValue::kStr: {
       // Mark that this field is a string translatable field, and map it
       // to its custom type name (e.g. vrf_id => vrf_t).
-      if (!field_name.empty()) {
-        translator.fields_p4runtime_type[field_name] = type_name;
+      if (field_name.has_value() && !field_name->empty()) {
+        translator.fields_p4runtime_type[*field_name] = type_name;
       }
 
       // Must translate the string into a bitvector according to the field type.
@@ -99,10 +97,11 @@ absl::StatusOr<z3::expr> FormatP4RTValue(const std::string &field_name,
       return context.bv_val(int_value, bitwidth);
     }
     default: {
-      if (translator.fields_p4runtime_type.count(field_name)) {
+      if (field_name.has_value() &&
+          translator.fields_p4runtime_type.count(*field_name)) {
         return absl::InvalidArgumentError(absl::StrCat(
             "A table entry provides a non-string value ", value.DebugString(),
-            "to a string translated field", field_name));
+            "to a string translated field", *field_name));
       }
 
       // Rely on PDPI to convert the value since its logic is non-trivial and
@@ -120,27 +119,83 @@ absl::StatusOr<z3::expr> FormatP4RTValue(const std::string &field_name,
   }
 }
 
-absl::StatusOr<std::string> TranslateValueToP4RT(
-    const std::string &field_name, const std::string &value,
-    const P4RuntimeTranslator &translator) {
-  // Not translatable: identity function.
-  if (!translator.fields_p4runtime_type.count(field_name)) {
-    return value;
+absl::StatusOr<std::pair<std::string, bool>> TranslateZ3ValueStringToP4RT(
+    const std::string &value, const std::string &field_name,
+    const std::optional<std::string> &type_name,
+    const P4RuntimeTranslator &translator, std::optional<pdpi::Format> format) {
+  // Use `type_name` as the default field type.
+  std::string field_type;
+  if (type_name.has_value() && !type_name->empty()) field_type = *type_name;
+
+  // If `field_name` is found in the mapping to P4Runtime translated field
+  // types, use the field type based on the `field_name`.
+  if (auto it = translator.fields_p4runtime_type.find(field_name);
+      it != translator.fields_p4runtime_type.end()) {
+    field_type = it->second;
+  }
+
+  // Get the allocator based on the field type.
+  auto it = translator.p4runtime_translation_allocators.find(field_type);
+  if (it == translator.p4runtime_translation_allocators.end()) {
+    if (format.has_value() && *format == pdpi::Format::STRING) {
+      // With symbolic table entries, it is possible for a field type to not be
+      // registered in the translator. For such cases, we simply use the string
+      // representation of the numeric value. We can do this because from
+      // `FormatP4RTValue` we see that previously unknown field types are all
+      // translated dynamically. Therefore, as long as the mapping is bijective
+      // and consistent, things should be fine.
+      return std::make_pair(std::to_string(Z3ValueStringToInt(value)), true);
+    } else {
+      // Not translatable: identity function.
+      return std::make_pair(value, false);
+    }
   }
 
   // Translatable: do the reverse translation via the type name.
-  const std::string &field_type_name =
-      translator.fields_p4runtime_type.at(field_name);
-  const IdAllocator &allocator =
-      translator.p4runtime_translation_allocators.at(field_type_name);
+  const IdAllocator &allocator = it->second;
 
   // Turn the value from a string to an int.
   uint64_t int_value = Z3ValueStringToInt(value);
   ASSIGN_OR_RETURN(std::string p4rt_value, allocator.IdToString(int_value),
                    _.SetPrepend()
-                       << "failed to translate dataplane value of field '"
+                       << "Failed to translate dataplane value of field '"
                        << field_name << "' to P4Runtime representation: ");
-  return p4rt_value;
+  return std::make_pair(p4rt_value, true);
+}
+
+absl::StatusOr<pdpi::IrValue> TranslateZ3ValueStringToIrValue(
+    const std::string &value, int bitwidth, const std::string &field_name,
+    const std::string &type_name, const P4RuntimeTranslator &translator,
+    const pdpi::Format &format) {
+  ASSIGN_OR_RETURN(auto translated_value,
+                   values::TranslateZ3ValueStringToP4RT(
+                       value, field_name, type_name, translator, format));
+  const std::string &p4rt_value = translated_value.first;
+  bool translated = translated_value.second;
+  std::string byte_string;
+
+  if (translated) {
+    byte_string = p4rt_value;
+  } else {
+    pdpi::BitString bit_string;
+    int bitstring_width = bitwidth;
+    // Round up the bitwidth to the nearest multiple of 8 for converting to IR
+    // value via byte strings.
+    if (bitwidth % 8 != 0) {
+      bitstring_width += 8 - (bitwidth % 8);
+    }
+    RETURN_IF_ERROR(
+        AppendZ3ValueStringToBitString(bit_string, value, bitstring_width));
+    ASSIGN_OR_RETURN(byte_string, bit_string.ToByteString());
+  }
+
+  if (format == pdpi::Format::STRING) {
+    pdpi::IrValue ir_value;
+    ir_value.set_str(byte_string);
+    return ir_value;
+  }
+
+  return pdpi::ArbitraryByteStringToIrValue(format, bitwidth, byte_string);
 }
 
 IdAllocator::IdAllocator(const TranslationData &translation_data)
@@ -184,9 +239,17 @@ absl::StatusOr<std::string> IdAllocator::IdToString(uint64_t value) const {
     return this->id_to_string_map_.at(value);
   }
 
-  // Could not find the bitvector in reverse map!
-  return absl::InvalidArgumentError(absl::StrCat(
-      "Cannot translate bitvector '", value, "' to a string value."));
+  if (translation_data_.dynamic_translation) {
+    // With symbolic table entries, it is possible for a dynamically translated
+    // type to not have the mapping for a particular value, in which case we
+    // simply use the string representation of the numeric value.
+    return std::to_string(value);
+  } else {
+    // But for statically translated types (e.g., port_t), return an internal
+    // error if no mapping is found in the reverse map.
+    return gutil::InternalErrorBuilder()
+           << "Cannot translate bitvector '" << value << "' to a string value.";
+  }
 }
 
 }  // namespace values