Skip to content

Testing cleanups #191

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
merged 12 commits into from
Apr 17, 2018
Merged

Testing cleanups #191

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
80ce2d7
kevm: also log test output when in `test-profile` mode
Apr 12, 2018
09bbad7
kevm: add get-failing command for listing failing tests
Apr 13, 2018
edc6477
Makefile: exclude bad_vm_tests from target test-all-vm
Apr 16, 2018
cc6f6a5
Makefile: default to ./kevm test-profile for testing instead of ./kev…
Apr 13, 2018
a2b772e
Makefile: more specific K file dependencies for OCaml backend
Apr 11, 2018
6a22d57
Makefile: more specific build deps for gas analysis tests
Apr 16, 2018
1576804
Makefile: exclude more VMTests which use BLOCKHASH
Apr 11, 2018
072f4ae
Makefile: split-proof-tests as dependency of each proof test
Apr 14, 2018
324d912
tests/templates/output-success.kast: remove unused output file
Apr 12, 2018
b292ef4
evm: reformat configuration declaration
Apr 11, 2018
d937330
evm: make #setMode an InternalOp so its handled by exceptions
Apr 16, 2018
bba1cbb
evm, driver, tests/{*.out,proofs}: remove <callLog> cell for VMTests …
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
17 changes: 11 additions & 6 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ else
LIBFLAG=-shared
endif

.build/%/driver-kompiled/constants.$(EXT): $(defn_files)
.build/%/driver-kompiled/constants.$(EXT): $(ocaml_files) $(node_files)
@echo "== kompile: $@"
eval $$(opam config env) \
&& ${K_BIN}/kompile --debug --main-module ETHEREUM-SIMULATION \
Expand Down Expand Up @@ -186,7 +186,7 @@ endif
# -----

# Override this with `make TEST=echo` to list tests instead of running
TEST=./kevm test
TEST=./kevm test-profile

test-all: test-all-concrete test-all-proof
test: test-concrete test-proof
Expand Down Expand Up @@ -223,13 +223,18 @@ bad_vm_tests= $(wildcard tests/ethereum-tests/VMTests/vmBlockInfoTest/blockhash*
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/201503102037PYTHON.json \
tests/ethereum-tests/VMTests/vmRandomTest/201503102148PYTHON.json \
tests/ethereum-tests/VMTests/vmRandomTest/201503102300PYTHON.json \
tests/ethereum-tests/VMTests/vmRandomTest/201503110050PYTHON.json \
Copy link
Contributor

@dwightguth dwightguth Apr 16, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

test-all-vm needs to not test the bad_vm_tests.

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))
all_vm_tests=$(filter-out $(bad_vm_tests), $(vm_tests))
quick_vm_tests=$(filter-out $(slow_vm_tests), $(all_vm_tests))

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

Expand Down Expand Up @@ -265,7 +270,7 @@ test-interactive: $(interactive_tests:=.test)
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
tests/interactive/gas-analysis/%.evm.test: tests/interactive/gas-analysis/%.evm tests/interactive/gas-analysis/%.evm.out build-ocaml build-java
MODE=GASANALYZE $(TEST) $< $<.out

# ProofTests
Expand All @@ -275,7 +280,7 @@ proof_tests=$(wildcard $(proof_dir)/*/*-spec.k)

test-proof: $(proof_tests:=.test)

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

split-proof-tests: tests/proofs/make.timestamp
Expand Down
13 changes: 2 additions & 11 deletions driver.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -315,7 +315,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
// -------------------------------------------------------------------------------------------
rule #postKeys => ( SetItem("post") SetItem("postState") )
rule #allPostKeys => ( #postKeys SetItem("expect") SetItem("export") SetItem("expet") )
rule #checkKeys => ( #allPostKeys SetItem("logs") SetItem("callcreates") SetItem("out") SetItem("gas")
rule #checkKeys => ( #allPostKeys SetItem("logs") SetItem("out") SetItem("gas")
SetItem("blockHeader") SetItem("transactions") SetItem("uncleHeaders") SetItem("genesisBlockHeader")
)

Expand All @@ -328,7 +328,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
```{.k .standalone}
syntax Set ::= "#discardKeys" [function]
// ----------------------------------------
rule #discardKeys => ( SetItem("//") SetItem("_info") )
rule #discardKeys => ( SetItem("//") SetItem("_info") SetItem("callcreates") )

rule <k> run TESTID : { KEY : _ , REST } => run TESTID : { REST } ... </k> requires KEY in #discardKeys
```
Expand All @@ -354,7 +354,6 @@ State Manipulation
<memoryUsed> _ => 0 </memoryUsed>
<callDepth> _ => 0 </callDepth>
<callStack> _ => .List </callStack>
<callLog> _ => .Set </callLog>
<program> _ => .Map </program>
<programBytes> _ => .WordStack </programBytes>
<id> _ => 0 </id>
Expand Down Expand Up @@ -718,14 +717,6 @@ Here we check the other post-conditions associated with an EVM test.
rule <k> check "gas" : ((GLEFT:String) => #parseWord(GLEFT)) ... </k>
rule <k> check "gas" : GLEFT => . ... </k> <gas> GLEFT </gas>

rule <k> check TESTID : { "callcreates" : CCREATES } => check "callcreates" : CCREATES ~> failure TESTID ... </k>
// -----------------------------------------------------------------------------------------------------------------
rule <k> check "callcreates" : { ("data" : (DATA:String)) , ("destination" : (ACCTTO:String)) , ("gasLimit" : (GLIMIT:String)) , ("value" : (VAL:String)) , .JSONList }
=> check "callcreates" : { #parseAddr(ACCTTO) | #parseWord(GLIMIT) | #parseWord(VAL) | #parseByteStack(DATA) }
...
</k>
rule <k> check "callcreates" : C:Call => . ... </k> <callLog> CL </callLog> requires C in CL

rule check TESTID : { "blockHeader" : BLOCKHEADER } => check "blockHeader" : BLOCKHEADER ~> failure TESTID
// ----------------------------------------------------------------------------------------------------------
rule <k> check "blockHeader" : { KEY : VALUE , REST } => check "blockHeader" : { KEY : VALUE } ~> check "blockHeader" : { REST } ... </k>
Expand Down
249 changes: 124 additions & 125 deletions evm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,128 +25,128 @@ We've broken up the configuration into two components; those parts of the state
In the comments next to each cell, we've marked which component of the YellowPaper state corresponds to each cell.

```k
configuration <k> $PGM:EthereumSimulation </k>
<exit-code exit=""> 1 </exit-code>
<mode> $MODE:Mode </mode>
<schedule> $SCHEDULE:Schedule </schedule>
<analysis> .Map </analysis>

<ethereum>

// EVM Specific
// ============

<evm>

// Mutable during a single transaction
// -----------------------------------

<output> .WordStack </output> // H_RETURN
<callStack> .List </callStack>
<interimStates> .List </interimStates>
<callLog> .Set </callLog>
<touchedAccounts> .Set </touchedAccounts>

<callState>
<program> .Map </program> // I_b
<programBytes> .WordStack </programBytes>

// I_*
<id> 0 </id> // I_a
<caller> 0 </caller> // I_s
<callData> .WordStack </callData> // I_d
<callValue> 0 </callValue> // I_v

// \mu_*
<wordStack> .WordStack </wordStack> // \mu_s
<localMem> .Map </localMem> // \mu_m
<pc> 0 </pc> // \mu_pc
<gas> 0 </gas> // \mu_g
<memoryUsed> 0 </memoryUsed> // \mu_i
<previousGas> 0 </previousGas>

<static> false </static>
<callDepth> 0 </callDepth>
</callState>

// A_* (execution substate)
<substate>
<selfDestruct> .Set </selfDestruct> // A_s
<log> .List </log> // A_l
<refund> 0 </refund> // A_r
</substate>

// Immutable during a single transaction
// -------------------------------------

<gasPrice> 0 </gasPrice> // I_p
<origin> 0 </origin> // I_o

// I_H* (block information)
<previousHash> 0 </previousHash> // I_Hp
<ommersHash> 0 </ommersHash> // I_Ho
<coinbase> 0 </coinbase> // I_Hc
<stateRoot> 0 </stateRoot> // I_Hr
<transactionsRoot> 0 </transactionsRoot> // I_Ht
<receiptsRoot> 0 </receiptsRoot> // I_He
<logsBloom> .WordStack </logsBloom> // I_Hb
<difficulty> 0 </difficulty> // I_Hd
<number> 0 </number> // I_Hi
<gasLimit> 0 </gasLimit> // I_Hl
<gasUsed> 0 </gasUsed> // I_Hg
<timestamp> 0 </timestamp> // I_Hs
<extraData> .WordStack </extraData> // I_Hx
<mixHash> 0 </mixHash> // I_Hm
<blockNonce> 0 </blockNonce> // I_Hn

<ommerBlockHeaders> [ .JSONList ] </ommerBlockHeaders>
<blockhash> .List </blockhash>

</evm>

// Ethereum Network
// ================

<network>

// Accounts Record
// ---------------

<activeAccounts> .Set </activeAccounts>
<accounts>
<account multiplicity="*" type="Map">
<acctID> 0 </acctID>
<balance> 0 </balance>
<code> .WordStack:AccountCode </code>
<storage> .Map </storage>
<nonce> 0 </nonce>
</account>
</accounts>

// Transactions Record
// -------------------

<txOrder> .List </txOrder>
<txPending> .List </txPending>

<messages>
<message multiplicity="*" type="Map">
<msgID> 0 </msgID>
<txNonce> 0 </txNonce> // T_n
<txGasPrice> 0 </txGasPrice> // T_p
<txGasLimit> 0 </txGasLimit> // T_g
<to> .Account </to> // T_t
<value> 0 </value> // T_v
<sigV> 0 </sigV> // T_w
<sigR> .WordStack </sigR> // T_r
<sigS> .WordStack </sigS> // T_s
<data> .WordStack </data> // T_i/T_e
</message>
</messages>

</network>

</ethereum>
configuration
<k> $PGM:EthereumSimulation </k>
<exit-code exit=""> 1 </exit-code>
<mode> $MODE:Mode </mode>
<schedule> $SCHEDULE:Schedule </schedule>
<analysis> .Map </analysis>

<ethereum>

// EVM Specific
// ============

<evm>

// Mutable during a single transaction
// -----------------------------------

<output> .WordStack </output> // H_RETURN
<callStack> .List </callStack>
<interimStates> .List </interimStates>
<touchedAccounts> .Set </touchedAccounts>

<callState>
<program> .Map </program> // I_b
<programBytes> .WordStack </programBytes>

// I_*
<id> 0 </id> // I_a
<caller> 0 </caller> // I_s
<callData> .WordStack </callData> // I_d
<callValue> 0 </callValue> // I_v

// \mu_*
<wordStack> .WordStack </wordStack> // \mu_s
<localMem> .Map </localMem> // \mu_m
<pc> 0 </pc> // \mu_pc
<gas> 0 </gas> // \mu_g
<memoryUsed> 0 </memoryUsed> // \mu_i
<previousGas> 0 </previousGas>

<static> false </static>
<callDepth> 0 </callDepth>
</callState>

// A_* (execution substate)
<substate>
<selfDestruct> .Set </selfDestruct> // A_s
<log> .List </log> // A_l
<refund> 0 </refund> // A_r
</substate>

// Immutable during a single transaction
// -------------------------------------

<gasPrice> 0 </gasPrice> // I_p
<origin> 0 </origin> // I_o

// I_H* (block information)
<previousHash> 0 </previousHash> // I_Hp
<ommersHash> 0 </ommersHash> // I_Ho
<coinbase> 0 </coinbase> // I_Hc
<stateRoot> 0 </stateRoot> // I_Hr
<transactionsRoot> 0 </transactionsRoot> // I_Ht
<receiptsRoot> 0 </receiptsRoot> // I_He
<logsBloom> .WordStack </logsBloom> // I_Hb
<difficulty> 0 </difficulty> // I_Hd
<number> 0 </number> // I_Hi
<gasLimit> 0 </gasLimit> // I_Hl
<gasUsed> 0 </gasUsed> // I_Hg
<timestamp> 0 </timestamp> // I_Hs
<extraData> .WordStack </extraData> // I_Hx
<mixHash> 0 </mixHash> // I_Hm
<blockNonce> 0 </blockNonce> // I_Hn

<ommerBlockHeaders> [ .JSONList ] </ommerBlockHeaders>
<blockhash> .List </blockhash>

</evm>

// Ethereum Network
// ================

<network>

// Accounts Record
// ---------------

<activeAccounts> .Set </activeAccounts>
<accounts>
<account multiplicity="*" type="Map">
<acctID> 0 </acctID>
<balance> 0 </balance>
<code> .WordStack:AccountCode </code>
<storage> .Map </storage>
<nonce> 0 </nonce>
</account>
</accounts>

// Transactions Record
// -------------------

<txOrder> .List </txOrder>
<txPending> .List </txPending>

<messages>
<message multiplicity="*" type="Map">
<msgID> 0 </msgID>
<txNonce> 0 </txNonce> // T_n
<txGasPrice> 0 </txGasPrice> // T_p
<txGasLimit> 0 </txGasLimit> // T_g
<to> .Account </to> // T_t
<value> 0 </value> // T_v
<sigV> 0 </sigV> // T_w
<sigR> .WordStack </sigR> // T_r
<sigS> .WordStack </sigS> // T_s
<data> .WordStack </data> // T_i/T_e
</message>
</messages>

</network>

</ethereum>

syntax EthereumSimulation
syntax AccountCode ::= WordStack
Expand All @@ -169,10 +169,9 @@ Our semantics is modal, with the initial mode being set on the command line via
- `#setMode_` sets the mode to the supplied one.

```k
syntax Mode ::= "#setMode" Mode
// -------------------------------
syntax InternalOp ::= "#setMode" Mode
// -------------------------------------
rule <k> #setMode EXECMODE => . ... </k> <mode> _ => EXECMODE </mode>
rule <k> EX:Exception ~> (#setMode _ => .) ... </k>
```

State Stacks
Expand Down
Loading