let malloc be local as well, add comments and a few tests
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -172,11 +172,11 @@ void Pointer::is_disjoint(const expr &len1, const Pointer &ptr2,
len2.zextOrTrunc(m.bits_size_t)));
}
-expr Pointer::is_block_alive() {
+expr Pointer::is_block_alive() const {
return m.blocks_liveness.load(get_bid());
}
-expr Pointer::is_at_heap() {
+expr Pointer::is_at_heap() const {
return m.blocks_kind.load(get_bid()) == 1;
}
@@ -248,12 +248,12 @@ pair<expr, vector<expr>> Memory::mkInput(const char *name) {
return { Pointer(*this, offset, local_bid, bid).release(), { var } };
}
-expr Memory::alloc(const expr &bytes, unsigned align, bool heap) {
- Pointer p(*this, ++last_bid, !heap);
+expr Memory::alloc(const expr &size, unsigned align, bool heap) {
+ Pointer p(*this, ++last_bid, true);
state->addPre(p.is_aligned(align));
- expr size = bytes.zextOrTrunc(bits_size_t);
- state->addPre(p.block_size() == size);
+ expr size_zextOrTrunced = size.zextOrTrunc(bits_size_t);
+ state->addPre(p.block_size() == size_zextOrTrunced);
state->addPre(!mk_liveness_uf().load(p.get_bid()));
blocks_liveness = blocks_liveness.store(p.get_bid(), true);

MODIFY
ir/memory.h
ir/memory.h
@@ -19,10 +19,13 @@ class State;
class Pointer {
Memory &m;
// [offset, local_bid, nonlocal_bid]
- // A pointer is pointing to a memory block that is allocated at the current
- // stackframe if local_bid is non-zero and nonlocal_bid is zero.
- // Otherwise, it is either pointing to a global variable, heap, or a
- // stackframe that is not one of this function call.
+ // A pointer is pointing to a local memory block if local_bid is non-zero and
+ // nonlocal_bid is zero. A local memory block is a memory block that is
+ // allocated by an instruction during the current function call. This does
+ // not include allocated blocks from a nested function call. A heap-allocated
+ // block can also be a local memory block.
+ // Otherwise, a pointer is pointing to a non-local block, which can be either
+ // of global variable, heap, or a stackframe that is not this function call.
// TODO: missing support for address space
smt::expr p;
@@ -74,8 +77,8 @@ public:
void is_dereferenceable(const smt::expr &bytes, unsigned align);
void is_disjoint(const smt::expr &len1, const Pointer &ptr2,
const smt::expr &len2) const;
- smt::expr is_block_alive();
- smt::expr is_at_heap();
+ smt::expr is_block_alive() const;
+ smt::expr is_at_heap() const;
// Makes a null pointer.
// TODO: add a bool flag that says whether the twin memory model is used.
@@ -116,7 +119,8 @@ public:
std::pair<smt::expr, std::vector<smt::expr>> mkInput(const char *name);
- smt::expr alloc(const smt::expr &bytes, unsigned align, bool heap);
+ // Allocates a new local memory block.
+ smt::expr alloc(const smt::expr &size, unsigned align, bool heap);
void free(const smt::expr &ptr);
void store(const smt::expr &ptr, const StateValue &val, Type &type,

ADD
tests/alive-tv/freshbid-alloca.src.ll
+define i8 @freshbid_alloca(i8* %ptr0) {
+ %ptr = alloca i8
+ store i8 10, i8* %ptr
+ store i8 20, i8* %ptr0
+ %v = load i8, i8* %ptr
+ ret i8 %v
+}

ADD
tests/alive-tv/freshbid-alloca.tgt.ll
+define i8 @freshbid_alloca(i8* %ptr0) {
+ %ptr = alloca i8
+ store i8 10, i8* %ptr
+ store i8 20, i8* %ptr0
+ %v = load i8, i8* %ptr
+ ret i8 10
+}

ADD
tests/alive-tv/freshbid-malloc.src.ll
+define i8 @freshbid_malloc(i8* %ptr0) {
+ %ptr = call noalias i8* @malloc(i64 1)
+ store i8 10, i8* %ptr
+ store i8 20, i8* %ptr0
+ %v = load i8, i8* %ptr
+ ret i8 %v
+}
+
+declare noalias i8* @malloc(i64)
+declare void @free(i8*)

ADD
tests/alive-tv/freshbid-malloc.tgt.ll
+define i8 @freshbid_malloc(i8* %ptr0) {
+ %ptr = call noalias i8* @malloc(i64 1)
+ store i8 10, i8* %ptr
+ store i8 20, i8* %ptr0
+ %v = load i8, i8* %ptr
+ ret i8 10
+}
+
+declare noalias i8* @malloc(i64)
+declare void @free(i8*)

let malloc be local as well, add comments and a few tests (#107)