Large EVM refactor

[feliam]

WIP
It make storage and memory be raw smtlib arrays.

• This enables to have unconstrained symbolic indexes. (previously we solved symbolic indexes eagerly)
• EVM internal api evm_cpu vs evm_world improved
• EVM basic block to smtlib. Arbitrary reasoning over EVM traces.
• Initial symbolic gas support. Gas restricts memory access on a memory read over a free symbolic index. Example: With a gas budget of 99, MREAD(free_symbolic_index) can not really read any memory offset but jjust the ones that it has enough gas for.
• world.transactions history can be queried from API/Detectors
• Instructions continuations. For example CALL has 2 versions one that runs before the tx and one that runs after it.
• Detector for simple integration test
  Fixes symbolic memory research #736
• LInk with special Manticore Library (like klee special functions)

$ python asm_to_smtlib.py 
CODE:
	0 PUSH1 0x60
	2 PUSH1 0x40
	4 MSTORE
	5 PUSH1 0x0
	7 DUP1
	8 PUSH1 0x14
	10 PUSH2 0x100
	13 EXP
	14 DUP2
	15 SLOAD
	16 DUP2
	17 PUSH1 0xff
	19 MUL
	20 NOT
	21 AND
	22 SWAP1
	23 DUP4
	24 ISZERO
	25 ISZERO
	26 MUL
	27 OR
	28 SWAP1
	29 SSTORE
	30 POP
	31 CALLVALUE
	32 ISZERO
	33 PUSH2 0x29
	36 JUMPI
STORAGE = (store STORAGE #x0000000000000000000000000000000000000000000000000000000000000000 (bvand (select STORAGE #x0000000000000000000000000000000000000000000000000000000000000000) #xffffffffffffffffffffff00ffffffffffffffffffffffffffffffffffffffff))
MEM = (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store EMPTY_MEMORY_13 #x0000000000000000000000000000000000000000000000000000000000000040 #x00) #x0000000000000000000000000000000000000000000000000000000000000041 #x00) #x0000000000000000000000000000000000000000000000000000000000000042 #x00) #x0000000000000000000000000000000000000000000000000000000000000043 #x00) #x0000000000000000000000000000000000000000000000000000000000000044 #x00) #x0000000000000000000000000000000000000000000000000000000000000045 #x00) #x0000000000000000000000000000000000000000000000000000000000000046 #x00) #x0000000000000000000000000000000000000000000000000000000000000047 #x00) #x0000000000000000000000000000000000000000000000000000000000000048 #x00) #x0000000000000000000000000000000000000000000000000000000000000049 #x00) #x000000000000000000000000000000000000000000000000000000000000004a #x00) #x000000000000000000000000000000000000000000000000000000000000004b #x00) #x000000000000000000000000000000000000000000000000000000000000004c #x00) #x000000000000000000000000000000000000000000000000000000000000004d #x00) #x000000000000000000000000000000000000000000000000000000000000004e #x00) #x000000000000000000000000000000000000000000000000000000000000004f #x00) #x0000000000000000000000000000000000000000000000000000000000000050 #x00) #x0000000000000000000000000000000000000000000000000000000000000051 #x00) #x0000000000000000000000000000000000000000000000000000000000000052 #x00) #x0000000000000000000000000000000000000000000000000000000000000053 #x00) #x0000000000000000000000000000000000000000000000000000000000000054 #x00) #x0000000000000000000000000000000000000000000000000000000000000055 #x00) #x0000000000000000000000000000000000000000000000000000000000000056 #x00) #x0000000000000000000000000000000000000000000000000000000000000057 #x00) #x0000000000000000000000000000000000000000000000000000000000000058 #x00) #x0000000000000000000000000000000000000000000000000000000000000059 #x00) #x000000000000000000000000000000000000000000000000000000000000005a #x00) #x000000000000000000000000000000000000000000000000000000000000005b #x00) #x000000000000000000000000000000000000000000000000000000000000005c #x00) #x000000000000000000000000000000000000000000000000000000000000005d #x00) #x000000000000000000000000000000000000000000000000000000000000005e #x00) #x000000000000000000000000000000000000000000000000000000000000005f #x60)
CONSTRAINTS:

PC: [41, 37]

---

This change is 

[offlinemark]

😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱 😱