Generates a symbolic graph of what happens to various aspects of the EVM.
Tracks history of stack variables & memory* and lets you collapse the history into a single statement like so:
IsZero(Eq(CalldataLoad { offset: Add(CalldataLoad { offset: 0x4 }, 0x4) }, 0x2a))
What this means is effectively:
let a := msg.data[0x4:0x4+32];
0 == (msg.data[a:a+32] == 0x2a)
Additionally integrates with graphviz:
Image from a run against https://github.com/paradigmxyz/paradigm-ctf-2022/blob/main/fun-reversing-challenge/public/contracts/Challenge.sol
Graphviz generation has two modes, cumulative, and incremental. Incremental does no stack history collapsing, while cumulative does.
Very alfa. if you want to use it, currently you have to modify a couple lines:
inc_dec_reset_get
to the bytecode of your contractdata
to be the calldata you want to send to your contractThis will be improved later but low priority while testing & building