fix detect f(freeze(undef)) -> f(undef) as incorrect refinement
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1588,21 +1588,23 @@ void FnCall::print(ostream &os) const {
}
static void unpack_inputs(State &s, Value &argv, Type &ty,
- const ParamAttrs &argflag,
- StateValue value, vector<StateValue> &inputs,
+ const ParamAttrs &argflag, StateValue value,
+ StateValue value2, vector<StateValue> &inputs,
vector<Memory::PtrInput> &ptr_inputs) {
if (auto agg = ty.getAsAggregateType()) {
for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
unpack_inputs(s, argv, agg->getChild(i), argflag, agg->extract(value, i),
- inputs, ptr_inputs);
+ agg->extract(value2, i), inputs, ptr_inputs);
}
- } else {
+ return;
+ }
+
+ auto unpack = [&](StateValue &&value) {
if (ty.isPtrType()) {
Pointer p(s.getMemory(), move(value.value));
p.stripAttrs();
if (argflag.has(ParamAttrs::Dereferenceable))
- s.addUB(
- p.isDereferenceable(argflag.derefBytes, bits_byte / 8, false));
+ s.addUB(p.isDereferenceable(argflag.derefBytes, bits_byte / 8, false));
if (argflag.has(ParamAttrs::NonNull))
s.addUB(p.isNonZero());
@@ -1613,7 +1615,9 @@ static void unpack_inputs(State &s, Value &argv, Type &ty,
} else {
inputs.emplace_back(move(value));
}
- }
+ };
+ unpack(move(value));
+ unpack(move(value2));
}
static void unpack_ret_ty (vector<Type*> &out_types, Type &ty) {
@@ -1674,13 +1678,22 @@ StateValue FnCall::toSMT(State &s) const {
ostringstream fnName_mangled;
fnName_mangled << fnName;
for (auto &[arg, flags] : args) {
- StateValue sv;
- if (flags.poisonImpliesUB())
+ // we duplicate each argument so that undef values are allowed to take
+ // different values so we can catch the bug in f(freeze(undef)) -> f(undef)
+ StateValue sv, sv2;
+ if (flags.poisonImpliesUB()) {
sv = s.getAndAddPoisonUB(*arg, flags.undefImpliesUB());
+ if (flags.undefImpliesUB())
+ sv2 = sv;
else
+ sv2 = s.getAndAddPoisonUB(*arg, false);
+ } else {
sv = s[*arg];
+ sv2 = s[*arg];
+ }
- unpack_inputs(s, *arg, arg->getType(), flags, sv, inputs, ptr_inputs);
+ unpack_inputs(s, *arg, arg->getType(), flags, move(sv), move(sv2), inputs,
+ ptr_inputs);
fnName_mangled << '#' << arg->getType();
}
fnName_mangled << '!' << getType();

MODIFY
ir/state.cpp
ir/state.cpp
@@ -472,15 +472,15 @@ expr State::FnCallInput::refinedBy(
!fncall_ranges.overlaps(fncall_ranges2))
return false;
- expr refines(true);
+ AndExpr refines;
for (unsigned i = 0, e = args_nonptr.size(); i != e; ++i) {
- refines &= args_nonptr[i].non_poison.implies(
+ refines.add(args_nonptr[i].non_poison.implies(
args_nonptr[i].value == args_nonptr2[i].value &&
- args_nonptr2[i].non_poison);
+ args_nonptr2[i].non_poison));
}
- if (refines.isFalse())
- return refines;
+ if (!refines)
+ return false;
set<expr> undef_vars;
for (unsigned i = 0, e = args_ptr.size(); i != e; ++i) {
@@ -494,10 +494,10 @@ expr State::FnCallInput::refinedBy(
expr eq_val = Pointer(m, ptr_in.value)
.fninputRefined(Pointer(m2, ptr_in2.value),
undef_vars, is_byval2);
- refines &= ptr_in.non_poison.implies(eq_val && ptr_in2.non_poison);
+ refines.add(ptr_in.non_poison.implies(eq_val && ptr_in2.non_poison));
- if (refines.isFalse())
- return refines;
+ if (!refines)
+ return false;
}
for (auto &v : undef_vars)
@@ -506,12 +506,12 @@ expr State::FnCallInput::refinedBy(
if (readsmem) {
auto restrict_ptrs = argmemonly2 ? &args_ptr2 : nullptr;
auto data = m.refined(m2, true, restrict_ptrs);
- refines &= get<0>(data);
+ refines.add(get<0>(data));
for (auto &v : get<2>(data))
s.addFnQuantVar(v);
}
- return refines;
+ return refines();
}
bool State::FnCallInput::operator<(const FnCallInput &rhs) const {

ADD
tests/alive-tv/calls/call-freeze.srctgt.ll
+define i8 @src(i8 %x) {
+ %freeze = freeze i8 undef
+ %r = call i8 @f(i8 %freeze)
+ ret i8 %r
+}
+
+define i8 @tgt(i8 %x) {
+ %r = call i8 @f(i8 undef)
+ ret i8 %r
+}
+
+declare i8 @f(i8)

fix #499: detect f(freeze(undef)) -> f(undef) as incorrect refinement