implement freeze for aggregates
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2518,34 +2518,31 @@ void Freeze::print(ostream &os) const {
os << getName() << " = freeze " << print_type(getType()) << val->getName();
}
-StateValue Freeze::toSMT(State &s) const {
- auto &v = s[*val];
- s.resetUndefVars();
+static StateValue freeze_elems(State &s, const Type &ty, const StateValue &v) {
+ if (auto agg = ty.getAsAggregateType()) {
+ vector<StateValue> vals;
+ for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
+ if (agg->isPadding(i))
+ continue;
+ vals.emplace_back(freeze_elems(s, agg->getChild(i), agg->extract(v, i)));
+ }
+ return agg->aggregateVals(vals);
+ }
- auto scalar = [&](auto &v, auto &np, auto &ty) -> StateValue {
- if (np.isTrue())
- return { expr(v), expr(np) };
+ if (v.non_poison.isTrue())
+ return v;
StateValue ret_type = ty.getDummyValue(true);
expr nondet = expr::mkFreshVar("nondet", ret_type.value);
s.addQuantVar(nondet);
- return { expr::mkIf(np, v, std::move(nondet)), std::move(ret_type.non_poison) };
- };
-
- // TODO: support recursive aggregates
-
- if (getType().isAggregateType()) {
- vector<StateValue> vals;
- auto ty = getType().getAsAggregateType();
- for (unsigned i = 0, e = ty->numElementsConst(); i != e; ++i) {
- if (ty->isPadding(i))
- continue;
- auto vi = ty->extract(v, i);
- vals.emplace_back(scalar(vi.value, vi.non_poison, ty->getChild(i)));
+ return { expr::mkIf(v.non_poison, v.value, nondet),
+ std::move(ret_type.non_poison) };
}
- return ty->aggregateVals(vals);
- }
- return scalar(v.value, v.non_poison, getType());
+
+StateValue Freeze::toSMT(State &s) const {
+ auto &v = s[*val];
+ s.resetUndefVars();
+ return freeze_elems(s, getType(), v);
}
expr Freeze::getTypeConstraints(const Function &f) const {

implement freeze for aggregates