From b578509858176cc0cded8a7ae4408392952c13be Mon Sep 17 00:00:00 2001 From: kishanps Date: Wed, 9 Aug 2023 00:25:17 -0700 Subject: [PATCH] [P4-Symbolic] Extend z3_util to evaluate bitvectors to unsigned integers. --- p4_symbolic/BUILD.bazel | 8 ++ p4_symbolic/z3_util.cc | 126 ++++++++++++++--- p4_symbolic/z3_util.h | 43 +++++- p4_symbolic/z3_util_test.cc | 272 ++++++++++++++++++++++++++++++++++-- 4 files changed, 418 insertions(+), 31 deletions(-) diff --git a/p4_symbolic/BUILD.bazel b/p4_symbolic/BUILD.bazel index f4e62fae..8b502c83 100644 --- a/p4_symbolic/BUILD.bazel +++ b/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", ], ) diff --git a/p4_symbolic/z3_util.cc b/p4_symbolic/z3_util.cc index 1e5efdf5..aab9ed1e 100644 --- a/p4_symbolic/z3_util.cc +++ b/p4_symbolic/z3_util.cc @@ -14,12 +14,25 @@ #include "p4_symbolic/z3_util.h" +#include +#include +#include + +#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 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 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 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 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 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 diff --git a/p4_symbolic/z3_util.h b/p4_symbolic/z3_util.h index 17267ab1..59f682fc 100644 --- a/p4_symbolic/z3_util.h +++ b/p4_symbolic/z3_util.h @@ -14,7 +14,15 @@ #ifndef PINS_P4_SYMBOLIC_Z3_UTIL_H_ #define PINS_P4_SYMBOLIC_Z3_UTIL_H_ +#include +#include +#include + +#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" @@ -22,15 +30,36 @@ namespace p4_symbolic { // -- Evaluation --------------------------------------------------------------- -absl::StatusOr 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 EvalZ3Bool(const z3::expr& bool_expr, + const z3::model& model); -absl::StatusOr 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 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 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 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 diff --git a/p4_symbolic/z3_util_test.cc b/p4_symbolic/z3_util_test.cc index 88de5194..0e804a6a 100644 --- a/p4_symbolic/z3_util_test.cc +++ b/p4_symbolic/z3_util_test.cc @@ -1,30 +1,284 @@ #include "p4_symbolic/z3_util.h" +#include +#include +#include + +#include "absl/numeric/int128.h" +#include "absl/status/status.h" #include "gmock/gmock.h" #include "gtest/gtest.h" +#include "gutil/status_matchers.h" +#include "p4_pdpi/string_encodings/bit_string.h" +#include "z3++.h" namespace p4_symbolic { namespace { +using ::gutil::StatusIs; + +TEST(EvalZ3Bool, CheckEvalZ3Bool) { + z3::context ctx; + z3::solver solver(ctx); + + // Construct expressions. + z3::expr expr1 = ctx.bool_val(true); + z3::expr expr2 = ctx.bool_val(false); + z3::expr expr3 = ctx.bool_val(true) && ctx.bool_val(false); + z3::expr expr4 = ctx.bool_val(true) || ctx.bool_val(false); + z3::expr expr5 = ctx.int_val(0); + z3::expr expr6 = ctx.bv_val(1, 1); + + z3::check_result check_result = solver.check(); + ASSERT_EQ(check_result, z3::sat); + z3::model model = solver.get_model(); + + // Check for evaluated values. + ASSERT_OK_AND_ASSIGN(bool ans1, EvalZ3Bool(expr1, model)); + EXPECT_TRUE(ans1); + ASSERT_OK_AND_ASSIGN(bool ans2, EvalZ3Bool(expr2, model)); + EXPECT_FALSE(ans2); + ASSERT_OK_AND_ASSIGN(bool ans3, EvalZ3Bool(expr3, model)); + EXPECT_FALSE(ans3); + ASSERT_OK_AND_ASSIGN(bool ans4, EvalZ3Bool(expr4, model)); + EXPECT_TRUE(ans4); + EXPECT_THAT(EvalZ3Bool(expr5, model), + StatusIs(absl::StatusCode::kInvalidArgument)); + EXPECT_THAT(EvalZ3Bool(expr6, model), + StatusIs(absl::StatusCode::kInvalidArgument)); +} + +TEST(EvalZ3Int, CheckEvalZ3Int) { + z3::context ctx; + z3::solver solver(ctx); + + // Construct expressions. + z3::expr expr1 = ctx.int_val(0); + z3::expr expr2 = ctx.int_val(1); + z3::expr expr3 = ctx.int_val(1000); + z3::expr expr4 = ctx.int_val(1) + ctx.int_val(-1); + z3::expr expr5 = ctx.int_val(1) - ctx.int_val(1); + z3::expr expr6 = ctx.bv_val(1, 1); + + z3::check_result check_result = solver.check(); + ASSERT_EQ(check_result, z3::sat); + z3::model model = solver.get_model(); + + // Check for evaluated values. + ASSERT_OK_AND_ASSIGN(int ans1, EvalZ3Int(expr1, model)); + EXPECT_EQ(ans1, 0); + ASSERT_OK_AND_ASSIGN(int ans2, EvalZ3Int(expr2, model)); + EXPECT_EQ(ans2, 1); + ASSERT_OK_AND_ASSIGN(int ans3, EvalZ3Int(expr3, model)); + EXPECT_EQ(ans3, 1000); + ASSERT_OK_AND_ASSIGN(int ans4, EvalZ3Int(expr4, model)); + EXPECT_EQ(ans4, 0); + ASSERT_OK_AND_ASSIGN(int ans5, EvalZ3Int(expr5, model)); + EXPECT_EQ(ans5, 0); + EXPECT_THAT(EvalZ3Int(expr6, model), + StatusIs(absl::StatusCode::kInvalidArgument)); +} + +TEST(EvalAndAppendZ3BitvectorToBitString, + CheckEvalAndAppendZ3BitvectorToBitString) { + z3::context ctx; + z3::solver solver(ctx); + + // Construct expressions. + z3::expr expr1 = ctx.bv_val(0, 1); + z3::expr expr2 = ctx.bv_val(0, 4); + z3::expr expr3 = ctx.bv_val(0, 7); + z3::expr expr4 = ctx.int_val(1); + + z3::check_result check_result = solver.check(); + ASSERT_EQ(check_result, z3::sat); + z3::model model = solver.get_model(); + + // Check for evaluated values. + pdpi::BitString ans1, ans2, ans3, ans4; + ASSERT_OK(EvalAndAppendZ3BitvectorToBitString(ans1, expr1, model)); + ASSERT_OK(EvalAndAppendZ3BitvectorToBitString(ans2, expr2, model)); + ASSERT_OK(EvalAndAppendZ3BitvectorToBitString(ans3, expr3, model)); + EXPECT_THAT(EvalAndAppendZ3BitvectorToBitString(ans4, expr4, model), + StatusIs(absl::StatusCode::kInvalidArgument)); + EXPECT_EQ(ans1.size(), 1); + ASSERT_OK_AND_ASSIGN(std::bitset<1> bit, ans1.ConsumeBitset<1>()); + EXPECT_FALSE(bit.test(0)); + ASSERT_OK_AND_ASSIGN(std::string hex2, ans2.ToHexString()); + EXPECT_EQ(hex2, "0x0"); + ASSERT_OK_AND_ASSIGN(std::string hex3, ans3.ToHexString()); + EXPECT_EQ(hex3, "0x00"); +} + +TEST(EvalZ3BitvectorToUInt, CheckEvalZ3BitvectorToUInt) { + z3::context ctx; + z3::solver solver(ctx); + + // Construct expressions. + z3::expr expr1 = ctx.int_val(0); + z3::expr expr2 = ctx.bv_val(0, 65); + z3::expr expr3 = ctx.bv_val(0, 64); + z3::expr expr4 = ctx.bv_val(42, 8); + + z3::check_result check_result = solver.check(); + ASSERT_EQ(check_result, z3::sat); + z3::model model = solver.get_model(); + + // Check for evaluated values. + EXPECT_THAT(EvalZ3BitvectorToUInt64(expr1, model), + StatusIs(absl::StatusCode::kInvalidArgument)); + EXPECT_THAT(EvalZ3BitvectorToUInt64(expr2, model), + StatusIs(absl::StatusCode::kInvalidArgument)); + ASSERT_OK_AND_ASSIGN(uint64_t ans3, EvalZ3BitvectorToUInt64(expr3, model)); + EXPECT_EQ(ans3, 0); + ASSERT_OK_AND_ASSIGN(uint64_t ans4, EvalZ3BitvectorToUInt64(expr4, model)); + EXPECT_EQ(ans4, 42); +} + +TEST(EvalZ3BitvectorToUInt128, CheckEvalZ3BitvectorToUInt128) { + z3::context ctx; + z3::solver solver(ctx); + + // Construct expressions. + z3::expr expr1 = ctx.int_val(0); + z3::expr expr2 = ctx.bv_val(0, 129); + z3::expr expr3 = ctx.bv_val(0, 128); + z3::expr expr4 = ctx.bv_val(42, 32); + z3::expr expr5 = ctx.bv_val(42, 31); + z3::expr expr6 = z3::shl(ctx.bv_val(1, 65), 64); + + z3::check_result check_result = solver.check(); + ASSERT_EQ(check_result, z3::sat); + z3::model model = solver.get_model(); + + // Check for evaluated values. + EXPECT_THAT(EvalZ3BitvectorToUInt128(expr1, model), + StatusIs(absl::StatusCode::kInvalidArgument)); + EXPECT_THAT(EvalZ3BitvectorToUInt128(expr2, model), + StatusIs(absl::StatusCode::kInvalidArgument)); + ASSERT_OK_AND_ASSIGN(absl::uint128 ans3, + EvalZ3BitvectorToUInt128(expr3, model)); + EXPECT_EQ(ans3, absl::MakeUint128(0, 0)); + ASSERT_OK_AND_ASSIGN(absl::uint128 ans4, + EvalZ3BitvectorToUInt128(expr4, model)); + EXPECT_EQ(ans4, absl::MakeUint128(0, 42)); + ASSERT_OK_AND_ASSIGN(absl::uint128 ans5, + EvalZ3BitvectorToUInt128(expr5, model)); + EXPECT_EQ(ans5, absl::MakeUint128(0, 42)); + ASSERT_OK_AND_ASSIGN(absl::uint128 ans6, + EvalZ3BitvectorToUInt128(expr6, model)); + EXPECT_EQ(ans6, absl::MakeUint128(1, 0)); +} + +TEST(HexStringToZ3Bitvector, HexStringWithoutBitWidth) { + z3::context ctx; + z3::solver solver(ctx); + + // Construct expressions. + ASSERT_OK_AND_ASSIGN(z3::expr bv1, HexStringToZ3Bitvector(ctx, "0x0001")); + ASSERT_OK_AND_ASSIGN(z3::expr bv2, HexStringToZ3Bitvector(ctx, "0xdead")); + + z3::check_result check_result = solver.check(); + ASSERT_EQ(check_result, z3::sat); + z3::model model = solver.get_model(); + + // Check for expressions. + ASSERT_TRUE(bv1.is_bv()); + ASSERT_TRUE(bv2.is_bv()); + EXPECT_EQ(bv1.get_sort().bv_size(), 1); + EXPECT_EQ(bv2.get_sort().bv_size(), 16); + ASSERT_OK_AND_ASSIGN(uint64_t ans1, EvalZ3BitvectorToUInt64(bv1, model)); + ASSERT_OK_AND_ASSIGN(uint64_t ans2, EvalZ3BitvectorToUInt64(bv2, model)); + EXPECT_EQ(ans1, 1); + EXPECT_EQ(ans2, 0xdead); +} + +TEST(HexStringToZ3Bitvector, HexStringWithBitWidth) { + z3::context ctx; + z3::solver solver(ctx); + + // Construct expressions. + ASSERT_OK_AND_ASSIGN(z3::expr bv1, HexStringToZ3Bitvector(ctx, "0x0001", 16)); + ASSERT_OK_AND_ASSIGN(z3::expr bv2, HexStringToZ3Bitvector(ctx, "0xdead", 17)); + + z3::check_result check_result = solver.check(); + ASSERT_EQ(check_result, z3::sat); + z3::model model = solver.get_model(); + + // Check for expressions. + ASSERT_TRUE(bv1.is_bv()); + ASSERT_TRUE(bv2.is_bv()); + EXPECT_EQ(bv1.get_sort().bv_size(), 16); + EXPECT_EQ(bv2.get_sort().bv_size(), 17); + ASSERT_OK_AND_ASSIGN(uint64_t ans1, EvalZ3BitvectorToUInt64(bv1, model)); + ASSERT_OK_AND_ASSIGN(uint64_t ans2, EvalZ3BitvectorToUInt64(bv2, model)); + EXPECT_EQ(ans1, 1); + EXPECT_EQ(ans2, 0xdead); +} + +TEST(HexStringToZ3Bitvector, HexStringWithBitWidthThatIsTooShort) { + z3::context ctx; + z3::solver solver(ctx); + + // Construct expressions. + ASSERT_OK_AND_ASSIGN(z3::expr bv1, HexStringToZ3Bitvector(ctx, "0xdead", 8)); + ASSERT_OK_AND_ASSIGN(z3::expr bv2, HexStringToZ3Bitvector(ctx, "0xbeef", 4)); + + z3::check_result check_result = solver.check(); + ASSERT_EQ(check_result, z3::sat); + z3::model model = solver.get_model(); + + // Check for expressions. + ASSERT_TRUE(bv1.is_bv()); + ASSERT_TRUE(bv2.is_bv()); + EXPECT_EQ(bv1.get_sort().bv_size(), 8); + EXPECT_EQ(bv2.get_sort().bv_size(), 4); + ASSERT_OK_AND_ASSIGN(uint64_t ans1, EvalZ3BitvectorToUInt64(bv1, model)); + ASSERT_OK_AND_ASSIGN(uint64_t ans2, EvalZ3BitvectorToUInt64(bv2, model)); + EXPECT_EQ(ans1, 0xad); + EXPECT_EQ(ans2, 0xf); +} + TEST(Z3ValueStringToInt, WorksForBoolStrings) { - ASSERT_EQ(Z3ValueStringToInt("true"), 1); - ASSERT_EQ(Z3ValueStringToInt("false"), 0); + EXPECT_EQ(Z3ValueStringToInt("true"), 1); + EXPECT_EQ(Z3ValueStringToInt("false"), 0); } TEST(Z3ValueStringToInt, WorksForBinaryStrings) { - ASSERT_EQ(Z3ValueStringToInt("#b10"), 2); - ASSERT_EQ(Z3ValueStringToInt("#b01"), 1); + EXPECT_EQ(Z3ValueStringToInt("#b10"), 2); + EXPECT_EQ(Z3ValueStringToInt("#b01"), 1); } TEST(Z3ValueStringToInt, WorksForHexStrings) { - ASSERT_EQ(Z3ValueStringToInt("#x10"), 16); - ASSERT_EQ(Z3ValueStringToInt("#xff"), 255); - ASSERT_EQ(Z3ValueStringToInt("#x9"), 9); + EXPECT_EQ(Z3ValueStringToInt("#x10"), 16); + EXPECT_EQ(Z3ValueStringToInt("#xff"), 255); + EXPECT_EQ(Z3ValueStringToInt("#x9"), 9); } TEST(Z3ValueStringToInt, WorksForDecimalStrings) { - ASSERT_EQ(Z3ValueStringToInt("10"), 10); - ASSERT_EQ(Z3ValueStringToInt("900"), 900); + EXPECT_EQ(Z3ValueStringToInt("10"), 10); + EXPECT_EQ(Z3ValueStringToInt("900"), 900); +} + +TEST(AppendZ3ValueStringToBitString, InvalidZ3BitvectorValue) { + pdpi::BitString bit_string; + EXPECT_THAT(AppendZ3ValueStringToBitString(bit_string, "9527", 16), + StatusIs(absl::StatusCode::kInvalidArgument)); +} + +TEST(AppendZ3ValueStringToBitString, HexStringBitvector) { + pdpi::BitString bit_string; + ASSERT_OK(AppendZ3ValueStringToBitString(bit_string, "#x9527", 16)); + ASSERT_OK_AND_ASSIGN(std::string hex_string, bit_string.ToHexString()); + EXPECT_EQ(hex_string, "0x9527"); +} + +TEST(AppendZ3ValueStringToBitString, BitStringBitvector) { + pdpi::BitString bit_string; + ASSERT_OK( + AppendZ3ValueStringToBitString(bit_string, "#b1001010100100111", 16)); + ASSERT_OK_AND_ASSIGN(std::string hex_string, bit_string.ToHexString()); + EXPECT_EQ(hex_string, "0x9527"); } } // namespace