fix bug fncalls incompatibility with ptr attributes
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1098,16 +1098,20 @@ void FnCall::print(ostream &os) const {
os << "\t; WARNING: unknown known function";
}
-static void unpack_inputs(Type &ty, const StateValue &value,
+static void unpack_inputs(State&s, Type &ty, const StateValue &value,
vector<StateValue> &inputs,
vector<StateValue> &ptr_inputs) {
if (auto agg = ty.getAsAggregateType()) {
for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
- unpack_inputs(agg->getChild(i), agg->extract(value, i), inputs,
+ unpack_inputs(s, agg->getChild(i), agg->extract(value, i), inputs,
ptr_inputs);
}
+ } else if (ty.isPtrType()) {
+ Pointer p(s.getMemory(), value.value);
+ p.strip_attrs();
+ ptr_inputs.emplace_back(p.release(), expr(value.non_poison));
} else {
- (ty.isPtrType() ? ptr_inputs : inputs).emplace_back(value);
+ inputs.emplace_back(value);
}
}
@@ -1147,7 +1151,7 @@ StateValue FnCall::toSMT(State &s) const {
vector<Type*> out_types;
for (auto arg : args) {
- unpack_inputs(arg->getType(), s[*arg], inputs, ptr_inputs);
+ unpack_inputs(s, arg->getType(), s[*arg], inputs, ptr_inputs);
}
if (!isVoid())
unpack_ret_ty(out_types, getType());

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -314,7 +314,7 @@ Pointer::Pointer(const Memory &m, unsigned bid, bool local)
: m(m), p(
prepend_if(expr::mkUInt(local, 1),
expr::mkUInt(bid, bits_shortbid())
- .concat(expr::mkUInt(0, bits_for_offset + bits_for_ptrattrs)),
+ .concat_zeros(bits_for_offset + bits_for_ptrattrs),
ptr_has_local_bit())) {
assert((local && bid < num_locals) || (!local && bid < num_nonlocals));
assert(p.bits() == total_bits());
@@ -738,6 +738,11 @@ expr Pointer::is_readonly() const {
return p.extract(has_nocapture, has_nocapture) == 1;
}
+void Pointer::strip_attrs() {
+ p = p.extract(total_bits()-1, bits_for_ptrattrs)
+ .concat_zeros(bits_for_ptrattrs);
+}
+
Pointer Pointer::mkNullPointer(const Memory &m) {
assert(num_nonlocals > 0);
// A null pointer points to block 0 without any attribute.
@@ -1002,13 +1007,15 @@ pair<expr, expr> Memory::mkUndefInput(unsigned attributes) const {
return { p.release(), move(undef) };
}
-expr Memory::mkFnRet(const char *name) const {
+pair<expr,expr> Memory::mkFnRet(const char *name) const {
// TODO: can only alias with escaped local blocks!
- Pointer p(*this, expr::mkVar(name, Pointer::total_bits()));
+ expr var
+ = expr::mkFreshVar(name, expr::mkUInt(0, bits_for_bid + bits_for_offset));
+ Pointer p(*this, var.concat_zeros(bits_for_ptrattrs));
state->addAxiom(expr::mkIf(p.is_local(),
p.get_short_bid().ule(num_locals - 1),
p.get_short_bid().ule(num_nonlocals - 1)));
- return p.release();
+ return { p.release(), move(var) };
}
static expr disjoint_local_blocks(const Memory &m, const expr &addr,
@@ -1070,9 +1077,7 @@ Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
expr::mkUInt(0, bits_size_t - align_bits - 1));
state->addQuantVar(addr_var);
- expr blk_addr = align_bits ? addr_var.concat(expr::mkUInt(0, align_bits))
- : addr_var;
-
+ expr blk_addr = addr_var.concat_zeros(align_bits);
auto full_addr = expr::mkUInt(1, 1).concat(blk_addr);
// addr + size does not overflow

MODIFY
ir/memory.h
ir/memory.h
@@ -163,6 +163,8 @@ public:
smt::expr is_nocapture() const;
smt::expr is_readonly() const;
+ void strip_attrs();
+
smt::expr refined(const Pointer &other) const;
smt::expr fninput_refined(const Pointer &other) const;
smt::expr block_val_refined(const Pointer &other) const;
@@ -214,7 +216,7 @@ public:
void markByVal(unsigned bid);
smt::expr mkInput(const char *name, unsigned attributes) const;
std::pair<smt::expr, smt::expr> mkUndefInput(unsigned attributes) const;
- smt::expr mkFnRet(const char *name) const;
+ std::pair<smt::expr, smt::expr> mkFnRet(const char *name) const;
// Allocates a new memory block and returns (pointer expr, allocated).
// If bid is not specified, it creates a fresh block id by increasing

MODIFY
ir/state.cpp
ir/state.cpp
@@ -199,15 +199,20 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
= fn_call_data[name].try_emplace({ move(inputs), move(ptr_inputs),
memory, reads_memory, argmemonly });
+ auto mk_val = [this](const Type &t, const string &name) {
+ if (t.isPtrType())
+ return memory.mkFnRet(name.c_str());
+
+ auto v = expr::mkFreshVar(name.c_str(), t.getDummyValue(false).value);
+ return make_pair(v, v);
+ };
+
if (inserted) {
vector<StateValue> values;
string valname = name + "#val";
string npname = name + "#np";
for (auto t : out_types) {
- values.emplace_back(
- t->isPtrType()
- ? memory.mkFnRet(valname.c_str())
- : expr::mkFreshVar(valname.c_str(), t->getDummyValue(false).value),
+ values.emplace_back(mk_val(*t, valname).first,
expr::mkFreshVar(npname.c_str(), false));
}
@@ -222,11 +227,13 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
// if any of the arguments is poison, yield an arbitrary value, such that
// f(poison) -> f(42) works
vector<StateValue> ret;
+ auto T = out_types.begin();
auto var_name = name + "#pval";
for (auto &[v, np] : I->second.first) {
- auto var = expr::mkFreshVar(var_name.c_str(), v);
- ret.emplace_back(expr::mkIf(all_args_np, v, var), expr(np));
- addQuantVar(var);
+ auto [val_poison, var] = mk_val(**T, var_name);
+ ret.emplace_back(expr::mkIf(all_args_np, v, val_poison), expr(np));
+ addQuantVar(move(var));
+ ++T;
}
return ret;
}

ADD
tests/alive-tv/attrs/nocapture-noundef.src.ll
+; this is needed for correctness, since the cmn+branch needs to be strong
+; TEST-ARGS: -disable-undef-input
+
+define i8* @f(i8* %a, i8* nocapture %b) {
+ %cmp = icmp eq i8* %a, %b
+ br i1 %cmp, label %t, label %f
+
+t:
+ %v = call i8* @g(i8* %b)
+ ret i8* %v
+
+f:
+ ret i8* null
+}
+
+declare i8* @g(i8*)

ADD
tests/alive-tv/attrs/nocapture-noundef.tgt.ll
+define i8* @f(i8* %a, i8* nocapture %b) {
+ %cmp = icmp eq i8* %a, %b
+ br i1 %cmp, label %t, label %f
+
+t:
+ %v = call i8* @g(i8* %a)
+ ret i8* %v
+
+f:
+ ret i8* null
+}
+
+declare i8* @g(i8*)

MODIFY
tests/alive-tv/attrs/nocapture.src.ll
tests/alive-tv/attrs/nocapture.src.ll
@@ -33,3 +33,10 @@ A:
B:
ret i8* null
}
+
+define i8* @f7(i8* %a, i8* nocapture %b) {
+ %v = call i8* @g(i8* %a)
+ ret i8* %v
+}
+
+declare i8* @g(i8*)

MODIFY
tests/alive-tv/attrs/nocapture.tgt.ll
tests/alive-tv/attrs/nocapture.tgt.ll
@@ -36,3 +36,10 @@ A:
B:
ret i8* null
}
+
+define i8* @f7(i8* %a, i8* nocapture %b) {
+ %v = call i8* @g(i8* %a)
+ ret i8* %v
+}
+
+declare i8* @g(i8*)

fix bug #260: fncalls incompatibility with ptr attributes