fncall: add support for local ptr refinement
fixes
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -492,17 +492,48 @@ expr Pointer::is_heap_allocated() const {
expr Pointer::refined(const Pointer &other) const {
// This refers to a block that was malloc'ed within the function
- expr local = other.is_heap_allocated();
- local &= other.is_block_alive();
+ expr local = get_alloc_type() == other.get_alloc_type();
local &= block_size() == other.block_size();
local &= get_offset() == other.get_offset();
- // TODO: this induces an infinite loop; need a quantifier or rec function
- // TODO: needs variable offset
- //local &= block_refined(other);
- local = (is_heap_allocated() && is_block_alive()).implies(local);
+ // TODO: this induces an infinite loop
+ //local &= block_refined(other);
- return expr::mkIf(is_local(), local, *this == other);
+ return is_block_alive().implies(
+ other.is_block_alive() &&
+ expr::mkIf(is_local(), is_heap_allocated().implies(local),
+ *this == other));
+}
+
+expr Pointer::fninput_refined(const Pointer &other) const {
+ expr size = block_size();
+ expr off = get_offset();
+ expr size2 = other.block_size();
+ expr off2 = other.get_offset();
+
+ // We allow alloca->anything, but not local malloc->alloca/non-local ptr
+ // because we can't go from a free'able pointer to a non-free'able
+ expr local
+ = expr::mkIf(is_heap_allocated(),
+ other.is_local() && other.is_heap_allocated() && off == off2 &&
+ size2.uge(size),
+
+ // must maintain same dereferenceability before & after
+ expr::mkIf(off.sle(-1),
+ off == off2 && size2.uge(size),
+ off2.sge(0) &&
+ expr::mkIf(off.sle(size),
+ off2.sle(size2) && off2.uge(off) &&
+ (size2 - off2).uge(size - off),
+ off2.sgt(size2) && off == off2 &&
+ size2.uge(size))));
+
+ // TODO: this induces an infinite loop
+ // block_refined(other);
+
+ return is_block_alive().implies(
+ other.is_block_alive() &&
+ expr::mkIf(is_local(), local, *this == other));
}
expr Pointer::block_val_refined(const Pointer &other) const {

MODIFY
ir/memory.h
ir/memory.h
@@ -151,6 +151,7 @@ public:
smt::expr is_heap_allocated() const;
smt::expr refined(const Pointer &other) const;
+ smt::expr fninput_refined(const Pointer &other) const;
smt::expr block_val_refined(const Pointer &other) const;
smt::expr block_refined(const Pointer &other) const;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -330,7 +330,7 @@ void State::mkAxioms(State &tgt) {
for (unsigned i = 0, e = ptr_ins.size(); i != e; ++i) {
expr eq_val = Pointer(memory, ptr_ins[i].value)
- .refined(Pointer(memory, ptr_ins2[i].value));
+ .fninput_refined(Pointer(memory, ptr_ins2[i].value));
is_val_eq &= eq_val;
refines &= ptr_ins[i].non_poison
.implies(eq_val && ptr_ins2[i].non_poison);

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1131,6 +1131,16 @@ expr expr::ugt(uint64_t rhs) const {
return ugt(mkUInt(rhs, sort()));
}
+expr expr::sle(int64_t rhs) const {
+ C();
+ return sle(mkInt(rhs, sort()));
+}
+
+expr expr::sge(int64_t rhs) const {
+ C();
+ return sge(mkInt(rhs, sort()));
+}
+
expr expr::operator==(uint64_t rhs) const {
C();
return *this == mkUInt(rhs, sort());

MODIFY
smt/expr.h
smt/expr.h
@@ -230,6 +230,8 @@ public:
expr ult(uint64_t rhs) const;
expr uge(uint64_t rhs) const;
expr ugt(uint64_t rhs) const;
+ expr sle(int64_t rhs) const;
+ expr sge(int64_t rhs) const;
expr operator==(uint64_t rhs) const;
expr operator!=(uint64_t rhs) const;

ADD
tests/alive-tv/call-strfwd.src.ll
+; ERROR: Source is more defined
+
+define i8 @f(i8* %p) {
+ %a = call i8* @malloc(i64 1)
+ call void @llvm.memcpy.p0i8.p0i8.i64(i8* %a, i8* %p, i64 1, i1 false)
+ %b = call i8 @g(i8* %a)
+ ret i8 %b
+}
+
+declare i8 @g(i8*)
+declare i8* @malloc(i64)
+declare void @llvm.memcpy.p0i8.p0i8.i64(i8*, i8*, i64, i1)

ADD
tests/alive-tv/call-strfwd.tgt.ll
+define i8 @f(i8* %p) {
+ %b = call i8 @g(i8* %p)
+ ret i8 %b
+}
+
+declare i8 @g(i8*)

MODIFY
tests/alive-tv/call.src.ll
tests/alive-tv/call.src.ll
@@ -21,5 +21,21 @@ define i8 @f4(i8* %a) {
ret i8 %b
}
+define i8 @f5() {
+ %p0 = alloca i8
+ %p = alloca i8
+ %b = call i8 @g(i8* %p)
+ ret i8 %b
+}
+
+define i8 @f6(i8* %p) {
+ %a = alloca i8
+ call void @llvm.memcpy.p0i8.p0i8.i64(i8* %a, i8* %p, i64 1, i1 false)
+ %b = call i8 @g(i8* %a)
+ ret i8 %b
+}
+
declare i8 @g(i8*)
declare i8 @h(i8*) readnone
+
+declare void @llvm.memcpy.p0i8.p0i8.i64(i8*, i8*, i64, i1)

MODIFY
tests/alive-tv/call.tgt.ll
tests/alive-tv/call.tgt.ll
@@ -22,5 +22,18 @@ define i8 @f4(i8* %a) {
ret i8 %b
}
+define i8 @f5() {
+ %p = alloca i8
+ %b = call i8 @g(i8* %p)
+ ret i8 %b
+}
+
+define i8 @f6(i8* %p) {
+ %b = call i8 @g(i8* %p)
+ ret i8 %b
+}
+
declare i8 @g(i8*)
declare i8 @h(i8*) readnone
+
+declare void @llvm.memcpy.p0i8.p0i8.i64(i8*, i8*, i64, i1)

fncall: add support for local ptr refinement
fixes #227