fix freeze of aggregates
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1185,17 +1185,31 @@ void Freeze::print(ostream &os) const {
}
StateValue Freeze::toSMT(State &s) const {
- auto &[v, p] = s[*val];
+ auto &v = s[*val];
s.resetUndefVars();
- if (p.isTrue())
- return { expr(v), expr(p) };
+ auto scalar = [&](auto &v, auto &np, auto &ty) -> StateValue {
+ if (np.isTrue())
+ return { expr(v), expr(np) };
- StateValue ret_type = getType().getDummyValue(true);
+ StateValue ret_type = ty.getDummyValue(true);
expr nondet = expr::mkFreshVar("nondet", ret_type.value);
s.addQuantVar(nondet);
+ return { expr::mkIf(np, v, move(nondet)), move(ret_type.non_poison) };
+ };
- return { expr::mkIf(p, v, move(nondet)), 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) {
+ auto vi = ty->extract(v, i);
+ vals.emplace_back(scalar(vi.value, vi.non_poison, ty->getChild(i)));
+ }
+ return ty->aggregateVals(vals);
+ }
+ return scalar(v.value, v.non_poison, getType());
}
expr Freeze::getTypeConstraints(const Function &f) const {

MODIFY
tests/unit/freeze.opt
tests/unit/freeze.opt
@@ -5,11 +5,21 @@ Name: add
%x = add %y, %y
Name: poison
-%x = poison
+%x = i32 poison
+ =>
+%x = freeze poison
+
+Name: poison2
+%x = <2 x i4> poison
=>
%x = freeze poison
Name: undef
-%r = undef
+%r = i8 undef
+ =>
+%r = freeze undef
+
+Name: undef2
+%r = half undef
=>
%r = freeze undef

MODIFY
tests/unit/saturating.opt
tests/unit/saturating.opt
Name: add max
-%r = uadd_sat %x, -1
+%r = uadd_sat i4 %x, -1
=>
%r = -1
Name: uadd undef
-%r = uadd_sat %x, undef
+%r = uadd_sat i7 %x, undef
=>
%r = %x
@@ -41,6 +41,6 @@ Name: usub overflow
%r = 0
Name: usub undef
-%r = usub_sat %x, undef
+%r = usub_sat i7 %x, undef
=>
%r = %x

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -967,6 +967,10 @@ static unique_ptr<Instr> parse_instr(string_view name) {
case MALLOC:
return parse_malloc(name);
case INT_TYPE:
+ case HALF:
+ case FLOAT:
+ case DOUBLE:
+ case VECTOR_TYPE_PREFIX:
case NUM:
case FP_NUM:
case TRUE:

fix freeze of aggregates