Distribute scripts with pykwasm (#609)

* Fix typo

* Add module `scripts`

* Move `convert.py` into Python package

* Move `preprocessor.py` into Python package

* Move `kwasm` into Python package

* Set Version: 0.1.30

* Set Version: 0.1.31

* Set Version: 0.1.32

---------

Co-authored-by: devops <[email protected]>

.gitignore

@@ -1,4 +1,4 @@
-/.build/*
+/.kwasm-logs/
 /tests/*/*-out
 
 *.pdf

Makefile

@@ -28,7 +28,7 @@ clean: pykwasm
 # Testing
 # -------
 
-TEST  := ./kwasm
+TEST  := $(POETRY) run -- kwasm
 CHECK := git --no-pager diff --no-index --ignore-all-space -R
 
 TEST_CONCRETE_BACKEND := llvm

package/version

@@ -1 +1 @@
-0.1.31
+0.1.32

pykwasm/pyproject.toml

@@ -4,12 +4,18 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pykwasm"
-version = "0.1.31"
+version = "0.1.32"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
 ]
 
+[tool.poetry.scripts]
+wasm2kast = "pykwasm.wasm2kast:main"
+kwasm = "pykwasm.scripts.kwasm:main"
+kwasm-convert = "pykwasm.scripts.convert:main"
+kwasm-preprocess = "pykwasm.scripts.preprocessor:main"
+
 [tool.poetry.plugins.kdist]
 wasm-semantics = "pykwasm.kdist.plugin"
 
@@ -62,6 +68,3 @@ exclude = [
     'src/wasm/*',
     'src/tests/unit/test_wasm2kast\.py',
 ]
-
-[tool.poetry.scripts]
-wasm2kast = "pykwasm.wasm2kast:main"

pykwasm/src/pykwasm/scripts/convert.py

@@ -0,0 +1,45 @@
+# This script is not used during runtime.
+# It just helps converting some conformances test to a test that we can use by removing unsupported functions and converting hexfloat to normal float.
+# However it does not support multi-line assertions, function definitions, etc.
+# The test files under directory tests/simple/float were generated by this script.
+# example usage: kwasm-convert f32.wast
+
+import re
+import sys
+
+
+def hex2float(h: str) -> str:
+    print(h)
+    if 'nan' in h:
+        return h.replace('nan', 'NaN')
+    elif 'inf' in h:
+        return h.replace('inf', 'Infinity')
+    elif '0x' not in h:
+        return h
+    else:
+        return h.split()[0] + ' ' + '%e' % (float.fromhex(h.split()[1]))
+
+
+def main() -> None:
+    filename = sys.argv[1]
+    infile = 'tests/wasm-tests/test/core/%s' % filename
+    outfile = open('tests/simple/%s-c.%s' % tuple(filename.split('.')), 'w')
+    unsupported = [
+        'nan:',
+        '-nan',
+        'reinterpret',
+        'assert_return_canonical_nan',
+        'assert_return_arithmetic_nan',
+        'assert_invalid',
+        'assert_malformed',
+    ]
+    for line in open(infile).readlines():
+        if any(x in line for x in unsupported):
+            outfile.write(';; ' + line)
+        else:
+            outfile.write(re.sub(r'(?:(?:f32|f64)\.const )([^\)]+)', lambda m: hex2float(m.group()), line))
+    outfile.write('\n#clearConfig\n')
+
+
+if __name__ == '__main__':
+    main()

pykwasm/src/pykwasm/scripts/kwasm.py

@@ -0,0 +1,15 @@
+import sys
+from pathlib import Path
+
+from pyk.utils import run_process
+
+SCRIPT_FILE = Path(__file__).parent / 'kwasm.sh'
+
+
+def main() -> None:
+    proc_res = run_process(['bash', str(SCRIPT_FILE)] + sys.argv[1:], pipe_stdout=False, check=False)
+    sys.exit(proc_res.returncode)
+
+
+if __name__ == '__main__':
+    main()

kwasm → pykwasm/src/pykwasm/scripts/kwasm.sh

@@ -1,29 +1,13 @@
-#!/usr/bin/env bash
-
 set -euo pipefail
 shopt -s extglob
 
 notif() { echo "== $@" >&2 ; }
 fatal() { echo "[FATAL] $@" ; exit 1 ; }
 
-kwasm_dir="${KWASM_DIR:-$(dirname $0)}"
-build_dir="$kwasm_dir/.build"
-kdist_dir="$(poetry -C pykwasm run -- kdist which)"
+kdist_dir="$(kdist which)"
 defn_dir="${KWASM_DEFN_DIR:-$kdist_dir}/wasm-semantics"
-lib_dir="$build_dir/local/lib"
-k_release_dir="${K_RELEASE:-$kwasm_dir/deps/k/k-distribution/target/release/k}"
-if [[ ! -f "${k_release_dir}/bin/kompile" ]]; then
-    if which kompile &> /dev/null; then
-        k_release_dir="$(dirname $(which kompile))/.."
-    else
-        fatal "Cannot find K Installation!"
-    fi
-fi
-
-export PATH="$k_release_dir/lib/native/linux:$k_release_dir/lib/native/linux64:$k_release_dir/bin/:$PATH"
-export LD_LIBRARY_PATH="$k_release_dir/lib/native/linux64:$lib_dir:${LD_LIBRARY_PATH:-}"
 
-test_logs="$build_dir/logs"
+test_logs='.kwasm-logs'
 mkdir -p "$test_logs"
 test_log="$test_logs/tests.log"
 
@@ -33,12 +17,11 @@ export K_OPTS="${K_OPTS:--Xmx16G -Xss512m}"
 # ---------
 
 preprocess() {
-    local this_script_dir tmp_dir tmp_input
-    this_script_dir="$(dirname $0)"
+    local tmp_dir tmp_input
     tmp_dir="$(mktemp -d)"
     tmp_input="$tmp_dir/$(basename $run_file))"
     touch "$tmp_input"
-    python3 "$this_script_dir/preprocessor.py" "$run_file" > "$tmp_input"
+    kwasm-preprocess "$run_file" > "$tmp_input"
     run_file="$tmp_input"
 }
 
@@ -67,7 +50,7 @@ run_prove() {
     ! $repl       || additional_proof_args+=(--debugger)
     ! $bug_report || additional_proof_args+=(--haskell-backend-command "kore-exec --bug-report $bug_report_name")
 
-    kprove --definition "$defn_dir/$def_module" -I "$kwasm_dir" "$run_file" "${additional_proof_args[@]}" "$@"
+    kprove --definition "$defn_dir/$def_module" "$run_file" "${additional_proof_args[@]}" "$@"
 }
 
 # Main

pykwasm/src/pykwasm/scripts/preprocessor.py

@@ -0,0 +1,42 @@
+# Preprocessor that converts Wasm concrete syntax into a form parseable by K.
+# example usage: kwasm-preprocess f32.wast
+
+import re
+import sys
+
+
+def hex2float(h: str) -> str:
+    h = re.sub('_', '', h)
+    if 'nan' in h:
+        # TODO: Keep bit pattern of float, don't turn all of them into simple NaNs.
+        return re.sub('-?nan(:.*$)?', 'NaN', h)
+    elif 'inf' in h:
+        return h.replace('inf', 'Infinity')
+    elif '0x' in h:
+        try:
+            return h.split()[0] + ' ' + '%e' % (float.fromhex(h.split()[1]))
+        except OverflowError:
+            return h
+        except ValueError:
+            return h
+    else:
+        return h
+
+
+def main() -> None:
+    if len(list(sys.argv)) == 1:
+        infile = sys.stdin
+    else:
+        infile = open(sys.argv[1])
+
+    def replace(m: re.Match) -> str:
+        return hex2float(m.group())
+
+    for line in infile.readlines():
+        sys.stdout.write(re.sub(r'(?:(?:f32|f64)\.const )([^\)]+)', replace, line))
+
+    infile.close()
+
+
+if __name__ == '__main__':
+    main()