From 0a330a73dd2dadb9fe314bd964d5f1c182a4e102 Mon Sep 17 00:00:00 2001
From: gtrepta <50716988+gtrepta@users.noreply.github.com>
Date: Wed, 10 Jul 2024 10:26:05 -0500
Subject: [PATCH] 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 <devops@runtimeverification.com>
---
 Makefile                                |  2 +-
 package/version                         |  2 +-
 pykwasm/pyproject.toml                  |  2 +-
 pykwasm/src/pykwasm/scripts/kwasm.py    | 23 ++++++++++++++++++++---
 tests/conformance/look_for_supported.sh |  0
 tests/conformance/unparseable.txt       |  8 +-------
 tests/conformance/unsupported-llvm.txt  |  3 ++-
 7 files changed, 26 insertions(+), 14 deletions(-)
 mode change 100644 => 100755 tests/conformance/look_for_supported.sh

diff --git a/Makefile b/Makefile
index 9af5e1eb9..3a5ad4abf 100644
--- 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
index b9dbcf613..8c1c54a74 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.79
+0.1.80
diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml
index f30fc4b60..84a2da298 100644
--- 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. <contact@runtimeverification.com>",
diff --git a/pykwasm/src/pykwasm/scripts/kwasm.py b/pykwasm/src/pykwasm/scripts/kwasm.py
index 03e517b81..05fd03ccd 100644
--- 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
old mode 100644
new mode 100755
diff --git a/tests/conformance/unparseable.txt b/tests/conformance/unparseable.txt
index 9328bfbf6..21fe12db2 100644
--- 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
index 418a8b554..96a2b0498 100644
--- 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