fix undef ptrs aliasing with local ptrs if a function has no locals
MODIFY
ir/pointer.cpp
ir/pointer.cpp
@@ -103,6 +103,25 @@ expr Pointer::mkLongBid(const expr &short_bid, bool local) {
return expr::mkUInt(local, 1).concat(short_bid);
}
+expr Pointer::mkUndef(State &s) {
+ auto &m = s.getMemory();
+ bool force_local = false, force_nonlocal = false;
+ if (has_local_bit()) {
+ force_nonlocal = m.numLocals() == 0;
+ force_local = !force_nonlocal && m.numNonlocals() == 0;
+ }
+
+ unsigned var_bits = bits_for_bid + bits_for_offset
+ - (force_local | force_nonlocal);
+ expr var = expr::mkFreshVar("undef", expr::mkUInt(0, var_bits));
+ s.addUndefVar(expr(var));
+
+ if (force_local || force_nonlocal)
+ var = mkLongBid(var, force_local);
+
+ return var.concat_zeros(bits_for_ptrattrs);
+}
+
unsigned Pointer::totalBits() {
return bits_for_ptrattrs + bits_for_bid + bits_for_offset;
}

MODIFY
ir/pointer.h
ir/pointer.h
@@ -47,6 +47,7 @@ public:
const ParamAttrs &attr = {});
static smt::expr mkLongBid(const smt::expr &short_bid, bool local);
+ static smt::expr mkUndef(State &s);
static unsigned totalBits();
static unsigned bitsShortBid();

MODIFY
ir/type.cpp
ir/type.cpp
@@ -255,6 +255,13 @@ expr Type::combine_poison(const expr &boolean, const expr &orig) const {
expr::mkIf(boolean, expr::mkInt(-1, orig), expr::mkInt(0, orig)) & orig;
}
+StateValue Type::mkUndef(State &s) const {
+ auto val = getDummyValue(true);
+ expr var = expr::mkFreshVar("undef", val.value);
+ s.addUndefVar(expr(var));
+ return { move(var), move(val.non_poison) };
+}
+
pair<expr, expr> Type::mkUndefInput(State &s, const ParamAttrs &attrs) const {
auto var = expr::mkFreshVar("undef", mkInput(s, "", attrs));
return { var, var };
@@ -664,6 +671,10 @@ PtrType::refines(const State &src_s, const State &tgt_s, const StateValue &src,
(src.non_poison && tgt.non_poison).implies(p.refined(q)) };
}
+StateValue PtrType::mkUndef(State &s) const {
+ return { Pointer::mkUndef(s), true };
+}
+
expr PtrType::mkInput(State &s, const char *name,
const ParamAttrs &attrs) const {
return s.getMemory().mkInput(name, attrs);
@@ -940,6 +951,15 @@ AggregateType::refines(const State &src_s, const State &tgt_s,
return { expr::mk_and(poison), expr::mk_and(value) };
}
+StateValue AggregateType::mkUndef(State &s) const {
+ vector<StateValue> vals;
+ for (unsigned i = 0; i < elements; ++i) {
+ if (!isPadding(i))
+ vals.emplace_back(children[i]->mkUndef(s));
+ }
+ return aggregateVals(vals);
+}
+
expr AggregateType::mkInput(State &s, const char *name,
const ParamAttrs &attrs) const {
UNREACHABLE();
@@ -1367,6 +1387,10 @@ SymbolicType::refines(const State &src_s, const State &tgt_s,
DISPATCH(refines(src_s, tgt_s, src, tgt), UNREACHABLE());
}
+StateValue SymbolicType::mkUndef(State &st) const {
+ DISPATCH(mkUndef(st), UNREACHABLE());
+}
+
expr SymbolicType::mkInput(State &st, const char *name,
const ParamAttrs &attrs) const {
DISPATCH(mkInput(st, name, attrs), UNREACHABLE());

MODIFY
ir/type.h
ir/type.h
@@ -110,6 +110,7 @@ public:
refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const = 0;
+ virtual StateValue mkUndef(State &s) const;
virtual smt::expr
mkInput(State &s, const char *name, const ParamAttrs &attrs) const = 0;
virtual std::pair<smt::expr, smt::expr>
@@ -245,6 +246,7 @@ public:
std::pair<smt::expr, smt::expr>
refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
+ StateValue mkUndef(State &s) const override;
smt::expr
mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
std::pair<smt::expr, smt::expr>
@@ -302,6 +304,7 @@ public:
std::pair<smt::expr, smt::expr>
refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
+ StateValue mkUndef(State &s) const override;
smt::expr
mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
unsigned numPointerElements() const;
@@ -409,9 +412,9 @@ public:
std::pair<smt::expr, smt::expr>
refines(const State &src_s, const State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
+ StateValue mkUndef(State &s) const override;
smt::expr
- mkInput(State &s, const char *name, const ParamAttrs &attrs)
- const override;
+ mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
std::pair<smt::expr, smt::expr>
mkUndefInput(State &s, const ParamAttrs &attrs) const override;
void printVal(std::ostream &os, const State &s,

MODIFY
ir/value.cpp
ir/value.cpp
@@ -45,10 +45,7 @@ void UndefValue::print(ostream &os) const {
}
StateValue UndefValue::toSMT(State &s) const {
- auto val = getType().getDummyValue(true);
- expr var = expr::mkFreshVar("undef", val.value);
- s.addUndefVar(expr(var));
- return { move(var), move(val.non_poison) };
+ return getType().mkUndef(s);
}

ADD
tests/alive-tv/memory/undef-ptr.srctgt.ll
+define void @src() {
+ %c = alloca i8, align 1
+ call i32 @g(i32* undef)
+ ret void
+}
+
+define void @tgt() {
+ call i32 @g(i32* undef)
+ ret void
+}
+
+declare i32 @g(i32*)

fix #689: undef ptrs aliasing with local ptrs if a function has no locals