Question about inconsistency before/after LLVM's mem2reg optimization #73
Description
Hello sea-dsa developers,
I still observed some crashes in SV-COMP benchmarks even after the recent fixes. So I used c-reduce to produce a minimal C program for debugging. I observed some inconsistency with respect to LLVM's mem2reg optimization. Consider the following C program that c-reduce generates (let's temporary ignore the undefineness of this program and focus on the relevant part)
struct a {
long b
};
union c {
struct a d
};
e;
struct f {
union c g
} h() {
struct f *i;
if (i->g.d.b)
e = h;
}The following LLVM-IR program is produced by the command: clang-8 -O0 -c -emit-llvm -S -Xclang -disable-O0-optnone floppy_true.i.cil.c,
; ModuleID = 'floppy_true.i.cil.c'
source_filename = "floppy_true.i.cil.c"
target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-pc-linux-gnu"
%struct.f = type { %union.c }
%union.c = type { %struct.a }
%struct.a = type { i64 }
@e = common dso_local global i32 0, align 4
; Function Attrs: noinline nounwind uwtable
define dso_local i64 @h() #0 {
%1 = alloca %struct.f, align 8
%2 = alloca %struct.f*, align 8
%3 = load %struct.f*, %struct.f** %2, align 8
%4 = getelementptr inbounds %struct.f, %struct.f* %3, i32 0, i32 0
%5 = bitcast %union.c* %4 to %struct.a*
%6 = getelementptr inbounds %struct.a, %struct.a* %5, i32 0, i32 0
%7 = load i64, i64* %6, align 8
%8 = icmp ne i64 %7, 0
br i1 %8, label %9, label %10
; <label>:9: ; preds = %0
store i32 ptrtoint (i64 ()* @h to i32), i32* @e, align 4
br label %10
; <label>:10: ; preds = %9, %0
%11 = getelementptr inbounds %struct.f, %struct.f* %1, i32 0, i32 0
%12 = getelementptr inbounds %union.c, %union.c* %11, i32 0, i32 0
%13 = getelementptr inbounds %struct.a, %struct.a* %12, i32 0, i32 0
%14 = load i64, i64* %13, align 8
ret i64 %14
}
attributes #0 = { noinline nounwind uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
!llvm.module.flags = !{!0}
!llvm.ident = !{!1}
!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{!"clang version 8.0.1- (branches/release_80)"}sea-dsa's release build works fine for this program. However, if I enable the mem2reg optimization using the command: opt-8 floppy_true.i.cil.ll -mem2reg -S -o floppy_true.i.cil.ll, sea-dsa crashes on the following optimized program,
; ModuleID = 'floppy_true.i.cil.ll'
source_filename = "floppy_true.i.cil.c"
target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-pc-linux-gnu"
%struct.f = type { %union.c }
%union.c = type { %struct.a }
%struct.a = type { i64 }
@e = common dso_local global i32 0, align 4
; Function Attrs: noinline nounwind uwtable
define dso_local i64 @h() #0 {
%1 = alloca %struct.f, align 8
%2 = getelementptr inbounds %struct.f, %struct.f* undef, i32 0, i32 0
%3 = bitcast %union.c* %2 to %struct.a*
%4 = getelementptr inbounds %struct.a, %struct.a* %3, i32 0, i32 0
%5 = load i64, i64* %4, align 8
%6 = icmp ne i64 %5, 0
br i1 %6, label %7, label %8
; <label>:7: ; preds = %0
store i32 ptrtoint (i64 ()* @h to i32), i32* @e, align 4
br label %8
; <label>:8: ; preds = %7, %0
%9 = getelementptr inbounds %struct.f, %struct.f* %1, i32 0, i32 0
%10 = getelementptr inbounds %union.c, %union.c* %9, i32 0, i32 0
%11 = getelementptr inbounds %struct.a, %struct.a* %10, i32 0, i32 0
%12 = load i64, i64* %11, align 8
ret i64 %12
}
attributes #0 = { noinline nounwind uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
!llvm.module.flags = !{!0}
!llvm.ident = !{!1}
!0 = !{i32 1, !"wchar_size", i32 4}
!1 = !{!"clang version 8.0.1- (branches/release_80)"}It appears to me mem2reg does a fairly reasonable optimization here by converting access to uninitialized location into undef. So I'd expect sea-dsa not to crash on the resulting program.