fix padding of non-byte-types stores
Previously we would always set it to zero, but that would prevent removing
stores because they weren't NOPs
Fixes
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -402,6 +402,22 @@ int Memory::isInitialMemBlock(const expr &e, bool match_any_init) {
}
}
+static void pad(StateValue &v, unsigned amount, State &s) {
+ if (amount == 0)
+ return;
+
+ expr ty = expr::mkUInt(0, amount);
+ auto pad = [&](expr &v) {
+ expr var = expr::mkFreshVar("padding", ty);
+ v = var.concat(v);
+ s.addQuantVar(var);
+ };
+
+ pad(v.value);
+ if (!v.non_poison.isBool())
+ pad(v.non_poison);
+}
+
static vector<Byte> valueToBytes(const StateValue &val, const Type &fromType,
const Memory &mem, State *s) {
vector<Byte> bytes;
@@ -426,7 +442,7 @@ static vector<Byte> valueToBytes(const StateValue &val, const Type &fromType,
unsigned bitsize = bvval.bits();
unsigned bytesize = divide_up(bitsize, bits_byte);
- bvval = bvval.zext(bytesize * bits_byte - bitsize);
+ pad(bvval, bytesize * bits_byte - bitsize, *s);
unsigned np_mul = bits_poison_per_byte;
for (unsigned i = 0; i < bytesize; ++i) {

ADD
tests/alive-tv/memory/padding-nonbyte-2.srctgt.ll
+define i17 @src(i17* %p) {
+ %p2 = bitcast i17* %p to <2 x i17>*
+ store <2 x i17> <i17 1, i17 2>, <2 x i17>* %p2
+ %load = load i17, i17* %p
+ ret i17 %load
+}
+
+define i17 @tgt(i17* %p) {
+ %p2 = bitcast i17* %p to <2 x i17>*
+ store <2 x i17> <i17 1, i17 2>, <2 x i17>* %p2
+ ret i17 1
+}

ADD
tests/alive-tv/memory/padding-nonbyte-fail.srctgt.ll
+; ERROR: Value mismatch
+
+define i17 @src(i17* %p) {
+ %p2 = bitcast i17* %p to <2 x i17>*
+ store <2 x i17> <i17 1, i17 2>, <2 x i17>* %p2
+ %load = load i17, i17* %p
+ ret i17 %load
+}
+
+define i17 @tgt(i17* %p) {
+ %p2 = bitcast i17* %p to <2 x i17>*
+ store <2 x i17> <i17 1, i17 2>, <2 x i17>* %p2
+ ret i17 2
+}

ADD
tests/alive-tv/memory/padding-nonbyte.srctgt.ll
+define void @src(i28* %in) {
+ %val2 = load i28, i28* %in, align 4
+ store i28 %val2, i28* %in, align 4
+ ret void
+}
+
+define void @tgt(i28* %in) {
+ ret void
+}

fix padding of non-byte-types stores
Previously we would always set it to zero, but that would prevent removing
stores because they weren't NOPs
Fixes #701