[llvm-dev] Legality of transformation

[Roman Lebedev via llvm-dev]

On Sat, Apr 4, 2020 at 8:01 PM Akash Banerjee <cs18mtech11023 at iith.ac.in> wrote:
>
> Hi, in your example instead of returning A, returning undef is fine, but in my case, although all the elements of array A are undef, B is an exact copy of A , and this notion is left out in the transformed IR, whereas the assertion which depends on it is left intact.
> Please help me understand this better.
Please see https://llvm.org/docs/LangRef.html#undefined-values
B isn't exact copy of A, they both are filled with undefined values,
so they can compare any way they wish:

----------------------------------------
define i1 @main() {
%entry:
 %A = alloca i64 4, align 16
 %B = alloca i64 4, align 16
 %t0 = load i32, * %A, align 16
 %t1 = load i32, * %B, align 16
 %cmp = icmp eq i32 %t0, %t1
 ret i1 %cmp
}
=>
define i1 @main() {
%entry:
 ret i1 0
}
Transformation seems to be correct!

Summary:
 1 correct transformations
 0 incorrect transformations
 0 Alive2 errors

----------------------------------------
define i1 @main() {
%entry:
 %A = alloca i64 4, align 16
 %B = alloca i64 4, align 16
 %t0 = load i32, * %A, align 16
 %t1 = load i32, * %B, align 16
 %cmp = icmp eq i32 %t0, %t1
 ret i1 %cmp
}
=>
define i1 @main() {
%entry:
 ret i1 1
}
Transformation seems to be correct!

Summary:
 1 correct transformations
 0 incorrect transformations
 0 Alive2 errors

----------------------------------------
define i1 @main() {
%entry:
 %A = alloca i64 4, align 16
 %B = alloca i64 4, align 16
 %t0 = load i32, * %A, align 16
 %t1 = load i32, * %B, align 16
 %cmp = icmp eq i32 %t0, %t1
 ret i1 %cmp
}
=>
define i1 @main() {
%entry:
 ret i1 undef
}
Transformation seems to be correct!

Summary:
 1 correct transformations
 0 incorrect transformations
 0 Alive2 errors

Roman

> Thanks,
> Akash.
> On Sat, Apr 4, 2020 at 10:19 PM, Roman Lebedev <lebedev.ri at gmail.com> wrote:
>>
>> This refinement is correct as per the LLVM IR semantics,
>> since the memory is uninitialized.
>>
>> https://llvm.org/docs/LangRef.html#alloca-instruction
>>
>> > Semantics:
>> > Memory is allocated; a pointer is returned. The allocated memory is uninitialized,
>> > and loading from uninitialized memory produces an undefined value.
>>
>> $ /repositories/alive2/build-Clang-release/alive-tv /tmp/old.ll /tmp/new.ll
>>
>> ----------------------------------------
>> define i32 @main() {
>> %entry:
>>  %A = alloca i64 4, align 16
>>  %t = load i32, * %A, align 16
>>  ret i32 %t
>> }
>> =>
>> define i32 @main() {
>> %entry:
>>  ret i32 undef
>> }
>> Transformation seems to be correct!
>>
>> Summary:
>>  1 correct transformations
>>  0 incorrect transformations
>>  0 Alive2 errors
>>
>> Roman
>>
>> On Sat, Apr 4, 2020 at 7:34 PM Akash Banerjee via llvm-dev
>> <llvm-dev at lists.llvm.org> wrote:
>> >
>> > Please consider the following C code:
>> >     #define SZ 2048
>> >     int main(void) {
>> >       int A[SZ];
>> >       int B[SZ];
>> >       int i, tmp;
>> >       for (i = 0; i < SZ; i++) {
>> >         tmp = A[i];
>> >         B[i] = tmp;
>> >       }
>> >       assert(A[SZ/2] == B[SZ/2]);
>> >     }
>> >
>> > On running -O1 followed by -reg2mem I get the following IR:
>> > define dso_local i32 @main() local_unnamed_addr #0 {
>> > entry:
>> >   %A = alloca [2048 x i32], align 16
>> >   %B = alloca [2048 x i32], align 16
>> >   %"reg2mem alloca point" = bitcast i32 0 to i32
>> >   %arrayidx3 = getelementptr inbounds [2048 x i32], [2048 x i32]* %A, i64 0, i64 1024
>> >   %0 = load i32, i32* %arrayidx3, align 16
>> >   %arrayidx4 = getelementptr inbounds [2048 x i32], [2048 x i32]* %B, i64 0, i64 1024
>> >   %1 = load i32, i32* %arrayidx4, align 16
>> >   %cmp5 = icmp eq i32 %0, %1
>> >   %conv = zext i1 %cmp5 to i32
>> >   %call = call i32 (i32, ...) bitcast (i32 (...)* @assert to i32 (i32, ...)*)(i32 %conv) #2
>> >   ret i32 0
>> > }
>> >
>> > It is my understanding that in the original C code the assert would never fail, however in the optimized IR the assert might fail.
>> > I tried using clang to generate the executable, and the assert doesn't fail when using -O1 but fails with -O2 and -O3 in my setting. I also tried GCC and could not get it to hit an assert fail.
>> > Please help me in understanding the above transformation and its legality.
>> >
>> > Thanks,
>> > Akash.
>> >
>> > _______________________________________________
>> > LLVM Developers mailing list
>> > llvm-dev at lists.llvm.org
>> > https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev