Skip to content

Commit 133d028

Browse files
authored
Display final configuration on Web3 calls, add firefly_shutdown message (#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
1 parent e26718b commit 133d028

File tree

9 files changed

+121
-40
lines changed

9 files changed

+121
-40
lines changed

Jenkinsfile

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -66,9 +66,7 @@ pipeline {
6666
stage('Conformance (Web3)') {
6767
steps {
6868
sh '''
69-
nprocs=$(nproc)
70-
[ "$nprocs" -gt '16' ] && nprocs='16'
71-
make test-web3 -j"$nprocs"
69+
make test-web3
7270
'''
7371
}
7472
}

Makefile

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -389,6 +389,8 @@ CHECK:=git --no-pager diff --no-index --ignore-all-space
389389
KEVM_MODE:=NORMAL
390390
KEVM_SCHEDULE:=PETERSBURG
391391

392+
KEVM_WEB3_ARGS:=--shutdownable
393+
392394
test-all: test-all-conformance test-prove test-interactive test-parse
393395
test: test-conformance test-prove test-interactive test-parse
394396

@@ -419,15 +421,10 @@ tests/%.run-expected: tests/% tests/%.expected
419421
|| $(CHECK) tests/$*.expected tests/$*.$(TEST_CONCRETE_BACKEND)-out
420422
rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
421423

424+
tests/web3/no-shutdown/%: KEVM_WEB3_ARGS=
425+
422426
tests/%.run-web3: tests/%.in.json
423-
PORT=`tests/web3/get_port.py`; \
424-
./kevm web3 -p $$PORT & \
425-
while ! netcat -z 127.0.0.1 $$PORT; do \
426-
sleep 0.1; \
427-
done; \
428-
cat $^ | netcat 127.0.0.1 $$PORT -q 0 | diff - tests/$*.out.json; RESULT=$$? ; \
429-
pkill kevm-client -P $$$$ ; \
430-
[ $$? -eq 0 ]
427+
tests/web3/runtest.sh $< tests/$*.out.json $(KEVM_WEB3_ARGS)
431428

432429
tests/%.parse: tests/%
433430
$(TEST) kast --backend $(TEST_CONCRETE_BACKEND) $< kast > $@-out
@@ -482,7 +479,8 @@ failing_bchain_tests=$(shell cat tests/failing.$(TEST_CONCRETE_BACKEND))
482479
all_bchain_tests=$(filter-out $(bad_bchain_tests), $(filter-out $(failing_bchain_tests), $(bchain_tests)))
483480
quick_bchain_tests=$(filter-out $(slow_bchain_tests), $(all_bchain_tests))
484481

485-
web3_tests=$(wildcard tests/web3/*.in.json)
482+
web3_tests=$(wildcard tests/web3/*.in.json) \
483+
$(wildcard tests/web3/no-shutdown/*.in.json)
486484

487485
test-all-bchain: $(all_bchain_tests:=.run)
488486
test-slow-bchain: $(slow_bchain_tests:=.run)

deps/plugin

evm.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -169,6 +169,7 @@ Our semantics is modal, with the initial mode being set on the command line via
169169
```k
170170
syntax Mode ::= "NORMAL" [klabel(NORMAL), symbol]
171171
| "VMTESTS" [klabel(VMTESTS), symbol]
172+
// ---------------------------------------------------
172173
```
173174

174175
- `#setMode_` sets the mode to the supplied one.

kevm

Lines changed: 47 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,26 @@ run_search() {
6868
}
6969

7070
run_web3() {
71-
exec -a "$0 web3" ${defn_dir}/web3/kevm-client "$@"
71+
local web3_port
72+
web3_port="$1" ; shift
73+
run_file='-'
74+
exec -a "$0 web3" ${defn_dir}/web3/kevm-client -p "$web3_port" "$@" 3>&2 2>&1 1>&3 \
75+
| "$0" kast --backend web3 - pretty --input kore --module WEB3 --sort GeneratedTopCell
76+
}
77+
78+
run_web3_send() {
79+
local web3_port web3_method web3_params
80+
web3_port="$1" ; shift
81+
web3_method="$1" ; shift
82+
83+
join_args() {
84+
local IFS=','
85+
echo "$*"
86+
}
87+
web3_params="$(join_args "$@")"
88+
89+
echo '{"jsonrpc": "2.0", "id": 1, "method": "'"$web3_method"'", "params": ['"$web3_params"']}' \
90+
| netcat 127.0.0.1 "$web3_port" -q 0
7291
}
7392

7493
run_klab() {
@@ -139,22 +158,24 @@ run_command="$1" ; shift
139158

140159
if [[ "$run_command" == 'help' ]]; then
141160
echo "
142-
usage: $0 run [--backend (ocaml|java|llvm|haskell)] <pgm> <K arg>*
143-
$0 interpret [--backend (ocaml|llvm)] <pgm> <interpreter arg>*
144-
$0 kast [--backend (ocaml|java)] <pgm> <output format> <K arg>*
145-
$0 prove [--backend (java|haskell)] <spec> <K arg>* -m <def_module>
146-
$0 search [--backend (java|haskell)] <pgm> <pattern> <K arg>*
147-
$0 web3 [--backend (llvm)] -p <port>
148-
$0 klab-run <pgm> <K arg>*
149-
$0 klab-prove <spec> <K arg>* -m <def_module>
150-
$0 klab-view <spec>
161+
usage: $0 run [--backend (ocaml|java|llvm|haskell)] <pgm> <K arg>*
162+
$0 interpret [--backend (ocaml|llvm)] <pgm> <interpreter arg>*
163+
$0 kast [--backend (ocaml|java|llvm|haskell|web3)] <pgm> <output format> <K arg>*
164+
$0 prove [--backend (java|haskell)] <spec> <K arg>* -m <def_module>
165+
$0 search [--backend (java|haskell)] <pgm> <pattern> <K arg>*
166+
$0 web3 <port>
167+
$0 web3-send <port> <web3 method> <web3 params>
168+
$0 klab-run <pgm> <K arg>*
169+
$0 klab-prove <spec> <K arg>* -m <def_module>
170+
$0 klab-view <spec>
151171
152172
$0 run : Run a single EVM program
153173
$0 interpret : Run JSON EVM programs without K Frontend (external parser)
154174
$0 kast : Parse an EVM program and output it in a supported format
155175
$0 prove : Run an EVM K proof
156176
$0 search : Search for a K pattern in an EVM program execution
157177
$0 web3 : Run version of semantics which understand Web3 RPC (**UNDER CONSTRUCTION**)
178+
$0 web3-send : Send message to running Web3 instance of KEVM (**UNDER CONSTRUCTION**)
158179
$0 klab-(run|prove) : Run program or prove spec and dump StateLogs which KLab can read
159180
$0 klab-view : View the statelog associated with a given program or spec
160181
@@ -184,8 +205,14 @@ backend_dir="$defn_dir/$backend"
184205
[[ ! "$backend" == "ocaml" ]] || eval $(opam config env)
185206

186207
# get the run file
187-
if [[ ! "$run_command" == 'web3' ]]; then
208+
if [[ ! "$run_command" =~ web3* ]]; then
188209
run_file="$1" ; shift
210+
if [[ "$run_file" == '-' ]]; then
211+
tmp_input="$(mktemp)"
212+
trap "rm -rf $tmp_input" INT TERM EXIT
213+
cat - > "$tmp_input"
214+
run_file="$tmp_input"
215+
fi
189216
[[ -f "$run_file" ]] || fatal "File does not exist: $run_file"
190217
fi
191218

@@ -196,13 +223,14 @@ cCHAINID="#token(\"${CHAINID:-28346}\",\"Int\")"
196223
case "$run_command-$backend" in
197224

198225
# Running
199-
run-@(ocaml|java|llvm|haskell) ) run_krun "$@" ;;
200-
kast-@(ocaml|java|llvm|haskell) ) run_kast "$@" ;;
201-
interpret-@(ocaml|llvm) ) run_interpret "$@" ;;
202-
prove-@(java|haskell) ) run_prove "$@" ;;
203-
search-@(java|haskell) ) run_search "$@" ;;
204-
web3-@(llvm) ) run_web3 "$@" ;;
205-
klab-@(run|prove)-java ) run_klab "${run_command#klab-}" "$@" ;;
206-
klab-view-java ) view_klab "$@" ;;
226+
run-@(ocaml|java|llvm|haskell) ) run_krun "$@" ;;
227+
kast-@(ocaml|java|llvm|haskell|web3) ) run_kast "$@" ;;
228+
interpret-@(ocaml|llvm) ) run_interpret "$@" ;;
229+
prove-@(java|haskell) ) run_prove "$@" ;;
230+
search-@(java|haskell) ) run_search "$@" ;;
231+
web3-@(llvm) ) run_web3 "$@" ;;
232+
web3-send-@(llvm) ) run_web3_send "$@" ;;
233+
klab-@(run|prove)-java ) run_klab "${run_command#klab-}" "$@" ;;
234+
klab-view-java ) view_klab "$@" ;;
207235
*) $0 help ; fatal "Unknown command on backend: $run_command $backend" ;;
208236
esac
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": 1,
4+
"method": "net_version",
5+
"params": []
6+
}
7+
{
8+
"jsonrpc": "2.0",
9+
"id": 1,
10+
"method": "firefly_shutdown",
11+
"params": []
12+
}
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
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

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
#!/usr/bin/env bash
2+
3+
set -euo pipefail
4+
5+
input_file="$1" ; shift
6+
output_file="$1" ; shift
7+
8+
# Start Firefly
9+
PORT=$(tests/web3/get_port.py)
10+
./kevm web3 "$PORT" "$@" &
11+
kevm_client_pid="$!"
12+
while ! netcat -z 127.0.0.1 "$PORT"; do sleep 0.1; done
13+
14+
# Feed input in, store output in tmp file
15+
tmp_output_file="$(mktemp)"
16+
trap "rm -rf $tmp_output_file" INT TERM EXIT
17+
cat "$input_file" | netcat 127.0.0.1 "$PORT" -q 0 > "$tmp_output_file"
18+
19+
./kevm web3-send "$PORT" 'firefly_shutdown'
20+
echo
21+
timeout 20 tail --pid="$kevm_client_pid" -f /dev/null || true
22+
pkill -P "$kevm_client_pid" kevm-client || true
23+
timeout 20 tail --pid="$kevm_client_pid" -f /dev/null || true
24+
25+
exit_code='0'
26+
git --no-pager diff --no-index "$output_file" "$tmp_output_file" || exit_code="$?"
27+
28+
exit "$exit_code"

web3.md

Lines changed: 23 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,9 @@ module WEB3
1616
<chainID> $CHAINID:Int </chainID>
1717
</blockchain>
1818
<accountKeys> .Map </accountKeys>
19-
<snapshots> .List </snapshots>
19+
<snapshots> .List </snapshots>
2020
<web3socket> $SOCK:Int </web3socket>
21+
<web3shutdownable> $SHUTDOWNABLE:Bool </web3shutdownable>
2122
<web3clientsocket> 0:IOInt </web3clientsocket>
2223
<web3request>
2324
<jsonrpc> "":JSON </jsonrpc>
@@ -46,6 +47,7 @@ module WEB3
4647
rule #getString( KEY, J ) => {#getJSON( KEY, J )}:>String
4748
4849
syntax IOJSON ::= JSON | IOError
50+
// --------------------------------
4951
5052
syntax EthereumSimulation ::= accept() [symbol]
5153
// -----------------------------------------------
@@ -68,10 +70,10 @@ module WEB3
6870
syntax KItem ::= #loadRPCCall(IOJSON)
6971
// -------------------------------------
7072
rule <k> #loadRPCCall({ _ } #as J) => #checkRPCCall ~> #runRPCCall ... </k>
71-
<jsonrpc> _ => #getJSON("jsonrpc", J) </jsonrpc>
72-
<callid> _ => #getJSON("id" , J) </callid>
73-
<method> _ => #getJSON("method" , J) </method>
74-
<params> _ => #getJSON("params" , J) </params>
73+
<jsonrpc> _ => #getJSON("jsonrpc", J) </jsonrpc>
74+
<callid> _ => #getJSON("id" , J) </callid>
75+
<method> _ => #getJSON("method" , J) </method>
76+
<params> _ => #getJSON("params" , J) </params>
7577
7678
rule <k> #loadRPCCall(#EOF) => #shutdownWrite(SOCK) ~> #close(SOCK) ~> accept() ... </k>
7779
<web3clientsocket> SOCK </web3clientsocket>
@@ -107,7 +109,7 @@ module WEB3
107109
rule List2JSON(L) => List2JSON(L, .JSONList)
108110
109111
rule List2JSON(L ListItem(J), JS) => List2JSON(L, (J, JS))
110-
rule List2JSON(.List, JS) => [ JS ]
112+
rule List2JSON(.List , JS) => [ JS ]
111113
112114
syntax KItem ::= #sendResponse( JSON )
113115
// --------------------------------------
@@ -135,7 +137,7 @@ module WEB3
135137
rule <k> #checkRPCCall => . ...</k>
136138
<jsonrpc> "2.0" </jsonrpc>
137139
<method> _:String </method>
138-
<params> undef #Or [ _ ] #Or { _ } #Or undef </params>
140+
<params> undef #Or [ _ ] #Or { _ } </params>
139141
<callid> _:String #Or null #Or _:Int #Or undef </callid>
140142
141143
rule <k> #checkRPCCall => #sendResponse( "error": {"code": -32600, "message": "Invalid Request"} ) ... </k>
@@ -149,6 +151,8 @@ module WEB3
149151
150152
syntax KItem ::= "#runRPCCall"
151153
// ------------------------------
154+
rule <k> #runRPCCall => #firefly_shutdown ... </k>
155+
<method> "firefly_shutdown" </method>
152156
rule <k> #runRPCCall => #net_version ... </k>
153157
<method> "net_version" </method>
154158
rule <k> #runRPCCall => #web3_clientVersion ... </k>
@@ -176,13 +180,24 @@ module WEB3
176180
177181
rule <k> #runRPCCall => #sendResponse( "error": {"code": -32601, "message": "Method not found"} ) ... </k> [owise]
178182
183+
syntax KItem ::= "#firefly_shutdown"
184+
// ------------------------------------
185+
rule <k> #firefly_shutdown ~> _ => #putResponse({ "jsonrpc": "2.0" , "id": CALLID , "result": "Firefly client shutting down!" }, SOCK) </k>
186+
<web3shutdownable> true </web3shutdownable>
187+
<callid> CALLID </callid>
188+
<web3clientsocket> SOCK </web3clientsocket>
189+
<exit-code> _ => 0 </exit-code>
190+
191+
rule <k> #firefly_shutdown => #sendResponse( "error": {"code": -32800, "message": "Firefly client not started with `--shutdownable`!"} ) ... </k>
192+
<web3shutdownable> false </web3shutdownable>
193+
179194
syntax KItem ::= "#net_version"
180195
// -------------------------------
181196
rule <k> #net_version => #sendResponse( "result" : Int2String( CHAINID ) ) ... </k>
182197
<chainID> CHAINID </chainID>
183198
184199
syntax KItem ::= "#web3_clientVersion"
185-
// -------------------------------
200+
// --------------------------------------
186201
rule <k> #web3_clientVersion => #sendResponse( "result" : "Firefly RPC/v0.0.1/kevm" ) ... </k>
187202
188203
syntax KItem ::= "#eth_gasPrice"

0 commit comments

Comments
 (0)