Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3,538 changes: 831 additions & 2,707 deletions Cargo.lock

Large diffs are not rendered by default.

2 changes: 0 additions & 2 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -20,11 +20,9 @@ revm = { version = "2.3", default-features = false, features = [
"memory_limit",
"optional_eip3607"
] }
ethers-solc = { git = "https://github.com/gakonst/ethers-rs", features = ["full"]}
paste = "1.0.12"
rlp = "0.5.2"
serde = "1.0.164"
backtrace-on-stack-overflow = "0.3.0"
justerror = "1.1.0"
thiserror = "1.0.44"

Expand Down
2 changes: 1 addition & 1 deletion LICENSE
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
MIT License

Copyright (c) 2023 Tannr Allard
Copyright (c) 2023-2024 Tannr Allard

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
Expand Down
2 changes: 1 addition & 1 deletion examples/simple_storage.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ fn main() {
println!("traces: {:#?}", traces);
let reverted_traces = traces
.into_iter()
.filter(|t| *t.last().unwrap().clone() == Instruction::Revert)
.filter(|t| *t.last().unwrap().to_owned() == Instruction::Revert)
.collect::<Vec<_>>();
println!("TRACES WITH REVERTS {:#?}", reverted_traces);
}
11 changes: 7 additions & 4 deletions examples/simple_storage_deploy.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,11 @@ fn main() {
let mem_val_leaf_2 = leaf.get(1).unwrap().val.mem();
println!("MEM SIZE: {}", mem_val_leaf_2.size());
println!("MEM M_SIZE: {}", mem_val_leaf_2.m_size());

println!("LEAF 2 MEMORY CONCATENATED: {}", mem_val_leaf_2.memory_string());

println!(
"LEAF 2 MEMORY CONCATENATED: {}",
mem_val_leaf_2.memory_string()
);
}

let reachability_report = Evm::exec_check(execution);
Expand All @@ -32,7 +35,7 @@ fn main() {
println!("traces: {:#?}", traces);
let reverted_traces = traces
.into_iter()
.filter(|t| *t.last().unwrap().clone() == Instruction::Revert)
.filter(|t| *t.last().unwrap().to_owned() == Instruction::Revert)
.collect::<Vec<_>>();
println!("TRACES WITH REVERTS {:#?}", reverted_traces);
}
}
7 changes: 3 additions & 4 deletions examples/simple_token.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,11 +21,10 @@ fn main() {

let execution = evm.exec();
{
// eprintln!("STATE TREE: {:#?}", execution.states);
// eprintln!("STATE TREE: {:#?}", execution.states);
let leaf = execution.states.leaves();
eprintln!("LEAVES: {:#?}", leaf);
assert_eq!(14, leaf.len());

}

let reachability_report = Evm::exec_check(execution);
Expand All @@ -37,8 +36,8 @@ fn main() {
eprintln!("traces: {:#?}", traces);
let reverted_traces = traces
.into_iter()
.filter(|t| *t.last().unwrap().clone() == Instruction::Revert)
.filter(|t| *t.last().unwrap().to_owned() == Instruction::Revert)
.collect::<Vec<_>>();
eprintln!("TRACES WITH REVERTS {:#?}", reverted_traces);
//assert_eq!(8, reverted_traces.len());
}
}
2 changes: 1 addition & 1 deletion src/conversion/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ impl From<BitVec<32>> for Uint<256, 4> {
let byte = byte_extract.as_u64().unwrap() as u8;
numbits[i as usize] = byte;
}
Bits::from_be_bytes(numbits).as_uint().clone()
*Bits::from_be_bytes(numbits).as_uint()
}
}

Expand Down
17 changes: 10 additions & 7 deletions src/exec/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ impl<'ctx> Execution<'ctx> {
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, &env);
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 {
Expand Down Expand Up @@ -126,7 +126,7 @@ impl<'ctx> Execution<'ctx> {
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, &env);
let change_rec = curr_inst.exec(&curr_state, env);

let is_branch = change_rec.constraints.is_some();
curr_state.apply_change(change_rec.clone());
Expand Down Expand Up @@ -168,12 +168,15 @@ 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, &env);

let change_rec = curr_inst.exec(curr_state, env);

eprintln!("CHANGE REC IN STEP: {:#?}", change_rec);
eprintln!("Instruction: {:#?} STACK: {:#?}, ",curr_inst, curr_state.stack());

eprintln!(
"Instruction: {:#?} STACK: {:#?}, ",
curr_inst,
curr_state.stack()
);

let is_branch = change_rec.constraints.is_some();
curr_state.apply_change(change_rec.clone());
Expand Down
68 changes: 27 additions & 41 deletions src/instruction/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,15 +21,12 @@ use crate::{
stack::Stack,
};

use justerror::Error;
use super::smt::*;

use justerror::Error;

#[Error]
pub enum InstructionError {
StackEmpty{
pc: usize,
}
StackEmpty { pc: usize },
}
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Instruction {
Expand Down Expand Up @@ -670,7 +667,7 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
halt: false,
storage: None,
}
},
}
Instruction::Balance => {
let stack = mach.stack();
let addr = stack.peek().unwrap();
Expand Down Expand Up @@ -705,7 +702,7 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
}
Instruction::Caller => {
let stack = mach.stack();
let caller = env.caller();//caller().apply(&[]).as_bv().unwrap();
let caller = env.caller(); //caller().apply(&[]).as_bv().unwrap();
let stack_diff = StackChange::with_ops(vec![pop(), push(caller)]);

MachineRecord {
Expand Down Expand Up @@ -772,15 +769,17 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
src_offset.simplify();
size.simplify();
// eprintln!("MACH PC: {:#?}", mach.pc());
// eprintln!("MEM DEST OFFSET {:#?}, MEM READ OFFSET: {:#?}, MEM ITEM SIZE: {:#?}, MEM SIZE: {:#?}",
// dest_offset,
// src_offset,
// usize::from(size.clone()),
// eprintln!("MEM DEST OFFSET {:#?}, MEM READ OFFSET: {:#?}, MEM ITEM SIZE: {:#?}, MEM SIZE: {:#?}",
// dest_offset,
// src_offset,
// usize::from(size.clone()),
// mach.mem().m_size());
// eprintln!("TOTAL CODE BYTE LEN: {:#?}, TOTAL CODE SIZE: {:#?}", mach.pgm.bytes.len(), mach.pgm.get_size());

let code_last_idx_to_read = usize::from(src_offset.clone()) + usize::from(size.clone());
let code = &mach.pgm.bytes[src_offset.clone().into()..code_last_idx_to_read].to_vec();
let code_last_idx_to_read =
usize::from(src_offset.clone()) + usize::from(size.clone());
let code =
&mach.pgm.bytes[src_offset.clone().into()..code_last_idx_to_read].to_vec();
//eprintln!("CODE SIZE: {:#?}", code.len());
let mut i: usize = 0;
let mut mem_ops = vec![];
Expand All @@ -790,35 +789,28 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
}
let offset_add: BitVec<32> = bvi(i as i32);
let mut idx = (dest_offset.as_ref().bvadd(offset_add.as_ref())).simplify();
mem_ops.push(
MemOp::WriteByte { idx: idx.into(), val: code.get(i).expect(
&format!("Couldnt get code byte at index {}", i)
).clone() }
);

mem_ops.push(MemOp::WriteByte {
idx: idx.into(),
val: code
.get(i)
.unwrap_or_else(|| panic!("Couldnt get code byte at index {}", i))
.clone(),
});

i += 1;
}
let stack_change = StackChange::with_ops(
vec![
StackOp::Pop,
StackOp::Pop,
StackOp::Pop
]
);

let stack_change =
StackChange::with_ops(vec![StackOp::Pop, StackOp::Pop, StackOp::Pop]);

MachineRecord {
stack: Some(stack_change),
mem: Some(MemChange {
ops_log: mem_ops
}),
mem: Some(MemChange { ops_log: mem_ops }),
pc: (mach.pc(), mach.pc() + self.byte_size()),
constraints: None,
halt: false,
storage: None,
}


},
}
Instruction::GasPrice => {
let stack = mach.stack();
let price = gas_price().apply(&[]).as_bv().unwrap();
Expand Down Expand Up @@ -1084,9 +1076,8 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
}
}
Instruction::Jump => {

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 {
Expand All @@ -1103,10 +1094,6 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
halt: false,
storage: None,
}




}
Instruction::JumpI => {
let jump_dest = mach.stack().peek().unwrap();
Expand Down Expand Up @@ -1177,8 +1164,7 @@ impl<'ctx> MachineInstruction<'ctx, 32> for Instruction {
storage: None,
constraints: None,
}

},
}
Instruction::JumpDest => MachineRecord {
stack: None,
pc: (mach.pc(), mach.pc() + self.byte_size()),
Expand Down
76 changes: 37 additions & 39 deletions src/machine.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
#![allow(clippy::type_complexity)]
use std::collections::HashMap;
use std::sync::RwLock;
use std::{borrow::BorrowMut, cell::RefCell, rc::Rc};
Expand Down Expand Up @@ -76,7 +77,7 @@ pub struct Evm<'ctx> {
pub states: StateTree<'ctx>,
change_log: Vec<MachineRecord<32>>,
pub inverse_state: HashMap<Uuid, Uuid>,
ctx: RwLock<ExecutionEnv<'ctx>>
ctx: RwLock<ExecutionEnv<'ctx>>,
}

impl<'ctx> Evm<'ctx> {
Expand All @@ -93,7 +94,7 @@ impl<'ctx> Evm<'ctx> {
},
change_log: vec![],
inverse_state: Default::default(),
ctx: RwLock::new(ExecutionEnv::default())
ctx: RwLock::new(ExecutionEnv::default()),
}
}

Expand All @@ -117,7 +118,7 @@ impl<'ctx> Evm<'ctx> {
},
change_log: vec![],
inverse_state: Default::default(),
ctx: RwLock::new(env)
ctx: RwLock::new(env),
}
}

Expand Down Expand Up @@ -218,43 +219,40 @@ impl<'ctx> Machine<32> for Evm<'ctx> {
let first_step = exec.step_mut(self.ctx.read().as_ref().unwrap());
step_recs.push(first_step);
let mut ids = vec![];
loop {
if let Some(step) = step_recs.pop() {
// eprintln!(
// "HALTED LEFT: {}, HALTED RIGHT: {}",
// step.halted_left(),
// step.halted_right()
// );
// eprintln!(
// "LEFT ID: {:#?} RIGHT ID: {:#?}",
// step.left_id(),
// step.right_id()
// );
// if !step.halted_right() {
// 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, 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, self.ctx.read().as_ref().unwrap());
step_recs.push(nxt_step);
}
// }
while let Some(step) = step_recs.pop() {
// eprintln!(
// "HALTED LEFT: {}, HALTED RIGHT: {}",
// step.halted_left(),
// step.halted_right()
// );
// eprintln!(
// "LEFT ID: {:#?} RIGHT ID: {:#?}",
// step.left_id(),
// step.right_id()
// );
// if !step.halted_right() {
// 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, 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, self.ctx.read().as_ref().unwrap());
step_recs.push(nxt_step);
}
// }

if step.halted_left() && step.halted_right() {
eprintln!(
"Both have halted... Here are the step recs left: {:#?}",
step_recs
);
}
} else {
break;
if step.halted_left() && step.halted_right() {
eprintln!(
"Both have halted... Here are the step recs left: {:#?}",
step_recs
);
}
}
eprintln!("All ids that were executed during a step: {:#?}", ids);
Expand Down
Loading