Display final configuration on Web3 calls, add firefly_shutdown messa…

…ge (#446)

* evm: formatting

* web3: formatting

* web3: remove redundant #Or undef

* web3: add #kevm_shutdown message

* kevm: allow input file from stdin

* kevm: simpler inferface to web3 server, port is mandatory

* kevm: wrapper web3-send for interacting with running web3 server

* Makefile: formatting

* Makefile, tests/web3/runtest: separate out web3 test runner

* web3: only allow shutting down in SHUTDOWNABLE is set to true

* tests/web3/runtest.sh: make sure client is really dead no matter what

* Makefile, tests/web3/no-shutdown: test both with/without --shutdownable

* evm: formatting

* deps/plugin: update submodule

* Makefile, tests/web3/runtest: saner output for test-web3

* Jenkinsfile: test-web3 in sequence for saner output

* Makefile: increase timeout for test-web3 to 10s

* tests/web3/runtest: kill kevm-client specifically

* tests/web3/runtest.sh: explicitly wait for kevm client to shut down

* tests/web3/runtest.sh: make sure timeout doesnt force test to fail

* tests/web3/runtest: make sure parent process is killed too

* Makefile: no need for sleep 10

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
                 '''
               }
             }

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)

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.

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,22 +158,24 @@ run_command="$1" ; shift
 
 if [[ "$run_command" == 'help' ]]; then
     echo "
-        usage: $0 run        [--backend (ocaml|java|llvm|haskell)] <pgm>  <K arg>*
-               $0 interpret  [--backend (ocaml|llvm)]              <pgm>  <interpreter arg>*
-               $0 kast       [--backend (ocaml|java)]              <pgm>  <output format> <K arg>*
-               $0 prove      [--backend (java|haskell)]            <spec> <K arg>* -m <def_module>
-               $0 search     [--backend (java|haskell)]            <pgm>  <pattern> <K arg>*
-               $0 web3       [--backend (llvm)]                    -p <port>
-               $0 klab-run                                         <pgm>  <K arg>*
-               $0 klab-prove                                       <spec> <K arg>* -m <def_module>
-               $0 klab-view                                        <spec>
+        usage: $0 run        [--backend (ocaml|java|llvm|haskell)]      <pgm>  <K arg>*
+               $0 interpret  [--backend (ocaml|llvm)]                   <pgm>  <interpreter arg>*
+               $0 kast       [--backend (ocaml|java|llvm|haskell|web3)] <pgm>  <output format> <K arg>*
+               $0 prove      [--backend (java|haskell)]                 <spec> <K arg>* -m <def_module>
+               $0 search     [--backend (java|haskell)]                 <pgm>  <pattern> <K arg>*
+               $0 web3                                                  <port>
+               $0 web3-send                                             <port> <web3 method> <web3 params>
+               $0 klab-run                                              <pgm>  <K arg>*
+               $0 klab-prove                                            <spec> <K arg>* -m <def_module>
+               $0 klab-view                                             <spec>
 
            $0 run       : Run a single EVM program
            $0 interpret : Run JSON EVM programs without K Frontend (external parser)
            $0 kast      : Parse an EVM program and output it in a supported format
            $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

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": []
+}

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`!"}}

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"

web3.md

@@ -16,8 +16,9 @@ module WEB3
           <chainID> $CHAINID:Int </chainID>
         </blockchain>
         <accountKeys> .Map </accountKeys>
-        <snapshots> .List </snapshots> 
+        <snapshots> .List </snapshots>
         <web3socket> $SOCK:Int </web3socket>
+        <web3shutdownable> $SHUTDOWNABLE:Bool </web3shutdownable>
         <web3clientsocket> 0:IOInt </web3clientsocket>
         <web3request>
           <jsonrpc> "":JSON </jsonrpc>
@@ -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 <k> #loadRPCCall({ _ } #as J) => #checkRPCCall ~> #runRPCCall ... </k>
-         <jsonrpc> _             => #getJSON("jsonrpc", J) </jsonrpc>
-         <callid>  _             => #getJSON("id"     , J) </callid>
-         <method>  _             => #getJSON("method" , J) </method>
-         <params>  _             => #getJSON("params" , J) </params>
+         <jsonrpc> _ => #getJSON("jsonrpc", J) </jsonrpc>
+         <callid>  _ => #getJSON("id"     , J) </callid>
+         <method>  _ => #getJSON("method" , J) </method>
+         <params>  _ => #getJSON("params" , J) </params>
 
     rule <k> #loadRPCCall(#EOF) => #shutdownWrite(SOCK) ~> #close(SOCK) ~> accept() ... </k>
          <web3clientsocket> SOCK </web3clientsocket>
@@ -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 <k> #checkRPCCall => . ...</k>
          <jsonrpc> "2.0" </jsonrpc>
          <method> _:String </method>
-         <params> undef #Or [ _ ] #Or { _ } #Or undef </params>
+         <params> undef #Or [ _ ] #Or { _ } </params>
          <callid> _:String #Or null #Or _:Int #Or undef </callid>
 
     rule <k> #checkRPCCall => #sendResponse( "error": {"code": -32600, "message": "Invalid Request"} ) ... </k>
@@ -149,6 +151,8 @@ module WEB3
 
     syntax KItem ::= "#runRPCCall"
  // ------------------------------
+    rule <k> #runRPCCall => #firefly_shutdown ... </k>
+         <method> "firefly_shutdown" </method>
     rule <k> #runRPCCall => #net_version ... </k>
          <method> "net_version" </method>
     rule <k> #runRPCCall => #web3_clientVersion ... </k>
@@ -176,13 +180,24 @@ module WEB3
 
     rule <k> #runRPCCall => #sendResponse( "error": {"code": -32601, "message": "Method not found"} ) ... </k> [owise]
 
+    syntax KItem ::= "#firefly_shutdown"
+ // ------------------------------------
+    rule <k> #firefly_shutdown ~> _ => #putResponse({ "jsonrpc": "2.0" , "id": CALLID , "result": "Firefly client shutting down!" }, SOCK) </k>
+         <web3shutdownable> true </web3shutdownable>
+         <callid> CALLID </callid>
+         <web3clientsocket> SOCK </web3clientsocket>
+         <exit-code> _ => 0 </exit-code>
+
+    rule <k> #firefly_shutdown => #sendResponse( "error": {"code": -32800, "message": "Firefly client not started with `--shutdownable`!"} ) ... </k>
+         <web3shutdownable> false </web3shutdownable>
+
     syntax KItem ::= "#net_version"
  // -------------------------------
     rule <k> #net_version => #sendResponse( "result" : Int2String( CHAINID ) ) ... </k>
          <chainID> CHAINID </chainID>
 
     syntax KItem ::= "#web3_clientVersion"
- // -------------------------------
+ // --------------------------------------
     rule <k> #web3_clientVersion => #sendResponse( "result" : "Firefly RPC/v0.0.1/kevm" ) ... </k>
 
     syntax KItem ::= "#eth_gasPrice"