Module transform 

Verifying compiler transformations: that a target program refines a source program under LLVM’s semantics of poison, undefined behavior and floating point, for peephole transformations written in the transformation syntax the Alive paper introduced (Lopes et al., PLDI 2015), and for pairs of functions in a subset of LLVM IR (translation validation). Feature prove.

use bitwright::transform::{Config, Verdict, parse_transforms, verify};

let t = parse_transforms(
    "Name: add of a not
     %a = xor %x, -1
     %r = add %a, 1
       =>
     %r = sub 0, %x",
)?;
assert!(matches!(verify(&t[0], &Config::default()).verdict(), Verdict::Valid));

Each value is its bits and a poison flag; each program has an undefined-behavior condition; each nondeterministic choice (an undef use, a freeze of poison, a NaN’s sign and payload, a zero’s sign under nsz) is a leaf, chosen by the source existentially and by the target universally. Types left open are checked at each width (1 to 8, 16, 32, 64) and format (half, float, double) they may take, at most Config::max_types assignments (with more, the verdict is unknown). The rewrite-based fast-math flags (reassoc, arcp, contract, afn) are not modeled: a transformation that needs them is checked against exact IEEE semantics. What bitwright reads but does not model (pointers, an attribute or metadata of the target it does not know, a non-default floating-point environment) makes a transformation unsupported, never silently ignored.

A verdict rests on the encoding of LLVM’s semantics, the bit-blaster and, unless Config::certify asks for DRUP certificates, bitwright’s simplifier and SAT solver. smt (feature smtlib) writes the final questions for another solver to confirm.

Modules

ir

The form both front ends parse into: the values of a source and a target program in one arena, so the inputs and symbolic constants they share are the same nodes.

Structs

Assignment

One assignment of types to every node.

Config

How to verify.

Counterexample

Inputs where the target does something the source cannot.

FnText

A function definition’s text.

Inference

The outcome of inference.

Report

The checks of one transformation.

SyntaxError

An error at a line (1-based).

Enums

Mismatch

How the target fails to refine the source.

Shown

A value in a counterexample.

Verdict

The verdict at one type assignment, or overall.

Functions

function_pair

The transformation that tgt refines src: two functions of one signature, their parameters the shared inputs by position.

functions

The function definitions of a module.

infer

Infers a precondition over the symbolic constants of t (its own precondition, if any, is ignored) and verifies the transformation with it.

pairs

The function pairs to validate: @src and @tgt of one module; or, with a second module, each function of the first with the function of the same name in the second.

pairs_each

pairs, each pair read on its own: a pair outside the subset comes with its error, named, and the others are still read. The error is the module’s (a function without its closing brace, no @src and @tgt, no function in both files).

parse_transforms

Parses every transformation of a file in the transformation syntax.

smt

Each type assignment’s question as an SMT-LIB 2.6 script, for another solver to check what a verdict rests on: whether, at some input and with some choices of the target, the target does what none of the source’s executions found by the search does. For a valid transformation every script is unsatisfiable, which a solver confirms independently of bitwright’s SAT solver and simplifier (the encoding of LLVM’s semantics is bitwright’s); for an invalid one whose source makes no choices, the script of the failing assignment is satisfiable. One per type assignment, with its label (the transformation’s name and types): the script, or why there is none (the search did not decide, or the source makes choices and the counterexample is the verifier’s). The error is the transformation’s.

validate

Translation validation of two modules (see pairs_each): a report per function pair, one the subset cannot read reported unsupported with its error, so that the others are still checked. The error is the module’s.

verify

Verifies that the target of t refines its source, at each type assignment in turn (smallest first), stopping at the first counterexample.

Type Aliases

Pair

A function pair’s name and its transformation, or why it cannot be read.

Question

A type assignment’s label and its SMT-LIB question, or why it has none (see smt).