diff --git a/.gitignore b/.gitignore index ae615fb12..1b80e3c5f 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,4 @@ -/.build/* +/.kwasm-logs/ /tests/*/*-out *.pdf diff --git a/Makefile b/Makefile index d1b4a3296..f271ba0b6 100644 --- a/Makefile +++ b/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 diff --git a/convert.py b/convert.py deleted file mode 100644 index bfebd0f0b..000000000 --- a/convert.py +++ /dev/null @@ -1,39 +0,0 @@ -# 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: python convert.py f32.wast - -import re -import sys - - -def hex2float(h): - 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(): - 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() diff --git a/package/version b/package/version index db7a48047..28d007539 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.31 +0.1.32 diff --git a/preprocessor.py b/preprocessor.py deleted file mode 100644 index d75820fce..000000000 --- a/preprocessor.py +++ /dev/null @@ -1,39 +0,0 @@ -# Preprocessor that converts Wasm concrete syntax into a form parseable by K. -# example usage: python convert.py f32.wast - -import re -import sys - - -def hex2float(h): - 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 as e: - return h - else: - return h - - -def main(): - if len(list(sys.argv)) == 1: - infile = sys.stdin - else: - infile = open(sys.argv[1]) - for line in (infile.readlines()): - sys.stdout.write(re.sub(r"(?:(?:f32|f64)\.const )([^\)]+)", - lambda m: hex2float(m.group()), - line)) - infile.close() - - -if __name__ == "__main__": - main() diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml index aef85e14e..d92bb017c 100644 --- a/pykwasm/pyproject.toml +++ b/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. ", ] +[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" diff --git a/pykwasm/src/pykwasm/scripts/__init__.py b/pykwasm/src/pykwasm/scripts/__init__.py new file mode 100644 index 000000000..e69de29bb diff --git a/pykwasm/src/pykwasm/scripts/convert.py b/pykwasm/src/pykwasm/scripts/convert.py new file mode 100644 index 000000000..d3c6157d3 --- /dev/null +++ b/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() diff --git a/pykwasm/src/pykwasm/scripts/kwasm.py b/pykwasm/src/pykwasm/scripts/kwasm.py new file mode 100644 index 000000000..5defa2e3c --- /dev/null +++ b/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() diff --git a/kwasm b/pykwasm/src/pykwasm/scripts/kwasm.sh old mode 100755 new mode 100644 similarity index 80% rename from kwasm rename to pykwasm/src/pykwasm/scripts/kwasm.sh index 89b499801..a00640df9 --- a/kwasm +++ b/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 diff --git a/pykwasm/src/pykwasm/scripts/preprocessor.py b/pykwasm/src/pykwasm/scripts/preprocessor.py new file mode 100644 index 000000000..0080d5eef --- /dev/null +++ b/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()