alive2
alive2 copied to clipboard
AliveToolkit
Automatic verification of LLVM optimizations
Alive2 verifies the example below (`nsw` added to `%iv.next` in `%loop`) as correct without any unrolling options and with `--disable-undef-input -tgt-unroll=1 -src-unroll=1`. It fails to verify with `--disable-undef-input -tgt-unroll=2 -src-unroll=2`....
Reduced test case from @regehr: ```llvm define void @test() { entry: %i = alloca i32, align 4 %j = alloca i32, align 4 store i32 0, i32* %i, align 4...
```llvm ; Transforms/LoopFusion/cannot_fuse.ll define float @test(float* nocapture %a, i32 %n) { entry: %conv = zext i32 %n to i64 %cmp32 = icmp eq i32 %n, 0 br i1 %cmp32, label...
https://alive2.llvm.org/ce/z/J7_Uvt This says: ``` Mismatch in pointer(non-local, block_id=0, offset=0) Source value: #x01 Target value: #x01 ``` Which is the same value ... I guess what it tries to tell us...
Skolemization is not done in the memory refinement yet: we need to raise memory mismatch in this example. ``` @p = global i8 0 @q = global i8 0 define...
see this: ```llvm define i1 @two_nonnull_mallocs() { %0: %m = malloc i64 4 %n = malloc i64 4 %cmp = icmp eq * %m, %n ret i1 %cmp } =>...
LLVM has intrinsics for FP operations that specify not only the fast-math flags, but also the rounding mode. We are only missing support for passing around the rounding mode, everything...
The test goes through if dereferenceable is removed, the %n0->null rewrite in the phi is not done, or the call or the alloca go away. Weird.. ```llvm define i32* @src(i32*...
LLVM does this (from @regehr): ``` define i1 @fn(i64 %x) { %m = malloc i64 %x %cmp = icmp eq * %m, null, use_provenance ret i1 %cmp } => define...
LLVM supports pointers with offsets smaller than pointer size: https://reviews.llvm.org/D112370 We need to fix this in Alive.
Metadata
Owner
Metadata
Automatic verification of LLVM optimizations