Factor out Memory::PtrInput class, put assertions in State's methods
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1327,7 +1327,7 @@ void FnCall::print(ostream &os) const {
static void unpack_inputs(State&s, Type &ty, const ParamAttrs &argflag,
const StateValue &value, vector<StateValue> &inputs,
- vector<pair<StateValue, bool>> &ptr_inputs) {
+ vector<Memory::PtrInput> &ptr_inputs) {
if (auto agg = ty.getAsAggregateType()) {
for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
unpack_inputs(s, agg->getChild(i), argflag, agg->extract(value, i),
@@ -1400,7 +1400,7 @@ StateValue FnCall::toSMT(State &s) const {
}
vector<StateValue> inputs;
- vector<pair<StateValue, bool>> ptr_inputs;
+ vector<Memory::PtrInput> ptr_inputs;
vector<Type*> out_types;
ostringstream fnName_mangled;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1212,7 +1212,7 @@ pair<expr, expr> Memory::mkUndefInput(const ParamAttrs &attrs) const {
pair<expr,expr>
Memory::mkFnRet(const char *name,
- const vector<pair<StateValue, bool>> &ptr_inputs) const {
+ const vector<PtrInput> &ptr_inputs) const {
expr var
= expr::mkFreshVar(name, expr::mkUInt(0, bits_for_bid + bits_for_offset));
Pointer p(*this, var.concat_zeros(bits_for_ptrattrs));
@@ -1220,9 +1220,9 @@ Memory::mkFnRet(const char *name,
set<expr> local;
for (auto &in : ptr_inputs) {
// TODO: callee cannot observe the bid if this is byval.
- Pointer inp(*this, in.first.value);
+ Pointer inp(*this, in.val.value);
if (!inp.isLocal().isFalse())
- local.emplace(in.first.non_poison && p.getBid() == inp.getBid());
+ local.emplace(in.val.non_poison && p.getBid() == inp.getBid());
}
for (unsigned i = 0; i < num_locals; ++i) {
if (escaped_local_blks[i])
@@ -1249,7 +1249,7 @@ expr Memory::CallState::implies(const CallState &st) const {
}
Memory::CallState
-Memory::mkCallState(const vector<pair<StateValue, bool>> *ptr_inputs) const {
+Memory::mkCallState(const vector<PtrInput> *ptr_inputs) const {
Memory::CallState st;
st.empty = false;
@@ -1637,7 +1637,7 @@ expr Memory::int2ptr(const expr &val) const {
pair<expr,Pointer>
Memory::refined(const Memory &other, bool skip_constants,
- const vector<pair<StateValue, bool>> *set_ptrs) const {
+ const vector<PtrInput> *set_ptrs) const {
if (num_nonlocals <= has_null_block)
return { true, Pointer(*this, expr()) };
@@ -1672,7 +1672,7 @@ Memory::refined(const Memory &other, bool skip_constants,
expr c(false);
for (auto &itm: *set_ptrs) {
// TODO: deal with the byval arg case (itm.second)
- auto &ptr = itm.first;
+ auto &ptr = itm.val;
c |= ptr.non_poison && Pointer(*this, ptr.value).getBid() == ptr_bid;
}
ret = c.implies(ret);

MODIFY
ir/memory.h
ir/memory.h
@@ -247,11 +247,21 @@ public:
smt::expr mkInput(const char *name, const ParamAttrs &attrs) const;
std::pair<smt::expr, smt::expr> mkUndefInput(const ParamAttrs &attrs) const;
+ struct PtrInput {
+ StateValue val;
+ bool byval;
+
+ PtrInput(StateValue &&v, bool byval) : val(std::move(v)), byval(byval) {}
+ bool operator<(const PtrInput &rhs) const {
+ return std::tie(val, byval) < std::tie(rhs.val, rhs.byval);
+ }
+ };
+
std::pair<smt::expr, smt::expr>
mkFnRet(const char *name,
- const std::vector<std::pair<StateValue, bool>> &ptr_inputs) const;
+ const std::vector<PtrInput> &ptr_inputs) const;
CallState
- mkCallState(const std::vector<std::pair<StateValue, bool>> *ptr_inputs)
+ mkCallState(const std::vector<PtrInput> *ptr_inputs)
const;
void setState(const CallState &st);
@@ -296,7 +306,7 @@ public:
std::pair<smt::expr,Pointer>
refined(const Memory &other,
bool skip_constants,
- const std::vector<std::pair<StateValue, bool>> *set_ptrs = nullptr)
+ const std::vector<PtrInput> *set_ptrs = nullptr)
const;
// Returns true if a nocapture pointer byte is not in the memory.

MODIFY
ir/state.cpp
ir/state.cpp
@@ -216,7 +216,7 @@ void State::addNoReturn() {
const vector<StateValue>
State::addFnCall(const string &name, vector<StateValue> &&inputs,
- vector<pair<StateValue, bool>> &&ptr_inputs,
+ vector<Memory::PtrInput> &&ptr_inputs,
const vector<Type*> &out_types, const FnAttrs &attrs) {
// TODO: handle changes to memory due to fn call
// TODO: can read/write=false fn calls be removed?
@@ -232,8 +232,8 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
all_valid &= v.isValid();
}
for (auto &v : ptr_inputs) {
- all_args_np &= v.first.non_poison;
- all_valid &= v.first.isValid();
+ all_args_np &= v.val.non_poison;
+ all_valid &= v.val.isValid();
}
if (!all_valid) {

MODIFY
ir/state.h
ir/state.h
@@ -56,7 +56,7 @@ private:
smt::AndExpr axioms;
smt::AndExpr ooms;
- const BasicBlock *current_bb;
+ const BasicBlock *current_bb = nullptr;
std::set<smt::expr> quantified_vars;
// var -> ((value, not_poison), undef_vars, already_used?)
@@ -91,8 +91,7 @@ private:
struct FnCallInput {
std::vector<StateValue> args_nonptr;
- // (ptr arguments, is by_val arg?)
- std::vector<std::pair<StateValue, bool>> args_ptr;
+ std::vector<Memory::PtrInput> args_ptr;
Memory m;
bool readsmem, argmemonly;
bool operator<(const FnCallInput &rhs) const {
@@ -142,7 +141,7 @@ public:
const std::vector<StateValue>
addFnCall(const std::string &name, std::vector<StateValue> &&inputs,
- std::vector<std::pair<StateValue, bool>> &&ptr_inputs,
+ std::vector<Memory::PtrInput> &&ptr_inputs,
const std::vector<Type*> &out_types, const FnAttrs &attrs);
void addQuantVar(const smt::expr &var);

Factor out Memory::PtrInput class, put assertions in State's methods (#391)