diff --git a/Jenkinsfile b/Jenkinsfile
index fdcc43b..01e8226 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -11,7 +11,6 @@ pipeline {
when { changeRequest() }
steps { script { currentBuild.displayName = "PR ${env.CHANGE_ID}: ${env.CHANGE_TITLE}" } }
}
- stage('Definition Deps') { steps { sh 'make definition-deps -j4' } }
stage('Build') { steps { sh 'make build -j4' } }
stage('Test') {
options { timeout(time: 15, unit: 'MINUTES') }
diff --git a/Makefile b/Makefile
index 41f219d..4828c91 100644
--- a/Makefile
+++ b/Makefile
@@ -1,10 +1,13 @@
# Settings
# --------
-deps_dir := deps
-wasm_submodule := $(deps_dir)/wasm-semantics
-eei_submodule := $(deps_dir)/eei-semantics
-k_submodule := $(wasm_submodule)/deps/k
+BUILD_DIR := .build
+DEPS_DIR := deps
+DEFN_DIR := $(BUILD_DIR)/defn
+
+KWASM_SUBMODULE := $(DEPS_DIR)/wasm-semantics
+EEI_SUBMODULE := $(DEPS_DIR)/eei-semantics
+k_submodule := $(KWASM_SUBMODULE)/deps/k
ifneq (,$(wildcard $(k_submodule)/k-distribution/target/release/k/bin/*))
K_RELEASE ?= $(abspath $(k_submodule)/k-distribution/target/release/k)
@@ -15,123 +18,69 @@ K_BIN := $(K_RELEASE)/bin
K_LIB := $(K_RELEASE)/lib/kframework
export K_RELEASE
-PATH:=$(K_BIN):$(abspath $(wasm_submodule)):$(PATH)
+PATH:=$(K_BIN):$(abspath $(KWASM_SUBMODULE)):$(PATH)
export PATH
-build_dir := .build
-defn_dir := $(build_dir)/defn
-kompiled_dir_name := ewasm-test
-
-wasm_make := make --directory $(wasm_submodule) DEFN_DIR=../../$(defn_dir)
-eei_make := make --directory $(eei_submodule) DEFN_DIR=../../$(defn_dir)
-pandoc_tangle_submodule := $(wasm_submodule)/deps/pandoc-tangle
-tangler := $(pandoc_tangle_submodule)/tangle.lua
-LUA_PATH := $(pandoc_tangle_submodule)/?.lua;;
-export LUA_PATH
+KWASM_MAKE := make --directory $(KWASM_SUBMODULE) BUILD_DIR=../../$(BUILD_DIR) RELEASE=$(RELEASE)
-.PHONY: all clean \
- deps haskell-deps \
- defn defn-llvm defn-haskell \
- definition-deps wasm-definitions eei-definitions \
- build build-llvm build-haskell \
- test test-execution test-simple test-prove \
+.PHONY: all clean deps \
+ build \
+ test test-execution test-simple \
+ test-prove \
media presentations reports
all: build
clean:
- rm -rf $(build_dir)
- rm -f $(wasm_submodule)/make.timestamp
- rm -f $(eei_submodule)/make.timestamp
+ rm -rf $(BUILD_DIR)
git submodule update --init --recursive
- $(MAKE) clean -C $(wasm_submodule)
- $(MAKE) clean -C $(eei_submodule)
+ $(MAKE) clean -C $(KWASM_SUBMODULE)
+ $(MAKE) clean -C $(EEI_SUBMODULE)
# Build Dependencies (K Submodule)
# --------------------------------
-wasm_files=test.k wasm.k data.k kwasm-lemmas.k
-wasm_source_files:=$(patsubst %, $(wasm_submodule)/%, $(patsubst %.k, %.md, $(wasm_files)))
-eei_files:=eei.k
-eei_source_files:=$(patsubst %, $(eei_submodule)/%, $(patsubst %.k, %.md, $(eei_files)))
-ewasm_files:=ewasm-test.k driver.k ewasm.k kewasm-lemmas.k
-all_k_files:=$(ewasm_files) $(wasm_files) $(eei_files)
-
-deps: $(wasm_submodule)/make.timestamp $(eei_submodule)/make.timestamp definition-deps
-
-definition-deps: wasm-definitions eei-definitions
-
-wasm-definitions:
- $(wasm_make) -B defn-llvm
- $(wasm_make) -B defn-haskell
+EEI_FILES:=eei.md
+EEI_SOURCE_FILES:=$(patsubst %, $(EEI_SUBMODULE)/%, $(EEI_FILES))
+EWASM_FILES:=ewasm-test.md driver.md ewasm.md kewasm-lemmas.md
+EWASM_SOURCE_FILES:=$(EWASM_FILES)
+EXTRA_FILES:=$(EEI_FILES) $(EWASM_FILES)
+EXTRA_SOURCE_FILES:=$(patsubst %, $(KWASM_SUBMODULE)/%, $(EXTRA_FILES))
-eei-definitions: $(eei_source_files)
- $(eei_make) -B defn-llvm
- $(eei_make) -B defn-haskell
-
-$(wasm_submodule)/make.timestamp: $(wasm_source_files)
- git submodule update --init --recursive
- $(wasm_make) deps
- touch $(wasm_submodule)/make.timestamp
-
-$(eei_submodule)/make.timestamp: $(eei_source_files)
- git submodule update --init --recursive
- touch $(eei_submodule)/make.timestamp
+deps:
+ $(KWASM_MAKE) deps
# Building Definition
# -------------------
-llvm_dir:=$(defn_dir)/llvm
-llvm_defn:=$(patsubst %, $(llvm_dir)/%, $(all_k_files))
-llvm_kompiled:=$(llvm_dir)/ewasm-test-kompiled/interpreter
-
-haskell_dir:=$(defn_dir)/haskell
-haskell_defn:=$(patsubst %, $(haskell_dir)/%, $(all_k_files))
-haskell_kompiled:=$(haskell_dir)/ewasm-test-kompiled/definition.kore
-
-main_module=EWASM-TEST
-syntax_module=EWASM-TEST-SYNTAX
-
-# Tangle definition from *.md files
-
-defn: defn-llvm defn-haskell
-defn-llvm: $(llvm_defn)
-defn-haskell: $(haskell_defn)
-
-$(llvm_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 $@)
- pandoc --from markdown --to $(tangler) --metadata=code:.k $< > $@
+MAIN_MODULE=EWASM-TEST
+MAIN_SYNTAX_MODULE=EWASM-TEST-SYNTAX
+MAIN_DEFN_FILE=ewasm-test
# Build definitions
KOMPILE_OPTS :=
build: build-llvm build-haskell
-build-llvm: $(llvm_kompiled)
-build-haskell: $(haskell_kompiled)
-
-$(llvm_kompiled): $(llvm_defn)
- @echo "== kompile: $@"
- kompile --backend llvm \
- --directory $(llvm_dir) -I $(llvm_dir) \
- --main-module $(main_module) \
- --syntax-module $(syntax_module) $< \
- $(KOMPILE_OPTS)
-
-$(haskell_kompiled): $(haskell_defn)
- @echo "== kompile: $@"
- kompile --backend haskell \
- --directory $(haskell_dir) -I $(haskell_dir) \
- --main-module $(main_module) \
- --syntax-module $(syntax_module) $< \
- $(KOMPILE_OPTS)
+
+build-%: $(EXTRA_SOURCE_FILES)
+ $(KWASM_MAKE) build-$* \
+ DEFN_DIR=../../$(DEFN_DIR) \
+ llvm_main_module=$(MAIN_MODULE) \
+ llvm_syntax_module=$(MAIN_SYNTAX_MODULE) \
+ llvm_main_file=$(MAIN_DEFN_FILE) \
+ haskell_main_module=$(MAIN_MODULE) \
+ haskell_syntax_module=$(MAIN_SYNTAX_MODULE) \
+ haskell_main_file=$(MAIN_DEFN_FILE) \
+ EXTRA_SOURCE_FILES="$(EXTRA_FILES)" \
+ KOMPILE_OPTS="$(KOMPILE_OPTS)"
+
+$(KWASM_SUBMODULE)/%.md: %.md
+ cp $< $@
+
+$(KWASM_SUBMODULE)/%.md: $(EEI_SUBMODULE)/%.md
+ cp $< $@
# Testing
# -------
@@ -140,14 +89,10 @@ TEST_CONCRETE_BACKEND:=llvm
TEST_SYMBOLIC_BACKEND:=haskell
TEST:=./kewasm
KPROVE_MODULE:=KEWASM-LEMMAS
+KPROVE_MODULE_FILE=kewasm-lemmas.md
KPROVE_OPTS:=
CHECK:=git --no-pager diff --no-index --ignore-all-space
-tests/%/make.timestamp:
- @echo "== submodule: $@"
- git submodule update --init -- tests/$*
- touch $@
-
test: test-execution test-prove
# Generic Test Harnesses
@@ -165,7 +110,7 @@ tests/%.parse: tests/%
$(CHECK) $@-expected $@-out
rm -rf $@-out
-tests/%.prove: tests/%
+tests/%.prove: tests/% $(KWASM_SUBMODULE)/$(KPROVE_MODULE_FILE)
$(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $(filter --repl, $(KPROVE_OPTS)) $< --format-failures --def-module $(KPROVE_MODULE) $(filter-out --repl, $(KPROVE_OPTS))
### Execution Tests
diff --git a/deps/wasm-semantics b/deps/wasm-semantics
index a959393..d56298b 160000
--- a/deps/wasm-semantics
+++ b/deps/wasm-semantics
@@ -1 +1 @@
-Subproject commit a95939358242fd7050c0a94b606d04c1cb1e8fea
+Subproject commit d56298b602b7f5b30f6282125bb82610b68e7a7d
diff --git a/driver.md b/driver.md
index 1c7e069..28b4471 100644
--- a/driver.md
+++ b/driver.md
@@ -2,17 +2,19 @@ Ethereum Simulation
===================
```k
-require "ewasm.k"
-require "data.k"
+require "wasm-text.md"
+require "ewasm.md"
+require "data.md"
module DRIVER-SYNTAX
imports EWASM-SYNTAX
- imports WASM-SYNTAX
+ imports WASM-TEXT-SYNTAX
imports DRIVER
endmodule
module DRIVER
imports EWASM
+ imports WASM-TEXT
```
An Ewasm program is the invocation of an Ethereum contract containing Ewasm code.
@@ -111,7 +113,7 @@ Setting up the blockchain state
```k
syntax EthereumCommand ::= "#createContract" CallData ModuleDecl
// ----------------------------------------------------------------
- rule #createContract ADDRESS CODE => CODE ~> #storeModuleAt CallData2Int(ADDRESS) ...
+ rule #createContract ADDRESS CODE => text2abstract(CODE .Stmts) ~> #storeModuleAt CallData2Int(ADDRESS) ...
syntax EthereumCommand ::= "#storeModuleAt" CallData
// ----------------------------------------------------
diff --git a/ewasm-test.md b/ewasm-test.md
index afb0f12..a724d2f 100644
--- a/ewasm-test.md
+++ b/ewasm-test.md
@@ -4,8 +4,8 @@ Testing
We make use of the testing module for Wasm, which will let us make assertions about the Wasm runtime state.
```k
-requires "test.k" // WASM-TEST
-requires "driver.k"
+requires "test.md" // WASM-TEST
+requires "driver.md"
module EWASM-TEST-SYNTAX
imports WASM-TEST-SYNTAX
diff --git a/ewasm.md b/ewasm.md
index c3fb81a..1e34c25 100644
--- a/ewasm.md
+++ b/ewasm.md
@@ -2,11 +2,11 @@ Ewasm Specification
=================
```k
-require "wasm.k"
-require "eei.k"
+require "wasm.md"
+require "eei.md"
module EWASM-SYNTAX
- imports WASM-TOKEN-SYNTAX
+ imports WASM-SYNTAX
imports EWASM
endmodule
```
@@ -72,7 +72,7 @@ Then, when a `HostCall` instruction is encountered, parameters are gathered from
```k
rule ( import MODNAME FNAME (func OID:OptionalId TUSE:TypeUse) )
- => ( func OID TUSE .LocalDecls #eeiFunction(FNAME) .Instrs )
+ => #func(... type: TUSE, locals: .LocalDecls, body: #eeiFunction(FNAME) .Instrs, metadata: #meta(... id: OID, localIds: .Map))
...
requires MODNAME ==K #ethereumModule
diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md
index b1fa300..89d0b1f 100644
--- a/kewasm-lemmas.md
+++ b/kewasm-lemmas.md
@@ -5,8 +5,7 @@ These lemmas aid in verifying Ewasm programs behavior.
They are part of the *trusted* base, and so should be scrutinized carefully.
```k
-requires "kwasm-lemmas.k"
-requires "kewasm-lemmas.k"
+requires "kwasm-lemmas.md"
module KEWASM-LEMMAS
imports EWASM-TEST
diff --git a/tests/proofs/invoke-contract-spec.k b/tests/proofs/invoke-contract-spec.k
index c956858..1face3c 100644
--- a/tests/proofs/invoke-contract-spec.k
+++ b/tests/proofs/invoke-contract-spec.k
@@ -1,4 +1,4 @@
-requires "kewasm-lemmas.k"
+requires "kewasm-lemmas.md"
module INVOKE-CONTRACT-SPEC
imports KEWASM-LEMMAS
@@ -58,8 +58,5 @@ module INVOKE-CONTRACT-SPEC
...
-
- 0 => ?_
-
endmodule
diff --git a/tests/success-llvm.out b/tests/success-llvm.out
index 5969a42..e2e0683 100644
--- a/tests/success-llvm.out
+++ b/tests/success-llvm.out
@@ -143,9 +143,6 @@
true
-
- 0
-
.ParamStack