Alive-NJ is a reimplementation of the Automated LLVM's InstCombine Verifier, written by Nuno Lopes, David Menendez, Santosh Nagarakatte, and John Regehr and detailed in the paper "Provably Correct Peephole Optimizations with Alive", presented at PLDI 2015.
Alive-NJ is intended to facilitate experimentation with Alive semantics and extension of Alive into new areas.
Alive requires Python 2.7 and Z3 4.3.2 or later.
Z3 can be obtained from https://github.com/Z3Prover/z3
./run.py [file [file...]]
./run.py --help
Alive-NJ reads from standard input if no arguments are given.
Alive-NJ adds these features:
- Support for floating-point
half
,float
,double
,fp128
, andx86_fp80
types- Instructions:
fadd
,fsub
,fmul
,fdiv
,frem
,fcmp
,fptosi
,fptoui
,sitofp
,uitofp
,fpext
,fptrunc
- Symbolic constants, integer literals, and expressions using
+
,-
,*
,/
, and%
may be integer or floating point - Floating-point literals
- Special values
nan
,inf
,-inf
, and-0.0
- Precondition comparisons use IEEE semantics for floats (thus,
C == 0.0
is satisfied whenC
is positive or negative zero, andC == nan
is never satisfied) - Predicate
fpsame(C1,C2)
is satisfied whenC1
andC2
are structurally equal (meaningfpsame(nan,nan)
is true, butfpsame(0.0, -0.0)
is not)
- Full replaceability of
undef
: If%x
isundef
, thenxor %x, %x
isundef
- New constant symbols may be defined in the target, for example,
C2 = trunc(C1)
. These symbols are in scope in the precondition and target, sozext(C2) == C1
is a valid precondition. Note that, unliketrunc(C1)
, all uses ofC2
will have the same type.
We have found the following bugs with the floating point support in Alive-NJ:
- https://llvm.org/bugs/show_bug.cgi?id=26863
- https://llvm.org/bugs/show_bug.cgi?id=27151
- https://llvm.org/bugs/show_bug.cgi?id=27153
- https://llvm.org/bugs/show_bug.cgi?id=26862
- https://llvm.org/bugs/show_bug.cgi?id=26746
Alive-NJ does not include, or does not fully implement, these features:
- C++ code generation
- Flag inference
- Memory operations (
alloca
,store
,load
,getelementpointer
) - Pointer types
- Composition of optimizations and non-termination checking