use the type abstractions to convert from/to BV
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -80,9 +80,7 @@ StateValue AggregateConst::toSMT(State &s) const {
for (auto val : vals) {
state_vals.emplace_back(val->toSMT(s));
}
- auto aty = getType().getAsAggregateType();
- assert(aty);
- return aty->aggregateVals(state_vals);
+ return getType().getAsAggregateType()->aggregateVals(state_vals);
}
expr AggregateConst::getTypeConstraints() const {

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -169,16 +169,6 @@ static expr fm_poison(const expr &a, const expr &b, const expr &val,
return ret;
}
-static expr mk_poison_agg(expr &poison, unsigned agg_size) {
- assert(agg_size > 0);
- expr p = poison.toBVBool();
- expr r = p;
- for (unsigned i = 1; i != agg_size; ++i) {
- r = r.concat(p);
- }
- return r;
-}
-
StateValue BinOp::toSMT(State &s) const {
auto &[a, ap] = s[*lhs];
auto &[b, bp] = s[*rhs];
@@ -301,42 +291,36 @@ StateValue BinOp::toSMT(State &s) const {
not_poison &= (b == 0u || a != 0u);
break;
- case SAdd_Overflow:
- val = a + b;
- val = val.concat((!a.add_no_soverflow(b)).toBVBool());
- not_poison = mk_poison_agg(not_poison, 2);
- break;
-
- case UAdd_Overflow:
- val = a + b;
- val = val.concat((!a.add_no_uoverflow(b)).toBVBool());
- not_poison = mk_poison_agg(not_poison, 2);
- break;
-
- case SSub_Overflow:
- val = a - b;
- val = val.concat((!a.sub_no_soverflow(b)).toBVBool());
- not_poison = mk_poison_agg(not_poison, 2);
- break;
-
- case USub_Overflow:
- val = a - b;
- val = val.concat((!a.sub_no_uoverflow(b)).toBVBool());
- not_poison = mk_poison_agg(not_poison, 2);
- break;
-
- case SMul_Overflow:
- val = a * b;
- val = val.concat((!a.mul_no_soverflow(b)).toBVBool());
- not_poison = mk_poison_agg(not_poison, 2);
- break;
-
- case UMul_Overflow:
- val = a * b;
- val = val.concat((!a.mul_no_uoverflow(b)).toBVBool());
- not_poison = mk_poison_agg(not_poison, 2);
- break;
-
+ case SAdd_Overflow: {
+ vector<StateValue> vals = { { a + b, expr(not_poison) } };
+ vals.emplace_back((!a.add_no_soverflow(b)).toBVBool(), move(not_poison));
+ return getType().getAsAggregateType()->aggregateVals(vals);
+ }
+ case UAdd_Overflow: {
+ vector<StateValue> vals = { { a + b, expr(not_poison) } };
+ vals.emplace_back((!a.add_no_uoverflow(b)).toBVBool(), move(not_poison));
+ return getType().getAsAggregateType()->aggregateVals(vals);
+ }
+ case SSub_Overflow: {
+ vector<StateValue> vals = { { a - b, expr(not_poison) } };
+ vals.emplace_back((!a.sub_no_soverflow(b)).toBVBool(), move(not_poison));
+ return getType().getAsAggregateType()->aggregateVals(vals);
+ }
+ case USub_Overflow: {
+ vector<StateValue> vals = { { a - b, expr(not_poison) } };
+ vals.emplace_back((!a.sub_no_uoverflow(b)).toBVBool(), move(not_poison));
+ return getType().getAsAggregateType()->aggregateVals(vals);
+ }
+ case SMul_Overflow: {
+ vector<StateValue> vals = { { a * b, expr(not_poison) } };
+ vals.emplace_back((!a.mul_no_soverflow(b)).toBVBool(), move(not_poison));
+ return getType().getAsAggregateType()->aggregateVals(vals);
+ }
+ case UMul_Overflow: {
+ vector<StateValue> vals = { { a * b, expr(not_poison) } };
+ vals.emplace_back((!a.mul_no_uoverflow(b)).toBVBool(), move(not_poison));
+ return getType().getAsAggregateType()->aggregateVals(vals);
+ }
case FAdd:
val = a.fadd(b);
not_poison &= !fm_poison(a, b, val, flags);
@@ -359,7 +343,7 @@ StateValue BinOp::toSMT(State &s) const {
case FRem:
// TODO; Z3 has no support for LLVM's frem which is actually an fmod
- not_poison = expr();
+ not_poison = !fm_poison(a, b, val, flags);
break;
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -210,33 +210,20 @@ void Memory::free(const expr &ptr) {
void Memory::store(const expr &p, const StateValue &v, Type &type,
unsigned align) {
- expr val = v.value;
- expr poison = v.non_poison.toBVBool();
-
- if (type.isIntType()) {
- // do nothing
- } else if (type.isFloatType()) {
- val = val.float2BV();
- } else if (type.isPtrType()) {
- // TODO
- val = expr();
- } else {
- UNREACHABLE();
- }
-
- unsigned bits = val.bits();
+ StateValue val = type.toBV(v);
+ unsigned bits = val.value.bits();
unsigned bytes = divide_up(bits, 8);
- val = val.zext(bytes * 8 - bits);
+ val.value = val.value.zext(bytes * 8 - bits);
Pointer ptr(*this, p);
ptr.is_dereferenceable(bytes, align);
for (unsigned i = 0; i < bytes; ++i) {
// FIXME: right now we store in little-endian; consider others?
- expr data = val.extract((i + 1) * 8 - 1, i * 8);
+ expr data = val.value.extract((i + 1) * 8 - 1, i * 8);
auto p = (ptr + i).release();
- blocks_val = blocks_val.store(p, poison.concat(data));
+ blocks_val = blocks_val.store(p, val.non_poison.concat(data));
}
}
@@ -246,38 +233,27 @@ StateValue Memory::load(const expr &p, Type &type, unsigned align) {
Pointer ptr(*this, p);
ptr.is_dereferenceable(bytes, align);
- expr val, non_poison;
+ StateValue val;
bool first = true;
for (unsigned i = 0; i < bytes; ++i) {
auto ptr_i = (ptr + i).release();
expr pair = blocks_val.load(ptr_i);
expr v = pair.extract(8-1, 0);
- expr p = pair.extract(8, 8) == 1;
+ expr p = pair.extract(8, 8);
if (first) {
- val = move(v);
- non_poison = move(p);
+ val.value = move(v);
+ val.non_poison = move(p);
} else {
- val = v.concat(val);
- non_poison &= p;
+ val.value = v.concat(val.value);
+ val.non_poison = p | val.non_poison;
}
first = false;
}
- val = val.trunc(bits);
- if (type.isIntType()) {
- // do nothing
- } else if (type.isFloatType()) {
- val = val.BV2float(type.getDummyValue());
- } else if (type.isPtrType()) {
- // TODO
- val = expr();
- } else {
- UNREACHABLE();
- }
-
- return { move(val), move(non_poison) };
+ val.value = val.value.trunc(bits);
+ return type.fromBV(move(val));
}
void Memory::memset(const expr &p, const StateValue &val, const expr &bytes,

MODIFY
ir/type.cpp
ir/type.cpp
@@ -495,6 +495,15 @@ expr AggregateType::numElements() const {
var("elements", var_vector_elements);
}
+StateValue AggregateType::aggregateVals(const vector<StateValue> &vals) const {
+ StateValue v;
+ for (unsigned idx = 0; idx < elements; ++idx) {
+ auto vv = children[idx]->toBV(vals[idx]);
+ v = idx == 0 ? move(vv) : v.concat(vv);
+ }
+ return v;
+}
+
StateValue AggregateType::extract(const StateValue &val, unsigned index) const {
unsigned total_till_now = 0;
for (unsigned i = 0; i < index; ++i) {
@@ -637,17 +646,6 @@ expr AggregateType::map_reduce(expr(*map)(const StateValue&, const StateValue&),
return reduce(r);
}
-StateValue AggregateType::aggregateVals(const vector<StateValue> &vals) const {
- assert(vals.size() == elements);
-
- StateValue v;
- for (unsigned idx = 0; idx < elements; ++idx) {
- auto vv = children[idx]->toBV(vals[idx]);
- v = idx == 0 ? move(vv) : v.concat(vv);
- }
- return v;
-}
-
expr ArrayType::getTypeConstraints() const {
// TODO

MODIFY
ir/type.h
ir/type.h
@@ -207,6 +207,7 @@ protected:
public:
smt::expr numElements() const;
+ StateValue aggregateVals(const std::vector<StateValue> &vals) const;
IR::StateValue extract(const IR::StateValue &val, unsigned index) const;
IR::StateValue extract(const IR::StateValue &val,
const smt::expr &index) const;
@@ -229,7 +230,6 @@ public:
smt::expr(*map)(const IR::StateValue&, const IR::StateValue&),
smt::expr(*reduce)(const std::set<smt::expr>&),
const IR::StateValue &a, const IR::StateValue &b) const override;
- StateValue aggregateVals(const std::vector<StateValue> &vals) const;
};

use the type abstractions to convert from/to BV