support removal of duplicated readonly function calls
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1617,6 +1617,12 @@ pair<expr, expr> Memory::mkUndefInput(const ParamAttrs &attrs) const {
return { p.release(), move(undef) };
}
+expr Memory::PtrInput::operator==(const PtrInput &rhs) const {
+ if (byval != rhs.byval || nocapture != rhs.nocapture)
+ return false;
+ return val == rhs.val;
+}
+
pair<expr,expr>
Memory::mkFnRet(const char *name, const vector<PtrInput> &ptr_inputs) {
bool has_local = escaped_local_blks.numMayAlias(true);
@@ -1674,6 +1680,19 @@ Memory::CallState Memory::CallState::mkIf(const expr &cond,
return ret;
}
+expr Memory::CallState::operator==(const CallState &rhs) const {
+ if (empty != rhs.empty)
+ return false;
+ if (empty)
+ return true;
+
+ expr ret = non_local_block_liveness == rhs.non_local_block_liveness;
+ for (unsigned i = 0, e = non_local_block_val.size(); i != e; ++i) {
+ ret &= non_local_block_val[i] == rhs.non_local_block_val[i];
+ }
+ 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);
@@ -1682,6 +1701,7 @@ bool Memory::CallState::operator<(const CallState &rhs) const {
Memory::CallState
Memory::mkCallState(const vector<PtrInput> *ptr_inputs, bool nofree) const {
CallState st;
+ st.empty = false;
// TODO: handle havoc of local blocks

MODIFY
ir/memory.h
ir/memory.h
@@ -318,10 +318,12 @@ public:
class CallState {
std::vector<smt::expr> non_local_block_val;
smt::expr non_local_block_liveness;
+ bool empty = true;
public:
static CallState mkIf(const smt::expr &cond, const CallState &then,
const CallState &els);
+ smt::expr operator==(const CallState &rhs) const;
// for container use only
bool operator<(const CallState &rhs) const;
friend class Memory;
@@ -345,6 +347,7 @@ public:
PtrInput(StateValue &&v, bool byval, bool nocapture) :
val(std::move(v)), byval(byval), nocapture(nocapture) {}
+ smt::expr operator==(const PtrInput &rhs) const;
bool operator<(const PtrInput &rhs) const {
return std::tie(val, byval, nocapture) <
std::tie(rhs.val, rhs.byval, rhs.nocapture);

MODIFY
ir/state.cpp
ir/state.cpp
@@ -541,6 +541,24 @@ void State::addNoReturn() {
addUB(expr(false));
}
+expr State::FnCallInput::operator==(const FnCallInput &rhs) const {
+ if (readsmem != rhs.readsmem ||
+ argmemonly != rhs.argmemonly ||
+ fncall_ranges != rhs.fncall_ranges ||
+ m < rhs.m || rhs.m < m)
+ return false;
+
+ AndExpr eq;
+ for (unsigned i = 0, e = args_nonptr.size(); i != e; ++i) {
+ eq.add(args_nonptr[i] == rhs.args_nonptr[i]);
+ }
+
+ for (unsigned i = 0, e = args_ptr.size(); i != e; ++i) {
+ eq.add(args_ptr[i] == rhs.args_ptr[i]);
+ }
+ return eq();
+}
+
expr State::FnCallInput::refinedBy(
State &s, const vector<StateValue> &args_nonptr2,
const vector<Memory::PtrInput> &args_ptr2,
@@ -623,6 +641,15 @@ State::FnCallOutput State::FnCallOutput::mkIf(const expr &cond,
return ret;
}
+expr State::FnCallOutput::operator==(const FnCallOutput &rhs) const {
+ expr ret = ub == rhs.ub;
+ for (unsigned i = 0, e = retvals.size(); i != e; ++i) {
+ ret &= retvals[i] == rhs.retvals[i];
+ }
+ ret &= callstate == rhs.callstate;
+ return ret;
+}
+
bool State::FnCallOutput::operator<(const FnCallOutput &rhs) const {
return tie(retvals, ub, callstate) < tie(rhs.retvals, rhs.ub, rhs.callstate);
}
@@ -657,8 +684,9 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
// source may create new fn symbols, target just references src symbols
if (isSource()) {
+ auto &calls_fn = fn_call_data[name];
auto call_data_pair
- = fn_call_data[name].try_emplace({ move(inputs), move(ptr_inputs),
+ = calls_fn.try_emplace({ move(inputs), move(ptr_inputs),
analysis.ranges_fn_calls,
reads_memory ? memory : Memory(*this),
reads_memory, argmemonly });
@@ -689,6 +717,13 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
? memory.mkCallState(argmemonly ? &I->first.args_ptr : nullptr,
attrs.has(FnAttrs::NoFree))
: Memory::CallState() };
+
+ // add equality constraints between source's function calls
+ for (auto II = calls_fn.begin(), E = calls_fn.end(); II != E; ++II) {
+ if (II == I)
+ continue;
+ fn_call_pre &= (I->first == II->first).implies(I->second == II->second);
+ }
}
addUB(I->second.ub);

MODIFY
ir/state.h
ir/state.h
@@ -116,6 +116,7 @@ private:
Memory m;
bool readsmem, argmemonly;
+ smt::expr operator==(const FnCallInput &rhs) const;
smt::expr refinedBy(State &s, const std::vector<StateValue> &args_nonptr,
const std::vector<Memory::PtrInput> &args_ptr,
const ValueAnalysis::FnCallRanges &fncall_ranges,
@@ -131,6 +132,7 @@ private:
static FnCallOutput mkIf(const smt::expr &cond, const FnCallOutput &then,
const FnCallOutput &els);
+ smt::expr operator==(const FnCallOutput &rhs) const;
bool operator<(const FnCallOutput &rhs) const;
};
std::map<std::string, std::map<FnCallInput, FnCallOutput>> fn_call_data;

MODIFY
ir/state_value.cpp
ir/state_value.cpp
@@ -44,6 +44,11 @@ bool StateValue::isValid() const {
return value.isValid() && non_poison.isValid();
}
+expr StateValue::operator==(const StateValue &other) const {
+ return non_poison == other.non_poison &&
+ non_poison.implies(value == other.value);
+}
+
bool StateValue::eq(const StateValue &other) const {
return value.eq(other.value) && non_poison.eq(other.non_poison);
}

MODIFY
ir/state_value.h
ir/state_value.h
@@ -29,6 +29,7 @@ struct StateValue {
bool isValid() const;
+ smt::expr operator==(const StateValue &other) const;
bool eq(const StateValue &other) const;
std::set<smt::expr> vars() const;

ADD
tests/alive-tv/calls/readonly-undef.srctgt.ll
+declare i8 @func(i8) readonly
+
+define i8 @src() {
+ %V1 = call i8 @func(i8 undef)
+ %V2 = call i8 @func(i8 undef)
+ %diff = sub i8 %V1, %V2
+ ret i8 %diff
+}
+
+define i8 @tgt() {
+ %V1 = call i8 @func(i8 undef)
+ ret i8 0
+}

ADD
tests/alive-tv/calls/readonly.srctgt.ll
+declare i8 @func(i8) readonly
+
+define i8 @src(i8 %n) {
+ %V1 = call i8 @func(i8 %n)
+ %V2 = call i8 @func(i8 %n)
+ %diff = sub i8 %V1, %V2
+ ret i8 %diff
+}
+
+define i8 @tgt(i8 %n) {
+ %V1 = call i8 @func(i8 %n)
+ ret i8 0
+}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -394,7 +394,7 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
pre_src_forall = pre_src;
}
}
- expr pre = pre_src_exists && pre_tgt;
+ expr pre = pre_src_exists && pre_tgt && src_state.getFnPre();
pre_src_forall &= tgt_state.getFnPre();
auto [poison_cnstr, value_cnstr] = type.refines(src_state, tgt_state, a, b);

support removal of duplicated readonly function calls