ipsilon / eof

Validation code for the EOF specification
Apache License 2.0
43 stars 19 forks source link

question: Validating instruction and stack after terminating opcode #75

Closed rakita closed 7 months ago

rakita commented 7 months ago

First question: I see that we dont reset the successor_stack_height after termination opcode, this would mean that we would increment its max value. Not sure if this is correct?

Second question: I see in spec that "no instruction may be unreachable", do we validate if opcodes are accessible after RJUMP or termination opcode. i dont see that part in the code, is it maybe covered by code below by making StackHeightRange::max initialise to a big number:

https://github.com/ethereum/evmone/blob/master/lib/evmone/eof.cpp#L520-L521|

Third one: I see that in MegaEOF spec: "Code basic blocks must be ordered in a way that every block is reachable either by a forward jump or sequential flow of instructions. In other words, there is no basic block reachable only by a backward jump." https://notes.ethereum.org/@ipsilon/mega-eof-specification i can't find this check in code. validate_rjump_destinations checks validity of jumps but not if it is touching every instruction only with a forward jump.

gumb0 commented 7 months ago

First question: I see that we dont reset the successor_stack_height after termination opcode, this would mean that we would increment its max value. Not sure if this is correct?

I don't think there is a problem. On termination instruction none of the successor instruction heights are updated (because there are no successors), then when it gets to the next instruction, it must already be visited and current stack height is read from saved earlier value:

https://github.com/ethereum/evmone/blob/7bd7596c2754229f37344e10cdd49d638391f90f/lib/evmone/eof.cpp#L377

Second question: I see in spec that "no instruction may be unreachable", do we validate if opcodes are accessible after RJUMP or termination opcode. i dont see that part in the code, is it maybe covered by code below by making StackHeightRange::max initialise to a big number:

This check covers unreachable code: https://github.com/ethereum/evmone/blob/7bd7596c2754229f37344e10cdd49d638391f90f/lib/evmone/eof.cpp#L378-L383 All instructions are inspected sequentially, and if we reached an instruction that was not jumped to from earlier code, it is unreachable, due to the rule you mention in third question.

https://github.com/ethereum/evmone/blob/master/lib/evmone/eof.cpp#L520-L521|

This line just finds the max value in stack_heights.

Third one: I see that in MegaEOF spec: "Code basic blocks must be ordered in a way that every block is reachable either by a forward jump or sequential flow of instructions. In other words, there is no basic block reachable only by a backward jump." https://notes.ethereum.org/@ipsilon/mega-eof-specification i can't find this check in code. validate_rjump_destinations checks validity of jumps but not if it is touching every instruction only with a forward jump.

It's basically the same check for unreachable code.

If there is instruction reachable only by backwards jump, when we sequentially inspect every instruction and we reach this instruction, it's stack_height will be still LOC_UNVISITED, so then this code is unreachable according to this rule.

rakita commented 7 months ago

@gumb0 thank you for responding, it helped me figure out what I was missing and understand it better!