Try to use the bison parser for kwasm kast (#671)

* Sort failing lists. Add executable bit to script. Remove tokens.wast from unsupported-llvm as it's already in unparseable. * kwasm kast: Try to use the generated bison parser * Update unparseable and unsupported lists * Have the .parse targets in the Makefile output kore, slightly faster. * Set Version: 0.1.78 * Set Version: 0.1.80 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Jul 10, 2024 · 0a330a7 · 0a330a7
1 parent 7726913
commit 0a330a7
Show file tree

Hide file tree

Showing 7 changed files with 26 additions and 14 deletions.
diff --git a/Makefile b/Makefile
@@ -55,7 +55,7 @@ tests/%.run-term: tests/%
 	rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out-term
 
 tests/%.parse: tests/%
-	K_OPTS='-Xmx16G -Xss512m' $(TEST) kast $< kast > $@-out
+	K_OPTS='-Xmx16G -Xss512m' $(TEST) kast --output kore $< > $@-out
 	rm -rf $@-out
 
 tests/%.prove: tests/%

diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.79
+0.1.80
diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pykwasm"
-version = "0.1.79"
+version = "0.1.80"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/pykwasm/src/pykwasm/scripts/kwasm.py b/pykwasm/src/pykwasm/scripts/kwasm.py
@@ -10,9 +10,10 @@
 
 from pyk.cli.utils import dir_path, file_path
 from pyk.kdist import kdist
-from pyk.ktool.kprint import KAstOutput, _kast
+from pyk.ktool.kprint import KAstInput, KAstOutput, _kast
 from pyk.ktool.kprove import _kprove
 from pyk.ktool.krun import _krun
+from pyk.utils import run_process
 
 from .preprocessor import preprocess
 
@@ -51,9 +52,25 @@ def _exec_run(program: Path) -> None:
 
 def _exec_kast(program: Path, output: KAstOutput | None) -> None:
     definition_dir = kdist.get('wasm-semantics.llvm')
+    pgm_parser = definition_dir / 'parser_PGM'
 
-    with _preprocessed(program) as input_file:
-        proc_res = _kast(input_file, definition_dir=definition_dir, output=output, check=False)
+    with _preprocessed(program) as preprocessed_file:
+        input = KAstInput.PROGRAM
+        input_file = preprocessed_file
+
+        if pgm_parser.exists():
+            f = NamedTemporaryFile()
+            proc_res = run_process([str(pgm_parser), str(input_file)], check=False)
+            if proc_res.returncode != 0:
+                _exit_with_output(proc_res)
+            tmp_file = Path(f.name)
+            tmp_file.write_text(proc_res.stdout)
+
+            input = KAstInput.KORE
+            input_file = tmp_file
+
+        if (not pgm_parser.exists()) or output != KAstOutput.KORE:
+            proc_res = _kast(input_file, definition_dir=definition_dir, input=input, output=output, check=False)
 
     _exit_with_output(proc_res)
 

diff --git a/tests/conformance/look_for_supported.sh b/tests/conformance/look_for_supported.sh
diff --git a/tests/conformance/unparseable.txt b/tests/conformance/unparseable.txt
@@ -5,20 +5,14 @@ comments.wast
 conversions.wast
 data.wast
 endianness.wast
-f32_cmp.wast
-f32.wast
-f64_cmp.wast
-f64.wast
 float_exprs.wast
 float_literals.wast
 global.wast
 if.wast
 imports.wast
 loop.wast
+memory.wast
 memory_copy.wast
 memory_init.wast
-memory.wast
 select.wast
-skip-stack-guard-page.wast
-table_copy.wast
 tokens.wast
diff --git a/tests/conformance/unsupported-llvm.txt b/tests/conformance/unsupported-llvm.txt
@@ -2,7 +2,9 @@ address.wast
 align.wast
 call_indirect.wast
 const.wast
+f32.wast
 f32_bitwise.wast
+f64.wast
 f64_bitwise.wast
 fac.wast
 float_memory.wast
@@ -12,5 +14,4 @@ left-to-right.wast
 linking.wast
 memory_redundancy.wast
 memory_trap.wast
-tokens.wast
 traps.wast