Encode call site refinement without using quantified variables
MODIFY
ir/state.cpp
ir/state.cpp
@@ -279,21 +279,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
if (writes_memory)
memory.setState(I->second.callstate);
- if (all_args_np.isTrue())
return I->second.retvals;
-
- // if any of the arguments is poison, yield an arbitrary value, such that
- // f(poison) -> f(42) works
- vector<StateValue> ret;
- auto T = out_types.begin();
- auto var_name = name + "#pval";
- for (auto &[v, np] : I->second.retvals) {
- auto [val_poison, var] = mk_val(**T, var_name);
- ret.emplace_back(expr::mkIf(all_args_np, v, val_poison), expr(np));
- addQuantVar(move(var));
- ++T;
- }
- return ret;
}
void State::addQuantVar(const expr &var) {
@@ -409,14 +395,16 @@ void State::mkAxioms(State &tgt) {
if (!used2 || reads != reads2 || argmem != argmem2)
continue;
- expr refines(true), is_val_eq(true);
+ expr refines(true);
for (unsigned i = 0, e = ins.size(); i != e; ++i) {
- expr eq_val = ins[i].value == ins2[i].value;
- is_val_eq &= eq_val;
- refines &= ins[i].non_poison.implies(eq_val && ins2[i].non_poison);
+ string used = fn + "#arg" + to_string(i) + "used";
+ refines &=
+ expr::mkBoolVar(used.c_str()).implies(
+ ins[i].non_poison.implies(ins[i].value == ins2[i].value &&
+ ins2[i].non_poison));
}
- if (is_val_eq.isFalse() && refines.isFalse())
+ if (refines.isFalse())
continue;
for (unsigned i = 0, e = ptr_ins.size(); i != e; ++i) {
@@ -431,7 +419,6 @@ void State::mkAxioms(State &tgt) {
}
expr eq_val = Pointer(mem, ptr_in.value)
.fninputRefined(Pointer(mem2, ptr_in2.value), is_byval2);
- is_val_eq &= eq_val;
refines &= ptr_in.non_poison
.implies(eq_val && ptr_in2.non_poison);
}
@@ -439,16 +426,15 @@ void State::mkAxioms(State &tgt) {
if (reads2) {
auto restrict_ptrs = argmem2 ? &ptr_ins2 : nullptr;
expr mem_refined = mem.refined(mem2, true, restrict_ptrs).first;
- is_val_eq &= mem_refined;
refines &= mem_refined;
}
- expr ref_expr(true), eq_expr(true);
+ expr ref_expr(true);
for (unsigned i = 0, e = rets.size(); i != e; ++i) {
- eq_expr &= rets[i].value == rets2[i].value;
- ref_expr &= rets[i].non_poison.implies(rets2[i].non_poison);
+ ref_expr &=
+ rets[i].non_poison.implies(rets2[i].non_poison &&
+ rets[i].value == rets2[i].value);
}
- tgt.addPre(is_val_eq.implies(eq_expr));
tgt.addPre(refines.implies(ref_expr &&
ub.implies(ub2) &&
mem_state.implies(mem_state2)));

MODIFY
tests/alive-tv/call.src.ll
tests/alive-tv/call.src.ll
@@ -68,9 +68,17 @@ define void @f8() {
ret void
}
+define void @f9() {
+ %poison = sub nuw i32 0, 1
+ call void @j(i32 %poison)
+ call void @j(i32 %poison)
+ ret void
+}
+
declare i8 @g(i8*)
declare i8 @g2(i8* byval)
declare i8 @h(i8*) readnone
+declare void @j(i32)
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
@@ -61,9 +61,16 @@ define void @f8() {
ret void
}
+define void @f9() {
+ call void @j(i32 3)
+ call void @j(i32 4)
+ ret void
+}
+
declare i8 @g(i8*)
declare i8 @g2(i8* byval)
declare i8 @h(i8*) readnone
+declare void @j(i32)
declare i8* @k()
declare void @llvm.memcpy.p0i8.p0i8.i64(i8*, i8*, i64, i1)

MODIFY
tests/unit/call-error5.opt
tests/unit/call-error5.opt
@@ -5,4 +5,4 @@ ret i8 %d
=>
ret i8 1
-; FIXME: this test should fail!
+; ERROR: Value mismatch

Encode call site refinement without using quantified variables (#381)