Function evmil::analysis::insert_havocs

pub fn insert_havocs(insns: Vec<Instruction>) -> Vec<Instruction>

For a given bytecode sequence, identify and insert havoc instructions to prevent non-termination of more precise analyses. A havoc instruction is needed anywhere the value of a given stack location depends upon itself. This can arise, for example, in loops with code of the form x := x + 1. To understand this, consider the following example:

   push 0x10
loop:
   dup1
   iszero
   push exit
   jumpi
   push 0x1
   swap1
   sub
   push loop
   jump
exit:
   stop

This implements a simple loop which counts down from 0x10 with a counter stored at the bottom of the stack. For a precise analysis which models integer values concretely, this can lead to an infinite ascending chain (i.e. non-termination of the analysis). To resolve this, a havoc statement can be inserted as follows:

  push 0x10
loop:
  havoc 0x0
  ...