fn calls: add support for checking memory refinement when considering if fn calls are equal
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1070,7 +1070,7 @@ void FnCall::rauw(const Value &what, Value &with) {
}
void FnCall::print(ostream &os) const {
- if (!dynamic_cast<VoidType*>(&getType()))
+ if (!isVoid())
os << getName() << " = ";
os << "call " << print_type(getType()) << fnName << '(';
@@ -1135,11 +1135,12 @@ StateValue FnCall::toSMT(State &s) const {
for (auto arg : args) {
unpack_inputs(arg->getType(), s[*arg], inputs, ptr_inputs);
}
+ if (!isVoid())
unpack_ret_ty(out_types, getType());
unsigned idx = 0;
auto ret = s.addFnCall(fnName, move(inputs), move(ptr_inputs), out_types);
- return pack_return(getType(), ret, idx);
+ return isVoid() ? StateValue() : pack_return(getType(), ret, idx);
}
expr FnCall::getTypeConstraints(const Function &f) const {

MODIFY
ir/state.cpp
ir/state.cpp
@@ -175,6 +175,7 @@ const vector<StateValue>
State::addFnCall(const string &name, vector<StateValue> &&inputs,
vector<StateValue> &&ptr_inputs,
const vector<Type*> &out_types) {
+ // TODO: handle changes to memory due to fn call
expr all_args_np(true);
for (auto &v : inputs) {
all_args_np &= v.non_poison;
@@ -289,12 +290,11 @@ void State::syncSEdataWithSrc(const State &src) {
Memory::resetLocalBids();
}
-void State::mkAxioms(const State &tgt) {
+void State::mkAxioms(State &tgt) {
assert(isSource() && !tgt.isSource());
memory.mkAxioms();
// axioms for function calls
- // TODO: handle refinement of pointers & memory
for (auto &[fn, data] : tgt.fn_call_data) {
(void)fn;
for (auto I = data.begin(), E = data.end(); I != E; ++I) {
@@ -312,13 +312,27 @@ void State::mkAxioms(const State &tgt) {
refines &= !ins[i].non_poison || (eq_val && ins2[i].non_poison);
}
+ for (unsigned i = 0, e = ptr_ins.size(); i != e; ++i) {
+ expr eq_val = Pointer(memory, ptr_ins[i].value)
+ .refined(Pointer(memory, ptr_ins2[i].value));
+ is_val_eq &= eq_val;
+ refines &= ptr_ins[i].non_poison
+ .implies(eq_val && ptr_ins2[i].non_poison);
+ }
+
+ {
+ expr mem_refined = mem.refined(mem2).first;
+ is_val_eq &= mem_refined;
+ refines &= mem_refined;
+ }
+
expr ref_expr(true), eq_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);
}
- addAxiom(is_val_eq.implies(eq_expr));
- addAxiom(refines.implies(ref_expr && ub.implies(ub2)));
+ tgt.addPre(is_val_eq.implies(eq_expr));
+ tgt.addPre(refines.implies(ref_expr && ub.implies(ub2)));
}
}
}

MODIFY
ir/state.h
ir/state.h
@@ -142,7 +142,7 @@ public:
void markGlobalAsAllocated(const std::string &glbvar);
void syncSEdataWithSrc(const State &src);
- void mkAxioms(const State &tgt);
+ void mkAxioms(State &tgt);
private:
void addJump(const BasicBlock &dst, smt::expr &&domain);

ADD
tests/alive-tv/call-movestr.src.ll
+; ERROR: Source is more defined
+
+define i8 @f(i8* %a) {
+ store i8 3, i8* %a
+ %b = call i8 @g(i8* %a)
+ ret i8 %b
+}
+
+declare i8 @g(i8*)

ADD
tests/alive-tv/call-movestr.tgt.ll
+define i8 @f(i8* %a) {
+ %b = call i8 @g(i8* %a)
+ store i8 3, i8* %a
+ ret i8 %b
+}
+
+declare i8 @g(i8*)

ADD
tests/alive-tv/call-movestr2.src.ll
+; TODO: needs refinement of local blocks working
+; XPASS: Transformation seems to be correct
+
+define i8 @f() {
+ %a = alloca i8
+ store i8 3, i8* %a
+ %b = call i8 @g(i8* %a)
+ ret i8 %b
+}
+
+declare i8 @g(i8*)

ADD
tests/alive-tv/call-movestr2.tgt.ll
+define i8 @f() {
+ %a = alloca i8
+ %b = call i8 @g(i8* %a)
+ store i8 3, i8* %a
+ ret i8 %b
+}
+
+declare i8 @g(i8*)

ADD
tests/alive-tv/call.src.ll
+define i8 @f1() {
+ %a = alloca i8
+ %b = call i8 @g(i8* %a)
+ ret i8 %b
+}
+
+define i8 @f2(i8* %a) {
+ %b = call i8 @g(i8* %a)
+ ret i8 %b
+}
+
+define i8 @f3(i8* %a) {
+ store i8 undef, i8* %a
+ %b = call i8 @g(i8* %a)
+ ret i8 %b
+}
+
+declare i8 @g(i8*)

ADD
tests/alive-tv/call.tgt.ll
+define i8 @f1() {
+ %a = alloca i8
+ store i8 3, i8* %a
+ %b = call i8 @g(i8* %a)
+ ret i8 %b
+}
+
+define i8 @f2(i8* %a) {
+ %b = call i8 @g(i8* %a)
+ ret i8 %b
+}
+
+define i8 @f3(i8* %a) {
+ store i8 3, i8* %a
+ %b = call i8 @g(i8* %a)
+ ret i8 %b
+}
+
+declare i8 @g(i8*)

fn calls: add support for checking memory refinement when considering if fn calls are equal