From ba603b4200051603908446800ce00bc633420c91 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Tue, 21 Apr 2020 10:21:09 +0000 Subject: [PATCH 01/12] deps/wasm-semantics: update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 2e997c5..7575a3c 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 2e997c58c4f7a4af5e6c41604c9eca8c9a134fbd +Subproject commit 7575a3cab9fe05299e70b77310f9a70847141127 From 4c52694538e856ce9afe013acee5a813b6a2f8f8 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Tue, 21 Apr 2020 14:16:13 +0000 Subject: [PATCH 02/12] deps/wasm-semantics: update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 7575a3c..addbfcb 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 7575a3cab9fe05299e70b77310f9a70847141127 +Subproject commit addbfcbb4bb8192827fe0e949cd296d4a1441c6a From 5f0ac63b4f14101841e7671ca67cd055fe37008d Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Tue, 21 Apr 2020 16:31:17 +0000 Subject: [PATCH 03/12] deps/wasm-semantics: update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index addbfcb..7cc2210 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit addbfcbb4bb8192827fe0e949cd296d4a1441c6a +Subproject commit 7cc2210399ee16535b1c4641e54312b64157b3cd From a18017f993a7f531c2144fb11846f319df5507f0 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Tue, 21 Apr 2020 17:53:09 +0000 Subject: [PATCH 04/12] deps/wasm-semantics: update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 7cc2210..773ee43 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 7cc2210399ee16535b1c4641e54312b64157b3cd +Subproject commit 773ee434b03d7593eec59d993e8ae5c8ab092391 From 8bd57a79a3421a19e08e02f29029f083e9799b5a Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Wed, 22 Apr 2020 01:57:55 +0000 Subject: [PATCH 05/12] deps/wasm-semantics: update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 773ee43..39dfb66 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 773ee434b03d7593eec59d993e8ae5c8ab092391 +Subproject commit 39dfb666018a1eb209c093f692dcbe64b570deb6 From c730e94b86030a331b51bf6ccb40082b1c674df4 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Thu, 23 Apr 2020 10:15:24 +0000 Subject: [PATCH 06/12] deps/wasm-semantics: update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 39dfb66..1968196 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 39dfb666018a1eb209c093f692dcbe64b570deb6 +Subproject commit 1968196b855327c960943aa32161bf50671c24bf From 3268d1c17468f53a606b9097d30391f119b2ba52 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Thu, 23 Apr 2020 12:43:37 +0000 Subject: [PATCH 07/12] deps/wasm-semantics: update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 1968196..9c90a23 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 1968196b855327c960943aa32161bf50671c24bf +Subproject commit 9c90a2396109446a74f420fbae08cf71dfa6b814 From 313daa56952c10ca4a787bd4ec56328360e6b356 Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Fri, 24 Apr 2020 22:53:26 +0000 Subject: [PATCH 08/12] deps/wasm-semantics: update submodule --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index 9c90a23..efffc53 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit 9c90a2396109446a74f420fbae08cf71dfa6b814 +Subproject commit efffc53783bfd57953f52ffea4ac2a579164102f From 2a49753037a2eeb011877d789d29a3f8721bf32d Mon Sep 17 00:00:00 2001 From: RV Jenkins Date: Tue, 28 Apr 2020 15:44:04 +0000 Subject: [PATCH 09/12] deps/wasm-semantics: 75baf9b - Wrc20 balance fixes (#310) --- deps/wasm-semantics | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/wasm-semantics b/deps/wasm-semantics index efffc53..75baf9b 160000 --- a/deps/wasm-semantics +++ b/deps/wasm-semantics @@ -1 +1 @@ -Subproject commit efffc53783bfd57953f52ffea4ac2a579164102f +Subproject commit 75baf9b0db8cead6ae686881b9ce18ece6cc93f7 From 00f55c1a94d01132ecda3ec1a4cff355f206f02e Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 29 Apr 2020 17:02:39 +0000 Subject: [PATCH 10/12] Remove Java targets from Makefile --- Makefile | 29 ++++------------------------- 1 file changed, 4 insertions(+), 25 deletions(-) diff --git a/Makefile b/Makefile index abe0c51..a453e3b 100644 --- a/Makefile +++ b/Makefile @@ -21,9 +21,9 @@ export LUA_PATH .PHONY: all clean \ deps haskell-deps \ - defn defn-llvm defn-java defn-haskell \ + defn defn-llvm defn-haskell \ definition-deps wasm-definitions eei-definitions \ - build build-llvm build-java build-haskell \ + build build-llvm build-haskell \ test test-execution test-simple test-prove test-klab-prove \ media presentations reports @@ -52,12 +52,10 @@ deps: $(wasm_submodule)/make.timestamp $(eei_submodule)/make.timestamp definitio definition-deps: wasm-definitions eei-definitions wasm-definitions: - $(wasm_make) -B defn-java $(wasm_make) -B defn-llvm $(wasm_make) -B defn-haskell eei-definitions: $(eei_source_files) - $(eei_make) -B defn-java $(eei_make) -B defn-llvm $(eei_make) -B defn-haskell @@ -77,10 +75,6 @@ llvm_dir:=$(defn_dir)/llvm llvm_defn:=$(patsubst %, $(llvm_dir)/%, $(all_k_files)) llvm_kompiled:=$(llvm_dir)/ewasm-test-kompiled/interpreter -java_dir:=$(defn_dir)/java -java_defn:=$(patsubst %, $(java_dir)/%, $(all_k_files)) -java_kompiled:=$(java_dir)/ewasm-test-kompiled/compiled.txt - haskell_dir:=$(defn_dir)/haskell haskell_defn:=$(patsubst %, $(haskell_dir)/%, $(all_k_files)) haskell_kompiled:=$(haskell_dir)/ewasm-test-kompiled/definition.kore @@ -90,9 +84,8 @@ syntax_module=EWASM-TEST-SYNTAX # Tangle definition from *.md files -defn: defn-llvm defn-java defn-haskell +defn: defn-llvm defn-haskell defn-llvm: $(llvm_defn) -defn-java: $(java_defn) defn-haskell: $(haskell_defn) $(llvm_dir)/%.k: %.md $(tangler) @@ -100,11 +93,6 @@ $(llvm_dir)/%.k: %.md $(tangler) mkdir -p $(dir $@) pandoc --from markdown --to $(tangler) --metadata=code:.k $< > $@ -$(java_dir)/%.k: %.md $(tangler) - @echo "== tangle: $@" - mkdir -p $(dir $@) - pandoc --from markdown --to $(tangler) --metadata=code:.k $< > $@ - $(haskell_dir)/%.k: %.md $(tangler) @echo "== tangle: $@" mkdir -p $(dir $@) @@ -114,9 +102,8 @@ $(haskell_dir)/%.k: %.md $(tangler) KOMPILE_OPTS := -build: build-llvm build-java build-haskell +build: build-llvm build-haskell build-llvm: $(llvm_kompiled) -build-java: $(java_kompiled) build-haskell: $(haskell_kompiled) $(llvm_kompiled): $(llvm_defn) @@ -127,14 +114,6 @@ $(llvm_kompiled): $(llvm_defn) --syntax-module $(syntax_module) $< \ $(KOMPILE_OPTS) -$(java_kompiled): $(java_defn) - @echo "== kompile: $@" - $(k_bin)/kompile --backend java \ - --directory $(java_dir) -I $(java_dir) \ - --main-module $(main_module) \ - --syntax-module $(syntax_module) $< \ - $(KOMPILE_OPTS) - $(haskell_kompiled): $(haskell_defn) @echo "== kompile: $@" $(k_bin)/kompile --backend haskell \ From edab4e7eab45fb094a3bc5844465bad8ac76d7c2 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 29 Apr 2020 17:03:12 +0000 Subject: [PATCH 11/12] Remove klab targets from Makefile --- Makefile | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/Makefile b/Makefile index a453e3b..87dc80e 100644 --- a/Makefile +++ b/Makefile @@ -24,7 +24,7 @@ export LUA_PATH defn defn-llvm defn-haskell \ definition-deps wasm-definitions eei-definitions \ build build-llvm build-haskell \ - test test-execution test-simple test-prove test-klab-prove \ + test test-execution test-simple test-prove \ media presentations reports all: build @@ -157,9 +157,6 @@ tests/%.parse: tests/% tests/%.prove: tests/% $(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $(filter --repl, $(KPROVE_OPTS)) $< --format-failures --def-module $(KPROVE_MODULE) $(filter-out --repl, $(KPROVE_OPTS)) -tests/%.klab-prove: tests/% - $(TEST) klab-prove --backend java $(filter --repl, $(KPROVE_OPTS)) $< --format-failures --def-module $(KPROVE_MODULE) $(filter-out --repl, $(KPROVE_OPTS)) - ### Execution Tests test-execution: test-simple @@ -176,6 +173,3 @@ quick_proof_tests:=$(filter-out $(slow_proof_tests), $(proof_tests)) test-prove: $(proof_tests:=.prove) -### KLab interactive - -test-klab-prove: $(quick_proof_tests:=.klab-prove) From 125b46052debe1537dca777851e5da53e8d41b63 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 30 Apr 2020 09:32:59 +0000 Subject: [PATCH 12/12] Remove KLab and Java targets from kewasm script --- kewasm | 54 +++++++----------------------------------------------- 1 file changed, 7 insertions(+), 47 deletions(-) diff --git a/kewasm b/kewasm index 83e13eb..394fdf4 100755 --- a/kewasm +++ b/kewasm @@ -18,10 +18,6 @@ test_logs="$build_dir/logs" mkdir -p "$test_logs" test_log="$test_logs/tests.log" -KLAB_OUT="${KLAB_OUT:-$build_dir/klab}" -KLAB_NODE_STACK_SIZE="${KLAB_NODE_STACK_SIZE:-30000}" -export KLAB_OUT - # Utilities # --------- @@ -61,57 +57,24 @@ run_prove() { kprove --directory "$backend_dir" "$run_file" "$@" --haskell-backend-command "$haskell_backend_command" } -run_klab() { - local run_mode klab_log - - run_mode="$1" ; shift - klab_log="$(basename "${run_file%-spec.k}")" - - "$0" "$run_mode" --backend java "$run_file" \ - --state-log --state-log-path "$KLAB_OUT/data" --state-log-id "$klab_log" \ - --state-log-events OPEN,EXECINIT,SEARCHINIT,REACHINIT,REACHTARGET,REACHPROVED,NODE,RULE,SRULE,RULEATTEMPT,IMPLICATION,Z3QUERY,Z3RESULT,CLOSE \ - --output-flatten "_Map_ #And" \ - --output-tokenize "listStmt listValTypes <_>_ i32_WASM-DATA i64_WASM-DATA _:__WASM-DATA" \ - --no-alpha-renaming --restore-original-names --no-sort-collections \ - --output json \ - "$@" -} - -view_klab() { - local klab_log - - klab_log="$(basename "${run_file%-spec.k}")" - - # klab often runs out of stack space when running long-running KWasm programs - # klab debug "$klab_log" - node --stack-size=$KLAB_NODE_STACK_SIZE $(dirname $(which klab))/../libexec/klab-debug "$klab_log" -} - # Main # ---- usage() { echo " - usage: $0 run [--backend (llvm|java|haskell)] * - $0 kast [--backend (llvm|java)] * - $0 prove [--backend (java|haskell)] [--repl] * -m - $0 klab-run * - $0 klab-prove * -m - $0 klab-view [|] + usage: $0 run [--backend (llvm|haskell)] * + $0 kast [--backend (llvm)] * + $0 prove [--backend (haskell)] [--repl] * -m $0 run : Run a single WebAssembly program $0 kast : Parse a single WebAssembly program and output it in supported format $0 prove : Run a WebAssembly K proof - $0 klab-(run|prove) : Run or prove a spec and dump StateLogs which KLab can read - $0 klab-view : Launch KLab on the StateLog associated with the given program/spec. - Note: is a path to a file containing a WebAssembly program. + Note: is a path to a file containing a EWasm program. is a K specification to be proved. are any arguments you want to pass to K when executing/proving. is the format for Kast to output the term in. is the module to take as axioms for verification. - - KLab: Make sure that the 'klab/bin' directory is on your PATH to use this option. " } @@ -133,7 +96,6 @@ run_command="$1"; shift backend="llvm" repl=false [[ ! "$run_command" == 'prove' ]] || backend='haskell' -[[ ! "$run_command" =~ klab* ]] || backend='java' args=() while [[ $# -gt 0 ]]; do arg="$1" @@ -154,10 +116,8 @@ run_file="$1" ; shift [[ -f "$run_file" ]] || fatal "File does not exist: $run_file" case "$run_command-$backend" in - run-@(llvm|java|haskell) ) run_krun "$@" ;; - kast-@(llvm|java) ) run_kast "$@" ;; - prove-@(java|haskell) ) run_prove "$@" ;; - klab-@(run|prove)-java ) run_klab "${run_command#klab-}" "$@" ;; - klab-view-java ) view_klab "$@" ;; + run-@(llvm|haskell) ) run_krun "$@" ;; + kast-llvm ) run_kast "$@" ;; + prove-haskell ) run_prove "$@" ;; *) usage_fatal "Unknown command on '$backend' backend: $run_command" ;; esac