Clang inserts pointer "between" checks on high optimization

[karljs]

Running the Salsa20 SAW script example provided by @atomb for his tutorial leads to a pattern match failure for me by default.

$ saw salsa.saw
...
at :44:10: Pattern match failure in do expression at src/Lang/Crucible/LLVM/Translation/Instruction.hs:1271:14-20

When I add -O0 to the clang call in the Makefile, everything succeeds.

SAW build: nightly 2019-01-29

$ saw --version
0.2 (4099a6c)

This occurs with both clang/llvm 5.0 and 7.0 installed using Nix.

I can paste the SAW and C files if helpful, but they are contained in the saw-intro repository.

[robdockins]

Can you post the generated .bc file? I'm not able to reproduce the error, seems like your clang may be generating different code than mine.

[karljs]

@robdockins Here's the bitcode. This is generated with clang/llvm 5.0, but I can also try other versions if that's helpful.

salsa20.bc.zip

[robdockins]

Interesting... the version you sent me has done some pretty aggressive inlining and vectorization and loop elimination. I can reproduce the error with this version, I'll see if I can track down what's going on.

[robdockins]

OK, so there are a number of interesting issues with this code.

0. Clang has aggressively inlined all the interior functions, which means the compositional verification script doesn't work, but only the all-at-once verification script.
1. There was a bug involving the shufflevector instruction where the vector size of the inputs were getting mixed up, causing incorrect crucible code generation.
2. Value conversions (zext in particular) needed to be generalized over vector types.
3. Clang has done some very exciting strength reduction in s20_expand32 and introduced some ordering comparison tests on pointers from different allocation regions.

Items 1 and 2 are now fixed in master crucible, and will get pulled into saw soon.

Item 3 is a different ball of wax. The C standard says these kinds of comparisons are undefined behavior... but clang is happy to perform them and assume that there is some total ordering on allocated regions. The particular test it is doing (a pointer betweenness check) is a special idiom that actually doesn't depend on the particular ordering of regions, but recognizing this is difficult. Not exactly sure what to do about this. I'm pretty surprised clang is willing to insert this construct, actually.

[robdockins]

I think this issue can be resolved by the new lax pointer settings introduced in PR #294, once they get piped through to the SAW frontend.

[RyanGlScott]

I've opened GaloisInc/saw-script#1308 to track the SAW-side changes needed to make this work. At this point, I don't think there is anything left to do Crucible-wise, so I'll close this in favor of GaloisInc/saw-script#1308.