From 7ed4db2341922e412745e2a8b499c63d21fd144c Mon Sep 17 00:00:00 2001 From: mnemonikr <138624285+mnemonikr@users.noreply.github.com> Date: Mon, 15 Dec 2025 12:13:17 -0800 Subject: [PATCH] Added README.md to symbit crate --- Cargo.lock | 1 - crates/sym/Cargo.toml | 8 ++++-- crates/sym/README.md | 57 ++++++++++++++++++++++++++++++++++++++ crates/sym/src/aiger.rs | 27 ++++++++++++++++++ crates/sym/src/bit.rs | 14 ++++++++++ crates/sym/src/convert.rs | 26 ----------------- crates/sym/src/eval.rs | 12 ++++++-- crates/sym/src/lib.rs | 5 ++++ crates/sym/src/vec.rs | 4 +++ crates/sym/src/vec/ops.rs | 2 +- crates/sympcode/Cargo.toml | 2 +- 11 files changed, 125 insertions(+), 33 deletions(-) create mode 100644 crates/sym/README.md create mode 100644 crates/sym/src/aiger.rs diff --git a/Cargo.lock b/Cargo.lock index ec45c27..3f1623a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -835,7 +835,6 @@ name = "symbit" version = "0.1.0" dependencies = [ "aiger-circuit", - "pcode-ops", "thiserror", ] diff --git a/crates/sym/Cargo.toml b/crates/sym/Cargo.toml index 357680b..93e8bf7 100644 --- a/crates/sym/Cargo.toml +++ b/crates/sym/Cargo.toml @@ -13,5 +13,9 @@ rust-version.workspace = true [dependencies] thiserror.workspace = true -pcode-ops = { path = "../pcode-ops/" } -aiger-circuit = "1" +aiger-circuit = { version = "1", optional = true } + +[features] + +# Enables integration with aiger-circuit for generating AIGER formatted circuit +aiger = ["dep:aiger-circuit"] diff --git a/crates/sym/README.md b/crates/sym/README.md new file mode 100644 index 0000000..70b207f --- /dev/null +++ b/crates/sym/README.md @@ -0,0 +1,57 @@ +# Overview + +A symbolic bitvectors[^bitvec] library for use with theorem provers and other binary analysis tools. Supported operations include: + +* Bitwise arithmetic (`&`, `|`, `^`, `!`) +* Bit manipulation (`<<`, `>>`, extension, truncation) +* Bit segmentation (split, join) +* Integer arithmetic (`+`, `-`, `×`, `÷`) +* Integer comparison (`<`, `>`, `=`, `≠`, `≤`, `≥`) + +## Example + +```rust +# use symbit::{Evaluator, SymbolicBitVec}; +# fn f() -> Option<()> { +// Create 32-bit symbolic bitvecs. Each bit is an independent variable. +let x = SymbolicBitVec::with_size(32); +let y = SymbolicBitVec::with_size(32); + +// Compute the (symbolic) product of x and y. +let z = x.clone() * y.clone(); + +// Create an evaluator assuming both x and y are negative. +// This means their most-significant bits (msb) are 1 (true). +let x_msb = x.msb()?.maybe_variable()?; +let y_msb = y.msb()?.maybe_variable()?; +let eval = Evaluator::new([(x_msb, true), (y_msb, true)]); + +// If x and y are negative then z should be positive (msb = 0) +let e = eval.evaluate(z.msb()?); +assert_eq!(e.response, Some(false)); + +// Only the msb from x and y were used in this determination +assert_eq!(e.used_variables.len(), 2); + +// The least significant bit (lsb) of the product is a variable. +let e = eval.evaluate(z.lsb()?); +assert!(e.response.is_none()); + +// The product lsb is dependent only on the lsb of x and y. +let x_lsb = x.lsb()?.maybe_variable()?; +let y_lsb = x.lsb()?.maybe_variable()?; +assert_eq!(e.unassigned_variables.len(), 2); +assert!(e.unassigned_variables.contains(&x_lsb)); +assert!(e.unassigned_variables.contains(&y_lsb)); +# Some(()) +# } +``` + + +# Features + +## `aiger` + +AIGER is a standardized format for an and-inverter gate circuit. The `aiger` feature can be used to enable integration with the [aiger-circuit](https://crates.io/crates/aiger-circuit) crate for converting constraints on outputs into an AIGER formatted circuit. + +[^bitvec]: A bitvector is a fixed sized number of bits that models the semantics of signed and unsigned two's complement arithmetic. diff --git a/crates/sym/src/aiger.rs b/crates/sym/src/aiger.rs new file mode 100644 index 0000000..0c00fd0 --- /dev/null +++ b/crates/sym/src/aiger.rs @@ -0,0 +1,27 @@ +use std::rc::Rc; + +use aiger_circuit::circuit::{AigerCircuit, AndOperand, AsAigerCircuit}; + +use crate::bit::SymbolicBit; + +impl<'a> AsAigerCircuit<'a> for SymbolicBit { + type Inner = Self; + + fn as_aiger_circuit(&'a self) -> AigerCircuit<'a, Self::Inner> { + match self { + SymbolicBit::Literal(value) => AigerCircuit::Literal(*value), + SymbolicBit::Variable(id) => AigerCircuit::Variable(*id), + SymbolicBit::Not(x) => AigerCircuit::Not(x.as_ref()), + SymbolicBit::And(x, y) => AigerCircuit::And( + AndOperand { + id: Rc::as_ptr(x) as usize, + value: x.as_ref(), + }, + AndOperand { + id: Rc::as_ptr(y) as usize, + value: y.as_ref(), + }, + ), + } + } +} diff --git a/crates/sym/src/bit.rs b/crates/sym/src/bit.rs index 6e79b63..e568228 100644 --- a/crates/sym/src/bit.rs +++ b/crates/sym/src/bit.rs @@ -23,6 +23,20 @@ pub enum SymbolicBit { } impl SymbolicBit { + pub fn maybe_literal(&self) -> Option { + match self { + Self::Literal(b) => Some(*b), + _ => None, + } + } + + pub fn maybe_variable(&self) -> Option { + match self { + Self::Variable(id) => Some(*id), + _ => None, + } + } + pub fn equals(self, rhs: Self) -> Self { (self.clone() & rhs.clone()) | (!self & !rhs) } diff --git a/crates/sym/src/convert.rs b/crates/sym/src/convert.rs index 38f9656..dbcb02f 100644 --- a/crates/sym/src/convert.rs +++ b/crates/sym/src/convert.rs @@ -1,7 +1,3 @@ -use std::rc::Rc; - -use aiger_circuit::circuit::{AigerCircuit, AndOperand, AsAigerCircuit}; - use crate::bit::{FALSE, SymbolicBit}; use crate::buf::{SymbolicBitBuf, SymbolicByte}; use crate::vec::SymbolicBitVec; @@ -348,25 +344,3 @@ impl_little_endian!(u64); impl_little_endian!(u32); impl_little_endian!(u16); impl_little_endian!(u8); - -impl<'a> AsAigerCircuit<'a> for SymbolicBit { - type Inner = Self; - - fn as_aiger_circuit(&'a self) -> AigerCircuit<'a, Self::Inner> { - match self { - SymbolicBit::Literal(value) => AigerCircuit::Literal(*value), - SymbolicBit::Variable(id) => AigerCircuit::Variable(*id), - SymbolicBit::Not(x) => AigerCircuit::Not(x.as_ref()), - SymbolicBit::And(x, y) => AigerCircuit::And( - AndOperand { - id: Rc::as_ptr(x) as usize, - value: x.as_ref(), - }, - AndOperand { - id: Rc::as_ptr(y) as usize, - value: y.as_ref(), - }, - ), - } - } -} diff --git a/crates/sym/src/eval.rs b/crates/sym/src/eval.rs index f70f47d..9cf23b3 100644 --- a/crates/sym/src/eval.rs +++ b/crates/sym/src/eval.rs @@ -25,8 +25,10 @@ pub struct Evaluation { impl Evaluator { /// Create a new instance using the given [VariableAssignments]. The assignments are fixed for /// the lifetime of this evaluator. - pub fn new(assignments: VariableAssignments) -> Self { - Self { assignments } + pub fn new(assignments: impl Into) -> Self { + Self { + assignments: assignments.into(), + } } pub fn evaluate(&self, bit: &SymbolicBit) -> Evaluation { @@ -129,6 +131,12 @@ impl VariableAssignments { } } +impl> From for VariableAssignments { + fn from(iter: I) -> Self { + iter.into_iter().collect() + } +} + impl FromIterator<(usize, bool)> for VariableAssignments { fn from_iter>(iter: T) -> Self { Self { diff --git a/crates/sym/src/lib.rs b/crates/sym/src/lib.rs index fb51695..e406d45 100644 --- a/crates/sym/src/lib.rs +++ b/crates/sym/src/lib.rs @@ -1,3 +1,5 @@ +#![doc=include_str!("../README.md")] + mod bit; mod buf; mod convert; @@ -13,5 +15,8 @@ pub use crate::convert::concretize_into; pub use crate::eval::*; pub use crate::vec::*; +#[cfg(feature = "aiger")] +mod aiger; + #[cfg(test)] mod tests; diff --git a/crates/sym/src/vec.rs b/crates/sym/src/vec.rs index 6312ace..7b4f56c 100644 --- a/crates/sym/src/vec.rs +++ b/crates/sym/src/vec.rs @@ -23,6 +23,10 @@ impl SymbolicBitVec { self.bits.back() } + pub fn lsb(&self) -> Option<&SymbolicBit> { + self.bits.front() + } + pub fn is_empty(&self) -> bool { self.bits.is_empty() } diff --git a/crates/sym/src/vec/ops.rs b/crates/sym/src/vec/ops.rs index 92aec60..7a6e162 100644 --- a/crates/sym/src/vec/ops.rs +++ b/crates/sym/src/vec/ops.rs @@ -171,7 +171,7 @@ impl std::ops::Mul for SymbolicBitVec { fn mul(self, rhs: Self) -> Self::Output { // The output size is the sum of the number of bits. Clippy is overly zealous here flagging - // the addition as erroneous. + // the addition as erroneous. https://github.com/rust-lang/rust-clippy/issues/16247 #[allow(clippy::suspicious_arithmetic_impl)] let output_size = self.len() + rhs.len(); diff --git a/crates/sympcode/Cargo.toml b/crates/sympcode/Cargo.toml index 193e366..fe3a076 100644 --- a/crates/sympcode/Cargo.toml +++ b/crates/sympcode/Cargo.toml @@ -8,5 +8,5 @@ repository.workspace = true rust-version.workspace = true [dependencies] -symbit = { version = "0.1", path = "../sym" } +symbit = { version = "0.1", path = "../sym", features = ["aiger"] } pcode-ops = { version = "0.1", path = "../pcode-ops/" }