From e53c4c54934b27c2615d7f44d2d21ab2065a7133 Mon Sep 17 00:00:00 2001 From: Jon-Becker Date: Fri, 29 Dec 2023 10:22:36 -0600 Subject: [PATCH] chore(symbolic-exec): consolidate `JUMP`/`JUMPI` logic --- common/src/ether/evm/ext/exec/mod.rs | 149 ++++---------------------- common/src/ether/evm/ext/exec/util.rs | 36 ++++++- 2 files changed, 58 insertions(+), 127 deletions(-) diff --git a/common/src/ether/evm/ext/exec/mod.rs b/common/src/ether/evm/ext/exec/mod.rs index 1d386a87..779cb88c 100644 --- a/common/src/ether/evm/ext/exec/mod.rs +++ b/common/src/ether/evm/ext/exec/mod.rs @@ -1,15 +1,6 @@ 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::{ @@ -17,7 +8,17 @@ use crate::{ 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, }; @@ -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 ); @@ -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::>(); - - // (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 @@ -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!( @@ -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::>().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 diff --git a/common/src/ether/evm/ext/exec/util.rs b/common/src/ether/evm/ext/exec/util.rs index a8854276..122d1b38 100644 --- a/common/src/ether/evm/ext/exec/util.rs +++ b/common/src/ether/evm/ext/exec/util.rs @@ -1,3 +1,5 @@ +use std::collections::HashMap; + use ethers::types::U256; use crate::{ @@ -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" @@ -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>, +) -> 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::>(); + + // (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. @@ -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 }