fncall returning ptr: constrain ret val to allowed nonlocal bid
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -904,6 +904,15 @@ pair<expr, expr> Memory::mkUndefInput() const {
return { p.release(), move(offset) };
}
+expr Memory::mkFnRet(const char *name) const {
+ // TODO: can only alias with escaped local blocks!
+ Pointer p(*this, expr::mkVar(name, bits_for_bid + bits_for_offset));
+ state->addAxiom(expr::mkIf(p.is_local(),
+ p.get_short_bid().ule(num_locals - 1),
+ p.get_short_bid().ule(num_nonlocals - 1)));
+ return p.release();
+}
+
static expr disjoint_local_blocks(const Memory &m, const expr &addr,
const expr &sz, FunctionExpr &blk_addr) {
expr disj = true;

MODIFY
ir/memory.h
ir/memory.h
@@ -200,6 +200,7 @@ public:
smt::expr mkInput(const char *name) const;
std::pair<smt::expr, smt::expr> mkUndefInput() const;
+ smt::expr mkFnRet(const char *name) const;
// Allocates a new memory block and returns (pointer expr, allocated).
// If bid is not specified, it creates a fresh block id by increasing

MODIFY
ir/state.cpp
ir/state.cpp
@@ -205,7 +205,9 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
string npname = name + "#np";
for (auto t : out_types) {
values.emplace_back(
- expr::mkFreshVar(valname.c_str(), t->getDummyValue(false).value),
+ t->isPtrType()
+ ? memory.mkFnRet(valname.c_str())
+ : expr::mkFreshVar(valname.c_str(), t->getDummyValue(false).value),
expr::mkFreshVar(npname.c_str(), false));
}

MODIFY
tests/alive-tv/call.src.ll
tests/alive-tv/call.src.ll
@@ -35,7 +35,14 @@ define i8 @f6(i8* %p) {
ret i8 %b
}
+define void @f7() {
+ %ptr = call i8* @k()
+ %a = load i8, i8* %ptr, align 4
+ ret void
+}
+
declare i8 @g(i8*)
declare i8 @h(i8*) readnone
+declare i8* @k()
declare void @llvm.memcpy.p0i8.p0i8.i64(i8*, i8*, i64, i1)

MODIFY
tests/alive-tv/call.tgt.ll
tests/alive-tv/call.tgt.ll
@@ -33,7 +33,14 @@ define i8 @f6(i8* %p) {
ret i8 %b
}
+define void @f7() {
+ %ptr = call i8* @k()
+ %a = load i8, i8* %ptr, align 4
+ ret void
+}
+
declare i8 @g(i8*)
declare i8 @h(i8*) readnone
+declare i8* @k()
declare void @llvm.memcpy.p0i8.p0i8.i64(i8*, i8*, i64, i1)

fncall returning ptr: constrain ret val to allowed nonlocal bid