From 484d388799843f6a9429d98f69d1226ad54a9022 Mon Sep 17 00:00:00 2001 From: tannr Date: Sat, 24 Jun 2023 20:58:45 -0400 Subject: [PATCH] Use ruint's Uint to convert to Bitvecs in parser instead of using u64 --- src/conversion/mod.rs | 57 ++++++++-- src/instruction/mod.rs | 17 ++- src/lib.rs | 5 +- src/machine.rs | 2 +- src/memory.rs | 6 ++ src/parser.rs | 231 +++++++++++++++++++++++++++++++++-------- src/record.rs | 11 +- src/smt/bitvec/mod.rs | 14 +-- src/smt/bitvec/z3.rs | 13 +-- src/stack.rs | 7 +- src/state/evm.rs | 4 + src/traits.rs | 6 +- tests/lib.rs | 40 +++++++ tests/test_storage.rs | 0 14 files changed, 328 insertions(+), 85 deletions(-) create mode 100644 tests/lib.rs create mode 100644 tests/test_storage.rs diff --git a/src/conversion/mod.rs b/src/conversion/mod.rs index 599b0bb..5d058d5 100644 --- 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> for BitVec<32> { fn from(value: Uint<256, 4>) -> Self { @@ -39,14 +39,14 @@ impl From> for Uint<256, 4> { } } -impl From> for 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), + 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 From> for BitVec { } } -impl From> for BV<'static> { +impl From> for BV<'static> { fn from(bv: BitVec) -> Self { match bv.inner { BVType::Z3(bv) => bv, @@ -71,7 +71,24 @@ impl From> for BV<'static> { } } -impl AsRef> for BitVec { +impl From<[u8; SZ]> for BitVec { + 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 AsRef> for BitVec { fn as_ref(&self) -> &BV<'static> { match &self.inner { BVType::Z3(bv) => bv, @@ -80,6 +97,28 @@ impl AsRef> for BitVec { } } +#[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 index cde26cf..2305d8b 100644 --- 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() -> StackOp { +pub fn pop() -> StackOp { StackOp::Pop } pub fn add() -> Instruction { @@ -1553,7 +1562,7 @@ pub fn dup15() -> Instruction { pub fn dup16() -> Instruction { Instruction::Dup16 } -// pub fn push(size: usize, val: BitVec<>) -> Instruction { +// pub fn push(size: usize, val: BitVec<>) -> Instruction { // Instruction::Push5(BitVec::default()) // } diff --git a/src/lib.rs b/src/lib.rs index 35f3963..662293d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -23,7 +23,7 @@ use z3_ext::{ use rand::Rng; -pub fn bvi(val: impl Into) -> BitVec { +pub fn bvi(val: impl Into) -> BitVec { 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) -> BitVec<32> { BitVec::new_const(val) } -pub fn random_bv_arg() -> BitVec { +pub fn random_bv_arg() -> BitVec { 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"#; + } \ No newline at end of file diff --git a/src/machine.rs b/src/machine.rs index 63a8988..8855eda 100644 --- a/src/machine.rs +++ b/src/machine.rs @@ -124,7 +124,7 @@ impl<'ctx> Evm<'ctx> { } } - fn exec_check(&mut self) -> Vec<(ExecBranch, Option>)> { + pub fn exec_check(&mut self) -> Vec<(ExecBranch, Option>)> { 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 index 29c1dad..b927d0b 100644 --- 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; diff --git a/src/parser.rs b/src/parser.rs index ec282a3..d9945a3 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -3,6 +3,7 @@ use revm::{ opcode::OpCode, OPCODE_JUMPMAP }; use hex::{decode}; +use ruint::Uint; pub struct Parser<'a> { pgm: &'a str } @@ -56,14 +57,27 @@ impl<'a> Parser<'a> { } // Returns instruction + any left over bytes in the slice after extracting the opcode & opcode args -fn parse_push(bytes: &[u8]) -> (Instruction, u8, &[u8]) { +fn parse_push(bytes: &[u8]) -> (Instruction, u8, Vec) { let instruction_byte = *bytes.first().unwrap(); let push_size = push_size(instruction_byte); eprintln!("PUSH SIZE IS {}", push_size); - let push_val = &bytes[1..(push_size + 1) as usize]; - eprintln!("PUSH VAL IS {:#?}", push_val); - (push_op(push_size, push_val),push_size, &bytes[(push_size) as usize..bytes.len()]) + eprintln!("Bytes len is {}", bytes.len()); + if bytes.len() - 1 < push_size as usize { + let pad_len = push_size as usize - bytes.len() + 1; + eprintln!("pad len: {}", pad_len); + let mut new_bytes = bytes.to_vec(); + for _ in (0..pad_len) { + new_bytes.push(0); + } + let push_val = &new_bytes[1..(push_size + 1) as usize]; + (push_op(push_size, push_val),push_size, new_bytes[(push_size) as usize..new_bytes.len()].to_vec()) + } else { + let push_val = &bytes[1..(push_size + 1) as usize]; + eprintln!("PUSH VAL IS {:#?}", push_val); + (push_op(push_size, push_val),push_size, bytes[(push_size) as usize..bytes.len()].to_vec()) + } + } fn parse_dup(byte: u8) -> Instruction { @@ -109,52 +123,179 @@ fn push_size(b: u8) -> u8 { } } +// Add zeroes to the left side of a byte array until the byte array is a certain +pub fn zero_extend(bytes: &[u8]) -> [u8; SZ] { + let mut extended_bytes: [u8; SZ] = [0u8; SZ]; + if bytes.len() < SZ { + let pad_size = SZ - bytes.len(); + let last_idx = SZ - 1; + let start_idx = last_idx - (bytes.len() - 1); + extended_bytes[start_idx..].clone_from_slice(&bytes); + let padding_len = SZ - bytes.len(); + for i in (0..pad_size - 1) { + extended_bytes[i] = 0; + } -fn push_op(sz: u8, val: &[u8]) -> Instruction { - let mut zero_len = 8 - val.len(); - let mut buf = vec![]; - for _ in (0..zero_len) { - buf.push(0); + + } else { + extended_bytes.copy_from_slice(bytes); } - buf.extend_from_slice(val); + extended_bytes + + +} + + + +fn push_op(sz: u8, val: &[u8]) -> Instruction { + + // let val = if val.len() < 8 { + // let mut zero_len = if val.len() < 8 {8 - val.len()} else {0}; + // let mut buf = vec![]; + // for _ in (0..zero_len) { + // buf.push(0); + // } + // buf.extend_from_slice(val); + + // let mut sliced = [0u8; 8]; + // sliced.copy_from_slice(&buf); + // u64::from_be_bytes(sliced) + // } else { + // let mut buf = vec![]; + // buf.copy_from_slice() + // u64::from_be_bytes(val) + // }; - let mut sliced = [0u8; 8]; - sliced.copy_from_slice(&buf); - let val = u64::from_be_bytes(sliced); match sz { - 1 => push1(BitVec::<1>::new_literal(val)), - 2 => push2(BitVec::<2>::new_literal(val)), - 3 => push3(BitVec::<3>::new_literal(val)), - 4 => push4(BitVec::<4>::new_literal(val)), - 5 => push5(BitVec::<5>::new_literal(val)), - 6 => push6(BitVec::<6>::new_literal(val)), - 7 => push7(BitVec::<7>::new_literal(val)), - 8 => push8(BitVec::<8>::new_literal(val)), - 9 => push9(BitVec::<9>::new_literal(val)), - 10 => push10(BitVec::<10>::new_literal(val)), - 11 => push11(BitVec::<11>::new_literal(val)), - 12 => push12(BitVec::<12>::new_literal(val)), - 13 => push13(BitVec::<13>::new_literal(val)), - 14 => push14(BitVec::<14>::new_literal(val)), - 15 => push15(BitVec::<15>::new_literal(val)), - 16 => push16(BitVec::<16>::new_literal(val)), - 17 => push17(BitVec::<17>::new_literal(val)), - 18 => push18(BitVec::<18>::new_literal(val)), - 19 => push19(BitVec::<19>::new_literal(val)), - 20 => push20(BitVec::<20>::new_literal(val)), - 21 => push21(BitVec::<21>::new_literal(val)), - 21 => push22(BitVec::<22>::new_literal(val)), - 23 => push23(BitVec::<23>::new_literal(val)), - 24 => push24(BitVec::<24>::new_literal(val)), - 25 => push25(BitVec::<25>::new_literal(val)), - 26 => push26(BitVec::<26>::new_literal(val)), - 27 => push27(BitVec::<27>::new_literal(val)), - 28 => push28(BitVec::<28>::new_literal(val)), - 29 => push29(BitVec::<29>::new_literal(val)), - 30 => push30(BitVec::<30>::new_literal(val)), - 31 => push31(BitVec::<31>::new_literal(val)), - 32 => push32(BitVec::<32>::new_literal(val)), + 1 => { + let val = zero_extend::<1>(val); + push1(val.into()) + }, + 2 => { + let val = zero_extend::<2>(val).into(); + push2(val) + }, + 3 => { + let val = zero_extend::<3>(val).into(); + push3(val) + }, + 4 => { + let val = zero_extend::<4>(val).into(); + push4(val) + }, + 5 => { + let val = zero_extend::<5>(val).into(); + push5(val) + }, + 6 => { + let val = zero_extend::<6>(val).into(); + push6(val) + }, + 7 => { + let val = zero_extend::<7>(val).into(); + push7(val) + }, + 8 => { + let val = zero_extend::<8>(val).into(); + push8(val) + }, + 9 => { + let val = zero_extend::<9>(val).into(); + push9(val) + }, + 10 => { + let val = zero_extend::<10>(val).into(); + push10(val) + }, + 11 => { + let val = zero_extend::<11>(val).into(); + push11(val) + }, + 12 => { + let val = zero_extend::<12>(val).into(); + push12(val) + }, + 13 => { + let val = zero_extend::<13>(val).into(); + push13(val) + }, + 14 => { + let val = zero_extend::<14>(val).into(); + push14(val) + }, + 15 => { + let val = zero_extend::<15>(val).into(); + push15(val) + }, + 16 => { + let val = zero_extend::<16>(val).into(); + push16(val) + }, + 17 => { + let val = zero_extend::<17>(val).into(); + push17(val) + }, + 18 => { + let val = zero_extend::<18>(val).into(); + push18(val) + }, + 19 => { + let val = zero_extend::<19>(val).into(); + push19(val) + }, + 20 => { + let val = zero_extend::<20>(val).into(); + push20(val) + }, + 21 => { + let val = zero_extend::<21>(val).into(); + push21(val) + }, + 21 => { + let val = zero_extend::<22>(val).into(); + push22(val) + }, + 23 => { + let val = zero_extend::<23>(val).into(); + push23(val) + }, + 24 => { + let val = zero_extend::<24>(val).into(); + push24(val) + }, + 25 => { + let val = zero_extend::<25>(val).into(); + push25(val) + }, + 26 => { + let val = zero_extend::<26>(val).into(); + push26(val) + }, + 27 => { + let val = zero_extend::<27>(val).into(); + push27(val) + }, + 28 => { + let val = zero_extend::<28>(val).into(); + push28(val) + }, + 29 => { + let val = zero_extend::<29>(val).into(); + push29(val) + }, + 30 => { + let val = zero_extend::<30>(val).into(); + push30(val) + }, + 31 => { + let val = zero_extend::<31>(val).into(); + push31(val) + }, + 32 => { + let val = zero_extend::<32>(val).into(); + push32(val) + }, _ => { todo!() } diff --git a/src/record.rs b/src/record.rs index 2cd7c38..bb5196e 100644 --- a/src/record.rs +++ b/src/record.rs @@ -3,10 +3,11 @@ use crate::storage::Address; use ruint::aliases::*; use ruint::Uint; +use z3_ext::ast::Ast; use z3_ext::ast::Bool; #[derive(Clone, Debug)] -pub struct MachineRecord { +pub struct MachineRecord { pub mem: Option, pub stack: Option>, pub storage: Option, @@ -34,19 +35,19 @@ pub enum MemOp { Read { idx: Index }, } #[derive(Clone, Debug)] -pub enum StackOp { +pub enum StackOp { Push(BitVec), Pop, } #[derive(Default, Clone, Debug)] -pub struct StackChange { +pub struct StackChange { pub pop_qty: u64, pub push_qty: u64, pub ops: Vec>, } -impl StackChange { +impl StackChange { pub fn push(val: BitVec) -> Self { Self { pop_qty: 0, @@ -83,6 +84,6 @@ pub struct StorageChange { pub log: Vec, } -pub fn push(val: BitVec) -> StackOp { +pub fn push(val: BitVec) -> StackOp { StackOp::Push(val) } diff --git a/src/smt/bitvec/mod.rs b/src/smt/bitvec/mod.rs index f914329..719eaaa 100644 --- a/src/smt/bitvec/mod.rs +++ b/src/smt/bitvec/mod.rs @@ -13,13 +13,13 @@ pub enum BVType { pub type SymByte = BitVec<8>; #[derive(Debug, Clone, Eq)] -pub struct BitVec { +pub struct BitVec { pub inner: BVType, pub(crate) typ: super::SolverType, } -// impl PartialEq for BitVec { +// impl PartialEq for BitVec { // fn eq(&self, other: &Self) -> bool { // let BVType::Z3(a) = &self.inner; // let BVType::Z3(b) = &other.inner; @@ -28,7 +28,7 @@ pub struct BitVec { // } // } -impl Hash for BitVec { +impl Hash for BitVec { fn hash(&self, state: &mut H) { self.as_ref().hash(state); state.finish(); @@ -38,7 +38,7 @@ impl Hash for BitVec { } -impl BitVec { +impl BitVec { pub fn with_bv(bv: BV<'static>) -> Self { Self { inner: BVType::Z3(bv), @@ -50,17 +50,17 @@ impl BitVec { self.inner = BVType::Z3(bv.simplify()); } } -impl Default for BitVec { +impl Default for BitVec { fn default() -> Self { let ctx = ctx(); Self { - inner: BVType::Z3(BV::from_u64(ctx, 0, SZ * 8)), + inner: BVType::Z3(BV::from_u64(ctx, 0, (SZ * 8) as u32)), typ: SolverType::Z3, } } } -impl PartialEq for BitVec { +impl PartialEq for BitVec { fn eq(&self, other: &Self) -> bool { let a = self.as_ref(); diff --git a/src/smt/bitvec/z3.rs b/src/smt/bitvec/z3.rs index c6bf6ba..f21dc3e 100644 --- a/src/smt/bitvec/z3.rs +++ b/src/smt/bitvec/z3.rs @@ -3,12 +3,13 @@ use std::cmp::Ordering; use super::super::ctx; use super::{BVType, BitVec}; +use ruint::Uint; use z3::ast::{Ast, BV}; -impl BitVec { +impl BitVec { pub fn new_literal(val: u64) -> Self { let ctx = ctx(); - let bv = BV::from_u64(ctx, val, SZ * 8); + let bv = BV::from_u64(ctx, val, (SZ * 8) as u32); Self { inner: BVType::Z3(bv), typ: Default::default(), @@ -17,7 +18,7 @@ impl BitVec { pub fn new_const(name: impl AsRef) -> Self { - let bv = BV::new_const(ctx(), name.as_ref(), SZ * 8); + let bv = BV::new_const(ctx(), name.as_ref(), (SZ * 8) as u32); Self { inner: BVType::Z3(bv), typ: Default::default(), @@ -25,10 +26,10 @@ impl BitVec { } } -impl SymbolicValue, u64> for BitVec { +impl SymbolicValue, u64> for BitVec { fn new_literal(val: u64) -> Self { let ctx = ctx(); - let bv = BV::from_u64(ctx, val, SZ * 8); + let bv = BV::from_u64(ctx, val, (SZ * 8) as u32); Self { inner: BVType::Z3(bv), typ: Default::default(), @@ -36,7 +37,7 @@ impl SymbolicValue, u64> for BitVec { } fn new_const(name: impl AsRef) -> Self { - let bv = BV::new_const(ctx(), name.as_ref(), SZ * 8); + let bv = BV::new_const(ctx(), name.as_ref(), (SZ * 8) as u32); Self { inner: BVType::Z3(bv), typ: Default::default(), diff --git a/src/stack.rs b/src/stack.rs index ef4b961..b823309 100644 --- a/src/stack.rs +++ b/src/stack.rs @@ -9,18 +9,19 @@ use z3_ext::{ Config, }; #[derive(Default, Debug, Clone)] -pub struct Stack { +pub struct Stack { stack: SmallVec<[BitVec; 1024]>, size: usize, } -impl Stack { +impl Stack { pub fn push(&mut self, val: BitVec) { self.size += 1; self.stack.push(val); } pub fn pop(&mut self) -> BitVec { + eprintln!("STACK SIZE: {} AND STACK TOP {:#?}", self.size, self.peek()); self.size -= 1; self.stack.pop().unwrap() } @@ -50,7 +51,7 @@ impl Stack { } } -impl MachineComponent for Stack { +impl MachineComponent for Stack { type Record = StackChange; fn apply_change(&mut self, rec: Self::Record) { diff --git a/src/state/evm.rs b/src/state/evm.rs index 93dd0b9..a998628 100644 --- a/src/state/evm.rs +++ b/src/state/evm.rs @@ -54,6 +54,7 @@ impl<'ctx> EvmState { pub fn exec_once(mut self) -> (ExecBranch<'ctx>, Option>) { let inst = self.curr_instruction(); + eprintln!("CURRENT INSTRUCTION: {:#?} at pc: {}", inst, self.pc); let change = inst.exec(&self); self.state_transition(change) @@ -72,6 +73,9 @@ impl<'ctx> EvmState { storage } = rec; let mut new_state = self.clone(); + if halt { + return ((new_state, vec![]), None); + } if let Some(stack_rec) = stack { new_state.stack_apply(stack_rec); } diff --git a/src/traits.rs b/src/traits.rs index 7b1844d..5a8b5a4 100644 --- a/src/traits.rs +++ b/src/traits.rs @@ -8,7 +8,7 @@ use crate::state::evm::EvmState; use crate::storage::{AccountStorage, StorageValue}; use z3_ext::ast::Bool; -pub trait MachineState { +pub trait MachineState { type PC; fn pc(&self) -> Self::PC; @@ -26,7 +26,7 @@ pub trait MachineState { fn storage_apply(&mut self, storage_rec: StorageChange); } -pub trait Machine { +pub trait Machine { type State: MachineState; // All possible final states @@ -37,7 +37,7 @@ pub trait Machine { fn state_ref_mut(&mut self) -> &mut Self::State; } -pub trait MachineInstruction<'ctx, const SZ: u32> { +pub trait MachineInstruction<'ctx, const SZ: usize> { fn exec(&self, mach: &EvmState) -> MachineRecord; } diff --git a/tests/lib.rs b/tests/lib.rs new file mode 100644 index 0000000..f71c19b --- /dev/null +++ b/tests/lib.rs @@ -0,0 +1,40 @@ +extern crate ser; +use ser::{ + traits::*, + machine::*, + stack::*, + storage::*, + memory::*, + conversion::*, + bvc, + bvi, + parser::*, +}; +use z3::ast::*; + +pub const SIMPLE_COUNTER: &str = r"6080604052348015600f57600080fd5b5060043610603c5760003560e01c80633fb5c1cb1460415780638381f58a146053578063d09de08a14606d575b600080fd5b6051604c3660046083565b600055565b005b605b60005481565b60405190815260200160405180910390f35b6051600080549080607c83609b565b9190505550565b600060208284031215609457600080fd5b5035919050565b60006001820160ba57634e487b7160e01b600052601160045260246000fd5b506001019056fea2646970667358221220f0cfb2159c518c3da0ad864362bad5dc0715514a9ab679237253d506773a0a1b64736f6c63430008130033"; +pub const COUNTER_WITH_STORAGE_MAPPING: &str = r#"608060405234801561001057600080fd5b5060056000806001815260200190815260200160002081905550610197806100396000396000f3fe608060405234801561001057600080fd5b50600436106100365760003560e01c8063846719e01461003b578063d78233d61461006b575b600080fd5b6100556004803603810190610050919061010a565b61009b565b6040516100629190610146565b60405180910390f35b6100856004803603810190610080919061010a565b6100b7565b6040516100929190610146565b60405180910390f35b6000806000838152602001908152602001600020549050919050565b60006020528060005260406000206000915090505481565b600080fd5b6000819050919050565b6100e7816100d4565b81146100f257600080fd5b50565b600081359050610104816100de565b92915050565b6000602082840312156101205761011f6100cf565b5b600061012e848285016100f5565b91505092915050565b610140816100d4565b82525050565b600060208201905061015b6000830184610137565b9291505056fea2646970667358fe122066b287fef10118cba238fe38953bfefe938afefefefefe94fefe3682fefefefe64736f6c63430008110033"#; + +#[test] +#[ignore] +fn can_run_stored_pgm() { + let pgm = Parser::with_pgm(SIMPLE_COUNTER).parse(); + let mut evm = Evm::new(pgm); + + { + let sat_branches = evm.exec_check(); + assert_eq!(sat_branches.len(), 1); + let top = sat_branches + .first() + .unwrap() + .0 + .0 + .stack() + .peek() + .cloned() + .unwrap(); + eprintln!("Stack top size: {:#?}", top.as_ref().get_size()); + assert_eq!(top, bvi(5)); + } + eprintln!("STATES > {:#?}", evm.states); +} \ No newline at end of file diff --git a/tests/test_storage.rs b/tests/test_storage.rs new file mode 100644 index 0000000..e69de29