memory: simplify previous patch by allowing null->0, but not 0->null
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -174,11 +174,10 @@ void BinOp::print(ostream &os) const {
static void div_ub(State &s, const expr &a, const expr &b, const expr &ap,
const expr &bp, bool sign) {
- auto bits = b.bits();
s.addUB(bp);
s.addUB(b != 0);
if (sign)
- s.addUB((ap && a != expr::IntSMin(bits)) || b != expr::mkInt(-1, bits));
+ s.addUB((ap && a != expr::IntSMin(b.bits())) || b != expr::mkInt(-1, b));
}
static expr any_fp_zero(State &s, expr v) {

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -73,17 +73,15 @@ expr Byte::nonptr_value() const {
expr Byte::is_poison(bool fullbit) const {
expr np = nonptr_nonpoison();
return expr::mkIf(is_ptr(), !ptr_nonpoison(),
- fullbit ? np == expr::mkInt(-1, np.bits()) :
- !(np == expr::mkUInt(0, np.bits())));
+ fullbit ? np == expr::mkInt(-1, np)
+ : np != 0);
}
-expr Byte::is_zero(bool allow_poison) const {
- auto nullp = Pointer::mkNullPointer(m);
- auto np = nonptr_nonpoison(), nv = nonptr_value();
+expr Byte::is_zero() const {
return expr::mkIf(is_ptr(),
- (ptr_nonpoison() || allow_poison) && ptr_value() == nullp(),
- (np == expr::mkUInt(0, np.bits()) || allow_poison) &&
- nv == expr::mkUInt(0, nv.bits()));
+ ptr_nonpoison() &&
+ ptr_value() == Pointer::mkNullPointer(m)(),
+ nonptr_nonpoison() == 0 && nonptr_value() == 0);
}
Byte Byte::mkPoisonByte(const Memory &m) {
@@ -147,10 +145,10 @@ static vector<Byte> valueToBytes(const StateValue &val, const Type &fromType,
static StateValue bytesToValue(const Memory &m, const vector<Byte> &bytes,
const Type &toType) {
assert(!bytes.empty());
- auto nullp = Pointer::mkNullPointer(m);
if (toType.isPtrType()) {
assert(bytes.size() == bits_size_t / bits_byte);
+ auto nullp = Pointer::mkNullPointer(m);
expr loaded_ptr;
// The result is not poison if all of these hold:
// (1) There's no poison byte, and they are all pointer bytes
@@ -169,9 +167,9 @@ static StateValue bytesToValue(const Memory &m, const vector<Byte> &bytes,
} else {
non_poison &= ptr_value == loaded_ptr;
}
- non_poison &= b.is_ptr() || b.nonptr_value() == 0;
+ non_poison &= expr::mkIf(b.is_ptr(), b.ptr_byteoffset() == i,
+ b.nonptr_value() == 0);
non_poison &= !b.is_poison(false);
- non_poison &= b.is_ptr().implies(b.ptr_byteoffset() == i);
}
return { move(loaded_ptr), move(non_poison) };
@@ -182,13 +180,10 @@ static StateValue bytesToValue(const Memory &m, const vector<Byte> &bytes,
StateValue val;
bool first = true;
IntType ibyteTy("", bits_byte);
- auto zero = expr::mkUInt(0, bits_byte);
for (auto &b: bytes) {
- auto ptr_p = b.is_ptr().implies(b.ptr_value() == nullp() &&
- b.ptr_nonpoison());
- auto p = ibyteTy.combine_poison(move(ptr_p), b.nonptr_nonpoison());
- StateValue v(expr::mkIf(b.is_ptr(), zero, b.nonptr_value()), move(p));
+ StateValue v(b.nonptr_value(),
+ ibyteTy.combine_poison(!b.is_ptr(), b.nonptr_nonpoison()));
val = first ? move(v) : v.concat(val);
first = false;
}
@@ -487,7 +482,7 @@ expr Pointer::block_val_refined(const Pointer &other) const {
return val.is_poison() ||
expr::mkIf(is_ptr == is_ptr2,
expr::mkIf(is_ptr, ptr_cnstr, int_cnstr),
- val.is_zero() && val2.is_zero(false));
+ val.is_zero() && val2.is_zero());
}
expr Pointer::block_refined(const Pointer &other) const {

MODIFY
ir/memory.h
ir/memory.h
@@ -54,9 +54,7 @@ public:
smt::expr nonptr_nonpoison() const;
smt::expr nonptr_value() const;
smt::expr is_poison(bool fullbit = true) const;
- // Returns whether its value is integer zero or null pointer.
- // If poison is true, poison value is allowed
- smt::expr is_zero(bool allow_poison = true) const;
+ smt::expr is_zero() const; // zero or null
const smt::expr& operator()() const { return p; }

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -171,6 +171,11 @@ expr expr::mkInt(int64_t n, unsigned bits) {
return bits ? mkInt(n, mkBVSort(bits)) : expr();
}
+expr expr::mkInt(int64_t n, const expr &type) {
+ C2(type);
+ return mkInt(n, type.sort());
+}
+
expr expr::mkInt(const char *n, unsigned bits) {
return bits ? Z3_mk_numeral(ctx(), n, mkBVSort(bits)) : expr();
}

MODIFY
smt/expr.h
smt/expr.h
@@ -79,6 +79,7 @@ public:
static expr mkUInt(uint64_t n, unsigned bits);
static expr mkInt(int64_t n, unsigned bits);
+ static expr mkInt(int64_t n, const expr &type);
static expr mkInt(const char *n, unsigned bits);
static expr mkFloat(double n, const expr &type);
static expr mkHalf(float n);

MODIFY
tests/alive-tv/memory/zeroinit-memset.src.ll
tests/alive-tv/memory/zeroinit-memset.src.ll
; From Transforms/MemCpyOpt/fca2memcpy.ll
-; TEST-ARGS: -smt-to=15000 -disable-undef-input
+; TEST-ARGS: -smt-to=15000 -disable-undef-input -disable-poison-input
target datalayout = "e-i64:64-f80:128-n8:16:32:64"
-target triple = "x86_64-unknown-linux-gnu"
%S = type { i8*, i8, i32 }

MODIFY
tests/alive-tv/memory/zeroinit-memset.tgt.ll
tests/alive-tv/memory/zeroinit-memset.tgt.ll
-; ModuleID = 'zeroinit-memset.src.ll'
-source_filename = "zeroinit-memset.src.ll"
target datalayout = "e-i64:64-f80:128-n8:16:32:64"
-target triple = "x86_64-unknown-linux-gnu"
%S = type { i8*, i8, i32 }
define void @destroysrc(%S* %src, %S* %dst) {
@@ -11,7 +8,5 @@ define void @destroysrc(%S* %src, %S* %dst) {
store %S %1, %S* %dst
ret void
}
-; Function Attrs: argmemonly nounwind willreturn
-declare void @llvm.memset.p0i8.i64(i8* nocapture writeonly, i8, i64, i1 immarg) #0
-attributes #0 = { argmemonly nounwind willreturn }
+declare void @llvm.memset.p0i8.i64(i8* nocapture writeonly, i8, i64, i1 immarg)

memory: simplify previous patch by allowing null->0, but not 0->null