Question about inconsistency before/after LLVM's mem2reg optimization

[shaobo-he]

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.

[caballa]

The problem is that

 %2 = getelementptr inbounds %struct.f, %struct.f* undef, i32 0, i32 0

expects a cell already for the pointer operand but there is none. Typically, we solve this problem by running a pass that converts undef into nondeterminism. Right now, I was just adding patches that solve the problem of not having a cell for the gep's pointer operand case by case. I need to do it more systematic. I can have something soon.

[shaobo-he]

The problem is that

 %2 = getelementptr inbounds %struct.f, %struct.f* undef, i32 0, i32 0

expects a cell already for the pointer operand but there is none. Typically, we solve this problem by running a pass that converts undef into nondeterminism. Right now, I was just adding patches that solve the problem of not having a cell for the gep's pointer operand case by case. I need to do it more systematic. I can have something soon.

Thank you for your reply, @caballa. Btw, sea-dsa doesn't crash on the following program that's similar to the one above.

; ModuleID = 'unallocated_dereference_fail.ll'
source_filename = "unallocated_dereference_fail.c"
target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-pc-linux-gnu"

; Function Attrs: noinline nounwind uwtable
define dso_local i32 @main() #0 {
  %1 = getelementptr inbounds i32, i32* undef, i64 0
  %2 = load i32, i32* %1, align 4
  ret i32 %2
}

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)"}

I'm curious what's the difference here.