diff --git a/.gitignore b/.gitignore index 5d0be3f..f2ad452 100644 --- a/.gitignore +++ b/.gitignore @@ -3,4 +3,5 @@ *.txt.log* .idea/* *.hex -*.evm \ No newline at end of file +*.evm +*.txt \ No newline at end of file diff --git a/example-trace.txt b/example-trace.txt deleted file mode 100644 index f270726..0000000 --- a/example-trace.txt +++ /dev/null @@ -1,1024 +0,0 @@ ----- machine::machine_returns_one_exec_for_non_branching_pgm stdout ---- - - -------- Reachable State --------- -State EvmState { - memory: Memory { - inner: [], - }, - stack: Stack { - stack: [ - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ], - }, - pc: 8, - pgm: [ - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - a, - ), - typ: Z3, - }, - ), - Add, - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000007, - ), - typ: Z3, - }, - ), - JumpI, - Push( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ), - ], -} - - -MODEL:Some( - a -> #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff - , -) - - - -------- Full Trace Tree ------- -StateTree { - id: NodeId { - id: 763425973fbb4e2fba219c2b0b9e051a, - parent: None, - }, - val: EvmState { - memory: Memory { - inner: [], - }, - stack: Stack { - stack: [], - }, - pc: 0, - pgm: [ - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - a, - ), - typ: Z3, - }, - ), - Add, - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000007, - ), - typ: Z3, - }, - ), - JumpI, - Push( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ), - ], - }, - path_condition: None, - left: Some( - StateTree { - id: NodeId { - id: 93e5d25a069f4945afbc7202ca712223, - parent: None, - }, - val: EvmState { - memory: Memory { - inner: [], - }, - stack: Stack { - stack: [ - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ], - }, - pc: 1, - pgm: [ - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - a, - ), - typ: Z3, - }, - ), - Add, - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000007, - ), - typ: Z3, - }, - ), - JumpI, - Push( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ), - ], - }, - path_condition: None, - left: Some( - StateTree { - id: NodeId { - id: c31b9dd6c241473ebaecb540353f4925, - parent: None, - }, - val: EvmState { - memory: Memory { - inner: [], - }, - stack: Stack { - stack: [ - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - ], - }, - pc: 2, - pgm: [ - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - a, - ), - typ: Z3, - }, - ), - Add, - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000007, - ), - typ: Z3, - }, - ), - JumpI, - Push( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ), - ], - }, - path_condition: None, - left: Some( - StateTree { - id: NodeId { - id: 9b647bf4ac7b46a69242e59984017fef, - parent: None, - }, - val: EvmState { - memory: Memory { - inner: [], - }, - stack: Stack { - stack: [ - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - BitVec { - inner: Z3( - a, - ), - typ: Z3, - }, - ], - }, - pc: 3, - pgm: [ - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - a, - ), - typ: Z3, - }, - ), - Add, - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000007, - ), - typ: Z3, - }, - ), - JumpI, - Push( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ), - ], - }, - path_condition: None, - left: Some( - StateTree { - id: NodeId { - id: 66c4de3ffa364582a08255e69c277215, - parent: None, - }, - val: EvmState { - memory: Memory { - inner: [], - }, - stack: Stack { - stack: [ - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - BitVec { - inner: Z3( - (bvadd a #x0000000000000000000000000000000000000000000000000000000000000001), - ), - typ: Z3, - }, - ], - }, - pc: 4, - pgm: [ - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - a, - ), - typ: Z3, - }, - ), - Add, - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000007, - ), - typ: Z3, - }, - ), - JumpI, - Push( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ), - ], - }, - path_condition: None, - left: Some( - StateTree { - id: NodeId { - id: 850f56c7fb474be8964df31b0768e4e0, - parent: None, - }, - val: EvmState { - memory: Memory { - inner: [], - }, - stack: Stack { - stack: [ - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - BitVec { - inner: Z3( - (bvadd a #x0000000000000000000000000000000000000000000000000000000000000001), - ), - typ: Z3, - }, - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000007, - ), - typ: Z3, - }, - ], - }, - pc: 5, - pgm: [ - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - a, - ), - typ: Z3, - }, - ), - Add, - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000007, - ), - typ: Z3, - }, - ), - JumpI, - Push( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ), - ], - }, - path_condition: None, - left: Some( - StateTree { - id: NodeId { - id: 194b94b65ac34df1bb5dc6d6a2295ec1, - parent: None, - }, - val: EvmState { - memory: Memory { - inner: [], - }, - stack: Stack { - stack: [ - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ], - }, - pc: 6, - pgm: [ - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - a, - ), - typ: Z3, - }, - ), - Add, - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000007, - ), - typ: Z3, - }, - ), - JumpI, - Push( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ), - ], - }, - path_condition: Some( - (and (not (not (= (bvadd a - #x0000000000000000000000000000000000000000000000000000000000000001) - #x0000000000000000000000000000000000000000000000000000000000000000)))), - ), - left: Some( - StateTree { - id: NodeId { - id: 5ffdf966e9d1476689c4e71cab83e9e6, - parent: None, - }, - val: EvmState { - memory: Memory { - inner: [], - }, - stack: Stack { - stack: [ - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - ], - }, - pc: 7, - pgm: [ - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - a, - ), - typ: Z3, - }, - ), - Add, - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000007, - ), - typ: Z3, - }, - ), - JumpI, - Push( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ), - ], - }, - path_condition: Some( - (and (not (not (= (bvadd a - #x0000000000000000000000000000000000000000000000000000000000000001) - #x0000000000000000000000000000000000000000000000000000000000000000)))), - ), - left: Some( - StateTree { - id: NodeId { - id: cb50266a2e174d318063fe6585098087, - parent: None, - }, - val: EvmState { - memory: Memory { - inner: [], - }, - stack: Stack { - stack: [ - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ], - }, - pc: 8, - pgm: [ - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - a, - ), - typ: Z3, - }, - ), - Add, - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000007, - ), - typ: Z3, - }, - ), - JumpI, - Push( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ), - ], - }, - path_condition: Some( - (and (not (not (= (bvadd a - #x0000000000000000000000000000000000000000000000000000000000000001) - #x0000000000000000000000000000000000000000000000000000000000000000)))), - ), - left: None, - right: None, - }, - ), - right: None, - }, - ), - right: None, - }, - ), - right: Some( - StateTree { - id: NodeId { - id: 349b98b471ad4c908ea348e334a3132b, - parent: None, - }, - val: EvmState { - memory: Memory { - inner: [], - }, - stack: Stack { - stack: [ - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ], - }, - pc: 7, - pgm: [ - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - a, - ), - typ: Z3, - }, - ), - Add, - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000007, - ), - typ: Z3, - }, - ), - JumpI, - Push( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ), - ], - }, - path_condition: Some( - (and (not (= (bvadd a - #x0000000000000000000000000000000000000000000000000000000000000001) - #x0000000000000000000000000000000000000000000000000000000000000000))), - ), - left: Some( - StateTree { - id: NodeId { - id: 84c6c28a405c4b4b9cba4716a2e6014c, - parent: None, - }, - val: EvmState { - memory: Memory { - inner: [], - }, - stack: Stack { - stack: [ - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ], - }, - pc: 8, - pgm: [ - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000002, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000001, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - a, - ), - typ: Z3, - }, - ), - Add, - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000007, - ), - typ: Z3, - }, - ), - JumpI, - Push( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000064, - ), - typ: Z3, - }, - ), - Push32( - BitVec { - inner: Z3( - #x0000000000000000000000000000000000000000000000000000000000000032, - ), - typ: Z3, - }, - ), - ], - }, - path_condition: Some( - (and (not (= (bvadd a - #x0000000000000000000000000000000000000000000000000000000000000001) - #x0000000000000000000000000000000000000000000000000000000000000000))), - ), - left: None, - right: None, - }, - ), - right: None, - }, - ), - }, - ), - right: None, - }, - ), - right: None, - }, - ), - right: None, - }, - ), - right: None, - }, - ), - right: None, -} \ No newline at end of file diff --git a/examples/simple_storage.rs b/examples/simple_storage.rs index 4655871..8aa74a9 100644 --- a/examples/simple_storage.rs +++ b/examples/simple_storage.rs @@ -1,6 +1,7 @@ #![allow(unused_imports, unused)] use ser::{ - bvc, bvi, conversion::*, machine::*, memory::*, parser::*, stack::*, storage::*, traits::*, instruction::Instruction, + bvc, bvi, conversion::*, instruction::Instruction, machine::*, memory::*, parser::*, stack::*, + storage::*, traits::*, }; use z3::ast::*; @@ -17,17 +18,17 @@ fn main() { // as seen here https://bytegraph.xyz/bytecode/e5987a6f24f8af926faddae88de7980f/graph assert_eq!(7, leaf.len()); } - - - let reachability_report = Evm::exec_check(execution); println!("Report: {:#?}", reachability_report); - let traces = reachability_report.iter() + let traces = reachability_report + .iter() .map(|trace| trace.0.iter().map(|t| &t.1).collect::>()) .collect::>(); println!("traces: {:#?}", traces); - let reverted_traces = traces.into_iter().filter(|t| *t.last().unwrap().clone() == Instruction::Revert).collect::>(); + let reverted_traces = traces + .into_iter() + .filter(|t| *t.last().unwrap().clone() == Instruction::Revert) + .collect::>(); println!("TRACES WITH REVERTS {:#?}", reverted_traces); - } diff --git a/examples/swaps.rs b/examples/swaps.rs index 26d6d85..929904d 100644 --- a/examples/swaps.rs +++ b/examples/swaps.rs @@ -34,7 +34,7 @@ PUSH1 0x10 RETURN -MAYBE REVERT: +MAYBE REVERT: PUSH1 0x42 PUSH1 0x00 PUSH2 0x5000 diff --git a/src/conversion/mod.rs b/src/conversion/mod.rs index d677a7f..f4b39df 100644 --- a/src/conversion/mod.rs +++ b/src/conversion/mod.rs @@ -81,7 +81,6 @@ impl From<[u8; SZ]> for BitVec { 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()); @@ -97,9 +96,7 @@ pub fn bitvec_array_to_bv<'ctx>(value: Vec>) -> BV<'ctx> { for i in value.iter() { bv = bv.concat(i.as_ref()).simplify(); } - bv.extract((bv.get_size() - 8 - 1) as u32, 0) - .simplify() - + bv.extract((bv.get_size() - 8 - 1) as u32, 0).simplify() } impl TryFrom>> for BitVec { type Error = String; @@ -110,9 +107,10 @@ impl TryFrom>> for BitVec { for i in value.iter() { bv = bv.concat(i.as_ref()).simplify(); } - Ok(bv.extract((bv.get_size() - 8 - 1) as u32, 0) - .simplify() - .into()) + Ok(bv + .extract((bv.get_size() - 8 - 1) as u32, 0) + .simplify() + .into()) } } impl AsRef> for BitVec { diff --git a/src/instruction/mod.rs b/src/instruction/mod.rs index 8be9a3d..79eb993 100644 --- a/src/instruction/mod.rs +++ b/src/instruction/mod.rs @@ -185,7 +185,6 @@ fn exec_dup_nth(mach: &EvmState, n: usize) -> MachineRecord<32> { } fn exec_swap_nth(mach: &EvmState, n: usize) -> MachineRecord<32> { - MachineRecord { stack: Some(StackChange { pop_qty: 0, @@ -244,17 +243,14 @@ impl Instruction { impl<'ctx> MachineInstruction<'ctx, 32> for Instruction { fn exec(&self, mach: &EvmState) -> MachineRecord<32> { match self { - Instruction::Stop => { - MachineRecord { - halt: true, - stack: None, - mem: None, - constraints: None, - storage: None, - pc: (mach.pc(), mach.pc()) - } - } - , + Instruction::Stop => MachineRecord { + halt: true, + stack: None, + mem: None, + constraints: None, + storage: None, + pc: (mach.pc(), mach.pc()), + }, Instruction::Add => { let stack = mach.stack(); let [stack_top, stack_top2] = stack.peek_top().unwrap(); @@ -621,42 +617,37 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction { } Instruction::Sha3 => { let stack = mach.stack(); - let [ offset, size] = stack.peek_top().unwrap(); + let [offset, size] = stack.peek_top().unwrap(); let mut offsett = offset.clone(); let mut sizee = size.clone(); offsett.simplify(); sizee.simplify(); - + let mem = mach.mem().read_with_offset(offsett.clone(), sizee.clone()); let sz = usize::from(sizee.clone()); - + let mut bv: BV<'static> = bitvec_array_to_bv(mem); - - - - + let hashed = sha3(bv.get_size()).apply(&[&bv]); - + let hashed: BitVec<32> = hashed.as_bv().unwrap().into(); let mem_change = MemChange { - ops_log: vec![MemOp::Read {idx: offsett.clone()}] + ops_log: vec![MemOp::Read { + idx: offsett.clone(), + }], }; - let stack_change = StackChange::with_ops(vec![ - StackOp::Pop, - StackOp::Pop, - StackOp::Push(hashed) - ]); - + let stack_change = + StackChange::with_ops(vec![StackOp::Pop, StackOp::Pop, StackOp::Push(hashed)]); + MachineRecord { stack: Some(stack_change), mem: Some(mem_change), - pc: (mach.pc(), mach.pc() + self.byte_size()), + pc: (mach.pc(), mach.pc() + self.byte_size()), constraints: None, halt: false, storage: None, } - - }, + } Instruction::Address => todo!(), Instruction::Balance => { let stack = mach.stack(); @@ -892,7 +883,7 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction { let dest = stack.peek().unwrap(); let mut dest = dest.clone(); dest.simplify(); - + let mut val_mem = mach.memory.read_word(dest.clone()); val_mem.simplify(); @@ -1016,7 +1007,7 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction { } Instruction::Jump => { let jump_dest = mach.stack().peek().unwrap(); - + let jump_dest_concrete = jump_dest.as_ref().simplify().as_u64().unwrap() as usize; let stack_rec = StackChange { pop_qty: 1, @@ -1048,7 +1039,6 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction { push_qty: 0, ops: vec![StackOp::Pop, StackOp::Pop], }; - MachineRecord { stack: Some(stack_rec), diff --git a/src/memory.rs b/src/memory.rs index 884306b..bf965c3 100644 --- a/src/memory.rs +++ b/src/memory.rs @@ -76,11 +76,15 @@ impl Memory { val } - pub fn read_with_offset(&self, offset: Index, size: impl Into + Clone) -> Vec> { + pub fn read_with_offset( + &self, + offset: Index, + size: impl Into + Clone, + ) -> Vec> { let idx: usize = offset.into(); - + eprintln!("IDX: {idx:} and size: {:#?}", size.clone().into()); - let val = self.inner[idx .. (idx + size.clone().into())].to_vec(); + let val = self.inner[idx..(idx + size.clone().into())].to_vec(); eprintln!("VAL IN MEM READ EITH OFFSET: {:#?}", val); val } diff --git a/src/state/env.rs b/src/state/env.rs index 1842c21..364ae3f 100644 --- a/src/state/env.rs +++ b/src/state/env.rs @@ -1,4 +1,4 @@ -use z3_ext::ast::{Ast, AstKind, Array, BV}; +use z3_ext::ast::{Array, Ast, AstKind, BV}; use z3_ext::FuncDecl; use z3_ext::Sort; @@ -35,7 +35,7 @@ pub fn sha3<'ctx>(size: u32) -> FuncDecl<'ctx> { ctx(), format!("sha3_{}", id).as_str(), &[&Sort::bitvector(ctx(), size)], - &Sort::bitvector(ctx(), 256) + &Sort::bitvector(ctx(), 256), ); eprintln!("SHA3 FUNC: {:#?}", func); diff --git a/tests/lib.rs b/tests/lib.rs index 9f2c69e..8bfcee6 100644 --- a/tests/lib.rs +++ b/tests/lib.rs @@ -84,7 +84,7 @@ PUSH1 0x10 RETURN -MAYBE REVERT: +MAYBE REVERT: PUSH1 0x42 PUSH1 0x00 PUSH2 0x5000 @@ -138,4 +138,3 @@ fn test_swap2_jumpi_maybe_revert() { reachability_report.get(1).unwrap().1.unwrap() ); } - diff --git a/tests/test_storage.rs b/tests/test_storage.rs deleted file mode 100644 index 8b13789..0000000 --- a/tests/test_storage.rs +++ /dev/null @@ -1 +0,0 @@ -