[FEAT] Extensible Execution Strategies

[iamrecursion]

Description

With #47 merged, execution is now no longer total to ensure that it remains tractable to compute even on deeply-nested contracts. Instead, I am proposing an extensible mechanism for execution oracles that determine exactly how execution takes place.

These oracles would determine whether a given opcode gets executed through querying both their own state and the state of the virtual machine. Examples are:

• Limited JUMPDEST Branching: A global limit on how many times a JUMPDEST can create a branch when targeted by JUMPI (the current strategy).
• Stochastic Analysis: Spawn n threads all at the start of the bytecode. When encountering a JUMPI, deterministically flip a coin to determine whether the condition is true or false.
• Every Instruction Once: Visit every single reachable instruction in the contract exactly once (what we originally did, quite expensive but useful).
• Same Path Only: When a VMThread is forked at a JUMPI, track the thread that took the jump and the thread that does not. If that thread ever encounters the jump again, it must take the same path. It does this up to n times.
• Random Jump Target: At a JUMP, pick a random JUMPDEST that has not yet been visited. This risks introducing type incoherence, but means we get potentially better coverage.

Spec

• Implement a trait for ExecutionOracle similar to the following

pub trait ExecutionOracle {
  type ForkOutput;

  // Determines both _when_ and _how_ execution is advanced.
  fn advance_execution(&mut self, state: &mut VMState) -> bool;
  
  // Forks the state of the oracle, to allow state bifurcation 
  // when creating new threads of execution if needed. 
  fn fork(&self) -> ForkOutput;
}

• Implement the current execution strategy (limited JUMPDEST branching) as an ExecutionOracle.
• Make it possible to configure and specify one or more oracles when constructing the VM.
• Run the VM separately for each oracle, and combine all the results after execution.