memory: simplify encoding of pointer load
this now disallows loading null ptrs stored half as ptrs and half as 0-integer
transformation not seen in practice (yet/ever?)
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -249,7 +249,7 @@ static StateValue bytesToValue(const Memory &m, const vector<Byte> &bytes,
if (toType.isPtrType()) {
assert(bytes.size() == bits_program_pointer / bits_byte);
auto nullp = Pointer::mkNullPointer(m);
- expr loaded_ptr;
+ expr loaded_ptr, is_ptr;
// The result is not poison if all of these hold:
// (1) There's no poison byte, and they are all pointer bytes
// (2) All of the bytes have the same information
@@ -260,18 +260,22 @@ static StateValue bytesToValue(const Memory &m, const vector<Byte> &bytes,
for (unsigned i = 0, e = bytes.size(); i < e; ++i) {
auto &b = bytes[i];
- expr ptr_value = expr::mkIf(b.is_ptr(), b.ptr_value(), nullp());
+ expr ptr_value = b.ptr_value();
+ expr b_is_ptr = b.is_ptr();
if (i == 0) {
- loaded_ptr = move(ptr_value);
+ loaded_ptr = ptr_value;
+ is_ptr = move(b_is_ptr);
} else {
- non_poison &= ptr_value == loaded_ptr;
+ non_poison &= is_ptr == b_is_ptr;
}
- non_poison &= expr::mkIf(b.is_ptr(), b.ptr_byteoffset() == i,
+ non_poison &=
+ expr::mkIf(is_ptr,
+ b.ptr_byteoffset() == i && ptr_value == loaded_ptr,
b.nonptr_value() == 0);
non_poison &= !b.is_poison(false);
}
- return { move(loaded_ptr), move(non_poison) };
+ return { expr::mkIf(is_ptr, loaded_ptr, nullp()), move(non_poison) };
} else {
auto bitsize = toType.bits();

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -343,7 +343,7 @@ bool expr::isInt(int64_t &n) const {
return true;
}
-bool expr::isEq(expr &lhs, expr &rhs) {
+bool expr::isEq(expr &lhs, expr &rhs) const {
if (auto app = isAppOf(Z3_OP_EQ)) {
lhs = Z3_get_app_arg(ctx(), app, 0);
rhs = Z3_get_app_arg(ctx(), app, 1);
@@ -1027,6 +1027,12 @@ expr expr::cmp_eq(const expr &rhs, bool simplify) const {
if (rhs.isFalse())
return !*this;
+ {
+ expr lhs_a, lhs_b, rhs_a, rhs_b;
+ if (isEq(lhs_a, lhs_b) && rhs.isEq(rhs_a, rhs_b) && lhs_a.eq(rhs_a))
+ return lhs_b == rhs_b;
+ }
+
if (auto app = isAppOf(Z3_OP_CONCAT)) {
unsigned num_args = Z3_get_app_num_args(ctx(), app);
if (rhs.isConst()) {

MODIFY
smt/expr.h
smt/expr.h
@@ -121,7 +121,7 @@ public:
bool isUInt(uint64_t &n) const;
bool isInt(int64_t &n) const;
- bool isEq(expr &lhs, expr &rhs);
+ bool isEq(expr &lhs, expr &rhs) const;
bool isIf(expr &cond, expr &then, expr &els) const;
bool isConcat(expr &a, expr &b) const;
bool isExtract(expr &e, unsigned &high, unsigned &low) const;

memory: simplify encoding of pointer load
this now disallows loading null ptrs stored half as ptrs and half as 0-integer
transformation not seen in practice (yet/ever?)