geas icon indicating copy to clipboard operation
geas copied to clipboard

Stack analysis

Open fjl opened this issue 2 years ago • 0 comments

There is a general convention to annotate low level EVM programs with stack comments. It usually looks like this:

    push 10  ; [a]
    push 20  ; [b, a]
    add      ; [sum]
    push 0   ; [addr, sum]
    mstore   ; [] 

Would be nice if the assembler could parse these comments and check if they are correct. The stack effects of opcodes are static and known, so it should be possible to track this.

Verifying the stack correctness of the whole program is a non-goal. Instead, we should go for the best effort thing and only validate that continuous runs of comments are correct. The analysis could just give up when a jumpdest or the end of the current document is reached.

Would also be cool to declare/check the stack effect of instruction macros.

fjl avatar Sep 13 '23 17:09 fjl