Make null ptr byte and zero int byte compatible
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -70,10 +70,20 @@ expr Byte::nonptr_value() const {
return p.extract(bits_byte - 1, 0);
}
-expr Byte::is_poison() const {
+expr Byte::is_poison(bool fullbit) const {
expr np = nonptr_nonpoison();
return expr::mkIf(is_ptr(), !ptr_nonpoison(),
- np == expr::mkInt(-1, np.bits()));
+ fullbit ? np == expr::mkInt(-1, np.bits()) :
+ !(np == expr::mkUInt(0, np.bits())));
+}
+
+expr Byte::is_zero(bool allow_poison) const {
+ auto nullp = Pointer::mkNullPointer(m);
+ auto np = nonptr_nonpoison(), nv = nonptr_value();
+ 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()));
}
Byte Byte::mkPoisonByte(const Memory &m) {
@@ -134,8 +144,10 @@ static vector<Byte> valueToBytes(const StateValue &val, const Type &fromType,
return bytes;
}
-static StateValue bytesToValue(const vector<Byte> &bytes, const Type &toType) {
+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);
@@ -144,20 +156,22 @@ static StateValue bytesToValue(const vector<Byte> &bytes, const Type &toType) {
// (1) There's no poison byte, and they are all pointer bytes
// (2) All of the bytes have the same information
// (3) Byte offsets should be correct
+ // A zero integer byte is considered as a null pointer byte with any byte
+ // offset.
expr non_poison = true;
for (unsigned i = 0, e = bytes.size(); i < e; ++i) {
auto &b = bytes[i];
- expr ptr_value = b.ptr_value();
+ expr ptr_value = expr::mkIf(b.is_ptr(), b.ptr_value(), nullp());
if (i == 0) {
loaded_ptr = move(ptr_value);
} else {
non_poison &= ptr_value == loaded_ptr;
}
- non_poison &= b.is_ptr();
- non_poison &= b.ptr_nonpoison();
- non_poison &= b.ptr_byteoffset() == i;
+ non_poison &= b.is_ptr() || 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) };
@@ -168,10 +182,13 @@ static StateValue bytesToValue(const vector<Byte> &bytes, const Type &toType) {
StateValue val;
bool first = true;
IntType ibyteTy("", bits_byte);
+ auto zero = expr::mkUInt(0, bits_byte);
for (auto &b: bytes) {
- StateValue v(b.nonptr_value(),
- ibyteTy.combine_poison(!b.is_ptr(), b.nonptr_nonpoison()));
+ 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));
val = first ? move(v) : v.concat(val);
first = false;
}
@@ -468,7 +485,9 @@ expr Pointer::block_val_refined(const Pointer &other) const {
ptr_cnstr = val2.ptr_nonpoison() && load_ptr.refined(load_ptr2);
}
return val.is_poison() ||
- (is_ptr == is_ptr2 && expr::mkIf(is_ptr, ptr_cnstr, int_cnstr));
+ expr::mkIf(is_ptr == is_ptr2,
+ expr::mkIf(is_ptr, ptr_cnstr, int_cnstr),
+ val.is_zero() && val2.is_zero(false));
}
expr Pointer::block_refined(const Pointer &other) const {
@@ -900,7 +919,7 @@ StateValue Memory::load(const expr &p, const Type &type, unsigned align,
loadedBytes.emplace_back(*this, ::load(ptr_i, local_block_val,
non_local_block_val));
}
- ret = bytesToValue(loadedBytes, type);
+ ret = bytesToValue(*this, loadedBytes, type);
}
return state->rewriteUndef(move(ret));
}

MODIFY
ir/memory.h
ir/memory.h
@@ -53,7 +53,10 @@ public:
smt::expr ptr_byteoffset() const;
smt::expr nonptr_nonpoison() const;
smt::expr nonptr_value() const;
- smt::expr is_poison() 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;
const smt::expr& operator()() const { return p; }

MODIFY
tests/alive-tv/memory/gep-struct2.src.ll
tests/alive-tv/memory/gep-struct2.src.ll
+; TEST-ARGS: -smt-to=2000
target datalayout = "e-i32:32-i128:32-i8:8"
%0 = type [10 x { i32, i128, [5 x { i32, i8, i8 }] }]

MODIFY
tests/alive-tv/memory/pre-bigendian.src.ll
tests/alive-tv/memory/pre-bigendian.src.ll
; This was excerpted from GVN/PRE/rle.ll
+; TEST-ARGS: -smt-to=2000
target datalayout = "E-p:32:32:32-p1:16:16:16-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:32:64-f32:32:32-f64:64:64-n32"
define i8 @coerce_mustalias_pre0(i16* %P, i1 %cond) {

MODIFY
tests/alive-tv/memory/punning-intptr.src.ll
tests/alive-tv/memory/punning-intptr.src.ll
-; TEST-ARGS: -smt-to=9000
+; TEST-ARGS: -smt-to=9000 -disable-undef-input
target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"

MODIFY
tests/alive-tv/memory/punning-ptrint.src.ll
tests/alive-tv/memory/punning-ptrint.src.ll
-; TEST-ARGS: -disable-undef-input -disable-poison-input -smt-to=10000
-
-target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
+; TEST-ARGS: -disable-undef-input -smt-to=10000
define i8 @ptr_int_punning(i8** %pptr, i64 %n) {
- %ptr = call i8* @malloc(i64 1)
- %cmp = icmp eq i8* %ptr, null
- br i1 %cmp, label %BB1, label %BB2
-BB1:
- ret i8 0
-BB2:
+ %ptr = alloca i8
store i8* %ptr, i8** %pptr
%pi8 = bitcast i8** %pptr to i8*
%n2 = and i64 %n, 7
@@ -17,4 +10,3 @@ BB2:
; %v is poison.
ret i8 %v
}
-declare noalias i8* @malloc(i64)

MODIFY
tests/alive-tv/memory/punning-ptrint.tgt.ll
tests/alive-tv/memory/punning-ptrint.tgt.ll
-target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
-
define i8 @ptr_int_punning(i8** %pptr, i64 %n) {
- %ptr = call i8* @malloc(i64 1)
- %cmp = icmp eq i8* %ptr, null
- br i1 %cmp, label %BB1, label %BB2
-BB1:
- ret i8 0
-BB2:
+ %ptr = alloca i8
store i8* %ptr, i8** %pptr
ret i8 undef
}

MODIFY
tests/alive-tv/memory/store-removal.src.ll
tests/alive-tv/memory/store-removal.src.ll
@@ -3,3 +3,9 @@ define void @f(i8* %p) {
store i8 %v, i8* %p
ret void
}
+
+define void @f2(i8** %p) {
+ %v = load i8*, i8** %p
+ store i8* %v, i8** %p
+ ret void
+}

MODIFY
tests/alive-tv/memory/store-removal.tgt.ll
tests/alive-tv/memory/store-removal.tgt.ll
define void @f(i8* %p) {
ret void
}
+
+define void @f2(i8** %p) {
+ ret void
+}

ADD
tests/alive-tv/memory/zeroinit-memset.src.ll
+; From Transforms/MemCpyOpt/fca2memcpy.ll
+; TEST-ARGS: -smt-to=15000 -disable-undef-input
+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) {
+ %1 = load %S, %S* %src
+ store %S zeroinitializer, %S* %src
+ store %S %1, %S* %dst
+ ret void
+}
+
+

ADD
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) {
+ %1 = load %S, %S* %src
+ %2 = bitcast %S* %src to i8*
+ call void @llvm.memset.p0i8.i64(i8* align 8 %2, i8 0, i64 16, i1 false)
+ 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 }

ADD
tests/alive-tv/refinement/zero-null.src.ll
+define void @f(i64* %p) {
+ store i64 0, i64* %p
+ ret void
+}
+
+define void @f2(i64* %p) {
+ %p2 = bitcast i64* %p to i8**
+ store i8* null, i8** %p2, align 4
+ ret void
+}

ADD
tests/alive-tv/refinement/zero-null.tgt.ll
+define void @f(i64* %p) {
+ %p2 = bitcast i64* %p to i8**
+ store i8* null, i8** %p2, align 4
+ ret void
+}
+
+define void @f2(i64* %p) {
+ store i64 0, i64* %p
+ ret void
+}

Make null ptr byte and zero int byte compatible (#237)