Skip to content

Commit f530593

Browse files
kishanpsVSuryaprasad-HCL
kishanps
authored and
VSuryaprasad-HCL
committed
[P4-Symbolic] Extend z3_util to evaluate bitvectors to unsigned integers.
1 parent 27c83de commit f530593

File tree

4 files changed

+418
-31
lines changed

4 files changed

+418
-31
lines changed

‎p4_symbolic/BUILD.bazel

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,8 +50,11 @@ cc_library(
5050
"//p4_pdpi/string_encodings:hex_string",
5151
"@com_github_z3prover_z3//:api",
5252
"@com_gnu_gmp//:gmp",
53+
"@com_google_absl//absl/numeric:int128",
54+
"@com_google_absl//absl/status",
5355
"@com_google_absl//absl/status:statusor",
5456
"@com_google_absl//absl/strings",
57+
"@com_google_absl//absl/types:optional",
5558
],
5659
)
5760

@@ -116,6 +119,11 @@ cc_test(
116119
srcs = ["z3_util_test.cc"],
117120
deps = [
118121
":z3_util",
122+
"//gutil:status_matchers",
123+
"//p4_pdpi/string_encodings:bit_string",
124+
"@com_github_z3prover_z3//:api",
125+
"@com_google_absl//absl/numeric:int128",
126+
"@com_google_absl//absl/status",
119127
"@com_google_googletest//:gtest_main",
120128
],
121129
)

‎p4_symbolic/z3_util.cc

Lines changed: 107 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -14,12 +14,25 @@
1414

1515
#include "p4_symbolic/z3_util.h"
1616

17+
#include <cstddef>
18+
#include <cstdint>
19+
#include <string>
20+
21+
#include "absl/numeric/int128.h"
22+
#include "absl/status/status.h"
1723
#include "absl/status/statusor.h"
24+
#include "absl/strings/match.h"
25+
#include "absl/strings/numbers.h"
26+
#include "absl/strings/str_cat.h"
27+
#include "absl/strings/string_view.h"
1828
#include "absl/strings/strip.h"
29+
#include "absl/types/optional.h"
1930
#include "gmpxx.h"
2031
#include "gutil/status.h"
32+
#include "p4_pdpi/string_encodings/bit_string.h"
2133
#include "p4_pdpi/string_encodings/hex_string.h"
2234
#include "z3++.h"
35+
#include "z3_api.h"
2336

2437
namespace p4_symbolic {
2538

@@ -113,25 +126,32 @@ absl::Status AppendHexCharStringToPDPIBitString(
113126

114127
absl::StatusOr<bool> EvalZ3Bool(const z3::expr& bool_expr,
115128
const z3::model& model) {
116-
// TODO: Ensure this doesn't crash by checking sort first.
117-
auto value = model.eval(bool_expr, true).bool_value();
129+
if (!bool_expr.is_bool()) {
130+
return gutil::InvalidArgumentErrorBuilder()
131+
<< "Expected a boolean expression, found '" << bool_expr << "'";
132+
}
133+
134+
auto value = model.eval(bool_expr, /*model_completion=*/true).bool_value();
118135
switch (value) {
119136
case Z3_L_FALSE:
120137
return false;
121138
case Z3_L_TRUE:
122139
return true;
123140
default:
124-
break;
141+
return gutil::InternalErrorBuilder()
142+
<< "boolean expression '" << bool_expr
143+
<< "' evaluated to unexpected Boolean value " << value;
125144
}
126-
return gutil::InternalErrorBuilder()
127-
<< "boolean expression '" << bool_expr
128-
<< "' evaluated to unexpected Boolean value " << value;
129145
}
130146

131147
absl::StatusOr<int> EvalZ3Int(const z3::expr& int_expr,
132148
const z3::model& model) {
133-
// TODO: Ensure this doesn't crash by checking sort first.
134-
return model.eval(int_expr, true).get_numeral_int();
149+
if (!int_expr.is_int()) {
150+
return gutil::InvalidArgumentErrorBuilder()
151+
<< "Expected an integer expression, found '" << int_expr << "'";
152+
}
153+
154+
return model.eval(int_expr, /*model_completion=*/true).get_numeral_int();
135155
}
136156

137157
absl::Status EvalAndAppendZ3BitvectorToBitString(pdpi::BitString& output,
@@ -142,22 +162,73 @@ absl::Status EvalAndAppendZ3BitvectorToBitString(pdpi::BitString& output,
142162
<< "Expected a bitvector, found '" << bv_expr << "'";
143163
}
144164

145-
const std::string field_value =
165+
const std::string value =
166+
model.eval(bv_expr, /*model_completion=*/true).to_string();
167+
return AppendZ3ValueStringToBitString(output, value,
168+
bv_expr.get_sort().bv_size());
169+
}
170+
171+
absl::StatusOr<uint64_t> EvalZ3BitvectorToUInt64(const z3::expr& bv_expr,
172+
const z3::model& model) {
173+
if (!bv_expr.is_bv()) {
174+
return gutil::InvalidArgumentErrorBuilder()
175+
<< "Expected a bitvector, found '" << bv_expr << "'";
176+
}
177+
178+
if (bv_expr.get_sort().bv_size() > 64) {
179+
return gutil::InvalidArgumentErrorBuilder()
180+
<< "Expected a bitvector within 64 bits, found "
181+
<< bv_expr.get_sort().bv_size() << " bits";
182+
}
183+
184+
const std::string value =
146185
model.eval(bv_expr, /*model_completion=*/true).to_string();
147-
absl::string_view field_value_view = field_value;
148-
149-
if (absl::ConsumePrefix(&field_value_view, "#x")) {
150-
RETURN_IF_ERROR(AppendHexCharStringToPDPIBitString(
151-
output, field_value_view, bv_expr.get_sort().bv_size()));
152-
} else if (absl::ConsumePrefix(&field_value_view, "#b")) {
153-
RETURN_IF_ERROR(AppendBitCharStringToPDPIBitString(
154-
output, field_value_view, bv_expr.get_sort().bv_size()));
186+
return Z3ValueStringToInt(value);
187+
}
188+
189+
absl::StatusOr<absl::uint128> EvalZ3BitvectorToUInt128(const z3::expr& bv_expr,
190+
const z3::model& model) {
191+
if (!bv_expr.is_bv()) {
192+
return gutil::InvalidArgumentErrorBuilder()
193+
<< "Expected a bitvector, found '" << bv_expr << "'";
194+
}
195+
196+
if (bv_expr.get_sort().bv_size() > 128) {
197+
return gutil::InvalidArgumentErrorBuilder()
198+
<< "Expected a bitvector within 128 bits, found "
199+
<< bv_expr.get_sort().bv_size() << " bits";
200+
}
201+
202+
const std::string value_string =
203+
model.eval(bv_expr, /*model_completion=*/true).to_string();
204+
absl::string_view value = value_string;
205+
absl::uint128 result;
206+
207+
if (absl::ConsumePrefix(&value, "#x")) {
208+
if (!absl::SimpleHexAtoi(value, &result)) {
209+
return gutil::InvalidArgumentErrorBuilder()
210+
<< "Unable to convert hex string '" << value << "' to uint128";
211+
}
212+
} else if (absl::ConsumePrefix(&value, "#b")) {
213+
uint64_t hi = 0;
214+
uint64_t lo = 0;
215+
216+
if (value.size() > 64) {
217+
hi = std::stoull(std::string(value.substr(0, value.size() - 64)),
218+
/*idx=*/nullptr, /*base=*/2);
219+
lo = std::stoull(std::string(value.substr(value.size() - 64)),
220+
/*idx=*/nullptr, /*base=*/2);
221+
} else {
222+
lo = std::stoull(std::string(value), /*idx=*/nullptr, /*base=*/2);
223+
}
224+
225+
result = absl::MakeUint128(hi, lo);
155226
} else {
156227
return gutil::InvalidArgumentErrorBuilder()
157-
<< "Invalid Z3 bitvector value '" << field_value << "'";
228+
<< "Invalid Z3 bitvector value '" << value << "'";
158229
}
159230

160-
return absl::OkStatus();
231+
return result;
161232
}
162233

163234
absl::StatusOr<z3::expr> HexStringToZ3Bitvector(z3::context& context,
@@ -191,4 +262,21 @@ uint64_t Z3ValueStringToInt(const std::string& value) {
191262
}
192263
}
193264

265+
absl::Status AppendZ3ValueStringToBitString(pdpi::BitString& result,
266+
absl::string_view value,
267+
size_t num_bits) {
268+
if (absl::ConsumePrefix(&value, "#x")) {
269+
RETURN_IF_ERROR(
270+
AppendHexCharStringToPDPIBitString(result, value, num_bits));
271+
} else if (absl::ConsumePrefix(&value, "#b")) {
272+
RETURN_IF_ERROR(
273+
AppendBitCharStringToPDPIBitString(result, value, num_bits));
274+
} else {
275+
return gutil::InvalidArgumentErrorBuilder()
276+
<< "Invalid Z3 bitvector value '" << value << "'";
277+
}
278+
279+
return absl::OkStatus();
280+
}
281+
194282
} // namespace p4_symbolic

‎p4_symbolic/z3_util.h

Lines changed: 40 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,23 +14,52 @@
1414
#ifndef PINS_P4_SYMBOLIC_Z3_UTIL_H_
1515
#define PINS_P4_SYMBOLIC_Z3_UTIL_H_
1616

17+
#include <cstddef>
18+
#include <cstdint>
19+
#include <string>
20+
21+
#include "absl/numeric/int128.h"
22+
#include "absl/status/status.h"
1723
#include "absl/status/statusor.h"
24+
#include "absl/strings/string_view.h"
25+
#include "absl/types/optional.h"
1826
#include "p4_pdpi/string_encodings/bit_string.h"
1927
#include "z3++.h"
2028

2129
namespace p4_symbolic {
2230

2331
// -- Evaluation ---------------------------------------------------------------
2432

25-
absl::StatusOr<bool> EvalZ3Bool(const z3::expr &bool_expr,
26-
const z3::model &model);
33+
// Evaluates the given `bool_expr` to a boolean value based on the given
34+
// `model`. Returns an error if the given expression is not a boolean
35+
// expression.
36+
absl::StatusOr<bool> EvalZ3Bool(const z3::expr& bool_expr,
37+
const z3::model& model);
2738

28-
absl::StatusOr<int> EvalZ3Int(const z3::expr &int_expr, const z3::model &model);
39+
// Evaluates the given `int_expr` to an integer value based on the given
40+
// `model`. Returns an error if the given expression is not an integer
41+
// expression.
42+
absl::StatusOr<int> EvalZ3Int(const z3::expr& int_expr, const z3::model& model);
2943

44+
// Evaluates the given `bv_expr` bit-vector and appends the value to the
45+
// `output` bit-string based on the given `model`. Returns an error if the given
46+
// expression is not a bit-vector.
3047
absl::Status EvalAndAppendZ3BitvectorToBitString(pdpi::BitString& output,
3148
const z3::expr& bv_expr,
3249
const z3::model& model);
3350

51+
// Evaluates the given `bv_expr` bit-vector to uint64_t based on the given
52+
// `model`. Returns an error if the given expression is not a bit-vector or if
53+
// the size is over 64 bits.
54+
absl::StatusOr<uint64_t> EvalZ3BitvectorToUInt64(const z3::expr& bv_expr,
55+
const z3::model& model);
56+
57+
// Evaluates the given `bv_expr` bit-vector to absl::uint128 based on the given
58+
// `model`. Returns an error if the given expression is not a bit-vector or if
59+
// the size is over 128 bits.
60+
absl::StatusOr<absl::uint128> EvalZ3BitvectorToUInt128(const z3::expr& bv_expr,
61+
const z3::model& model);
62+
3463
// -- Constructing Z3 expressions ----------------------------------------------
3564

3665
// Returns Z3 bitvector of the given `hex_string` value.
@@ -50,6 +79,14 @@ HexStringToZ3Bitvector(z3::context &context, const std::string &hex_string,
5079
// fits in uint64_t (otherwise an exception will be thrown).
5180
uint64_t Z3ValueStringToInt(const std::string &value);
5281

82+
// Appends exactly `num_bits` bits to the `result` PDPI bit string from the
83+
// evaluated Z3 string `value`. Returns an error if the `value` is not a valid
84+
// Z3 bit-vector value (i.e., if it is not a hex string starting with "#x" and
85+
// not a binary bit string starting with "#b").
86+
absl::Status AppendZ3ValueStringToBitString(pdpi::BitString& result,
87+
absl::string_view value,
88+
size_t num_bits);
89+
5390
// == END OF PUBLIC INTERFACE ==================================================
5491

5592
} // namespace p4_symbolic

0 commit comments

Comments
 (0)