Home

Welcome to the alive-nj wiki!

Alive-NJ-2.1 includes several encoding variants for Alive, which may be selected using the --encoding command-line option. When no encoding is specified, Alive-NJ uses smtundef.

Several options are described by the LLVM Language Reference as having “undefined results”. We normally interpret this as an arbitrary bit-pattern, similar to LLVM's undef constant, but a poison value is also a reasonable interpretation. Operations which return undefined results include:

• shifts, when the shift amount equals or exceeds the argument bit-width
• floating-point operations including a nnan (or ninf) attribute, where one of the arguments is NaN (or infinite)
• floating-point conversions, where the input value is outside the range of the target type

The encoding pldi2015 reflects the semantics of Alive described in the original paper from PLDI 2015. Since then, we have come to consider these semantics incorrect.

The encoding poisononly is our interpretation of the semantics proposed by Lee, et. al., in “Taming Undefined Behavior in LLVM” (PLDI 2017). This effectively replaces undef with poison and adds the freeze instruction.

Encoding	Undefined results	select poison, %x, %y	select True, %x, poison	Other
pldi2015	undef	poison	poison	Too-large shifts are undefined behavior. Division by poison is poison. Inputs are never poison.
smtundef	undef	poison	poison
cpselect	undef	poison	%x
nccpselect	undef	select undef, %x, %y	%x
ubselect	undef	Undefined behavior	poison
ubcpselect	undef	Undefined behavior	%x
smtpoison	poison	poison	poison
poisononly	poison	poison	%x	Support for freeze.