Memory: fix non-const memcpy & memset lambdas
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1747,7 +1747,6 @@ StateValue Calloc::toSMT(State &s) const {
// If memset's size is zero, then ptr can be NULL.
s.getMemory().memset(p, { expr::mkUInt(0, 8), true }, calloc_sz, 1);
- auto nullp = Pointer::mkNullPointer(s.getMemory());
return { move(p), np_num && np_sz };
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -170,8 +170,8 @@ static bool observes_addresses() {
namespace IR {
-Pointer::Pointer(const Memory &m, const char *var_name)
- : m(m), p(expr::mkUInt(0, 1).concat(
+Pointer::Pointer(const Memory &m, const char *var_name, const expr &local)
+ : m(m), p(local.toBVBool().concat(
expr::mkFreshVar(var_name, expr::mkUInt(0, total_bits()-1)))) {}
Pointer::Pointer(const Memory &m, unsigned bid, bool local) : m(m) {
@@ -751,7 +751,7 @@ void Memory::memset(const expr &p, const StateValue &val, const expr &bytesize,
store(ptr + i, bytes[0](), local_block_val, non_local_block_val);
}
} else {
- Pointer idx(*this, "#idx");
+ Pointer idx(*this, "#idx", ptr.is_local());
expr cond = idx.uge(ptr).both() && idx.ult(ptr + bytesize).both();
store_lambda(idx, cond, bytes[0](), local_block_val, non_local_block_val);
}
@@ -774,7 +774,7 @@ void Memory::memcpy(const expr &d, const expr &s, const expr &bytesize,
local_block_val, non_local_block_val);
}
} else {
- Pointer dst_idx(*this, "#idx");
+ Pointer dst_idx(*this, "#idx", dst.is_local());
Pointer src_idx = src + (dst_idx.get_offset() - dst.get_offset());
expr cond = dst_idx.uge(dst).both() && dst_idx.ult(dst + bytesize).both();
store_lambda(dst_idx, cond,

MODIFY
ir/memory.h
ir/memory.h
@@ -39,7 +39,8 @@ class Pointer {
const smt::expr &ret_type) const;
public:
- Pointer(const Memory &m, const char *var_name);
+ Pointer(const Memory &m, const char *var_name,
+ const smt::expr &local = false);
Pointer(const Memory &m, smt::expr p) : m(m), p(std::move(p)) {}
Pointer(const Memory &m, unsigned bid, bool local);
Pointer(const Memory &m, const smt::expr &bid, const smt::expr &offset);

ADD
tests/alive-tv/memory/calloc-init-fail.src.ll
+target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
+
+define i8 @calloc_init() {
+ %ptr = call noalias i8* @calloc(i64 1, i64 1)
+ %i = ptrtoint i8* %ptr to i64
+ %cmp = icmp eq i64 %i, 0
+ br i1 %cmp, label %BB1, label %BB2
+BB1:
+ ret i8 1
+BB2:
+ %v = load i8, i8* %ptr
+ %w = add i8 %v, 2
+ ret i8 %w
+}
+
+; ERROR: Value mismatch
+
+declare noalias i8* @calloc(i64, i64)
+declare void @free(i8*)

ADD
tests/alive-tv/memory/calloc-init-fail.tgt.ll
+target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
+
+define i8 @calloc_init() {
+ %ptr = call noalias i8* @calloc(i64 1, i64 1)
+ %i = ptrtoint i8* %ptr to i64
+ %cmp = icmp eq i64 %i, 0
+ br i1 %cmp, label %BB1, label %BB2
+BB1:
+ ret i8 1
+BB2:
+ %v = load i8, i8* %ptr
+ ret i8 %v
+}
+
+declare noalias i8* @calloc(i64, i64)
+declare void @free(i8*)

Memory: fix non-const memcpy & memset lambdas (#188)