diff --git a/src/btor2/witness.rs b/src/btor2/witness.rs index bb48c94..6f639d1 100644 --- a/src/btor2/witness.rs +++ b/src/btor2/witness.rs @@ -5,7 +5,7 @@ use crate::btor2::parse::tokenize_line; use crate::ir; use crate::ir::{SignalKind, TypeCheck}; -use crate::sim::{Value, ValueStore, Witness}; +use crate::sim::{ScalarValue, ValueStore, Witness}; use std::io::{BufRead, Write}; enum ParserState { @@ -133,7 +133,7 @@ pub fn parse_witnesses(input: &mut impl BufRead, parse_max: usize) -> Result(tokens: &'a [&'a str]) -> (u64, &'a str, Value, Option) { +fn parse_assignment<'a>(tokens: &'a [&'a str]) -> (u64, &'a str, ScalarValue, Option) { let is_array = match tokens.len() { 3 => false, // its a bit vector 4 => true, @@ -148,10 +148,10 @@ fn parse_assignment<'a>(tokens: &'a [&'a str]) -> (u64, &'a str, Value, Option Result { +fn get_smt_value(smt_ctx: &mut smt::Context, expr: smt::SExpr) -> Result { let smt_value = smt_ctx.get_value(vec![expr])?[0].1; let atom = smt_ctx.get(smt_value); match atom { @@ -190,17 +190,17 @@ fn get_smt_value(smt_ctx: &mut smt::Context, expr: smt::SExpr) -> Result } } -fn smt_bit_vec_str_to_value(a: &str) -> Value { +fn smt_bit_vec_str_to_value(a: &str) -> ScalarValue { if let Some(suffix) = a.strip_prefix("#b") { - Value::from_bit_string(suffix) + ScalarValue::from_bit_string(suffix) } else if let Some(suffix) = a.strip_prefix("#x") { - Value::from_hex_string(suffix) + ScalarValue::from_hex_string(suffix) } else if a == "true" { - Value::Long(1) + ScalarValue::Long(1) } else if a == "false" { - Value::Long(0) + ScalarValue::Long(0) } else { - Value::from_decimal_string(a) + ScalarValue::from_decimal_string(a) } } diff --git a/src/sim/interpreter.rs b/src/sim/interpreter.rs index adffb7a..985f728 100644 --- a/src/sim/interpreter.rs +++ b/src/sim/interpreter.rs @@ -3,7 +3,7 @@ // author: Kevin Laeufer use crate::ir::*; -use crate::sim::{Value, ValueStore}; +use crate::sim::{ScalarValue, ValueStore}; /// Specifies how to initialize states that do not have #[derive(Debug, PartialEq, Copy, Clone)] @@ -20,7 +20,7 @@ pub trait Simulator { fn step(&mut self); /// Change the value of an input - fn set_input(&mut self, input_id: usize, value: Value); + fn set_input(&mut self, input_id: usize, value: ScalarValue); } /// Interpreter based simulator for a transition system. @@ -66,7 +66,7 @@ impl<'a> Simulator for Interpreter<'a> { todo!() } - fn set_input(&mut self, input_id: usize, value: Value) { + fn set_input(&mut self, input_id: usize, value: ScalarValue) { todo!() } } diff --git a/src/sim/mod.rs b/src/sim/mod.rs index c439c63..64fc130 100644 --- a/src/sim/mod.rs +++ b/src/sim/mod.rs @@ -7,4 +7,4 @@ mod values; // author: Kevin Laeufer pub mod interpreter; -pub use values::{Value, ValueRef, ValueStore, Witness}; +pub use values::{ScalarValue, ScalarValueRef, ValueStore, Witness}; diff --git a/src/sim/values.rs b/src/sim/values.rs index 626b251..5409361 100644 --- a/src/sim/values.rs +++ b/src/sim/values.rs @@ -4,7 +4,8 @@ use crate::ir::{Type, WidthInt}; use num_bigint::BigUint; -use num_traits::{Num, Zero}; +use num_traits::{Num, ToPrimitive, Zero}; +use std::fmt::Debug; /// Contains the initial state and the inputs over `len` cycles. #[derive(Debug, Default)] @@ -98,40 +99,40 @@ impl ValueStore { state } - pub fn get(&self, index: usize) -> Option { + pub fn get(&self, index: usize) -> Option { let meta = self.meta.get(index)?.as_ref()?; self.get_from_meta(meta) } - fn get_from_meta(&self, meta: &StorageMetaData) -> Option { + fn get_from_meta(&self, meta: &StorageMetaData) -> Option { if !meta.is_valid { return None; } - let res: ValueRef = match meta.tpe { - StorageType::Long => ValueRef::Long(self.longs[meta.index as usize]), - StorageType::Big => ValueRef::Big(&self.bigs[meta.index as usize]), + let res: ScalarValueRef = match meta.tpe { + StorageType::Long => ScalarValueRef::Long(self.longs[meta.index as usize]), + StorageType::Big => ScalarValueRef::Big(&self.bigs[meta.index as usize]), }; Some(res) } - pub fn update(&mut self, index: usize, value: Value) { + pub fn update(&mut self, index: usize, value: ScalarValue) { let meta = self.meta.get_mut(index).unwrap().as_mut().unwrap(); meta.is_valid = true; match (meta.tpe, value) { - (StorageType::Long, Value::Long(value)) => { + (StorageType::Long, ScalarValue::Long(value)) => { self.longs[meta.index as usize] = value; } - (StorageType::Big, Value::Big(value)) => { + (StorageType::Big, ScalarValue::Big(value)) => { self.bigs[meta.index as usize] = value; } - (StorageType::Big, Value::Long(value)) => { + (StorageType::Big, ScalarValue::Long(value)) => { self.bigs[meta.index as usize] = BigUint::from(value); } _ => panic!("Incompatible value for storage type: {:?}", meta.tpe), }; } - pub fn insert(&mut self, index: usize, value: Value) { + pub fn insert(&mut self, index: usize, value: ScalarValue) { match self.meta.get(index) { Some(_) => self.update(index, value), None => { @@ -143,13 +144,13 @@ impl ValueStore { }; } - fn allocate_for_value(&mut self, value: Value) -> StorageMetaData { + fn allocate_for_value(&mut self, value: ScalarValue) -> StorageMetaData { let (tpe, index) = match value { - Value::Long(val) => { + ScalarValue::Long(val) => { self.longs.push(val); (StorageType::Long, self.longs.len() - 1) } - Value::Big(val) => { + ScalarValue::Big(val) => { self.bigs.push(val); (StorageType::Big, self.bigs.len() - 1) } @@ -183,7 +184,7 @@ impl<'a> ValueStoreIter<'a> { } impl<'a> Iterator for ValueStoreIter<'a> { - type Item = Option>; + type Item = Option>; fn next(&mut self) -> Option { match self.underlying.next() { @@ -194,49 +195,49 @@ impl<'a> Iterator for ValueStoreIter<'a> { } } -#[derive(Debug, PartialEq, Clone)] -pub enum Value { +#[derive(Debug)] +pub enum ScalarValue { Long(u64), Big(BigUint), } -impl Value { +impl ScalarValue { /// parses a string of 1s and 0s into a value. pub fn from_bit_string(value: &str) -> Self { if value.len() <= 64 { - Value::Long(u64::from_str_radix(value, 2).unwrap()) + ScalarValue::Long(u64::from_str_radix(value, 2).unwrap()) } else { - Value::Big(BigUint::from_str_radix(value, 2).unwrap()) + ScalarValue::Big(BigUint::from_str_radix(value, 2).unwrap()) } } pub fn from_hex_string(value: &str) -> Self { if value.len() <= (64 / 4) { - Value::Long(u64::from_str_radix(value, 16).unwrap()) + ScalarValue::Long(u64::from_str_radix(value, 16).unwrap()) } else { - Value::Big(BigUint::from_str_radix(value, 16).unwrap()) + ScalarValue::Big(BigUint::from_str_radix(value, 16).unwrap()) } } pub fn from_decimal_string(value: &str) -> Self { match u64::from_str_radix(value, 10) { - Ok(value) => Value::Long(value), - Err(_) => Value::Big(BigUint::from_str_radix(value, 10).unwrap()), + Ok(value) => ScalarValue::Long(value), + Err(_) => ScalarValue::Big(BigUint::from_str_radix(value, 10).unwrap()), } } pub fn is_zero(&self) -> bool { match &self { - Value::Long(value) => *value == 0, - Value::Big(value) => value.is_zero(), + ScalarValue::Long(value) => *value == 0, + ScalarValue::Big(value) => value.is_zero(), } } /// Returns the value as a fixed with bit string. Returns None if the value is an array. pub fn to_bit_string(&self, width: WidthInt) -> Option { let base_str = match &self { - Value::Long(value) => format!("{value:b}"), - Value::Big(value) => value.to_str_radix(2), + ScalarValue::Long(value) => format!("{value:b}"), + ScalarValue::Big(value) => value.to_str_radix(2), }; let base_len = base_str.len(); if base_len == width as usize { @@ -253,23 +254,23 @@ impl Value { } #[derive(Debug, PartialEq)] -pub enum ValueRef<'a> { +pub enum ScalarValueRef<'a> { Long(u64), Big(&'a BigUint), } -impl<'a> ValueRef<'a> { - pub fn cloned(&self) -> Value { +impl<'a> ScalarValueRef<'a> { + pub fn cloned(&self) -> ScalarValue { match self { - ValueRef::Long(value) => Value::Long(*value), - ValueRef::Big(value) => Value::Big((*value).clone()), + ScalarValueRef::Long(value) => ScalarValue::Long(*value), + ScalarValueRef::Big(value) => ScalarValue::Big((*value).clone()), } } pub fn is_zero(&self) -> bool { match self { - ValueRef::Long(value) => *value == 0, - ValueRef::Big(value) => value.is_zero(), + ScalarValueRef::Long(value) => *value == 0, + ScalarValueRef::Big(value) => value.is_zero(), } } @@ -279,6 +280,97 @@ impl<'a> ValueRef<'a> { } } +pub trait TryFromValue: Sized { + // TODO: investigate using std::convert::TryFrom instead! + fn try_from(value: ScalarValue) -> Option; +} + +impl TryFromValue for u64 { + fn try_from(value: ScalarValue) -> Option { + match value { + ScalarValue::Long(v) => Some(v), + ScalarValue::Big(v) => v.to_u64(), + } + } +} + +impl TryFromValue for BigUint { + fn try_from(value: ScalarValue) -> Option { + match value { + ScalarValue::Long(v) => Some(BigUint::from(v)), + ScalarValue::Big(v) => Some(v), + } + } +} + +pub trait IntoValueRef: Sized { + // TODO: investigate using std::convert::Into instead! + fn into(&self) -> ScalarValueRef<'_>; +} + +impl IntoValueRef for u64 { + fn into(&self) -> ScalarValueRef<'_> { + ScalarValueRef::Long(*self) + } +} + +impl IntoValueRef for BigUint { + fn into(&self) -> ScalarValueRef<'_> { + ScalarValueRef::Big(self) + } +} + +pub trait ArrayValue: Debug { + fn update(&mut self, index: ScalarValue, value: ScalarValue); + fn get(&self, index: ScalarValue) -> ScalarValueRef; +} + +#[derive(Debug, PartialEq)] +pub struct SparseArrayValue +where + I: PartialEq + TryFromValue + Debug, + D: TryFromValue + IntoValueRef + Debug, +{ + default: D, + updates: Vec<(I, D)>, +} + +impl SparseArrayValue +where + I: PartialEq + TryFromValue + Debug, + D: TryFromValue + IntoValueRef + Debug, +{ + fn new(default: D) -> Self { + Self { + default, + updates: Vec::new(), + } + } +} + +impl ArrayValue for SparseArrayValue +where + I: PartialEq + TryFromValue + Debug, + D: TryFromValue + IntoValueRef + Debug, +{ + fn update(&mut self, index: ScalarValue, value: ScalarValue) { + self.updates + .push((I::try_from(index).unwrap(), D::try_from(value).unwrap())); + } + + fn get(&self, index: ScalarValue) -> ScalarValueRef { + // find the latest update + let raw_index = I::try_from(index).unwrap(); + for (ii, dd) in self.updates.iter().rev() { + if *ii == raw_index { + return dd.into(); + } + } + // no update found + (&self.default).into() + } +} + #[cfg(test)] mod tests { use super::*; @@ -289,7 +381,7 @@ mod tests { assert_eq!(std::mem::size_of::(), 24); // Not sure how we are fitting that, but it's nice that Value is no bigger than a BigUInt - assert_eq!(std::mem::size_of::(), 24); + assert_eq!(std::mem::size_of::(), 24); // We store 4 bytes of meta-data for every item in the storage assert_eq!(std::mem::size_of::(), 4);