Co-authored-by: Daejun Park <[email protected]>

Co-authored-by: karmacoma <[email protected]>

Co-authored-by: Daejun Park <[email protected]>

Co-authored-by: Daejun Park <[email protected]>

+ reorganize main loop to reduce indentation level

Co-authored-by: karmacoma <[email protected]>
Co-authored-by: Daejun Park <[email protected]>

Introduces models for call contexts, messages and call outputs. Depending on the verbosity level, we now render a an execution trace for counterexample paths, setUp() + explored paths and test deployment (constructor) path.

This also introduces a number of semantic fixes related to context handling, such as:
- max call depth
- forbidden opcodes in static context
- reading returndata out of bounds reverts
 
Additionally we now have better handling of exceptions for control flow: we can halt the current context by raising a subclass of EvmException, or halt the current path by raising a subclass of HalmosException.

Co-authored-by: Daejun Park <[email protected]>

Includes a bunch of things:

    type based counterexample rendering (different rendering for uints, signed ints, address, bool, bytes, string, bytes32...)
    console.log functions leverage the same type based rendering
    includes a bunch of new console.log functions + tests
    updates to latest halmos-cheatcode, implements the new cheatcodes (createInt, createInt256, createBytes4, createString) and add tests for these functions

Plus some internal reorganizing:

    move utils-like functions from sevm.py to utils.py
    move cheatcode and console.log handling logic from sevm.py to cheatcodes.py and console.py
    switch to a lookup+handler based mechanism in console and halmos_cheat_code

Co-authored-by: Antonio Viggiano <[email protected]>