From 33beb417bc1bd0b0278129f45d3cfaee9507c3b7 Mon Sep 17 00:00:00 2001 From: mnemonikr <138624285+mnemonikr@users.noreply.github.com> Date: Mon, 15 Dec 2025 15:10:02 -0800 Subject: [PATCH] Move symbit crate to its own repository --- Cargo.lock | 4 +- crates/sym/Cargo.toml | 21 -- crates/sym/README.md | 57 ---- crates/sym/src/aiger.rs | 27 -- crates/sym/src/bit.rs | 152 --------- crates/sym/src/buf.rs | 396 ---------------------- crates/sym/src/convert.rs | 346 ------------------- crates/sym/src/eval.rs | 146 -------- crates/sym/src/lib.rs | 22 -- crates/sym/src/tests.rs | 5 - crates/sym/src/tests/bit.rs | 90 ----- crates/sym/src/tests/bitbuf.rs | 51 --- crates/sym/src/tests/bitvec.rs | 535 ----------------------------- crates/sym/src/tests/convert.rs | 157 --------- crates/sym/src/tests/eval.rs | 194 ----------- crates/sym/src/vec.rs | 572 -------------------------------- crates/sym/src/vec/convert.rs | 35 -- crates/sym/src/vec/ops.rs | 180 ---------- crates/sympcode/Cargo.toml | 2 +- 19 files changed, 4 insertions(+), 2988 deletions(-) delete mode 100644 crates/sym/Cargo.toml delete mode 100644 crates/sym/README.md delete mode 100644 crates/sym/src/aiger.rs delete mode 100644 crates/sym/src/bit.rs delete mode 100644 crates/sym/src/buf.rs delete mode 100644 crates/sym/src/convert.rs delete mode 100644 crates/sym/src/eval.rs delete mode 100644 crates/sym/src/lib.rs delete mode 100644 crates/sym/src/tests.rs delete mode 100644 crates/sym/src/tests/bit.rs delete mode 100644 crates/sym/src/tests/bitbuf.rs delete mode 100644 crates/sym/src/tests/bitvec.rs delete mode 100644 crates/sym/src/tests/convert.rs delete mode 100644 crates/sym/src/tests/eval.rs delete mode 100644 crates/sym/src/vec.rs delete mode 100644 crates/sym/src/vec/convert.rs delete mode 100644 crates/sym/src/vec/ops.rs diff --git a/Cargo.lock b/Cargo.lock index 3f1623a..5206ef6 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -832,7 +832,9 @@ checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" [[package]] name = "symbit" -version = "0.1.0" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "76682cead7c03b796d41b40df11b06aead4ef695d9313702f329094595204dea" dependencies = [ "aiger-circuit", "thiserror", diff --git a/crates/sym/Cargo.toml b/crates/sym/Cargo.toml deleted file mode 100644 index 93e8bf7..0000000 --- a/crates/sym/Cargo.toml +++ /dev/null @@ -1,21 +0,0 @@ -[package] -name = "symbit" -description = "Symbolic representation of binary data" -version = "0.1.0" - -authors.workspace = true -edition.workspace = true -license.workspace = true -repository.workspace = true -rust-version.workspace = true - -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html - -[dependencies] -thiserror.workspace = true -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 deleted file mode 100644 index 70b207f..0000000 --- a/crates/sym/README.md +++ /dev/null @@ -1,57 +0,0 @@ -# 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 deleted file mode 100644 index 0c00fd0..0000000 --- a/crates/sym/src/aiger.rs +++ /dev/null @@ -1,27 +0,0 @@ -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 deleted file mode 100644 index e568228..0000000 --- a/crates/sym/src/bit.rs +++ /dev/null @@ -1,152 +0,0 @@ -use std::rc::Rc; - -pub const FALSE: SymbolicBit = SymbolicBit::Literal(false); -pub const TRUE: SymbolicBit = SymbolicBit::Literal(true); - -/// A value that can be used to represent a variable bit, possibly with constraints on its value. -#[derive(Debug, Clone, PartialEq, Eq)] -pub enum SymbolicBit { - /// A literal `true` or `false` value. - Literal(bool), - - /// A variable value. The parameter is the identifier for this variable. Two variables with the - /// same identifier are equivalent. - Variable(usize), - - /// The negation of a symbolic bit. The `!` operator should be preferred to this, as it has the - /// opportunity to perform simplications where a direct construction does not. - Not(Rc), - - /// The conjunction of two symbolic bits. The `&` operator should be preferred to this, as it - /// has the opportunity to perform simpliciations where a direct construction does not. - And(Rc, Rc), -} - -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) - } - - pub fn select(self, lhs: Self, rhs: Self) -> Self { - (self.clone() & lhs) | (!self & rhs) - } - - pub fn is_identical(&self, rhs: &Self) -> bool { - match self { - Self::Literal(x) => { - if let Self::Literal(y) = rhs { - return *x == *y; - } - } - Self::Variable(x) => { - if let Self::Variable(y) = rhs { - return *x == *y; - } - } - Self::Not(x) => { - if let Self::Not(y) = rhs { - if Rc::ptr_eq(x, y) { - return true; - } else if let Self::Variable(x) = **x - && let Self::Variable(y) = **y - { - // Check if same variable - return x == y; - } - } - } - Self::And(x, y) => { - if let Self::And(u, v) = rhs { - if Rc::ptr_eq(x, u) && Rc::ptr_eq(y, v) || Rc::ptr_eq(x, v) && Rc::ptr_eq(y, u) - { - return true; - } else if let Self::Variable(x) = **x - && let Self::Variable(y) = **y - && let Self::Variable(u) = **u - && let Self::Variable(v) = **v - { - // Check if same variables - return x == u && y == v || x == v && y == u; - } - } - } - } - - false - } -} - -impl Default for SymbolicBit { - fn default() -> Self { - FALSE - } -} - -impl std::ops::Not for SymbolicBit { - type Output = Self; - - fn not(self) -> Self::Output { - match self { - SymbolicBit::Literal(false) => SymbolicBit::Literal(true), - SymbolicBit::Literal(true) => SymbolicBit::Literal(false), - SymbolicBit::Not(y) => Rc::unwrap_or_clone(y), - _ => SymbolicBit::Not(Rc::new(self)), - } - } -} - -impl std::ops::BitAnd for SymbolicBit { - type Output = Self; - - fn bitand(self, rhs: Self) -> Self::Output { - if self.is_identical(&rhs) { - return self; - } - - match self { - SymbolicBit::Literal(false) => return SymbolicBit::Literal(false), - SymbolicBit::Literal(true) => return rhs, - SymbolicBit::Not(z) if z.is_identical(&rhs) => return SymbolicBit::Literal(false), - _ => (), - } - - match rhs { - SymbolicBit::Literal(false) => return SymbolicBit::Literal(false), - SymbolicBit::Literal(true) => return self, - SymbolicBit::Not(z) if z.is_identical(&self) => return SymbolicBit::Literal(false), - _ => (), - } - - SymbolicBit::And(Rc::new(self), Rc::new(rhs)) - } -} - -impl std::ops::BitOr for SymbolicBit { - type Output = Self; - - fn bitor(self, rhs: Self) -> Self::Output { - !(!self & !rhs) - } -} - -impl std::ops::BitXor for SymbolicBit { - type Output = Self; - - fn bitxor(self, rhs: Self) -> Self::Output { - (self.clone() & !rhs.clone()) | (!self & rhs) - } -} diff --git a/crates/sym/src/buf.rs b/crates/sym/src/buf.rs deleted file mode 100644 index 61bc074..0000000 --- a/crates/sym/src/buf.rs +++ /dev/null @@ -1,396 +0,0 @@ -//! Module for a collection of symbolic bits whose count are known at compile-time. -use std::mem::MaybeUninit; -use std::ops::Deref; - -use crate::bit::{FALSE, SymbolicBit}; - -/// An array of symbolic bits. -#[derive(PartialEq, Eq, Debug, Clone)] -pub struct SymbolicBitBuf { - bits: [SymbolicBit; N], -} - -impl IntoIterator for SymbolicBitBuf { - type Item = SymbolicBit; - type IntoIter = std::array::IntoIter; - - fn into_iter(self) -> Self::IntoIter { - self.bits.into_iter() - } -} - -/// An 8-bit byte of symbolic bits. -pub type SymbolicByte = SymbolicBitBuf<8>; - -impl std::ops::Deref for SymbolicBitBuf { - type Target = [SymbolicBit]; - - fn deref(&self) -> &Self::Target { - &self.bits - } -} - -impl AsRef for SymbolicBitBuf -where - T: ?Sized, - as std::ops::Deref>::Target: AsRef, -{ - fn as_ref(&self) -> &T { - self.deref().as_ref() - } -} - -impl From for SymbolicBitBuf { - fn from(bit: SymbolicBit) -> Self { - let mut result = Self::default(); - result[0] = bit; - result - } -} - -impl From<[SymbolicBit; N]> for SymbolicBitBuf { - fn from(bits: [SymbolicBit; N]) -> Self { - Self { bits } - } -} - -impl From> for [SymbolicBit; N] { - fn from(buf: SymbolicBitBuf) -> Self { - buf.bits - } -} - -impl Default for SymbolicBitBuf { - fn default() -> Self { - Self { bits: [FALSE; N] } - } -} - -impl std::ops::Index for SymbolicBitBuf { - type Output = SymbolicBit; - fn index(&self, index: usize) -> &Self::Output { - &self.bits[index] - } -} - -impl std::ops::IndexMut for SymbolicBitBuf { - fn index_mut(&mut self, index: usize) -> &mut Self::Output { - &mut self.bits[index] - } -} - -impl From> for Vec { - fn from(mut value: SymbolicBitBuf) -> Self { - const { - assert!(N.is_multiple_of(8)); - } - - let mut result = Vec::with_capacity(N / 8); - let (buf_bytes, _) = value.bits.as_chunks_mut::<8>(); - for buf_byte in buf_bytes { - let mut byte = [FALSE; 8]; - std::mem::swap(&mut byte, buf_byte); - result.push(SymbolicByte::from(byte)); - } - - result - } -} - -impl TryFrom> for SymbolicBitBuf { - type Error = String; - - fn try_from(value: Vec) -> Result { - if N == 8 * value.len() { - let initializer = |uninit_bits: &mut [MaybeUninit]| { - value - .into_iter() - .flat_map(|byte| byte.into_inner().into_iter()) - .enumerate() - .for_each(|(i, bit)| { - uninit_bits[i].write(bit); - }) - }; - - // SAFETY: All bits are initialized - unsafe { Ok(SymbolicBitBuf::::initialize(initializer)) } - } else { - Err(format!( - "value has {num_bits} bits, expected {N} bits", - num_bits = 8 * value.len(), - )) - } - } -} - -impl TryFrom> for SymbolicBitBuf { - type Error = String; - - fn try_from(value: Vec<&SymbolicByte>) -> Result { - if N == 8 * value.len() { - let initializer = |uninit_bits: &mut [MaybeUninit]| { - value - .into_iter() - .flat_map(|byte| byte.inner().iter()) - .cloned() - .enumerate() - .for_each(|(i, bit)| { - uninit_bits[i].write(bit); - }) - }; - - // SAFETY: All bits are initialized - unsafe { Ok(SymbolicBitBuf::::initialize(initializer)) } - } else { - Err(format!( - "value has {num_bits} bits, expected {N} bits", - num_bits = 8 * value.len(), - )) - } - } -} - -enum ShiftDirection { - Left, - Right, -} - -impl SymbolicBitBuf { - /// Create a new `SymbolicBitBuf` with the bits initialized by the callback. - /// - /// # Safety - /// - /// All of the bits must be initialized by the initializer callback. - #[inline] - unsafe fn initialize(initializer: F) -> Self - where - F: FnOnce(&mut [MaybeUninit]), - { - let mut bits: [std::mem::MaybeUninit; N] = - unsafe { std::mem::MaybeUninit::uninit().assume_init() }; - - initializer(&mut bits); - - // SAFETY: Assumes all bits are initialized - let bits = unsafe { (&bits as *const _ as *const [SymbolicBit; N]).read() }; - - Self { bits } - } - - #[must_use] - pub fn into_inner(self) -> [SymbolicBit; N] { - self.bits - } - - #[must_use] - pub fn inner(&self) -> &[SymbolicBit; N] { - &self.bits - } - - #[must_use] - pub fn equals(self, rhs: Self) -> SymbolicBit { - self.bits - .into_iter() - .zip(rhs.bits) - .map(|(lhs, rhs)| lhs.equals(rhs)) - .fold(SymbolicBit::Literal(true), |lhs, rhs| lhs & rhs) - } - - /// Concatenates this buffer with another, resulting in a single buffer containing `[self:rhs]`. - /// - /// # Future - /// - /// Once [generic_const_exprs](https://github.com/rust-lang/rust/issues/76560) is stabilized, - /// the value of `O` can be computed from `N` and `M` and will no longer be part of the type - /// signature. - #[must_use] - pub fn concat( - self, - rhs: SymbolicBitBuf, - ) -> SymbolicBitBuf { - const { - assert!(N + M == O, "output size must be sum of buffer sizes"); - } - - let initializer = |uninit_bits: &mut [MaybeUninit]| { - self.bits - .into_iter() - .chain(rhs.bits) - .enumerate() - .for_each(|(i, bit)| { - uninit_bits[i].write(bit); - }) - }; - - // SAFETY: All bits are initialized - unsafe { SymbolicBitBuf::::initialize(initializer) } - } - - fn shift(&mut self, amount: usize, shift_in: SymbolicBit, direction: ShiftDirection) { - match direction { - ShiftDirection::Left => { - // [ 0 1 2 3 4 5 6 7 ] << 3 - // [ x x x 0 1 2 3 4 ] - for i in (amount..N).rev() { - self.bits.swap(i, i - amount); - } - for i in 0..usize::min(N, amount) { - self.bits[i] = shift_in.clone(); - } - } - ShiftDirection::Right => { - // [ 0 1 2 3 4 5 6 7 ] >> 3 - // [ 3 4 5 6 7 x x x ] - for i in amount..N { - self.bits.swap(i, i - amount); - } - for i in 0..usize::min(N, amount) { - self.bits[N - 1 - i] = shift_in.clone(); - } - } - } - } - - fn mux(&mut self, rhs: Self, selector: SymbolicBit) { - rhs.bits.into_iter().enumerate().for_each(|(i, rhs)| { - let lhs = std::mem::take(&mut self.bits[i]); - self.bits[i] = selector.clone().select(lhs, rhs); - }); - } -} - -impl std::ops::Not for SymbolicBitBuf { - type Output = Self; - - fn not(mut self) -> Self::Output { - for i in 0..N { - let bit = std::mem::take(&mut self.bits[i]); - self.bits[i] = !bit; - } - - self - } -} - -impl std::ops::BitAndAssign for SymbolicBitBuf { - fn bitand_assign(&mut self, rhs: Self) { - rhs.bits.into_iter().enumerate().for_each(|(i, rhs)| { - let lhs = std::mem::take(&mut self.bits[i]); - self.bits[i] = lhs & rhs; - }); - } -} - -impl std::ops::BitOrAssign for SymbolicBitBuf { - fn bitor_assign(&mut self, rhs: Self) { - rhs.bits.into_iter().enumerate().for_each(|(i, rhs)| { - let lhs = std::mem::take(&mut self.bits[i]); - self.bits[i] = lhs | rhs; - }); - } -} - -impl std::ops::BitXorAssign for SymbolicBitBuf { - fn bitxor_assign(&mut self, rhs: Self) { - rhs.bits.into_iter().enumerate().for_each(|(i, rhs)| { - let lhs = std::mem::take(&mut self.bits[i]); - self.bits[i] = lhs ^ rhs; - }); - } -} - -impl std::ops::BitAnd for SymbolicBitBuf { - type Output = Self; - - fn bitand(mut self, rhs: Self) -> Self::Output { - self &= rhs; - self - } -} - -impl std::ops::BitOr for SymbolicBitBuf { - type Output = Self; - - fn bitor(mut self, rhs: Self) -> Self::Output { - self |= rhs; - self - } -} - -impl std::ops::BitXor for SymbolicBitBuf { - type Output = Self; - - fn bitxor(mut self, rhs: Self) -> Self::Output { - self ^= rhs; - self - } -} - -impl std::ops::ShlAssign for SymbolicBitBuf { - fn shl_assign(&mut self, rhs: Self) { - for (i, shift_bit) in rhs.bits.into_iter().enumerate() { - let mut shifted_value = self.clone(); - shifted_value.shift(1 << i, FALSE, ShiftDirection::Left); - self.mux(shifted_value, !shift_bit); - } - } -} - -impl std::ops::Shl for SymbolicBitBuf { - type Output = Self; - - fn shl(mut self, rhs: Self) -> Self::Output { - self <<= rhs; - self - } -} - -impl std::ops::ShlAssign for SymbolicBitBuf { - fn shl_assign(&mut self, rhs: usize) { - self.shift(rhs, FALSE, ShiftDirection::Left); - } -} - -impl std::ops::Shl for SymbolicBitBuf { - type Output = Self; - - fn shl(mut self, rhs: usize) -> Self::Output { - self <<= rhs; - self - } -} - -/// Performs an **unsigned** right shift. -impl std::ops::ShrAssign for SymbolicBitBuf { - fn shr_assign(&mut self, rhs: Self) { - for (i, shift_bit) in rhs.bits.into_iter().enumerate() { - let mut shifted_value = self.clone(); - shifted_value.shift(1 << i, FALSE, ShiftDirection::Right); - self.mux(shifted_value, !shift_bit); - } - } -} - -impl std::ops::Shr for SymbolicBitBuf { - type Output = Self; - - fn shr(mut self, rhs: Self) -> Self::Output { - self >>= rhs; - self - } -} - -impl std::ops::ShrAssign for SymbolicBitBuf { - fn shr_assign(&mut self, rhs: usize) { - self.shift(rhs, FALSE, ShiftDirection::Right); - } -} - -impl std::ops::Shr for SymbolicBitBuf { - type Output = Self; - - fn shr(mut self, rhs: usize) -> Self::Output { - self >>= rhs; - self - } -} diff --git a/crates/sym/src/convert.rs b/crates/sym/src/convert.rs deleted file mode 100644 index dbcb02f..0000000 --- a/crates/sym/src/convert.rs +++ /dev/null @@ -1,346 +0,0 @@ -use crate::bit::{FALSE, SymbolicBit}; -use crate::buf::{SymbolicBitBuf, SymbolicByte}; -use crate::vec::SymbolicBitVec; - -#[derive(thiserror::Error, Debug)] -pub enum ConcretizationError { - #[error("non-literal bit at index {bit_index}")] - NonLiteralBit { bit_index: usize }, - - #[error("value exceeded maximum number of bytes ({max_bytes})")] - Overflow { max_bytes: usize }, -} - -impl From for SymbolicBit { - fn from(value: bool) -> Self { - SymbolicBit::Literal(value) - } -} - -impl TryFrom for bool { - type Error = ConcretizationError; - - fn try_from(value: SymbolicBit) -> Result { - if let SymbolicBit::Literal(value) = value { - Ok(value) - } else { - Err(ConcretizationError::NonLiteralBit { bit_index: 0 }) - } - } -} - -impl From for SymbolicBitVec { - fn from(value: SymbolicBit) -> Self { - std::iter::once(value).collect() - } -} - -/// A wrapper around a value that implements [LittleEndian]. This wrapper implements conversions to -/// and from [SymbolicBitVec] and [SymbolicBitBuf]. Use the macro [concrete_type!] to automatically -/// implement the conversions for a type using this wrapper. -/// -/// # Examples -/// -/// ``` -/// # use symbit::{ConcreteValue, SymbolicBitBuf}; -/// let value = ConcreteValue::new(0xDEADBEEFu32); -/// let buf = SymbolicBitBuf::<32>::from(value); -/// assert_eq!(value, buf.try_into().unwrap()); -/// ``` -#[repr(transparent)] -#[derive(Debug, Copy, Clone, PartialEq, Eq)] -pub struct ConcreteValue> { - value: T, -} - -impl> ConcreteValue { - pub fn new(value: T) -> Self { - Self { value } - } - - pub fn into_inner(self) -> T { - self.value - } - - pub fn symbolize(self) -> Vec { - symbolize(self.value.into_words()).collect() - } -} - -impl> From for ConcreteValue { - fn from(value: T) -> Self { - ConcreteValue { value } - } -} - -impl, const BITS: usize> TryFrom> - for ConcreteValue -{ - type Error = ConcretizationError; - fn try_from(value: SymbolicBitBuf) -> Result { - concretize_bits_into::(value).map(ConcreteValue::from) - } -} - -impl, const BITS: usize> TryFrom<&SymbolicBitBuf> - for ConcreteValue -{ - type Error = ConcretizationError; - fn try_from(value: &SymbolicBitBuf) -> Result { - concretize_bits::(value.iter()).map(ConcreteValue::from) - } -} - -impl, const BITS: usize> From> - for SymbolicBitBuf -{ - fn from(value: ConcreteValue) -> Self { - const { - assert!(8 * BYTES == BITS, "8 BITS must be 1 BYTE"); - } - - // SAFETY: Asserted BITS agrees with BYTES, so the vec length is BITS - let array: [SymbolicBit; BITS] = unsafe { value.symbolize().try_into().unwrap_unchecked() }; - - array.into() - } -} - -impl> TryFrom - for ConcreteValue -{ - type Error = ConcretizationError; - fn try_from(value: SymbolicBitVec) -> Result { - concretize_bits_into::(value).map(ConcreteValue::from) - } -} - -impl> TryFrom<&SymbolicBitVec> - for ConcreteValue -{ - type Error = ConcretizationError; - fn try_from(value: &SymbolicBitVec) -> Result { - concretize_bits::(value.iter()).map(ConcreteValue::from) - } -} - -impl> From> for SymbolicBitVec { - fn from(value: ConcreteValue) -> Self { - value.symbolize().into_iter().collect() - } -} - -#[macro_export] -macro_rules! concrete_type { - ($target:ty) => { - impl TryFrom for $target { - type Error = ConcretizationError; - fn try_from(value: SymbolicBitVec) -> Result { - ConcreteValue::try_from(value).map(ConcreteValue::into_inner) - } - } - - impl TryFrom<&SymbolicBitVec> for $target { - type Error = ConcretizationError; - fn try_from(value: &SymbolicBitVec) -> Result { - ConcreteValue::try_from(value).map(ConcreteValue::into_inner) - } - } - - impl From<$target> for SymbolicBitVec { - fn from(value: $target) -> Self { - ConcreteValue::new(value).into() - } - } - - impl From<$target> for SymbolicBitBuf<{ 8 * std::mem::size_of::<$target>() }> { - fn from(value: $target) -> Self { - ConcreteValue::new(value).into() - } - } - - concrete_type!($target, { 8 * std::mem::size_of::<$target>() }); - }; - ($target:ty, $size:expr) => { - impl TryFrom> for $target { - type Error = ConcretizationError; - fn try_from(value: SymbolicBitBuf<$size>) -> Result { - ConcreteValue::try_from(value).map(ConcreteValue::into_inner) - } - } - - impl TryFrom<&SymbolicBitBuf<$size>> for $target { - type Error = ConcretizationError; - fn try_from(value: &SymbolicBitBuf<$size>) -> Result { - ConcreteValue::try_from(value).map(ConcreteValue::into_inner) - } - } - }; -} - -concrete_type!(u8); -concrete_type!(u8, 1); -concrete_type!(u8, 2); -concrete_type!(u8, 3); -concrete_type!(u8, 4); -concrete_type!(u8, 5); -concrete_type!(u8, 6); -concrete_type!(u8, 7); -concrete_type!(u16); -concrete_type!(u32); -concrete_type!(u64); -concrete_type!(u128); -concrete_type!(usize); - -impl FromIterator for SymbolicBitVec { - fn from_iter>(iter: T) -> Self { - iter.into_iter() - .flat_map(|bitvec| bitvec.into_iter()) - .collect() - } -} - -impl FromIterator for SymbolicBitVec { - fn from_iter>(iter: T) -> Self { - iter.into_iter() - .flat_map(|byte| byte.into_inner().into_iter()) - .collect() - } -} - -impl FromIterator for SymbolicBitVec { - fn from_iter>(iter: T) -> Self { - symbolize(iter).collect() - } -} - -pub fn symbolize(iter: impl IntoIterator) -> impl Iterator { - iter.into_iter().flat_map(|byte| { - let mut bits = [FALSE; 8]; - - for (index, bit) in bits.iter_mut().enumerate() { - *bit = SymbolicBit::Literal((byte & (1 << index)) > 0); - } - - bits - }) -} - -pub fn concretize<'a, T, const N: usize>( - iter: impl Iterator, -) -> std::result::Result -where - T: LittleEndian, -{ - concretize_bits(iter.map(|byte| byte.as_ref()).flat_map(|bits| bits.iter())) -} - -pub fn concretize_into( - iter: impl IntoIterator, -) -> std::result::Result -where - T: LittleEndian, -{ - concretize_bits_into( - iter.into_iter() - .map(|byte| byte.into_inner()) - .flat_map(|bits| bits.into_iter()), - ) -} - -pub fn concretize_bits_cow<'a, T, const N: usize>( - iter: impl Iterator>, -) -> std::result::Result -where - T: LittleEndian, -{ - // TODO Once we can use this directly in the function signature we can remove N - // - // Tracking issue: https://github.com/mnemonikr/symbolic-pcode/issues/108 - const { - assert!(std::mem::size_of::() == N, "N must match size of T"); - }; - - let mut bytes = [0u8; N]; - let mut byte_index = 0; - let mut bit_index = 0; - for cow_bit in iter { - if byte_index >= N { - return Err(ConcretizationError::Overflow { max_bytes: N }); - } - - let bit = match cow_bit { - std::borrow::Cow::Owned(SymbolicBit::Literal(bit)) => bit, - std::borrow::Cow::Borrowed(SymbolicBit::Literal(bit)) => *bit, - _ => { - return Err(ConcretizationError::NonLiteralBit { - bit_index: 8 * byte_index + bit_index, - }); - } - }; - - if bit { - bytes[byte_index] |= 1 << bit_index; - } - - bit_index += 1; - if bit_index == 8 { - bit_index = 0; - byte_index += 1; - } - } - - Ok(T::from_words(bytes)) -} - -pub fn concretize_bits<'a, T, const N: usize>( - iter: impl Iterator, -) -> std::result::Result -where - T: LittleEndian, -{ - concretize_bits_cow(iter.map(std::borrow::Cow::Borrowed)) -} - -pub fn concretize_bits_into( - iter: impl IntoIterator, -) -> std::result::Result -where - T: LittleEndian, -{ - concretize_bits_cow(iter.into_iter().map(std::borrow::Cow::Owned)) -} - -/// Little-endian representation of an object with a known size at compile-time. The default word -/// size is a byte. -pub trait LittleEndian { - /// Create an instance of this object from a little-endian representation. - fn from_words(words: [T; N]) -> Self; - - /// Convert self into an array of words. - fn into_words(self) -> [T; N]; -} - -macro_rules! impl_little_endian { - ($target:ty) => { - impl_little_endian!($target, { std::mem::size_of::<$target>() }); - }; - ($target:ty, $size:expr) => { - impl LittleEndian<$size> for $target { - fn from_words(bytes: [u8; $size]) -> Self { - Self::from_le_bytes(bytes) - } - - fn into_words(self) -> [u8; $size] { - self.to_le_bytes() - } - } - }; -} - -impl_little_endian!(usize); -impl_little_endian!(u128); -impl_little_endian!(u64); -impl_little_endian!(u32); -impl_little_endian!(u16); -impl_little_endian!(u8); diff --git a/crates/sym/src/eval.rs b/crates/sym/src/eval.rs deleted file mode 100644 index 9cf23b3..0000000 --- a/crates/sym/src/eval.rs +++ /dev/null @@ -1,146 +0,0 @@ -use std::collections::{BTreeMap, BTreeSet}; - -use crate::{SymbolicBit, SymbolicBitVec}; - -/// A simple evaluator that evaluates a [SymbolicBit] given a [VariableAssignments]. Portions of the -/// evaluation may be cached since the variable assignments are fixed for a given evaluator. -#[derive(Clone, Debug, Default)] -pub struct Evaluator { - assignments: VariableAssignments, -} - -#[derive(Clone, Default, PartialEq, Eq, Debug)] -pub struct Evaluation { - /// The evaluation response. This may not be populated if there was a symbolic bit without a - /// known concrete value - pub response: Option, - - /// Variables that were used and their assigned value - pub used_variables: BTreeMap, - - /// Variables that were used in the evaluation but did not have an assignment - pub unassigned_variables: BTreeSet, -} - -impl Evaluator { - /// Create a new instance using the given [VariableAssignments]. The assignments are fixed for - /// the lifetime of this evaluator. - pub fn new(assignments: impl Into) -> Self { - Self { - assignments: assignments.into(), - } - } - - pub fn evaluate(&self, bit: &SymbolicBit) -> Evaluation { - match bit { - SymbolicBit::Literal(x) => Evaluation { - response: Some(*x), - ..Default::default() - }, - SymbolicBit::Variable(id) => { - let response = self.assignments.get(*id); - if let Some(x) = response { - Evaluation { - response, - used_variables: std::iter::once((*id, x)).collect(), - ..Default::default() - } - } else { - Evaluation { - response, - unassigned_variables: std::iter::once(*id).collect(), - ..Default::default() - } - } - } - SymbolicBit::Not(bit) => { - let mut evaluation = self.evaluate(bit); - evaluation.response = evaluation.response.map(|x| !x); - evaluation - } - SymbolicBit::And(lhs, rhs) => { - let mut lhs = self.evaluate(lhs); - if let Some(lhs_response) = lhs.response { - if !lhs_response { - // LHS is false, do not need to evaluate RHS - lhs - } else { - // LHS is true, evaluate RHS - let mut rhs = self.evaluate(rhs); - if let Some(rhs_response) = rhs.response { - // RHS is concrete value - lhs.response = Some(lhs_response && rhs_response); - lhs.used_variables.append(&mut rhs.used_variables); - lhs - } else { - // RHS is symbolic - rhs - } - } - } else { - // LHS is not concrete. Should still evaluate RHS in case it is false - let rhs = self.evaluate(rhs); - if matches!(rhs.response, Some(false)) { - // RHS is false, ignore LHS - rhs - } else { - // RHS is either true or symbolic but LHS is already symbolic - lhs - } - } - } - } - } -} - -impl From for Evaluator { - fn from(value: VariableAssignments) -> Self { - Self::new(value) - } -} - -/// Mapping [SymbolicBit::Variable] identifiers to [SymbolicBit::Literal] values. -#[derive(Clone, Debug, Default)] -pub struct VariableAssignments { - assignments: BTreeMap, -} - -impl VariableAssignments { - /// Create variable assignments given a [SymbolicBitVec] containing only [SymbolicBit::Variable] - /// variants and another [SymbolicBitVec] containing only [SymbolicBit::Literal] variants. - /// Incorrect variants in either will be ignored. - /// - /// Both bit vectors should have the same length. In the event they are not equal, the shorter - /// length will be used for both. - pub fn from_bitvecs(variables: &SymbolicBitVec, literals: &SymbolicBitVec) -> Self { - let iter = - std::iter::zip(variables.iter(), literals.iter()).filter_map(|(variable, literal)| { - if let SymbolicBit::Variable(variable) = variable - && let SymbolicBit::Literal(literal) = literal - { - return Some((*variable, *literal)); - } - - None - }); - Self::from_iter(iter) - } - - pub fn get(&self, variable_id: usize) -> Option { - self.assignments.get(&variable_id).copied() - } -} - -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 { - assignments: iter.into_iter().collect(), - } - } -} diff --git a/crates/sym/src/lib.rs b/crates/sym/src/lib.rs deleted file mode 100644 index e406d45..0000000 --- a/crates/sym/src/lib.rs +++ /dev/null @@ -1,22 +0,0 @@ -#![doc=include_str!("../README.md")] - -mod bit; -mod buf; -mod convert; -mod eval; -mod vec; - -pub use crate::bit::*; -pub use crate::buf::*; -pub use crate::convert::ConcreteValue; -pub use crate::convert::ConcretizationError; -pub use crate::convert::concretize; -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/tests.rs b/crates/sym/src/tests.rs deleted file mode 100644 index 4f2ed8f..0000000 --- a/crates/sym/src/tests.rs +++ /dev/null @@ -1,5 +0,0 @@ -mod bit; -mod bitbuf; -mod bitvec; -mod convert; -mod eval; diff --git a/crates/sym/src/tests/bit.rs b/crates/sym/src/tests/bit.rs deleted file mode 100644 index df4d421..0000000 --- a/crates/sym/src/tests/bit.rs +++ /dev/null @@ -1,90 +0,0 @@ -use crate::*; - -#[test] -fn bit_equality() { - let x = SymbolicBit::Literal(true); - assert_eq!(x.clone().equals(x), SymbolicBit::Literal(true)); - - let x = SymbolicBit::Literal(false); - assert_eq!(x.clone().equals(x), SymbolicBit::Literal(true)); -} - -#[test] -fn double_negation() { - let x = SymbolicBit::Variable(0); - assert_eq!(!!x.clone(), x); -} - -#[test] -fn conjunction_with_false() { - let x = SymbolicBit::Variable(0); - assert_eq!( - x.clone() & SymbolicBit::Literal(false), - SymbolicBit::Literal(false), - ); - assert_eq!( - SymbolicBit::Literal(false) & x.clone(), - SymbolicBit::Literal(false), - ); -} - -#[test] -fn conjunction_with_true() { - let x = SymbolicBit::Variable(0); - assert_eq!(x.clone() & SymbolicBit::Literal(true), x); - assert_eq!(SymbolicBit::Literal(true) & x.clone(), x); -} - -#[test] -fn conjunction_with_negated_self() { - let x = SymbolicBit::Variable(0); - assert_eq!(x.clone() & !x.clone(), SymbolicBit::Literal(false)); - assert_eq!(!x.clone() & x.clone(), SymbolicBit::Literal(false)); -} - -#[test] -fn disjunction_with_false() { - let x = SymbolicBit::Variable(0); - assert_eq!(x.clone() | SymbolicBit::Literal(false), x); - assert_eq!(SymbolicBit::Literal(false) | x.clone(), x); -} - -#[test] -fn disjunction_with_true() { - let x = SymbolicBit::Variable(0); - assert_eq!( - x.clone() | SymbolicBit::Literal(true), - SymbolicBit::Literal(true) - ); - assert_eq!( - SymbolicBit::Literal(true) | x.clone(), - SymbolicBit::Literal(true), - ); -} - -#[test] -fn exclusive_or_with_same_variable() { - let x = SymbolicBit::Variable(0); - assert_eq!(x.clone() ^ x.clone(), SymbolicBit::Literal(false)); -} - -#[test] -fn exclusive_or_with_complex_self() { - let x = complex_bit(); - assert_eq!(x.clone() ^ x.clone(), SymbolicBit::Literal(false)); -} - -#[test] -fn exclusive_or_with_zero() { - let x = SymbolicBit::Variable(0); - assert_eq!(x.clone() ^ SymbolicBit::Literal(false), x); - assert_eq!(SymbolicBit::Literal(false) ^ x.clone(), x); -} - -fn complex_bit() -> SymbolicBit { - let mut bit = SymbolicBit::Literal(true); - for i in 0..5 { - bit = SymbolicBit::Variable(i) & bit; - } - bit -} diff --git a/crates/sym/src/tests/bitbuf.rs b/crates/sym/src/tests/bitbuf.rs deleted file mode 100644 index 41be150..0000000 --- a/crates/sym/src/tests/bitbuf.rs +++ /dev/null @@ -1,51 +0,0 @@ -use crate::{FALSE, SymbolicBitBuf, TRUE}; - -#[test] -fn ops_not() { - let x: SymbolicBitBuf<1> = [FALSE].into(); - assert_eq!(u8::try_from(!x.clone()).unwrap(), 0x1); - assert_eq!(u8::try_from(!!x).unwrap(), 0x0); -} - -#[test] -fn ops_bitor() { - let x: SymbolicBitBuf<4> = [FALSE, FALSE, TRUE, TRUE].into(); - let y: SymbolicBitBuf<4> = [FALSE, TRUE, FALSE, TRUE].into(); - assert_eq!(u8::try_from(x | y).unwrap(), 0x0E); -} - -#[test] -fn ops_bitand() { - let x: SymbolicBitBuf<4> = [FALSE, FALSE, TRUE, TRUE].into(); - let y: SymbolicBitBuf<4> = [FALSE, TRUE, FALSE, TRUE].into(); - assert_eq!(u8::try_from(x & y).unwrap(), 0x08); -} - -#[test] -fn ops_shl_usize() { - let x: SymbolicBitBuf<4> = [TRUE, FALSE, FALSE, FALSE].into(); - let result = u8::try_from(x << 1).unwrap(); - assert_eq!(result, 0x2); -} - -#[test] -fn ops_shl_sym() { - let x: SymbolicBitBuf<4> = [TRUE, FALSE, FALSE, FALSE].into(); - let result = u8::try_from(x.clone() << x).unwrap(); - assert_eq!(result, 0x2); -} - -#[test] -fn ops_shr_usize() { - let x: SymbolicBitBuf<4> = [FALSE, TRUE, FALSE, FALSE].into(); - let result = u8::try_from(x >> 1).unwrap(); - assert_eq!(result, 0x1); -} - -#[test] -fn ops_shr_sym() { - let x: SymbolicBitBuf<4> = [FALSE, TRUE, FALSE, FALSE].into(); - let y: SymbolicBitBuf<4> = [TRUE, FALSE, FALSE, FALSE].into(); - let result = u8::try_from(x >> y).unwrap(); - assert_eq!(result, 0x1); -} diff --git a/crates/sym/src/tests/bitvec.rs b/crates/sym/src/tests/bitvec.rs deleted file mode 100644 index 8c5b1a9..0000000 --- a/crates/sym/src/tests/bitvec.rs +++ /dev/null @@ -1,535 +0,0 @@ -use crate::{SymbolicBit, SymbolicBitVec}; - -#[test] -fn add_bytes_no_carry() { - let x: SymbolicBitVec = 0xAAu8.into(); - let y: SymbolicBitVec = 0x55u8.into(); - let sum: u8 = (x + y).try_into().expect("failed byte converison"); - assert_eq!(sum, 0xFF); -} - -#[test] -fn one_plus_one() { - let x: SymbolicBitVec = 0x01u8.into(); - let y: SymbolicBitVec = 0x01u8.into(); - let sum: u8 = (x + y).try_into().expect("failed byte converison"); - assert_eq!(sum, 0x02); -} - -#[test] -fn maximal_carry_addition() { - let x: SymbolicBitVec = 0x7Fu8.into(); - let y: SymbolicBitVec = 0x7Fu8.into(); - let sum: u8 = (x + y).try_into().expect("failed byte converison"); - assert_eq!(sum, 0xFE); -} - -#[test] -fn negative_one() { - let one: SymbolicBitVec = 0x01u8.into(); - let negative_one: u8 = (-one).try_into().expect("failed byte converison"); - assert_eq!(negative_one, u8::MAX); -} - -#[test] -fn addition_overflow() { - let x: SymbolicBitVec = u8::MAX.into(); - let sum: u8 = (x + 1u8.into()).try_into().expect("failed byte converison"); - assert_eq!(sum, 0x00); -} - -#[test] -fn addition_overflow_carry() { - let x: SymbolicBitVec = u8::MAX.into(); - let y: SymbolicBitVec = 1u8.into(); - let carry = x.addition_carry_bits(y); - assert_eq!(carry[8], SymbolicBit::Literal(true)); - - let x: SymbolicBitVec = (u8::MAX - 1).into(); - let y: SymbolicBitVec = 1u8.into(); - let carry = x.addition_carry_bits(y); - assert_eq!(carry[8], SymbolicBit::Literal(false)); -} - -#[test] -fn subtraction() { - for n in u8::MIN..=u8::MAX { - let x: SymbolicBitVec = n.into(); - let y: SymbolicBitVec = n.into(); - let diff: u8 = (x - y).try_into().expect("failed byte converison"); - assert_eq!(diff, 0); - } -} - -#[test] -fn subtraction_borrows() { - let test_data = (u8::MIN..=u8::MAX) - .map(|value| (value, value, false)) - .chain(vec![ - (0x00, 0x80, true), // 0 - (-128) != -128 - (0x01, 0x81, true), // 1 - (-127) != -128 - (0x80, 0x00, false), // -128 - 0 = -128 - (0x80, 0x01, true), // -128 - 1 != 127 - ]) - .collect::>(); - - for (lhs, rhs, expected_result) in test_data { - let x: SymbolicBitVec = lhs.into(); - let y: SymbolicBitVec = rhs.into(); - let (_, borrows) = x.subtraction_with_borrow(y); - assert_eq!( - borrows, - SymbolicBit::Literal(expected_result), - "expected {lhs:#02x} - {rhs:#02x} borrow to be {expected_result}" - ); - } -} - -#[test] -fn left_shift() { - for n in u8::MIN..u8::MAX { - let x: SymbolicBitVec = 1u8.into(); - let result: u8 = (x << n as usize) - .try_into() - .expect("failed byte conversion"); - - // Rust panics if shifting more than byte size - let expected_result = if n < 8 { 1u8 << n } else { 0 }; - assert_eq!(result, expected_result); - } -} - -#[test] -fn symbolic_concrete_conversions() { - for n in 0..u8::MAX { - let symbolic_byte: SymbolicBitVec = n.into(); - let concrete_byte: u8 = symbolic_byte - .try_into() - .expect("failed to convert back into byte"); - assert_eq!(concrete_byte, n); - } -} - -#[test] -fn sign_extension() { - let x: SymbolicBitVec = u8::MAX.into(); - let sext: u16 = x - .sign_extend(8) - .try_into() - .expect("failed concrete conversion"); - assert_eq!(sext, 0xFFFFu16); -} - -#[test] -fn zero_extension() { - let x: SymbolicBitVec = u8::MAX.into(); - let zext: u16 = x - .zero_extend(8) - .try_into() - .expect("failed concrete conversion"); - assert_eq!(zext, 0x00FFu16); -} - -#[test] -fn concatenation() { - let x: SymbolicBitVec = 0xADu8.into(); - let y: SymbolicBitVec = 0xDEu8.into(); - let concat: u16 = x.concat(y).try_into().expect("failed type conversion"); - assert_eq!(concat, 0xDEADu16); -} - -#[test] -fn truncation_lsb() { - let x: SymbolicBitVec = 0xDEADu16.into(); - let truncated: u8 = x - .truncate_lsb(8) - .try_into() - .expect("failed type converison"); - assert_eq!(truncated, 0xDEu8); -} - -#[test] -fn truncation_msb() { - let x: SymbolicBitVec = 0xDEADu16.into(); - let truncated: u8 = x - .truncate_msb(8) - .try_into() - .expect("failed type converison"); - assert_eq!(truncated, 0xADu8); -} - -#[test] -fn split_into_bytes() { - let x: SymbolicBitVec = 0xDEADu16.into(); - let split = x.into_parts(8); - assert_eq!(split.len(), 2); - - let byte: u8 = (&split[0]).try_into().expect("failed type conversion"); - assert_eq!(byte, 0xADu8); - - let byte: u8 = (&split[1]).try_into().expect("failed type conversion"); - assert_eq!(byte, 0xDEu8); -} - -#[test] -fn one_bit_equality() { - let x = SymbolicBitVec::constant(0, 1); - let y = SymbolicBitVec::constant(0, 1); - let eq = x.equals(y); - assert_eq!(eq, SymbolicBit::Literal(true)); - - let x = SymbolicBitVec::constant(0, 1); - let y = SymbolicBitVec::constant(1, 1); - let eq = x.equals(y); - assert_eq!(eq, SymbolicBit::Literal(false)); -} - -#[test] -fn equals() { - let x: SymbolicBitVec = 0xFEEDF00Du32.into(); - let y: SymbolicBitVec = 0xDEEDF00Du32.into(); - let eq = x.clone().equals(x.clone()); - let neq = x.equals(y); - assert_eq!(eq, SymbolicBit::Literal(true)); - assert_eq!(neq, SymbolicBit::Literal(false)); -} - -#[test] -fn less_than() { - for x in 0..16u8 { - for y in 0..16u8 { - let sym_x = SymbolicBitVec::constant(x.into(), 4); - let sym_y = SymbolicBitVec::constant(y.into(), 4); - let result = sym_x.less_than(sym_y); - assert_eq!(result, SymbolicBit::Literal(x < y), "failed {x} < {y}"); - } - } -} - -#[test] -fn greater_than() { - for x in 0..16u8 { - for y in 0..16u8 { - let sym_x = SymbolicBitVec::constant(x.into(), 4); - let sym_y = SymbolicBitVec::constant(y.into(), 4); - let result = sym_x.greater_than(sym_y); - assert_eq!(result, SymbolicBit::Literal(x > y), "failed {x} > {y}"); - } - } -} - -#[test] -fn signed_less_than() { - let neg_one: SymbolicBitVec = 0xFFu8.into(); - let neg_two: SymbolicBitVec = 0xFEu8.into(); - let pos_one: SymbolicBitVec = 0x01u8.into(); - let pos_two: SymbolicBitVec = 0x02u8.into(); - - assert_eq!( - neg_two.clone().signed_less_than(neg_one.clone()), - SymbolicBit::Literal(true), - "Expect -2 < -1 (signed comparison)", - ); - assert_eq!( - neg_one.clone().signed_less_than(pos_one.clone()), - SymbolicBit::Literal(true), - "Expect -1 < 1 (signed comparison)", - ); - assert_eq!( - pos_one.clone().signed_less_than(pos_two.clone()), - SymbolicBit::Literal(true), - "Expect 1 < 2 (signed comparison)", - ); - assert_eq!( - pos_one.clone().signed_less_than(pos_one.clone()), - SymbolicBit::Literal(false), - "Expect 1 < 1 to be false (signed comparison)", - ); - assert_eq!( - neg_one.clone().signed_less_than(neg_one.clone()), - SymbolicBit::Literal(false), - "Expect -1 < -1 to be false (signed comparison)", - ); -} - -#[test] -fn signed_greater_than() { - let neg_one: SymbolicBitVec = 0xFFu8.into(); - let neg_two: SymbolicBitVec = 0xFEu8.into(); - let pos_one: SymbolicBitVec = 0x01u8.into(); - let pos_two: SymbolicBitVec = 0x02u8.into(); - - assert_eq!( - pos_two.clone().signed_greater_than(pos_one.clone()), - SymbolicBit::Literal(true), - "Expect 2 > 1 (signed comparison)", - ); - assert_eq!( - pos_one.clone().signed_greater_than(neg_one.clone()), - SymbolicBit::Literal(true), - "Expect 1 > -1 (signed comparison)", - ); - assert_eq!( - neg_one.clone().signed_greater_than(neg_two.clone()), - SymbolicBit::Literal(true), - "Expect -1 > -2 (signed comparison)", - ); - assert_eq!( - pos_one.clone().signed_greater_than(pos_one.clone()), - SymbolicBit::Literal(false), - "Expect 1 > 1 to be false (signed comparison)", - ); - assert_eq!( - neg_one.clone().signed_greater_than(neg_one.clone()), - SymbolicBit::Literal(false), - "Expect -1 > -1 to be false (signed comparison)", - ); -} - -#[test] -fn signed_less_than_eq() { - let neg_one: SymbolicBitVec = 0xFFu8.into(); - let neg_two: SymbolicBitVec = 0xFEu8.into(); - let pos_one: SymbolicBitVec = 0x01u8.into(); - let pos_two: SymbolicBitVec = 0x02u8.into(); - - assert_eq!( - neg_two.clone().signed_less_than_eq(neg_one.clone()), - SymbolicBit::Literal(true), - "Expect -2 < -1 (signed comparison)", - ); - assert_eq!( - neg_one.clone().signed_less_than_eq(pos_one.clone()), - SymbolicBit::Literal(true), - "Expect -1 < 1 (signed comparison)", - ); - assert_eq!( - pos_one.clone().signed_less_than_eq(pos_two.clone()), - SymbolicBit::Literal(true), - "Expect 1 < 2 (signed comparison)", - ); - assert_eq!( - pos_one.clone().signed_less_than_eq(pos_one.clone()), - SymbolicBit::Literal(true), - "Expect 1 < 1 (signed comparison)", - ); - assert_eq!( - neg_one.clone().signed_less_than_eq(neg_one.clone()), - SymbolicBit::Literal(true), - "Expect -1 < -1 (signed comparison)", - ); -} - -#[test] -fn signed_greater_than_eq() { - let neg_one: SymbolicBitVec = 0xFFu8.into(); - let neg_two: SymbolicBitVec = 0xFEu8.into(); - let pos_one: SymbolicBitVec = 0x01u8.into(); - let pos_two: SymbolicBitVec = 0x02u8.into(); - - assert_eq!( - pos_two.clone().signed_greater_than_eq(pos_one.clone()), - SymbolicBit::Literal(true), - "Expect 2 >= 1 (signed comparison)", - ); - assert_eq!( - pos_one.clone().signed_greater_than_eq(neg_one.clone()), - SymbolicBit::Literal(true), - "Expect 1 >= -1 (signed comparison)", - ); - assert_eq!( - neg_one.clone().signed_greater_than_eq(neg_two.clone()), - SymbolicBit::Literal(true), - "Expect -1 >= -2 (signed comparison)", - ); - assert_eq!( - pos_one.clone().signed_greater_than_eq(pos_one.clone()), - SymbolicBit::Literal(true), - "Expect 1 >= 1 (signed comparison)", - ); - assert_eq!( - neg_one.clone().signed_greater_than_eq(neg_one.clone()), - SymbolicBit::Literal(true), - "Expect -1 >= -1 (signed comparison)", - ); -} - -#[test] -fn popcount() { - for n in 0..=8 { - let value = SymbolicBitVec::constant((1 << n) - 1, 8); - let popcount = value.popcount(); - let popcount: u8 = popcount.try_into().expect("failed converison"); - assert_eq!(popcount, n); - } -} - -#[test] -fn shift_left() { - for n in 0..=8 { - let value = SymbolicBitVec::constant(0b0000_0001, 8); - let shift_amount = SymbolicBitVec::constant(n, 8); - let expected = if n < 8 { 1 << n } else { 0 }; - let result = value << shift_amount; - assert_eq!(result.len(), 8); - - let result: u8 = result.try_into().expect("failed conversion"); - assert_eq!(result, expected, "failed 1 << {n}"); - } -} - -#[test] -fn shift_right() { - for n in 0..=8 { - let value = SymbolicBitVec::constant(0b1000_0000, 8); - let shift_amount = SymbolicBitVec::constant(n, 8); - let expected = if n < 8 { 0x80 >> n } else { 0 }; - let result: u8 = (value >> shift_amount) - .try_into() - .expect("failed conversion"); - assert_eq!(result, expected, "failed 0x80 >> {n}"); - } -} - -#[test] -fn signed_shift_right_negative() { - for n in 0..=8 { - let value = SymbolicBitVec::constant(0b1000_0000, 8); - let shift_amount = SymbolicBitVec::constant(n, 8); - let expected = if n < 8 { (-128 as i8 >> n) as u8 } else { 0xFF }; - let result: u8 = value - .signed_shift_right(shift_amount) - .try_into() - .expect("failed conversion"); - assert_eq!(result, expected, "failed signed shift 0x80 >> {n}"); - } -} - -#[test] -fn signed_shift_right_positive() { - for n in 0..=8 { - let value = SymbolicBitVec::constant(0b0111_1111, 8); - let shift_amount = SymbolicBitVec::constant(n, 8); - let expected = if n < 8 { 0x7F >> n } else { 0 }; - let result: u8 = value - .signed_shift_right(shift_amount) - .try_into() - .expect("failed conversion"); - assert_eq!(result, expected, "failed signed shift 0x7F >> {n}"); - } -} - -#[test] -fn multiply() { - let output_bits = 8; - for n in 0..16u8 { - let value = SymbolicBitVec::constant(n.into(), 4); - let square = value.clone() * value; - assert_eq!( - square.len(), - output_bits, - "expected {output_bits} bits in result" - ); - - let square: u8 = square.try_into().expect("failed conversion"); - assert_eq!(square, n * n, "failed {n} * {n}"); - } -} - -#[test] -fn signed_multiply() { - let output_bits = 8; - for n in 0..16u8 { - let value = SymbolicBitVec::constant(n.into(), 4); - let value = value.sign_extend(4); - let n: u8 = value.clone().try_into().expect("failed conversion"); - let square = value.clone().multiply(value, output_bits); - assert_eq!( - square.len(), - output_bits, - "expected {output_bits} bits in result" - ); - - let square: u8 = square.try_into().expect("failed conversion"); - - let n = n as i8; - assert_eq!(square as i8, n * n, "failed {n} * {n}"); - } -} - -#[test] -fn single_bit_multiply() { - let output_bits = 1; - for n in 0..16u8 { - let expected = (n * n) & 1; - let value = SymbolicBitVec::constant(n.into(), 4); - let value = value.sign_extend(4); - let n: u8 = value.clone().try_into().expect("failed conversion"); - let result = value.clone().multiply(value, output_bits); - assert_eq!( - result.len(), - output_bits, - "expected {output_bits} bits in result" - ); - - let result: u8 = result.try_into().expect("failed conversion"); - assert_eq!(result, expected, "failed to select lsb of {n} * {n}"); - } -} - -#[test] -fn unsigned_divide() { - for dividend in 0..16u8 { - for divisor in 1..16u8 { - let sym_dividend = SymbolicBitVec::constant(dividend.into(), 4); - let sym_divisor = SymbolicBitVec::constant(divisor.into(), 4); - let (quotient, remainder) = sym_divisor.unsigned_divide(sym_dividend); - - let quotient: u8 = quotient.try_into().expect("failed quotient conversion"); - let remainder: u8 = remainder.try_into().expect("failed remainder conversion"); - - let expected_quotient = dividend / divisor; - let expected_remainder = dividend % divisor; - assert_eq!( - quotient, expected_quotient, - "invalid quotient for {dividend} / {divisor}" - ); - assert_eq!( - remainder, expected_remainder, - "invalid remainder for {dividend} / {divisor}" - ); - } - } -} - -#[test] -fn signed_divide() { - for dividend in 0..16u8 { - for divisor in 1..16u8 { - let sym_dividend = SymbolicBitVec::constant(dividend.into(), 4).sign_extend(4); - let sym_divisor = SymbolicBitVec::constant(divisor.into(), 4).sign_extend(4); - let dividend: u8 = sym_dividend.clone().try_into().unwrap(); - let dividend = dividend as i8; - let divisor: u8 = sym_divisor.clone().try_into().unwrap(); - let divisor = divisor as i8; - - let (quotient, remainder) = sym_divisor.signed_divide(sym_dividend); - - let quotient: u8 = quotient.try_into().expect("failed quotient conversion"); - let quotient = quotient as i8; - let remainder: u8 = remainder.try_into().expect("failed remainder conversion"); - let remainder = remainder as i8; - - let expected_quotient = dividend / divisor; - let expected_remainder = dividend % divisor; - assert_eq!( - quotient, expected_quotient, - "invalid quotient for {dividend} / {divisor}" - ); - assert_eq!( - remainder, expected_remainder, - "invalid remainder for {dividend} / {divisor}" - ); - } - } -} diff --git a/crates/sym/src/tests/convert.rs b/crates/sym/src/tests/convert.rs deleted file mode 100644 index 45ac898..0000000 --- a/crates/sym/src/tests/convert.rs +++ /dev/null @@ -1,157 +0,0 @@ -use crate::*; - -#[test] -fn concretize_buf() { - assert_eq!(0, u128::try_from(SymbolicBitBuf::<128>::default()).unwrap()); - assert_eq!(0, u64::try_from(SymbolicBitBuf::<64>::default()).unwrap()); - assert_eq!(0, u32::try_from(SymbolicBitBuf::<32>::default()).unwrap()); - assert_eq!(0, u16::try_from(SymbolicBitBuf::<16>::default()).unwrap()); - assert_eq!(0, u8::try_from(SymbolicBitBuf::<8>::default()).unwrap()); - assert_eq!( - 0, - usize::try_from(SymbolicBitBuf::<{ 8 * std::mem::size_of::() }>::default()).unwrap() - ); -} - -#[test] -fn symbolicbitbuf_conversions() { - let value: u8 = 0x5A; - let buf = SymbolicBitBuf::from(value); - assert_eq!(value, u8::try_from(&buf).unwrap()); - assert_eq!(value, u8::try_from(buf).unwrap()); - - let value: u16 = 0xBEEF; - let buf = SymbolicBitBuf::from(value); - assert_eq!(value, u16::try_from(&buf).unwrap()); - assert_eq!(value, u16::try_from(buf).unwrap()); - - let value: u32 = 0xDEADBEEF; - let buf = SymbolicBitBuf::from(value); - assert_eq!(value, u32::try_from(&buf).unwrap()); - assert_eq!(value, u32::try_from(buf).unwrap()); - - let value: u64 = 0xFEEDBEEF_0BADF00D; - let buf = SymbolicBitBuf::from(value); - assert_eq!(value, u64::try_from(&buf).unwrap()); - assert_eq!(value, u64::try_from(buf).unwrap()); - - let value: u128 = 0xFEEDBEEF_0BADF00D_DEADBEEF_DEAD4BED; - let buf = SymbolicBitBuf::from(value); - assert_eq!(value, u128::try_from(&buf).unwrap()); - assert_eq!(value, u128::try_from(buf).unwrap()); -} - -#[test] -fn symbolicbitvec_conversions() { - let value: u8 = 0x5A; - assert_eq!(value, u8::try_from(SymbolicBitVec::from(value)).unwrap()); - - let value: u16 = 0xBEEF; - assert_eq!(value, u16::try_from(SymbolicBitVec::from(value)).unwrap()); - - let value: u32 = 0xDEADBEEF; - assert_eq!(value, u32::try_from(SymbolicBitVec::from(value)).unwrap()); - - let value: u64 = 0xFEEDBEEF_0BADF00D; - assert_eq!(value, u64::try_from(SymbolicBitVec::from(value)).unwrap()); - - let value: u128 = 0xFEEDBEEF_0BADF00D_DEADBEEF_DEAD4BED; - assert_eq!(value, u128::try_from(SymbolicBitVec::from(value)).unwrap()); -} - -#[test] -fn bool_happy() { - assert!(bool::try_from(SymbolicBit::from(true)).unwrap()); -} - -#[test] -fn bool_error() { - let err = bool::try_from(SymbolicBit::Variable(0)).unwrap_err(); - assert!(matches!( - err, - ConcretizationError::NonLiteralBit { bit_index: 0 } - )); -} - -#[test] -fn combine_bitvecs() { - let zero = SymbolicBitVec::constant(0, 1); - let one = SymbolicBitVec::constant(1, 1); - let array = [zero, one]; - - // Little endian format means this should be 0b10 when combined - let combined: SymbolicBitVec = array.into_iter().collect(); - assert_eq!(0b10u8, combined.try_into().unwrap()); -} - -#[test] -fn combine_symbytes_into_vec() { - let zero = SymbolicByte::from(0u8); - let one = SymbolicByte::from(1u8); - let array = [zero, one]; - - // Little endian format means this should be 0x0100 when combined - let combined: SymbolicBitVec = array.into_iter().collect(); - assert_eq!(0x0100u16, combined.try_into().unwrap()); -} - -#[test] -fn concretize_happy() { - let zero = SymbolicByte::from(0u8); - let one = SymbolicByte::from(1u8); - let array = [zero, one]; - - assert_eq!(0x0100u16, concretize(array.iter()).unwrap()); - assert_eq!(0x0100u16, concretize_into(array).unwrap()); -} - -#[test] -fn concretize_overflow_err() { - let zero = SymbolicByte::from(0u8); - let one = SymbolicByte::from(1u8); - let array = [zero, one]; - - let err = concretize::(array.iter()).unwrap_err(); - assert!(matches!( - err, - ConcretizationError::Overflow { max_bytes: 1 } - )); - - let err = concretize_into::(array).unwrap_err(); - assert!(matches!( - err, - ConcretizationError::Overflow { max_bytes: 1 } - )); -} - -#[test] -fn concretize_symbolic_err() { - let byte = SymbolicByte::from(SymbolicBit::Variable(0)); - let array = [byte]; - let err = concretize::(array.iter()).unwrap_err(); - assert!(matches!( - err, - ConcretizationError::NonLiteralBit { bit_index: 0 } - )); - - let err = concretize_into::(array).unwrap_err(); - assert!(matches!( - err, - ConcretizationError::NonLiteralBit { bit_index: 0 } - )); -} - -#[test] -fn concrete_value_derives() { - let x = ConcreteValue::new(1u8); - - // Clone - #[expect(clippy::clone_on_copy)] - let y = x.clone(); - - // PartialEq - assert_eq!(x, y); - - // Debug - assert_eq!("ConcreteValue { value: 1 }", format!("{x:?}")); -} diff --git a/crates/sym/src/tests/eval.rs b/crates/sym/src/tests/eval.rs deleted file mode 100644 index 23f85b9..0000000 --- a/crates/sym/src/tests/eval.rs +++ /dev/null @@ -1,194 +0,0 @@ -use std::rc::Rc; - -use crate::*; - -#[test] -fn evaluate_literal() { - let eval = Evaluator::default(); - assert!(eval.evaluate(&TRUE).response.unwrap()); - assert!(!eval.evaluate(&FALSE).response.unwrap()); -} - -#[test] -fn evaluate_variable() { - let x = SymbolicBit::Variable(0); - let y = SymbolicBit::Variable(1); - let evaluator = Evaluator::new(VariableAssignments::from_iter([(0, true), (1, false)])); - let x_eval = evaluator.evaluate(&x); - - assert!(x_eval.response.unwrap(), "evaluation should be true"); - assert!(x_eval.used_variables.get(&0).unwrap(), "x should be true"); - assert!( - !x_eval.used_variables.contains_key(&1), - "y should not be used" - ); - - let y_eval = evaluator.evaluate(&y); - assert!(!y_eval.response.unwrap(), "evaluation should be false"); - assert!(!y_eval.used_variables.get(&1).unwrap(), "y should be false"); - assert!( - !y_eval.used_variables.contains_key(&0), - "x should not be used" - ); -} - -#[test] -fn evaluate_expression() { - let x = SymbolicBit::Variable(0); - let y = SymbolicBit::Variable(1); - let evaluator = Evaluator::new(VariableAssignments::from_iter([(0, true), (1, false)])); - let z = x ^ y; - let evaluation = evaluator.evaluate(&z); - - assert!( - evaluation.response.unwrap(), - "true xor false should be true" - ); - assert!( - evaluation.used_variables.get(&0).unwrap(), - "x should be true" - ); - assert!( - !evaluation.used_variables.get(&1).unwrap(), - "y should be false" - ); -} - -#[test] -fn evaluate_symbolic_expression() { - let x = SymbolicBit::Variable(0); - let y = SymbolicBit::Variable(1); - let evaluator = Evaluator::new(VariableAssignments::from_iter(std::iter::empty())); - let z = x ^ y; - let evaluation = evaluator.evaluate(&z); - - assert!( - evaluation.response.is_none(), - "evaluation should not have a concrete value" - ); - - // One of x or y may not be considered unassigned due to short-circuiting of the evaluation - assert!( - evaluation.unassigned_variables.contains(&0) - || evaluation.unassigned_variables.contains(&1), - "either x or y (or both) should be unassigned" - ); -} - -#[test] -fn evaluate_false_and_symbolic() { - let x = SymbolicBit::Variable(0); - let y = SymbolicBit::Variable(1); - let z = SymbolicBit::And(Rc::new(x), Rc::new(y)); - let evaluator = Evaluator::new(VariableAssignments::from_iter([(0, false)])); - let evaluation = evaluator.evaluate(&z); - - assert!(!evaluation.response.unwrap(), "evaluation should be false"); - assert!( - evaluation.unassigned_variables.is_empty(), - "all evaluated variables should be assigned" - ); -} - -#[test] -fn evaluate_true_and_symbolic() { - let x = SymbolicBit::Variable(0); - let y = SymbolicBit::Variable(1); - let z = SymbolicBit::And(Rc::new(x), Rc::new(y)); - let evaluator = Evaluator::new(VariableAssignments::from_iter([(0, true)])); - let evaluation = evaluator.evaluate(&z); - - assert!( - evaluation.response.is_none(), - "evaluation should be symbolic" - ); - assert!( - evaluation.unassigned_variables.contains(&1), - "y should be unassigned" - ); -} - -#[test] -fn evaluate_symbolic_and_false() { - let x = SymbolicBit::Variable(0); - let y = SymbolicBit::Variable(1); - let z = SymbolicBit::And(Rc::new(x), Rc::new(y)); - let evaluator = Evaluator::new(VariableAssignments::from_iter([(1, false)])); - let evaluation = evaluator.evaluate(&z); - - assert!(!evaluation.response.unwrap(), "evaluation should be false"); - assert!( - evaluation.unassigned_variables.is_empty(), - "all evaluated variables should be assigned" - ); -} - -#[test] -fn evaluate_symbolic_and_true() { - let x = SymbolicBit::Variable(0); - let y = SymbolicBit::Variable(1); - let z = SymbolicBit::And(Rc::new(x), Rc::new(y)); - let evaluator = Evaluator::new(VariableAssignments::from_iter([(1, true)])); - let evaluation = evaluator.evaluate(&z); - - assert!( - evaluation.response.is_none(), - "evaluation should be symbolic" - ); - assert!( - evaluation.unassigned_variables.contains(&0), - "x should be unassigned" - ); -} - -#[test] -fn var_assignments_from_bitvecs() { - let variables = SymbolicBitVec::from_iter([SymbolicBit::Variable(0), SymbolicBit::Variable(1)]); - let literals = SymbolicBitVec::from_iter([TRUE, FALSE]); - let assignments = VariableAssignments::from_bitvecs(&variables, &literals); - assert!(assignments.get(0).unwrap()); - assert!(!assignments.get(1).unwrap()); -} - -#[test] -fn var_assignments_from_swapped_bitvecs() { - let variables = SymbolicBitVec::from_iter([SymbolicBit::Variable(0), SymbolicBit::Variable(1)]); - let literals = SymbolicBitVec::from_iter([TRUE, FALSE]); - - // Swapped the literals and the variables - let assignments = VariableAssignments::from_bitvecs(&literals, &variables); - - assert!(assignments.get(0).is_none()); - assert!(assignments.get(1).is_none()); -} - -#[test] -fn var_assignments_from_bitvecs_without_literals() { - let variables = SymbolicBitVec::from_iter([SymbolicBit::Variable(0), SymbolicBit::Variable(1)]); - - // Swapped the literals and the variables - let assignments = VariableAssignments::from_bitvecs(&variables, &variables); - - assert!(assignments.get(0).is_none()); - assert!(assignments.get(1).is_none()); -} - -#[test] -fn evaluator_from_assignments() { - let variables = SymbolicBitVec::from_iter([SymbolicBit::Variable(0), SymbolicBit::Variable(1)]); - let literals = SymbolicBitVec::from_iter([TRUE, FALSE]); - let assignments = VariableAssignments::from_bitvecs(&variables, &literals); - let evaluator = Evaluator::from(assignments); - assert!( - evaluator - .evaluate(&SymbolicBit::Variable(0)) - .response - .unwrap() - ); - assert!( - !evaluator - .evaluate(&SymbolicBit::Variable(1)) - .response - .unwrap() - ); -} diff --git a/crates/sym/src/vec.rs b/crates/sym/src/vec.rs deleted file mode 100644 index 7b4f56c..0000000 --- a/crates/sym/src/vec.rs +++ /dev/null @@ -1,572 +0,0 @@ -use std::collections::VecDeque; -use std::sync::atomic::{AtomicUsize, Ordering}; - -use crate::bit::{FALSE, SymbolicBit, TRUE}; -use crate::buf::SymbolicByte; - -mod convert; -mod ops; - -#[derive(Debug, Clone)] -pub struct SymbolicBitVec { - bits: VecDeque, -} - -enum ShiftDirection { - Left, - Right, -} - -static START_SYMBOL: AtomicUsize = AtomicUsize::new(0); -impl SymbolicBitVec { - pub fn msb(&self) -> Option<&SymbolicBit> { - self.bits.back() - } - - pub fn lsb(&self) -> Option<&SymbolicBit> { - self.bits.front() - } - - pub fn is_empty(&self) -> bool { - self.bits.is_empty() - } - - pub fn num_bytes(&self) -> usize { - self.bits.len().div_ceil(8) - } - - pub fn len(&self) -> usize { - self.bits.len() - } - - pub fn iter(&self) -> impl Iterator { - self.bits.iter() - } - - pub fn iter_mut(&mut self) -> impl Iterator { - self.bits.iter_mut() - } - - pub fn with_size(num_bits: usize) -> Self { - let start_symbol = START_SYMBOL.fetch_add(num_bits, Ordering::SeqCst); - let mut bits = VecDeque::with_capacity(num_bits); - for i in 0..num_bits { - bits.push_back(SymbolicBit::Variable(start_symbol + i)); - } - - Self { bits } - } - - pub fn into_bytes(self) -> Vec { - assert!(self.bits.len().is_multiple_of(8)); - let num_bytes = self.bits.len() / 8; - - let mut bits = [FALSE; 8]; - let mut bytes = Vec::with_capacity(num_bytes); - - for (i, bit) in self.bits.into_iter().enumerate() { - bits[i % 8] = bit; - if (i + 1).is_multiple_of(8) { - bytes.push(bits.into()); - bits = [FALSE; 8]; - } - } - - bytes - } - - pub fn into_parts(self, num_bits: usize) -> Vec { - assert!(self.bits.len().is_multiple_of(8)); - let mut parts = Vec::new(); - let mut remainder = self; - while remainder.len() > num_bits { - let mut next_split = remainder.bits; - remainder.bits = next_split.split_off(num_bits); - parts.push(SymbolicBitVec { bits: next_split }); - } - parts.push(remainder); - parts - } - - pub fn empty() -> Self { - Self { - bits: VecDeque::with_capacity(0), - } - } - - pub fn constant(mut value: usize, num_bits: usize) -> Self { - let mut bits = VecDeque::with_capacity(num_bits); - for _ in 0..num_bits { - bits.push_back(SymbolicBit::Literal(value & 0x1 > 0)); - value >>= 1; - } - - if value > 0 { - // TODO Throw error, this should be a result - } - - Self { bits } - } - - pub fn signed_minimum_value(num_bits: usize) -> Self { - Self { - bits: std::iter::repeat_n(FALSE, num_bits - 1) - .chain(std::iter::once(TRUE)) - .collect(), - } - } - - pub fn signed_maximum_value(num_bits: usize) -> Self { - Self { - bits: std::iter::repeat_n(TRUE, num_bits - 1) - .chain(std::iter::once(FALSE)) - .collect(), - } - } - - pub fn contains_variable(&self) -> bool { - self.bits - .iter() - .any(|bit| !matches!(*bit, SymbolicBit::Literal(_))) - } - - pub fn equals(self, rhs: Self) -> SymbolicBit { - assert_eq!(self.bits.len(), rhs.bits.len()); - self.equals_unchecked(rhs) - } - - fn equals_unchecked(mut self, mut rhs: Self) -> SymbolicBit { - if self.bits.len() == 1 { - // SAFETY: Know both self and rhs bits length is 1 - unsafe { - self.msb() - .cloned() - .unwrap_unchecked() - .equals(rhs.msb().cloned().unwrap_unchecked()) - } - } else { - let partition = self.bits.len() / 2; - let self_part: Self = self.bits.split_off(partition).into_iter().collect(); - let rhs_part: Self = rhs.bits.split_off(partition).into_iter().collect(); - self_part.equals_unchecked(rhs_part) & self.equals_unchecked(rhs) - } - } - - /// Concatenates the left-hand side with the right-hand side, creating a new `SymbolicBitVec` - /// with a combined length of both inputs. - pub fn concat(mut self, mut rhs: Self) -> Self { - let mut bits = VecDeque::with_capacity(self.bits.len() + rhs.bits.len()); - bits.append(&mut self.bits); - bits.append(&mut rhs.bits); - Self { bits } - } - - /// Creates a new `SymbolicBitVec` with the specified number of least-significant bits removed. - pub fn truncate_lsb(self, num_bits_truncated: usize) -> Self { - Self { - bits: self.bits.into_iter().skip(num_bits_truncated).collect(), - } - } - - /// Creates a new `SymbolicBitVec` with the specified number of most-significant bits removed. - pub fn truncate_msb(self, num_bits_truncated: usize) -> Self { - let num_bits = self.bits.len(); - Self { - bits: self - .bits - .into_iter() - .take(num_bits - num_bits_truncated) - .collect(), - } - } - - /// Create a new `SymbolicBitVec` with the number of additional zero bits specified as the - /// most-significant bits. - pub fn zero_extend(self, num_bits: usize) -> Self { - self.concat(SymbolicBitVec::constant(0, num_bits)) - } - - /// Create a new `SymbolicBitVec` with the number of additional bits specified as the - /// most-significant bits. The additional bits are clones of the original most significant-bit. - pub fn sign_extend(self, num_bits: usize) -> Self { - let mut extension = VecDeque::with_capacity(num_bits); - let msb = self.msb().unwrap(); - for _ in 0..num_bits { - extension.push_back(msb.clone()); - } - - let extension = Self { bits: extension }; - self.concat(extension) - } - - pub fn addition_with_carry(self, rhs: Self) -> (Self, SymbolicBit) { - let mut carry = self.clone().addition_carry_bits(rhs.clone()); - let overflow = carry.bits.pop_back().unwrap(); - let sum = self ^ rhs ^ carry; - (sum, overflow) - } - - pub fn subtraction_with_borrow(self, rhs: Self) -> (Self, SymbolicBit) { - let diff = self.clone() - rhs.clone(); - - // Positive overflow occurs if sign bits are (0, 1) but 1 in sum - let positive_overflow = !self.msb().cloned().unwrap() - & rhs.msb().cloned().unwrap() - & diff.msb().cloned().unwrap(); - - // Negative overflow occurs if sign bits are (1, 0) but 0 in sum - let negative_overflow = self.msb().cloned().unwrap() - & !rhs.msb().cloned().unwrap() - & !diff.msb().cloned().unwrap(); - - // Overflow occurs if either positive or negative overflow occurs - (diff, positive_overflow | negative_overflow) - } - - /// Multiply two integers together. When multiplying unsigned integers together, the number of - /// output bits should be the sum of input sizes unless a lesser size is known in advance. - /// - /// # Unsigned Example - /// - /// ``` - /// # use symbit::SymbolicBitVec; - /// let x = SymbolicBitVec::constant(2, 4); - /// let y = SymbolicBitVec::constant(15, 4); - /// - /// let output_bits = x.len() + y.len(); - /// let product: u8 = x.multiply(y, output_bits).try_into().unwrap(); - /// assert_eq!(product, 30); - /// ``` - /// - /// When multiplying signed integers, both inputs should be sign-extended to the requisite - /// output size. The `output_bits` argument should be set to this size as well. - /// - /// # Signed Example - /// - /// ``` - /// # use symbit::SymbolicBitVec; - /// let x = SymbolicBitVec::constant(0x2, 4); // Positive 2 - /// let y = SymbolicBitVec::constant(0xF, 4); // Negative 1 - /// - /// // Need 8 bits to represent the product of 4-bit numbers - /// let output_bits = x.len() + y.len(); - /// - /// // Sign extend both x and y to match output length - /// let x = x.sign_extend(output_bits - 4); - /// let y = y.sign_extend(output_bits - 4); - /// - /// // Multiply the values, but only keep 8 bits of output - /// let product: u8 = x.multiply(y, output_bits).try_into().unwrap(); - /// let product = product as i8; - /// assert_eq!(product, -2); - /// ``` - pub fn multiply(self, rhs: Self, output_bits: usize) -> Self { - let rhs_size = rhs.len(); - - // The initial zero sum may need to be fewer bits than normal if the number of output bits - // is smaller than self. While additional zeros would not negatively impact the - // computation, this ensures that the final product has the expected number of output bits. - let zero = SymbolicBitVec::constant(0, usize::min(self.len(), output_bits)); - let mut product = rhs.concat(zero.clone()); - - for n in 0..rhs_size { - let selector = product.bits[0].clone(); - - // The number of bits to sum depends on the number of output bits requested. - // We can avoid unnecessary additions in this manner. Consider the following - // where only 4 output bits are requested: - // - // a0 a1 a2 a3 - // b0 b1 b2 b3 - // ----------- - // 0 0 0 0 | [initial sum] - // y0 y1 y2 y3 | [b0] - // y0 y1 y2 | y3 [b1] - // y0 y1 | y2 y3 [b2] - // y0 | y1 y2 y3 [b3] - // ---------------------- - // - // Everything to the right of the | separator does not need to be computed. - let max_sum_bits = output_bits.saturating_sub(n); - let num_sum_bits = usize::min(self.len(), max_sum_bits); - let carry = if num_sum_bits > 0 { - // Select the bits to sum, truncating the most significant bits as necessary - - // Extract num_sum_bits from product starting from rhs_size and store in x. - // The value that's replaced into the product is unimportant since these - // bits will be overwritten by the sum x + y. - let mut x = SymbolicBitVec::constant(0, num_sum_bits); - product - .iter_mut() - .skip(rhs_size) - .take(num_sum_bits) - .zip(x.iter_mut()) - .for_each(|(p, x)| std::mem::swap(p, x)); - - let mut y = self.clone().truncate_msb(self.len() - num_sum_bits); - y.mux_mut(SymbolicBitVec::constant(0, num_sum_bits), selector); - - let (sum, carry) = x.addition_with_carry(y); - for (i, bit) in sum.bits.into_iter().enumerate() { - product.bits[rhs_size + i] = bit; - } - - Some(carry) - } else { - None - }; - - // Remove the current least significant bit corresponding to the RHS and shift - // everything down. - product.bits.pop_front(); - - // The carry bit should only be added if the next iteration would not result in a - // truncated addition. This is to ensure the number of product bits at the conclusion - // of this loop contains the expected number of output bits. - if max_sum_bits > self.len() { - product.bits.push_back(carry.unwrap()); - } - } - - product - } - - /// Computes the unsigned integer division of `dividend` / `self` and returns - /// `(quotient, remainder)`. - /// - /// # Division by zero - /// - /// Division by zero is undefined. It is the responsibility of the caller to ensure the divisor - /// is non-zero. - pub fn unsigned_divide(self, dividend: Self) -> (Self, Self) { - // Zero extend so self and rhs are the same length - let divisor = match dividend.len().saturating_sub(self.len()) { - 0 => self, - n => self.zero_extend(n), - }; - - let dividend = match divisor.len().saturating_sub(dividend.len()) { - 0 => dividend, - n => dividend.zero_extend(n), - }; - - let mut quotient = SymbolicBitVec::constant(0, dividend.len()); - let mut remainder = SymbolicBitVec::constant(0, dividend.len()); - - for next_bit in dividend.bits.into_iter().rev() { - remainder.bits.rotate_right(1); - remainder.bits[0] = next_bit; - - // Check if RHS is less than working set - let selector = remainder.clone().less_than(divisor.clone()); - let diff = remainder.clone() - divisor.clone(); - remainder.mux_mut(diff, selector.clone()); - - quotient.bits.rotate_right(1); - quotient.bits[0] = !selector; - } - - (quotient, remainder) - } - - pub fn signed_divide(self, dividend: Self) -> (Self, Self) { - let divisor_msb = self.msb().cloned().unwrap(); - let dividend_msb = dividend.msb().cloned().unwrap(); - - let mut unsigned_divisor = self.clone(); - unsigned_divisor.mux_mut(-self, !divisor_msb.clone()); - - let mut unsigned_dividend = dividend.clone(); - unsigned_dividend.mux_mut(-dividend, !dividend_msb.clone()); - - let (mut quotient, mut remainder) = unsigned_divisor.unsigned_divide(unsigned_dividend); - - let negated_quotient = -quotient.clone(); - quotient.mux_mut( - negated_quotient, - divisor_msb.clone().equals(dividend_msb.clone()), - ); - - let negated_remainder = -remainder.clone(); - remainder.mux_mut(negated_remainder, !dividend_msb); - - (quotient, remainder) - } - - pub fn addition_carry_bits(self, rhs: Self) -> Self { - assert_eq!(self.bits.len(), rhs.bits.len()); - let mut carry = VecDeque::with_capacity(self.bits.len() + 1); - carry.push_back(FALSE); - carry.push_back(self[0].clone() & rhs[0].clone()); - for i in 1..self.bits.len() { - carry.push_back( - (self[i].clone() & rhs[i].clone()) - | (self[i].clone() & carry[i].clone()) - | (rhs[i].clone() & carry[i].clone()), - ); - } - - Self { bits: carry } - } - - pub fn unsigned_addition_overflow(self, rhs: Self) -> SymbolicBit { - let len = self.len(); - let carry_bits = self.addition_carry_bits(rhs); - carry_bits[len].clone() - } - - pub fn signed_addition_overflow(self, rhs: Self) -> SymbolicBit { - let sum = self.clone() + rhs.clone(); - - // Positive overflow occurs if sign bit is 0 for LHS and RHS but 1 in sum - let positive_overflow = !self[self.len() - 1].clone() - & !rhs[rhs.len() - 1].clone() - & sum[sum.len() - 1].clone(); - - // Negative overflow occurs if sign bit is 1 for LHS and RHS but 0 in sum - let negative_overflow = - self[self.len() - 1].clone() & rhs[rhs.len() - 1].clone() & !sum[sum.len() - 1].clone(); - - // Overflow occurs if either positive or negative overflow occurs - positive_overflow | negative_overflow - } - - pub fn less_than(mut self, mut rhs: Self) -> SymbolicBit { - assert_eq!(self.len(), rhs.len()); - if self.is_empty() { - return FALSE; - } - - let lhs_msb = self.bits.pop_back().unwrap(); - let rhs_msb = rhs.bits.pop_back().unwrap(); - let less_than = lhs_msb.clone().equals(FALSE) & rhs_msb.clone().equals(TRUE); - - if self.bits.is_empty() { - less_than - } else { - less_than | (lhs_msb.equals(rhs_msb) & self.less_than(rhs)) - } - } - - pub fn less_than_eq(self, rhs: Self) -> SymbolicBit { - self.clone().less_than(rhs.clone()) | self.equals(rhs) - } - - pub fn greater_than(mut self, mut rhs: Self) -> SymbolicBit { - assert_eq!(self.len(), rhs.len()); - if self.is_empty() { - return FALSE; - } - - let lhs_msb = self.bits.pop_back().unwrap(); - let rhs_msb = rhs.bits.pop_back().unwrap(); - let greater_than = lhs_msb.clone().equals(TRUE) & rhs_msb.clone().equals(FALSE); - - if self.is_empty() { - greater_than - } else { - greater_than | (lhs_msb.equals(rhs_msb) & self.greater_than(rhs)) - } - } - - pub fn greater_than_eq(self, rhs: Self) -> SymbolicBit { - self.clone().greater_than(rhs.clone()) | self.equals(rhs) - } - - pub fn signed_less_than(self, rhs: Self) -> SymbolicBit { - assert_eq!(self.len(), rhs.len()); - if self.is_empty() { - return FALSE; - } - - let lhs_sign_bit = self.msb().cloned().unwrap(); - let rhs_sign_bit = rhs.msb().cloned().unwrap(); - let mixed_sign_case = - lhs_sign_bit.clone().equals(TRUE) & rhs_sign_bit.clone().equals(FALSE); - let same_sign_case = lhs_sign_bit.equals(rhs_sign_bit) & self.less_than(rhs); - - mixed_sign_case | same_sign_case - } - - pub fn signed_less_than_eq(self, rhs: Self) -> SymbolicBit { - self.clone().signed_less_than(rhs.clone()) | self.equals(rhs) - } - - pub fn signed_greater_than(self, rhs: Self) -> SymbolicBit { - assert_eq!(self.len(), rhs.len()); - let lhs_sign_bit = self[self.len() - 1].clone(); - let rhs_sign_bit = rhs[rhs.len() - 1].clone(); - let mixed_sign_case = - lhs_sign_bit.clone().equals(FALSE) & rhs_sign_bit.clone().equals(TRUE); - let same_sign_case = lhs_sign_bit.equals(rhs_sign_bit) & self.greater_than(rhs); - - mixed_sign_case | same_sign_case - } - - pub fn signed_greater_than_eq(self, rhs: Self) -> SymbolicBit { - self.clone().signed_greater_than(rhs.clone()) | self.equals(rhs) - } - - pub fn popcount(self) -> Self { - let len = if self.is_empty() { - // This special case is needed to avoid taking log2 of 0 - 1 - } else { - // ilog2 rounds down. If it rounds down, need to add 1. If it is a power of 2 then also - // need to add 1 to account for if all bits are set - self.len().ilog2() as usize + 1 - }; - - let mut result = SymbolicBitVec::constant(0, len); - for bit in self.bits.into_iter() { - let bit: SymbolicBitVec = bit.into(); - let bit = bit.zero_extend(len - 1); - result = result + bit; - } - result - } - - pub fn signed_shift_right(mut self, rhs: Self) -> Self { - let sign_bit = self.msb().cloned().unwrap(); - for (i, shift_bit) in rhs.into_iter().enumerate() { - let mut shifted_value = self.clone(); - shifted_value.shift_mut(1 << i, sign_bit.clone(), ShiftDirection::Right); - self.mux_mut(shifted_value, !shift_bit); - } - self - } - - fn shift_mut(&mut self, amount: usize, shift_in: SymbolicBit, direction: ShiftDirection) { - let len = self.len(); - - match direction { - ShiftDirection::Left => { - // [ 0 1 2 3 4 5 6 7 ] << 3 - // [ x x x 0 1 2 3 4 ] - for i in (amount..len).rev() { - self.bits.swap(i, i - amount); - } - for i in 0..usize::min(len, amount) { - self.bits[i] = shift_in.clone(); - } - } - ShiftDirection::Right => { - // [ 0 1 2 3 4 5 6 7 ] >> 3 - // [ 3 4 5 6 7 x x x ] - for i in amount..len { - self.bits.swap(i, i - amount); - } - for i in 0..usize::min(len, amount) { - self.bits[len - 1 - i] = shift_in.clone(); - } - } - } - } - - fn mux_mut(&mut self, rhs: Self, selector: SymbolicBit) { - rhs.bits.into_iter().enumerate().for_each(|(i, rhs)| { - let lhs = std::mem::take(&mut self.bits[i]); - self.bits[i] = selector.clone().select(lhs, rhs); - }); - } -} diff --git a/crates/sym/src/vec/convert.rs b/crates/sym/src/vec/convert.rs deleted file mode 100644 index e316f39..0000000 --- a/crates/sym/src/vec/convert.rs +++ /dev/null @@ -1,35 +0,0 @@ -use super::SymbolicBitVec; -use crate::bit::SymbolicBit; -use crate::buf::SymbolicByte; - -impl TryInto> for SymbolicBitVec { - type Error = String; - - fn try_into(self) -> Result, Self::Error> { - if self.bits.len().is_multiple_of(8) { - Ok(self.into_bytes()) - } else { - Err(format!( - "invalid number of bits: {len}", - len = self.bits.len() - )) - } - } -} - -impl IntoIterator for SymbolicBitVec { - type Item = SymbolicBit; - type IntoIter = std::collections::vec_deque::IntoIter; - - fn into_iter(self) -> Self::IntoIter { - self.bits.into_iter() - } -} - -impl FromIterator for SymbolicBitVec { - fn from_iter>(iter: T) -> Self { - Self { - bits: iter.into_iter().collect(), - } - } -} diff --git a/crates/sym/src/vec/ops.rs b/crates/sym/src/vec/ops.rs deleted file mode 100644 index 7a6e162..0000000 --- a/crates/sym/src/vec/ops.rs +++ /dev/null @@ -1,180 +0,0 @@ -use super::{ShiftDirection, SymbolicBitVec}; -use crate::bit::{FALSE, SymbolicBit}; - -impl std::ops::Index for SymbolicBitVec { - type Output = SymbolicBit; - - fn index(&self, index: usize) -> &Self::Output { - &self.bits[index] - } -} - -impl std::ops::Not for SymbolicBitVec { - type Output = Self; - - fn not(self) -> Self::Output { - Self { - bits: self.bits.into_iter().map(|bit| !bit).collect(), - } - } -} - -impl std::ops::BitAnd for SymbolicBitVec { - type Output = Self; - - fn bitand(self, rhs: Self) -> Self::Output { - assert_eq!(self.bits.len(), rhs.bits.len()); - Self { - bits: self - .bits - .into_iter() - .zip(rhs.bits) - .map(|(lhs, rhs)| lhs & rhs) - .collect(), - } - } -} - -impl std::ops::BitOr for SymbolicBitVec { - type Output = Self; - - fn bitor(self, rhs: Self) -> Self::Output { - assert_eq!(self.bits.len(), rhs.bits.len()); - Self { - bits: self - .bits - .into_iter() - .zip(rhs.bits) - .map(|(lhs, rhs)| lhs | rhs) - .collect(), - } - } -} - -impl std::ops::BitXor for SymbolicBitVec { - type Output = Self; - - fn bitxor(self, rhs: Self) -> Self::Output { - assert_eq!(self.bits.len(), rhs.bits.len()); - Self { - bits: self - .bits - .into_iter() - .zip(rhs.bits) - .map(|(lhs, rhs)| lhs ^ rhs) - .collect(), - } - } -} - -impl std::ops::Shl for SymbolicBitVec { - type Output = Self; - - fn shl(mut self, rhs: usize) -> Self::Output { - self <<= rhs; - self - } -} - -impl std::ops::Shl for SymbolicBitVec { - type Output = Self; - - fn shl(mut self, rhs: Self) -> Self::Output { - self <<= rhs; - self - } -} - -impl std::ops::ShlAssign for SymbolicBitVec { - fn shl_assign(&mut self, rhs: usize) { - self.shift_mut(rhs, FALSE, ShiftDirection::Left); - } -} - -impl std::ops::ShlAssign for SymbolicBitVec { - fn shl_assign(&mut self, rhs: Self) { - for (i, shift_bit) in rhs.bits.into_iter().enumerate() { - let mut shifted_value = self.clone(); - shifted_value.shift_mut(1 << i, FALSE, ShiftDirection::Left); - self.mux_mut(shifted_value, !shift_bit); - } - } -} - -/// Performs an _unsigned_ right shift. -impl std::ops::ShrAssign for SymbolicBitVec { - fn shr_assign(&mut self, rhs: Self) { - for (i, shift_bit) in rhs.bits.into_iter().enumerate() { - let mut shifted_value = self.clone(); - shifted_value.shift_mut(1 << i, FALSE, ShiftDirection::Right); - self.mux_mut(shifted_value, !shift_bit); - } - } -} - -impl std::ops::ShrAssign for SymbolicBitVec { - fn shr_assign(&mut self, rhs: usize) { - self.shift_mut(rhs, FALSE, ShiftDirection::Right); - } -} - -impl std::ops::Shr for SymbolicBitVec { - type Output = Self; - - fn shr(mut self, rhs: Self) -> Self::Output { - self >>= rhs; - self - } -} - -impl std::ops::Shr for SymbolicBitVec { - type Output = Self; - - fn shr(mut self, rhs: usize) -> Self::Output { - self >>= rhs; - self - } -} - -impl std::ops::Add for SymbolicBitVec { - type Output = Self; - - fn add(self, rhs: Self) -> Self::Output { - assert_eq!(self.bits.len(), rhs.bits.len()); - // The carry bit size is actually N+1 in order to track whether an overflow has occurred. - // The addition does not care about the overflow so remove this bit - let (sum, _) = self.addition_with_carry(rhs); - sum - } -} - -impl std::ops::Neg for SymbolicBitVec { - type Output = Self; - - fn neg(self) -> Self::Output { - let num_bits = self.bits.len(); - !self + SymbolicBitVec::constant(1, num_bits) - } -} - -impl std::ops::Sub for SymbolicBitVec { - type Output = Self; - - fn sub(self, rhs: Self) -> Self::Output { - assert_eq!(self.bits.len(), rhs.bits.len()); - self + (-rhs) - } -} - -impl std::ops::Mul for SymbolicBitVec { - type Output = Self; - - 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. https://github.com/rust-lang/rust-clippy/issues/16247 - #[allow(clippy::suspicious_arithmetic_impl)] - let output_size = self.len() + rhs.len(); - - self.multiply(rhs, output_size) - } -} diff --git a/crates/sympcode/Cargo.toml b/crates/sympcode/Cargo.toml index fe3a076..fb9eb23 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", features = ["aiger"] } +symbit = { version = "0.1", features = ["aiger"] } pcode-ops = { version = "0.1", path = "../pcode-ops/" }