diff --git a/.build/k b/.build/k
index a27fd3e..7a1ad9e 160000
--- a/.build/k
+++ b/.build/k
@@ -1 +1 @@
-Subproject commit a27fd3eb30327c044d5524836a0b223fb63e1e5b
+Subproject commit 7a1ad9ef2fbadf9a6f0ec0d2a9f90cfab9d0e145
diff --git a/Dockerfile b/Dockerfile
new file mode 100644
index 0000000..6c5eeb7
--- /dev/null
+++ b/Dockerfile
@@ -0,0 +1,34 @@
+FROM ubuntu:bionic
+
+ENV TZ=America/Chicago
+RUN ln --symbolic --no-dereference --force /usr/share/zoneinfo/$TZ /etc/localtime \
+ && echo $TZ > /etc/timezone
+
+RUN apt update \
+ && apt upgrade --yes \
+ && apt install --yes \
+ autoconf curl flex gcc libffi-dev libmpfr-dev libtool libz3-dev make \
+ maven opam openjdk-8-jdk pandoc pkg-config python3 python-pygments \
+ python-recommonmark python-sphinx time zlib1g-dev z3
+
+RUN update-alternatives --set java /usr/lib/jvm/java-8-openjdk-amd64/jre/bin/java
+
+RUN curl -sSL https://get.haskellstack.org/ | sh
+
+ARG USER_ID=1000
+ARG GROUP_ID=1000
+RUN groupadd --gid $GROUP_ID user \
+ && useradd --create-home --uid $USER_ID --shell /bin/sh --gid user user
+
+USER $USER_ID:$GROUP_ID
+
+ADD .build/k/k-distribution/src/main/scripts/bin/k-configure-opam-dev .build/k/k-distribution/src/main/scripts/bin/k-configure-opam-common /home/user/.tmp-opam/bin/
+ADD .build/k/k-distribution/src/main/scripts/lib/opam /home/user/.tmp-opam/lib/opam/
+RUN cd /home/user \
+ && ./.tmp-opam/bin/k-configure-opam-dev
+
+ENV LC_ALL=C.UTF-8
+ADD --chown=user:user .build/k/haskell-backend/src/main/native/haskell-backend/stack.yaml /home/user/.tmp-haskell/
+ADD --chown=user:user .build/k/haskell-backend/src/main/native/haskell-backend/kore/package.yaml /home/user/.tmp-haskell/kore/
+RUN cd /home/user/.tmp-haskell \
+ && stack build --only-snapshot --test --bench --no-haddock-deps --haddock --library-profiling
diff --git a/Jenkinsfile b/Jenkinsfile
new file mode 100644
index 0000000..243b811
--- /dev/null
+++ b/Jenkinsfile
@@ -0,0 +1,59 @@
+pipeline {
+ agent {
+ dockerfile {
+ additionalBuildArgs '--build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)'
+ }
+ }
+ stages {
+ stage("Init title") {
+ when { changeRequest() }
+ steps {
+ script {
+ currentBuild.displayName = "PR ${env.CHANGE_ID}: ${env.CHANGE_TITLE}"
+ }
+ }
+ }
+ stage('Dependencies') {
+ steps {
+ ansiColor('xterm') {
+ sh '''
+ make clean
+ make deps
+ '''
+ }
+ }
+ }
+ stage('Build') {
+ steps {
+ ansiColor('xterm') {
+ sh '''
+ make build -j4
+ '''
+ }
+ }
+ }
+ stage('Test') {
+ parallel {
+ stage('IMP') {
+ steps {
+ ansiColor('xterm') {
+ sh '''
+ make test-imp -j8
+ '''
+ }
+ }
+ }
+ stage('FUN') {
+ steps {
+ ansiColor('xterm') {
+ sh '''
+ echo "SKIPPING!!!"
+ # make test-fun -j8
+ '''
+ }
+ }
+ }
+ }
+ }
+ }
+}
diff --git a/Makefile b/Makefile
index b65e460..2be5673 100644
--- a/Makefile
+++ b/Makefile
@@ -3,136 +3,146 @@
build_dir:=.build
defn_dir:=$(build_dir)/defn
-
k_submodule:=$(build_dir)/k
-k_bin:=$(k_submodule)/k-distribution/target/release/k/bin
-kompile:=$(k_bin)/kompile
-krun:=$(k_bin)/krun
-
pandoc_tangle_submodule:=$(build_dir)/pandoc-tangle
+k_bin:=$(k_submodule)/k-distribution/target/release/k/bin
tangler:=$(pandoc_tangle_submodule)/tangle.lua
-LUA_PATH:=$(pandoc_tangle_submodule)/?.lua;;
-export LUA_PATH
-pandoc:=pandoc --from markdown --to markdown --lua-filter "$(tangler)"
-test_dir:=tests
-test_output:=.build/logs
+LUA_PATH=$(pandoc_tangle_submodule)/?.lua;;
+export LUA_PATH
-.PHONY: deps deps-k deps-ocaml deps-tangle \
- defn defn-imp defn-imp-kcompile defn-imp-krun defn-fun defn-fun-krun defn-fun-kcompile \
- build build-imp build-imp-kcompile build-imp-krun build-fun build-fun-krun build-fun-kcompile \
- test test-imp test-fun
+.PHONY: all clean \
+ deps ocaml-deps haskell-deps \
+ defn defn-imp defn-imp-ocaml defn-imp-java defn-fun defn-fun-ocaml defn-fun-java \
+ build build-imp build-imp-ocaml build-imp-java build-fun build-fun-ocaml build-fun-java \
+ test test-imp test-fun
all: build
clean:
rm -rf $(build_dir)
+ git submodule update --init --recursive
-# Dependencies
-# ------------
+# Build Dependencies (K Submodule)
+# --------------------------------
-deps: deps-k deps-ocaml deps-tangle
-deps-k: $(k_submodule)/make.timestamp
-deps-tangle: $(pandoc_tangle_submodule)/make.timestamp
+deps: $(k_submodule)/make.timestamp $(pandoc_tangle_submodule)/make.timestamp ocaml-deps
$(k_submodule)/make.timestamp:
- git submodule update --init -- $(k_submodule)
- cd $(k_submodule) \
- && mvn package -q -DskipTests
+ git submodule update --init --recursive
+ cd $(k_submodule) && mvn package -DskipTests -Dllvm.backend.skip
touch $(k_submodule)/make.timestamp
$(pandoc_tangle_submodule)/make.timestamp:
git submodule update --init -- $(pandoc_tangle_submodule)
touch $(pandoc_tangle_submodule)/make.timestamp
-deps-ocaml:
- opam init --quiet --no-setup
- opam repository add k "$(k_submodule)/k-distribution/target/release/k/lib/opam" \
- || opam repository set-url k "$(k_submodule)/k-distribution/target/release/k/lib/opam"
- opam update
- opam switch 4.06.1+k
+ocaml-deps:
eval $$(opam config env) \
- opam install --yes mlgmp zarith uuidm ocaml-protoc rlp yojson hex ocp-ocamlres
+ opam install --yes mlgmp zarith uuidm
+
+# Building Definition
+# -------------------
+
+imp_defn_dir:=$(defn_dir)/imp
+imp_krun_files:=imp.k
+imp_kcompile_files:=kat-imp.k kat.k imp.k
+
+imp_ocaml_dir:=$(imp_defn_dir)/ocaml
+imp_ocaml_defn:=$(patsubst %, $(imp_ocaml_dir)/%, $(imp_krun_files))
+imp_ocaml_kompiled:=$(imp_ocaml_dir)/imp-kompiled/interpreter
-# Build definition
-# ----------------
+imp_java_dir:=$(imp_defn_dir)/java
+imp_java_defn:=$(patsubst %, $(imp_java_dir)/%, $(imp_kcompile_files))
+imp_java_kompiled:=$(imp_java_dir)/kat-imp-kompiled/compiled.txt
-imp_dir=$(defn_dir)/imp
-imp_kcompile_files:=$(patsubst %, $(imp_dir)/kcompile/%, kat-imp.k kat.k imp.k)
-imp_krun_files:=$(patsubst %, $(imp_dir)/krun/%, imp.k)
+fun_defn_dir:=$(defn_dir)/fun
+fun_krun_files:=fun.k
+fun_kcompile_files:=kat-fun.k kat.k fun.k
-fun_dir=$(defn_dir)/fun
-fun_kcompile_files:=$(patsubst %, $(fun_dir)/kcompile/%, kat-fun.k kat.k fun.k)
-fun_krun_files:=$(patsubst %, $(fun_dir)/krun/%, fun.k)
+fun_ocaml_dir:=$(fun_defn_dir)/ocaml
+fun_ocaml_defn:=$(patsubst %, $(fun_ocaml_dir)/%, $(fun_krun_files))
+fun_ocaml_kompiled:=$(fun_ocaml_dir)/fun-kompiled/interpreter
+
+fun_java_dir:=$(fun_defn_dir)/java
+fun_java_defn:=$(patsubst %, $(fun_java_dir)/%, $(fun_kcompile_files))
+fun_java_kompiled:=$(fun_java_dir)/kat-fun-kompiled/compiled.txt
+
+# Tangle definition from *.md files
+
+krun_tangler:='.k,.krun'
+kcompile_tangler:='.k,.kcompile'
defn: defn-imp defn-fun
+defn-imp: defn-imp-ocaml defn-imp-java
+defn-fun: defn-fun-ocaml defn-fun-java
-defn-imp: defn-imp-kcompile defn-imp-krun
-defn-imp-kcompile: $(imp_kcompile_files)
-defn-imp-krun: $(imp_krun_files)
+defn-imp-ocaml: $(imp_ocaml_defn)
+defn-imp-java: $(imp_java_defn)
+defn-fun-ocaml: $(fun_ocaml_defn)
+defn-fun-java: $(fun_java_defn)
-$(imp_dir)/kcompile/%.k: %.md
- @echo >&2 "== tangle: $@"
+$(imp_ocaml_dir)/%.k: %.md $(pandoc_tangle_submodule)/make.timestamp
+ @echo "== tangle: $@"
mkdir -p $(dir $@)
- $(pandoc) --metadata=code:'.k,.kcompile' $< > $@
+ pandoc --from markdown --to markdown --lua-filter=$(tangler) --metadata=code:$(krun_tangler) $< > $@
-$(imp_dir)/krun/%.k: %.md
- @echo >&2 "== tangle: $@"
+$(imp_java_dir)/%.k: %.md $(pandoc_tangle_submodule)/make.timestamp
+ @echo "== tangle: $@"
mkdir -p $(dir $@)
- $(pandoc) --metadata=code:'.k,.krun' $< > $@
+ pandoc --from markdown --to markdown --lua-filter=$(tangler) --metadata=code:$(kcompile_tangler) $< > $@
-defn-fun: defn-fun-kcompile defn-fun-krun
-defn-fun-kcompile: $(fun_kcompile_files)
-defn-fun-krun: $(fun_krun_files)
-
-$(fun_dir)/kcompile/%.k: %.md
- @echo >&2 "== tangle: $@"
+$(fun_ocaml_dir)/%.k: %.md $(pandoc_tangle_submodule)/make.timestamp
+ @echo "== tangle: $@"
mkdir -p $(dir $@)
- $(pandoc) --metadata=code:'.k,.kcompile' $< > $@
+ pandoc --from markdown --to markdown --lua-filter=$(tangler) --metadata=code:$(krun_tangler) $< > $@
-$(fun_dir)/krun/%.k: %.md
- @echo >&2 "== tangle: $@"
+$(fun_java_dir)/%.k: %.md $(pandoc_tangle_submodule)/make.timestamp
+ @echo "== tangle: $@"
mkdir -p $(dir $@)
- $(pandoc) --metadata=code:'.k,.krun' $< > $@
+ pandoc --from markdown --to markdown --lua-filter=$(tangler) --metadata=code:$(kcompile_tangler) $< > $@
-# Backends (for running and compiling)
+# Build definitions
build: build-imp build-fun
+build-imp: build-imp-ocaml build-imp-java
+build-fun: build-fun-ocaml build-fun-java
-build-imp: build-imp-kcompile build-imp-krun
-build-imp-kcompile: $(imp_dir)/kcompile/kat-imp-kompiled/timestamp
-build-imp-krun: $(imp_dir)/krun/imp-kompiled/interpreter
+build-imp-ocaml: $(imp_ocaml_kompiled)
+build-imp-java: $(imp_java_kompiled)
+build-fun-ocaml: $(fun_ocaml_kompiled)
+build-fun-java: $(fun_java_kompiled)
-$(imp_dir)/kcompile/kat-imp-kompiled/timestamp: $(imp_kcompile_files)
+$(imp_ocaml_kompiled): $(imp_ocaml_defn)
@echo "== kompile: $@"
- $(kompile) --main-module IMP-ANALYSIS --backend java \
- --syntax-module IMP-ANALYSIS $< --directory $(imp_dir)/kcompile
+ eval $$(opam config env) \
+ $(k_bin)/kompile -O3 --non-strict --backend ocaml \
+ --directory $(imp_ocaml_dir) -I $(imp_ocaml_dir) \
+ --main-module IMP --syntax-module IMP $<
-$(imp_dir)/krun/imp-kompiled/interpreter: $(imp_krun_files)
+$(imp_java_kompiled): $(imp_java_defn)
@echo "== kompile: $@"
- eval $$(opam config env) \
- $(kompile) --main-module IMP --backend ocaml \
- --syntax-module IMP $< --directory $(imp_dir)/krun
+ $(k_bin)/kompile --backend java \
+ --directory $(imp_java_dir) -I $(imp_java_dir) \
+ --main-module IMP-ANALYSIS --syntax-module IMP-ANALYSIS $<
-build-fun: build-fun-kcompile build-fun-krun
-build-fun-kcompile: $(fun_dir)/kcompile/kat-fun-kompiled/timestamp
-build-fun-krun: $(fun_dir)/krun/fun-kompiled/interpreter
-
-$(fun_dir)/kcompile/kat-fun-kompiled/timestamp: $(fun_kcompile_files)
+$(fun_ocaml_kompiled): $(fun_ocaml_defn)
@echo "== kompile: $@"
- eval $$(opam config env) \
- $(kompile) --main-module FUN-ANALYSIS --backend java \
- --syntax-module FUN-UNTYPED-SYNTAX $< --directory $(fun_dir)/kcompile
+ eval $$(opam config env) \
+ $(k_bin)/kompile -O3 --non-strict --backend ocaml \
+ --directory $(fun_ocaml_dir) -I $(fun_ocaml_dir) \
+ --main-module FUN-UNTYPED --syntax-module FUN-UNTYPED $<
-$(fun_dir)/krun/fun-kompiled/interpreter: $(fun_krun_files)
+$(fun_java_kompiled): $(fun_java_defn)
@echo "== kompile: $@"
- eval $$(opam config env) \
- $(kompile) --main-module FUN-UNTYPED --backend ocaml \
- --syntax-module FUN-UNTYPED-SYNTAX $< --directory $(fun_dir)/krun
+ $(k_bin)/kompile --backend java \
+ --directory $(fun_java_dir) -I $(fun_java_dir) \
+ --main-module FUN-ANALYSIS --syntax-module FUN-ANALYSIS $<
# Testing
# -------
+test_dir:=tests
test_imp_files:=$(wildcard $(test_dir)/imp/*.strat)
test_fun_files:=$(wildcard $(test_dir)/fun/*.strat)
diff --git a/fun.md b/fun.md
index 02dd748..56127e5 100644
--- a/fun.md
+++ b/fun.md
@@ -23,16 +23,6 @@ To make it more interesting and to highlight some of K's strengths, FUN includes
- Functions declared in `let`/`letrec` binders and declared anonymously can take multiple space-separated arguments.
In addition, functions can be partially applied to arguments, allowing the function to be evaluated incrementally.
- For example, the following is the reduction sequence of a partially applied anonymous function:
-
- ```
- (fun x y -> x) 3
- => closure(.Map, x y -> x, .Bindings, .List ) 3
- => closure(.Map, y -> x, x = 3 and .Bindings, ListItem(3))
- ```
-
- with store location `L` pointing at the value `3`.
-
- Functions can be defined using pattern matching over the available data-types.
For example, the program
@@ -46,6 +36,8 @@ To make it more interesting and to highlight some of K's strengths, FUN includes
defines a function `max` that calculates the maximum element of a non-empty list, and the function
```
+ datatype ('a,'b) pair = Pair 'a 'b
+
letrec ack = fun (Pair 0 n) -> n + 1
| (Pair m 0) -> ack (Pair (m - 1) 1)
| (Pair m n) -> ack (Pair (m - 1) (ack (Pair m (n - 1))))
@@ -104,14 +96,6 @@ Two special names `$x` and `$k` are used in the semantics for desugaring builtin
// -------------------------------
```
-### Symbolic Integers
-
-```kcompile
- syntax Int ::= "symbolicInt" [function]
- // ---------------------------------------
- rule symbolicInt => ?V:Int
-```
-
### Values
Expression constructs will be defined throughtout the syntax module.
@@ -439,11 +423,11 @@ Expressions
rule V1:Val == V2:Val => V1 ==K V2 ...
rule V1:Val != V2:Val => V1 =/=K V2 ...
- rule ! T => notBool(T) ...
- rule true && E => E ...
- rule false && _ => false ...
- rule true || _ => true ...
- rule false || E => E ...
+ rule ! T:Bool => notBool(T) ...
+ rule true && E => E ...
+ rule false && _ => false ...
+ rule true || _ => true ...
+ rule false || E => E ...
```
Lists must be handled carefully, because not every `ClosureVal` should be considered fully evaluated.
@@ -460,10 +444,10 @@ Lists must be handled carefully, because not every `ClosureVal` should be consid
rule E : ES => E ~> #consTail ES ...
requires notBool areFullyEvaluated(E : ES)
- rule V ~> #consTail ES => ES ~> #consHead V ...
+ rule V:Val ~> #consTail ES => ES ~> #consHead V ...
requires isFullyEvaluated(V)
- rule VS ~> #consHead V => V : VS ...
+ rule VS:Vals ~> #consHead V => V : VS ...
requires areFullyEvaluated(VS)
```
diff --git a/imp.md b/imp.md
index c1c109d..487ef3c 100644
--- a/imp.md
+++ b/imp.md
@@ -31,8 +31,8 @@ module IMP
### Symbolic Integers
```kcompile
- syntax Int ::= "symbolicInt" [function]
- // ---------------------------------------
+ syntax Int ::= "symbolicInt" [function, impure]
+ // -----------------------------------------------
rule symbolicInt => ?V:Int
```
@@ -51,11 +51,11 @@ IMP has `AExp` for arithmetic expressions (over integers).
| AExp "+" AExp [left, seqstrict]
| "(" AExp ")" [bracket]
// ---------------------------------------
- rule I1 + I2 => I1 +Int I2
- rule I1 - I2 => I1 -Int I2
- rule I1 * I2 => I1 *Int I2
- rule I / 0 => div-zero-error [tag(divzero)]
- rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0 [tag(divnonzero)]
+ rule I1 + I2 => I1 +Int I2 ...
+ rule I1 - I2 => I1 -Int I2 ...
+ rule I1 * I2 => I1 *Int I2 ...
+ rule I / 0 => div-zero-error ... [tag(divzero)]
+ rule I1 / I2 => I1 /Int I2 ... requires I2 =/=Int 0 [tag(divnonzero)]
```
IMP has `BExp` for boolean expressions.
@@ -69,12 +69,12 @@ IMP has `BExp` for boolean expressions.
> BExp "&&" BExp [left, strict(1)]
| "(" BExp ")" [bracket]
// ----------------------------------------
- rule I1 <= I2 => I1 <=Int I2
- rule I1 < I2 => I1 I1 ==Int I2
- rule ! T => notBool T
- rule true && B => B
- rule false && _ => false
+ rule I1 <= I2 => I1 <=Int I2 ...
+ rule I1 < I2 => I1
+ rule I1 == I2 => I1 ==Int I2 ...
+ rule ! T:Bool => notBool T ...
+ rule true && B => B ...
+ rule false && _ => false ...
```
IMP has `{_}` for creating blocks of statements.
@@ -82,8 +82,8 @@ IMP has `{_}` for creating blocks of statements.
```k
syntax Block ::= "{" "}" | "{" Stmt "}"
// ---------------------------------------
- rule { } => .
- rule { S } => S
+ rule { } => . ...
+ rule { S } => S ...
```
IMP has `int_;` for declaring variables and `_=_;` for assignment.
@@ -92,7 +92,7 @@ IMP has `int_;` for declaring variables and `_=_;` for assignment.
syntax Ids ::= List{Id,","}
syntax Stmt ::= Block | "int" Ids ";"
// -------------------------------------
- rule int .Ids ; => .
+ rule int .Ids ; => . ...
rule int (X, XS => XS) ; ...
MEM => MEM [ X <- 0 ]
@@ -116,7 +116,7 @@ IMP has `if(_)_else_` for choice, `while(_)_` for looping, and `__` for sequenci
syntax Stmt ::= Stmt Stmt [left]
// --------------------------------
- rule S1:Stmt S2:Stmt => S1 ~> S2
+ rule S1:Stmt S2:Stmt => S1 ~> S2 ...
syntax priority int_;_IMP _=_;_IMP if(_)_else__IMP while(_)__IMP > ___IMP
endmodule
diff --git a/kat b/kat
index daf630b..e681aef 100755
--- a/kat
+++ b/kat
@@ -1,10 +1,24 @@
#!/usr/bin/env bash
-set -e # Exit immediately if any command fails
+set -euo pipefail
+shopt -s extglob
+
+kat_script="$0"
+while [[ -h "$kat_script" ]]; do
+ kat_dir="$(cd -P "$(dirname "$kat_script")" && pwd)"
+ kat_script="$(readlink "$kat_script")"
+ [[ "$kat_script" != /* ]] && kat_script="$kat_dir/$kat_script"
+done
+kat_dir="$(cd -P "$(dirname "$kat_script")" && pwd)"
+
+build_dir="$kat_dir/.build"
+release_dir="$build_dir/k/k-distribution/target/release/k"
+defn_dir="$build_dir/defn"
+
+export PATH="$release_dir/lib/native/linux:$release_dir/lib/native/linux64:$release_dir/bin/:$PATH"
-build_dir="$(pwd)/.build"
test_logs="$build_dir/logs"
-failing_log="$test_logs/failing.lastrun"
+test_log="$test_logs/tests.log"
mkdir -p "$test_logs"
# Utilities
@@ -18,16 +32,15 @@ warn() { progress "[WARNING] $@" ; }
# -----------------
run_env() {
- local run_type release_dir
- run_type="$1" ; shift
- run_file="$1" ; shift
- release_dir="$build_dir/k/k-distribution/target/release/k"
- export PATH="$release_dir/lib/native/linux:$release_dir/lib/native/linux64:$release_dir/bin/:$PATH"
- eval $(opam config env)
+ local run_backend run_file
+ run_backend="$1" ; shift
+ run_file="$1" ; shift
+ [[ "$run_backend" != 'ocaml' ]] || eval $(opam config env)
+ [[ -f "$run_file" ]] || die "File does not exist: '$run_file'"
case "$run_file" in
- *.imp) DEFN_DIRECTORY="$build_dir/defn/imp/$run_type" ;;
- *.fun) DEFN_DIRECTORY="$build_dir/defn/fun/$run_type" ;;
- *) die "Do not know definition to run with: '$run_file'" ;;
+ *.imp) DEFN_DIRECTORY="$build_dir/defn/imp/$run_backend" ;;
+ *.fun) DEFN_DIRECTORY="$build_dir/defn/fun/$run_backend" ;;
+ *) die "Do not know definition to run with: '$run_file'" ;;
esac
}
@@ -38,14 +51,14 @@ run_krun() {
local run_file strategy
run_file="$1" ; shift
strategy="$1" ; shift
- run_env kcompile "$run_file"
+ run_env java "$run_file"
export K_OPTS=-Xss500m
krun --directory "$DEFN_DIRECTORY" -cSTRATEGY="$strategy" "$run_file" "$@"
}
run_krun_orig() {
local run_file="$1" ; shift
- run_env krun "$run_file"
+ run_env ocaml "$run_file"
export K_OPTS=-Xss500m
krun --directory "$DEFN_DIRECTORY" "$run_file" "$@"
}
@@ -61,23 +74,32 @@ run_program() {
fi
}
-run_kdebug() {
- local run_file strategy
- run_file="$1" ; shift
- strategy="$1" ; shift
- run_krun "$run_file" "$strategy" --debugger "$@"
-}
+run_klab() {
+ local run_file run_strategy
-run_ksearch() {
- local run_file strategy
- run_file="$1" ; shift
- strategy="$1" ; shift
- run_krun "$run_file" "$strategy" --search "$@"
+ run_file="$1" ; shift
+ run_strategy="$1" ; shift
+
+ rm -rf '/tmp/klab'
+
+ $0 run $run_file "$run_strategy" \
+ --state-log --state-log-path /tmp/klab --state-log-id wasmtest \
+ --state-log-events OPEN,EXECINIT,SEARCHINIT,REACHINIT,REACHTARGET,REACHPROVED,NODE,RULE,SRULE,RULEATTEMPT,IMPLICATION,Z3QUERY,Z3RESULT,CLOSE \
+ --output json \
+ --output-tokenize ' ' \
+ --debug \
+ --no-sort-collections \
+ --restore-original-names \
+ --no-alpha-renaming \
+ >/dev/null
+
+ progress 'Run `TMPDIR=/tmp KLAB_EVMS_PATH=foo klab debugg wasmtest` to explore execution trace.'
}
run_test() {
local test_name test_ext test_file test_strat test_out test_expected
local exec_strategy exit_status
+
test_name="$1" ; shift
exit_status='0'
@@ -116,40 +138,29 @@ run_test() {
# Main
# ----
-cd "$(dirname $0)"
-
# main functionality
run_command="$1" ; shift
case "$run_command" in
# Running
- run) run_program "$@" ;;
- debug) run_kdebug "$@" ;;
- search) run_ksearch "$@" ;;
+ run) run_program "$@" ;;
+ klab-run) run_klab "$@" ;;
# Testing
test) run_test "$@" ;;
*) echo "
- usage: $0 [run|debug|search] *
+ usage: $0 run *
+ $0 test
# Running
# -------
- $0 run Run a single program using given strategy
- $0 debug Run a single program using given strategy in the debugger
- $0 search Search a single program's executions using given strategy
+ $0 run: Run a single program using given strategy
+ $0 test: Test that running a program with given strategies produces the correct output.
Note: is a path to a file containing a program (languages supported: IMP, FUN).
is a term in sort STRATEGY.
If `STRATEGY == orig`, then it runs with the *original* semantics under the OCaml backend.
-
- # Testing
- # -------
- $0 test Test that running with `run-orig` produces the correct hash.
-
- Note: is the path to the program in `tests/`
- is the expected md5sum of the output
-
- Note: This command is more for devs and CI servers.
+ name of a test in `tests/imp` or `tests/fun` without extension, eg. `tests/imp/collatz`.
" ; exit ;;
esac
diff --git a/kat-imp.md b/kat-imp.md
index 1decf8a..2d4fda2 100644
--- a/kat-imp.md
+++ b/kat-imp.md
@@ -37,7 +37,7 @@ Here the definition of a `State` for IMP is given, as well as the definitions of
### Define `#branch` and `#normal`
```k
- rule #normal => ^ lookup | ^ assignment
+ rule #normal => ^ regular | ^ lookup | ^ assignment
rule #branch => ^ iftrue | ^ iffalse | ^ divzero | ^ divnonzero
rule #loop => ^ whileIMP
```
diff --git a/kat.md b/kat.md
index d296d1c..2ddff09 100644
--- a/kat.md
+++ b/kat.md
@@ -100,7 +100,7 @@ Here, a wrapper around this functionality is provided which will try to execute
rule #STUCK() ~> (S:Strategy => .) ...
rule #STUCK() ~> #try => pop ~> #false ...
- rule SA:StrategyApplied => . ...
+ rule #appliedRule(_) => . ...
syntax Pred ::= "can?" Strategy
// -------------------------------
@@ -397,8 +397,8 @@ Things added to the sort `StateOp` will automatically load the current state for
```k
syntax Strategy ::= "exec" | "trace"
// ------------------------------------
- rule exec => step * ...
- rule trace => (step ; push) * ...
+ rule exec => step * ...
+ rule trace => (step ; push) * ; push ...
syntax Pred ::= "eval"
// ----------------------
@@ -414,7 +414,7 @@ Things added to the sort `StateOp` will automatically load the current state for
syntax Strategy ::= "exec-to-branch" | "#exec-to-branch"
// --------------------------------------------------------
rule exec-to-branch
- => (#normal | #loop | ^ regular) *
+ => (#normal | #loop) *
~> which-can? #branch
~> #exec-to-branch
...
@@ -603,7 +603,7 @@ The interface of this analysis requires you define when to abstract and how to a
Finally, semantics based compilation is provided as a macro.
- `compile-step` will generate the rule associated to the state at the top of the `states` stack.
- **Note**: Here we assume `#loop`, `#branch`, and `#normal | ^ regular` are disjoint strategies.
+ **Note**: Here we assume `#loop`, `#branch`, and `#normal` are disjoint strategies.
```k
syntax Strategy ::= "compile-step"
@@ -619,8 +619,8 @@ Finally, semantics based compilation is provided as a macro.
else if try-state? STATE < #branch >
then ( split-rules STATE #branch
)
- else if try-state? STATE < ^ regular | #normal >
- then ( push STATE < (^ regular | #normal) * > )
+ else if try-state? STATE < #normal >
+ then ( push STATE < #normal * > )
else ( mk-rule STATE )
...
diff --git a/tangle b/tangle
deleted file mode 100755
index 748a7b7..0000000
--- a/tangle
+++ /dev/null
@@ -1,122 +0,0 @@
-#!/usr/bin/env zsh
-
-return='0'
-
-tests=( # straight-line-1-bimc1 straight-line-1-bimc2
- # straight-line-2-bimc1 straight-line-2-bimc2 straight-line-2-bimc3
- inf-div-bad-bimc inf-div-good-bimc
- # sum-bimc1 sum-bimc2 sum-bimc3
- # collatz-bimc collatz-all-bimc
- # krazy-loop-correct-bimc krazy-loop-incorrect-bimc1 krazy-loop-incorrect-bimc2
- # straight-line-1-sbc straight-line-2-sbc
- # dead-if-sbc
- # sum-sbc sum-plus-sbc
- # collatz-sbc collatz-all-sbc
- # krazy-loop-incorrect-sbc krazy-loop-correct-sbc
- )
-
-compiled_programs=( collatz collatz-all
- krazy-loop-incorrect krazy-loop-correct
- )
-
-gecho() {
- echo -e '\e[32m'$@'\e[39m'
-}
-
-recho() {
- echo -e '\e[31m'$@'\e[39m'
-}
-
-h1() {
- header="$1"
- echo
- echo "$header"
- echo "$(echo "$header" | sed -n 's/./=/gp')"
- echo
-}
-
-h2() {
- header="$1"
- echo "$header"
- echo "$(echo "$header" | sed -n 's/./-/gp')"
-}
-
-h3() {
- header="$1"
- echo "### $header"
-}
-
-tangle_gen() {
-
- h2 "generating tests ..."
- # ----------------------
- [[ ! -d tests/output ]] && mkdir -p tests/output
- pandoc-tangle --from markdown --to code-sh --code test KAT-IMP-examples.md > tests/test.sh
- for test in $tests; do
- pandoc-tangle --from markdown --to code-k --code "$test" KAT-IMP-examples.md > "tests/output/$test.out"
- done
-
- h2 "generating sbc-ed programs and benchmarks ..."
- # -----------------------------------------------
- for program in $compiled_programs; do
- [[ ! -d "tests/$program-compiled" ]] && mkdir -p "tests/$program-compiled"
- pandoc-tangle --from markdown --to code-k --code "$program-compiled" KAT-IMP-examples.md > "tests/$program-compiled/$program.k"
- pandoc-tangle --from markdown --to code-sh --code "benchmark-$program" KAT-IMP-examples.md > "tests/benchmark-$program.sh"
- done
-}
-
-tangle_tests() {
-
- for test in $tests; do
- h2 "running '$test' ..."
- # ---------------------
- bash tests/test.sh $test
- if [[ "$?" == '0' ]]; then
- gecho "SUCCESS"
- else
- recho "FAILURE"
- fi
- done
-}
-
-tangle_benchmarks() {
-
- for program in $compiled_programs; do
-
- h2 "running benchmarks for '$program' ..."
- # ---------------------------------------
- PROGRAM="$(echo "$program" | awk '{print toupper($0)}')"
-
- h3 "kompiling '$PROGRAM-COMPILED' ..."
- ###
- pushd "tests/$program-compiled"
- kompile --debug --main-module "$PROGRAM-COMPILED" --syntax-module "$PROGRAM-COMPILED" "$program.k" || exit 1
- popd
-
- h3 "running benchmarks for '$program' ..."
- ###
- pushd tests
- bash "benchmark-$program.sh"
- popd
- done
-}
-
-[[ "$#" == '0' ]] && set all
-
-while [[ "$#" -gt '0' ]]; do
- tangle_command="$1" && shift
-
- h1 "attempting tangle command '$tangle_command' ..."
- # =================================================
-
- case "$tangle_command" in
- all) set gen kompile examples test bench ;;
- gen) tangle_gen ;;
- examples) tangle_examples ;;
- test) tangle_tests ;;
- bench) tangle_benchmarks ;;
- *) echo "Unrecognized option: '$tangle_command' ..." ;;
- esac
-done
-
-exit "$return"
diff --git a/tests/imp/collatz-all-upto.expected b/tests/imp/collatz-all-upto.expected
index b31acf0..102ba0a 100644
--- a/tests/imp/collatz-all-upto.expected
+++ b/tests/imp/collatz-all-upto.expected
@@ -106,7 +106,7 @@ Strategy: compile
requires 2 <=Int V14 ==K true
#And
- V14 <=Int V14 /Int 2 *Int 2 ==K false > , <
+ ( V14 <=Int V14 /Int 2 *Int 2 ) ==K false > , <
while ( 2 <= n ) { if ( n <= ( n / 2 ) * 2 ) { n = n / 2 ; } else { n = 3 * n + 1 ; } x = x + 1 ; } ~> c = c + 1 ; ~> while ( c <= b ) { n = c ; while ( 2 <= n ) { if ( n <= ( n / 2 ) * 2 ) { n = n / 2 ; } else { n = 3 * n + 1 ; } x = x + 1 ; } c = c + 1 ; }
diff --git a/tests/imp/collatz-all.expected b/tests/imp/collatz-all.expected
index 556ae99..6f0f9fc 100644
--- a/tests/imp/collatz-all.expected
+++ b/tests/imp/collatz-all.expected
@@ -1,9 +1,9 @@
-Strategy: step-with skip ; step 3 ; bimc 5000 (bexp? n <= 1000)
+Strategy: step 3 ; bimc 5000 (bexp? n <= 1000)
================================================================================
- #STUCK ( ) ~> #bimc-result #true in 891 steps ~> ^ regular *
+ #STUCK ( ) ~> #bimc-result #true in 891 steps
diff --git a/tests/imp/collatz-all.strat b/tests/imp/collatz-all.strat
index 7ac85f9..d39cc61 100644
--- a/tests/imp/collatz-all.strat
+++ b/tests/imp/collatz-all.strat
@@ -1,2 +1,2 @@
-step-with skip ; step 3 ; bimc 5000 (bexp? n <= 1000)
+step 3 ; bimc 5000 (bexp? n <= 1000)
compile
diff --git a/tests/imp/collatz.expected b/tests/imp/collatz.expected
index 47bb28d..2c99b09 100644
--- a/tests/imp/collatz.expected
+++ b/tests/imp/collatz.expected
@@ -1,5 +1,5 @@
-Strategy: step-with skip ; step 2 ; bimc 5000 (bexp? n <= 1000)
+Strategy: step 2 ; bimc 5000 (bexp? n <= 1000)
================================================================================
@@ -194,11 +194,11 @@ Strategy: step-with skip ; step 2 ; bimc 5000 (bexp? n <= 1000)
-Strategy: step-with skip ; step 2 ; bimc 20 (bexp? n <= 1000)
+Strategy: step 2 ; bimc 20 (bexp? n <= 1000)
================================================================================
- #STUCK ( ) ~> #bimc-result #true in 20 steps ~> ^ regular *
+ #STUCK ( ) ~> #bimc-result #true in 20 steps
diff --git a/tests/imp/collatz.strat b/tests/imp/collatz.strat
index 8e51354..245f397 100644
--- a/tests/imp/collatz.strat
+++ b/tests/imp/collatz.strat
@@ -1,2 +1,2 @@
-step-with skip ; step 2 ; bimc 5000 (bexp? n <= 1000)
-step-with skip ; step 2 ; bimc 20 (bexp? n <= 1000)
+step 2 ; bimc 5000 (bexp? n <= 1000)
+step 2 ; bimc 20 (bexp? n <= 1000)
diff --git a/tests/imp/div-zero.expected b/tests/imp/div-zero.expected
index 846c121..3774a09 100644
--- a/tests/imp/div-zero.expected
+++ b/tests/imp/div-zero.expected
@@ -49,7 +49,7 @@ Strategy: compile
x |-> V0
y |-> 7 /Int V0
- requires V0 ==K 0 ==K false > , <
+ requires V0 ==Int 0 ==K false > , <
int x , y , .Ids ; x = 0 ; y = V2 ; y = 7 / x ;
diff --git a/tests/imp/if-div-zero.expected b/tests/imp/if-div-zero.expected
index 0a0ad4d..4a2cfa4 100644
--- a/tests/imp/if-div-zero.expected
+++ b/tests/imp/if-div-zero.expected
@@ -78,7 +78,7 @@ Strategy: compile
requires 7 /Int V0 <=Int 3 ==K false
#And
- V0 ==K 0 ==K false > , <
+ ( V0 ==Int 0 ) ==K false > , <
int x , y , .Ids ; y = 7 ; x = V1 ; if ( y / x <= 3 ) { x = 1 ; } else { x = -1 ; }
@@ -95,7 +95,7 @@ Strategy: compile
requires 7 /Int V1 <=Int 3 ==K true
#And
- V1 ==K 0 ==K false > , <
+ V1 ==Int 0 ==K false > , <
int x , y , .Ids ; y = 7 ; x = 0 ; if ( y / x <= 3 ) { x = 1 ; } else { x = -1 ; }
diff --git a/tests/imp/inf-div-bad.expected b/tests/imp/inf-div-bad.expected
index 385b016..461198b 100644
--- a/tests/imp/inf-div-bad.expected
+++ b/tests/imp/inf-div-bad.expected
@@ -2454,7 +2454,7 @@ Strategy: compile
requires 0 <=Int V3 ==K true
#And
- V3 ==K 0 ==K false > , <
+ V3 ==Int 0 ==K false > , <
while ( 0 <= x ) { y = y / x ; x = x - 1 ; }
diff --git a/tests/imp/inf-div-unknown-fixed.expected b/tests/imp/inf-div-unknown-fixed.expected
index d760d94..eadd8c9 100644
--- a/tests/imp/inf-div-unknown-fixed.expected
+++ b/tests/imp/inf-div-unknown-fixed.expected
@@ -74,7 +74,7 @@ Strategy: compile
requires 0 <=Int V6 ==K true
#And
- 0
+ ( 0
.States
diff --git a/tests/imp/inf-div-unknown.expected b/tests/imp/inf-div-unknown.expected
index 6390a88..5c23620 100644
--- a/tests/imp/inf-div-unknown.expected
+++ b/tests/imp/inf-div-unknown.expected
@@ -56,7 +56,7 @@ Strategy: compile
requires 0 <=Int V4 ==K true
#And
- V4 ==K 0 ==K false > , <
+ V4 ==Int 0 ==K false > , <
while ( 0 <= x ) { y = y / x ; x = x - 1 ; }
diff --git a/tests/imp/krazy-loop-correct.expected b/tests/imp/krazy-loop-correct.expected
index d4c1b1d..0094fed 100644
--- a/tests/imp/krazy-loop-correct.expected
+++ b/tests/imp/krazy-loop-correct.expected
@@ -1,5 +1,5 @@
-Strategy: step-with skip ; step 6 ; bimc 5000 (not can? (^ divzero))
+Strategy: step 6 ; bimc 5000 (not can? (^ divzero))
================================================================================
diff --git a/tests/imp/krazy-loop-correct.strat b/tests/imp/krazy-loop-correct.strat
index defb62c..1d27842 100644
--- a/tests/imp/krazy-loop-correct.strat
+++ b/tests/imp/krazy-loop-correct.strat
@@ -1 +1 @@
-step-with skip ; step 6 ; bimc 5000 (not can? (^ divzero))
+step 6 ; bimc 5000 (not can? (^ divzero))
diff --git a/tests/imp/krazy-loop-incorrect.expected b/tests/imp/krazy-loop-incorrect.expected
index 52a3240..86f6878 100644
--- a/tests/imp/krazy-loop-incorrect.expected
+++ b/tests/imp/krazy-loop-incorrect.expected
@@ -1,5 +1,5 @@
-Strategy: step-with skip ; step 6 ; bimc 5000 (not can? (^ divzero))
+Strategy: step 6 ; bimc 5000 (not can? (^ divzero))
================================================================================
@@ -33942,7 +33942,7 @@ Strategy: step-with skip ; step 6 ; bimc 5000 (not can? (^ divzero))
-Strategy: step-with skip ; step 6 ; bimc 2825 (not can? (^ divzero))
+Strategy: step 6 ; bimc 2825 (not can? (^ divzero))
================================================================================
diff --git a/tests/imp/krazy-loop-incorrect.strat b/tests/imp/krazy-loop-incorrect.strat
index aa6fb02..d6d37a4 100644
--- a/tests/imp/krazy-loop-incorrect.strat
+++ b/tests/imp/krazy-loop-incorrect.strat
@@ -1,2 +1,2 @@
-step-with skip ; step 6 ; bimc 5000 (not can? (^ divzero))
-step-with skip ; step 6 ; bimc 2825 (not can? (^ divzero))
+step 6 ; bimc 5000 (not can? (^ divzero))
+step 6 ; bimc 2825 (not can? (^ divzero))
diff --git a/tests/imp/straight-line-1.expected b/tests/imp/straight-line-1.expected
index fbb4ca2..58d566e 100644
--- a/tests/imp/straight-line-1.expected
+++ b/tests/imp/straight-line-1.expected
@@ -1,5 +1,5 @@
-Strategy: step-with skip ; step ; bimc 1 (bexp? x <= 7)
+Strategy: step ; bimc 1 (bexp? x <= 7)
================================================================================
@@ -32,7 +32,7 @@ Strategy: step-with skip ; step ; bimc 1 (bexp? x <= 7)
-Strategy: step-with skip ; step ; bimc 2 (bexp? x <= 7)
+Strategy: step ; bimc 2 (bexp? x <= 7)
================================================================================
diff --git a/tests/imp/straight-line-1.strat b/tests/imp/straight-line-1.strat
index 48523e0..0e05d6f 100644
--- a/tests/imp/straight-line-1.strat
+++ b/tests/imp/straight-line-1.strat
@@ -1,2 +1,2 @@
-step-with skip ; step ; bimc 1 (bexp? x <= 7)
-step-with skip ; step ; bimc 2 (bexp? x <= 7)
+step ; bimc 1 (bexp? x <= 7)
+step ; bimc 2 (bexp? x <= 7)
diff --git a/tests/imp/straight-line-2.expected b/tests/imp/straight-line-2.expected
index 0704437..fb73a24 100644
--- a/tests/imp/straight-line-2.expected
+++ b/tests/imp/straight-line-2.expected
@@ -1,5 +1,5 @@
-Strategy: step-with skip ; step ; bimc 1 (bexp? x <= 7)
+Strategy: step ; bimc 1 (bexp? x <= 7)
================================================================================
@@ -32,7 +32,7 @@ Strategy: step-with skip ; step ; bimc 1 (bexp? x <= 7)
-Strategy: step-with skip ; step ; bimc 2 (bexp? x <= 7)
+Strategy: step ; bimc 2 (bexp? x <= 7)
================================================================================
@@ -72,7 +72,7 @@ Strategy: step-with skip ; step ; bimc 2 (bexp? x <= 7)
-Strategy: step-with skip ; step ; bimc 500 (bexp? x <= 7)
+Strategy: step ; bimc 500 (bexp? x <= 7)
================================================================================
diff --git a/tests/imp/straight-line-2.strat b/tests/imp/straight-line-2.strat
index 2751bbc..3412980 100644
--- a/tests/imp/straight-line-2.strat
+++ b/tests/imp/straight-line-2.strat
@@ -1,3 +1,3 @@
-step-with skip ; step ; bimc 1 (bexp? x <= 7)
-step-with skip ; step ; bimc 2 (bexp? x <= 7)
-step-with skip ; step ; bimc 500 (bexp? x <= 7)
+step ; bimc 1 (bexp? x <= 7)
+step ; bimc 2 (bexp? x <= 7)
+step ; bimc 500 (bexp? x <= 7)
diff --git a/tests/imp/sum.expected b/tests/imp/sum.expected
index 1ed8803..e366aaf 100644
--- a/tests/imp/sum.expected
+++ b/tests/imp/sum.expected
@@ -1,5 +1,5 @@
-Strategy: step-with skip ; step ; bimc 500 (bexp? s <= 32)
+Strategy: step ; bimc 500 (bexp? s <= 32)
================================================================================
@@ -274,7 +274,7 @@ Strategy: step-with skip ; step ; bimc 500 (bexp? s <= 32)
-Strategy: step-with skip ; step ; bimc 31 (bexp? s <= 32)
+Strategy: step ; bimc 31 (bexp? s <= 32)
================================================================================
@@ -549,7 +549,7 @@ Strategy: step-with skip ; step ; bimc 31 (bexp? s <= 32)
-Strategy: step-with skip ; step ; bimc 30 (bexp? s <= 32)
+Strategy: step ; bimc 30 (bexp? s <= 32)
================================================================================
diff --git a/tests/imp/sum.strat b/tests/imp/sum.strat
index 76b44f3..b1f3629 100644
--- a/tests/imp/sum.strat
+++ b/tests/imp/sum.strat
@@ -1,5 +1,5 @@
-step-with skip ; step ; bimc 500 (bexp? s <= 32)
-step-with skip ; step ; bimc 31 (bexp? s <= 32)
-step-with skip ; step ; bimc 30 (bexp? s <= 32)
+step ; bimc 500 (bexp? s <= 32)
+step ; bimc 31 (bexp? s <= 32)
+step ; bimc 30 (bexp? s <= 32)
exec-to-branch
compile