Open
Description
alive2 report: https://alive2.llvm.org/ce/z/-RsHE_
----------------------------------------
define i64 @fun0(ptr %val0, ptr %val1, ptr %val2, i1 %val3) {
entry:
br i1 %val3, label %then, label %else
else:
br label %exit
then:
%val4 = load <4 x i32>, ptr %val1, align 16
%val5 = load <4 x i32>, ptr %val1, align 16
%val7 = select i1 0, ptr %val0, ptr %val1
br label %exit
exit:
%val8 = phi ptr [ %val7, %then ], [ null, %else ]
%val9 = load i64, ptr %val8, align 4
ret i64 %val9
}
=>
define i64 @fun0(ptr %val0, ptr %val1, ptr %val2, i1 %val3) {
entry:
br i1 %val3, label %then, label %else
else:
%val9.pre = load i64, ptr null, align 4
br label %exit
then:
%val4 = load <4 x i32>, ptr %val1, align 16
%#0 = bitcast <4 x i32> %val4 to i128
%#1 = trunc i128 %#0 to i64
br label %exit
exit:
%val9 = phi i64 [ %#1, %then ], [ %val9.pre, %else ]
ret i64 %val9
}
Transformation doesn't verify!
ERROR: Target is more poisonous than source
Example:
ptr %val0 = null / Address=#x00
ptr %val1 = pointer(non-local, block_id=2, offset=0) / Address=#x40
ptr %val2 = null / Address=#x00
i1 %val3 = #x1 (1)
Source:
>> Jump to %then
<4 x i32> %val4 = < #x00000000 (0), #x00000000 (0), poison, #x00000000 (0) >
<4 x i32> %val5 = < #x00000000 (0), #x00000000 (0), poison, #x00000000 (0) >
ptr %val7 = pointer(non-local, block_id=2, offset=0) / Address=#x40
>> Jump to %exit
ptr %val8 = pointer(non-local, block_id=2, offset=0) / Address=#x40
i64 %val9 = #x0000000000000000 (0)
SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 > size: 0 align: 4 alloc type: 0 alive: false address: 0
Contents:
*: #x00000000
Block 1 > size: 1 align: 1 alloc type: 0 alive: true address: 9
Contents:
*: #x00000000
Block 2 > size: 19 align: 1 alloc type: 0 alive: true address: 64
Contents:
if (and (= idx #b000000) (not (= idx #b000010)) (not (= idx #b000011)))
#x00000000
else
if (and (= idx #b000010) (not (= idx #b000011)))
null, byte offset=0
else
if (or (and (not (= idx #b000000)) (not (= idx #b000010)) (not (= idx #b000011)))
(= idx #b000011))
#x00000000
else
poison
Block 3 > size: 8 align: 1 alloc type: 0 alive: true address: 1
Contents:
*: #x00000000
Target:
>> Jump to %then
<4 x i32> %val4 = < #x00000000 (0), #x00000000 (0), poison, #x00000000 (0) >
i128 %#0 = poison
i64 %#1 = poison
>> Jump to %exit
i64 %val9 = poison
Source value: #x0000000000000000 (0)
Target value: poison
Summary:
0 correct transformations
1 incorrect transformations
0 failed-to-prove transformations
0 Alive2 errors
%val4
is loaded as <4 x i32>
and then loaded again as i64
.
This second load
is replaced by trunc i64 (bitcast <4 x i32> %val4 to i128)
.
But if an element of the vector is poison
, the result of trunc (bitcast ...)
is poison
in tgt
, while the result is just concatenation of the first two elements in src
.