diff --git a/Jenkinsfile b/Jenkinsfile index 838b07fc71..cb6d34ff9c 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -66,9 +66,7 @@ pipeline { stage('Conformance (Web3)') { steps { sh ''' - nprocs=$(nproc) - [ "$nprocs" -gt '16' ] && nprocs='16' - make test-web3 -j"$nprocs" + make test-web3 ''' } } diff --git a/Makefile b/Makefile index abff96d1af..df4cd31e68 100644 --- a/Makefile +++ b/Makefile @@ -389,6 +389,8 @@ CHECK:=git --no-pager diff --no-index --ignore-all-space KEVM_MODE:=NORMAL KEVM_SCHEDULE:=PETERSBURG +KEVM_WEB3_ARGS:=--shutdownable + test-all: test-all-conformance test-prove test-interactive test-parse test: test-conformance test-prove test-interactive test-parse @@ -419,15 +421,10 @@ tests/%.run-expected: tests/% tests/%.expected || $(CHECK) tests/$*.expected tests/$*.$(TEST_CONCRETE_BACKEND)-out rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out +tests/web3/no-shutdown/%: KEVM_WEB3_ARGS= + tests/%.run-web3: tests/%.in.json - PORT=`tests/web3/get_port.py`; \ - ./kevm web3 -p $$PORT & \ - while ! netcat -z 127.0.0.1 $$PORT; do \ - sleep 0.1; \ - done; \ - cat $^ | netcat 127.0.0.1 $$PORT -q 0 | diff - tests/$*.out.json; RESULT=$$? ; \ - pkill kevm-client -P $$$$ ; \ - [ $$? -eq 0 ] + tests/web3/runtest.sh $< tests/$*.out.json $(KEVM_WEB3_ARGS) tests/%.parse: tests/% $(TEST) kast --backend $(TEST_CONCRETE_BACKEND) $< kast > $@-out @@ -482,7 +479,8 @@ failing_bchain_tests=$(shell cat tests/failing.$(TEST_CONCRETE_BACKEND)) all_bchain_tests=$(filter-out $(bad_bchain_tests), $(filter-out $(failing_bchain_tests), $(bchain_tests))) quick_bchain_tests=$(filter-out $(slow_bchain_tests), $(all_bchain_tests)) -web3_tests=$(wildcard tests/web3/*.in.json) +web3_tests=$(wildcard tests/web3/*.in.json) \ + $(wildcard tests/web3/no-shutdown/*.in.json) test-all-bchain: $(all_bchain_tests:=.run) test-slow-bchain: $(slow_bchain_tests:=.run) diff --git a/deps/plugin b/deps/plugin index 08b21dc2ca..d62fac05f4 160000 --- a/deps/plugin +++ b/deps/plugin @@ -1 +1 @@ -Subproject commit 08b21dc2ca19b60d3d6c1cef6be23983ec23a355 +Subproject commit d62fac05f44d811b092e3612fec8309f7e0ee1b4 diff --git a/evm.md b/evm.md index aefc51e019..795f74121b 100644 --- a/evm.md +++ b/evm.md @@ -169,6 +169,7 @@ Our semantics is modal, with the initial mode being set on the command line via ```k syntax Mode ::= "NORMAL" [klabel(NORMAL), symbol] | "VMTESTS" [klabel(VMTESTS), symbol] + // --------------------------------------------------- ``` - `#setMode_` sets the mode to the supplied one. diff --git a/kevm b/kevm index 0530000806..8149b469a0 100755 --- a/kevm +++ b/kevm @@ -68,7 +68,26 @@ run_search() { } run_web3() { - exec -a "$0 web3" ${defn_dir}/web3/kevm-client "$@" + local web3_port + web3_port="$1" ; shift + run_file='-' + exec -a "$0 web3" ${defn_dir}/web3/kevm-client -p "$web3_port" "$@" 3>&2 2>&1 1>&3 \ + | "$0" kast --backend web3 - pretty --input kore --module WEB3 --sort GeneratedTopCell +} + +run_web3_send() { + local web3_port web3_method web3_params + web3_port="$1" ; shift + web3_method="$1" ; shift + + join_args() { + local IFS=',' + echo "$*" + } + web3_params="$(join_args "$@")" + + echo '{"jsonrpc": "2.0", "id": 1, "method": "'"$web3_method"'", "params": ['"$web3_params"']}' \ + | netcat 127.0.0.1 "$web3_port" -q 0 } run_klab() { @@ -139,15 +158,16 @@ run_command="$1" ; shift if [[ "$run_command" == 'help' ]]; then echo " - usage: $0 run [--backend (ocaml|java|llvm|haskell)] * - $0 interpret [--backend (ocaml|llvm)] * - $0 kast [--backend (ocaml|java)] * - $0 prove [--backend (java|haskell)] * -m - $0 search [--backend (java|haskell)] * - $0 web3 [--backend (llvm)] -p - $0 klab-run * - $0 klab-prove * -m - $0 klab-view + usage: $0 run [--backend (ocaml|java|llvm|haskell)] * + $0 interpret [--backend (ocaml|llvm)] * + $0 kast [--backend (ocaml|java|llvm|haskell|web3)] * + $0 prove [--backend (java|haskell)] * -m + $0 search [--backend (java|haskell)] * + $0 web3 + $0 web3-send + $0 klab-run * + $0 klab-prove * -m + $0 klab-view $0 run : Run a single EVM program $0 interpret : Run JSON EVM programs without K Frontend (external parser) @@ -155,6 +175,7 @@ if [[ "$run_command" == 'help' ]]; then $0 prove : Run an EVM K proof $0 search : Search for a K pattern in an EVM program execution $0 web3 : Run version of semantics which understand Web3 RPC (**UNDER CONSTRUCTION**) + $0 web3-send : Send message to running Web3 instance of KEVM (**UNDER CONSTRUCTION**) $0 klab-(run|prove) : Run program or prove spec and dump StateLogs which KLab can read $0 klab-view : View the statelog associated with a given program or spec @@ -184,8 +205,14 @@ backend_dir="$defn_dir/$backend" [[ ! "$backend" == "ocaml" ]] || eval $(opam config env) # get the run file -if [[ ! "$run_command" == 'web3' ]]; then +if [[ ! "$run_command" =~ web3* ]]; then run_file="$1" ; shift + if [[ "$run_file" == '-' ]]; then + tmp_input="$(mktemp)" + trap "rm -rf $tmp_input" INT TERM EXIT + cat - > "$tmp_input" + run_file="$tmp_input" + fi [[ -f "$run_file" ]] || fatal "File does not exist: $run_file" fi @@ -196,13 +223,14 @@ cCHAINID="#token(\"${CHAINID:-28346}\",\"Int\")" case "$run_command-$backend" in # Running - run-@(ocaml|java|llvm|haskell) ) run_krun "$@" ;; - kast-@(ocaml|java|llvm|haskell) ) run_kast "$@" ;; - interpret-@(ocaml|llvm) ) run_interpret "$@" ;; - prove-@(java|haskell) ) run_prove "$@" ;; - search-@(java|haskell) ) run_search "$@" ;; - web3-@(llvm) ) run_web3 "$@" ;; - klab-@(run|prove)-java ) run_klab "${run_command#klab-}" "$@" ;; - klab-view-java ) view_klab "$@" ;; + run-@(ocaml|java|llvm|haskell) ) run_krun "$@" ;; + kast-@(ocaml|java|llvm|haskell|web3) ) run_kast "$@" ;; + interpret-@(ocaml|llvm) ) run_interpret "$@" ;; + prove-@(java|haskell) ) run_prove "$@" ;; + search-@(java|haskell) ) run_search "$@" ;; + web3-@(llvm) ) run_web3 "$@" ;; + web3-send-@(llvm) ) run_web3_send "$@" ;; + klab-@(run|prove)-java ) run_klab "${run_command#klab-}" "$@" ;; + klab-view-java ) view_klab "$@" ;; *) $0 help ; fatal "Unknown command on backend: $run_command $backend" ;; esac diff --git a/tests/web3/no-shutdown/net_version.in.json b/tests/web3/no-shutdown/net_version.in.json new file mode 100644 index 0000000000..54ec4b22d5 --- /dev/null +++ b/tests/web3/no-shutdown/net_version.in.json @@ -0,0 +1,12 @@ +{ + "jsonrpc": "2.0", + "id": 1, + "method": "net_version", + "params": [] +} +{ + "jsonrpc": "2.0", + "id": 1, + "method": "firefly_shutdown", + "params": [] +} diff --git a/tests/web3/no-shutdown/net_version.out.json b/tests/web3/no-shutdown/net_version.out.json new file mode 100644 index 0000000000..4b067249c5 --- /dev/null +++ b/tests/web3/no-shutdown/net_version.out.json @@ -0,0 +1 @@ +{"jsonrpc":"2.0","id":1,"result":"28346"}{"jsonrpc":"2.0","id":1,"error":{"code":-32800,"message":"Firefly client not started with `--shutdownable`!"}} \ No newline at end of file diff --git a/tests/web3/runtest.sh b/tests/web3/runtest.sh new file mode 100755 index 0000000000..92fe181c40 --- /dev/null +++ b/tests/web3/runtest.sh @@ -0,0 +1,28 @@ +#!/usr/bin/env bash + +set -euo pipefail + +input_file="$1" ; shift +output_file="$1" ; shift + +# Start Firefly +PORT=$(tests/web3/get_port.py) +./kevm web3 "$PORT" "$@" & +kevm_client_pid="$!" +while ! netcat -z 127.0.0.1 "$PORT"; do sleep 0.1; done + +# Feed input in, store output in tmp file +tmp_output_file="$(mktemp)" +trap "rm -rf $tmp_output_file" INT TERM EXIT +cat "$input_file" | netcat 127.0.0.1 "$PORT" -q 0 > "$tmp_output_file" + +./kevm web3-send "$PORT" 'firefly_shutdown' +echo +timeout 20 tail --pid="$kevm_client_pid" -f /dev/null || true +pkill -P "$kevm_client_pid" kevm-client || true +timeout 20 tail --pid="$kevm_client_pid" -f /dev/null || true + +exit_code='0' +git --no-pager diff --no-index "$output_file" "$tmp_output_file" || exit_code="$?" + +exit "$exit_code" diff --git a/web3.md b/web3.md index f2bfd0996f..816b43afcf 100644 --- a/web3.md +++ b/web3.md @@ -16,8 +16,9 @@ module WEB3 $CHAINID:Int .Map - .List + .List $SOCK:Int + $SHUTDOWNABLE:Bool 0:IOInt "":JSON @@ -46,6 +47,7 @@ module WEB3 rule #getString( KEY, J ) => {#getJSON( KEY, J )}:>String syntax IOJSON ::= JSON | IOError + // -------------------------------- syntax EthereumSimulation ::= accept() [symbol] // ----------------------------------------------- @@ -68,10 +70,10 @@ module WEB3 syntax KItem ::= #loadRPCCall(IOJSON) // ------------------------------------- rule #loadRPCCall({ _ } #as J) => #checkRPCCall ~> #runRPCCall ... - _ => #getJSON("jsonrpc", J) - _ => #getJSON("id" , J) - _ => #getJSON("method" , J) - _ => #getJSON("params" , J) + _ => #getJSON("jsonrpc", J) + _ => #getJSON("id" , J) + _ => #getJSON("method" , J) + _ => #getJSON("params" , J) rule #loadRPCCall(#EOF) => #shutdownWrite(SOCK) ~> #close(SOCK) ~> accept() ... SOCK @@ -107,7 +109,7 @@ module WEB3 rule List2JSON(L) => List2JSON(L, .JSONList) rule List2JSON(L ListItem(J), JS) => List2JSON(L, (J, JS)) - rule List2JSON(.List, JS) => [ JS ] + rule List2JSON(.List , JS) => [ JS ] syntax KItem ::= #sendResponse( JSON ) // -------------------------------------- @@ -135,7 +137,7 @@ module WEB3 rule #checkRPCCall => . ... "2.0" _:String - undef #Or [ _ ] #Or { _ } #Or undef + undef #Or [ _ ] #Or { _ } _:String #Or null #Or _:Int #Or undef rule #checkRPCCall => #sendResponse( "error": {"code": -32600, "message": "Invalid Request"} ) ... @@ -149,6 +151,8 @@ module WEB3 syntax KItem ::= "#runRPCCall" // ------------------------------ + rule #runRPCCall => #firefly_shutdown ... + "firefly_shutdown" rule #runRPCCall => #net_version ... "net_version" rule #runRPCCall => #web3_clientVersion ... @@ -176,13 +180,24 @@ module WEB3 rule #runRPCCall => #sendResponse( "error": {"code": -32601, "message": "Method not found"} ) ... [owise] + syntax KItem ::= "#firefly_shutdown" + // ------------------------------------ + rule #firefly_shutdown ~> _ => #putResponse({ "jsonrpc": "2.0" , "id": CALLID , "result": "Firefly client shutting down!" }, SOCK) + true + CALLID + SOCK + _ => 0 + + rule #firefly_shutdown => #sendResponse( "error": {"code": -32800, "message": "Firefly client not started with `--shutdownable`!"} ) ... + false + syntax KItem ::= "#net_version" // ------------------------------- rule #net_version => #sendResponse( "result" : Int2String( CHAINID ) ) ... CHAINID syntax KItem ::= "#web3_clientVersion" - // ------------------------------- + // -------------------------------------- rule #web3_clientVersion => #sendResponse( "result" : "Firefly RPC/v0.0.1/kevm" ) ... syntax KItem ::= "#eth_gasPrice"