Skip to content

Commit

Permalink
[P4-Symbolic] Extend z3_util to evaluate bitvectors to unsigned integ…
Browse files Browse the repository at this point in the history 
…ers.
  • Loading branch information
@kishanps @VSuryaprasad-HCL
kishanps authored and VSuryaprasad-HCL committed Jan 20, 2025
1 parent 6f0c0d9 commit b578509
Show file tree
Hide file tree
Showing 4 changed files with 418 additions and 31 deletions.
8 changes: 8 additions & 0 deletions p4_symbolic/BUILD.bazel
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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",
],
)

Expand Down Expand Up @@ -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",
],
)
126 changes: 107 additions & 19 deletions p4_symbolic/z3_util.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {

Expand Down Expand Up @@ -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,
Expand All @@ -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,
Expand Down Expand Up @@ -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
43 changes: 40 additions & 3 deletions p4_symbolic/z3_util.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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
Expand Down
Loading

0 comments on commit b578509

Please sign in to comment.