Let memset raise UB if vbytes is larger than bits_size_t
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2048,6 +2048,9 @@ StateValue Memset::toSMT(State &s) const {
auto &[vbytes, np_bytes] = s[*bytes];
s.addUB(vbytes.ugt(0).implies(np_ptr));
s.addUB(np_bytes);
+ if (vbytes.bits() > bits_size_t)
+ s.addUB(np_bytes.implies(vbytes.ule(
+ expr::mkInt(-1, bits_size_t).zext(vbytes.bits() - bits_size_t))));
s.getMemory().memset(vptr, s[*val].zextOrTrunc(8), vbytes, align);
return {};
}

ADD
tests/alive-tv/memory/memset-large.src.ll
+; TEST-ARGS: -smt-to=2000 -disable-undef-input
+declare void @llvm.memset.p0i8.i128(i8*, i8, i128, i1)
+
+define void @f(i8* %p, i128 %n) {
+ %n2 = add nuw i128 %n, 1
+ call void @llvm.memset.p0i8.i128(i8* %p, i8 0, i128 %n2, i1 0)
+ ret void
+}

ADD
tests/alive-tv/memory/memset-large.tgt.ll
+declare void @llvm.memset.p0i8.i128(i8*, i8, i128, i1)
+
+define void @f(i8* %p, i128 %n) {
+ store i8 0, i8* %p
+ %p2 = getelementptr i8, i8* %p, i64 1
+ call void @llvm.memset.p0i8.i128(i8* %p2, i8 0, i128 %n, i1 0)
+ ret void
+}

Let memset raise UB if vbytes is larger than bits_size_t (#250)