AggregateType maintains padding elements, and *_overflow should consider this too
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -564,7 +564,7 @@ StateValue BinOp::toSMT(State &s) const {
bi->non_poison));
}
}
- return ty->aggregateVals(vals);
+ return ty->aggregateVals(vals, true);
}
if (vertical_zip) {
@@ -572,7 +572,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);
+ return getType().getAsAggregateType()->aggregateVals(vals, true);
}
return scalar_op(a.value, a.non_poison, b.value, b.non_poison);
}
@@ -591,7 +591,7 @@ expr BinOp::getTypeConstraints(const Function &f) const {
lhs->getType() == rhs->getType();
if (auto ty = getType().getAsStructType()) {
- instrconstr &= ty->numElements() == 2 &&
+ instrconstr &= ty->numElementsExcludingPadding() == 2 &&
ty->getChild(0) == lhs->getType() &&
ty->getChild(1).enforceIntOrVectorType(1) &&
ty->getChild(1).enforceVectorTypeEquiv(lhs->getType());

MODIFY
ir/type.cpp
ir/type.cpp
@@ -701,19 +701,41 @@ expr AggregateType::numElements() const {
var("elements", var_vector_elements);
}
-StateValue AggregateType::aggregateVals(const vector<StateValue> &vals) const {
- assert(vals.size() == elements);
+unsigned AggregateType::numPaddingsConst() const {
+ unsigned count = 0;
+ for (bool b : is_padding)
+ count += b;
+ return count;
+}
+
+expr AggregateType::numElementsExcludingPadding() const {
+ auto elems = numElements();
+ return numElements() - expr::mkInt(numPaddingsConst(), elems);
+}
+
+StateValue AggregateType::aggregateVals(const vector<StateValue> &vals,
+ bool needsPadding) const {
+ assert(vals.size() + (needsPadding ? numPaddingsConst() : 0) == elements);
// structs can be empty
- if (vals.empty())
+ if (vals.empty() && !needsPadding)
return { expr::mkUInt(0, 1), true };
StateValue v;
bool first = true;
+ unsigned val_idx = 0;
for (unsigned idx = 0; idx < elements; ++idx) {
- if (children[idx]->bits() == 0)
+ if (children[idx]->bits() == 0) {
+ assert(!isPadding(idx));
+ val_idx++;
continue;
+ }
- auto vv = children[idx]->toBV(vals[idx]);
+ StateValue vv;
+ if (needsPadding && isPadding(idx))
+ vv = children[idx]->getDummyValue(false);
+ else
+ vv = vals[val_idx++];
+ vv = children[idx]->toBV(move(vv));
v = first ? move(vv) : v.concat(vv);
first = false;
}

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

ADD
tests/alive-tv/memory/umul_overflow-fail.srctgt.ll
+; TEST-ARGS: -disable-undef-input -smt-to=5000
+define void @src(i32 %a, i32 %b, {i32, i1}* %p) {
+ %mul = call { i32, i1 } @llvm.umul.with.overflow.i32(i32 %a, i32 %b)
+ store {i32, i1} %mul, {i32, i1}* %p
+ ret void
+}
+
+define void @tgt(i32 %a, i32 %b, {i32, i1}* %p) {
+ %mul = call { i32, i1 } @llvm.smul.with.overflow.i32(i32 %a, i32 %b)
+ store {i32, i1} %mul, {i32, i1}* %p
+ ret void
+}
+
+; ERROR: Mismatch in memory
+declare { i32, i1 } @llvm.umul.with.overflow.i32(i32, i32) nounwind readnone speculatable willreturn
+declare { i32, i1 } @llvm.smul.with.overflow.i32(i32, i32) nounwind readnone speculatable willreturn

ADD
tests/alive-tv/memory/umul_overflow.srctgt.ll
+; TEST-ARGS: -disable-undef-input
+define void @src(i32 %a, i32 %b, {i32, i1}* %p) {
+ %mul = call { i32, i1 } @llvm.umul.with.overflow.i32(i32 %a, i32 %b)
+ store {i32, i1} %mul, {i32, i1}* %p
+ ret void
+}
+
+define void @tgt(i32 %a, i32 %b, {i32, i1}* %p) {
+ %mul = call { i32, i1 } @llvm.umul.with.overflow.i32(i32 %a, i32 %b)
+ store {i32, i1} %mul, {i32, i1}* %p
+ ret void
+}
+
+declare { i32, i1 } @llvm.umul.with.overflow.i32(i32, i32) nounwind readnone speculatable willreturn

ADD
tests/alive-tv/sadd_overflow.srctgt.ll
+declare { i32, i1 } @llvm.sadd.with.overflow.i32(i32, i32) nounwind readnone
+
+define { i32, i1 } @src(i8 %a, i8 %b) {
+ %aa = sext i8 %a to i32
+ %bb = sext i8 %b to i32
+ %x = call { i32, i1 } @llvm.sadd.with.overflow.i32(i32 %aa, i32 %bb)
+ ret { i32, i1 } %x
+}
+
+
+define { i32, i1 } @tgt(i8 %a, i8 %b) {
+ %aa = sext i8 %a to i32
+ %bb = sext i8 %b to i32
+ %x = add nsw i32 %aa, %bb
+ %tmp = insertvalue {i32, i1} {i32 undef, i1 false}, i32 %x, 0
+ ret {i32, i1} %tmp
+}

ADD
tests/alive-tv/sadd_overflow_vec.srctgt.ll
+define <2 x i1> @src() {
+ %t = call { <2 x i32>, <2 x i1> } @llvm.sadd.with.overflow.v2i32(<2 x i32> <i32 2147483647, i32 2147483647>, <2 x i32> <i32 1, i32 1>)
+ %v = extractvalue { <2 x i32>, <2 x i1> } %t, 1
+ ret <2 x i1> %v
+}
+
+define <2 x i1> @tgt() {
+ ret <2 x i1> <i1 1, i1 1>
+}
+
+declare { <2 x i32>, <2 x i1> } @llvm.sadd.with.overflow.v2i32(<2 x i32>, <2 x i32>)

ADD
tests/alive-tv/umul_overflow.srctgt.ll
+define void @src(i32 %a, i32 %b) {
+ %mul = call { i32, i1 } @llvm.umul.with.overflow.i32(i32 %a, i32 %b)
+ ret void
+}
+
+define void @tgt(i32 %a, i32 %b) {
+ %mul = call { i32, i1 } @llvm.umul.with.overflow.i32(i32 %a, i32 %b)
+ ret void
+}
+
+declare { i32, i1 } @llvm.umul.with.overflow.i32(i32, i32) nounwind readnone speculatable willreturn

AggregateType maintains padding elements, and *_overflow should consider this too (#350)