False negative in LoopVectorizePass on runtime-checks-difference.ll in Compiler Explorer instance

[FlashSheridan]

The following command produces an Alive2 output file, which I’ll attach, containing the unsoundness report below.

$LLVM2_BUILD/bin/llvm-lit -vva "-Dopt=$ALIVE2_HOME/alive2/build/opt-alive.sh --print-after-all" $LLVM2_HOME/llvm/test/Transforms/LoopVectorize/runtime-checks-difference.ll

Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target

Example:
ptr nocapture noundef %dst = pointer(non-local, block_id=1, offset=1, attrs=1)
ptr nocapture nowrite noundef %src = pointer(non-local, block_id=1, offset=1, attrs=3)
i64 noundef %m = #x0000000000000001 (1)
i64 noundef %n = #x0000000000000001 (1)

But the Alive2 Compiler Explorer instance says of the before and after versions of nested_loop_start_of_inner_ptr_addrec_is_same_outer_addrec (slightly modified):

Transformation seems to be correct!

Summary:
2 correct transformations
0 incorrect transformations
0 failed-to-prove transformations
0 Alive2 errors

I captured the LLVM IR as the output from --print-after-all in the above command, which I’ll also attach. I renamed the second instance of the function, and (matching the Alive2 IR in the attached file) stripped metadata (whose definitions were omitted from the output) from the end of two branch instructions. The adjusted source and results are at https://alive2.llvm.org/ce/z/9SWW42.
    I’m not sure whether the Compiler Explorer instance or my local run is correct, but presumably they can’t both be.
    I originally noticed a different problem with runtime-checks-difference.ll when running Lit under Alive2 with our local 15.0.4 fork, forcibly adding -O3, which is our normal optimization. Compiler Explorer also thought that transformation was correct.

Configuration

Alive2 ToT 1352eaa,
built with Clang ToT (18.0.0 8f6f5ec77) per the ReadMe for Translation Validation
runtime-checks-difference.ll at fd9a777e018d
MacOS 13.6.3 22G436 on M1 Max
MacOSX14.2.sdk
Xcode 15.1 15C65

Linux

Similar results on my somewhat messy Linux build:
Alive2 approximately 1352eaa,
built with Ubuntu clang version 15.0.7
LLVM 13893a08d913 (but runtime-checks-difference.ll@fd9a777e018d),
Jammy Jellyfish (22.04.2 LTS 5.15.0-72-generic x86_64)

• runtime-checks-difference_Ck4mXqEP.txt
• runtime-checks-difference.ll ToT no O3.log
• runtime-checks-difference.ll.zip

[regehr]

the CE instance gets upgraded kind of randomly, basically when I get around to it, so that may explain the discrepancy here.

one thing that I think we should do is include the commit hash in alive --version's output, instead of what we currently print:

LLVM (http://llvm.org/):
  LLVM version 18.0.0git
  Optimized build with assertions.

this sort of commit hook is a bit painful and I've totally forgotten the details but it's possible

[FlashSheridan]

the CE instance gets upgraded kind of randomly, basically when I get around to it, so that may explain the discrepancy here.

Thanks, looking forward to the next time you get around to it.

one thing that I think we should do is include the commit hash in alive --version's output, …
this sort of commit hook is a bit painful and I've totally forgotten the details but it's possible

Our LLVM fork does it, and I agree that it’s very helpful. The (somewhat old) public version of the code is at https://github.com/matter-labs/era-compiler-llvm/blob/7f77a4b04a3f7abb820b66a0a7433359d460ea08/llvm/lib/Support/CommandLine.cpp#L2750

[regehr]

here are the dates of the last few builds, including the current one from yesterday:

drwxrwxr-x 5 ce ce 4096 Oct 27 21:47 build-23
drwxrwxr-x 5 ce ce 4096 Nov  2 03:17 build-24
drwxrwxr-x 5 ce ce 4096 Nov 21 01:25 build-25
drwxrwxr-x 5 ce ce 4096 Dec 13 22:52 build

[regehr]

ah, it's already there, it's in the --help output not the --version output: https://alive2.llvm.org/ce/z/jQgHL7

so you can see that the version currently on the CE instance lines up with 030007d

[nunoplopes]

The new result is correct: there's indeed a bug in LLVM.
It's just that CE didn't catch up yet with the latest bug fixes.

[FlashSheridan]

The new result is correct: there's indeed a bug in LLVM.

Is that one of the ones you recently added to BugList.md?
 
 

It's just that CE didn't catch up yet with the latest bug fixes.

But if the CE instance lines up with 030007d (2023-12-13), shouldn’t it be at least as accurate as my local copy (1352eaa, 2023-12-05)?

[nunoplopes]

The new result is correct: there's indeed a bug in LLVM.

Is that one of the ones you recently added to BugList.md?    

No, it's a known issue in LLVM, where inttptr is introduced to calculate distance between pointers. But these pointers are marked as noescape and inttoptr escapes. I think we need a new intrinsic for pointer subtraction that doesn't escape.
It's non-trivial, that's why it hasn't been fixed yet.

It's just that CE didn't catch up yet with the latest bug fixes.

But if the CE instance lines up with 030007d (2023-12-13), shouldn’t it be at least as accurate as my local copy (1352eaa, 2023-12-05)?

I dunno. My local version reproduces the bug, so I'm happy that Alive2 is doing its job. CE will eventually catch up with the latest Alive & Z3 versions and then it will flag the bug as well.
Note that there's also some caching going on, so the result may be lagging as well because of that.

[FlashSheridan]

Thank you, I’ll add a warning to our wiki to rely on a local version of Alive2 rather than the (tempting) Compiler Explorer instance.

[regehr]

that's a good thing to warn people about, but also I think we can expect that the vast majority of test cases that people try out will find Alive's output being pretty stable over longish periods of time