fix trim allowed set of fncall returned local ptrs
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1010,13 +1010,23 @@ pair<expr, expr> Memory::mkUndefInput(unsigned attributes) const {
return { p.release(), move(undef) };
}
-pair<expr,expr> Memory::mkFnRet(const char *name) const {
+pair<expr,expr>
+Memory::mkFnRet(const char *name, const vector<StateValue> &ptr_inputs) const {
// TODO: can only alias with escaped local blocks!
expr var
= expr::mkFreshVar(name, expr::mkUInt(0, bits_for_bid + bits_for_offset));
Pointer p(*this, var.concat_zeros(bits_for_ptrattrs));
+
+ // TODO: missing escaped local ptrs
+ expr local(false);
+ for (auto &in : ptr_inputs) {
+ Pointer inp(*this, in.value);
+ if (!inp.is_local().isFalse())
+ local |= in.non_poison && p.get_bid() == inp.get_bid();
+ }
+
state->addAxiom(expr::mkIf(p.is_local(),
- p.get_short_bid().ule(num_locals - 1),
+ local,
p.get_short_bid().ule(num_nonlocals - 1)));
return { p.release(), move(var) };
}

MODIFY
ir/memory.h
ir/memory.h
@@ -232,7 +232,8 @@ public:
smt::expr mkInput(const char *name, unsigned attributes) const;
std::pair<smt::expr, smt::expr> mkUndefInput(unsigned attributes) const;
- std::pair<smt::expr, smt::expr> mkFnRet(const char *name) const;
+ std::pair<smt::expr, smt::expr>
+ mkFnRet(const char *name, const std::vector<StateValue> &ptr_inputs) const;
CallState mkCallState() const;
void setState(const CallState &st);

MODIFY
ir/state.cpp
ir/state.cpp
@@ -200,9 +200,9 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
= fn_call_data[name].try_emplace({ move(inputs), move(ptr_inputs),
memory, reads_memory, argmemonly });
- auto mk_val = [this](const Type &t, const string &name) {
+ auto mk_val = [&](const Type &t, const string &name) {
if (t.isPtrType())
- return memory.mkFnRet(name.c_str());
+ return memory.mkFnRet(name.c_str(), get<1>(I->first));
auto v = expr::mkFreshVar(name.c_str(), t.getDummyValue(false).value);
return make_pair(v, v);

ADD
tests/alive-tv/call-fail.src.ll
+; ERROR: Value mismatch
+
+define i1 @f() {
+ %p = alloca i8, align 1
+ %call = call i8* @g(i8* %p)
+ %c = icmp eq i8* %p, %call
+ ret i1 %c
+}
+
+declare i8* @g(i8*)

ADD
tests/alive-tv/call-fail.tgt.ll
+define i1 @f() {
+ %p = alloca i8, align 1
+ %call = call i8* @g(i8* %p)
+ ret i1 false
+}
+
+declare i8* @g(i8*)

MODIFY
tests/alive-tv/call.src.ll
tests/alive-tv/call.src.ll
@@ -41,6 +41,13 @@ define void @f7() {
ret void
}
+define void @f8() {
+ %p = alloca i8, align 1
+ %call = call i8* @k()
+ %x = load i8, i8* %call, align 1
+ ret void
+}
+
declare i8 @g(i8*)
declare i8 @h(i8*) readnone
declare i8* @k()

MODIFY
tests/alive-tv/call.tgt.ll
tests/alive-tv/call.tgt.ll
@@ -39,6 +39,12 @@ define void @f7() {
ret void
}
+define void @f8() {
+ %call = call i8* @k()
+ %x = load i8, i8* %call, align 1
+ ret void
+}
+
declare i8 @g(i8*)
declare i8 @h(i8*) readnone
declare i8* @k()

fix #263: trim allowed set of fncall returned local ptrs