<div><div><div dir="auto">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.</div></div></div><div dir="auto">Please help me understand this better.</div><div dir="auto"><br></div><div dir="auto">Thanks,</div><div dir="auto">Akash.</div><div><div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Apr 4, 2020 at 10:19 PM, Roman Lebedev <<a href="mailto:lebedev.ri@gmail.com" target="_blank">lebedev.ri@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">This refinement is correct as per the LLVM IR semantics,<br>
since the memory is uninitialized.<br>
<br>
<a href="https://llvm.org/docs/LangRef.html#alloca-instruction" rel="noreferrer" target="_blank">https://llvm.org/docs/LangRef.html#alloca-instruction</a><br>
<br>
> Semantics:<br>
> Memory is allocated; a pointer is returned. The allocated memory is uninitialized,<br>
> and loading from uninitialized memory produces an undefined value.<br>
<br>
$ /repositories/alive2/build-Clang-release/alive-tv /tmp/old.ll /tmp/new.ll<br>
<br>
----------------------------------------<br>
define i32 @main() {<br>
%entry:<br>
 %A = alloca i64 4, align 16<br>
 %t = load i32, * %A, align 16<br>
 ret i32 %t<br>
}<br>
=><br>
define i32 @main() {<br>
%entry:<br>
 ret i32 undef<br>
}<br>
Transformation seems to be correct!<br>
<br>
Summary:<br>
 1 correct transformations<br>
 0 incorrect transformations<br>
 0 Alive2 errors<br>
<br>
Roman<br>
<br>
On Sat, Apr 4, 2020 at 7:34 PM Akash Banerjee via llvm-dev<br>
<<a href="mailto:llvm-dev@lists.llvm.org" target="_blank">llvm-dev@lists.llvm.org</a>> wrote:<br>
><br>
> Please consider the following C code:<br>
>     #define SZ 2048<br>
>     int main(void) {<br>
>       int A[SZ];<br>
>       int B[SZ];<br>
>       int i, tmp;<br>
>       for (i = 0; i < SZ; i++) {<br>
>         tmp = A[i];<br>
>         B[i] = tmp;<br>
>       }<br>
>       assert(A[SZ/2] == B[SZ/2]);<br>
>     }<br>
><br>
> On running -O1 followed by -reg2mem I get the following IR:<br>
> define dso_local i32 @main() local_unnamed_addr #0 {<br>
> entry:<br>
>   %A = alloca [2048 x i32], align 16<br>
>   %B = alloca [2048 x i32], align 16<br>
>   %"reg2mem alloca point" = bitcast i32 0 to i32<br>
>   %arrayidx3 = getelementptr inbounds [2048 x i32], [2048 x i32]* %A, i64 0, i64 1024<br>
>   %0 = load i32, i32* %arrayidx3, align 16<br>
>   %arrayidx4 = getelementptr inbounds [2048 x i32], [2048 x i32]* %B, i64 0, i64 1024<br>
>   %1 = load i32, i32* %arrayidx4, align 16<br>
>   %cmp5 = icmp eq i32 %0, %1<br>
>   %conv = zext i1 %cmp5 to i32<br>
>   %call = call i32 (i32, ...) bitcast (i32 (...)* @assert to i32 (i32, ...)*)(i32 %conv) #2<br>
>   ret i32 0<br>
> }<br>
><br>
> It is my understanding that in the original C code the assert would never fail, however in the optimized IR the assert might fail.<br>
> 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.<br>
> Please help me in understanding the above transformation and its legality.<br>
><br>
> Thanks,<br>
> Akash.<br>
><br>
> _______________________________________________<br>
> LLVM Developers mailing list<br>
> <a href="mailto:llvm-dev@lists.llvm.org" target="_blank">llvm-dev@lists.llvm.org</a><br>
> <a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev" rel="noreferrer" target="_blank">https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev</a><br>
</blockquote></div></div>
</div>