Use ruint's Uint to convert to Bitvecs in parser instead of using u64

WilfredTA · Jun 25, 2023 · 484d388 · 484d388
1 parent fc2023c
commit 484d388
Show file tree

Hide file tree

Showing 14 changed files with 328 additions and 85 deletions.
diff --git a/src/conversion/mod.rs b/src/conversion/mod.rs
@@ -2,9 +2,9 @@ use std::cmp::Ordering;
 
 use ruint::{uint, Uint, ToUintError, FromUintError, Bits};
 use rlp::{Encodable, Decodable};
-use z3_ext::ast::Ast;
+use z3_ext::{ast::Ast, Context};
 use serde::{Deserialize, Serialize};
-use crate::{BV, BVType, BitVec, bvc, bvi, ctx, bvi_8byte};
+use crate::{BV, BVType, BitVec, bvc, bvi, ctx, bvi_8byte, parser::zero_extend, record::push, instruction::{push32, Instruction}};
 
 impl From<Uint<256, 4>> for BitVec<32> {
     fn from(value: Uint<256, 4>) -> Self {
@@ -39,14 +39,14 @@ impl From<BitVec<32>> for Uint<256, 4> {
     }
 }
 
-impl<const SZ: u32> From<BV<'static>> for BitVec<SZ> {
+impl<const SZ: usize> 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),
+        let bv = match bvsz.cmp(&(bit_sz as u32)) {
+            Ordering::Less => bv.zero_ext((bit_sz - bvsz as usize) as u32),
             Ordering::Equal => bv,
-            Ordering::Greater => bv.extract(bit_sz, 0),
+            Ordering::Greater => bv.extract(bit_sz as u32, 0),
         };
         // let bv = if bvsz < bit_sz {
         //     bv.zero_ext(bit_sz - bvsz)
@@ -62,7 +62,7 @@ impl<const SZ: u32> From<BV<'static>> for BitVec<SZ> {
     }
 }
 
-impl<const SZ: u32> From<BitVec<SZ>> for BV<'static> {
+impl<const SZ: usize> From<BitVec<SZ>> for BV<'static> {
     fn from(bv: BitVec<SZ>) -> Self {
         match bv.inner {
             BVType::Z3(bv) => bv,
@@ -71,7 +71,24 @@ impl<const SZ: u32> From<BitVec<SZ>> for BV<'static> {
     }
 }
 
-impl<const SZ: u32> AsRef<BV<'static>> for BitVec<SZ> {
+impl<const SZ: usize> From<[u8; SZ]> for BitVec<SZ> {
+    fn from(value: [u8; SZ]) -> Self {
+        let ctx: &'static Context = ctx();
+        let mut bv:  BV<'static> = BV::from_u64(ctx, 0, 8);
+
+
+       for i in value.iter() {
+           let new_bv: BV<'static> = bvi::<1>(*i).into();
+            bv = bv.concat(&new_bv).simplify();
+
+       }
+       eprintln!("VALUE CONVERTING FROM: {:#x?}", value);
+       eprintln!("BV IN SLICE CONVERT: {:#?} SIZE: {}", bv, bv.get_size());
+       bv.extract((bv.get_size() - 8 - 1) as u32, 0).simplify().into()
+    }
+}
+
+impl<const SZ: usize> AsRef<BV<'static>> for BitVec<SZ> {
     fn as_ref(&self) -> &BV<'static> {
         match &self.inner {
             BVType::Z3(bv) => bv,
@@ -80,6 +97,28 @@ impl<const SZ: u32> AsRef<BV<'static>> for BitVec<SZ> {
     }
 }
 
+#[cfg(test)]
+fn push_arg_to_push(arg: &[u8]) -> Instruction {
+    let slice_full = zero_extend::<32>(&arg).into();
+    push32(slice_full)
+}
+
+#[test]
+fn test_slice_to_op_arg() {
+    let mut slice8 = 327000_u64.to_be_bytes();
+    let inst = push_arg_to_push(&slice8);
+}
+#[test]
+fn test_slice_to_bitvec() {
+    let mut slice8 = 327000_u64.to_be_bytes();
+
+    let slice_full = zero_extend::<32>(&slice8);
+    let bv: BitVec<32> = slice_full.into();
+
+    let num = uint!(0x000000000000000000000000000000000000000000000000000000000004FD58_U256);
+    let bv_as_num: Uint<256,4> = bv.into();
+    assert_eq!(num, bv_as_num);
+}
 
 #[test]
 fn test_u256_to_bytes() {
@@ -89,7 +128,7 @@ fn test_u256_to_bytes() {
 
     let bytes: [u8; 32] = num.to_be_bytes();
 
-    let numbit: Bits<256, 4 >= Bits::from_be_bytes(bytes);
+    let numbit: Bits<256, 4> = Bits::from_be_bytes(bytes);
     let newnum: Uint<256, 4> = numbit.as_uint().clone();
     assert_eq!(num, newnum);
 }

diff --git a/src/instruction/mod.rs b/src/instruction/mod.rs
@@ -603,7 +603,7 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
             Instruction::CallValue => {
                 let stack = mach.stack();
                 let call_val = call_value().apply(&[]).as_bv().unwrap();
-                let stack_diff = StackChange::with_ops(vec![pop(), push(call_val.into())]);
+                let stack_diff = StackChange::with_ops(vec![push(call_val.into())]);
 
                 MachineRecord {
                     stack: Some(stack_diff),
@@ -1448,7 +1448,16 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
             Instruction::DelegateCall => todo!(),
             Instruction::Create2 => todo!(),
             Instruction::StaticCall => todo!(),
-            Instruction::Revert => todo!(),
+            Instruction::Revert => {
+                MachineRecord {
+                    mem: None,
+                    stack: None,
+                    storage: None,
+                    pc: (mach.pc(), mach.pc()),
+                    constraints: None,
+                    halt: true,
+                }
+            },
             Instruction::Invalid => todo!(),
             Instruction::SelfDestruct => todo!(),
             Instruction::SignExtend => todo!(),
@@ -1491,7 +1500,7 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
     }
 }
 
-pub fn pop<const SZ: u32>() -> StackOp<SZ> {
+pub fn pop<const SZ: usize>() -> StackOp<SZ> {
     StackOp::Pop
 }
 pub fn add() -> Instruction {
@@ -1553,7 +1562,7 @@ pub fn dup15() -> Instruction {
 pub fn dup16() -> Instruction {
     Instruction::Dup16
 }
-// pub fn push<const SZ: u32>(size: usize, val: BitVec<>) -> Instruction {
+// pub fn push<const SZ: usize>(size: usize, val: BitVec<>) -> Instruction {
 //     Instruction::Push5(BitVec::default())
 // }
 

diff --git a/src/lib.rs b/src/lib.rs
@@ -23,7 +23,7 @@ use z3_ext::{
 use rand::Rng;
 
 
-pub fn bvi<const SZ: u32>(val: impl Into<i32>) -> BitVec<SZ> {
+pub fn bvi<const SZ: usize>(val: impl Into<i32>) -> BitVec<SZ> {
     BitVec::new_literal(val.into() as u64)
 }
 
@@ -37,7 +37,7 @@ pub fn bvi_8byte(val: u64) -> BitVec<8> {
 pub fn bvc(val: impl AsRef<str>) -> BitVec<32> {
     BitVec::new_const(val)
 }
-pub fn random_bv_arg<const SZ: u32>() -> BitVec<SZ> {
+pub fn random_bv_arg<const SZ: usize>() -> BitVec<SZ> {
     let mut rng = rand::thread_rng();
     let rand_num: u64 = rng.gen();
     BitVec::new_literal(rand_num)
@@ -51,4 +51,5 @@ mod test {
      */
     pub const SIMPLE_COUNTER: &str = r"6080604052348015600f57600080fd5b5060043610603c5760003560e01c80633fb5c1cb1460415780638381f58a146053578063d09de08a14606d575b600080fd5b6051604c3660046083565b600055565b005b605b60005481565b60405190815260200160405180910390f35b6051600080549080607c83609b565b9190505550565b600060208284031215609457600080fd5b5035919050565b60006001820160ba57634e487b7160e01b600052601160045260246000fd5b506001019056fea2646970667358221220f0cfb2159c518c3da0ad864362bad5dc0715514a9ab679237253d506773a0a1b64736f6c63430008130033";
     pub const COUNTER_WITH_STORAGE_MAPPING: &str = r#"608060405234801561001057600080fd5b5060056000806001815260200190815260200160002081905550610197806100396000396000f3fe608060405234801561001057600080fd5b50600436106100365760003560e01c8063846719e01461003b578063d78233d61461006b575b600080fd5b6100556004803603810190610050919061010a565b61009b565b6040516100629190610146565b60405180910390f35b6100856004803603810190610080919061010a565b6100b7565b6040516100929190610146565b60405180910390f35b6000806000838152602001908152602001600020549050919050565b60006020528060005260406000206000915090505481565b600080fd5b6000819050919050565b6100e7816100d4565b81146100f257600080fd5b50565b600081359050610104816100de565b92915050565b6000602082840312156101205761011f6100cf565b5b600061012e848285016100f5565b91505092915050565b610140816100d4565b82525050565b600060208201905061015b6000830184610137565b9291505056fea2646970667358fe122066b287fef10118cba238fe38953bfefe938afefefefefe94fefe3682fefefefe64736f6c63430008110033"#;
+
 }
diff --git a/src/machine.rs b/src/machine.rs
@@ -124,7 +124,7 @@ impl<'ctx> Evm<'ctx> {
         }
     }
 
-    fn exec_check(&mut self) -> Vec<(ExecBranch, Option<Model<'ctx>>)> {
+    pub fn exec_check(&mut self) -> Vec<(ExecBranch, Option<Model<'ctx>>)> {
         let evm_trace = self.exec();
         let mut solver = z3_ext::Solver::new(ctx());
         evm_trace

diff --git a/src/memory.rs b/src/memory.rs
@@ -17,10 +17,16 @@ impl MachineComponent for Memory {
     type Record = MemChange;
 
     fn apply_change(&mut self, rec: Self::Record) {
+
         let MemChange { ops_log } = rec;
         let mut highest_idx = self.highest_idx;
         ops_log.into_iter().for_each(|op| match op {
             MemOp::Write { val, idx } => {
+                let mut val = val;
+                val.simplify();
+                let mut idx = idx;
+                idx.simplify();
+                eprintln!("MEM WRITE FOR MEM APPLY: idx: {:#?}, value: {:#?}", idx, val);
                 let idx_cmp: usize = idx.clone().into();
                 if idx_cmp > highest_idx {
                     highest_idx = idx_cmp;