New fncall encoding
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1659,24 +1659,29 @@ Memory::mkFnRet(const char *name, const vector<PtrInput> &ptr_inputs) {
return { p.release(), move(var) };
}
-expr Memory::CallState::implies(const CallState &st) const {
- if (empty || st.empty)
- return true;
- // NOTE: using equality here is an approximation.
- // TODO: benchmark using quantifiers to state implication
- expr ret(true);
- for (unsigned i = 0, e = non_local_block_val.size(); i != e; ++i) {
- ret &= non_local_block_val[i] == st.non_local_block_val[i];
- }
- if (liveness_var.isValid() && st.liveness_var.isValid())
- ret &= liveness_var == st.liveness_var;
+Memory::CallState Memory::CallState::mkIf(const expr &cond,
+ const CallState &then,
+ const CallState &els) {
+ CallState ret;
+ for (unsigned i = 0, e = then.non_local_block_val.size(); i != e; ++i) {
+ ret.non_local_block_val.emplace_back(
+ expr::mkIf(cond, then.non_local_block_val[i],
+ els.non_local_block_val[i]));
+ }
+ ret.non_local_block_liveness
+ = expr::mkIf(cond, then.non_local_block_liveness,
+ els.non_local_block_liveness);
return ret;
}
+bool Memory::CallState::operator<(const CallState &rhs) const {
+ return tie(non_local_block_val, non_local_block_liveness) <
+ tie(rhs.non_local_block_val, rhs.non_local_block_liveness);
+}
+
Memory::CallState
Memory::mkCallState(const vector<PtrInput> *ptr_inputs, bool nofree) const {
CallState st;
- st.empty = false;
// TODO: handle havoc of local blocks
@@ -1723,10 +1728,10 @@ Memory::mkCallState(const vector<PtrInput> *ptr_inputs, bool nofree) const {
if (mask.isAllOnes()) {
st.non_local_block_liveness = non_local_block_liveness;
} else {
- st.liveness_var = expr::mkFreshVar("blk_liveness", mk_liveness_array());
+ auto liveness_var = expr::mkFreshVar("blk_liveness", mk_liveness_array());
// functions can free an object, but cannot bring a dead one back to live
st.non_local_block_liveness
- = non_local_block_liveness & (st.liveness_var | mask);
+ = non_local_block_liveness & (liveness_var | mask);
}
} else {
st.non_local_block_liveness = non_local_block_liveness;
@@ -2225,12 +2230,18 @@ expr Memory::blockRefined(const Pointer &src, const Pointer &tgt, unsigned bid,
assert(src.isWritable().eq(tgt.isWritable()));
+ expr aligned(true);
+ expr src_align = src.blockAlignment();
+ expr tgt_align = tgt.blockAlignment();
+ // if they are both non-const, then the condition holds per the precondition
+ if (src_align.isConst() || tgt_align.isConst())
+ aligned = src_align.ule(tgt_align);
+
expr alive = src.isBlockAlive();
return alive == tgt.isBlockAlive() &&
blk_size == tgt.blockSize() &&
src.getAllocType() == tgt.getAllocType() &&
- state->simplifyWithAxioms(
- src.blockAlignment().ule(tgt.blockAlignment())) &&
+ aligned &&
alive.implies(val_refines);
}
@@ -2364,8 +2375,7 @@ Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {
bool Memory::operator<(const Memory &rhs) const {
// FIXME: remove this once we move to C++20
- // NOTE: we don't compare field state so that memories from src/tgt can
- // compare equal
+ assert(state == rhs.state);
return
tie(non_local_block_val, local_block_val,
non_local_block_liveness, local_block_liveness, local_blk_addr,
@@ -2382,6 +2392,32 @@ bool Memory::operator<(const Memory &rhs) const {
rhs.ptr_alias, rhs.next_nonlocal_bid);
}
+bool Memory::cmpFnCallInput(const Memory &rhs) const {
+ assert(state == rhs.state && state->isSource());
+ // first compare non-local memory only
+ auto nla = tie(non_local_block_val, non_local_block_liveness,
+ non_local_blk_size, non_local_blk_align, non_local_blk_kind,
+ byval_blks, escaped_local_blks);
+ auto nlb = tie(rhs.non_local_block_val, rhs.non_local_block_liveness,
+ rhs.non_local_blk_size, rhs.non_local_blk_align,
+ rhs.non_local_blk_kind, rhs.byval_blks,
+ rhs.escaped_local_blks);
+ if (nla < nlb)
+ return true;
+ if (nla > nlb)
+ return false;
+
+ // if nothing local escaped, then memories are equivalent for the callee
+ if (escaped_local_blks.numMayAlias(true) == 0)
+ return false;
+
+ return
+ tie(local_block_val, local_block_liveness, local_blk_addr, local_blk_size,
+ local_blk_align, local_blk_kind) <
+ tie(rhs.local_block_val, rhs.local_block_liveness, rhs.local_blk_addr,
+ rhs.local_blk_size, rhs.local_blk_align, rhs.local_blk_kind);
+}
+
#define P(name, expr) do { \
auto v = m.eval(expr, false); \
uint64_t n; \

MODIFY
ir/memory.h
ir/memory.h
@@ -318,11 +318,12 @@ public:
class CallState {
std::vector<smt::expr> non_local_block_val;
smt::expr non_local_block_liveness;
- smt::expr liveness_var;
- bool empty = true;
public:
- smt::expr implies(const CallState &st) const;
+ static CallState mkIf(const smt::expr &cond, const CallState &then,
+ const CallState &els);
+ // for container use only
+ bool operator<(const CallState &rhs) const;
friend class Memory;
};
@@ -411,6 +412,7 @@ public:
// for container use only
bool operator<(const Memory &rhs) const;
+ bool cmpFnCallInput(const Memory &rhs) const;
static void printAliasStats(std::ostream &os) {
AliasSet::printStats(os);

MODIFY
ir/state.cpp
ir/state.cpp
@@ -219,9 +219,6 @@ const StateValue& State::operator[](const Value &val) {
if (is_non_undef) {
// We don't need to add uvar to undef_vars
- // We add it to quantified_vars as a safety net because the current
- // encoding of function call may lose uvars to be quantified, currently.
- // They should be optimized ideally if never used.
quantified_vars.insert(uvars.begin(), uvars.end());
return simplify(sval, true);
}
@@ -465,6 +462,92 @@ void State::addNoReturn() {
addUB(expr(false));
}
+expr State::FnCallInput::refinedBy(
+ State &s, const vector<StateValue> &args_nonptr2,
+ const vector<Memory::PtrInput> &args_ptr2,
+ const ValueAnalysis::FnCallRanges &fncall_ranges2,
+ const Memory &m2, bool readsmem2, bool argmemonly2) const {
+
+ if (readsmem != readsmem2 || argmemonly != argmemonly2 ||
+ !fncall_ranges.overlaps(fncall_ranges2))
+ return false;
+
+ expr refines(true);
+ for (unsigned i = 0, e = args_nonptr.size(); i != e; ++i) {
+ refines &= args_nonptr[i].non_poison.implies(
+ args_nonptr[i].value == args_nonptr2[i].value &&
+ args_nonptr2[i].non_poison);
+ }
+
+ if (refines.isFalse())
+ return refines;
+
+ set<expr> undef_vars;
+ for (unsigned i = 0, e = args_ptr.size(); i != e; ++i) {
+ // TODO: needs to take read/read2 as input to control if mem blocks
+ // need to be compared
+ auto &[ptr_in, is_byval, is_nocapture] = args_ptr[i];
+ auto &[ptr_in2, is_byval2, is_nocapture2] = args_ptr2[i];
+ if (is_byval != is_byval2 || is_nocapture != is_nocapture2)
+ return false;
+
+ 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);
+
+ if (refines.isFalse())
+ return refines;
+ }
+
+ for (auto &v : undef_vars)
+ s.addFnQuantVar(v);
+
+ if (readsmem) {
+ auto restrict_ptrs = argmemonly2 ? &args_ptr2 : nullptr;
+ auto data = m.refined(m2, true, restrict_ptrs);
+ refines &= get<0>(data);
+ for (auto &v : get<2>(data))
+ s.addFnQuantVar(v);
+ }
+
+ return refines;
+}
+
+bool State::FnCallInput::operator<(const FnCallInput &rhs) const {
+ return tie(args_nonptr, args_ptr, fncall_ranges, m, readsmem, argmemonly) <
+ tie(rhs.args_nonptr, rhs.args_ptr, rhs.fncall_ranges, rhs.m,
+ rhs.readsmem, rhs.argmemonly);
+#if 0
+ auto a = tie(args_nonptr, args_ptr, fncall_ranges, readsmem, argmemonly);
+ auto b = tie(rhs.args_nonptr, rhs.args_ptr, rhs.fncall_ranges, rhs.readsmem,
+ rhs.argmemonly);
+ if (a < b)
+ return true;
+ if (a > b)
+ return false;
+ return m.cmpFnCallInput(rhs.m);
+#endif
+}
+
+State::FnCallOutput State::FnCallOutput::mkIf(const expr &cond,
+ const FnCallOutput &a,
+ const FnCallOutput &b) {
+ FnCallOutput ret;
+ ret.ub = expr::mkIf(cond, a.ub, b.ub);
+ ret.callstate = Memory::CallState::mkIf(cond, a.callstate, b.callstate);
+ assert(a.retvals.size() == b.retvals.size());
+ for (unsigned i = 0, e = a.retvals.size(); i != e; ++i) {
+ ret.retvals.emplace_back(
+ StateValue::mkIf(cond, a.retvals[i], b.retvals[i]));
+ }
+ return ret;
+}
+
+bool State::FnCallOutput::operator<(const FnCallOutput &rhs) const {
+ return tie(retvals, ub, callstate) < tie(rhs.retvals, rhs.ub, rhs.callstate);
+}
+
vector<StateValue>
State::addFnCall(const string &name, vector<StateValue> &&inputs,
vector<Memory::PtrInput> &&ptr_inputs,
@@ -491,7 +574,10 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
memory.escapeLocalPtr(v.val.value);
}
- // TODO: this doesn't need to compare the full memory, just a subset of fields
+ vector<StateValue> retval;
+
+ // source may create new fn symbols, target just references src symbols
+ if (isSource()) {
auto call_data_pair
= fn_call_data[name].try_emplace({ move(inputs), move(ptr_inputs),
analysis.ranges_fn_calls,
@@ -502,18 +588,19 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
if (inserted) {
auto mk_val = [&](const Type &t, const string &name) {
- if (t.isPtrType())
- return memory.mkFnRet(name.c_str(), I->first.args_ptr).first;
-
- return expr::mkFreshVar(name.c_str(), t.getDummyValue(false).value);
+ return t.isPtrType()
+ // TODO: remove 2nd ret val of mkFnRet
+ ? memory.mkFnRet(name.c_str(), I->first.args_ptr).first
+ : expr::mkFreshVar(name.c_str(), t.getDummyValue(false).value);
};
vector<StateValue> values;
string valname = name + "#val";
string npname = name + "#np";
for (auto t : out_types) {
- expr np = noundef ? expr(true) : expr::mkFreshVar(npname.c_str(), false);
- values.emplace_back(mk_val(*t, valname), move(np));
+ values.emplace_back(
+ mk_val(*t, valname),
+ noundef ? expr(true) : expr::mkFreshVar(npname.c_str(), false));
}
string ub_name = name + "#ub";
@@ -522,10 +609,42 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
writes_memory
? memory.mkCallState(argmemonly ? &I->first.args_ptr : nullptr,
attrs.has(FnAttrs::NoFree))
- : Memory::CallState(),
- true };
+ : Memory::CallState() };
+ }
+
+ addUB(I->second.ub);
+ retval = I->second.retvals;
+ if (writes_memory)
+ memory.setState(I->second.callstate);
+ }
+ else {
+ // target: this fn call must match one from the source, otherwise it's UB
+ ChoiceExpr<FnCallOutput> data;
+
+ for (auto &[in, out] : fn_call_data[name]) {
+ auto refined = in.refinedBy(*this, inputs, ptr_inputs,
+ analysis.ranges_fn_calls, memory,
+ reads_memory, argmemonly);
+ data.add(out, move(refined));
+ }
+
+ if (data) {
+ auto [d, domain, qvar, pre] = data();
+ addUB(move(domain));
+ addUB(move(d.ub));
+ retval = move(d.retvals);
+ if (writes_memory)
+ memory.setState(d.callstate);
+
+ fn_call_pre &= pre;
+ if (qvar.isValid())
+ fn_call_qvars.emplace(move(qvar));
} else {
- I->second.used = true;
+ addUB(expr(false));
+ for (auto *t : out_types) {
+ retval.emplace_back(t->getDummyValue(false));
+ }
+ }
}
if (writes_memory) {
@@ -536,12 +655,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
}
}
- addUB(I->second.ub);
-
- if (writes_memory)
- memory.setState(I->second.callstate);
-
- return I->second.retvals;
+ return retval;
}
void State::useUnsupported(const char *name) {
@@ -552,6 +666,10 @@ void State::addQuantVar(const expr &var) {
quantified_vars.emplace(var);
}
+void State::addFnQuantVar(const expr &var) {
+ fn_call_qvars.emplace(var);
+}
+
void State::addUndefVar(expr &&var) {
undef_vars.emplace(move(var));
}
@@ -626,99 +744,12 @@ void State::syncSEdataWithSrc(const State &src) {
itm.second.second = false;
fn_call_data = src.fn_call_data;
- for (auto &[fn, map] : fn_call_data) {
- (void)fn;
- for (auto &[in, data] : map) {
- (void)in;
- data.used = false;
- }
- }
-
memory.syncWithSrc(src.returnMemory());
}
void State::mkAxioms(State &tgt) {
assert(isSource() && !tgt.isSource());
returnMemory().mkAxioms(tgt.returnMemory());
-
- // axioms for function calls
- // We would potentially need to do refinement check of tgt x tgt, but it
- // doesn't seem to be needed in practice for optimizations
- // since there's no introduction of calls in tgt
- for (auto &[fn, data] : fn_call_data) {
- auto &data2 = tgt.fn_call_data.at(fn);
-
- for (auto I = data.begin(), E = data.end(); I != E; ++I) {
- auto &[ins, ptr_ins, fn_ranges, mem, reads, argmem] = I->first;
- auto &[rets, ub, mem_state, used] = I->second;
- assert(used); (void)used;
-
- for (auto I2 = data2.begin(), E2 = data2.end(); I2 != E2; ++I2) {
- auto &[ins2, ptr_ins2, fn_ranges2, mem2, reads2, argmem2] = I2->first;
- auto &[rets2, ub2, mem_state2, used2] = I2->second;
-
- if (!used2 || reads != reads2 || argmem != argmem2 ||
- !fn_ranges.overlaps(fn_ranges2) || ub.eq(ub2))
- continue;
-
- expr refines(true);
- for (unsigned i = 0, e = ins.size(); i != e; ++i) {
- refines &= ins[i].non_poison.implies(ins[i].value == ins2[i].value &&
- ins2[i].non_poison);
- }
-
- if (refines.isFalse())
- continue;
-
- set<expr> undef_vars;
- for (unsigned i = 0, e = ptr_ins.size(); i != e; ++i) {
- // TODO: needs to take read/read2 as input to control if mem blocks
- // need to be compared
- auto &[ptr_in, is_byval, is_nocapture] = ptr_ins[i];
- auto &[ptr_in2, is_byval2, is_nocapture2] = ptr_ins2[i];
- if (is_byval != is_byval2 || is_nocapture != is_nocapture2) {
- refines = false;
- break;
- }
-
- expr eq_val = Pointer(mem, ptr_in.value)
- .fninputRefined(Pointer(mem2, ptr_in2.value),
- undef_vars, is_byval2);
- refines &= ptr_in.non_poison
- .implies(eq_val && ptr_in2.non_poison);
-
- if (refines.isFalse())
- break;
- }
-
- if (refines.isFalse())
- continue;
-
- quantified_vars.insert(undef_vars.begin(), undef_vars.end());
-
- if (reads2) {
- auto restrict_ptrs = argmem2 ? &ptr_ins2 : nullptr;
- auto data = mem.refined(mem2, true, restrict_ptrs);
- refines &= get<0>(data);
- quantified_vars.insert(get<2>(data).begin(), get<2>(data).end());
- }
-
- expr ref_expr(true);
- for (unsigned i = 0, e = rets.size(); i != e; ++i) {
- ref_expr &=
- rets[i].non_poison.implies(rets2[i].non_poison &&
- rets[i].value == rets2[i].value);
- }
- tgt.addPre(refines.implies(ref_expr &&
- ub.implies(ub2) &&
- mem_state.implies(mem_state2)));
- }
- }
- }
-}
-
-expr State::simplifyWithAxioms(expr &&e) const {
- return axioms.contains(e) ? expr(true) : move(e);
}
}

MODIFY
ir/state.h
ir/state.h
@@ -116,20 +116,26 @@ private:
Memory m;
bool readsmem, argmemonly;
- bool operator<(const FnCallInput &rhs) const {
- return std::tie(args_nonptr, args_ptr, fncall_ranges, m, readsmem,
- argmemonly) <
- std::tie(rhs.args_nonptr, rhs.args_ptr, rhs.fncall_ranges, rhs.m,
- rhs.readsmem, rhs.argmemonly);
- }
+ smt::expr refinedBy(State &s, const std::vector<StateValue> &args_nonptr,
+ const std::vector<Memory::PtrInput> &args_ptr,
+ const ValueAnalysis::FnCallRanges &fncall_ranges,
+ const Memory &m, bool readsmem, bool argmemonly) const;
+
+ bool operator<(const FnCallInput &rhs) const;
};
+
struct FnCallOutput {
std::vector<StateValue> retvals;
smt::expr ub;
Memory::CallState callstate;
- bool used;
+
+ static FnCallOutput mkIf(const smt::expr &cond, const FnCallOutput &then,
+ const FnCallOutput &els);
+ bool operator<(const FnCallOutput &rhs) const;
};
std::map<std::string, std::map<FnCallInput, FnCallOutput>> fn_call_data;
+ smt::expr fn_call_pre = true;
+ std::set<smt::expr> fn_call_qvars;
public:
State(Function &f, bool source);
@@ -175,6 +181,7 @@ public:
auto& getUnsupported() const { return used_unsupported; }
void addQuantVar(const smt::expr &var);
+ void addFnQuantVar(const smt::expr &var);
void addUndefVar(smt::expr &&var);
auto& getUndefVars() const { return undef_vars; }
void resetUndefVars();
@@ -189,8 +196,10 @@ public:
auto& getMemory() { return memory; }
auto& getAxioms() const { return axioms; }
auto& getPre() const { return precondition; }
+ auto& getFnPre() const { return fn_call_pre; }
const auto& getValues() const { return values; }
const auto& getQuantVars() const { return quantified_vars; }
+ const auto& getFnQuantVars() const { return fn_call_qvars; }
auto& functionDomain() const { return function_domain; }
auto& returnDomain() const { return return_domain; }
@@ -215,7 +224,6 @@ public:
void syncSEdataWithSrc(const State &src);
void mkAxioms(State &tgt);
- smt::expr simplifyWithAxioms(smt::expr &&e) const;
private:
void addJump(const BasicBlock &dst, smt::expr &&domain);

MODIFY
smt/exprs.h
smt/exprs.h
// Distributed under the MIT license that can be found in the LICENSE file.
#include "smt/expr.h"
+#include "util/compiler.h"
#include <cassert>
#include <map>
#include <ostream>
#include <set>
+#include <tuple>
#include <utility>
namespace smt {
@@ -106,6 +108,62 @@ public:
};
+// non-deterministic choice of one of the options with potentially overlapping
+// domains
+template <typename T>
+class ChoiceExpr {
+ std::map<T, expr> vals; // val -> domain
+
+public:
+ template <typename V, typename D>
+ void add(V &&val, D &&domain) {
+ if (domain.isFalse())
+ return;
+ auto [I, inserted] = vals.try_emplace(std::forward<V>(val),
+ std::forward<D>(domain));
+ if (!inserted)
+ I->second |= std::forward<D>(domain);
+ }
+
+ operator bool() const {
+ return !vals.empty();
+ }
+
+ expr domain() const {
+ OrExpr ret;
+ for (auto &p : vals) {
+ ret.add(expr(p.second));
+ }
+ return ret();
+ }
+
+ // returns: data, domain, quant var, precondition
+ std::tuple<T,expr,expr,expr> operator()() const {
+ expr dom = domain();
+ if (vals.size() == 1)
+ return { vals.begin()->first, vals.begin()->second, expr(), true };
+
+ unsigned bits = util::ilog2_ceil(vals.size()+1, false);
+ expr qvar = expr::mkFreshVar("choice", expr::mkUInt(0, bits));
+
+ T ret;
+ expr pre = !dom;
+ auto I = vals.begin();
+ bool first = true;
+
+ for (unsigned i = vals.size(); i > 0; --i) {
+ auto cmp = qvar == (i-1);
+ pre = expr::mkIf(cmp, I->second, pre);
+ ret = first ? I->first : T::mkIf(cmp, I->first, ret);
+ first = false;
+ ++I;
+ }
+
+ return { std::move(ret), std::move(dom), std::move(qvar), std::move(pre) };
+ }
+};
+
+
class FunctionExpr {
std::map<expr, expr> fn; // key -> val
std::optional<expr> default_val;

RENAME
tests/alive-tv/fncall-noreturn.srctgt.ll
tests/alive-tv/calls/fncall-noreturn.srctgt.ll
ADD
tests/alive-tv/calls/fncall-noreturn2.srctgt.ll
+define void @fn(i32 %code, i1 %c) {
+ br i1 %c, label %then, label %else
+
+then:
+ call void @exit(i32 0)
+ unreachable
+
+else:
+ call void @exit(i32 %code)
+ unreachable
+}
+
+declare void @exit(i32) noreturn

RENAME
tests/alive-tv/fncall-vararg.src.ll
tests/alive-tv/calls/fncall-vararg.srctgt.ll
-target triple = "x86_64-unknown-linux-gnu"
+; ERROR: Source is more defined than target
+target triple = "x86_64-unknown-linux-gnu"
declare void @g(i8*, ...)
-define void @f() {
+
+define void @src() {
tail call void (i8*, ...) @g(i8* null, i32 0)
ret void
}
-; ERROR: Source is more defined than target
+
+define void @tgt() {
+ tail call void (i8*, ...) @g(i8* null)
+ ret void
+}

DELETE
tests/alive-tv/fncall-vararg.tgt.ll
-target triple = "x86_64-unknown-linux-gnu"
-
-declare void @g(i8*, ...)
-define void @f() {
- tail call void (i8*, ...) @g(i8* null)
- ret void
-}

RENAME
tests/alive-tv/br-undef.srctgt.ll
tests/alive-tv/undef/br-undef4.srctgt.ll
ADD
tests/alive-tv/undef/fncall-freeze.srctgt.ll
+; ERROR: Source is more defined than target
+
+declare void @foo_i8(i8)
+
+define void @src(i8 %x, i8 %y) {
+ %cond.fr = freeze i1 undef
+ %s = select i1 %cond.fr, i8 %x, i8 0
+ %s2 = select i1 %cond.fr, i8 0, i8 %x
+ call void @foo_i8(i8 %s)
+ call void @foo_i8(i8 %s2)
+ ret void
+}
+
+define void @tgt(i8 %x, i8 %y) {
+ call void @foo_i8(i8 0)
+ call void @foo_i8(i8 0)
+ ret void
+}

ADD
tests/alive-tv/undef/fncall-freeze2.srctgt.ll
+; ERROR: Value mismatch
+
+declare i8 @foo_i8(i8) readonly
+
+define i8 @src(i8 %x, i8 %y) {
+ %cond.fr = freeze i1 undef
+ %s = select i1 %cond.fr, i8 %x, i8 0
+ %s2 = select i1 %cond.fr, i8 0, i8 %x
+ %a = call i8 @foo_i8(i8 %s)
+ %b = call i8 @foo_i8(i8 %s2)
+ %c = add i8 %a, %b
+ ret i8 %c
+}
+
+define i8 @tgt(i8 %x, i8 %y) {
+ %a = call i8 @foo_i8(i8 0)
+ %b = call i8 @foo_i8(i8 0)
+ %c = add i8 %a, %b
+ ret i8 %c
+}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -345,6 +345,8 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
auto &uvars = ap.second;
auto qvars = src_state.getQuantVars();
qvars.insert(ap.second.begin(), ap.second.end());
+ auto &fn_qvars = tgt_state.getFnQuantVars();
+ qvars.insert(fn_qvars.begin(), fn_qvars.end());
auto err = [&](const Result &r, print_var_val_ty print, const char *msg) {
error(errs, src_state, tgt_state, r, var, msg, check_each_var, print);
@@ -393,6 +395,7 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
}
}
expr pre = pre_src_exists && pre_tgt;
+ pre_src_forall &= tgt_state.getFnPre();
auto [poison_cnstr, value_cnstr] = type.refines(src_state, tgt_state, a, b);
expr undef_cnstr = encode_undef_refinement(type, ap, bp);

New fncall encoding (#498)