bitwright/lib.rs
1//! Hash-consed fixed-width bit-vector expressions: exact evaluation, bit-level facts, and
2//! verified simplification.
3//!
4//! A guide with tested examples is in the repository's `book/`; the design reference is
5//! `docs/design.md`.
6//!
7//! - [`BitVec`]: exact values of 1..=512 bits with total, SMT-LIB QF_BV semantics for every
8//! operator ([`UnOp`], [`BinOp`], [`CmpOp`], casts, [`BitVec::select`]).
9//! - [`Context`]: a hash-consed expression arena with construction-time canonicalization,
10//! symbols, O(1) structural metadata, iterative traversal, evaluation and substitution, and a
11//! text syntax ([`Context::parse`], [`Context::display`]).
12//! - [`Facts`]: known bits, an unsigned strided interval and a signed range per node (a reduced
13//! product), computed lazily and iteratively under a work cap, and tri-state proofs
14//! ([`Context::prove`]), also under consumer-defined constraints ([`Assumptions`]: facts and
15//! 1-bit predicates, propagated to operands, with the constraints each result relies on
16//! reported as a [`Reliance`]).
17//! - [`rules`]: the `.bwr` rule language and its compiler; `check` (feature `check`, default):
18//! the soundness checker and proof ledgers.
19//! - [`engine`]: the simplifier: proven rules and normal-form passes (linear, xor, bitwise,
20//! comparisons, casts, demanded bits, equalities through invertible maps, and for
21//! deobfuscation divisions by constants, linear MBA and bit shuffles), applied bottom-up under
22//! caller-owned budgets, with a memo, telemetry and host hooks. [`Query::Injective`] and [`Query::Bijective`] ask
23//! whether an expression is an invertible function of one of its subexpressions.
24//! - [`ext`]: host-defined extension operations (multi-output, total), registered in a
25//! [`Registry`](ext::Registry) and built with [`Context::ext`].
26//! - [`translate`]: a host's IR into expressions and back (`Semantics`, `Lowering`, `Raise`,
27//! and `Template` for semantics given as text at run time); host rewrites in Rust are
28//! [`engine::Rewrite`].
29//! - `mba` (feature `mba`): the MBA service with an evidence gate and bitwright's own solvers;
30//! `eqsat` (feature `eqsat`): a bounded equality-saturation search; `smtlib` (feature
31//! `smtlib`): SMT-LIB export, import and rule obligations.
32//!
33//! ```
34//! use bitwright::{BinOp, BitVec, Width};
35//!
36//! let x = BitVec::from_u64(Width::W8, 200)?;
37//! let y = BitVec::from_u64(Width::W8, 100)?;
38//! assert_eq!(BitVec::apply_bin(BinOp::Add, &x, &y)?.to_u64(), Some(44)); // mod 2^8
39//! assert!(BitVec::apply_bin(BinOp::UDiv, &x, &BitVec::zero(Width::W8))?.is_ones()); // total
40//! # Ok::<(), Box<dyn std::error::Error>>(())
41//! ```
42//!
43//! ```
44//! use bitwright::{Context, ParseOptions, Width};
45//!
46//! let mut cx = Context::new();
47//! let a = cx.parse("y + x", &ParseOptions::width(Width::W32))?;
48//! let b = cx.parse("x + y", &ParseOptions::width(Width::W32))?;
49//! assert_eq!(a, b); // canonical operand order: one node
50//! // Construction canonicalizes and folds constants, but does not simplify further.
51//! let c = cx.parse("(x - (2 + 3)) + 5", &ParseOptions::width(Width::W32))?;
52//! assert_eq!(cx.display(c).to_string(), "x - 5 + 5");
53//! # Ok::<(), bitwright::Error>(())
54//! ```
55
56/// `with_*` setters for configuration structs, one per listed field:
57/// `setters!(Type { with_a: a: T, with_b: b ? U, })`, where `?` stores `Some(value)`. Every
58/// entry ends with a comma.
59macro_rules! setters {
60 ($t:ident $(<$lt:lifetime>)? { $($body:tt)* }) => {
61 impl$(<$lt>)? $t$(<$lt>)? {
62 setters!(@items $t; $($body)*);
63 }
64 };
65 (@items $t:ident; ) => {};
66 (@items $t:ident; $set:ident : $field:ident ? $fty:ty, $($rest:tt)*) => {
67 #[doc = concat!("Sets [`", stringify!($field), "`](", stringify!($t), "::", stringify!($field), ").")]
68 #[must_use]
69 pub fn $set(mut self, value: $fty) -> Self {
70 self.$field = Some(value);
71 self
72 }
73 setters!(@items $t; $($rest)*);
74 };
75 (@items $t:ident; $set:ident : $field:ident : $fty:ty, $($rest:tt)*) => {
76 #[doc = concat!("Sets [`", stringify!($field), "`](", stringify!($t), "::", stringify!($field), ").")]
77 #[must_use]
78 pub fn $set(mut self, value: $fty) -> Self {
79 self.$field = value;
80 self
81 }
82 setters!(@items $t; $($rest)*);
83 };
84}
85
86#[cfg(feature = "check")]
87pub mod check;
88pub mod engine;
89#[cfg(feature = "eqsat")]
90pub mod eqsat;
91mod error;
92mod expr;
93pub mod ext;
94mod facts;
95pub mod fp;
96mod hash;
97mod invert;
98pub mod lift;
99#[cfg(feature = "mba")]
100pub mod mba;
101pub mod memory;
102mod ops;
103#[cfg(feature = "prove")]
104pub mod prove;
105pub mod rules;
106#[cfg(feature = "smtlib")]
107pub mod smtlib;
108#[cfg(feature = "prove")]
109pub mod synth;
110#[cfg(test)]
111mod testutil;
112#[cfg(feature = "prove")]
113pub mod transform;
114
115/// The README's and the book's examples (`book/src`), compiled and run as doctests.
116#[cfg(doctest)]
117mod book {
118 #[doc = include_str!("../../README.md")]
119 struct Readme;
120 #[doc = include_str!("../../book/src/getting-started.md")]
121 struct GettingStarted;
122 #[doc = include_str!("../../book/src/semantics.md")]
123 struct Semantics;
124 #[doc = include_str!("../../book/src/floating-point.md")]
125 struct FloatingPoint;
126 #[doc = include_str!("../../book/src/facts.md")]
127 struct Facts;
128 #[doc = include_str!("../../book/src/constraints.md")]
129 struct Constraints;
130 #[doc = include_str!("../../book/src/extensions.md")]
131 struct Extensions;
132 #[doc = include_str!("../../book/src/memory.md")]
133 struct MemoryChapter;
134 #[cfg(feature = "mba")]
135 #[doc = include_str!("../../book/src/lifting.md")]
136 struct Lifting;
137 #[doc = include_str!("../../book/src/simplifying.md")]
138 struct Simplifying;
139 #[cfg(feature = "check")]
140 #[doc = include_str!("../../book/src/rules.md")]
141 struct Rules;
142 #[cfg(feature = "check")]
143 #[doc = include_str!("../../book/src/checking.md")]
144 struct Checking;
145 #[cfg(feature = "check")]
146 #[doc = include_str!("../../book/src/compilers.md")]
147 struct Compilers;
148 #[cfg(feature = "prove")]
149 #[doc = include_str!("../../book/src/transformations.md")]
150 struct Transformations;
151 #[cfg(feature = "mba")]
152 #[doc = include_str!("../../book/src/deobfuscation.md")]
153 struct Deobfuscation;
154 #[doc = include_str!("../../book/src/invertibility.md")]
155 struct Invertibility;
156 #[cfg(feature = "eqsat")]
157 #[doc = include_str!("../../book/src/eqsat.md")]
158 struct Eqsat;
159 #[cfg(feature = "smtlib")]
160 #[doc = include_str!("../../book/src/smtlib.md")]
161 struct Smtlib;
162 #[cfg(all(feature = "check", feature = "mba", feature = "smtlib"))]
163 #[doc = include_str!("../../book/src/examples.md")]
164 struct Examples;
165 #[doc = include_str!("../../book/src/stability.md")]
166 struct Stability;
167}
168pub mod text;
169pub mod translate;
170mod value;
171
172pub use error::{Error, ParseError, ValueError, WidthError};
173pub use expr::traps;
174pub use expr::{
175 ArenaCounters, Bounded, Context, ContextConfig, Env, Expr, ExprMap, ExprSet, FnEnv, Mark,
176 Substitution, SymbolId, SymbolKey, View,
177};
178pub use facts::{
179 Assumptions, ConstraintId, Facts, KnownBits, Proof, Query, Reliance, SRange, Truth, URange,
180};
181pub use fp::{FpFormat, RoundingMode};
182pub use ops::{BinOp, CmpOp, CmpOpExt, UnOp};
183pub use text::{ParseOptions, PrintOptions};
184pub use value::{BitVec, Width};