bitwright 0.11.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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177

//! Hash-consed fixed-width bit-vector expressions: exact evaluation, bit-level facts, and
//! verified simplification.
//!
//! A guide with tested examples is in the repository's `book/`; the design reference is
//! `docs/design.md`.
//!
//! - [`BitVec`]: exact values of 1..=512 bits with total, SMT-LIB QF_BV semantics for every
//!   operator ([`UnOp`], [`BinOp`], [`CmpOp`], casts, [`BitVec::select`]).
//! - [`Context`]: a hash-consed expression arena with construction-time canonicalization,
//!   symbols, O(1) structural metadata, iterative traversal, evaluation and substitution, and a
//!   text syntax ([`Context::parse`], [`Context::display`]).
//! - [`Facts`]: known bits, an unsigned strided interval and a signed range per node (a reduced
//!   product), computed lazily and iteratively under a work cap, and tri-state proofs
//!   ([`Context::prove`]), also under consumer-defined constraints ([`Assumptions`]: facts and
//!   1-bit predicates, propagated to operands, with the constraints each result relies on
//!   reported as a [`Reliance`]).
//! - [`rules`]: the `.bwr` rule language and its compiler; `check` (feature `check`, default):
//!   the soundness checker and proof ledgers.
//! - [`engine`]: the simplifier: proven rules and normal-form passes (linear, xor, bitwise,
//!   comparisons, casts, demanded bits, equalities through invertible maps, and for
//!   deobfuscation linear MBA and bit shuffles), applied bottom-up under caller-owned budgets,
//!   with a memo, telemetry and host hooks. [`Query::Injective`] and [`Query::Bijective`] ask
//!   whether an expression is an invertible function of one of its subexpressions.
//! - [`ext`]: host-defined extension operations (multi-output, total), registered in a
//!   [`Registry`](ext::Registry) and built with [`Context::ext`].
//! - `mba` (feature `mba`): the MBA service with an evidence gate and bitwright's own solvers;
//!   `eqsat` (feature `eqsat`): a bounded equality-saturation search; `smtlib` (feature
//!   `smtlib`): SMT-LIB export, import and rule obligations.
//!
//! ```
//! use bitwright::{BinOp, BitVec, Width};
//!
//! let x = BitVec::from_u64(Width::W8, 200)?;
//! let y = BitVec::from_u64(Width::W8, 100)?;
//! assert_eq!(BitVec::apply_bin(BinOp::Add, &x, &y)?.to_u64(), Some(44)); // mod 2^8
//! assert!(BitVec::apply_bin(BinOp::UDiv, &x, &BitVec::zero(Width::W8))?.is_ones()); // total
//! # Ok::<(), Box<dyn std::error::Error>>(())
//! ```
//!
//! ```
//! use bitwright::{Context, ParseOptions, Width};
//!
//! let mut cx = Context::new();
//! let a = cx.parse("y + x", &ParseOptions::width(Width::W32))?;
//! let b = cx.parse("x + y", &ParseOptions::width(Width::W32))?;
//! assert_eq!(a, b); // canonical operand order: one node
//! // Construction canonicalizes and folds constants, but does not simplify further.
//! let c = cx.parse("(x - (2 + 3)) + 5", &ParseOptions::width(Width::W32))?;
//! assert_eq!(cx.display(c).to_string(), "x - 5 + 5");
//! # Ok::<(), bitwright::Error>(())
//! ```

/// `with_*` setters for configuration structs, one per listed field:
/// `setters!(Type { with_a: a: T, with_b: b ? U, })`, where `?` stores `Some(value)`. Every
/// entry ends with a comma.
macro_rules! setters {
    ($t:ident $(<$lt:lifetime>)? { $($body:tt)* }) => {
        impl$(<$lt>)? $t$(<$lt>)? {
            setters!(@items $t; $($body)*);
        }
    };
    (@items $t:ident; ) => {};
    (@items $t:ident; $set:ident : $field:ident ? $fty:ty, $($rest:tt)*) => {
        #[doc = concat!("Sets [`", stringify!($field), "`](", stringify!($t), "::", stringify!($field), ").")]
        #[must_use]
        pub fn $set(mut self, value: $fty) -> Self {
            self.$field = Some(value);
            self
        }
        setters!(@items $t; $($rest)*);
    };
    (@items $t:ident; $set:ident : $field:ident : $fty:ty, $($rest:tt)*) => {
        #[doc = concat!("Sets [`", stringify!($field), "`](", stringify!($t), "::", stringify!($field), ").")]
        #[must_use]
        pub fn $set(mut self, value: $fty) -> Self {
            self.$field = value;
            self
        }
        setters!(@items $t; $($rest)*);
    };
}

#[cfg(feature = "check")]
pub mod check;
pub mod engine;
#[cfg(feature = "eqsat")]
pub mod eqsat;
mod error;
mod expr;
pub mod ext;
mod facts;
pub mod fp;
mod hash;
mod invert;
pub mod lift;
#[cfg(feature = "mba")]
pub mod mba;
pub mod memory;
mod ops;
#[cfg(feature = "prove")]
pub mod prove;
pub mod rules;
#[cfg(feature = "smtlib")]
pub mod smtlib;
#[cfg(feature = "prove")]
pub mod synth;
#[cfg(test)]
mod testutil;
#[cfg(feature = "prove")]
pub mod transform;

/// The README's and the book's examples (`book/src`), compiled and run as doctests.
#[cfg(doctest)]
mod book {
    #[doc = include_str!("../../README.md")]
    struct Readme;
    #[doc = include_str!("../../book/src/getting-started.md")]
    struct GettingStarted;
    #[doc = include_str!("../../book/src/semantics.md")]
    struct Semantics;
    #[doc = include_str!("../../book/src/floating-point.md")]
    struct FloatingPoint;
    #[doc = include_str!("../../book/src/facts.md")]
    struct Facts;
    #[doc = include_str!("../../book/src/constraints.md")]
    struct Constraints;
    #[doc = include_str!("../../book/src/extensions.md")]
    struct Extensions;
    #[doc = include_str!("../../book/src/memory.md")]
    struct MemoryChapter;
    #[cfg(feature = "mba")]
    #[doc = include_str!("../../book/src/lifting.md")]
    struct Lifting;
    #[doc = include_str!("../../book/src/simplifying.md")]
    struct Simplifying;
    #[cfg(feature = "check")]
    #[doc = include_str!("../../book/src/rules.md")]
    struct Rules;
    #[cfg(feature = "check")]
    #[doc = include_str!("../../book/src/checking.md")]
    struct Checking;
    #[cfg(feature = "prove")]
    #[doc = include_str!("../../book/src/transformations.md")]
    struct Transformations;
    #[cfg(feature = "mba")]
    #[doc = include_str!("../../book/src/deobfuscation.md")]
    struct Deobfuscation;
    #[doc = include_str!("../../book/src/invertibility.md")]
    struct Invertibility;
    #[cfg(feature = "eqsat")]
    #[doc = include_str!("../../book/src/eqsat.md")]
    struct Eqsat;
    #[cfg(feature = "smtlib")]
    #[doc = include_str!("../../book/src/smtlib.md")]
    struct Smtlib;
    #[cfg(all(feature = "check", feature = "mba", feature = "smtlib"))]
    #[doc = include_str!("../../book/src/examples.md")]
    struct Examples;
    #[doc = include_str!("../../book/src/stability.md")]
    struct Stability;
}
pub mod text;
mod value;

pub use error::{Error, ParseError, ValueError, WidthError};
pub use expr::traps;
pub use expr::{
    ArenaCounters, Bounded, Context, ContextConfig, Env, Expr, ExprMap, ExprSet, FnEnv, Mark,
    Substitution, SymbolId, SymbolKey, View,
};
pub use facts::{
    Assumptions, ConstraintId, Facts, KnownBits, Proof, Query, Reliance, SRange, Truth, URange,
};
pub use fp::{FpFormat, RoundingMode};
pub use ops::{BinOp, CmpOp, CmpOpExt, UnOp};
pub use text::{ParseOptions, PrintOptions};
pub use value::{BitVec, Width};