alive2
alive2 copied to clipboard
AliveToolkit
Volatile load/store support
https://bugs.llvm.org/show_bug.cgi?id=45360 is reporting a newly-exposed miscompile, but the test case contains volatile accesses, and alive2 doesn't like those. While i can get alive to accept test cases by manually dropping volatile quals, i'm not sure if that is semantically-preserving.
that test case has a randomly generated look to it, and also a C-Reduced look to it :)
if I am correct, then the volatile is necessary (or else C-Reduce would have eliminated it) but not semantically meaningful in any high-level sense. so it should be OK to take the code before and after the buggy optimization, and at that point remove the volatiles, if that makes sense.
regarding supporting volatile accesses in alive2: this requires the same machinery as supporting side-effecting function calls. we have to keep a log of volatile accesses in src and tgt, and then ensure that for every input, src and tgt produce the same log.
Ok, I had not been paying attention to this but it looks like we properly record side-effecting functions: http://volta.cs.utah.edu:8080/z/y9ZuRW Thus, I hope supporting volatile accesses using the same mechanism isn't too difficult, is this correct @nunoplopes and @aqjune ? If nobody plans to work on this in the near future I may be able to get one of my people to do it.
Indeed, there are many volatile loads/stores in LLVM unit tests, and we are skipping them. It will be great they can be inspected as well.
The way how fn calls are encoded is as follows. We have axioms stating that for any two function call instructions (in either src or tgt), if (1) they are calling the same function (2) inputs(=args + input mem) are same, then their output (ret val & memory) should be same as well. To be precise, it is refinement rather than equality, but anyway it works like this at the high-level.
To encode volatile accesses: for v = load retty volatile ptr, we can assume that it is a function call v = call load_volatile_retty(ptr). Similarly for store.
One case that I'm uncertain is the semantics of volatile load/store on local blocks, such as alloca. Do they also have side effects? The level of difficulty of volatile encoding seems to be quite dependent on this.
I wonder what @nunoplopes think as well.
I'd like to implement this by myself. It might not be very close future, because I'm using my bandwidth mainly for adding/optimizing freezes in LLVM right now. The reason why I'd like to work on this is that I have a submitted paper for encoding LLVM memory model in SMT, and I think it should be mentioned there if volatile is added to Alive2. :)
Hi Juneyoung, this all sounds great.
My reading of the Langref is that volatile accesses to local blocks are treated exactly the same as other volatile accesses: accesses may not be added or removed.
One potential difficulty in volatile is that it probably should be encoded per-byte, because for example it is legal to take 4 adjacent 1-byte volatile loads and coalesce them into a single 4-byte load.
@LebedevRI if after removing volatile a test fail with Alive2, then it would fail as well with volatile. The problem is that it may pass without volatile and fail with it. That's why right now we don't attempt to run the test by simply ignoring volatile.
This feature is not high on my priority list, though. Nor on Juneyoung's, despite his excitement :) There are a lot of other things to do before this..
actually I was wrong above. C and C++ allow splitting/merging of volatile accesses but LLVM doesn't:
IR-level volatile loads and stores cannot safely be optimized into llvm.memcpy or llvm.memmove intrinsics even when those intrinsics are flagged volatile. Likewise, the backend should never split or merge target-legal volatile load/store instructions. Similarly, IR-level volatile loads and stores cannot change from integer to floating-point or vice versa.
FYI, I share Alive2's stats from LLVM's unit tests at 1179e30.
noalias is the top 1 for unsupported ir feature, partially because it appears a lot, partially because it hides all other reasons (noalias appears at function signature).
metadata 7 seems to be alias.scope. noalias + alias.scope + volatile are all hard.. :/
memcmp is the one that I'm going to attack after noreturn (#309) is resolved. Fixing noreturn PR wouldn't take very long time, I hope.
For non-memory things, llvm.fabs / ffs / ffsll seems interesting and easy to attack. Is the semantics of these straightforward? (I wouldn't be surprised if it turns out to be non-trivial. :) ) There is llvm.experimental.widenable.condition too, but I couldn't fully understand what its semantics is. Is it okay for it to be encoded as just a function returning boolean value without touching memory?
@zhengyangl want do fabs, ffs, and ffsll?
llvm.experimental.widenable.condition is weird! it looks to me like returning an indeterminate i1 is the correct modeling
regarding other unsupported functions:
printf and fprintf are easy when the return value is ignored, we could just model these as returning an arbitrary i32 and see what happens?
@zhengyangl are pow, powf, and exp2 very difficult? I would imagine that sqrt, sin, cos, exp, and log might be very difficult for z3. maxnum, minnum, ceil, and nearbyint all seem pretty easy for us and for z3.
LLVM doesn't optimize most functions, or just considers simple cases. Most recognized functions are just so LLVM can add readsonly/whatever attributes. We just need to learn the same tricks as LLVM, not full modeling of the whole libc.
These trivial ones seems easy to implement. I will send a patch for llvm.[maxnum|minnum|ceil|floor|nearbyint|fabs]. And after that I'll send another patch for ffs/ffsll.
@nunoplopes Hi Nuno, I am working on maxnum and minnum, llvm langref* is saying that minnum(+/-0.0, +/-0.0) could return either -0.0 or 0.0. How do we model this definition in alive2?
* https://llvm.org/docs/LangRef.html#id504
I think it should be nondeterministic choice (as freeze does) to support following transformations:
minnum(x, y) -> minnum(y, x) // commutativity should hold when x = 0.0 & y = -0.0
minnum(x, y) -> minnum(x, y) // identity should hold when x = 0.0 & y = -0.0
But to be sure I suggest running LLVM unit tests & double check whether it does not raise spurious errors.
Update: Maybe simpler encoding should be always returning -0.0 ; it will explain optimization
minnum(x, y) -> y // if x is guaranteed to be positive & y is guaranteed to be negative
... but I'm not 100% sure, running unit tests will really help.
@aqjune Hi Juneyoung, after encoding returning -0 for the input (+0, -0) and (-0, +0), alive thinks this transform is wrong. Maybe always returning -0 is not a good encoding. Any thoughts?
define float @minnum_f32_p0_minnum_val_n0(float %x) {
%0:
%y = fminnum float %x, -0.000000
%z = fminnum float %y, 0.000000
ret float %z
}
=>
define float @minnum_f32_p0_minnum_val_n0(float %x) {
%0:
%1 = fminnum float %x, 0.000000
ret float %1
}
Transformation doesn't verify!
ERROR: Value mismatch
Example:
float %x = NaN
Source:
float %y = #x80000000 (-0.0)
float %z = #x80000000 (-0.0)
Target:
float %1 = #x00000000 (+0.0)
Source value: #x80000000 (-0.0)
Target value: #x00000000 (+0.0)
The transform is in llvm/llvm/test/Transforms/InstCombine/minnum.ll.
is this the only new test failure? what happens if you return nondeterministic choice of -0 and +0?
This is amazing, so returning -0.0 doesn't work. Would using nondeterministic choice work? Maybe you want to create a fresh variable and call addQuantVar .
@regehr @aqjune making returning value non-det makes llvm/llvm/test/Transforms/InstCombine/minnum.ll pass. I'll wrap up and run on whole test suite and see.
PR for minnum/maxnum support https://github.com/AliveToolkit/alive2/pull/352