From 61a1dee2f891f5ec1a1ae51d8e8cebaeda20c16b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kevin=20L=C3=A4ufer?= Date: Tue, 14 Nov 2023 11:09:15 -0500 Subject: [PATCH] wip: create data structure to hold state or inputs --- Cargo.toml | 1 - src/btor2/mod.rs | 1 + src/btor2/witness.rs | 5 ++ src/lib.rs | 1 + src/mc/mod.rs | 4 ++ src/mc/state.rs | 161 +++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 172 insertions(+), 1 deletion(-) create mode 100644 src/btor2/witness.rs create mode 100644 src/mc/mod.rs create mode 100644 src/mc/state.rs diff --git a/Cargo.toml b/Cargo.toml index 84acc7f..fe1ac0f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -25,4 +25,3 @@ insta = { version = "1.34.0", features = ["yaml"] } [profile.dev.package] insta.opt-level = 3 -similar.opt-level = 3 diff --git a/src/btor2/mod.rs b/src/btor2/mod.rs index 8a3928a..2ea035f 100644 --- a/src/btor2/mod.rs +++ b/src/btor2/mod.rs @@ -3,6 +3,7 @@ // author: Kevin Laeufer mod parse; mod serialize; +mod witness; pub use parse::{parse_file, parse_str}; pub use serialize::{serialize, serialize_to_str}; diff --git a/src/btor2/witness.rs b/src/btor2/witness.rs new file mode 100644 index 0000000..5d56dc7 --- /dev/null +++ b/src/btor2/witness.rs @@ -0,0 +1,5 @@ +// Copyright 2023 The Regents of the University of California +// released under BSD 3-Clause License +// author: Kevin Laeufer + +pub fn parse_witness() {} diff --git a/src/lib.rs b/src/lib.rs index 1d4558c..4608004 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -6,3 +6,4 @@ extern crate lazy_static; pub mod btor2; pub mod ir; +mod mc; diff --git a/src/mc/mod.rs b/src/mc/mod.rs new file mode 100644 index 0000000..ba97079 --- /dev/null +++ b/src/mc/mod.rs @@ -0,0 +1,4 @@ +// Copyright 2023 The Regents of the University of California +// released under BSD 3-Clause License +// author: Kevin Laeufer +mod state; diff --git a/src/mc/state.rs b/src/mc/state.rs new file mode 100644 index 0000000..d45a0d2 --- /dev/null +++ b/src/mc/state.rs @@ -0,0 +1,161 @@ +// Copyright 2023 The Regents of the University of California +// released under BSD 3-Clause License +// author: Kevin Laeufer + +use crate::ir::Type; +use num_bigint::BigUint; + +/// Contains the initial state and the inputs over `len` cycles. +pub struct Witness { + /// The starting state. Contains an optional value for each state. + init: State, + /// The inputs over time. Each entry contains an optional value for each input. + inputs: Vec, +} + +impl Witness { + pub fn len(&self) -> usize { + self.inputs.len() + } +} + +#[derive(Debug, PartialEq, Eq, Clone, Copy)] +enum StorageType { + Long, + Big, +} + +#[derive(Debug, PartialEq, Eq, Clone, Copy)] +struct StorageMetaData { + /// Indicates in what format the data is stored. + tpe: StorageType, + /// Index into the storage type specific array. + index: u16, + /// Indicates whether the store contains valid data. A `get` will return `None` for invalid data. + is_valid: bool, +} + +fn smt_tpe_to_storage_tpe(tpe: Type) -> StorageType { + match tpe { + Type::BV(len) if len <= 64 => StorageType::Long, + Type::BV(_) => StorageType::Big, + Type::Array(_) => todo!("add array support"), + } +} + +/// Represents concrete values which can be updated, but state cannot be added once created. +pub struct State { + meta: Vec, + longs: Vec, + bigs: Vec, + // TODO: add array support + //arrays: Vec, +} + +impl Default for State { + fn default() -> Self { + State { + meta: Vec::default(), + longs: Vec::default(), + bigs: Vec::default(), + } + } +} + +impl State { + pub fn new(types: impl Iterator) -> Self { + let mut state = State::default(); + let mut long_count = 0; + let mut big_count = 0; + for tpe in types { + let storage_tpe = smt_tpe_to_storage_tpe(tpe); + let index = match storage_tpe { + StorageType::Long => { + long_count += 1; + long_count - 1 + } + StorageType::Big => { + big_count += 1; + big_count - 1 + } + }; + let meta = StorageMetaData { + tpe: storage_tpe, + index: index as u16, + is_valid: false, + }; + state.meta.push(meta); + } + // initialize arrays with default data + state.longs.resize(long_count, u64::default()); + state.bigs.resize(big_count, BigUint::default()); + + state + } + + pub fn get(&self, index: usize) -> Option { + let meta = self.meta.get(index)?; + 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]), + }; + Some(res) + } + + pub fn update(&mut self, index: usize, value: Value) { + let meta = self.meta.get(index).unwrap(); + match (meta.tpe, value) { + (StorageType::Long, Value::Long(value)) => { + self.longs[meta.index as usize] = value; + } + (StorageType::Big, Value::Big(value)) => { + self.bigs[meta.index as usize] = value; + } + (StorageType::Big, Value::Long(value)) => { + self.bigs[meta.index as usize] = BigUint::from(value); + } + _ => panic!("Incompatible value for storage type: {:?}", meta.tpe), + }; + } +} + +#[derive(Debug, PartialEq, Clone)] +pub enum Value { + Long(u64), + Big(BigUint), +} + +#[derive(Debug, PartialEq)] +pub enum ValueRef<'a> { + Long(u64), + Big(&'a BigUint), +} + +impl<'a> ValueRef<'a> { + fn cloned(&self) -> Value { + match self { + ValueRef::Long(value) => Value::Long(*value), + ValueRef::Big(value) => Value::Big((*value).clone()), + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn ir_type_size() { + // External BigUInt + 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); + + // We store 4 bytes of meta-data for every item in the storage + assert_eq!(std::mem::size_of::(), 4); + } +}