Skip to content
This repository was archived by the owner on Mar 23, 2023. It is now read-only.

Commit ffdd31e

Browse files
rv-jenkinshjorthjort
rv-jenkins
and
hjorthjort
authored
Update dependency: deps/wasm-semantics (#18)
* deps/wasm-semantics: update submodule * deps/wasm-semantics: update submodule * deps/wasm-semantics: update submodule * deps/wasm-semantics: update submodule * deps/wasm-semantics: update submodule * deps/wasm-semantics: update submodule * deps/wasm-semantics: update submodule * deps/wasm-semantics: update submodule * deps/wasm-semantics: 75baf9b - Wrc20 balance fixes (#310) * Remove Java targets from Makefile * Remove klab targets from Makefile * Remove KLab and Java targets from kewasm script Co-authored-by: hjorthjort <rikard.hjort@gmail.com>
1 parent f7ca6da commit ffdd31e

3 files changed

Lines changed: 13 additions & 80 deletions

File tree

‎Makefile‎

Lines changed: 5 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -21,10 +21,10 @@ export LUA_PATH
2121

2222
.PHONY: all clean \
2323
deps haskell-deps \
24-
defn defn-llvm defn-java defn-haskell \
24+
defn defn-llvm defn-haskell \
2525
definition-deps wasm-definitions eei-definitions \
26-
build build-llvm build-java build-haskell \
27-
test test-execution test-simple test-prove test-klab-prove \
26+
build build-llvm build-haskell \
27+
test test-execution test-simple test-prove \
2828
media presentations reports
2929

3030
all: build
@@ -52,12 +52,10 @@ deps: $(wasm_submodule)/make.timestamp $(eei_submodule)/make.timestamp definitio
5252
definition-deps: wasm-definitions eei-definitions
5353

5454
wasm-definitions:
55-
$(wasm_make) -B defn-java
5655
$(wasm_make) -B defn-llvm
5756
$(wasm_make) -B defn-haskell
5857

5958
eei-definitions: $(eei_source_files)
60-
$(eei_make) -B defn-java
6159
$(eei_make) -B defn-llvm
6260
$(eei_make) -B defn-haskell
6361

@@ -77,10 +75,6 @@ llvm_dir:=$(defn_dir)/llvm
7775
llvm_defn:=$(patsubst %, $(llvm_dir)/%, $(all_k_files))
7876
llvm_kompiled:=$(llvm_dir)/ewasm-test-kompiled/interpreter
7977

80-
java_dir:=$(defn_dir)/java
81-
java_defn:=$(patsubst %, $(java_dir)/%, $(all_k_files))
82-
java_kompiled:=$(java_dir)/ewasm-test-kompiled/compiled.txt
83-
8478
haskell_dir:=$(defn_dir)/haskell
8579
haskell_defn:=$(patsubst %, $(haskell_dir)/%, $(all_k_files))
8680
haskell_kompiled:=$(haskell_dir)/ewasm-test-kompiled/definition.kore
@@ -90,21 +84,15 @@ syntax_module=EWASM-TEST-SYNTAX
9084

9185
# Tangle definition from *.md files
9286

93-
defn: defn-llvm defn-java defn-haskell
87+
defn: defn-llvm defn-haskell
9488
defn-llvm: $(llvm_defn)
95-
defn-java: $(java_defn)
9689
defn-haskell: $(haskell_defn)
9790

9891
$(llvm_dir)/%.k: %.md $(tangler)
9992
@echo "== tangle: $@"
10093
mkdir -p $(dir $@)
10194
pandoc --from markdown --to $(tangler) --metadata=code:.k $< > $@
10295

103-
$(java_dir)/%.k: %.md $(tangler)
104-
@echo "== tangle: $@"
105-
mkdir -p $(dir $@)
106-
pandoc --from markdown --to $(tangler) --metadata=code:.k $< > $@
107-
10896
$(haskell_dir)/%.k: %.md $(tangler)
10997
@echo "== tangle: $@"
11098
mkdir -p $(dir $@)
@@ -114,9 +102,8 @@ $(haskell_dir)/%.k: %.md $(tangler)
114102

115103
KOMPILE_OPTS :=
116104

117-
build: build-llvm build-java build-haskell
105+
build: build-llvm build-haskell
118106
build-llvm: $(llvm_kompiled)
119-
build-java: $(java_kompiled)
120107
build-haskell: $(haskell_kompiled)
121108

122109
$(llvm_kompiled): $(llvm_defn)
@@ -127,14 +114,6 @@ $(llvm_kompiled): $(llvm_defn)
127114
--syntax-module $(syntax_module) $< \
128115
$(KOMPILE_OPTS)
129116

130-
$(java_kompiled): $(java_defn)
131-
@echo "== kompile: $@"
132-
$(k_bin)/kompile --backend java \
133-
--directory $(java_dir) -I $(java_dir) \
134-
--main-module $(main_module) \
135-
--syntax-module $(syntax_module) $< \
136-
$(KOMPILE_OPTS)
137-
138117
$(haskell_kompiled): $(haskell_defn)
139118
@echo "== kompile: $@"
140119
$(k_bin)/kompile --backend haskell \
@@ -178,9 +157,6 @@ tests/%.parse: tests/%
178157
tests/%.prove: tests/%
179158
$(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $(filter --repl, $(KPROVE_OPTS)) $< --format-failures --def-module $(KPROVE_MODULE) $(filter-out --repl, $(KPROVE_OPTS))
180159

181-
tests/%.klab-prove: tests/%
182-
$(TEST) klab-prove --backend java $(filter --repl, $(KPROVE_OPTS)) $< --format-failures --def-module $(KPROVE_MODULE) $(filter-out --repl, $(KPROVE_OPTS))
183-
184160
### Execution Tests
185161

186162
test-execution: test-simple
@@ -197,6 +173,3 @@ quick_proof_tests:=$(filter-out $(slow_proof_tests), $(proof_tests))
197173

198174
test-prove: $(proof_tests:=.prove)
199175

200-
### KLab interactive
201-
202-
test-klab-prove: $(quick_proof_tests:=.klab-prove)

‎deps/wasm-semantics‎

‎kewasm‎

Lines changed: 7 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -18,10 +18,6 @@ test_logs="$build_dir/logs"
1818
mkdir -p "$test_logs"
1919
test_log="$test_logs/tests.log"
2020

21-
KLAB_OUT="${KLAB_OUT:-$build_dir/klab}"
22-
KLAB_NODE_STACK_SIZE="${KLAB_NODE_STACK_SIZE:-30000}"
23-
export KLAB_OUT
24-
2521
# Utilities
2622
# ---------
2723

@@ -61,57 +57,24 @@ run_prove() {
6157
kprove --directory "$backend_dir" "$run_file" "$@" --haskell-backend-command "$haskell_backend_command"
6258
}
6359

64-
run_klab() {
65-
local run_mode klab_log
66-
67-
run_mode="$1" ; shift
68-
klab_log="$(basename "${run_file%-spec.k}")"
69-
70-
"$0" "$run_mode" --backend java "$run_file" \
71-
--state-log --state-log-path "$KLAB_OUT/data" --state-log-id "$klab_log" \
72-
--state-log-events OPEN,EXECINIT,SEARCHINIT,REACHINIT,REACHTARGET,REACHPROVED,NODE,RULE,SRULE,RULEATTEMPT,IMPLICATION,Z3QUERY,Z3RESULT,CLOSE \
73-
--output-flatten "_Map_ #And" \
74-
--output-tokenize "listStmt listValTypes <_>_ i32_WASM-DATA i64_WASM-DATA _:__WASM-DATA" \
75-
--no-alpha-renaming --restore-original-names --no-sort-collections \
76-
--output json \
77-
"$@"
78-
}
79-
80-
view_klab() {
81-
local klab_log
82-
83-
klab_log="$(basename "${run_file%-spec.k}")"
84-
85-
# klab often runs out of stack space when running long-running KWasm programs
86-
# klab debug "$klab_log"
87-
node --stack-size=$KLAB_NODE_STACK_SIZE $(dirname $(which klab))/../libexec/klab-debug "$klab_log"
88-
}
89-
9060
# Main
9161
# ----
9262

9363
usage() {
9464
echo "
95-
usage: $0 run [--backend (llvm|java|haskell)] <pgm> <K args>*
96-
$0 kast [--backend (llvm|java)] <pgm> <output format> <K args>*
97-
$0 prove [--backend (java|haskell)] [--repl] <spec> <K args>* -m <def_module>
98-
$0 klab-run <pgm> <K arg>*
99-
$0 klab-prove <spec> <K arg>* -m <def_module>
100-
$0 klab-view [<pgm>|<spec>]
65+
usage: $0 run [--backend (llvm|haskell)] <pgm> <K args>*
66+
$0 kast [--backend (llvm)] <pgm> <output format> <K args>*
67+
$0 prove [--backend (haskell)] [--repl] <spec> <K args>* -m <def_module>
10168
10269
$0 run : Run a single WebAssembly program
10370
$0 kast : Parse a single WebAssembly program and output it in supported format
10471
$0 prove : Run a WebAssembly K proof
105-
$0 klab-(run|prove) : Run or prove a spec and dump StateLogs which KLab can read
106-
$0 klab-view : Launch KLab on the StateLog associated with the given program/spec.
10772
108-
Note: <pgm> is a path to a file containing a WebAssembly program.
73+
Note: <pgm> is a path to a file containing a EWasm program.
10974
<spec> is a K specification to be proved.
11075
<K args> are any arguments you want to pass to K when executing/proving.
11176
<output format> is the format for Kast to output the term in.
11277
<def_module> is the module to take as axioms for verification.
113-
114-
KLab: Make sure that the 'klab/bin' directory is on your PATH to use this option.
11578
"
11679
}
11780

@@ -133,7 +96,6 @@ run_command="$1"; shift
13396
backend="llvm"
13497
repl=false
13598
[[ ! "$run_command" == 'prove' ]] || backend='haskell'
136-
[[ ! "$run_command" =~ klab* ]] || backend='java'
13799
args=()
138100
while [[ $# -gt 0 ]]; do
139101
arg="$1"
@@ -154,10 +116,8 @@ run_file="$1" ; shift
154116
[[ -f "$run_file" ]] || fatal "File does not exist: $run_file"
155117

156118
case "$run_command-$backend" in
157-
run-@(llvm|java|haskell) ) run_krun "$@" ;;
158-
kast-@(llvm|java) ) run_kast "$@" ;;
159-
prove-@(java|haskell) ) run_prove "$@" ;;
160-
klab-@(run|prove)-java ) run_klab "${run_command#klab-}" "$@" ;;
161-
klab-view-java ) view_klab "$@" ;;
119+
run-@(llvm|haskell) ) run_krun "$@" ;;
120+
kast-llvm ) run_kast "$@" ;;
121+
prove-haskell ) run_prove "$@" ;;
162122
*) usage_fatal "Unknown command on '$backend' backend: $run_command" ;;
163123
esac

0 commit comments

Comments
 (0)