Skip to content

Commit

Permalink
chore(symbolic-exec): consolidate JUMP/JUMPI logic
Browse files Browse the repository at this point in the history
  • Loading branch information
Jon-Becker committed Dec 29, 2023
1 parent 9b73388 commit e53c4c5
Show file tree
Hide file tree
Showing 2 changed files with 58 additions and 127 deletions.
149 changes: 23 additions & 126 deletions common/src/ether/evm/ext/exec/mod.rs
Original file line number Diff line number Diff line change
@@ -1,23 +1,24 @@
mod jump_frame;
mod util;

use self::{
jump_frame::JumpFrame,
util::{
historical_diffs_approximately_equal, jump_condition_appears_recursive,
jump_condition_contains_mutated_memory_access,
jump_condition_contains_mutated_storage_access, stack_contains_too_many_of_the_same_item,
stack_diff, stack_item_source_depth_too_deep,
},
};
use crate::{
debug_max,
ether::evm::{
core::{
stack::Stack,
vm::{State, VM},
},
ext::exec::util::stack_contains_too_many_items,
ext::exec::{
jump_frame::JumpFrame,
util::{
historical_diffs_approximately_equal, jump_condition_appears_recursive,
jump_condition_contains_mutated_memory_access,
jump_condition_contains_mutated_storage_access,
jump_stack_depth_less_than_max_stack_depth, stack_contains_too_many_items,
stack_contains_too_many_of_the_same_item, stack_diff,
stack_item_source_depth_too_deep,
},
},
},
utils::strings::decode_hex,
};
Expand Down Expand Up @@ -90,10 +91,11 @@ impl VM {
vm_trace.operations.push(state.clone());
vm_trace.gas_used = vm.gas_used;

// if we encounter a JUMPI, create children taking both paths and break
if state.last_instruction.opcode == 0x57 {
// if we encounter a JUMP(I), create children taking both paths and break
if state.last_instruction.opcode == 0x57 || state.last_instruction.opcode == 0x56 {
debug_max!(
"found branch due to JUMPI instruction at {}",
"found branch due to JUMP{} instruction at {}",
if state.last_instruction.opcode == 0x57 { "I" } else { "" },
state.last_instruction.instruction
);

Expand Down Expand Up @@ -126,26 +128,13 @@ impl VM {
return vm_trace
}

// break out of loops
// (1) get all keys that match jump_frame.pc and jump_frame.jumpdest
let matching_keys = handled_jumps
.keys()
.filter(|key| key.pc == jump_frame.pc && key.jumpdest == jump_frame.jumpdest)
.collect::<Vec<&JumpFrame>>();

// (a) get the max stack_depth of all matching keys
let max_stack_depth =
matching_keys.iter().map(|key| key.stack_depth).max().unwrap_or(0);

// (b) if the current stack depth is less than the max stack depth, we don't need to
// continue.
if jump_frame.stack_depth < max_stack_depth {
debug_max!("jump matches loop-detection heuristic: 'jump_stack_depth_less_than_max_stack_depth'");
debug_max!("jump terminated.");
// if the jump stack depth is less than the max stack depth of all previous matching
// jumps, it's probably a loop
if jump_stack_depth_less_than_max_stack_depth(&jump_frame, handled_jumps) {
return vm_trace
}

// (2) perform heuristic checks on historical stacks
// perform heuristic checks on historical stacks
match handled_jumps.get_mut(&jump_frame) {
Some(historical_stacks) => {
// for every stack that we have encountered for this jump, perform some
Expand Down Expand Up @@ -245,6 +234,10 @@ impl VM {
}
}

if state.last_instruction.opcode == 0x56 {
continue
}

// we didnt break out, so now we crate branching paths to cover all possibilities
*branch_count += 1;
debug_max!(
Expand Down Expand Up @@ -275,102 +268,6 @@ impl VM {
}
}

// if we encounter a JUMP
if state.last_instruction.opcode == 0x56 {
// build hashable jump frame
let jump_frame = JumpFrame::new(
state.last_instruction.instruction,
state.last_instruction.inputs[0],
vm.stack.size(),
true,
);

// if the stack contains too many items, it's probably a loop
if stack_contains_too_many_items(&vm.stack) {
return vm_trace
}

// if the stack has over 16 items of the same source, it's probably a loop
if stack_contains_too_many_of_the_same_item(&vm.stack) {
return vm_trace
}

// if any item on the stack has a depth > 16, it's probably a loop (because of stack
// too deep)
if stack_item_source_depth_too_deep(&vm.stack) {
return vm_trace
}

// perform heuristic checks on historical stacks
match handled_jumps.get_mut(&jump_frame) {
Some(historical_stacks) => {
// for every stack that we have encountered for this jump, perform some
// heuristic checks to determine if this might be a loop
if historical_stacks.iter().any(|hist_stack| {
// check if any historical stack is the same as the current stack
if hist_stack == &vm.stack {
debug_max!(
"jump matches loop-detection heuristic: 'jump_path_already_handled'"
);
return true
}

// calculate the difference of the current stack and the historical stack
let stack_diff = stack_diff(&vm.stack, hist_stack);
if stack_diff.is_empty() {
// the stack_diff is empty (the stacks are the same), so we've
// already handled this path
debug_max!(
"jump matches loop-detection heuristic: 'stack_diff_is_empty'"
);
return true
}

debug_max!("stack diff: [{}]", stack_diff.iter().map(|frame| format!("{}", frame.value)).collect::<Vec<String>>().join(", "));

false
}) {
debug_max!("jump terminated.");
debug_max!(
"adding historical stack {} to jump frame {:?}",
&format!("{:#016x?}", vm.stack.hash()),
jump_frame
);

// this key exists, but the stack is different, so the jump is new
historical_stacks.push(vm.stack.clone());
return vm_trace
}

if historical_diffs_approximately_equal(&vm.stack, historical_stacks) {
debug_max!("jump terminated.");
debug_max!(
"adding historical stack {} to jump frame {:?}",
&format!("{:#016x?}", vm.stack.hash()),
jump_frame
);

// this key exists, but the stack is different, so the jump is new
historical_stacks.push(vm.stack.clone());
return vm_trace
} else {
debug_max!(
"adding historical stack {} to jump frame {:?}",
&format!("{:#016x?}", vm.stack.hash()),
jump_frame
);
// this key exists, but the stack is different, so the jump is new
historical_stacks.push(vm.stack.clone());
}
}
None => {
// this key doesnt exist, so the jump is new
debug_max!("added new jump frame: {:?}", jump_frame);
handled_jumps.insert(jump_frame, vec![vm.stack.clone()]);
}
}
}

// when the vm exits, this path is complete
if vm.exitcode != 255 || !vm.returndata.is_empty() {
break
Expand Down
36 changes: 35 additions & 1 deletion common/src/ether/evm/ext/exec/util.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
use std::collections::HashMap;

use ethers::types::U256;

use crate::{
Expand All @@ -7,6 +9,8 @@ use crate::{
utils::io::logging::Logger,
};

use super::jump_frame::JumpFrame;

/// Given two stacks A and B, return A - B, i.e. the items in A that are not in B.
/// This operation takes order into account, so if A = [1, 2, 3] and B = [1, 3, 2], then A - B =
/// [2]. This is referred to as the "stack diff"
Expand Down Expand Up @@ -34,6 +38,36 @@ pub fn stack_contains_too_many_items(stack: &Stack) -> bool {
false
}

/// Check if the current jump frame has a stack depth less than the max stack depth of all previous
/// matching jumps. If yes, the stack is not growing and we likely have a loop.
pub fn jump_stack_depth_less_than_max_stack_depth(
current_jump_frame: &JumpFrame,
handled_jumps: &HashMap<JumpFrame, Vec<Stack>>,
) -> bool {
// (1) get all keys that match current_jump_frame.pc and current_jump_frame.jumpdest
let matching_keys = handled_jumps
.keys()
.filter(|key| {
key.pc == current_jump_frame.pc && key.jumpdest == current_jump_frame.jumpdest
})
.collect::<Vec<&JumpFrame>>();

// (a) get the max stack_depth of all matching keys
let max_stack_depth = matching_keys.iter().map(|key| key.stack_depth).max().unwrap_or(0);

// (b) if the current stack depth is less than the max stack depth, we don't need to
// continue.
if current_jump_frame.stack_depth < max_stack_depth {
debug_max!(
"jump matches loop-detection heuristic: 'jump_stack_depth_less_than_max_stack_depth'"
);
debug_max!("jump terminated.");
return true
}

false
}

/// Check if the given stack contains too many of the same item.
/// If the stack contains more than 16 of the same item (with the same sources), it is considered a
/// loop.
Expand Down Expand Up @@ -162,7 +196,7 @@ pub fn historical_diffs_approximately_equal(stack: &Stack, historical_stacks: &[
}

// check if all stack diffs are the same
if !stack_diffs.iter().all(|diff| diff[0] == stack_diffs[0][0]) {
if !stack_diffs.iter().all(|diff| diff.get(0) == stack_diffs.get(0).unwrap_or(&vec![]).get(0)) {
return false
}

Expand Down

0 comments on commit e53c4c5

Please sign in to comment.