[P4_Symbolic] Extend z3_util to evaluate bitvectors to unsigned integers.

p4_symbolic/BUILD.bazel

@@ -50,8 +50,11 @@ cc_library(
         "//p4_pdpi/string_encodings:hex_string",
         "@com_github_z3prover_z3//:api",
         "@com_gnu_gmp//:gmp",
+        "@com_google_absl//absl/numeric:int128",
+        "@com_google_absl//absl/status",
         "@com_google_absl//absl/status:statusor",
         "@com_google_absl//absl/strings",
+        "@com_google_absl//absl/types:optional",
     ],
 )
 
@@ -116,6 +119,11 @@ cc_test(
     srcs = ["z3_util_test.cc"],
     deps = [
         ":z3_util",
+        "//gutil:status_matchers",
+        "//p4_pdpi/string_encodings:bit_string",
+        "@com_github_z3prover_z3//:api",
+        "@com_google_absl//absl/numeric:int128",
+        "@com_google_absl//absl/status",
         "@com_google_googletest//:gtest_main",
     ],
 )

p4_symbolic/z3_util.cc

@@ -14,12 +14,25 @@
 
 #include "p4_symbolic/z3_util.h"
 
+#include <cstddef>
+#include <cstdint>
+#include <string>
+
+#include "absl/numeric/int128.h"
+#include "absl/status/status.h"
 #include "absl/status/statusor.h"
+#include "absl/strings/match.h"
+#include "absl/strings/numbers.h"
+#include "absl/strings/str_cat.h"
+#include "absl/strings/string_view.h"
 #include "absl/strings/strip.h"
+#include "absl/types/optional.h"
 #include "gmpxx.h"
 #include "gutil/status.h"
+#include "p4_pdpi/string_encodings/bit_string.h"
 #include "p4_pdpi/string_encodings/hex_string.h"
 #include "z3++.h"
+#include "z3_api.h"
 
 namespace p4_symbolic {
 
@@ -113,25 +126,32 @@ absl::Status AppendHexCharStringToPDPIBitString(
 
 absl::StatusOr<bool> EvalZ3Bool(const z3::expr& bool_expr,
                                 const z3::model& model) {
-  // TODO: Ensure this doesn't crash by checking sort first.
-  auto value = model.eval(bool_expr, true).bool_value();
+  if (!bool_expr.is_bool()) {
+    return gutil::InvalidArgumentErrorBuilder()
+           << "Expected a boolean expression, found '" << bool_expr << "'";
+  }
+
+  auto value = model.eval(bool_expr, /*model_completion=*/true).bool_value();
   switch (value) {
     case Z3_L_FALSE:
       return false;
     case Z3_L_TRUE:
       return true;
     default:
-      break;
+      return gutil::InternalErrorBuilder()
+             << "boolean expression '" << bool_expr
+             << "' evaluated to unexpected Boolean value " << value;
   }
-  return gutil::InternalErrorBuilder()
-         << "boolean expression '" << bool_expr
-         << "' evaluated to unexpected Boolean value " << value;
 }
 
 absl::StatusOr<int> EvalZ3Int(const z3::expr& int_expr,
                               const z3::model& model) {
-  // TODO: Ensure this doesn't crash by checking sort first.
-  return model.eval(int_expr, true).get_numeral_int();
+  if (!int_expr.is_int()) {
+    return gutil::InvalidArgumentErrorBuilder()
+           << "Expected an integer expression, found '" << int_expr << "'";
+  }
+
+  return model.eval(int_expr, /*model_completion=*/true).get_numeral_int();
 }
 
 absl::Status EvalAndAppendZ3BitvectorToBitString(pdpi::BitString& output,
@@ -142,22 +162,73 @@ absl::Status EvalAndAppendZ3BitvectorToBitString(pdpi::BitString& output,
            << "Expected a bitvector, found '" << bv_expr << "'";
   }
 
-  const std::string field_value =
+  const std::string value =
+      model.eval(bv_expr, /*model_completion=*/true).to_string();
+  return AppendZ3ValueStringToBitString(output, value,
+                                        bv_expr.get_sort().bv_size());
+}
+
+absl::StatusOr<uint64_t> EvalZ3BitvectorToUInt64(const z3::expr& bv_expr,
+                                                 const z3::model& model) {
+  if (!bv_expr.is_bv()) {
+    return gutil::InvalidArgumentErrorBuilder()
+           << "Expected a bitvector, found '" << bv_expr << "'";
+  }
+
+  if (bv_expr.get_sort().bv_size() > 64) {
+    return gutil::InvalidArgumentErrorBuilder()
+           << "Expected a bitvector within 64 bits, found "
+           << bv_expr.get_sort().bv_size() << " bits";
+  }
+
+  const std::string value =
       model.eval(bv_expr, /*model_completion=*/true).to_string();
-  absl::string_view field_value_view = field_value;
-
-  if (absl::ConsumePrefix(&field_value_view, "#x")) {
-    RETURN_IF_ERROR(AppendHexCharStringToPDPIBitString(
-        output, field_value_view, bv_expr.get_sort().bv_size()));
-  } else if (absl::ConsumePrefix(&field_value_view, "#b")) {
-    RETURN_IF_ERROR(AppendBitCharStringToPDPIBitString(
-        output, field_value_view, bv_expr.get_sort().bv_size()));
+  return Z3ValueStringToInt(value);
+}
+
+absl::StatusOr<absl::uint128> EvalZ3BitvectorToUInt128(const z3::expr& bv_expr,
+                                                       const z3::model& model) {
+  if (!bv_expr.is_bv()) {
+    return gutil::InvalidArgumentErrorBuilder()
+           << "Expected a bitvector, found '" << bv_expr << "'";
+  }
+
+  if (bv_expr.get_sort().bv_size() > 128) {
+    return gutil::InvalidArgumentErrorBuilder()
+           << "Expected a bitvector within 128 bits, found "
+           << bv_expr.get_sort().bv_size() << " bits";
+  }
+
+  const std::string value_string =
+      model.eval(bv_expr, /*model_completion=*/true).to_string();
+  absl::string_view value = value_string;
+  absl::uint128 result;
+
+  if (absl::ConsumePrefix(&value, "#x")) {
+    if (!absl::SimpleHexAtoi(value, &result)) {
+      return gutil::InvalidArgumentErrorBuilder()
+             << "Unable to convert hex string '" << value << "' to uint128";
+    }
+  } else if (absl::ConsumePrefix(&value, "#b")) {
+    uint64_t hi = 0;
+    uint64_t lo = 0;
+
+    if (value.size() > 64) {
+      hi = std::stoull(std::string(value.substr(0, value.size() - 64)),
+                       /*idx=*/nullptr, /*base=*/2);
+      lo = std::stoull(std::string(value.substr(value.size() - 64)),
+                       /*idx=*/nullptr, /*base=*/2);
+    } else {
+      lo = std::stoull(std::string(value), /*idx=*/nullptr, /*base=*/2);
+    }
+
+    result = absl::MakeUint128(hi, lo);
   } else {
     return gutil::InvalidArgumentErrorBuilder()
-           << "Invalid Z3 bitvector value '" << field_value << "'";
+           << "Invalid Z3 bitvector value '" << value << "'";
   }
 
-  return absl::OkStatus();
+  return result;
 }
 
 absl::StatusOr<z3::expr> HexStringToZ3Bitvector(z3::context& context,
@@ -191,4 +262,21 @@ uint64_t Z3ValueStringToInt(const std::string& value) {
   }
 }
 
+absl::Status AppendZ3ValueStringToBitString(pdpi::BitString& result,
+                                            absl::string_view value,
+                                            size_t num_bits) {
+  if (absl::ConsumePrefix(&value, "#x")) {
+    RETURN_IF_ERROR(
+        AppendHexCharStringToPDPIBitString(result, value, num_bits));
+  } else if (absl::ConsumePrefix(&value, "#b")) {
+    RETURN_IF_ERROR(
+        AppendBitCharStringToPDPIBitString(result, value, num_bits));
+  } else {
+    return gutil::InvalidArgumentErrorBuilder()
+           << "Invalid Z3 bitvector value '" << value << "'";
+  }
+
+  return absl::OkStatus();
+}
+
 }  // namespace p4_symbolic

p4_symbolic/z3_util.h

@@ -14,23 +14,52 @@
 #ifndef PINS_P4_SYMBOLIC_Z3_UTIL_H_
 #define PINS_P4_SYMBOLIC_Z3_UTIL_H_
 
+#include <cstddef>
+#include <cstdint>
+#include <string>
+
+#include "absl/numeric/int128.h"
+#include "absl/status/status.h"
 #include "absl/status/statusor.h"
+#include "absl/strings/string_view.h"
+#include "absl/types/optional.h"
 #include "p4_pdpi/string_encodings/bit_string.h"
 #include "z3++.h"
 
 namespace p4_symbolic {
 
 // -- Evaluation ---------------------------------------------------------------
 
-absl::StatusOr<bool> EvalZ3Bool(const z3::expr &bool_expr,
-                                const z3::model &model);
+// Evaluates the given `bool_expr` to a boolean value based on the given
+// `model`. Returns an error if the given expression is not a boolean
+// expression.
+absl::StatusOr<bool> EvalZ3Bool(const z3::expr& bool_expr,
+                                const z3::model& model);
 
-absl::StatusOr<int> EvalZ3Int(const z3::expr &int_expr, const z3::model &model);
+// Evaluates the given `int_expr` to an integer value based on the given
+// `model`. Returns an error if the given expression is not an integer
+// expression.
+absl::StatusOr<int> EvalZ3Int(const z3::expr& int_expr, const z3::model& model);
 
+// Evaluates the given `bv_expr` bit-vector and appends the value to the
+// `output` bit-string based on the given `model`. Returns an error if the given
+// expression is not a bit-vector.
 absl::Status EvalAndAppendZ3BitvectorToBitString(pdpi::BitString& output,
                                                  const z3::expr& bv_expr,
                                                  const z3::model& model);
 
+// Evaluates the given `bv_expr` bit-vector to uint64_t based on the given
+// `model`. Returns an error if the given expression is not a bit-vector or if
+// the size is over 64 bits.
+absl::StatusOr<uint64_t> EvalZ3BitvectorToUInt64(const z3::expr& bv_expr,
+                                                 const z3::model& model);
+
+// Evaluates the given `bv_expr` bit-vector to absl::uint128 based on the given
+// `model`. Returns an error if the given expression is not a bit-vector or if
+// the size is over 128 bits.
+absl::StatusOr<absl::uint128> EvalZ3BitvectorToUInt128(const z3::expr& bv_expr,
+                                                       const z3::model& model);
+
 // -- Constructing Z3 expressions ----------------------------------------------
 
 // Returns Z3 bitvector of the given `hex_string` value.
@@ -50,6 +79,14 @@ HexStringToZ3Bitvector(z3::context &context, const std::string &hex_string,
 // fits in uint64_t (otherwise an exception will be thrown).
 uint64_t Z3ValueStringToInt(const std::string &value);
 
+// Appends exactly `num_bits` bits to the `result` PDPI bit string from the
+// evaluated Z3 string `value`. Returns an error if the `value` is not a valid
+// Z3 bit-vector value (i.e., if it is not a hex string starting with "#x" and
+// not a binary bit string starting with "#b").
+absl::Status AppendZ3ValueStringToBitString(pdpi::BitString& result,
+                                            absl::string_view value,
+                                            size_t num_bits);
+
 // == END OF PUBLIC INTERFACE ==================================================
 
 }  // namespace p4_symbolic