From 355b72da92cbfd9f4a688f081c0af05aefff4912 Mon Sep 17 00:00:00 2001
From: kishanps <kishanps@google.com>
Date: Wed, 9 Aug 2023 00:48:11 -0700
Subject: [PATCH] [P4_Symbolic] Extend reverse P4Runtime translation for
symbolic entries. Remove unneeded function.
---
p4_symbolic/sai/BUILD.bazel | 1 +
p4_symbolic/sai/sai.cc | 19 +++--
p4_symbolic/symbolic/BUILD.bazel | 5 +-
p4_symbolic/symbolic/action.cc | 9 ++-
p4_symbolic/symbolic/context.cc | 4 -
p4_symbolic/symbolic/context.h | 3 +-
p4_symbolic/symbolic/table.cc | 6 +-
p4_symbolic/symbolic/table_entry.cc | 10 +--
p4_symbolic/symbolic/util.cc | 26 +++---
p4_symbolic/symbolic/values.cc | 119 +++++++++++++++++++++-------
p4_symbolic/symbolic/values.h | 47 +++++++++--
p4_symbolic/symbolic/values_test.cc | 19 ++---
12 files changed, 186 insertions(+), 82 deletions(-)
diff --git a/p4_symbolic/sai/BUILD.bazel b/p4_symbolic/sai/BUILD.bazel
index 118219ef..7fa2ddd4 100644
--- 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
index 85a410b2..37d85520 100644
--- a/p4_symbolic/sai/sai.cc
+++ b/p4_symbolic/sai/sai.cc
@@ -14,6 +14,8 @@
#include "p4_symbolic/sai/sai.h"
+#include <cstdint>
+#include <optional>
#include <string>
#include <type_traits>
#include <unordered_set>
@@ -21,14 +23,17 @@
#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
index 83b607f8..df9137da 100644
--- 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
index 2da1674c..7e6b369a 100644
--- 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
index 0459a1e4..90297c40 100644
--- 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
index 492bc8fc..c8083006 100644
--- 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/table.cc b/p4_symbolic/symbolic/table.cc
index 24817773..c254b962 100644
--- 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
index da0adc57..08c4494f 100644
--- 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
index 63c5ca70..702929eb 100644
--- 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).
diff --git a/p4_symbolic/symbolic/values.cc b/p4_symbolic/symbolic/values.cc
index 536ec002..35d6c566 100644
--- a/p4_symbolic/symbolic/values.cc
+++ b/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
diff --git a/p4_symbolic/symbolic/values.h b/p4_symbolic/symbolic/values.h
index 92f37549..b6f58bb2 100644
--- a/p4_symbolic/symbolic/values.h
+++ b/p4_symbolic/symbolic/values.h
@@ -22,6 +22,7 @@
#define P4_SYMBOLIC_SYMBOLIC_VALUES_H_
#include <cstdint>
+#include <optional>
#include <string>
#include <unordered_map>
#include <utility>
@@ -85,6 +86,8 @@ class IdAllocator {
// This struct stores all the state that is required to translate string values
// to internal bitvectors per custom p4 type (e.g. vrf_t), and reverse translate
// bitvector values of fields of such a custom type to a string value.
+// TODO: Consider simplifying the implementation of
+// P4RuntimeTranslator and the related functions.
struct P4RuntimeTranslator {
// Maps a type name to an allocator responsible for translating values for
// that type.
@@ -114,11 +117,15 @@ absl::StatusOr<pdpi::IrValue> ParseIrValue(const std::string &value);
// translated values (i.e. string IrValues) the bitwidth MUST be 0, in which
// case we use the minimum number of bits to encode the resulting translated
// 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);
+//
+// If `field_name` is provided (e.g., for entry field matches), it is used to
+// look up the type of the value from the field-to-type mapping in the
+// translator, which is then used for the actual translation. Otherwise (e.g.,
+// for action parameters), `type_name` is used instead.
+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);
// Reverse translation: operates opposite to FormatP4RTValue().
// If the given field was not detected to be translatable (perhaps it is indeed
@@ -127,9 +134,33 @@ absl::StatusOr<z3::expr> FormatP4RTValue(const std::string &field_name,
// were previously translated by a call to FormatP4RTValue), then the value
// is looked up using the reverse mapping inside the given translator, if that
// look fails, an absl error is returned.
-absl::StatusOr<std::string>
-TranslateValueToP4RT(const std::string &field_name, const std::string &value,
- const P4RuntimeTranslator &translator);
+// A boolean is also returned to indicate whether a translation took place.
+//
+// If `field_name` is provided (e.g., for entry field matches) and when
+// `type_name` is not provided or empty (e.g., for entry field matches that
+// match on locally defined variables), it is used to look up the type of the
+// value from the field-to-type mapping in the translator, which is then used
+// for the actual translation. Otherwise (e.g., for action parameters or entry
+// field matches that provide a type name), `type_name` is used instead.
+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 = std::nullopt);
+
+// Similar to `TranslateZ3ValueToP4RT` but additionally converts the translated
+// P4Runtime string representation to PDPI IR value.
+//
+// If `field_name` is provided (e.g., for entry field matches) and when
+// `type_name` is not provided or empty (e.g., for entry field matches that
+// match on locally defined variables), it is used to look up the type of the
+// value from the field-to-type mapping in the translator, which is then used
+// for the actual translation. Otherwise (e.g., for action parameters or entry
+// field matches that provide a type name), `type_name` is used instead.
+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);
} // namespace values
} // namespace symbolic
diff --git a/p4_symbolic/symbolic/values_test.cc b/p4_symbolic/symbolic/values_test.cc
index 4b1c9eeb..f43577a1 100644
--- a/p4_symbolic/symbolic/values_test.cc
+++ b/p4_symbolic/symbolic/values_test.cc
@@ -35,16 +35,17 @@ TEST(TranslateValueToP4RT, ReverseTranslatedValuesAreEqualToTheOriginalOnes) {
pdpi::IrValue ir_value;
ir_value.set_str(id);
ASSERT_OK_AND_ASSIGN(
- z3::expr expr, FormatP4RTValue(kFieldName, kFieldType, ir_value,
+ z3::expr expr, FormatP4RTValue(ir_value, kFieldName, kFieldType,
/*bitwidth=*/0, z3_context, translator));
z3_value_to_id[expr.to_string()] = id;
}
// Check that the reverse translation is as expected.
for (const auto& [z3_value, expected_id] : z3_value_to_id) {
- ASSERT_OK_AND_ASSIGN(
- const std::string actual_id,
- TranslateValueToP4RT(kFieldName, z3_value, translator));
+ ASSERT_OK_AND_ASSIGN(const auto translated_value,
+ TranslateZ3ValueStringToP4RT(z3_value, kFieldName,
+ kFieldType, translator));
+ const std::string& actual_id = translated_value.first;
ASSERT_THAT(actual_id, testing::Eq(expected_id));
}
}
@@ -58,7 +59,7 @@ TEST(FormatP4RTValue, WorksFor64BitIPv6) {
R"pb(ipv6: "0000:ffff:ffff:ffff::")pb"));
ASSERT_OK_AND_ASSIGN(
z3::expr z3_expr,
- FormatP4RTValue(kFieldName, kFieldType, ir_value,
+ FormatP4RTValue(ir_value, kFieldName, kFieldType,
/*bitwidth=*/64, z3_context, translator));
ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x0000'ffff'ffff'ffffULL);
}
@@ -70,7 +71,7 @@ TEST(FormatP4RTValue, WorksForIpv4) {
R"pb(ipv4: "127.0.0.1")pb"));
ASSERT_OK_AND_ASSIGN(
z3::expr z3_expr,
- FormatP4RTValue(kFieldName, kFieldType, ir_value,
+ FormatP4RTValue(ir_value, kFieldName, kFieldType,
/*bitwidth=*/32, z3_context, translator));
ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x7f000001);
}
@@ -82,7 +83,7 @@ TEST(FormatP4RTValue, WorksForMac) {
R"pb(mac: "01:02:03:04:05:06")pb"));
ASSERT_OK_AND_ASSIGN(
z3::expr z3_expr,
- FormatP4RTValue(kFieldName, kFieldType, ir_value,
+ FormatP4RTValue(ir_value, kFieldName, kFieldType,
/*bitwidth=*/48, z3_context, translator));
ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0x01'02'03'04'05'06ULL);
}
@@ -94,7 +95,7 @@ TEST(FormatP4RTValue, WorksForHexString) {
R"pb(hex_str: "0xabcd")pb"));
ASSERT_OK_AND_ASSIGN(
z3::expr z3_expr,
- FormatP4RTValue(kFieldName, kFieldType, ir_value,
+ FormatP4RTValue(ir_value, kFieldName, kFieldType,
/*bitwidth=*/16, z3_context, translator));
ASSERT_EQ(Z3ValueStringToInt(z3_expr.to_string()), 0xabcd);
}
@@ -104,7 +105,7 @@ TEST(FormatP4RTValue, FailsForStringWithNonZeroBitwidth) {
z3::context z3_context;
ASSERT_OK_AND_ASSIGN(auto ir_value, gutil::ParseTextProto<pdpi::IrValue>(
R"pb(str: "dummy_value")pb"));
- ASSERT_THAT(FormatP4RTValue(kFieldName, kFieldType, ir_value,
+ ASSERT_THAT(FormatP4RTValue(ir_value, kFieldName, kFieldType,
/*bitwidth=*/16, z3_context, translator),
StatusIs(absl::StatusCode::kInvalidArgument));
}