Skip to content
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.

Sign up for GitHub

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

Typed exceptions #187

Merged
merged 10 commits into from
Apr 19, 2018
Merged

Typed exceptions #187

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
81a66cc
network, Makefile: add file for formalizing the EVM-C api, start with…
Mar 23, 2018
44ea4f7
evm: distinguish between INVALID and UNDEFINED(_) opcodes
Mar 28, 2018
99393b6
evm, driver, tests/.../output: add <statusCode> cell using status cod…
Apr 11, 2018
be1c950
driver: add `status_` command for asserting the contents of the `stat…
Apr 11, 2018
e394724
evm: switch from untyped exceptions `#exception` to typed `#exception…
Apr 11, 2018
11a8958
evm, driver, evm-node: check for exceptional status when catching `#e…
Apr 11, 2018
ccdf0ee
evm, driver, analysis, evm-node, tests/*.out: `#end` generates an exc…
Apr 11, 2018
fad4f8b
evm, driver, evm-node: `#revert` generates an exception, sets `status…
Apr 11, 2018
504d878
evm, driver, analysis, evm-node: remove #exception, #revert, rename #…
Apr 14, 2018
abc14fa
tests/proofs: update proofs submodule
Apr 12, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,7 @@ build-node: .build/vm/kevm-vm
standalone_tangle:=.k:not(.node),.standalone
node_tangle:=.k:not(.standalone),.node

k_files:=driver.k data.k evm.k analysis.k krypto.k edsl.k evm-node.k
k_files:=driver.k data.k network.k evm.k analysis.k krypto.k edsl.k evm-node.k
ocaml_files:=$(patsubst %,.build/ocaml/%,$(k_files))
java_files:=$(patsubst %,.build/java/%,$(k_files))
node_files:=$(patsubst %,.build/node/%,$(k_files))
Expand Down
2 changes: 1 addition & 1 deletion analysis.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ We'll need to make summaries of the state which collect information about how mu

syntax KItem ::= "#endSummary"
// ------------------------------
rule <k> (#end => .) ~> #endSummary ... </k>
rule <statusCode> EVMC_SUCCESS </statusCode> <k> (#halt => .) ~> #endSummary ... </k>
rule <k> #endSummary => . ... </k> <pc> PCOUNT </pc> <gas> GAVAIL </gas> <memoryUsed> MEMUSED </memoryUsed>
<analysis> ... "blocks" |-> (ListItem({ PCOUNT1 | GAVAIL1 | MEMUSED1 } => { PCOUNT1 ==> PCOUNT | GAVAIL1 -Int GAVAIL | MEMUSED -Int MEMUSED1 }) REST) ... </analysis>
```
Expand Down
43 changes: 26 additions & 17 deletions driver.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ Some Ethereum commands take an Ethereum specification (eg. for an account or tra
rule <k> .EthereumSimulation => . ... </k>
rule <k> ETC ETS:EthereumSimulation => ETC ~> ETS ... </k>
rule <k> ETC1:EthereumCommand ~> ETC2 ETS:EthereumSimulation => ETC1 ~> ETC2 ~> ETS ... </k>
rule <k> EX:Exception ~> ETC2 ETS:EthereumSimulation => EX ~> ETC2 ~> ETS ... </k>
rule <k> KI:KItem ~> ETC2 ETS:EthereumSimulation => KI ~> ETC2 ~> ETS ... </k>

syntax EthereumSimulation ::= JSON
// ----------------------------------
Expand Down Expand Up @@ -72,7 +72,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
### Driving Execution

- `start` places `#next` on the `<k>` cell so that execution of the loaded state begin.
- `flush` places `#finalize` on the `<k>` cell once it sees `#end` in the `<k>` cell, clearing any exceptions it finds.
- `flush` places `#finalize` on the `<k>` cell.

```{.k .standalone}
syntax EthereumCommand ::= "start"
Expand All @@ -83,8 +83,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a

syntax EthereumCommand ::= "flush"
// ----------------------------------
rule <mode> EXECMODE </mode> <k> #end ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ... </k>
rule <mode> EXECMODE </mode> <k> #exception ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ~> #exception ... </k>
rule <mode> EXECMODE </mode> <statusCode> EVMC_SUCCESS </statusCode> <k> #halt ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ... </k>
rule <mode> EXECMODE </mode> <statusCode> _:ExceptionalStatusCode </statusCode> <k> #halt ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ~> #halt ... </k>
```

- `startTx` computes the sender of the transaction, and places loadTx on the `k` cell.
Expand Down Expand Up @@ -178,10 +178,11 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a

syntax EthereumCommand ::= "#finishTx"
// --------------------------------------
rule <k> #exception ~> #finishTx => #popCallStack ~> #popWorldState ... </k>
rule <k> #revert ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... </k> <gas> GAVAIL </gas>
rule <statusCode> _:ExceptionalStatusCode </statusCode> <k> #halt ~> #finishTx => #popCallStack ~> #popWorldState ... </k>
rule <statusCode> EVMC_REVERT </statusCode> <k> #halt ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... </k> <gas> GAVAIL </gas>

rule <k> #end ~> #finishTx => #mkCodeDeposit ACCT ... </k>
rule <statusCode> EVMC_SUCCESS </statusCode>
<k> #halt ~> #finishTx => #mkCodeDeposit ACCT ... </k>
<id> ACCT </id>
<txPending> ListItem(TXID:Int) ... </txPending>
<message>
Expand All @@ -190,7 +191,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
...
</message>

rule <k> #end ~> #finishTx => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ... </k>
rule <statusCode> EVMC_SUCCESS </statusCode>
<k> #halt ~> #finishTx => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ... </k>
<id> ACCT </id>
<gas> GAVAIL </gas>
<txPending> ListItem(TXID:Int) ... </txPending>
Expand Down Expand Up @@ -248,11 +250,17 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
syntax Mode ::= "SUCCESS"
// -------------------------

syntax EthereumCommand ::= "exception" | "failure" String | "success"
// ---------------------------------------------------------------------
rule <k> #exception ~> exception => . ... </k>
syntax EthereumCommand ::= "exception" | "status" StatusCode
// ------------------------------------------------------------
rule <statusCode> _:ExceptionalStatusCode </statusCode>
<k> #halt ~> exception => . ... </k>

rule <k> status SC => . ... </k> <statusCode> SC </statusCode>

syntax EthereumCommand ::= "failure" String | "success"
// -------------------------------------------------------
rule <k> success => . ... </k> <exit-code> _ => 0 </exit-code> <mode> _ => SUCCESS </mode>
rule failure _ => .
rule <k> failure _ => . ... </k>
```

### Running Tests
Expand Down Expand Up @@ -396,10 +404,11 @@ State Manipulation
syntax EthreumCommand ::= "clearNETWORK"
// ----------------------------------------
rule <k> clearNETWORK => . ... </k>
<activeAccounts> _ => .Set </activeAccounts>
<accounts> _ => .Bag </accounts>
<messages> _ => .Bag </messages>
<schedule> _ => DEFAULT </schedule>
<statusCode> _ => .StatusCode </statusCode>
<activeAccounts> _ => .Set </activeAccounts>
<accounts> _ => .Bag </accounts>
<messages> _ => .Bag </messages>
<schedule> _ => DEFAULT </schedule>
```

### Loading State
Expand Down Expand Up @@ -631,7 +640,7 @@ The `"rlp"` key loads the block information.
```{.k .standalone}
syntax EthereumCommand ::= "check" JSON
// ---------------------------------------
rule <k> #exception ~> check J:JSON => check J ~> #exception ... </k>
rule <k> #halt ~> check J:JSON => check J ~> #halt ... </k>

rule <k> check DATA : { .JSONList } => . ... </k> requires DATA =/=String "transactions"
rule <k> check DATA : [ .JSONList ] => . ... </k> requires DATA =/=String "ommerHeaders"
Expand Down
16 changes: 10 additions & 6 deletions evm-node.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -184,14 +184,18 @@ Because the same account may be loaded more than once, implementations of this i
- `#endCreate` and `#endVM` clean up after the transaction finishes and store the return status code of the top level call frame on the top of the `<k>` cell.

```{.k .node}
syntax Exception ::= "#endVM" | "#endCreate"
// --------------------------------------------
rule <k> #exception ~> #endVM => #popCallStack ~> #popWorldState ~> 0 </k>
syntax KItem ::= "#endVM" | "#endCreate"
// ----------------------------------------
rule <statusCode> _:ExceptionalStatusCode </statusCode>
<k> #halt ~> #endVM => #popCallStack ~> #popWorldState ~> 0 </k>
<output> _ => .WordStack </output>
rule <k> #revert ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 </k>
<gas> GAVAIL </gas>

rule <k> #end ~> #endVM => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> 1 </k>
rule <statusCode> EVMC_REVERT </statusCode>
<k> #halt ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 </k>
<gas> GAVAIL </gas>

rule <statusCode> EVMC_SUCCESS </statusCode>
<k> #halt ~> #endVM => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> 1 </k>
<gas> GAVAIL </gas>

rule <k> #endCreate => W ... </k> <wordStack> W : WS </wordStack>
Expand Down
Loading