refactor execution algorithm

examples/simple_pgm.rs

@@ -0,0 +1,31 @@
+
+
+use ser::{
+    traits::*,
+    machine::*,
+    stack::*,
+    storage::*,
+    memory::*,
+    conversion::*,
+    bvc,
+    bvi,
+    parser::*,
+};
+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 execution_trace = evm.exec();
+
+    let leaf = execution_trace.states.leaves();
+    assert_eq!(1, leaf.len());
+    let final_tree = leaf.first().unwrap().clone();
+    // eprintln!("FINAL TREE: {:#?}", final_tree);
+
+    let mut mem_val = final_tree.val.mem_read(bvi(0));
+    mem_val.simplify();
+    assert_eq!(bvi(66), mem_val);
+}

examples/simple_storage.rs

@@ -0,0 +1,34 @@
+
+
+use ser::{
+    traits::*,
+    machine::*,
+    stack::*,
+    storage::*,
+    memory::*,
+    conversion::*,
+    bvc,
+    bvi,
+    parser::*,
+};
+use z3::ast::*;
+
+pub const STORAGE_SIMPLE: &str = r#"6080604052348015600f57600080fd5b506004361060325760003560e01c80631ab06ee5146037578063fac333ac146056575b600080fd5b605460423660046085565b60009182526020829052604090912055565b005b6073606136600460a6565b60006020819052908152604090205481565b60405190815260200160405180910390f35b60008060408385031215609757600080fd5b50508035926020909101359150565b60006020828403121560b757600080fd5b503591905056fea26469706673582212204a6bf5c04a6e273d775914b20b0bab1bca28228be5562d496002981e13ff015264736f6c63430008130033"#; 
+
+
+fn main() {
+    let pgm = Parser::with_pgm(STORAGE_SIMPLE).parse();
+    let mut evm = Evm::new(pgm);
+
+
+    let execution = evm.exec();
+
+    let leaf = execution.states.leaves();
+    assert_eq!(2, leaf.len());
+
+    let final_tree = leaf.get(1).unwrap().clone();
+
+    let mut mem_val = final_tree.val.mem_read(bvi(64)); // 0x40
+    mem_val.simplify();
+    assert_eq!(bvi(128), mem_val); // 0x80
+}

src/exec/mod.rs

@@ -0,0 +1,195 @@
+use uuid::Uuid;
+
+use crate::{record::{
+    MachineRecord
+}, instruction::Instruction, traits::{MachineInstruction, MachineComponent, MachineState}};
+use crate::state::evm::EvmState;
+use crate::state::tree::*;
+
+
+#[derive(Default, Debug)]
+pub struct Execution<'ctx> {
+    changes: Vec<MachineRecord<32>>,
+    program: Vec<Instruction>,
+    pub states: StateTree<'ctx>
+}
+
+#[derive(Default, Debug)]
+pub struct StepRecord 
+
+{
+    left_insert: Option<NodeId>,
+    right_insert: Option<NodeId>,
+    halted_left: bool,
+    halted_right: bool
+}
+
+impl StepRecord {
+
+    pub fn new(halted_left: bool, halted_right: bool) -> Self {
+        Self {
+            halted_left, halted_right, ..Default::default()
+        }
+    }
+    pub fn halted_left(&self) -> bool {
+        self.halted_left
+    }
+
+    pub fn halted_right(&self) -> bool {
+        self.halted_right
+    }
+    pub fn branched(&self) -> bool {
+        self.left_insert.is_some() && self.right_insert.is_some()
+    }
+
+    pub fn left_id(&self) -> Option<&NodeId> {
+        self.left_insert.as_ref()
+    }
+
+    pub fn right_id(&self) -> Option<&NodeId> {
+        self.right_insert.as_ref()
+    }
+
+    pub fn set_left(mut self, left: NodeId) -> Self {
+        self.left_insert = Some(left);
+        self
+    }
+    pub fn set_right(mut self, right: NodeId) -> Self {
+        self.right_insert = Some(right);
+        self
+    }
+}
+
+impl<'ctx> Execution<'ctx> {
+
+    pub fn new(start_state: EvmState, pgm: Vec<Instruction>) -> Self {
+        Self {
+            program: pgm,
+            states: StateTree::from((start_state, None)),
+            ..Default::default()
+        }
+    }
+
+    // Returns the StepRecord AND updates the Exec state tree
+    pub fn step_mut(&mut self)  -> 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 is_branch = change_rec.constraints.is_some();
+        curr_state.apply_change(change_rec.clone());
+        let mut report = StepRecord::new(false, change_rec.halt);
+        if is_branch {
+            // then curr_state.apply generated the right branching state; thus, a state tree w/
+            // an additional constraint
+            // and left tree (by convention left path represents straight line execution) is the negation of such constraint
+            let mut left_state = curr_state.clone();
+            left_state.set_pc(curr_pc + 1);
+            if !left_state.can_continue() {
+                report.halted_left = true;
+            }
+
+            let left_tree = StateTree::from((left_state.clone(), change_rec.constraints.clone().unwrap().not()));
+            let right_tree = StateTree::from((left_state, change_rec.constraints.unwrap()));
+
+            let left_tree_ref = self.states.insert_left_of(left_tree, curr_state_id.id());
+
+
+            let right_tree_ref = self.states.insert_right_of(right_tree, curr_state_id.id());
+
+            report = report.set_left(left_tree_ref);
+            report.set_right(right_tree_ref)
+
+        } else {
+            let left_tree = StateTree::from((curr_state, None));
+            let left_id = self.states.insert_left_of(left_tree, curr_state_id.id());
+
+            report.set_left(left_id)
+        }
+
+    }
+
+    // Returns the step record but does not mutate the Exec state tree
+    pub fn step(&self)  -> 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 is_branch = change_rec.constraints.is_some();
+        curr_state.apply_change(change_rec.clone());
+        let mut report = StepRecord::new(false, change_rec.halt);
+        if is_branch {
+            // then curr_state.apply generated the right branching state; thus, a state tree w/
+            // an additional constraint
+            // and left tree (by convention left path represents straight line execution) is the negation of such constraint
+            let mut left_state = curr_state.clone();
+            left_state.set_pc(curr_pc + 1);
+            if !left_state.can_continue() {
+                report.halted_left = true;
+            }
+            let left_tree = StateTree::from((left_state.clone(), change_rec.constraints.clone().unwrap().not()));
+            let right_tree = StateTree::from((left_state, change_rec.constraints.unwrap()));
+
+            report.set_left(left_tree.id.clone()).set_right(right_tree.id.clone())
+
+        } else {
+            let left_tree = StateTree::from((curr_state, None));
+
+            report.set_left(left_tree.id.clone())
+        }
+
+    }
+
+
+    pub fn step_from_mut(&mut self, node_id: &NodeId) -> StepRecord {
+        let curr_state_id = node_id.clone();
+        let mut curr_state_tree = self.states.find_by_id(node_id).unwrap().clone();
+        let mut curr_state = &mut curr_state_tree.val;
+        if !curr_state.can_continue() {
+
+            return StepRecord::new(true, true);
+        }
+
+        let curr_inst = curr_state.curr_instruction();
+        let curr_pc = curr_state.pc();
+        let change_rec = curr_inst.exec(&curr_state);
+
+        let is_branch = change_rec.constraints.is_some();
+        curr_state.apply_change(change_rec.clone());
+        let curr_state = curr_state;
+        let mut report = StepRecord::new(false, change_rec.halt);
+       // assert_eq!(change_rec.halt, curr_state.halt);
+        if is_branch {
+            // then curr_state.apply generated the right branching state; thus, a state tree w/
+            // an additional constraint
+            // and left tree (by convention left path represents straight line execution) is the negation of such constraint
+            let mut left_state = curr_state.clone();
+            left_state.set_pc(curr_pc + 1);
+            report.halted_left = left_state.halt;
+
+            let left_tree = StateTree::from((left_state.clone(), change_rec.constraints.clone().unwrap().not()));
+            let right_tree = StateTree::from((left_state, change_rec.constraints.unwrap()));
+            let left_tree_ref = self.states.insert_left_of(left_tree, node_id.id());
+            let right_tree_ref = self.states.insert_right_of(right_tree, node_id.id());
+            // curr_state_tree.left = Some(Box::new(left_tree));
+            // curr_state_tree.right = Some(Box::new(right_tree));
+
+            report.set_left(left_tree_ref)
+                .set_right(right_tree_ref)
+
+        } else {
+            let left_tree = StateTree::from((curr_state.clone(), None));
+            let left_tree_ref = self.states.insert_left_of(left_tree, curr_state_id.id());
+            //curr_state_tree.left = Some(Box::new(left_tree));
+
+            report.set_left(left_tree_ref)
+        }
+
+
+    }
+}
+

src/instruction/mod.rs

@@ -1444,7 +1444,16 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
             Instruction::Create => todo!(),
             Instruction::Call => todo!(),
             Instruction::CallCode => todo!(),
-            Instruction::Return => todo!(),
+            Instruction::Return => {
+                MachineRecord {
+                    mem: None,
+                    stack: None,
+                    storage: None,
+                    pc: (mach.pc(), mach.pc()),
+                    constraints: None,
+                    halt: true,
+                }
+            },
             Instruction::DelegateCall => todo!(),
             Instruction::Create2 => todo!(),
             Instruction::StaticCall => todo!(),

src/lib.rs

@@ -12,6 +12,7 @@ pub mod traits;
 pub mod conversion;
 pub mod storage;
 pub mod parser;
+pub mod exec;
 use paste::{expr, item, paste};
 use instruction::*;
 use smt::*;