Update dependency: deps/wasm-semantics

Makefile

@@ -21,10 +21,10 @@ 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 \
-        test test-execution test-simple test-prove test-klab-prove \
+        build build-llvm build-haskell \
+        test test-execution test-simple test-prove \
         media presentations reports
 
 all: build
@@ -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,21 +84,15 @@ 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)
 	@echo "==  tangle: $@"
 	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               \
@@ -178,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
@@ -197,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)

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)]      <pgm>  <K args>*
-           $0 kast       [--backend (llvm|java)]              <pgm>  <output format> <K args>*
-           $0 prove      [--backend (java|haskell)] [--repl]  <spec> <K args>* -m <def_module>
-           $0 klab-run                                        <pgm>  <K arg>*
-           $0 klab-prove                                      <spec> <K arg>* -m <def_module>
-           $0 klab-view                                       [<pgm>|<spec>]
+    usage: $0 run        [--backend (llvm|haskell)]      <pgm>  <K args>*
+           $0 kast       [--backend (llvm)]              <pgm>  <output format> <K args>*
+           $0 prove      [--backend (haskell)] [--repl]  <spec> <K args>* -m <def_module>
 
        $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: <pgm> is a path to a file containing a WebAssembly program.
+       Note: <pgm> is a path to a file containing a EWasm program.
              <spec> is a K specification to be proved.
              <K args> are any arguments you want to pass to K when executing/proving.
              <output format> is the format for Kast to output the term in.
              <def_module> 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