search for: alive2

Hi folks, I've been running a Compiler Explorer instance with Alive2 on a machine in my office, but availability has been poor due to random factors and of course recently it hasn't been easy or convenient to go in and fix things when the machine gets wedged. Nuno and I would like to ask the LLVM community if it's OK to point alive.llvm.org at a cloud m...

+1 to alive2.llvm.org On Thu, Jun 18, 2020 at 8:11 AM John Regehr via llvm-dev <llvm-dev at lists.llvm.org> wrote: > > > If we can get Alive1 up there too, that would be even better. I still > > use that to try to prove things where it's not obvious how to express > > the relatio...

No concerns from me. I use Alive2 all the time, and it would be fantastic to have it available online reliably. If we can get Alive1 up there too, that would be even better. I still use that to try to prove things where it's not obvious how to express the relationships in pure LLVM IR: https://rise4fun.com/Alive/NDu On Wed,...

...stead do a sensible thing and actually make them first class citizens, by introducing intrinsics and use then throughout. This has been previously discussed in: https://lists.llvm.org/pipermail/llvm-dev/2016-November/106868.html Proposed LangRef semantics: https://reviews.llvm.org/D81829 Proposed alive2 implementation: https://github.com/AliveToolkit/alive2/pull/353 Roman.

...able to identify that CC could have been either 0 or 1 (effectively avoiding the 'default' case of the switch and therefore the '0xdeadc0de' constant). As a result the function 'tgt' is optimized in the way I would expect it to be. This also seemed to be a good exercise for Alive2, so I fed it with the unoptimized 'src' and the optimized 'tgt' functions to prove their equivalence, obtaining the result 'Transformation seems to be correct'. As a counter-proof I tampered with the logic or modified the constants, obtaining a valid proof of why the transfo...

...select instructions, which leads to multiple reads from v, which changes the result when v is undef. We should be able to fix this in our compiler by inserting a freeze instruction, but to me this raises a more complicated point around function inlining that is illustrated by this example: https://alive2.llvm.org/ce/z/wcYxCB (I don't know if the output of Alive2 is meaningful here or if there are limitations around function calls). Function inlining in LLVM currently does *not* introduce freezes. However, calls to intrinsics such as llvm.minimum.* etc. are presumably expected to introduce free...

Hi everyone, In a twitch chat someone redirected me to an example that is not optimized: https://godbolt.org/z/BL-4jL I included the original source code and this is after -O2. We both thought that the -8 branch could be optimized out. I added a nuw in the subtraction and it actually does it. Any thoughts on why that doesn't happen already? Best, Stefanos Baziotis -------------- next part

I came across this comment in SelectionDAG.cpp: case ISD::FADD: case ISD::FSUB: case ISD::FMUL: case ISD::FDIV: case ISD::FREM: // If both operands are undef, the result is undef. If 1 operand is undef, // the result is NaN. This should match the behavior of the IR optimizer. That isn't intuitive to me. I would have expected a binary FP operation with one undef operand to

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

There's a question about the behavior of funnel shift [1] + select and poison here that reminds me of previous discussions about select and poison [2]: https://github.com/AliveToolkit/alive2/pull/32#discussion_r257528880 Example: define i8 @fshl_zero_shift_guard(i8 %x, i8 %y, i8 %sh) { %c = icmp eq i8 %sh, 0 %f = fshl i8 %x, i8 %y, i8 %sh %s = select i1 %c, i8 %x, i8 %f ; shift amount is 0 returns x (same as fshl) ret i8 %s } => define i8 @fshl_zero_shift_guard(i8 %x, i8 %y, i8 %sh...

On Fri, Feb 7, 2020 at 12:29 PM Nuno Lopes <nunoplopes at sapo.pt> wrote: > > It's not correct (output of Alive2): > > define half @fn(half %a) { > %b = fadd half %a, undef > ret half %b > } > => > define half @fn(half %a) { > ret half undef > } > Transformation doesn't verify! > ERROR: Value mismatch > > Example: > half %a = #x0e02 (0.000366687774?) &...

...e code will be at runtime. Besides providing the ability to call the function, that pointer can also be used, after bitcasting it, to modify the machine code implementing the function. What does the optimizer assume about the memory containing the machine code? The following is an example where Alive2 assumes that transforming @src to @tgt is correct (note that @f is marked readnone): declare i32 @f() readnone declare void @modify_f() define i32 @src() { call void @modify_f() %r = call i32 @f() ret i32 %r } define i32 @tgt() { %r = call i32 @f() call void @modify_f() ret i...

Hi, I've been wondering why LLVMs GEP instructions are based on types, rather than encoding the raw address calculation as a base pointer plus some scaled offsets (still in the form of a GEP, to retain provenance). The type information does not seem particularly useful (shouldn't be used as an optimization base, because struct layouts lie), but increases the non-canonical IR space (there

Hello, This is an RFC for adding intrinsics which perform saturating signed/unsigned left shift. There is currently a patch on Phabricator here: https://reviews.llvm.org/D83216 The intrinsics are of the form i32 @llvm.sshl.sat.i32(i32, i32) i32 @llvm.ushl.sat.i32(i32, i32) <4 x i32> @llvm.sshl.sat.v4i32(<4 x i32>, <4 x i32>) <4 x i32>

...y 25, 2019 4:29 PM > Subject: [llvm-dev] funnel shift, select, and poison > > > There's a question about the behavior of funnel shift [1] + select and > poison here that reminds me of previous discussions about select and > poison > [2]: > https://github.com/AliveToolkit/alive2/pull/32#discussion_r257528880 > > Example: > define i8 @fshl_zero_shift_guard(i8 %x, i8 %y, i8 %sh) { > %c = icmp eq i8 %sh, 0 > %f = fshl i8 %x, i8 %y, i8 %sh > %s = select i1 %c, i8 %x, i8 %f ; shift amount is 0 returns x (same as > fshl) > ret i8 %s > } > => >...

Ok, makes sense. My suggestion is that we patch the IR Verifier to ensure that the mask is indeed a vector of constants and/or undefs. Right now it only runs the standard checks for instructions. We will also run Alive2 on the test suite to make sure undef is never replaced in practice. Thanks, Nuno -----Original Message----- From: Eli Friedman <efriedma at quicinc.com> Sent: 27 de novembro de 2019 01:10 To: Nuno Lopes <nuno.lopes at ist.utl.pt>; LLVMdev <llvm-dev at lists.llvm.org> Cc: spatel...

...bruary 25, 2019 4:29 PM > Subject: [llvm-dev] funnel shift, select, and poison > > > There's a question about the behavior of funnel shift [1] + select and > poison here that reminds me of previous discussions about select and poison > [2]: > https://github.com/AliveToolkit/alive2/pull/32#discussion_r257528880 > > Example: > define i8 @fshl_zero_shift_guard(i8 %x, i8 %y, i8 %sh) { > %c = icmp eq i8 %sh, 0 > %f = fshl i8 %x, i8 %y, i8 %sh > %s = select i1 %c, i8 %x, i8 %f ; shift amount is 0 returns x (same as > fshl) > ret i8 %s > } > => >...

Hi John, I hadn't seen alive2, amazing program, thank you! Keep up the good work. > I'm not sure that I've captured what you mean here To be more specific for everyone: - First of all, I hope it's clear that in the original (C) code, the region - 0x8 > 1000 branch should be eliminated. That is because it is...

...oring values in structures or unions is unspecified. - IPSCCP ignores padding and directly stores a constant aggregate if possible: https://godbolt.org/z/ddWq9z Memcpyopt ignores padding when copying an aggregate or storing a constant: https://godbolt.org/z/hY6ndd / https://godbolt.org/z/3WMP5a - Alive2 (with store operation updated) did not find any problematic transformation from LLVM unit tests and while running translation validation on a few C programs. The patch is here: https://reviews.llvm.org/D86189 Thanks, Juneyoung -- Juneyoung Lee Software Foundation Lab, Seoul National University...

define dso_local i32 @f(i32 %0) { %2 = and i32 %0, 7 %3 = icmp eq i32 %2, 7 %4 = zext i1 %3 to i32 ret i32 %4 } I thought instcombine would remove it. It doesn't and nothing else does either. LLVM Version is 10.0.0. /Riyaz -------------- next part -------------- An HTML attachment was scrubbed... URL: