change types module to conversion; move z3 conversion type to convers…

…ion module
WilfredTA · Jun 24, 2023 · 8e7ff11 · 8e7ff11
1 parent e7ca61d
commit 8e7ff11
Show file tree

Hide file tree

Showing 3 changed files with 44 additions and 41 deletions.
diff --git a/src/types/mod.rs → src/conversion/mod.rs b/src/types/mod.rs → 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<BitVec<32>> for Uint<256, 4> {
     }
 }
 
+impl<const SZ: u32> From<BV<'static>> for BitVec<SZ> {
+    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<const SZ: u32> From<BitVec<SZ>> for BV<'static> {
+    fn from(bv: BitVec<SZ>) -> Self {
+        match bv.inner {
+            BVType::Z3(bv) => bv,
+            _ => panic!("Should never happen"),
+        }
+    }
+}
+
+impl<const SZ: u32> AsRef<BV<'static>> for BitVec<SZ> {
+    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
@@ -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
@@ -24,46 +24,6 @@ impl<const SZ: u32> BitVec<SZ> {
         }
     }
 }
-impl<const SZ: u32> From<BV<'static>> for BitVec<SZ> {
-    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<const SZ: u32> From<BitVec<SZ>> for BV<'static> {
-    fn from(bv: BitVec<SZ>) -> Self {
-        match bv.inner {
-            BVType::Z3(bv) => bv,
-            _ => panic!("Should never happen"),
-        }
-    }
-}
-
-impl<const SZ: u32> AsRef<BV<'static>> for BitVec<SZ> {
-    fn as_ref(&self) -> &BV<'static> {
-        match &self.inner {
-            BVType::Z3(bv) => bv,
-            _ => panic!("Should never happen"),
-        }
-    }
-}
 
 impl<const SZ: u32> SymbolicValue<BV<'static>, u64> for BitVec<SZ> {
     fn new_literal(val: u64) -> Self {