adding --disable-undef-input and --disable-poison-input creates a value mismatch (with --tgt-is-asm)

[regehr]

ok this one really made me tear my hair out. here's a src and tgt where Alive validates refinement

source_filename = "M2"
target datalayout = "e-m:e-i8:8:32-i16:16:32-i64:64-i128:128-n32:64-S128"
target triple = "aarch64-linux-gnu"

define ptr @indexed_compare(ptr %0, i64 %1) {
  %3 = getelementptr inbounds i32, ptr %0, i64 %1
  br label %4

4:                                                ; preds = %4, %2
  %5 = phi ptr [ %7, %4 ], [ %3, %2 ]
  %6 = getelementptr inbounds i32, ptr %0, i32 100
  %7 = getelementptr inbounds i32, ptr %5, i64 1
  %8 = icmp ult ptr %6, %5
  br i1 %8, label %9, label %4

9:                                                ; preds = %4
  ret ptr %5
}

; ModuleID = 'M2'
source_filename = "M2"
target datalayout = "e-m:e-i8:8:32-i16:16:32-i64:64-i128:128-n32:64-S128"
target triple = "aarch64-linux-gnu"

; Function Attrs: nofree norecurse nosync nounwind memory(none)
define ptr @indexed_compare(ptr %0, i64 %1) local_unnamed_addr #0 {
arm_tv_entry:
  %2 = ptrtoint ptr %0 to i64
  %a2_2 = shl i64 %1, 2
  %a2_4 = add i64 %2, -4
  %a3_1 = add i64 %a2_4, %a2_2
  %a5_1 = add i64 %2, 400
  br label %.LBB0_1

.LBB0_1:                                          ; preds = %.LBB0_1, %arm_tv_entry
  %X8.0 = phi i64 [ %a3_1, %arm_tv_entry ], [ %a6_1, %.LBB0_1 ]
  %a6_1 = add i64 %X8.0, 4
  %a7_5.not = icmp ult i64 %a5_1, %a6_1
  br i1 %a7_5.not, label %"1", label %.LBB0_1

"1":                                              ; preds = %.LBB0_1
  %3 = inttoptr i64 %a6_1 to ptr
  ret ptr %3
}

attributes #0 = { nofree norecurse nosync nounwind memory(none) }

I'll leave out the output. it also validates when either poison or undef is disabled. but when I disable both I get this value mismatch with a nonsensical CEX.

regehr@ohm:~/tmp$ ~/alive2-regehr/build/alive-tv test-997574204.ll tgt.ll --tgt-is-asm --disable-undef-input --disable-poison-input

----------------------------------------
define ptr @indexed_compare(ptr %#0, i64 %#1) {
#2:
  %#5 = gep inbounds ptr %#0, 4 x i64 %#1
  br label %#3

#3:
  %#6 = phi ptr [ %#8, %#3 ], [ %#5, %#2 ]
  %#7 = gep inbounds ptr %#0, 4 x i32 100
  %#8 = gep inbounds ptr %#6, 4 x i64 1
  %#9 = icmp ult ptr %#7, %#6
  br i1 %#9, label %#4, label %#3

#4:
  ret ptr %#6
}
=>
define ptr @indexed_compare(ptr %#0, i64 %#1) nofree asm memory(none) {
arm_tv_entry:
  %#2 = ptrtoint ptr %#0 to i64
  %a2_2 = shl i64 %#1, 2
  %a2_4 = add i64 %#2, -4
  %a3_1 = add i64 %a2_4, %a2_2
  %a5_1 = add i64 %#2, 400
  br label %.LBB0_1

.LBB0_1:
  %X8.0 = phi i64 [ %a3_1, %arm_tv_entry ], [ %a6_1, %.LBB0_1 ]
  %a6_1 = add i64 %X8.0, 4
  %a7_5.not = icmp ult i64 %a5_1, %a6_1
  br i1 %a7_5.not, label %1, label %.LBB0_1

1:
  %#3 = int2ptr i64 %a6_1 to ptr
  ret ptr %#3
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:
ptr %#0 = pointer(non-local, block_id=1, offset=0)
i64 %#1 = #x00000000000000fd (253)

Source:
ptr %#5 = pointer(non-local, block_id=1, offset=1012)
  >> Jump to %#3
ptr %#6 = pointer(non-local, block_id=1, offset=1012)
ptr %#7 = pointer(non-local, block_id=1, offset=400)
ptr %#8 = poison
i1 %#9 = #x1 (1)
  >> Jump to %#4

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >   size: 0 align: 1    alloc type: 0   alive: false    address: 0
Block 1 >   size: 1012  align: 1    alloc type: 0   alive: true address: 12

Target:
i64 %#2 = #x000000000000000c (12)
i64 %a2_2 = #x00000000000003f4 (1012)
i64 %a2_4 = #x0000000000000008 (8)
i64 %a3_1 = #x00000000000003fc (1020)
i64 %a5_1 = #x000000000000019c (412)
  >> Jump to %.LBB0_1
i64 %X8.0 = #x00000000000003fc (1020)
i64 %a6_1 = #x0000000000000400 (1024)
i1 %a7_5.not = #x1 (1)
  >> Jump to %1
ptr %#3 = pointer(non-local, block_id=1, offset=1012)
Source value: pointer(non-local, block_id=1, offset=1012)
Target value: pointer(non-local, block_id=1, offset=1012)

Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors
regehr@ohm:~/tmp$ 

[regehr]

regehr@ohm:~/alive2-regehr/build$ cat src.ll 
; ModuleID = 'M2'
source_filename = "M2"
target datalayout = "e-m:e-i8:8:32-i16:16:32-i64:64-i128:128-n32:64-S128"
target triple = "aarch64-linux-gnu"

define ptr @test_array2(ptr %0) {
  %2 = getelementptr inbounds i32, ptr %0, i64 4
  ret ptr %2
}
regehr@ohm:~/alive2-regehr/build$ cat tgt.ll
; ModuleID = 'M2'
source_filename = "M2"
target datalayout = "e-m:e-i8:8:32-i16:16:32-i64:64-i128:128-n32:64-S128"
target triple = "aarch64-linux-gnu"

; Function Attrs: mustprogress nofree norecurse nosync nounwind willreturn memory(none)
define ptr @test_array2(ptr %0) local_unnamed_addr #0 {
arm_tv_entry:
  %1 = ptrtoint ptr %0 to i64
  %a2_1 = add i64 %1, 16
  %2 = inttoptr i64 %a2_1 to ptr
  ret ptr %2
}

attributes #0 = { mustprogress nofree norecurse nosync nounwind willreturn memory(none) }
regehr@ohm:~/alive2-regehr/build$ ./alive-tv src.ll tgt.ll --tgt-is-asm

----------------------------------------
define ptr @test_array2(ptr %#0) {
#1:
  %#2 = gep inbounds ptr %#0, 4 x i64 4
  ret ptr %#2
}
=>
define ptr @test_array2(ptr %#0) nofree willreturn asm memory(none) {
arm_tv_entry:
  %#1 = ptrtoint ptr %#0 to i64
  %a2_1 = add i64 %#1, 16
  %#2 = int2ptr i64 %a2_1 to ptr
  ret ptr %#2
}
Transformation seems to be correct!

Summary:
  1 correct transformations
  0 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors
regehr@ohm:~/alive2-regehr/build$ ./alive-tv src.ll tgt.ll --tgt-is-asm --disable-undef-input

----------------------------------------
define ptr @test_array2(ptr %#0) {
#1:
  %#2 = gep inbounds ptr %#0, 4 x i64 4
  ret ptr %#2
}
=>
define ptr @test_array2(ptr %#0) nofree willreturn asm memory(none) {
arm_tv_entry:
  %#1 = ptrtoint ptr %#0 to i64
  %a2_1 = add i64 %#1, 16
  %#2 = int2ptr i64 %a2_1 to ptr
  ret ptr %#2
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:
ptr %#0 = pointer(non-local, block_id=1, offset=0, attrs=1)

Source:
ptr %#2 = pointer(non-local, block_id=1, offset=16, attrs=1)

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >   size: 0 align: 1    alloc type: 0   alive: false    address: 0
Block 1 >   size: 16    align: 1    alloc type: 0   alive: true address: 14

Target:
i64 %#1 = #x000000000000000e (14)
i64 %a2_1 = #x000000000000001e (30)
ptr %#2 = pointer(non-local, block_id=1, offset=16)
Source value: pointer(non-local, block_id=1, offset=16, attrs=1)
Target value: pointer(non-local, block_id=1, offset=16)

Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors
regehr@ohm:~/alive2-regehr/build$ 

[regehr]

still running into this issue. I can stop using --disable-undef-input but I don't want undefs on the src side either, so I would like to use that flag.

I'm also running into issues where something validates on one of my machines and gives a value mismatch on another -- that should never happen, right?

[nunoplopes]

Yeah, that's bad. You may have a bad Z3 is one of the machines. Z3 was a bit broken for a couple of weeks; you may have caught it. I can't reproduce the error you pasted above on my computer.

[regehr]

oh no!!! this is my main compute machine and I rebuilt Z3 there last night just before sending you this :(

[regehr]

I ran these on both machines with --se-verbose --smt-log and the Z3 queries are different, here's the difff

Johns-MacBook-Pro:build regehr$ diff -cbw out.txt out-ohm.txt 
*** out.txt Tue Nov 21 09:17:59 2023
--- out-ohm.txt Tue Nov 21 09:18:41 2023
***************
*** 19,27 ****
       (bvule ((_ extract 63 0) |%#0|)
              (concat #b0 (blk_size ((_ extract 64 64) |%#0|))))
       (not (= #b1 ((_ extract 63 63) |%#0|)))
       (bvule (bvadd ((_ extract 63 0) |%#0|) #x0000000000000010)
              (concat #b0 (blk_size ((_ extract 64 64) |%#0|))))
-      (bvsle ((_ extract 63 0) |%#0|) #x7fffffffffffffef)
       (not (= #b1
               ((_ extract 63 63)
                 (bvadd ((_ extract 63 0) |%#0|) #x0000000000000010))))) / UB=(= #b0 |isundef_%#0|)
--- 19,27 ----
       (bvule ((_ extract 63 0) |%#0|)
              (concat #b0 (blk_size ((_ extract 64 64) |%#0|))))
       (not (= #b1 ((_ extract 63 63) |%#0|)))
+      (bvsle ((_ extract 63 0) |%#0|) #x7fffffffffffffef)
       (bvule (bvadd ((_ extract 63 0) |%#0|) #x0000000000000010)
              (concat #b0 (blk_size ((_ extract 64 64) |%#0|))))
       (not (= #b1
               ((_ extract 63 63)
                 (bvadd ((_ extract 63 0) |%#0|) #x0000000000000010))))) / UB=(= #b0 |isundef_%#0|)
***************
*** 34,42 ****
       (bvule ((_ extract 63 0) |%#0|)
              (concat #b0 (blk_size ((_ extract 64 64) |%#0|))))
       (not (= #b1 ((_ extract 63 63) |%#0|)))
       (bvule (bvadd ((_ extract 63 0) |%#0|) #x0000000000000010)
              (concat #b0 (blk_size ((_ extract 64 64) |%#0|))))
-      (bvsle ((_ extract 63 0) |%#0|) #x7fffffffffffffef)
       (not (= #b1
               ((_ extract 63 63)
                 (bvadd ((_ extract 63 0) |%#0|) #x0000000000000010)))))
--- 34,42 ----
       (bvule ((_ extract 63 0) |%#0|)
              (concat #b0 (blk_size ((_ extract 64 64) |%#0|))))
       (not (= #b1 ((_ extract 63 63) |%#0|)))
+      (bvsle ((_ extract 63 0) |%#0|) #x7fffffffffffffef)
       (bvule (bvadd ((_ extract 63 0) |%#0|) #x0000000000000010)
              (concat #b0 (blk_size ((_ extract 64 64) |%#0|))))
       (not (= #b1
               ((_ extract 63 63)
                 (bvadd ((_ extract 63 0) |%#0|) #x0000000000000010)))))
***************
*** 111,120 ****
  ((_ extract 64 64) |%#0|): non-local: 11

! Transformation seems to be correct!

  Summary:
!   1 correct transformations
!   0 incorrect transformations
    0 failed-to-prove transformations
    0 Alive2 errors
--- 111,141 ----
  ((_ extract 64 64) |%#0|): non-local: 11

! Transformation doesn't verify!

+ ERROR: Value mismatch
+ 
+ Example:
+ ptr %#0 = pointer(non-local, block_id=1, offset=0, attrs=1)
+ 
+ Source:
+ ptr %#2 = pointer(non-local, block_id=1, offset=16, attrs=1)
+ 
+ SOURCE MEMORY STATE
+ ===================
+ NON-LOCAL BLOCKS:
+ Block 0 > size: 0 align: 1    alloc type: 0   alive: false    address: 0
+ Block 1 > size: 16    align: 1    alloc type: 0   alive: true address: 14
+ 
+ Target:
+ i64 %#1 = #x000000000000000e (14)
+ i64 %a2_1 = #x000000000000001e (30)
+ ptr %#2 = pointer(non-local, block_id=1, offset=16)
+ Source value: pointer(non-local, block_id=1, offset=16, attrs=1)
+ Target value: pointer(non-local, block_id=1, offset=16)
+ 
  Summary:
!   0 correct transformations
!   1 incorrect transformations
    0 failed-to-prove transformations
    0 Alive2 errors
Johns-MacBook-Pro:build regehr$ 

[regehr]

the execution of alive-tv that signals a value mismatch is clean as far as valgrind can tell. I can't check the other one since that one is running on my Mac.

I recompiled both Z3 and Alive2 with Clang instead of GCC and I still see this value mismatch. but the counterexample is different now. argh!!!! something is really broken here.

[regehr]

worse still, when I build Z3 and Alive2 with -fsanitize=address,undefined the problem goes away but no errors are signaled.

this behavior is recent, I'm afraid something has gone badly wrong in Z3 lately

[regehr]

anyhow, although I'd like to help debug this, I don't have a mechanism for doing that, I've backed off to an older Z3 and will just use that for a while