add AggregateType::aggregateVals()
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -76,14 +76,13 @@ AggregateConst::AggregateConst(Type &type, vector<Value*> &&vals)
: Constant(type, agg_const_str(vals)), vals(move(vals)) {}
StateValue AggregateConst::toSMT(State &s) const {
- StateValue v;
- bool first = true;
+ vector<StateValue> state_vals;
for (auto val : vals) {
- auto vv = val->getType().toBV(val->toSMT(s));
- v = first ? move(vv) : v.concat(vv);
- first = false;
+ state_vals.emplace_back(val->toSMT(s));
}
- return v;
+ auto aty = getType().getAsAggregateType();
+ assert(aty);
+ return aty->aggregateVals(state_vals);
}
expr AggregateConst::getTypeConstraints() const {

MODIFY
ir/type.cpp
ir/type.cpp
@@ -637,6 +637,17 @@ 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
@@ -229,6 +229,7 @@ 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;
};

add AggregateType::aggregateVals()