fncall: add support for argmemonly
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1088,6 +1088,8 @@ void FnCall::print(ostream &os) const {
os << " noread";
if (flags & NoWrite)
os << " nowrite";
+ if (flags & ArgMemOnly)
+ os << " argmemonly";
if (flags & NNaN)
os << " NNaN";
@@ -1151,7 +1153,8 @@ StateValue FnCall::toSMT(State &s) const {
unsigned idx = 0;
auto ret = s.addFnCall(fnName, move(inputs), move(ptr_inputs), out_types,
- !(flags & NoRead), !(flags & NoWrite));
+ !(flags & NoRead), !(flags & NoWrite),
+ flags & ArgMemOnly);
return isVoid() ? StateValue() : pack_return(getType(), ret, flags, idx);
}

MODIFY
ir/instr.h
ir/instr.h
@@ -170,7 +170,8 @@ public:
class FnCall final : public Instr {
public:
- enum Flags { None = 0, NoRead = 1 << 0, NoWrite = 1 << 1, NNaN = 1 << 2 };
+ enum Flags { None = 0, NoRead = 1 << 0, NoWrite = 1 << 1, ArgMemOnly = 1 << 2,
+ NNaN = 1 << 3 };
private:
std::string fnName;
std::vector<Value*> args;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -175,7 +175,7 @@ const vector<StateValue>
State::addFnCall(const string &name, vector<StateValue> &&inputs,
vector<StateValue> &&ptr_inputs,
const vector<Type*> &out_types, bool reads_memory,
- bool writes_memory) {
+ bool writes_memory, bool argmemonly) {
// TODO: handle changes to memory due to fn call
// TODO: can read/write=false fn calls be removed?
@@ -197,7 +197,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
auto [I, inserted]
= fn_call_data[name].try_emplace({ move(inputs), move(ptr_inputs),
- memory, reads_memory });
+ memory, reads_memory, argmemonly });
if (inserted) {
vector<StateValue> values;
@@ -310,12 +310,12 @@ void State::mkAxioms(State &tgt) {
for (auto &[fn, data] : fn_call_data) {
(void)fn;
for (auto I = data.begin(), E = data.end(); I != E; ++I) {
- auto &[ins, ptr_ins, mem, reads] = I->first;
+ auto &[ins, ptr_ins, mem, reads, argmem] = I->first;
auto &[rets, ub] = I->second;
auto &data2 = tgt.fn_call_data.at(fn);
for (auto I2 = data2.begin(), E2 = data2.end(); I2 != E2; ++I2) {
- auto &[ins2, ptr_ins2, mem2, reads2] = I2->first;
+ auto &[ins2, ptr_ins2, mem2, reads2, argmem2] = I2->first;
auto &[rets2, ub2] = I2->second;
expr refines(true), is_val_eq(true);
@@ -326,6 +326,8 @@ void State::mkAxioms(State &tgt) {
}
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
expr eq_val = Pointer(mem, ptr_ins[i].value)
.fninput_refined(Pointer(mem2, ptr_ins2[i].value));
is_val_eq &= eq_val;
@@ -333,7 +335,7 @@ void State::mkAxioms(State &tgt) {
.implies(eq_val && ptr_ins2[i].non_poison);
}
- if (reads && reads2) {
+ if (reads && reads2 && !argmem && !argmem2) {
expr mem_refined = mem.refined(mem2).first;
is_val_eq &= mem_refined;
refines &= mem_refined;

MODIFY
ir/state.h
ir/state.h
@@ -69,11 +69,11 @@ private:
std::set<smt::expr> return_undef_vars;
// store data for function calls:
- // inputs: non-ptr arguments, ptr arguments, memory, reads memory?
+ // inputs: non-ptr arguments, ptr arguments, memory, reads memory?, argmemonly
// outputs: values, UB
std::map<std::string,
std::map<std::tuple<std::vector<StateValue>, std::vector<StateValue>,
- Memory, bool>,
+ Memory, bool, bool>,
std::pair<std::vector<StateValue>, smt::expr>>>
fn_call_data;
@@ -105,7 +105,7 @@ public:
addFnCall(const std::string &name, std::vector<StateValue> &&inputs,
std::vector<StateValue> &&ptr_inputs,
const std::vector<Type*> &out_types, bool reads_memory,
- bool writes_memory);
+ bool writes_memory, bool argmemonly);
void addQuantVar(const smt::expr &var);
void addUndefVar(smt::expr &&var);

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -245,6 +245,8 @@ public:
flags |= FnCall::NoRead | FnCall::NoWrite;
if (i.hasFnAttr(llvm::Attribute::WriteOnly))
flags |= FnCall::NoRead;
+ if (i.hasFnAttr(llvm::Attribute::ArgMemOnly))
+ flags |= FnCall::ArgMemOnly;
if (auto op = dyn_cast<llvm::FPMathOperator>(&i)) {
if (op->hasNoNaNs())
flags |= FnCall::NNaN;

fncall: add support for argmemonly