Skip to content

Commit

Permalink
code cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@WilfredTA
WilfredTA committed Aug 2, 2023
1 parent 3af822a commit 9ce2d04
Show file tree
Hide file tree
Showing 18 changed files with 430 additions and 502 deletions.
17 changes: 3 additions & 14 deletions examples/simple_pgm.rs
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,9 @@


#![allow(unused_imports)]
use ser::{
traits::*,
machine::*,
stack::*,
storage::*,
memory::*,
conversion::*,
bvc,
bvi,
parser::*,
bvc, bvi, conversion::*, machine::*, memory::*, parser::*, stack::*, storage::*, traits::*,
};
use z3::ast::*;


pub const SUPERSIMPLE: &str = r#"604260005260206000F3"#;
fn main() {
let pgm = Parser::with_pgm(SUPERSIMPLE).parse();
Expand All @@ -23,8 +13,7 @@ fn main() {
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);
Expand Down
23 changes: 6 additions & 17 deletions examples/simple_storage.rs
View file
Original file line number Diff line number Diff line change
@@ -1,33 +1,22 @@


#![allow(unused_imports)]
use ser::{
traits::*,
machine::*,
stack::*,
storage::*,
memory::*,
conversion::*,
bvc,
bvi,
parser::*,
bvc, bvi, conversion::*, machine::*, memory::*, parser::*, stack::*, storage::*, traits::*,
};
use z3::ast::*;

pub const STORAGE_SIMPLE: &str = r#"6080604052348015600f57600080fd5b506004361060325760003560e01c80631ab06ee5146037578063fac333ac146056575b600080fd5b605460423660046085565b60009182526020829052604090912055565b005b6073606136600460a6565b60006020819052908152604090205481565b60405190815260200160405180910390f35b60008060408385031215609757600080fd5b50508035926020909101359150565b60006020828403121560b757600080fd5b503591905056fea26469706673582212204a6bf5c04a6e273d775914b20b0bab1bca28228be5562d496002981e13ff015264736f6c63430008130033"#;

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
Expand Down
60 changes: 30 additions & 30 deletions src/conversion/mod.rs
View file
Original file line number Diff line number Diff line change
@@ -1,22 +1,27 @@
use std::cmp::Ordering;

use ruint::{uint, Uint, ToUintError, FromUintError, Bits};
use rlp::{Encodable, Decodable};
use z3_ext::{ast::Ast, Context};
use crate::{
bvc, bvi, bvi_8byte, ctx,
instruction::{push32, Instruction},
parser::zero_extend,
record::push,
BVType, BitVec, BV,
};
use rlp::{Decodable, Encodable};
use ruint::{uint, Bits, FromUintError, ToUintError, Uint};
use serde::{Deserialize, Serialize};
use crate::{BV, BVType, BitVec, bvc, bvi, ctx, bvi_8byte, parser::zero_extend, record::push, instruction::{push32, Instruction}};
use z3_ext::{ast::Ast, Context};

impl From<Uint<256, 4>> for BitVec<32> {
fn from(value: Uint<256, 4>) -> Self {
let mut bv: BV<'static> = BV::from_u64(ctx(), 0, 8);
let bytes: [u8; 32] = value.clone().to_be_bytes();

for i in bytes.iter() {
let new_bv: BV<'static> = bvi::<1>(*i).into();
bv = bv.concat(&new_bv).simplify();
}
bv.extract(256 - 8 - 1, 0).simplify().into()
let mut bv: BV<'static> = BV::from_u64(ctx(), 0, 8);
let bytes: [u8; 32] = value.clone().to_be_bytes();

for i in bytes.iter() {
let new_bv: BV<'static> = bvi::<1>(*i).into();
bv = bv.concat(&new_bv).simplify();
}
bv.extract(256 - 8 - 1, 0).simplify().into()
}
}

Expand All @@ -29,13 +34,10 @@ impl From<BitVec<32>> for Uint<256, 4> {
let offset = 256 - (i * 8) - 1;
let byte_extract: BV<'static> = value.extract(offset, offset - 7).simplify();
// since byte_extract is a single byte, downcasting to u8 will not change the number
let byte = byte_extract.as_u64().unwrap() as u8;
let byte = byte_extract.as_u64().unwrap() as u8;
numbits[i as usize] = byte;


}
Bits::from_be_bytes(numbits).as_uint().clone()

}
}

Expand Down Expand Up @@ -74,17 +76,17 @@ impl<const SZ: usize> From<BitVec<SZ>> for BV<'static> {
impl<const SZ: usize> From<[u8; SZ]> for BitVec<SZ> {
fn from(value: [u8; SZ]) -> Self {
let ctx: &'static Context = ctx();
let mut bv: BV<'static> = BV::from_u64(ctx, 0, 8);

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();
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()
}
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 All @@ -111,12 +113,12 @@ fn test_slice_to_op_arg() {
#[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();
let bv_as_num: Uint<256, 4> = bv.into();
assert_eq!(num, bv_as_num);
}

Expand Down Expand Up @@ -144,7 +146,6 @@ fn test_to_bv() {
let mut expected = bvi(9);
expected.simplify();
assert_eq!(expected, bv_2);

}

#[test]
Expand All @@ -153,5 +154,4 @@ fn test_from_bv() {
let num = uint!(0x000000000000000000000000000000000000000000000000000000000004FD58_U256);
let bv_to_num: Uint<256, 4> = bv.into();
assert_eq!(num, bv_to_num);

}
}
82 changes: 41 additions & 41 deletions src/exec/mod.rs
View file
Original file line number Diff line number Diff line change
@@ -1,34 +1,34 @@
use uuid::Uuid;

use crate::{record::{
MachineRecord
}, instruction::Instruction, traits::{MachineInstruction, MachineComponent, MachineState}};
use crate::state::evm::EvmState;
use crate::state::tree::*;

use crate::{
instruction::Instruction,
record::MachineRecord,
traits::{MachineComponent, MachineInstruction, MachineState},
};

#[derive(Default, Debug)]
pub struct Execution<'ctx> {
changes: Vec<MachineRecord<32>>,
program: Vec<Instruction>,
pub states: StateTree<'ctx>
pub states: StateTree<'ctx>,
}

#[derive(Default, Debug)]
pub struct StepRecord

{
pub struct StepRecord {
left_insert: Option<NodeId>,
right_insert: Option<NodeId>,
halted_left: bool,
halted_right: bool
halted_right: bool,
}

impl StepRecord {

pub fn new(halted_left: bool, halted_right: bool) -> Self {
Self {
halted_left, halted_right, ..Default::default()
halted_left,
halted_right,
..Default::default()
}
}
pub fn halted_left(&self) -> bool {
Expand Down Expand Up @@ -61,7 +61,6 @@ impl StepRecord {
}

impl<'ctx> Execution<'ctx> {

pub fn new(start_state: EvmState, pgm: Vec<Instruction>) -> Self {
Self {
program: pgm,
Expand All @@ -71,7 +70,8 @@ impl<'ctx> Execution<'ctx> {
}

// Returns the StepRecord AND updates the Exec state tree
pub fn step_mut(&mut self) -> StepRecord { // bool returns if there is a branch
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();
Expand All @@ -90,29 +90,30 @@ impl<'ctx> Execution<'ctx> {
if !left_state.can_continue() {
report.halted_left = true;
}

let left_tree = StateTree::from((left_state.clone(), change_rec.constraints.clone().unwrap().not()));

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
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();
Expand All @@ -131,29 +132,30 @@ impl<'ctx> Execution<'ctx> {
if !left_state.can_continue() {
report.halted_left = true;
}
let left_tree = StateTree::from((left_state.clone(), change_rec.constraints.clone().unwrap().not()));
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())

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);
Expand All @@ -162,34 +164,32 @@ impl<'ctx> Execution<'ctx> {
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);
// 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 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)

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)
}


}
}

Loading

0 comments on commit 9ce2d04

Please sign in to comment.