llvm dev - Apr 2020 - Legality of transformation

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20200404/014bff91/attachment.html>

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

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.

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20200404/aee10590/attachment-0001.html>

On Sat, Apr 4, 2020 at 9:33 AM 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.
>
Reading uninitialized memory is undefined behavior in C I believe, so even
without talking about LLVM IR semantics your original program is incorrect
as soon a you read from A.

clang ub.c -fsanitize=memory && ./a.out

*==10365==WARNING: MemorySanitizer: use-of-uninitialized-value*

    #0 0x496ce7 in main (/tmp/a.out+0x496ce7)

    #1 0x7f2e71f27bba in __libc_start_main
(/lib/x86_64-linux-gnu/libc.so.6+0x26bba)

    #2 0x41e299 in _start (/tmp/a.out+0x41e299)


SUMMARY: MemorySanitizer: use-of-uninitialized-value (/tmp/a.out+0x496ce7)
in main

Exiting


-- 
Mehdi
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20200404/5495d0a2/attachment.html>

On 4/4/20 12:23 PM, Mehdi AMINI via llvm-dev wrote:
> On Sat, Apr 4, 2020 at 9:33 AM 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.
>>
> Reading uninitialized memory is undefined behavior in C I believe, so even
> without talking about LLVM IR semantics your original program is incorrect
> as soon a you read from A.
I don't think reading and writing undef values is not undefined behavior 
(in IR).

Using undef values in branches (and some other ways) is.

The "problem" here is, as Roman noted, the fact that you cannot assume
either of these hold:

   `undef != undef` or `undef == undef`.


Cheers,

   Johannes

> clang ub.c -fsanitize=memory && ./a.out
>
> *==10365==WARNING: MemorySanitizer: use-of-uninitialized-value*
>
>      #0 0x496ce7 in main (/tmp/a.out+0x496ce7)
>
>      #1 0x7f2e71f27bba in __libc_start_main
> (/lib/x86_64-linux-gnu/libc.so.6+0x26bba)
>
>      #2 0x41e299 in _start (/tmp/a.out+0x41e299)
>
>
> SUMMARY: MemorySanitizer: use-of-uninitialized-value (/tmp/a.out+0x496ce7)
> in main
>
> Exiting
>
>
>
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20200405/cf972136/attachment.html>