Merge branch 'master' into _update-deps/runtimeverification/k

Author: bbyalcinkaya

.github/workflows/test-pr.yml

@@ -15,23 +15,19 @@ jobs:
       - name: 'Check out code'
         uses: actions/checkout@v3
         with:
-          token: ${{ secrets.JENKINS_GITHUB_PAT }}
           # fetch-depth 0 means deep clone the repo
           fetch-depth: 0
           ref: ${{ github.event.pull_request.head.sha }}
-      - name: 'Configure GitHub user'
-        run: |
-          git config user.name devops
-          git config user.email devops@runtimeverification.com
-      - name: 'Update version'
+      - name: 'Check version was bumped'
         run: |
           og_version=$(git show origin/${GITHUB_BASE_REF}:package/version)
           ./package/version.sh bump ${og_version}
           ./package/version.sh sub
-          new_version=$(cat package/version)
-          git add --update && git commit --message "Set Version: ${new_version}" || true
-      - name: 'Push updates'
-        run: git push origin HEAD:${GITHUB_HEAD_REF}
+          if ! git diff --quiet; then
+            echo "::error::Version was not bumped for this PR. Run './package/version.sh bump ${og_version} && ./package/version.sh sub' locally and commit the result."
+            git diff
+            exit 1
+          fi
 
   pykwasm-code-quality-checks:
     name: 'Code Quality Checks'

pykwasm/pyproject.toml

@@ -9,8 +9,7 @@ description = ""
 readme = "README.md"
 requires-python = "~=3.10"
 dependencies = [
-    "kframework>=7.1.337",
-    "py-wasm@git+https://github.com/runtimeverification/py-wasm.git@0.3.1"
+    "kframework>=7.1.337"
 ]
 
 [[project.authors]]

pykwasm/src/pykwasm/binary/__init__.py

@@ -0,0 +1 @@
+from .module import parse_module

pykwasm/src/pykwasm/binary/combinators.py

@@ -0,0 +1,43 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+from .integers import u32
+from .utils import WasmParseError, reset
+
+if TYPE_CHECKING:
+    from .utils import A, InputStream, Parser
+
+
+def sized(p: Parser[A], s: InputStream) -> A:
+    size = u32(s)
+    start_pos = s.tell()
+    res = p(s)
+    end_pos = s.tell()
+    if end_pos - start_pos != size:
+        raise WasmParseError('Size mismatch')
+    return res
+
+
+def parse_n(p: Parser[A], n: int, s: InputStream) -> list[A]:
+    results = []
+    for _ in range(n):
+        x = p(s)
+        results.append(x)
+    return results
+
+
+def list_of(p: Parser[A], s: InputStream) -> list[A]:
+    n = u32(s)
+    return parse_n(p, n, s)
+
+
+def either(ps: list[Parser[A]], s: InputStream) -> A:
+    for p in ps:
+        pos = s.tell()
+        try:
+            return p(s)
+        except WasmParseError:
+            reset(pos, s)
+            continue
+    raise WasmParseError('None of the alternatives succeeded')

pykwasm/src/pykwasm/binary/floats.py

@@ -0,0 +1,21 @@
+from __future__ import annotations
+
+import struct
+from typing import TYPE_CHECKING
+
+from .utils import read_bytes
+
+if TYPE_CHECKING:
+    from .utils import InputStream
+
+
+def f32(s: InputStream) -> float:
+    bs = read_bytes(4, s)
+    f = struct.unpack('<f', bs)[0]
+    return f
+
+
+def f64(s: InputStream) -> float:
+    bs = read_bytes(8, s)
+    f = struct.unpack('<d', bs)[0]
+    return f

pykwasm/src/pykwasm/binary/indices.py

@@ -0,0 +1,74 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+import pykwasm.kwasm_ast as wast
+
+from .integers import u32
+from .utils import WasmParseError, read_byte
+
+if TYPE_CHECKING:
+    from pyk.kast.inner import KInner
+
+    from .utils import InputStream
+
+
+def typeidx(s: InputStream) -> int:
+    return u32(s)
+
+
+def funcidx(s: InputStream) -> int:
+    return u32(s)
+
+
+def tableidx(s: InputStream) -> int:
+    return u32(s)
+
+
+# TODO multi-memory support is future work; the K semantics models a single memory,
+# so any reference to a memory other than 0 is rejected instead of mis-executing.
+def memidx(s: InputStream) -> int:
+    x = u32(s)
+    if x != 0:
+        raise WasmParseError(f'Multi-memory is not supported. Expected memory index 0, got: {x}')
+    return x
+
+
+def globalidx(s: InputStream) -> int:
+    return u32(s)
+
+
+def tagidx(s: InputStream) -> int:
+    return u32(s)
+
+
+def elemidx(s: InputStream) -> int:
+    return u32(s)
+
+
+def dataidx(s: InputStream) -> int:
+    return u32(s)
+
+
+def localidx(s: InputStream) -> int:
+    return u32(s)
+
+
+def labelidx(s: InputStream) -> int:
+    return u32(s)
+
+
+def externidx(s: InputStream) -> KInner:
+    match read_byte(s):
+        case 0x00:
+            return wast.externidx_func(funcidx(s))
+        case 0x01:
+            return wast.externidx_table(tableidx(s))
+        case 0x02:
+            return wast.externidx_memory(memidx(s))
+        case 0x03:
+            return wast.externidx_global(globalidx(s))
+        case 0x04:
+            return wast.externidx_tag(tagidx(s))
+        case x:
+            raise WasmParseError(f'Invalid externidx descriptor: {x}')