Skip to content

Remove vmtest dependencies #183

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

Merged
pirapira merged 15 commits into from
Apr 11, 2018
Merged

Remove vmtest dependencies #183

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
355158a
evm, tests/: move parts of state saved by #pushCallStack into cell ca…
Apr 2, 2018
74b7417
evm: use configuration fragments for storing <callState> in the <call…
Apr 2, 2018
e222f80
evm: factor out `#incrementNonce` operator
Apr 2, 2018
56dec1d
Makefile, evm: remove dependence of OPCODE execution on VMTESTS, disa…
Apr 3, 2018
fe926b9
kevm: make sure to remove temporary files
Apr 3, 2018
cf840f6
driver: remove check of account balance after execution for VMTESTS mode
Apr 3, 2018
8098f47
driver, evm: remove dependence of finalizeTx on VMTESTS
Apr 3, 2018
8cd9701
evm, driver, evm-node, tests/: combine #{push,pop,drop}{Substate,Worl…
Apr 3, 2018
210669b
tests/proofs: update submodule with changes to configuration
Apr 2, 2018
ed12abd
tests/interactive/add0: remove interactive test from VMTests set
Apr 3, 2018
08de1af
Makefile, tests/{templates,interactive}: switch to generic way of che…
Apr 3, 2018
65d0e81
kevm, Makefile: use exit-code based testing except for interactive tests
Apr 3, 2018
896505a
Makefile: more specific build dependencies for test-suites
Apr 3, 2018
a4ddf52
Makefile: three more slow bchain tests
Apr 10, 2018
fcc1198
Makefile: more specific exclusion of VM tests
pirapira Apr 5, 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
34 changes: 24 additions & 10 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -215,31 +215,45 @@ test-conformance: test-vm test-bchain

vm_tests=$(wildcard tests/ethereum-tests/VMTests/*/*.json)
slow_vm_tests=$(wildcard tests/ethereum-tests/VMTests/vmPerformance/*.json)
quick_vm_tests=$(filter-out $(slow_vm_tests), $(vm_tests))
bad_vm_tests= $(wildcard tests/ethereum-tests/VMTests/vmBlockInfoTest/blockhash*.json) \
$(wildcard tests/ethereum-tests/VMTests/vmEnvironmentalInfo/balance*.json) \
$(wildcard tests/ethereum-tests/VMTests/vmSystemOperations/*call*.json) \
$(wildcard tests/ethereum-tests/VMTests/vmSystemOperations/*Call*.json) \
$(wildcard tests/ethereum-tests/VMTests/vmSystemOperations/*create*.json) \
tests/ethereum-tests/VMTests/vmEnvironmentalInfo/env1.json \
tests/ethereum-tests/VMTests/vmEnvironmentalInfo/extcodecopy0AddressTooBigRight.json \
tests/ethereum-tests/VMTests/vmEnvironmentalInfo/ExtCodeSizeAddressInputTooBigRightMyAddress.json \
tests/ethereum-tests/VMTests/vmRandomTest/201503110226PYTHON_DUP6.json \
tests/ethereum-tests/VMTests/vmRandomTest/randomTest.json \
tests/ethereum-tests/VMTests/vmSystemOperations/PostToNameRegistrator0.json \
tests/ethereum-tests/VMTests/vmSystemOperations/PostToReturn1.json
quick_vm_tests=$(filter-out $(slow_vm_tests) $(bad_vm_tests), $(vm_tests))

test-all-vm: $(vm_tests:=.test)
test-slow-vm: $(slow_vm_tests:=.test)
test-vm: $(quick_vm_tests:=.test)

tests/ethereum-tests/VMTests/%.test: tests/ethereum-tests/VMTests/% build
MODE=VMTESTS $(TEST) $< tests/templates/output-success.txt
tests/ethereum-tests/VMTests/%.test: tests/ethereum-tests/VMTests/% build-ocaml
MODE=VMTESTS $(TEST) $<

# BlockchainTests

bchain_tests=$(wildcard tests/ethereum-tests/BlockchainTests/GeneralStateTests/*/*.json)
slow_bchain_tests=$(wildcard tests/ethereum-tests/BlockchainTests/GeneralStateTests/stQuadraticComplexityTest/*.json) \
$(wildcard tests/ethereum-tests/BlockchainTests/GeneralStateTests/stStaticCall/static_Call50000*.json) \
$(wildcard tests/ethereum-tests/BlockchainTests/GeneralStateTests/stStaticCall/static_Return50000*.json) \
$(wildcard tests/ethereum-tests/BlockchainTests/GeneralStateTests/stStaticCall/static_Call1MB1024Calldepth_d1g0v0.json)
# $(wildcard tests/BlockchainTests/GeneralStateTests/*/*/*_Constantinople.json)
$(wildcard tests/ethereum-tests/BlockchainTests/GeneralStateTests/stStaticCall/static_Call1MB1024Calldepth_d1g0v0.json) \
tests/ethereum-tests/BlockchainTests/GeneralStateTests/stRandom/randomStatetest177_d0g0v0.json \
tests/ethereum-tests/BlockchainTests/GeneralStateTests/stSpecialTest/JUMPDEST_Attack_d0g0v0.json \
tests/ethereum-tests/BlockchainTests/GeneralStateTests/stSpecialTest/JUMPDEST_AttackwithJump_d0g0v0.json
quick_bchain_tests=$(filter-out $(slow_bchain_tests), $(bchain_tests))

test-all-bchain: $(bchain_tests:=.test)
test-slow-bchain: $(bchain_tests:=.test)
test-bchain: $(quick_bchain_tests:=.test)

tests/ethereum-tests/BlockchainTests/%.test: tests/ethereum-tests/BlockchainTests/% build
$(TEST) $< tests/templates/output-success.txt
tests/ethereum-tests/BlockchainTests/%.test: tests/ethereum-tests/BlockchainTests/% build-ocaml
$(TEST) $<

# InteractiveTests

Expand All @@ -248,8 +262,8 @@ interactive_tests:=$(wildcard tests/interactive/*.json) \

test-interactive: $(interactive_tests:=.test)

tests/interactive/%.json.test: tests/interactive/%.json tests/interactive/%.json.out build
$(TEST) $< $<.out
tests/interactive/%.json.test: tests/interactive/%.json build-ocaml build-java
$(TEST) $< tests/templates/output-success.json

tests/interactive/gas-analysis/%.evm.test: tests/interactive/gas-analysis/%.evm tests/interactive/gas-analysis/%.evm.out build
MODE=GASANALYZE $(TEST) $< $<.out
Expand All @@ -262,7 +276,7 @@ proof_tests=$(wildcard $(proof_dir)/*/*-spec.k)
test-proof: $(proof_tests:=.test)

$(proof_dir)/%.test: $(proof_dir)/% build-java
$(TEST) $< tests/templates/proof-success.txt
$(TEST) $<

split-proof-tests: tests/proofs/make.timestamp
$(MAKE) -C tests/proofs $@
Expand Down
17 changes: 11 additions & 6 deletions driver.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,8 +83,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a

syntax EthereumCommand ::= "flush"
// ----------------------------------
rule <k> #end ~> flush => #finalizeTx(false) ... </k>
rule <k> #exception ~> flush => #finalizeTx(false) ~> #exception ... </k>
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>
```

- `startTx` computes the sender of the transaction, and places loadTx on the `k` cell.
Expand Down Expand Up @@ -178,8 +178,8 @@ 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 ~> #popSubstate ... </k>
rule <k> #revert ~> #finishTx => #popCallStack ~> #popWorldState ~> #popSubstate ~> #refund GAVAIL ... </k> <gas> GAVAIL </gas>
rule <k> #exception ~> #finishTx => #popCallStack ~> #popWorldState ... </k>
rule <k> #revert ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... </k> <gas> GAVAIL </gas>

rule <k> #end ~> #finishTx => #mkCodeDeposit ACCT ... </k>
<id> ACCT </id>
Expand All @@ -190,7 +190,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
...
</message>

rule <k> #end ~> #finishTx => #popCallStack ~> #dropWorldState ~> #dropSubstate ~> #refund GAVAIL ... </k>
rule <k> #end ~> #finishTx => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ... </k>
<id> ACCT </id>
<gas> GAVAIL </gas>
<txPending> ListItem(TXID:Int) ... </txPending>
Expand Down Expand Up @@ -656,12 +656,17 @@ The `"rlp"` key loads the block information.
rule <k> check "account" : { (ACCT:Int) : { "code" : ((CODE:String) => #parseByteStack(CODE)) } } ... </k>
rule <k> check "account" : { (ACCT:Int) : { "storage" : ({ STORAGE:JSONList } => #parseMap({ STORAGE })) } } ... </k>

rule <k> check "account" : { ACCT : { "balance" : (BAL:Int) } } => . ... </k>
rule <mode> EXECMODE </mode>
<k> check "account" : { ACCT : { "balance" : (BAL:Int) } } => . ... </k>
<account>
<acctID> ACCT </acctID>
<balance> BAL </balance>
...
</account>
requires EXECMODE =/=K VMTESTS

rule <mode> VMTESTS </mode>
<k> check "account" : { ACCT : { "balance" : (BAL:Int) } } => . ... </k>

rule <k> check "account" : { ACCT : { "nonce" : (NONCE:Int) } } => . ... </k>
<account>
Expand Down
6 changes: 3 additions & 3 deletions evm-node.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -186,12 +186,12 @@ Because the same account may be loaded more than once, implementations of this i
```{.k .node}
syntax Exception ::= "#endVM" | "#endCreate"
// --------------------------------------------
rule <k> #exception ~> #endVM => #popCallStack ~> #popWorldState ~> #popSubstate ~> 0 </k>
rule <k> #exception ~> #endVM => #popCallStack ~> #popWorldState ~> 0 </k>
<output> _ => .WordStack </output>
rule <k> #revert ~> #endVM => #popCallStack ~> #popWorldState ~> #popSubstate ~> #refund GAVAIL ~> 0 </k>
rule <k> #revert ~> #endVM => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 </k>
<gas> GAVAIL </gas>

rule <k> #end ~> #endVM => #popCallStack ~> #dropWorldState ~> #dropSubstate ~> #refund GAVAIL ~> 1 </k>
rule <k> #end ~> #endVM => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ~> 1 </k>
<gas> GAVAIL </gas>

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