fix undef/poison values with aggregate types
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -570,7 +570,7 @@ StateValue ConversionOp::toSMT(State &s) const {
else if (getType().isIntType() && val->getType().isFloatType())
newval = v.float2BV();
else if (getType().isFloatType() && val->getType().isIntType())
- newval = v.BV2float(getType().getDummyValue());
+ newval = v.BV2float(getType().getDummyValue(true).value);
else
UNREACHABLE();
break;
@@ -796,14 +796,16 @@ StateValue FnCall::toSMT(State &s) const {
return {};
// create a new variable that can take any value if function is poison
- expr val = expr::mkUF(fnName.c_str(), value_args, getType().getDummyValue());
+ StateValue ret_type = getType().getDummyValue(true);
+ expr val = expr::mkUF(fnName.c_str(), value_args, ret_type.value);
if (!all_args_np.isTrue()) {
auto var_name = fnName + '#' + fresh_id();
- auto var = expr::mkVar(var_name.c_str(), getType().getDummyValue());
+ auto var = expr::mkVar(var_name.c_str(), ret_type.value);
s.addQuantVar(var);
val = expr::mkIf(all_args_np, val, var);
}
+ // FIXME: broken for functions that return aggregate types
auto poison_name = fnName + "#poison";
add_implies_axiom(poison_name);
@@ -1024,10 +1026,11 @@ StateValue Freeze::toSMT(State &s) const {
return { expr(v), expr(p) };
auto name = "nondet_" + fresh_id();
- expr nondet = expr::mkVar(name.c_str(), getType().getDummyValue());
+ StateValue ret_type = getType().getDummyValue(true);
+ expr nondet = expr::mkVar(name.c_str(), ret_type.value);
s.addQuantVar(nondet);
- return { expr::mkIf(p, v, move(nondet)), true };
+ return { expr::mkIf(p, v, move(nondet)), move(ret_type.non_poison) };
}
expr Freeze::getTypeConstraints(const Function &f) const {

MODIFY
ir/type.cpp
ir/type.cpp
@@ -207,7 +207,7 @@ unsigned VoidType::bits() const {
UNREACHABLE();
}
-expr VoidType::getDummyValue() const {
+StateValue VoidType::getDummyValue(bool non_poison) const {
UNREACHABLE();
}
@@ -241,8 +241,8 @@ unsigned IntType::bits() const {
return bitwidth;
}
-expr IntType::getDummyValue() const {
- return expr::mkUInt(0, bits());
+StateValue IntType::getDummyValue(bool non_poison) const {
+ return { expr::mkUInt(0, bits()), non_poison };
}
expr IntType::getTypeConstraints() const {
@@ -338,21 +338,22 @@ expr FloatType::toBV(expr e) const {
}
expr FloatType::fromBV(expr e) const {
- return e.BV2float(getDummyValue());
+ return e.BV2float(getDummyValue(true).value);
}
expr FloatType::sizeVar() const {
return defined ? expr::mkUInt(getFpType(), var_bw_bits) : Type::sizeVar();
}
-expr FloatType::getDummyValue() const {
+StateValue FloatType::getDummyValue(bool non_poison) const {
+ expr e;
switch (fpType) {
- case Half: return expr::mkHalf(0);
- case Float: return expr::mkFloat(0);
- case Double: return expr::mkDouble(0);
+ case Half: e = expr::mkHalf(0); break;
+ case Float: e = expr::mkFloat(0); break;
+ case Double: e = expr::mkDouble(0); break;
case Unknown: UNREACHABLE();
}
- UNREACHABLE();
+ return { move(e), non_poison };
}
expr FloatType::getTypeConstraints() const {
@@ -449,8 +450,8 @@ unsigned PtrType::bits() const {
return 64+8+8;
}
-expr PtrType::getDummyValue() const {
- return expr::mkUInt(0, bits());
+StateValue PtrType::getDummyValue(bool non_poison) const {
+ return { expr::mkUInt(0, bits()), non_poison };
}
expr PtrType::getTypeConstraints() const {
@@ -535,6 +536,11 @@ expr AggregateType::numElements() const {
}
StateValue AggregateType::aggregateVals(const vector<StateValue> &vals) const {
+ assert(vals.size() == elements);
+ // structs can be empty
+ if (vals.empty())
+ return { expr::mkUInt(0, 1), true };
+
StateValue v;
for (unsigned idx = 0; idx < elements; ++idx) {
auto vv = children[idx]->toBV(vals[idx]);
@@ -582,16 +588,12 @@ unsigned AggregateType::bits() const {
return bw;
}
-expr AggregateType::getDummyValue() const {
- if (elements == 0)
- return expr::mkUInt(0, 1);
-
- expr ret;
+StateValue AggregateType::getDummyValue(bool non_poison) const {
+ vector<StateValue> vals;
for (unsigned i = 0; i < elements; ++i) {
- auto v = children[i]->toBV(children[i]->getDummyValue());
- ret = i == 0 ? move(v) : ret.concat(v);
+ vals.emplace_back(children[i]->getDummyValue(non_poison));
}
- return ret;
+ return aggregateVals(vals);
}
expr AggregateType::getTypeConstraints() const {
@@ -807,14 +809,14 @@ unsigned SymbolicType::bits() const {
UNREACHABLE();
}
-expr SymbolicType::getDummyValue() const {
+StateValue SymbolicType::getDummyValue(bool non_poison) const {
switch (typ) {
- case Int: return i->getDummyValue();
- case Float: return f->getDummyValue();
- case Ptr: return p->getDummyValue();
- case Array: return a->getDummyValue();
- case Vector: return v->getDummyValue();
- case Struct: return s->getDummyValue();
+ case Int: return i->getDummyValue(non_poison);
+ case Float: return f->getDummyValue(non_poison);
+ case Ptr: return p->getDummyValue(non_poison);
+ case Array: return a->getDummyValue(non_poison);
+ case Vector: return v->getDummyValue(non_poison);
+ case Struct: return s->getDummyValue(non_poison);
case Undefined:
break;
}

MODIFY
ir/type.h
ir/type.h
@@ -42,7 +42,7 @@ public:
virtual unsigned bits() const = 0;
// to use when one needs the corresponding SMT type
- virtual smt::expr getDummyValue() const = 0;
+ virtual IR::StateValue getDummyValue(bool non_poison) const = 0;
virtual smt::expr getTypeConstraints() const = 0;
virtual smt::expr sizeVar() const;
@@ -100,7 +100,7 @@ class VoidType final : public Type {
public:
VoidType() : Type("void") {}
unsigned bits() const override;
- smt::expr getDummyValue() const override;
+ IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
void fixup(const smt::Model &m) override;
std::pair<smt::expr, smt::expr>
@@ -122,7 +122,7 @@ public:
: Type(std::move(name)), bitwidth(bitwidth), defined(true) {}
unsigned bits() const override;
- smt::expr getDummyValue() const override;
+ IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
smt::expr sizeVar() const override;
smt::expr operator==(const IntType &rhs) const;
@@ -157,7 +157,7 @@ public:
: Type(std::move(name)), fpType(fpType), defined(true) {}
unsigned bits() const override;
FpType getFpType() const { return fpType; };
- smt::expr getDummyValue() const override;
+ IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
smt::expr sizeVar() const override;
smt::expr operator==(const FloatType &rhs) const;
@@ -187,7 +187,7 @@ public:
PtrType(unsigned addr_space);
unsigned bits() const override;
- smt::expr getDummyValue() const override;
+ IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const PtrType &rhs) const;
smt::expr sameType(const PtrType &rhs) const;
@@ -228,7 +228,7 @@ public:
Type& getChild(unsigned index) const { return *children[index]; }
unsigned bits() const override;
- smt::expr getDummyValue() const override;
+ IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const AggregateType &rhs) const;
smt::expr sameType(const AggregateType &rhs) const;
@@ -297,7 +297,7 @@ public:
SymbolicType(std::string &&name, unsigned type_mask);
unsigned bits() const override;
- smt::expr getDummyValue() const override;
+ IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const Type &rhs) const;
smt::expr sameType(const Type &rhs) const;

MODIFY
ir/value.cpp
ir/value.cpp
@@ -49,9 +49,10 @@ void UndefValue::print(ostream &os) const {
StateValue UndefValue::toSMT(State &s) const {
auto name = getFreshName();
- expr var = expr::mkVar(name.c_str(), getType().getDummyValue());
+ auto val = getType().getDummyValue(true);
+ expr var = expr::mkVar(name.c_str(), val.value);
s.addUndefVar(var);
- return { move(var), true };
+ return { move(var), move(val.non_poison) };
}
string UndefValue::getFreshName() {
@@ -64,7 +65,7 @@ void PoisonValue::print(ostream &os) const {
}
StateValue PoisonValue::toSMT(State &s) const {
- return { getType().getDummyValue(), false };
+ return getType().getDummyValue(false);
}

fix undef/poison values with aggregate types