bitwright 0.16.0

Hash-consed fixed-width bit-vector expressions: exact evaluation, bit-level facts, and verified simplification.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58

//! 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));
//! # Ok::<(), bitwright::transform::SyntaxError>(())
//! ```
//!
//! 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.

mod alive;
pub(crate) mod encode;
mod infer;
pub mod ir;
mod lex;
pub(crate) mod llvm;
mod parse;
#[cfg(test)]
mod tests;
#[cfg(test)]
mod tests_semantics;
pub(crate) mod types;
mod value;
mod verify;

pub use alive::parse_transforms;
pub use infer::{Inference, infer};
pub use lex::SyntaxError;
pub use llvm::{FnText, Pair, function_pair, functions, pairs, pairs_each};
pub use types::Assignment;
pub use verify::{Config, Counterexample, Mismatch, Report, Shown, Verdict, validate, verify};
#[cfg(feature = "smtlib")]
pub use verify::{Question, smt};