Add configurable env support & update caller, calldatasize & calldata…

…load to use configurable env
WilfredTA · Aug 6, 2023 · 8b734a5 · 8b734a5
1 parent 4fa06fb
commit 8b734a5
Show file tree

Hide file tree

Showing 13 changed files with 195 additions and 103 deletions.
diff --git a/examples/simple_pgm.rs b/examples/simple_pgm.rs
@@ -7,7 +7,7 @@ use z3::ast::*;
 pub const SUPERSIMPLE: &str = r#"604260005260206000F3"#;
 fn main() {
     let pgm = Parser::with_pgm(SUPERSIMPLE).parse();
-    let mut evm = Evm::new(pgm);
+    let mut evm = Evm::with_pgm(pgm);
 
     let execution_trace = evm.exec();
     {

diff --git a/examples/simple_storage.rs b/examples/simple_storage.rs
@@ -10,7 +10,7 @@ pub const STORAGE_SIMPLE: &str = r#"6080604052348015600f57600080fd5b506004361060
 fn main() {
     let pgm = Parser::with_pgm(STORAGE_SIMPLE).parse();
 
-    let mut evm = Evm::new(pgm);
+    let mut evm = Evm::with_pgm(pgm);
 
     let execution = evm.exec();
     {

diff --git a/examples/simple_storage_deploy.rs b/examples/simple_storage_deploy.rs
@@ -9,7 +9,7 @@ use z3::ast::*;
 pub const COUNTER_WITH_STORAGE_MAPPING_DEPLOY: &str = r#"608060405234801561001057600080fd5b5060056000806001815260200190815260200160002081905550610197806100396000396000f3fe608060405234801561001057600080fd5b50600436106100365760003560e01c8063846719e01461003b578063d78233d61461006b575b600080fd5b6100556004803603810190610050919061010a565b61009b565b6040516100629190610146565b60405180910390f35b6100856004803603810190610080919061010a565b6100b7565b6040516100929190610146565b60405180910390f35b6000806000838152602001908152602001600020549050919050565b60006020528060005260406000206000915090505481565b600080fd5b6000819050919050565b6100e7816100d4565b81146100f257600080fd5b50565b600081359050610104816100de565b92915050565b6000602082840312156101205761011f6100cf565b5b600061012e848285016100f5565b91505092915050565b610140816100d4565b82525050565b600060208201905061015b6000830184610137565b9291505056fea2646970667358fe122066b287fef10118cba238fe38953bfefe938afefefefefe94fefe3682fefefefe64736f6c63430008110033"#;
 fn main() {
     let pgm = Parser::with_pgm(COUNTER_WITH_STORAGE_MAPPING_DEPLOY).parse();
-    let mut evm = Evm::new(pgm);
+    let mut evm = Evm::with_pgm(pgm);
 
     let execution = evm.exec();
     {

diff --git a/examples/simple_token.rs b/examples/simple_token.rs
@@ -6,28 +6,29 @@ use ser::{
 use z3::ast::*;
 
 pub const SIMPLE_TOKEN: &str = r#"608060405234801561001057600080fd5b50600436106100415760003560e01c806327e235e314610046578063a9059cbb14610078578063f8b2cb4f1461008d575b600080fd5b610066610054366004610143565b60006020819052908152604090205481565b60405190815260200160405180910390f35b61008b610086366004610165565b6100b6565b005b61006661009b366004610143565b6001600160a01b031660009081526020819052604090205490565b336000908152602081905260409020548111156100d257600080fd5b33600090815260208190526040812080548392906100f19084906101a5565b90915550506001600160a01b0382166000908152602081905260408120805483929061011e9084906101be565b90915550505050565b80356001600160a01b038116811461013e57600080fd5b919050565b60006020828403121561015557600080fd5b61015e82610127565b9392505050565b6000806040838503121561017857600080fd5b61018183610127565b946020939093013593505050565b634e487b7160e01b600052601160045260246000fd5b818103818111156101b8576101b861018f565b92915050565b808201808211156101b8576101b861018f56fea264697066735822122041d29a76727a31c9e4ec86703553a675712f98921d6c4bc9b23f274a963de18264736f6c63430008130033"#;
-
+pub const SIMPLE_TOKEN_2: &str = r#"608060405234801561001057600080fd5b50600436106100365760003560e01c806327e235e31461003b578063a9059cbb1461006d575b600080fd5b61005b610049366004610117565b60006020819052908152604090205481565b60405190815260200160405180910390f35b61008061007b366004610139565b610082565b005b33600090815260208190526040812080548392906100a1908490610179565b909155505033600090815260208190526040812080548392906100c5908490610192565b90915550506001600160a01b038216600090815260208190526040812080548392906100f2908490610179565b90915550505050565b80356001600160a01b038116811461011257600080fd5b919050565b60006020828403121561012957600080fd5b610132826100fb565b9392505050565b6000806040838503121561014c57600080fd5b610155836100fb565b946020939093013593505050565b634e487b7160e01b600052601160045260246000fd5b8082018082111561018c5761018c610163565b92915050565b8181038181111561018c5761018c61016356fea26469706673582212201cf1ad42b1d09ece2257b07f3c87313378c1740e47897aef8282a8bce21f250564736f6c63430008130033"#;
 fn main() {
-    let pgm = Parser::with_pgm(SIMPLE_TOKEN).parse();
-    let mut evm = Evm::new(pgm);
+    let pgm = Parser::with_pgm(SIMPLE_TOKEN_2).parse();
+    let mut evm = Evm::with_pgm(pgm);
 
     let execution = evm.exec();
     {
         let leaf = execution.states.leaves();
-        assert_eq!(15, leaf.len());
+        eprintln!("LEAVES: {:#?}", leaf);
+        assert_eq!(14, leaf.len());
 
     }
 
     let reachability_report = Evm::exec_check(execution);
-    println!("Report: {:#?}", reachability_report);
+    eprintln!("Report: {:#?}", reachability_report);
     let traces = reachability_report
         .iter()
         .map(|trace| trace.0.iter().map(|t| &t.1).collect::<Vec<_>>())
         .collect::<Vec<_>>();
-    println!("traces: {:#?}", traces);
+    eprintln!("traces: {:#?}", traces);
     let reverted_traces = traces
         .into_iter()
         .filter(|t| *t.last().unwrap().clone() == Instruction::Revert)
         .collect::<Vec<_>>();
-    println!("TRACES WITH REVERTS {:#?}", reverted_traces);
+    eprintln!("TRACES WITH REVERTS {:#?}", reverted_traces);
 }
diff --git a/examples/swaps.rs b/examples/swaps.rs
@@ -52,7 +52,7 @@ const SWAP2_JUMPI_MAYBE_REVERT: &str = r#"6042600061500036600d57fd5b6000f3"#;
 const SWAP3_JUMPI_RETURN_16: &str = r#"60426000615000604091600e57fd5b6000f3"#;
 fn main() {
     let pgm = Parser::with_pgm(SWAP2_JUMPI_MAYBE_REVERT).parse();
-    let mut evm = Evm::new(pgm);
+    let mut evm = Evm::with_pgm(pgm);
     let execution = evm.exec();
     //eprintln!("Execution tree: {:#?}", execution.states.clone());
     // Should have two paths: both reachable. The first reachable path is the one in which calldata is zero and there is a revert.

diff --git a/src/exec/mod.rs b/src/exec/mod.rs
@@ -1,6 +1,7 @@
 use uuid::Uuid;
 
 use crate::parser::Program;
+use crate::state::context::ExecutionEnv;
 use crate::state::evm::EvmState;
 use crate::state::tree::*;
 use crate::{
@@ -71,13 +72,13 @@ impl<'ctx> Execution<'ctx> {
     }
 
     // Returns the StepRecord AND updates the Exec state tree
-    pub fn step_mut(&mut self) -> StepRecord {
+    pub fn step_mut(&mut self, env: &ExecutionEnv) -> StepRecord {
         // bool returns if there is a branch
         let curr_state_id = self.states.id.clone();
         let mut curr_state = self.states.val.clone();
         let curr_inst = curr_state.curr_instruction();
         let curr_pc = curr_state.pc();
-        let change_rec = curr_inst.exec(&curr_state);
+        let change_rec = curr_inst.exec(&curr_state, &env);
         //eprintln!("CHANGE REC IN EXEC: {:#?}", change_rec);
         let is_branch = change_rec.constraints.is_some();
         if is_branch {
@@ -119,13 +120,13 @@ impl<'ctx> Execution<'ctx> {
     }
 
     // Returns the step record but does not mutate the Exec state tree
-    pub fn step(&self) -> StepRecord {
+    pub fn step(&self, env: &ExecutionEnv) -> StepRecord {
         // bool returns if there is a branch
         let curr_state_id = self.states.id.clone();
         let mut curr_state = self.states.val.clone();
         let curr_inst = curr_state.curr_instruction();
         let curr_pc = curr_state.pc();
-        let change_rec = curr_inst.exec(&curr_state);
+        let change_rec = curr_inst.exec(&curr_state, &env);
 
         let is_branch = change_rec.constraints.is_some();
         curr_state.apply_change(change_rec.clone());
@@ -155,9 +156,10 @@ impl<'ctx> Execution<'ctx> {
         }
     }
 
-    pub fn step_from_mut(&mut self, node_id: &NodeId) -> StepRecord {
+    pub fn step_from_mut(&mut self, node_id: &NodeId, env: &ExecutionEnv) -> StepRecord {
         let curr_state_id = node_id.clone();
         let mut curr_state_tree = self.states.find_by_id(node_id).unwrap().clone();
+        eprintln!("CURR STATE:{:#?} ", curr_state_tree);
         let mut curr_state = &mut curr_state_tree.val;
         if !curr_state.can_continue() {
             return StepRecord::new(true, true);
@@ -166,7 +168,9 @@ impl<'ctx> Execution<'ctx> {
         let curr_inst = curr_state.curr_instruction();
         let curr_pc = curr_state.pc();
         //eprintln!("CURR STATE IN STEP FROM MUT: {:#?}", curr_state);
-        let change_rec = curr_inst.exec(&curr_state);
+
+        let change_rec = curr_inst.exec(&curr_state, &env);
+
         eprintln!("CHANGE REC IN STEP: {:#?}", change_rec);
         eprintln!("Instruction: {:#?} STACK: {:#?}, ",curr_inst, curr_state.stack());
 

diff --git a/src/instruction/mod.rs b/src/instruction/mod.rs
@@ -6,6 +6,7 @@ use z3_ext::ast::{Ast, Bool, BV};
 
 use crate::conversion::bitvec_array_to_bv;
 use crate::record::{push, MemChange, MemOp, StorageChange, StorageOp};
+use crate::state::context::ExecutionEnv;
 use crate::state::env::*;
 use crate::state::evm::EvmState;
 use crate::state::tree::StateTree;
@@ -251,7 +252,7 @@ impl Instruction {
 }
 impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
     type Error = InstructionError;
-    fn exec(&self, mach: &EvmState) -> MachineRecord<32> {
+    fn exec(&self, mach: &EvmState, env: &ExecutionEnv) -> MachineRecord<32> {
         match self {
             Instruction::Stop => MachineRecord {
                 halt: true,
@@ -704,8 +705,8 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
             }
             Instruction::Caller => {
                 let stack = mach.stack();
-                let caller = caller().apply(&[]).as_bv().unwrap();
-                let stack_diff = StackChange::with_ops(vec![pop(), push(caller.into())]);
+                let caller = env.caller();//caller().apply(&[]).as_bv().unwrap();
+                let stack_diff = StackChange::with_ops(vec![pop(), push(caller)]);
 
                 MachineRecord {
                     stack: Some(stack_diff),
@@ -733,8 +734,8 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
             Instruction::CallDataLoad => {
                 let stack = mach.stack();
                 let offset = stack.peek().unwrap();
-                let call_data = call_data_load().apply(&[offset.as_ref()]).as_bv().unwrap();
-                let stack_diff = StackChange::with_ops(vec![pop(), push(call_data.into())]);
+                let call_data = env.calldataload(offset);
+                let stack_diff = StackChange::with_ops(vec![pop(), push(call_data)]);
 
                 MachineRecord {
                     stack: Some(stack_diff),
@@ -747,8 +748,8 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
             }
             Instruction::CallDataSize => {
                 let stack = mach.stack();
-                let call_data_sz = call_data_size().apply(&[]).as_bv().unwrap();
-                let stack_diff = StackChange::with_ops(vec![push(call_data_sz.into())]);
+                let call_data_sz = env.calldatasize();
+                let stack_diff: StackChange<32> = StackChange::with_ops(vec![push(call_data_sz)]);
 
                 MachineRecord {
                     stack: Some(stack_diff),
@@ -1084,10 +1085,9 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
             }
             Instruction::Jump => {
 
-                let jump_dest = mach.stack().peek().expect(&format!("
-                    Expected stack.peek() to return, but didnt. Stack: {:#?}, pc: {}, 
-                ", mach.stack(), mach.pc()));
-
+                let jump_dest = mach.stack().peek().unwrap();
+
+                eprintln!("JUMP DEST: {:#?}", jump_dest);
                 let jump_dest_concrete = jump_dest.as_ref().simplify().as_u64().unwrap() as usize;
                 let stack_rec = StackChange {
                     pop_qty: 1,
@@ -1103,6 +1103,10 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
                     halt: false,
                     storage: None,
                 }
+
+
+
+
             }
             Instruction::JumpI => {
                 let jump_dest = mach.stack().peek().unwrap();

diff --git a/src/machine.rs b/src/machine.rs
@@ -1,4 +1,5 @@
 use std::collections::HashMap;
+use std::sync::RwLock;
 use std::{borrow::BorrowMut, cell::RefCell, rc::Rc};
 use uuid::Uuid;
 
@@ -11,6 +12,7 @@ use crate::exec::Execution;
 use crate::instruction::*;
 use crate::memory::*;
 use crate::parser::Program;
+use crate::state::context::ExecutionEnv;
 use crate::state::evm::EvmState;
 use crate::state::tree::{NodeId, StateTree};
 use crate::storage::{AccountStorage, Address};
@@ -69,12 +71,12 @@ pub struct TransactionContext {
 // It also provides a handler to an Execution, which in turn provides a handler to EvmState
 // so that when an Instruction requires *reading* environmental / network state OR when an Instruction's behavior
 // *depends* on env / network state, it can access it through the Evm, which can be initialized with things like a Transaction context
-#[derive(Clone)]
 pub struct Evm<'ctx> {
     pgm: Program,
     pub states: StateTree<'ctx>,
     change_log: Vec<MachineRecord<32>>,
     pub inverse_state: HashMap<Uuid, Uuid>,
+    ctx: RwLock<ExecutionEnv<'ctx>>
 }
 
 impl<'ctx> Evm<'ctx> {
@@ -91,6 +93,7 @@ impl<'ctx> Evm<'ctx> {
             },
             change_log: vec![],
             inverse_state: Default::default(),
+            ctx: RwLock::new(ExecutionEnv::default())
         }
     }
 
@@ -100,7 +103,7 @@ impl<'ctx> Evm<'ctx> {
 }
 
 impl<'ctx> Evm<'ctx> {
-    pub fn new(pgm: Program) -> Self {
+    pub fn new(pgm: Program, env: ExecutionEnv<'ctx>) -> Self {
         let evm_state = EvmState::with_pgm(pgm.clone());
 
         Self {
@@ -114,6 +117,7 @@ impl<'ctx> Evm<'ctx> {
             },
             change_log: vec![],
             inverse_state: Default::default(),
+            ctx: RwLock::new(env)
         }
     }
 
@@ -211,7 +215,7 @@ impl<'ctx> Machine<32> for Evm<'ctx> {
         let mut halt = false;
         let mut step_recs = vec![];
         let mut exec = Execution::new(self.states.val.clone(), self.pgm.clone());
-        let first_step = exec.step_mut();
+        let first_step = exec.step_mut(self.ctx.read().as_ref().unwrap());
         step_recs.push(first_step);
         let mut ids = vec![];
         loop {
@@ -230,15 +234,15 @@ impl<'ctx> Machine<32> for Evm<'ctx> {
                 //     let continue_from_right = step.right_id();
                 if let Some(right_id) = step.right_id() {
                     ids.push(right_id.id());
-                    let nxt_right_step = exec.step_from_mut(right_id);
+                    let nxt_right_step = exec.step_from_mut(right_id, self.ctx.read().as_ref().unwrap());
                     step_recs.push(nxt_right_step);
                 }
                 //}
                 // if !step.halted_left() {
                 //     let continue_from_left = step.left_id();
                 if let Some(left_id) = step.left_id() {
                     ids.push(left_id.id());
-                    let nxt_step = exec.step_from_mut(left_id);
+                    let nxt_step = exec.step_from_mut(left_id, self.ctx.read().as_ref().unwrap());
                     step_recs.push(nxt_step);
                 }
                 // }

diff --git a/src/stack.rs b/src/stack.rs
@@ -27,19 +27,11 @@ impl<const SZ: usize> Stack<SZ> {
     }
 
     pub fn peek(&self) -> Option<&BitVec<SZ>> {
-        if (self.size) >= self.stack.len() {
-            eprintln!("ERROR: STACK SIZE IS INCONSISTENT WITH INTERNAL STACK... Stack size: {}, internal stack len: {}, stack: {:#?}", 
-            self.size,
-            self.stack.len(),
-            self.stack
-        );
-        }
         if self.size == 0 {
-            self.stack.get(0)
-        } else {
-
-            self.stack.get(self.size - 1)
+            return None;
+            eprintln!("SIZE IS 0.. STACK: {:#?}", self.stack);
         }
+        self.stack.get(self.size - 1)
     }
 
     pub fn size(&self) -> usize {