diff --git a/Makefile b/Makefile index 90d905e0f9..3b7c010681 100644 --- a/Makefile +++ b/Makefile @@ -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 \ @@ -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 @@ -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 \ 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) @@ -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 @@ -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 diff --git a/driver.md b/driver.md index ef26726c7b..dd9e37d10a 100644 --- a/driver.md +++ b/driver.md @@ -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") ) @@ -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 run TESTID : { KEY : _ , REST } => run TESTID : { REST } ... requires KEY in #discardKeys ``` @@ -354,7 +354,6 @@ State Manipulation _ => 0 _ => 0 _ => .List - _ => .Set _ => .Map _ => .WordStack _ => 0 @@ -718,14 +717,6 @@ Here we check the other post-conditions associated with an EVM test. rule check "gas" : ((GLEFT:String) => #parseWord(GLEFT)) ... rule check "gas" : GLEFT => . ... GLEFT - rule check TESTID : { "callcreates" : CCREATES } => check "callcreates" : CCREATES ~> failure TESTID ... - // ----------------------------------------------------------------------------------------------------------------- - rule 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) } - ... - - rule check "callcreates" : C:Call => . ... CL requires C in CL - rule check TESTID : { "blockHeader" : BLOCKHEADER } => check "blockHeader" : BLOCKHEADER ~> failure TESTID // ---------------------------------------------------------------------------------------------------------- rule check "blockHeader" : { KEY : VALUE , REST } => check "blockHeader" : { KEY : VALUE } ~> check "blockHeader" : { REST } ... diff --git a/evm.md b/evm.md index c6db3238de..faf9745f39 100644 --- a/evm.md +++ b/evm.md @@ -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 $PGM:EthereumSimulation - 1 - $MODE:Mode - $SCHEDULE:Schedule - .Map - - - - // EVM Specific - // ============ - - - - // Mutable during a single transaction - // ----------------------------------- - - .WordStack // H_RETURN - .List - .List - .Set - .Set - - - .Map // I_b - .WordStack - - // I_* - 0 // I_a - 0 // I_s - .WordStack // I_d - 0 // I_v - - // \mu_* - .WordStack // \mu_s - .Map // \mu_m - 0 // \mu_pc - 0 // \mu_g - 0 // \mu_i - 0 - - false - 0 - - - // A_* (execution substate) - - .Set // A_s - .List // A_l - 0 // A_r - - - // Immutable during a single transaction - // ------------------------------------- - - 0 // I_p - 0 // I_o - - // I_H* (block information) - 0 // I_Hp - 0 // I_Ho - 0 // I_Hc - 0 // I_Hr - 0 // I_Ht - 0 // I_He - .WordStack // I_Hb - 0 // I_Hd - 0 // I_Hi - 0 // I_Hl - 0 // I_Hg - 0 // I_Hs - .WordStack // I_Hx - 0 // I_Hm - 0 // I_Hn - - [ .JSONList ] - .List - - - - // Ethereum Network - // ================ - - - - // Accounts Record - // --------------- - - .Set - - - 0 - 0 - .WordStack:AccountCode - .Map - 0 - - - - // Transactions Record - // ------------------- - - .List - .List - - - - 0 - 0 // T_n - 0 // T_p - 0 // T_g - .Account // T_t - 0 // T_v - 0 // T_w - .WordStack // T_r - .WordStack // T_s - .WordStack // T_i/T_e - - - - - - + configuration + $PGM:EthereumSimulation + 1 + $MODE:Mode + $SCHEDULE:Schedule + .Map + + + + // EVM Specific + // ============ + + + + // Mutable during a single transaction + // ----------------------------------- + + .WordStack // H_RETURN + .List + .List + .Set + + + .Map // I_b + .WordStack + + // I_* + 0 // I_a + 0 // I_s + .WordStack // I_d + 0 // I_v + + // \mu_* + .WordStack // \mu_s + .Map // \mu_m + 0 // \mu_pc + 0 // \mu_g + 0 // \mu_i + 0 + + false + 0 + + + // A_* (execution substate) + + .Set // A_s + .List // A_l + 0 // A_r + + + // Immutable during a single transaction + // ------------------------------------- + + 0 // I_p + 0 // I_o + + // I_H* (block information) + 0 // I_Hp + 0 // I_Ho + 0 // I_Hc + 0 // I_Hr + 0 // I_Ht + 0 // I_He + .WordStack // I_Hb + 0 // I_Hd + 0 // I_Hi + 0 // I_Hl + 0 // I_Hg + 0 // I_Hs + .WordStack // I_Hx + 0 // I_Hm + 0 // I_Hn + + [ .JSONList ] + .List + + + + // Ethereum Network + // ================ + + + + // Accounts Record + // --------------- + + .Set + + + 0 + 0 + .WordStack:AccountCode + .Map + 0 + + + + // Transactions Record + // ------------------- + + .List + .List + + + + 0 + 0 // T_n + 0 // T_p + 0 // T_g + .Account // T_t + 0 // T_v + 0 // T_w + .WordStack // T_r + .WordStack // T_s + .WordStack // T_i/T_e + + + + + + syntax EthereumSimulation syntax AccountCode ::= WordStack @@ -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 #setMode EXECMODE => . ... _ => EXECMODE - rule EX:Exception ~> (#setMode _ => .) ... ``` State Stacks diff --git a/kevm b/kevm index b9f372a973..8657265908 100755 --- a/kevm +++ b/kevm @@ -110,17 +110,28 @@ run_test_profile() { local test_file="$1" ; shift local start_time="$(date '+%s')" local exit_status='0' - run_test "$test_file" "$@" || exit_status="$?" + local output_log_dir="$test_logs/$(dirname -- "$test_file")" + local stdout_log="$test_logs/$test_file.out" + local stderr_log="$test_logs/$test_file.err" + [[ -d "$output_log_dir" ]] || mkdir -p "$output_log_dir" + run_test "$test_file" "$@" 1> "$stdout_log" 2> "$stderr_log" || exit_status="$?" local end_time="$(date '+%s')" if [[ "$exit_status" == '0' ]]; then echo "$test_file" >> "$now_passing" else echo "$test_file" >> "$now_failing" + cat "$stdout_log" + cat "$stderr_log" >&2 fi echo "$((end_time - start_time)) $test_file" >> "$run_times" exit "$exit_status" } +run_get_failing() { + count="${1:-1}" + cat "$now_failing" | sort -R | head -n"$count" +} + # Main # ---- @@ -137,6 +148,7 @@ case "$run_command" in interpret) run_interpreter "$@" ;; test) run_test "$@" ;; test-profile) run_test_profile "$@" ;; + get-failing) run_get_failing "$@" ;; *) echo " usage: $0 * @@ -161,6 +173,7 @@ case "$run_command" in $0 interpret Run a single EVM program (in JSON testing format) using fast interpreter $0 test Run a single EVM program like it's a test $0 test-profile Same as test, but generate list of failing tests and dump timing information + $0 get-failing [] Return a list of failing tests, at most . Note: is the expected output of the given test. These commands are more for devs and CI servers. diff --git a/tests/interactive/gas-analysis/sumTo10.evm.out b/tests/interactive/gas-analysis/sumTo10.evm.out index a0e23227a4..c294a23d62 100644 --- a/tests/interactive/gas-analysis/sumTo10.evm.out +++ b/tests/interactive/gas-analysis/sumTo10.evm.out @@ -29,9 +29,6 @@ .List - - .Set - .Set diff --git a/tests/proofs b/tests/proofs index 455a504cf0..205b030e9a 160000 --- a/tests/proofs +++ b/tests/proofs @@ -1 +1 @@ -Subproject commit 455a504cf04fef7984561970335bfa011045e233 +Subproject commit 205b030e9a9bcda0595d9a47a16be735637dca33 diff --git a/tests/templates/output-success.json b/tests/templates/output-success.json index 3fe267ceb8..0c7f3b6670 100644 --- a/tests/templates/output-success.json +++ b/tests/templates/output-success.json @@ -25,9 +25,6 @@ .List - - .Set - .Set diff --git a/tests/templates/output-success.kast b/tests/templates/output-success.kast deleted file mode 100644 index b5532f1bba..0000000000 --- a/tests/templates/output-success.kast +++ /dev/null @@ -1 +0,0 @@ -``(``(.K),``(#token("0","Int")),``(`SUCCESS_ETHEREUM-SIMULATION`(.KList)),``(`DEFAULT_EVM`(.KList)),``(`.Map`(.KList)),``(``(``(`.WordStack_EVM-DATA`(.KList)),``(`.List`(.KList)),``(`.List`(.KList)),``(`.List`(.KList)),``(`.Set`(.KList)),``(`.Set`(.KList)),``(``(`.Map`(.KList)),``(`.WordStack_EVM-DATA`(.KList)),``(#token("0","Int")),``(#token("0","Int")),``(`.WordStack_EVM-DATA`(.KList)),``(#token("0","Int")),``(`.WordStack_EVM-DATA`(.KList)),``(`.Map`(.KList)),``(#token("0","Int")),``(#token("0","Int")),``(#token("0","Int")),``(#token("0","Int")),``(#token("false","Bool")),``(#token("0","Int"))),``(``(`.Set`(.KList)),``(`.List`(.KList)),``(#token("0","Int"))),``(#token("0","Int")),``(#token("0","Int")),``(#token("0","Int")),``(#token("0","Int")),``(#token("0","Int")),``(#token("0","Int")),``(#token("0","Int")),``(#token("0","Int")),``(`.WordStack_EVM-DATA`(.KList)),``(#token("0","Int")),``(#token("0","Int")),``(#token("0","Int")),``(#token("0","Int")),``(#token("0","Int")),``(`.WordStack_EVM-DATA`(.KList)),``(#token("0","Int")),``(#token("0","Int")),``(`[_]_EVM-DATA`(`.List{"_,__EVM-DATA"}`(.KList))),``(`.List`(.KList))),``(``(`.Set`(.KList)),``(`.AccountCellMap`(.KList)),``(`.List`(.KList)),``(`.List`(.KList)),``(`.MessageCellMap`(.KList))))) \ No newline at end of file