New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Subroutines and Static Jumps for the EVM #615

Open
gcolvin opened this Issue Apr 27, 2017 · 25 comments

Comments

Projects
None yet
4 participants
@gcolvin
Collaborator

gcolvin commented Apr 27, 2017

#Current PR: https://github.com/ethereum/EIPs/blob/master/EIPS/eip-615.md
Working draft:

eip: 615
title: Subroutines and Static Jumps for the EVM
discussions-to: https://github.com/ethereum/EIPs/issues/615
status: Draft
type: Standards Track
category: Core
author: Greg Colvin (greg@colvin.org), Paweł Bylica, Christian Reitwiessner
created: 2016-12-10

Simple Summary

This EIP introduces new EVM opcodes and conditions on EVM code to support subroutines and static jumps, disallow dynamic jumps, and thereby make EVM code amenable to linear-time static analysis. This will provide for better compilation, interpretation, transpilation, and formal analysis of EVM code.

Abstract

EVM code is difficult to analyze formally, hobbling a critical tool for preventing the many expensive bugs our blockchain has experienced. And all current implementations of the Ethereum Virtual Machine, including the just-in-time compilers, are much too slow. This proposal identifies a major reason for this and proposes changes to the EVM specification to address the problem.

In particular, it imposes restrictions on current EVM code and proposes new instructions to help provide for

  • better formal analysis tools
  • faster interpretation
  • better-optimized compilation to native code
  • faster transpilation to eWASM
  • better compilation from other languages, including eWASM and Solidity

These goals are achieved by

  • disallowing dynamic jumps
  • introducing subroutines—jumps with return support
  • disallowing pathological control flow and uses of the stack

We also propose to validate—in linear time—that EVM contracts correctly use subroutines, avoid misuse of the stack, and meet other safety conditions before placing them on the blockchain. Validated code precludes most runtime exceptions and the need to test for them. And well-behaved control flow and use of the stack makes life easier for interpreters, compilers, formal analysis, and other tools.

Motivation

Currently the EVM supports dynamic jumps, where the address to jump to is an argument on the stack. These dynamic jumps obscure the structure of the code and thus mostly inhibit control- and data-flow analysis. This puts the quality and speed of optimized compilation fundamentally at odds. Further, since every jump can potentially be to any jump destination in the code, the number of possible paths through the code goes up as the product of the number of jumps by the number of destinations, as does the time complexity of static analysis. But absent dynamic jumps code can be statically analyzed in linear time.

Static analysis includes validation, and much of optimization, compilation, transpilation, and formal analysis; every part of the tool chain benefits when linear-time analysis is available. In particular, faster control-flow analysis means faster compilation of EVM code to native code, and better data-flow analysis can help the compiler and the interpreter better track the size of the values on the stack and use native 64- and 32-bit operations when possible. Also, conditions which are checked at validation time don’t have to be checked repeatedly at runtime.

Note that analyses of a contract’s bytecode before execution—such as optimizations performed before interpretation, JIT compilation, and on-the-fly machine code generation—must be efficient and linear-time. Otherwise, specially crafted contracts can be used as attack vectors against clients that use static analysis of EVM code before the creation or execution of contracts.

Specification

Proposal

We propose to deprecate two existing instructions—JUMP and JUMPI. They take their argument on the stack, which means that unless the value is constant they can jump to any JUMPDEST. (In simple cases like PUSH 0 JUMP the value on the stack can be known to be constant, but in general it's difficult.) We must nonetheless continue to support them in old code.

Having deprecated JUMP and JUMPI, we propose new instructions to support their legitimate uses.

Preliminaries

These forms

  • INSTRUCTION x,
  • INSTRUCTION x, y
  • INSTRUCTION n, x ...
  • INSTRUCTION z ...

name instructions with one, two, and two or more arguments, respectively. An instruction is represented in the bytecode as a single-byte opcode. Any arguments are laid out as immediate data bytes following the opcode inline, interpreted as RLP-encoded, values, sequences, or lists of twos-complement signed integers. (Negative values are reserved for extensions.)

Primitives

The two most important uses of JUMP and JUMPI are static jumps and return jumps. Conditional and unconditional static jumps are the mainstay of control flow. Return jumps are implemented as a dynamic jump to a return address pushed on the stack. With the combination of a static jump and a dynamic return jump you can—and Solidity does—implement subroutines. The problem is that static analysis cannot tell the one place the return jump is going, so it must analyze every possibility.

Static jumps are provided by

  • JUMPTO jump_target
  • JUMPIF jump_target
    which are the same as JUMP and JUMPI except that they jump to an immediate jump_target rather than an address on the stack.

To support subroutines, BEGINSUB, JUMPSUB, and RETURNSUB are provided. Brief descriptions follow, and full semantics are given below.

  • BEGINSUB n_args, n_results
    marks the single entry to a subroutine. n_args items are taken off of the stack at entry to, and n_results items are placed on the stack at return from the subroutine. The subroutine ends at the next BEGINSUB instruction (or `BEGINDATA, below) or at the end of the bytecode.

  • JUMPSUB jump_target
    jumps to an immediate subroutine address.

  • RETURNSUB
    returns from the current subroutine to the instruction following the JUMPSUB that entered it.

These five simple instructions form the primitives of the proposal.

Data

In order to validate subroutines, EVM bytecode must be sequentially scanned matching jumps to their destinations. Since creation code has to contain the runtime code as data, that code might not correctly validate in the creation context and also does not have to be validated prior to the execution of the creation code. Because of that, there needs to be a way to place data into the bytecode that will be skipped over and not validated. Such data will prove useful for other purposes as well.

  • BEGINDATA
    specifies that all of the following bytes to the end of the bytecode are data, and not reachable code.

Indirect Jumps

The primitive operations provide for static jumps. Dynamic jumps are also used for O(1) indirection: an address to jump to is selected to push on the stack and be jumped to. So we also propose two more instructions to provide for constrained indirection. We support these with vectors of JUMPDEST or BEGINSUB offsets stored inline, which can be selected with an index on the stack. That constrains validation to a specified subset of all possible destinations. The danger of quadratic blow up is avoided because it takes as much space to store the jump vectors as it does to code the worst case exploit.

Dynamic jumps to a JUMPDEST are used to implement O(1) jumptables, which are useful for dense switch statements, and are implemented as instructions similar to this one on most CPUs.

  • JUMPV n, jumpdest ...
    jumps to one of a vector of n JUMPDEST offsets via a zero-based index on the stack. The vector is stored inline in the bytecode. If the index is greater than or equal to n - 1 the last (default) offset is used.

Dynamic jumps to a BEGINSUB are used to implement O(1) virtual functions and callbacks, which take just two pointer dereferences on most CPUs.

  • JUMPSUBV n, beginsub ...
    jumps to one of a vector of n BEGINSUB offsets via a zero-based index on the stack. The vector is stored inline in the bytecode, MSB-first. If the index is greater than or equal to n - 1 the last (default) offset is used.

JUMPV and JUMPSUBV are not strictly necessary. They provide O(1) operations that can be replaced by O(n) or O(log n) EVM code using static jumps, but that code will be slower, larger and use more gas for things that can and should be fast, small, and cheap, and that are directly supported in WASM with br_table and call_indirect.

Variable Access

These operations provide convenient access to subroutine parameters and other variables at fixed stack offsets within a subroutine.

  • PUTLOCAL n
    Pops the top value on the stack and copies it to local variable n.
    - The n of stack items below the frame pointer to put a value at.

  • GETLOCAL n
    Pushes the value of local variable n on the stack.
    - The n of stack items below the frame pointer to get a value from.

Local variable n is the n'th stack item below the frame pointer—FP[-n] as defined below.

Semantics

Jumps to and returns from subroutines are described here in terms of

  • the EVM data stack, (as defined in the Yellow Paper) usually just called “the stack”,
  • a return stack of JUMPSUB and JUMPSUBV offsets, and
  • a frame stack of frame pointers.

We will adopt the following conventions to describe the machine state:

  • The program counter PC is (as usual) the byte offset of the currently executing instruction.
  • The stack pointer SP corresponds to the Yellow Paper's substate s of the machine state.
    The stack pointer addresses the current top of the stack of data values, where new items are pushed. The stack grows towards lower addresses.
  • The frame pointer FP is set to SP + n_args at entry to the currently executing subroutine.
  • The stack items between the frame pointer and the current stack pointer are called the frame.
  • The current number of items in the frame, FP - SP, is the frame size.

Defining the frame pointer so as to include the arguments is unconventional, but better fits our stack semantics and simplifies the remainder of the proposal.

The frame pointer and return stacks are internal to the subroutine mechanism, and not directly accessible to the program. This is necessary to prevent the program from modifying its state in ways that could be invalid.

The first instruction of an array of EVM bytecode begins execution of a main routine with no arguments, SP and FP set to 0, and with one value on the return stack—code size - 1. (Executing the virtual byte of 0 after this offset causes an EVM to stop. Thus executing a RETURNSUB with no prior JUMPSUB or JUMBSUBV—that is, in the main routine—executes a STOP.)

Execution of a subroutine begins with JUMPSUB or JUMPSUBV, which

  • push PC on the return stack,
  • push FP on the frame stack,
    thus suspending execution of the current subroutine, and
  • set FP to SP + n_args, and
  • set PC to the specified BEGINSUB address,
    thus beginning execution of the new subroutine.
    (The main routine is not addressable by JUMPSUB instructions.)

Execution of a subroutine is suspended during and resumed after execution of nested subroutines, and ends upon encountering a RETURNSUB, which

  • sets FP to the top of the virtual frame stack and pops the stack, and
  • sets PC to top of the return stack and pops the stack
  • advances PC to the next instruction
    thus resuming execution of the enclosing subroutine or main program.
    A STOP orRETURN` also ends the execution of a subroutine.

For example, after a JUMPSUB to a BEGINSUB 2, 0 like this

PUSH 10
PUSH 11
JUMPSUB _beginsub_
PUSH 12
PUSH 13

the stack looks like this

10 <- FP
11
12
13
   <- SP

Validity

We would like to consider EVM code valid if and only if no execution of the program can lead to an exceptional halting state. But we must and will validate code in linear time. So our validation does not consider the code’s data and computations, only its control flow and stack use. This means we will reject programs with invalid code paths, even if those paths cannot be executed at runtime. Most conditions can be validated, and will not need to be checked at runtime; the exceptions are sufficient gas and sufficient stack. So some false negatives and runtime checks are the price we pay for linear time validation.

Execution is as defined in the Yellow Paper—a sequence of changes in the EVM state. The conditions on valid code are preserved by state changes. At runtime, if execution of an instruction would violate a condition the execution is in an exceptional halting state. The yellow paper defines five such states.

1 Insufficient gas

2 More than 1024 stack items

3 Insufficient stack items

4 Invalid jump destination

5 Invalid instruction

We propose to expand and extend the Yellow Paper conditions to handle the new instructions we propose.

To handle the return stack we expand the conditions on stack size:

2a The size of the data stack does not exceed 1024.

2b The size of the return stack does not exceed 1024.

Given our more detailed description of the data stack we restate condition 3—stack underflow—as

3 SP must be less than or equal to FP

Since the various DUP and SWAP operations—as well as PUTLOCAL and GETLOCAL—are formalized as taking items off the stack and putting them back on, this prevents them from accessing data below the frame pointer, since taking too many items off of the stack would mean that SP is less than FP.

To handle the new jump instructions and subroutine boundaries we expand the conditions on jumps and jump destinations.

4a JUMPTO, JUMPIF, and JUMPV address only JUMPDEST instructions.

4b JUMPSUB and JUMPSUBV address only BEGINSUB instructions.

4c JUMP instructions do not address instructions outside of the subroutine they occur in.

We have two new conditions on execution to ensure consistent use of the stack by subroutines:

6 For JUMPSUB and JUMPSUBV the frame size is at least the n_args of the BEGINSUB(s) to jump to.

7 For RETURNSUB the frame size is equal to the n_results of the enclosing BEGINSUB.

Finally, we have one condition that prevents pathological uses of the stack:

8 For every instruction in the code the frame size is constant.

In practice, we must test at runtime for conditions 1 and 2—sufficient gas and sufficient stack. We don’t know how much gas there will be, we don’t know how deep a recursion may go, and analysis of stack depth even for non-recursive programs is non-trivial.

All of the remaining conditions we validate statically.

Validation

Validation comprises two tasks:

  • Checking that jump destinations are correct and instructions valid.
  • Checking that subroutines satisfy the conditions on control flow and stack use.

We sketch out these two validation functions in pseudo-C below. To simplify the presentation only the five primitives are handled (JUMPV and JUMPSUBV would just add more complexity to loop over their vectors), we assume helper functions for extracting instruction arguments from immediate data and managing the stack pointer and program counter, and some optimizations are forgone.

Validating jumps

Validating that jumps are to valid addresses takes two sequential passes over the bytecode—one to build sets of jump destinations and subroutine entry points, another to check that addresses jumped to are in the appropriate sets.

    bytecode[code_size]   // contains EVM bytecode to validate
    is_sub[code_size]     // is there a BEGINSUB at PC?
    is_dest[code_size]    // is there a JUMPDEST at PC?
    sub_for_pc[code_size] // which BEGINSUB is PC in?
    
    bool validate_jumps(PC)
    {
        current_sub = PC

        // build sets of BEGINSUBs and JUMPDESTs
        for (PC = 0; instruction = bytecode[PC]; PC = advance_pc(PC))
        {
            if instruction is invalid
                return false
            if instruction is BEGINDATA
                break;
            if instruction is BEGINSUB
                is_sub[PC] = true
                current_sub = PC
                sub_for_pc[PC] = current_sub
            if instruction is JUMPDEST
                is_dest[PC] = true
            sub_for_pc[PC] = current_sub
        }
        
        // check that targets are in subroutine
        for (PC = 0; instruction = bytecode[PC]; PC = advance_pc(PC))
        {
            if instruction is BEGINDATA
                break;
            if instruction is BEGINSUB
                current_sub = PC
            if instruction is JUMPSUB
                if is_sub[jump_target(PC)] is false
                    return false
            if instruction is JUMPTO or JUMPIF
                if is_dest[jump_target(PC)] is false
                    return false
            if sub_for_pc[PC] is not current_sub
                return false
       }
        return true
    }

Note that code like this is already run by EVMs to check dynamic jumps, including building the jump destination set every time a contract is run, and doing a lookup in the jump destination set before every jump.

Validating subroutines

This function can be seen as a symbolic execution of a subroutine in the EVM code, where only the effect of the instructions on the state being validated is computed. Thus the structure of this function is very similar to an EVM interpreter. This function can also be seen as an acyclic traversal of the directed graph formed by taking instructions as vertexes and sequential and branching connections as edges, checking conditions along the way. The traversal is accomplished via recursion, and cycles are broken by returning when a vertex which has already been visited is reached. The time complexity of this traversal is O(n-vertices + n-edges)

The basic approach is to call validate_subroutine(i, 0, 0), for i equal to the first instruction in the EVM code through each BEGINDATA offset. validate_subroutine() traverses instructions sequentially, recursing when JUMP and JUMPI instructions are encountered. When a destination is reached that has been visited before it returns, thus breaking cycles. It returns true if the subroutine is valid, false otherwise.

    bytecode[code_size]     // contains EVM bytecode to validate
    frame_size[code_size ]  // is filled with -1

    // we validate each subroutine individually, as if at top level
    // * PC is the offset in the code to start validating at
    // * return_pc is the top PC on return stack that RETURNSUB returns to
    // * at top level FP = SP = 0 is both the frame size and the stack size
    // * as items are pushed SP get more negative, so the stack size is -SP
    validate_subroutine(PC, return_pc, SP)
    {
        // traverse code sequentially, recurse for jumps
        while true
        {
            instruction = bytecode[PC]

            // if frame size set we have been here before
            if frame_size[PC] >= 0
            {
                // check for constant frame size
                if instruction is JUMPDEST
                    if -SP != frame_size[PC]
                        return false

                // return to break cycle
                return true
            }
            frame_size[PC] = -SP

            // effect of instruction on stack
            n_removed = removed_items(instructions)
            n_added = added_items(instruction)

            // check for stack underflow
            if -SP < n_removed
                return false

            // net effect of removing and adding stack items
            SP += n_removed
            SP -= n_added

            // check for stack overflow
            if -SP > 1024
                return false

            if instruction is STOP, RETURN, or SUICIDE
                return true	   

            // violates single entry
            if instruction is BEGINSUB
                 return false

            // return to top or from recursion to JUMPSUB
            if instruction is RETURNSUB
                break;

            if instruction is JUMPSUB
            {
                // check for enough arguments
                sub_pc = jump_target(PC)
                if -SP < n_args(sub_pc)
                    return false
                return true
            }

            // reset PC to destination of jump
            if instruction is JUMPTO
            {
                PC = jump_target(PC)
                continue 
            }

            // recurse to jump to code to validate 
            if instruction is JUMPIF
            {
                if not validate_subroutine(jump_target(PC), return_pc, SP)
                    return false
            }

            // advance PC according to instruction
            PC = advance_pc(PC)
        }

        // check for right number of results
        if (-SP != n_results(return_pc)
            return false
        return true
    }

Costs & Codes

All of the instructions are O(1) with a small constant, requiring just a few machine operations each, whereas a JUMP or JUMPI must do an O(log n) binary search of an array of JUMPDEST offsets before every jump. With the cost of JUMPI being high and the cost of JUMP being mid, we suggest the cost of JUMPV and JUMPSUBV should be mid, JUMPSUB and JUMPIF should be low, andJUMPTO should be verylow. Measurement will tell.

We suggest the following opcodes:

0xb0 JUMPTO
0xb1 JUMPIF
0xb2 JUMPV
0xb3 JUMPSUB
0xb4 JUMPSUBV
0xb5 BEGINSUB
0xb6 BEGINDATA
0xb7 RETURNSUB
0xb8 PUTLOCAL
0xb9 GETLOCAL

Backwards Compatibility

These changes would need to be implemented in phases at decent intervals:

1 If this EIP is accepted, invalid code should be deprecated. Tools should stop generating invalid code, users should stop writing it, and clients should warn about loading it.

2 A later hard fork would require clients to place only valid code on the block chain. Note that despite the fork old EVM code will still need to be supported indefinitely.

If desired, the period of deprecation can be extended indefinitely by continuing to accept code not versioned as new—but without validation. That is, by delaying step 2. Since we must continue to run old code this is not technically difficult.

Implementation

Implementation of this proposal need not be difficult, At the least, interpreters can simply be extended with the new opcodes and run unchanged otherwise. The new opcodes require only stacks for the frame pointers and return offsets and the few pushes, pops, and assignments described above. Compiled code can use native call instructions. Further optimizations include minimizing runtime checks for exceptions and otherwise taking advantage of validated code wherever possible. An untested prototype is available in the lead author's cpp-ethereum repository.

@seed

This comment has been minimized.

Show comment
Hide comment
@seed

seed Nov 13, 2017

This is a very useful proposal, especially for anything that involves decompilation of bytecode.
It would be great to have support for this proposal in the Solidity compiler.

I have a few questions regarding the variable access section.
Is the purpose of GETLOCAL and PUTLOCAL to allow writing more efficient bytecode?
Is the objective to reduce memory accesses by using the stack instead?

seed commented Nov 13, 2017

This is a very useful proposal, especially for anything that involves decompilation of bytecode.
It would be great to have support for this proposal in the Solidity compiler.

I have a few questions regarding the variable access section.
Is the purpose of GETLOCAL and PUTLOCAL to allow writing more efficient bytecode?
Is the objective to reduce memory accesses by using the stack instead?

@gcolvin

This comment has been minimized.

Show comment
Hide comment
@gcolvin

gcolvin Nov 13, 2017

Collaborator

Yeah, it's to support local variables on the stack that are too far away to reach with DUP or SWAP. So more efficient bytecode, and also a better target for transpiling from eWASM.

Collaborator

gcolvin commented Nov 13, 2017

Yeah, it's to support local variables on the stack that are too far away to reach with DUP or SWAP. So more efficient bytecode, and also a better target for transpiling from eWASM.

@seed

This comment has been minimized.

Show comment
Hide comment
@seed

seed Nov 13, 2017

Thanks.

What is the semantics of GETLOCAL n, when n is greater than the number of arguments specified in BEGINSUB? I'd suspect an exception is thrown in that case?

It seems that the number of return variables specified in BEGINSUB, isn't used anywhere.
According to my understanding, whenever we execute a RETSUB, the following should be true: FP - narg + nret == SP. If so, should an EVM interpreter check this and throw an exception otherwise?

seed commented Nov 13, 2017

Thanks.

What is the semantics of GETLOCAL n, when n is greater than the number of arguments specified in BEGINSUB? I'd suspect an exception is thrown in that case?

It seems that the number of return variables specified in BEGINSUB, isn't used anywhere.
According to my understanding, whenever we execute a RETSUB, the following should be true: FP - narg + nret == SP. If so, should an EVM interpreter check this and throw an exception otherwise?

@seed

This comment has been minimized.

Show comment
Hide comment
@seed

seed Nov 13, 2017

Could you please clarify if GETLOCAL n, where n is positive, is accessing an argument or local variable? It seems that the former is true, but it would be good to be more explicit about this in the proposal.

seed commented Nov 13, 2017

Could you please clarify if GETLOCAL n, where n is positive, is accessing an argument or local variable? It seems that the former is true, but it would be good to be more explicit about this in the proposal.

@seed

This comment has been minimized.

Show comment
Hide comment
@seed

seed Nov 13, 2017

Actually, the following is really confusing to me:

Execution of a subroutine begins with JUMPSUB or JUMPSUBV, which
...
set FP to SP + n_args, and

Shouldn't this be rather "set FP to SP" or "set FP to SP - n_args" because the arguments have already been placed on the stack at this point.

seed commented Nov 13, 2017

Actually, the following is really confusing to me:

Execution of a subroutine begins with JUMPSUB or JUMPSUBV, which
...
set FP to SP + n_args, and

Shouldn't this be rather "set FP to SP" or "set FP to SP - n_args" because the arguments have already been placed on the stack at this point.

@gcolvin

This comment has been minimized.

Show comment
Hide comment
@gcolvin

gcolvin Nov 13, 2017

Collaborator

Perhaps, Seed. It confuses me too. It's been a long while since I wrote and implemented this, so it will take a little study. Getting near bedtime here, and I've got 100 miles of driving to get home tomorrow, so please be patient. It's on my stack to do a cleanup pass and new PR for this and 616, so I much appreciate your review. (If you read C++ your questions might be answered in the code at https://github.com/ethereum/cpp-ethereum/tree/develop/libevm)

Collaborator

gcolvin commented Nov 13, 2017

Perhaps, Seed. It confuses me too. It's been a long while since I wrote and implemented this, so it will take a little study. Getting near bedtime here, and I've got 100 miles of driving to get home tomorrow, so please be patient. It's on my stack to do a cleanup pass and new PR for this and 616, so I much appreciate your review. (If you read C++ your questions might be answered in the code at https://github.com/ethereum/cpp-ethereum/tree/develop/libevm)

@seed

This comment has been minimized.

Show comment
Hide comment
@seed

seed Nov 19, 2017

We started specifying the semantics of new instructions in Lem.
See https://github.com/seed/eth-isabelle/blob/evm15/lem/evm.lem

One of the things we noticed is that it makes more sense to setup the stack-frame with the BEGINSUB instruction because we have the number of function arguments at hand. It also makes sense when compared native assembly like x86, where the stack-frame is created in the body of the function, not by the CALL instruction.

I'll be continuing the specification next week and will probably have more comments to make.

seed commented Nov 19, 2017

We started specifying the semantics of new instructions in Lem.
See https://github.com/seed/eth-isabelle/blob/evm15/lem/evm.lem

One of the things we noticed is that it makes more sense to setup the stack-frame with the BEGINSUB instruction because we have the number of function arguments at hand. It also makes sense when compared native assembly like x86, where the stack-frame is created in the body of the function, not by the CALL instruction.

I'll be continuing the specification next week and will probably have more comments to make.

@gcolvin

This comment has been minimized.

Show comment
Hide comment
@gcolvin

gcolvin Nov 19, 2017

Collaborator

You ask

What is the semantics of GETLOCAL n, when n is greater than the number of arguments specified in BEGINSUB?"

It pushes FP[-n] on the stack.
You also ask

According to my understanding, whenever we execute a RETSUB, the following should be true: FP - narg + nret == SP.

Close.
I think both cases are handled by condition 3, that after the execution of an instruction SP <= FP.

Collaborator

gcolvin commented Nov 19, 2017

You ask

What is the semantics of GETLOCAL n, when n is greater than the number of arguments specified in BEGINSUB?"

It pushes FP[-n] on the stack.
You also ask

According to my understanding, whenever we execute a RETSUB, the following should be true: FP - narg + nret == SP.

Close.
I think both cases are handled by condition 3, that after the execution of an instruction SP <= FP.

@gcolvin

This comment has been minimized.

Show comment
Hide comment
@gcolvin

gcolvin Nov 19, 2017

Collaborator

As for setting up the stack frame, the semantics is given as:

Execution of a subroutine begins with JUMPSUB or JUMPSUBV, which

  • push PC on the return stack,
  • push FP on the frame stack,thus suspending execution of the current subroutine, and
  • set FP to SP + n_args, and
  • set PC to the specified BEGINSUB address,
    thus beginning execution of the new subroutine.

I'm not sure it matters where or in what order anything in between encountering the JUMPSUB and executing the BEGINSUB is described as happening, so long as the program winds up executing the instruction after the BEGINSUB with the correct stack. So get the semantics right and we can get the English right.

Collaborator

gcolvin commented Nov 19, 2017

As for setting up the stack frame, the semantics is given as:

Execution of a subroutine begins with JUMPSUB or JUMPSUBV, which

  • push PC on the return stack,
  • push FP on the frame stack,thus suspending execution of the current subroutine, and
  • set FP to SP + n_args, and
  • set PC to the specified BEGINSUB address,
    thus beginning execution of the new subroutine.

I'm not sure it matters where or in what order anything in between encountering the JUMPSUB and executing the BEGINSUB is described as happening, so long as the program winds up executing the instruction after the BEGINSUB with the correct stack. So get the semantics right and we can get the English right.

@gcolvin

This comment has been minimized.

Show comment
Hide comment
@gcolvin

gcolvin Nov 26, 2017

Collaborator

@seed I've edited to make clear that SP is mu-sub-s in the yellow paper, and removed the reference in the text to SP being the stack size. The rest of the pointer arithmetic in the text is (I think) now consistent with the stack growing towards lower addresses, so that positive offsets off the stack pointer and negative offsets off the frame pointer both reach into the stack frame. The validation pseudocode I have not fixed.

Collaborator

gcolvin commented Nov 26, 2017

@seed I've edited to make clear that SP is mu-sub-s in the yellow paper, and removed the reference in the text to SP being the stack size. The rest of the pointer arithmetic in the text is (I think) now consistent with the stack growing towards lower addresses, so that positive offsets off the stack pointer and negative offsets off the frame pointer both reach into the stack frame. The validation pseudocode I have not fixed.

@seed

This comment has been minimized.

Show comment
Hide comment
@seed

seed Dec 3, 2017

Thanks for updating the proposal. It does make a lot more sense.

Note that μs growing towards lower addresses doesn't make much sense to me in the context of the yellow paper because the EVM doesn't expose stack addresses in any way.

Let me try to confirm my understanding of the proposal with an example:
[other subroutines stack frames] [arg1] [arg2] < FP is here > [local1] [local2] <SP/top is here>.

where μs[0] = local2, μs[1] = local1, μs[2] = arg2, ...
and GETLOCAL 0 = arg2, GETLOCAL 1 = arg1
and GETLOCAL -1 = local1, GETLOCAL -2 = local2

Few questions:
Is the above correct?
Is the validation code expected to reject GETLOCAL 3 and GETLOCAL -3?
Are EVM interpreters meant to throw an invalid stack access exception when they encounter these?

seed commented Dec 3, 2017

Thanks for updating the proposal. It does make a lot more sense.

Note that μs growing towards lower addresses doesn't make much sense to me in the context of the yellow paper because the EVM doesn't expose stack addresses in any way.

Let me try to confirm my understanding of the proposal with an example:
[other subroutines stack frames] [arg1] [arg2] < FP is here > [local1] [local2] <SP/top is here>.

where μs[0] = local2, μs[1] = local1, μs[2] = arg2, ...
and GETLOCAL 0 = arg2, GETLOCAL 1 = arg1
and GETLOCAL -1 = local1, GETLOCAL -2 = local2

Few questions:
Is the above correct?
Is the validation code expected to reject GETLOCAL 3 and GETLOCAL -3?
Are EVM interpreters meant to throw an invalid stack access exception when they encounter these?

@gcolvin

This comment has been minimized.

Show comment
Hide comment
@gcolvin

gcolvin Dec 4, 2017

Collaborator

@seed The EVM doesn't expose stack addresses, but in 9.5 the Yellow Paper says, "Stack items are added or removed from the left-most, lower-indexed portion of the series." And throughout Appendix H we have notation like µ's[0] ≡ µs[0] + µs[1]. So in this proposal after, e.g.

PUSH 10
PUSH 11
JUMPSUB _x_
PUSH 12
PUSH 13

the stack looks like

10 <- FP
11
12
13
   <- SP

and GETLOCAL 0 is 10 and GETLOCAL 3 is 13. So GETLOCAL can address the subroutine arguments, and might better be named GETVAR. Negative arguments are not possible (args are unsigned ints) and GETLOCAL n where n > 3 would be rejected by the validator.

Collaborator

gcolvin commented Dec 4, 2017

@seed The EVM doesn't expose stack addresses, but in 9.5 the Yellow Paper says, "Stack items are added or removed from the left-most, lower-indexed portion of the series." And throughout Appendix H we have notation like µ's[0] ≡ µs[0] + µs[1]. So in this proposal after, e.g.

PUSH 10
PUSH 11
JUMPSUB _x_
PUSH 12
PUSH 13

the stack looks like

10 <- FP
11
12
13
   <- SP

and GETLOCAL 0 is 10 and GETLOCAL 3 is 13. So GETLOCAL can address the subroutine arguments, and might better be named GETVAR. Negative arguments are not possible (args are unsigned ints) and GETLOCAL n where n > 3 would be rejected by the validator.

@seed

This comment has been minimized.

Show comment
Hide comment
@seed

seed Dec 5, 2017

@gcolvin for some reason I had assumed FP = SP at entry of subroutine. Never mind, with the example it all makes sense now, thanks. I would actually suggest adding the example to the proposal.

seed commented Dec 5, 2017

@gcolvin for some reason I had assumed FP = SP at entry of subroutine. Never mind, with the example it all makes sense now, thanks. I would actually suggest adding the example to the proposal.

@seed

This comment has been minimized.

Show comment
Hide comment
@seed

seed Dec 5, 2017

The proposal uses the minus sign (-) instead of the em-dash (—) symbols in a few places which can lead to confusion.
Examples:

Local variable n is the n'th stack item below the frame pointer - FP[-n] as defined below.

I believe the first - should be a —. Also the syntax introduced, FP[-n], doesn't seem to be used elsewhere.

The first instruction of an array of EVM bytecode begins execution of a main routine with no arguments, SP and FP set to 0, and with one value on the return stack - code size - 1. (Executing the virtual byte of 0 after this offset causes an EVM to stop. Thus executing a RETURNSUB with no prior JUMPSUB or JUMBSUBV - that is, in the main routine - executes a STOP.)

Here again em-dashes should be used.

seed commented Dec 5, 2017

The proposal uses the minus sign (-) instead of the em-dash (—) symbols in a few places which can lead to confusion.
Examples:

Local variable n is the n'th stack item below the frame pointer - FP[-n] as defined below.

I believe the first - should be a —. Also the syntax introduced, FP[-n], doesn't seem to be used elsewhere.

The first instruction of an array of EVM bytecode begins execution of a main routine with no arguments, SP and FP set to 0, and with one value on the return stack - code size - 1. (Executing the virtual byte of 0 after this offset causes an EVM to stop. Thus executing a RETURNSUB with no prior JUMPSUB or JUMBSUBV - that is, in the main routine - executes a STOP.)

Here again em-dashes should be used.

@gcolvin

This comment has been minimized.

Show comment
Hide comment
@gcolvin

gcolvin Dec 5, 2017

Collaborator

You are right on the punctuation. I was too lazy to crawl through layers of menus to find the em-dash. I took the array syntax from the yellow paper (e.g. µs[0]). It would be nice if markdown wasn't too primitive (that is, more primitive than what we used 40 years ago) to support subscripts, but might we still do better to switch from SP and FP to µs and µf?

You are also right about the example diagram.

Collaborator

gcolvin commented Dec 5, 2017

You are right on the punctuation. I was too lazy to crawl through layers of menus to find the em-dash. I took the array syntax from the yellow paper (e.g. µs[0]). It would be nice if markdown wasn't too primitive (that is, more primitive than what we used 40 years ago) to support subscripts, but might we still do better to switch from SP and FP to µs and µf?

You are also right about the example diagram.

@seed

This comment has been minimized.

Show comment
Hide comment
@seed

seed Dec 5, 2017

We finished the Lem implementation of JUMPIF, JUMPTO, JUMPSUB, RETURNSUB, BEGINSUB, GETLOCAL, PUTLOCAL.
See https://github.com/seed/eth-isabelle/blob/evm15/lem/evm.lem

Few questions/comments resulting from this:

  • Should the address popped from the return stack by RETURNSUB point to a JUMPDEST? Or is JUMPSUB implicitly implying that the next instruction is the target of a RETURNSUB.
  • It seems more natural for JUMPSUB to push the return address of the next instruction, instead of jumping back to the JUMPSUB and advancing the PC in RETURNSUB.
  • The size of a JUMPSUB instruction is 3 bytes, so initialising the return stack to "code_size - 1" is misleading, though harmless. To reach the the first virtual STOP after the bytecode when executing a RETURNSUB we need to initialise the return stack with "code_size - 3".

To properly test both the Lem code and the cpp-Ethereum client at this point we need the Solidity compiler to output subroutine instructions.
Do you know the status of subroutine support in the Solidity compiler?

seed commented Dec 5, 2017

We finished the Lem implementation of JUMPIF, JUMPTO, JUMPSUB, RETURNSUB, BEGINSUB, GETLOCAL, PUTLOCAL.
See https://github.com/seed/eth-isabelle/blob/evm15/lem/evm.lem

Few questions/comments resulting from this:

  • Should the address popped from the return stack by RETURNSUB point to a JUMPDEST? Or is JUMPSUB implicitly implying that the next instruction is the target of a RETURNSUB.
  • It seems more natural for JUMPSUB to push the return address of the next instruction, instead of jumping back to the JUMPSUB and advancing the PC in RETURNSUB.
  • The size of a JUMPSUB instruction is 3 bytes, so initialising the return stack to "code_size - 1" is misleading, though harmless. To reach the the first virtual STOP after the bytecode when executing a RETURNSUB we need to initialise the return stack with "code_size - 3".

To properly test both the Lem code and the cpp-Ethereum client at this point we need the Solidity compiler to output subroutine instructions.
Do you know the status of subroutine support in the Solidity compiler?

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Dec 5, 2017

Member

It can compile "Solidity inline assembly" programs to EVM 1.5:

{
  function f(a) -> b
  {
    b := add(a, 5)
  }

  let x := f(2)
}

using solc --assemble --machine=evm15 test.asm

results in the following bytecode:

b000000011b560006005820190509050b75b6002b30000000550
Member

axic commented Dec 5, 2017

It can compile "Solidity inline assembly" programs to EVM 1.5:

{
  function f(a) -> b
  {
    b := add(a, 5)
  }

  let x := f(2)
}

using solc --assemble --machine=evm15 test.asm

results in the following bytecode:

b000000011b560006005820190509050b75b6002b30000000550
@seed

This comment has been minimized.

Show comment
Hide comment
@seed

seed Dec 5, 2017

@axic thanks, I'll look into it.
Has anyone written tests to stimulate that part of the compiler, which we could potentially use to compare the behaviour of new instructions?

seed commented Dec 5, 2017

@axic thanks, I'll look into it.
Has anyone written tests to stimulate that part of the compiler, which we could potentially use to compare the behaviour of new instructions?

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Dec 6, 2017

Member

@seed it is not tested since the testing client (cpp-ethereum) build we have didn't support it. It could be added if some submits a PR.

Member

axic commented Dec 6, 2017

@seed it is not tested since the testing client (cpp-ethereum) build we have didn't support it. It could be added if some submits a PR.

@gcolvin

This comment has been minimized.

Show comment
Hide comment
@gcolvin

gcolvin Dec 6, 2017

Collaborator

@seed Are you talking about initializing the return stack in the cpp-ethereum code or in the validation pseudocode?

No JUMPDEST is involved. Just a JUMPSUB to a BEGINSUB, and a RETURNSUB back to the JUMPSUB. The x86 CALL instruction pushes the PC on the stack and RET pops it and jumps to it. Then the PC gets incremented in the usual way. That was the model I had in mind, it's how the C++ code is written for JUMP, and I think it comports with (136) in the Yellow Paper. (The C++ code is not written to match this model for RETURNSUB, although the behavior is the same.)

Collaborator

gcolvin commented Dec 6, 2017

@seed Are you talking about initializing the return stack in the cpp-ethereum code or in the validation pseudocode?

No JUMPDEST is involved. Just a JUMPSUB to a BEGINSUB, and a RETURNSUB back to the JUMPSUB. The x86 CALL instruction pushes the PC on the stack and RET pops it and jumps to it. Then the PC gets incremented in the usual way. That was the model I had in mind, it's how the C++ code is written for JUMP, and I think it comports with (136) in the Yellow Paper. (The C++ code is not written to match this model for RETURNSUB, although the behavior is the same.)

@gcolvin

This comment has been minimized.

Show comment
Hide comment
@gcolvin

gcolvin Dec 8, 2017

Collaborator

So far as a formal spec (or implementation) goes I think you can specify it however you like, so long as the PC winds up in the right place. It could be changed here too if it helps, but I find it more clear the way it is.

Collaborator

gcolvin commented Dec 8, 2017

So far as a formal spec (or implementation) goes I think you can specify it however you like, so long as the PC winds up in the right place. It could be changed here too if it helps, but I find it more clear the way it is.

@nootropicat

This comment has been minimized.

Show comment
Hide comment
@nootropicat

nootropicat Jan 26, 2018

For formal analysis purposes, all of this is implementable right now as an intermediate language that's easily compilable to evm. PUTLOCAL and GETLOCAL are indeed very useful but there's no need for separate opcodes - stack could be mapped to negative memory and accessed with MLOAD/MSTORE (ie. the stack starts at (-32) and every push goes downwards). Space of one-byte opcodes is limited.

Why not add it as a precompiled contract? Ie. the very first instruction (in EVM) calls it with code as an argument. The gas cost of that particular call could be set to zero, in effect working only as a costless (except storage) marking for a different vm version. This would totally avoid problems due to deprecating opcodes and backwards compatibility, allowing for a much more fundamental changes.

In principle I very much dislike the idea of breaking backwards compatibility. What if someone has a compiled contract on some private blockchain? It would be impossible to deploy on the public one without recompilation. What if there's some private or just unknown language that compiles to evm? Its compiler would have to be rewritten. Even if one doesn't exist at the moment (most likely), potential ones that may exist may not be written at all, because the risk of compatibility-breaking changes would be judged as too high. For all these reasons modern processors still support old 16 bit code - even including undocumented accidental instructions (ie. ffreep)!

nootropicat commented Jan 26, 2018

For formal analysis purposes, all of this is implementable right now as an intermediate language that's easily compilable to evm. PUTLOCAL and GETLOCAL are indeed very useful but there's no need for separate opcodes - stack could be mapped to negative memory and accessed with MLOAD/MSTORE (ie. the stack starts at (-32) and every push goes downwards). Space of one-byte opcodes is limited.

Why not add it as a precompiled contract? Ie. the very first instruction (in EVM) calls it with code as an argument. The gas cost of that particular call could be set to zero, in effect working only as a costless (except storage) marking for a different vm version. This would totally avoid problems due to deprecating opcodes and backwards compatibility, allowing for a much more fundamental changes.

In principle I very much dislike the idea of breaking backwards compatibility. What if someone has a compiled contract on some private blockchain? It would be impossible to deploy on the public one without recompilation. What if there's some private or just unknown language that compiles to evm? Its compiler would have to be rewritten. Even if one doesn't exist at the moment (most likely), potential ones that may exist may not be written at all, because the risk of compatibility-breaking changes would be judged as too high. For all these reasons modern processors still support old 16 bit code - even including undocumented accidental instructions (ie. ffreep)!

@gcolvin

This comment has been minimized.

Show comment
Hide comment
@gcolvin

gcolvin Jan 26, 2018

Collaborator

The difference with PUTLOCAL and GETLOCAL is that they have to respect frame boundaries. This proposal was meant to break compatibility less than eWasm, which breaks it completely.

Collaborator

gcolvin commented Jan 26, 2018

The difference with PUTLOCAL and GETLOCAL is that they have to respect frame boundaries. This proposal was meant to break compatibility less than eWasm, which breaks it completely.

@nootropicat

This comment has been minimized.

Show comment
Hide comment
@nootropicat

nootropicat Jan 26, 2018

Respect how? You replied previously that they don't throw "It pushes FP[-n] on the stack.". So they act as memory access just with fp as the offset.

nootropicat commented Jan 26, 2018

Respect how? You replied previously that they don't throw "It pushes FP[-n] on the stack.". So they act as memory access just with fp as the offset.

@gcolvin

This comment has been minimized.

Show comment
Hide comment
@gcolvin

gcolvin Jan 26, 2018

Collaborator

Validity condition 3. Programs that try to get or put a stack slot outside of the local frame are invalid. Memory access isn't constrained that way.

Collaborator

gcolvin commented Jan 26, 2018

Validity condition 3. Programs that try to get or put a stack slot outside of the local frame are invalid. Memory access isn't constrained that way.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment