diff --git a/src/types/mod.rs b/src/conversion/mod.rs similarity index 66% rename from src/types/mod.rs rename to src/conversion/mod.rs index 7e63a04..599b0bb 100644 --- a/src/types/mod.rs +++ b/src/conversion/mod.rs @@ -1,3 +1,5 @@ +use std::cmp::Ordering; + use ruint::{uint, Uint, ToUintError, FromUintError, Bits}; use rlp::{Encodable, Decodable}; use z3_ext::ast::Ast; @@ -37,6 +39,47 @@ impl From> for Uint<256, 4> { } } +impl From> for BitVec { + fn from(bv: BV<'static>) -> Self { + let bit_sz = SZ * 8; + let bvsz = bv.get_size(); + let bv = match bvsz.cmp(&bit_sz) { + Ordering::Less => bv.zero_ext(bit_sz - bvsz), + Ordering::Equal => bv, + Ordering::Greater => bv.extract(bit_sz, 0), + }; + // let bv = if bvsz < bit_sz { + // bv.zero_ext(bit_sz - bvsz) + // } else if bvsz > bit_sz { + // bv.extract(bit_sz, 0) + // } else { + // bv + // }; + Self { + inner: BVType::Z3(bv), + typ: Default::default(), + } + } +} + +impl From> for BV<'static> { + fn from(bv: BitVec) -> Self { + match bv.inner { + BVType::Z3(bv) => bv, + _ => panic!("Should never happen"), + } + } +} + +impl AsRef> for BitVec { + fn as_ref(&self) -> &BV<'static> { + match &self.inner { + BVType::Z3(bv) => bv, + _ => panic!("Should never happen"), + } + } +} + #[test] fn test_u256_to_bytes() { diff --git a/src/lib.rs b/src/lib.rs index 652231d..35f3963 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -9,7 +9,7 @@ pub mod smt; pub mod stack; pub mod state; pub mod traits; -pub mod types; +pub mod conversion; pub mod storage; pub mod parser; use paste::{expr, item, paste}; diff --git a/src/smt/bitvec/z3.rs b/src/smt/bitvec/z3.rs index 5db08e9..c6bf6ba 100644 --- a/src/smt/bitvec/z3.rs +++ b/src/smt/bitvec/z3.rs @@ -24,46 +24,6 @@ impl BitVec { } } } -impl From> for BitVec { - fn from(bv: BV<'static>) -> Self { - let bit_sz = SZ * 8; - let bvsz = bv.get_size(); - let bv = match bvsz.cmp(&bit_sz) { - Ordering::Less => bv.zero_ext(bit_sz - bvsz), - Ordering::Equal => bv, - Ordering::Greater => bv.extract(bit_sz, 0), - }; - // let bv = if bvsz < bit_sz { - // bv.zero_ext(bit_sz - bvsz) - // } else if bvsz > bit_sz { - // bv.extract(bit_sz, 0) - // } else { - // bv - // }; - Self { - inner: BVType::Z3(bv), - typ: Default::default(), - } - } -} - -impl From> for BV<'static> { - fn from(bv: BitVec) -> Self { - match bv.inner { - BVType::Z3(bv) => bv, - _ => panic!("Should never happen"), - } - } -} - -impl AsRef> for BitVec { - fn as_ref(&self) -> &BV<'static> { - match &self.inner { - BVType::Z3(bv) => bv, - _ => panic!("Should never happen"), - } - } -} impl SymbolicValue, u64> for BitVec { fn new_literal(val: u64) -> Self {