malloc and calloc raise UB if undef is given
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2704,8 +2704,7 @@ StateValue Malloc::toSMT(State &s) const {
s.addUB(expr(false));
auto &m = s.getMemory();
- auto &[sz, np_size] = s.getAndAddUndefs(*size);
- s.addUB(np_size);
+ auto &[sz, np_size] = s.getAndAddPoisonUB(*size, true);
unsigned align = heap_block_alignment;
expr nonnull = expr::mkBoolVar("malloc_never_fails");
@@ -2782,10 +2781,8 @@ void Calloc::print(ostream &os) const {
}
StateValue Calloc::toSMT(State &s) const {
- auto &[nm, np_num] = s.getAndAddUndefs(*num);
- auto &[sz, np_sz] = s.getAndAddUndefs(*size);
- s.addUB(np_num);
- s.addUB(np_sz);
+ auto &[nm, np_num] = s.getAndAddPoisonUB(*num, true);
+ auto &[sz, np_sz] = s.getAndAddPoisonUB(*size, true);
unsigned align = heap_block_alignment;
auto np = np_num && np_sz;

ADD
tests/alive-tv/memory/calloc-undef.srctgt.ll
+define void @src(i1 %cond) {
+ br i1 %cond, label %A, label %B
+A:
+ %ptr = call i8* @calloc(i64 undef, i64 0)
+ ret void
+B:
+ %ptr2 = call i8* @calloc(i64 0, i64 undef)
+ ret void
+}
+
+define void @tgt(i1 %cond) {
+ unreachable
+}
+
+declare i8* @calloc(i64, i64)

DELETE
tests/alive-tv/memory/malloc-undef.src.ll
-; ERROR: Value mismatch
-
-define i8 @malloc_undef() {
- %ptr = call i8* @malloc(i64 undef)
- %isnull = icmp eq i8* %ptr, null
- br i1 %isnull, label %EXIT, label %STORE
-EXIT:
- ret i8 0
-STORE:
- ret i8 1
-}
-
-declare i8* @malloc(i64)

ADD
tests/alive-tv/memory/malloc-undef.srctgt.ll
+define void @src() {
+ %ptr = call i8* @malloc(i64 undef)
+ ret void
+}
+
+define void @tgt() {
+ unreachable
+}
+
+declare i8* @malloc(i64)

DELETE
tests/alive-tv/memory/malloc-undef.tgt.ll
-define i8 @malloc_undef() {
- %ptr = call i8* @malloc(i64 undef)
- %addr = ptrtoint i8* %ptr to i64
- %isnull = icmp eq i64 %addr, 0
- br i1 %isnull, label %EXIT, label %STORE
-EXIT:
- ret i8 0
-STORE:
- ret i8 3
-}
-
-declare i8* @malloc(i64)

malloc and calloc raise UB if undef is given (#678)