simplify AggregateType::aggregateVals() to always add poison padding
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -680,7 +680,7 @@ StateValue BinOp::toSMT(State &s) const {
bi->non_poison));
}
}
- return retty->aggregateVals(vals, true);
+ return retty->aggregateVals(vals);
}
if (vertical_zip) {
@@ -688,7 +688,7 @@ StateValue BinOp::toSMT(State &s) const {
auto [v1, v2] = zip_op(a.value, a.non_poison, b.value, b.non_poison);
vals.emplace_back(move(v1));
vals.emplace_back(move(v2));
- return getType().getAsAggregateType()->aggregateVals(vals, true);
+ return getType().getAsAggregateType()->aggregateVals(vals);
}
return scalar_op(a.value, a.non_poison, b.value, b.non_poison);
}
@@ -1377,6 +1377,9 @@ static StateValue update_repack(Type *type,
indices.pop_back();
vector<StateValue> vals;
for (unsigned i = 0, e = ty->numElementsConst(); i < e; ++i) {
+ if (ty->isPadding(i))
+ continue;
+
auto v = ty->extract(val, i);
if (i == cur_idx) {
vals.emplace_back(indices.empty() ?
@@ -1602,7 +1605,7 @@ pack_return(State &s, Type &ty, vector<StateValue> &vals, const FnAttrs &attrs,
continue;
vs.emplace_back(pack_return(s, agg->getChild(i), vals, attrs, idx));
}
- return agg->aggregateVals(vs, true);
+ return agg->aggregateVals(vs);
}
auto &ret = vals[idx++];
@@ -1922,7 +1925,7 @@ StateValue Freeze::toSMT(State &s) const {
auto vi = ty->extract(v, i);
vals.emplace_back(scalar(vi.value, vi.non_poison, ty->getChild(i)));
}
- return ty->aggregateVals(vals, true);
+ return ty->aggregateVals(vals);
}
return scalar(v.value, v.non_poison, getType());
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1959,7 +1959,7 @@ StateValue Memory::load(const Pointer &ptr, const Type &type, set<expr> &undef,
byteofs += getStoreByteSize(aty->getChild(i));
}
assert(byteofs == bytecount);
- return aty->aggregateVals(member_vals, true);
+ return aty->aggregateVals(member_vals);
}
bool is_ptr = type.isPtrType();

MODIFY
ir/type.cpp
ir/type.cpp
@@ -722,9 +722,8 @@ expr AggregateType::numElementsExcludingPadding() const {
return numElements() - expr::mkInt(numPaddingsConst(), elems);
}
-StateValue AggregateType::aggregateVals(const vector<StateValue> &vals,
- bool needsPadding) const {
- assert(vals.size() + (needsPadding ? numPaddingsConst() : 0) == elements);
+StateValue AggregateType::aggregateVals(const vector<StateValue> &vals) const {
+ assert(vals.size() + numPaddingsConst() == elements);
// structs can be empty
if (elements == 0)
return { expr::mkUInt(0, 1), expr::mkUInt(1, 1) };
@@ -740,7 +739,7 @@ StateValue AggregateType::aggregateVals(const vector<StateValue> &vals,
}
StateValue vv;
- if (needsPadding && isPadding(idx))
+ if (isPadding(idx))
vv = children[idx]->getDummyValue(false);
else
vv = vals[val_idx++];
@@ -810,11 +809,10 @@ unsigned AggregateType::np_bits() const {
StateValue AggregateType::getDummyValue(bool non_poison) const {
vector<StateValue> vals;
for (unsigned i = 0; i < elements; ++i) {
- if (isPadding(i))
- continue;
+ if (!isPadding(i))
vals.emplace_back(children[i]->getDummyValue(non_poison));
}
- return aggregateVals(vals, true);
+ return aggregateVals(vals);
}
expr AggregateType::getTypeConstraints() const {

MODIFY
ir/type.h
ir/type.h
@@ -269,8 +269,7 @@ public:
unsigned numElementsConst() const { return elements; }
unsigned numPaddingsConst() const;
- StateValue aggregateVals(const std::vector<StateValue> &vals,
- bool needsPadding = false) const;
+ StateValue aggregateVals(const std::vector<StateValue> &vals) const;
IR::StateValue extract(const IR::StateValue &val, unsigned index,
bool fromInt = false) const;
Type& getChild(unsigned index) const { return *children[index]; }

MODIFY
ir/value.cpp
ir/value.cpp
@@ -132,8 +132,10 @@ AggregateValue::AggregateValue(Type &type, vector<Value*> &&vals)
StateValue AggregateValue::toSMT(State &s) const {
vector<StateValue> state_vals;
- for (auto val : vals) {
- state_vals.emplace_back(val->toSMT(s));
+ auto agg = getType().getAsAggregateType();
+ for (unsigned i = 0, e = vals.size(); i < e; ++i) {
+ if (!agg->isPadding(i))
+ state_vals.emplace_back(vals[i]->toSMT(s));
}
return getType().getAsAggregateType()->aggregateVals(state_vals);
}
@@ -191,7 +193,7 @@ StateValue Input::mkInput(State &s, const Type &ty, unsigned child) const {
auto name = getSMTName(child + i);
vals.emplace_back(mkInput(s, agg->getChild(i), child + i));
}
- return agg->aggregateVals(vals, true);
+ return agg->aggregateVals(vals);
}
bool has_byval = hasAttribute(ParamAttrs::ByVal);

simplify AggregateType::aggregateVals() to always add poison padding