Skip to content

Commit

Permalink
Add sparse pc->instruction map
Browse files Browse the repository at this point in the history
  • Loading branch information
WilfredTA committed Aug 2, 2023
1 parent 9ce2d04 commit 55c3861
Show file tree
Hide file tree
Showing 15 changed files with 399 additions and 162 deletions.
18 changes: 12 additions & 6 deletions examples/simple_pgm.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,19 @@ 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();

let leaf = execution_trace.states.leaves();
assert_eq!(1, leaf.len());
let final_tree = leaf.first().unwrap().clone();
let mut mem_val = final_tree.val.mem_read(bvi(0));
mem_val.simplify();
assert_eq!(bvi(66), mem_val);
}

let mut mem_val = final_tree.val.mem_read(bvi(0));
mem_val.simplify();
assert_eq!(bvi(66), mem_val);

let tree_flattened = execution_trace.states.into_iter().collect::<Vec<_>>();
eprintln!("Nodes in tree: {}\nTree Nodes: {:#?}", tree_flattened.len(), tree_flattened);
}
13 changes: 12 additions & 1 deletion examples/simple_storage.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,14 @@ 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());

Expand All @@ -21,3 +24,11 @@ fn main() {
mem_val.simplify();
assert_eq!(bvi(128), mem_val); // 0x80
}

let mut report = std::string::String::default();
// execution.states.into_iter().for_each(|(state, constraint)| {
// report = format!("{}\n{} -- Constraints: {:#?}", report, state, constraint);
// });
//eprintln!("Execution report: {}", report);
eprintln!("Tree: {:#?}", execution.states);
}
4 changes: 2 additions & 2 deletions src/conversion/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -82,8 +82,8 @@ impl<const SZ: usize> From<[u8; SZ]> for BitVec<SZ> {
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());
// 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()
Expand Down
24 changes: 18 additions & 6 deletions src/exec/mod.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
use uuid::Uuid;

use crate::parser::Program;
use crate::state::evm::EvmState;
use crate::state::tree::*;
use crate::{
Expand All @@ -11,7 +12,7 @@ use crate::{
#[derive(Default, Debug)]
pub struct Execution<'ctx> {
changes: Vec<MachineRecord<32>>,
program: Vec<Instruction>,
program: Program,
pub states: StateTree<'ctx>,
}

Expand Down Expand Up @@ -61,7 +62,7 @@ impl StepRecord {
}

impl<'ctx> Execution<'ctx> {
pub fn new(start_state: EvmState, pgm: Vec<Instruction>) -> Self {
pub fn new(start_state: EvmState, pgm: Program) -> Self {
Self {
program: pgm,
states: StateTree::from((start_state, None)),
Expand All @@ -77,8 +78,11 @@ impl<'ctx> Execution<'ctx> {
let curr_inst = curr_state.curr_instruction();
let curr_pc = curr_state.pc();
let change_rec = curr_inst.exec(&curr_state);

eprintln!("CHANGE REC IN EXEC: {:#?}", change_rec);
let is_branch = change_rec.constraints.is_some();
if is_branch {
eprintln!("IS BRANCH HERE:\nChange record {:#?}\nCurr_state pc: {}", change_rec, curr_pc);
}
curr_state.apply_change(change_rec.clone());
let mut report = StepRecord::new(false, change_rec.halt);
if is_branch {
Expand Down Expand Up @@ -158,10 +162,17 @@ 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 is_branch = change_rec.constraints.is_some();
curr_state.apply_change(change_rec.clone());
if is_branch {
eprintln!("IS BRANCH HERE:\nChange record {:#?}\nCurr_state pc: {}", change_rec, curr_pc);
}
if change_rec.halt {
eprintln!("Halt occurred here: {:#?}", change_rec);
}
let curr_state = curr_state;
let mut report = StepRecord::new(false, change_rec.halt);
// assert_eq!(change_rec.halt, curr_state.halt);
Expand All @@ -170,14 +181,15 @@ impl<'ctx> Execution<'ctx> {
// 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();
let right_tree = StateTree::from((left_state.clone(), change_rec.constraints.clone().unwrap()));
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(),
left_state,
change_rec.constraints.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));
Expand Down
Loading

0 comments on commit 55c3861

Please sign in to comment.