Let the initial memory have pointers to non-local blocks only
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -372,9 +372,17 @@ Memory::Memory(State &state) : state(&state) {
blocks_val = mk_val_array("blks_val");
blocks_liveness = mk_liveness_uf();
{
+ Pointer idx(*this, "#idx0");
+
+ // All non-local blocks cannot initially contain pointers to local blocks.
+ auto byte = Byte(*this, blocks_val.load(idx()));
+ Pointer loadedptr(*this, byte.ptr_value());
+ expr cond = byte.is_ptr() == 0 || byte.ptr_nonpoison() == 0 ||
+ !loadedptr.is_local();
+ state.addPre(expr::mkForAll({ idx() }, move(cond)));
+
// initialize all local blocks as non-pointer, poison value
// This is okay because loading a pointer as non-pointer is also poison.
- Pointer idx(*this, "#idx0");
expr is_local = idx.is_local();
expr val = expr::mkIf(is_local, expr::mkUInt(0, bitsByte()),
blocks_val.load(idx()));

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

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

RENAME
tests/alive-tv/memory/freshbid-malloc.src.ll
tests/alive-tv/memory/freshbid-malloc-1.src.ll
+; target: 64 bits ptr addr
+target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
+
define i8 @freshbid_malloc(i8* %ptr0) {
%ptr = call noalias i8* @malloc(i64 1)
+ %i = ptrtoint i8* %ptr to i64
+ %cmp = icmp eq i64 %i, 0
+ br i1 %cmp, label %BB1, label %BB2
+BB1:
+ ret i8 0
+BB2:
store i8 10, i8* %ptr
store i8 20, i8* %ptr0
%v = load i8, i8* %ptr

RENAME
tests/alive-tv/memory/freshbid-malloc.tgt.ll
tests/alive-tv/memory/freshbid-malloc-1.tgt.ll
+; target: 64 bits ptr addr
+target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
+
define i8 @freshbid_malloc(i8* %ptr0) {
%ptr = call noalias i8* @malloc(i64 1)
+ %i = ptrtoint i8* %ptr to i64
+ %cmp = icmp eq i64 %i, 0
+ br i1 %cmp, label %BB1, label %BB2
+BB1:
+ ret i8 0
+BB2:
store i8 10, i8* %ptr
store i8 20, i8* %ptr0
%v = load i8, i8* %ptr

ADD
tests/alive-tv/memory/freshbid-malloc-2.src.ll
+; target: 64 bits ptr addr
+target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
+
+define i8 @freshbid_malloc(i8** %pptr) {
+ %ptr = call noalias i8* @malloc(i64 1)
+ %ptr0 = load i8*, i8** %pptr
+ %i = ptrtoint i8* %ptr to i64
+ %cmp = icmp eq i64 %i, 0
+ br i1 %cmp, label %BB1, label %BB2
+BB1:
+ ret i8 0
+BB2:
+ 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/memory/freshbid-malloc-2.tgt.ll
+; target: 64 bits ptr addr
+target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
+
+define i8 @freshbid_malloc(i8** %pptr) {
+ %ptr = call noalias i8* @malloc(i64 1)
+ %ptr0 = load i8*, i8** %pptr
+ %i = ptrtoint i8* %ptr to i64
+ %cmp = icmp eq i64 %i, 0
+ br i1 %cmp, label %BB1, label %BB2
+BB1:
+ ret i8 0
+BB2:
+ 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*)

RENAME
tests/alive-tv/memory/glb-arg-noalias-fail.src.ll
tests/alive-tv/memory/glb-arg-noalias-fail-1.src.ll
RENAME
tests/alive-tv/memory/glb-arg-noalias-fail.tgt.ll
tests/alive-tv/memory/glb-arg-noalias-fail-1.tgt.ll
ADD
tests/alive-tv/memory/glb-arg-noalias-fail-2.src.ll
+@glb = global i8 0
+
+define i8 @glb_arg_noalias(i8** %pptr) {
+ %ptr = load i8*, i8** %pptr
+ store i8 10, i8* %ptr
+ store i8 20, i8* @glb
+ %v = load i8, i8* %ptr
+ ret i8 %v
+}
+
+; ERROR: Value mismatch

ADD
tests/alive-tv/memory/glb-arg-noalias-fail-2.tgt.ll
+@glb = global i8 0
+
+define i8 @glb_arg_noalias(i8** %pptr) {
+ %ptr = load i8*, i8** %pptr
+ store i8 10, i8* %ptr
+ store i8 20, i8* @glb
+ ret i8 10
+}
+
+; ERROR: Value mismatch

Let the initial memory have pointers to non-local blocks only (#121)