fncalls: add support for readnone/writeonly attributes
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1084,6 +1084,11 @@ void FnCall::print(ostream &os) const {
}
os << ')';
+ if (flags & NoRead)
+ os << " noread";
+ if (flags & NoWrite)
+ os << " nowrite";
+
if (!valid)
os << "\t; WARNING: unknown known function";
}
@@ -1139,7 +1144,8 @@ StateValue FnCall::toSMT(State &s) const {
unpack_ret_ty(out_types, getType());
unsigned idx = 0;
- auto ret = s.addFnCall(fnName, move(inputs), move(ptr_inputs), out_types);
+ auto ret = s.addFnCall(fnName, move(inputs), move(ptr_inputs), out_types,
+ !(flags & NoRead), !(flags & NoWrite));
return isVoid() ? StateValue() : pack_return(getType(), ret, idx);
}
@@ -1150,7 +1156,7 @@ expr FnCall::getTypeConstraints(const Function &f) const {
unique_ptr<Instr> FnCall::dup(const string &suffix) const {
auto r = make_unique<FnCall>(getType(), getName() + suffix, string(fnName),
- valid);
+ flags, valid);
r->args = args;
return r;
}

MODIFY
ir/instr.h
ir/instr.h
@@ -169,13 +169,18 @@ public:
class FnCall final : public Instr {
+public:
+ enum Flags { None = 0, NoRead = 1 << 0, NoWrite = 1 << 1 };
+private:
std::string fnName;
std::vector<Value*> args;
+ unsigned flags;
bool valid;
public:
FnCall(Type &type, std::string &&name, std::string &&fnName,
- bool valid = true)
- : Instr(type, std::move(name)), fnName(std::move(fnName)), valid(valid) {}
+ unsigned flags = None, bool valid = true)
+ : Instr(type, std::move(name)), fnName(std::move(fnName)), flags(flags),
+ valid(valid) {}
void addArg(Value &arg);
std::vector<Value*> operands() const override;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -174,8 +174,11 @@ void State::addUB(const expr &ub) {
const vector<StateValue>
State::addFnCall(const string &name, vector<StateValue> &&inputs,
vector<StateValue> &&ptr_inputs,
- const vector<Type*> &out_types) {
+ const vector<Type*> &out_types, bool reads_memory,
+ bool writes_memory) {
// TODO: handle changes to memory due to fn call
+ // TODO: can read/write=false fn calls be removed?
+
expr all_args_np(true);
bool all_valid = true;
for (auto &v : inputs) {
@@ -192,8 +195,13 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
return vector<StateValue>(out_types.size());
}
+ optional<Memory> mem_in;
+ if (reads_memory)
+ mem_in = memory;
+
auto [I, inserted]
- = fn_call_data[name].try_emplace({move(inputs), move(ptr_inputs), memory});
+ = fn_call_data[name].try_emplace({ move(inputs), move(ptr_inputs),
+ move(mem_in)});
if (inserted) {
vector<StateValue> values;
@@ -328,8 +336,8 @@ void State::mkAxioms(State &tgt) {
.implies(eq_val && ptr_ins2[i].non_poison);
}
- {
- expr mem_refined = mem.refined(mem2).first;
+ if (mem && mem2) {
+ expr mem_refined = mem->refined(*mem2).first;
is_val_eq &= mem_refined;
refines &= mem_refined;
}

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

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -238,8 +238,17 @@ public:
if (!ty)
return error(i);
+ unsigned flags = 0;
+ if (i.hasFnAttr(llvm::Attribute::ReadOnly))
+ flags |= FnCall::NoWrite;
+ if (i.hasFnAttr(llvm::Attribute::ReadNone))
+ flags |= FnCall::NoRead | FnCall::NoWrite;
+ if (i.hasFnAttr(llvm::Attribute::WriteOnly))
+ flags |= FnCall::NoRead;
+
string fn_name = '@' + fn->getName().str();
- auto call = make_unique<FnCall>(*ty, value_name(i), move(fn_name), !known);
+ auto call = make_unique<FnCall>(*ty, value_name(i), move(fn_name), flags,
+ !known);
for (auto &arg : i.args()) {
auto a = get_operand(arg);
if (!a)

MODIFY
tests/alive-tv/call.src.ll
tests/alive-tv/call.src.ll
@@ -15,4 +15,11 @@ define i8 @f3(i8* %a) {
ret i8 %b
}
+define i8 @f4(i8* %a) {
+ store i8 3, i8* %a
+ %b = call i8 @h(i8* %a)
+ ret i8 %b
+}
+
declare i8 @g(i8*)
+declare i8 @h(i8*) readnone

MODIFY
tests/alive-tv/call.tgt.ll
tests/alive-tv/call.tgt.ll
@@ -16,4 +16,11 @@ define i8 @f3(i8* %a) {
ret i8 %b
}
+define i8 @f4(i8* %a) {
+ %b = call i8 @h(i8* %a)
+ store i8 3, i8* %a
+ ret i8 %b
+}
+
declare i8 @g(i8*)
+declare i8 @h(i8*) readnone

fncalls: add support for readnone/writeonly attributes