Add sign-extension operators (#523)

* implement sign-extension operators * add tests * update py-wasm * wasm2kast: add sign extension operators * add mx basic-features.wat binary parser test * install wabt with apt-get
runtimeverification · Nov 14, 2023 · cfd200d · cfd200d
1 parent 822d849
commit cfd200d
Show file tree

Hide file tree

Showing 10 changed files with 22,212 additions and 162 deletions.
diff --git a/Dockerfile b/Dockerfile
@@ -8,7 +8,8 @@ RUN    apt-get update              \
                        curl        \
                        pandoc      \
                        python3     \
-                       python3-pip
+                       python3-pip \
+                       wabt
 
 RUN    git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.15 \
     && cd z3                                                         \
@@ -33,11 +34,4 @@ RUN pip3 install --user  \
            cytoolz       \
            numpy
 
-RUN    git clone 'https://github.com/WebAssembly/wabt' --branch 1.0.13 --recurse-submodules wabt \
-    && cd wabt                                                                                   \
-    && mkdir build                                                                               \
-    && cd build                                                                                  \
-    && cmake ..                                                                                  \
-    && cmake --build .
-
 ENV PATH=/home/user/wabt/build:/home/user/.local/bin:$PATH
diff --git a/numeric.md b/numeric.md
@@ -24,6 +24,11 @@ module WASM-NUMERIC-SYNTAX
                    | "nearest" [klabel(aNearest), symbol]
  // -----------------------------------------------------
 
+    syntax ExtendS ::= "extend8_s"   [klabel(aExtend8_s) , symbol]
+                     | "extend16_s"  [klabel(aExtend16_s), symbol]
+                     | "extend32_s"  [klabel(aExtend32_s), symbol]
+ // ---------------------------------------------------------------
+
     syntax IBinOp ::= "add" [klabel(intAdd), symbol]
                     | "sub" [klabel(intSub), symbol]
                     | "mul" [klabel(intMul), symbol]
@@ -110,9 +115,10 @@ module WASM-NUMERIC
 `*UnOp` takes one oprand and returns a `Val`.
 
 ```k
-    syntax Val ::= IValType "." IUnOp Int   [klabel(intUnOp)  , function]
-                 | FValType "." FUnOp Float [klabel(floatUnOp), function]
- // ---------------------------------------------------------------------
+    syntax Val ::= IValType "." IUnOp   Int   [klabel(intUnOp)    , function]
+                 | FValType "." FUnOp   Float [klabel(floatUnOp)  , function]
+                 | IValType "." ExtendS Int   [klabel(extendSUnOp), function]
+ // ---------------------------------------------------------------------------
 ```
 
 #### Unary Operators for Integers
@@ -178,6 +184,20 @@ There are 7 unary operators for floats: `abs`, `neg`, `sqrt`, `floor`, `ceil`, `
     rule FTYPE . nearest F => < FTYPE > -0.0              requires (notBool #isInfinityOrNaN (F)) andBool          Float2Int(F) ==Int 0 andBool signFloat(F)
 ```
 
+#### Sign-extension Operators for Integers
+
+There are 3 sign-extension operators for integers.
+
+- `extend8_s`
+- `extend16_s`
+- `extend32_s`
+
+```k
+    rule ITYPE . extend8_s I  => #extends(ITYPE, 1, #wrap(1, I)) 
+    rule ITYPE . extend16_s I => #extends(ITYPE, 2, #wrap(2, I))
+    rule ITYPE . extend32_s I => #extends(ITYPE, 4, #wrap(4, I))
+```
+
 ### Binary Operators
 
 `*BinOp` takes two oprands and returns a `Val`.
@@ -425,7 +445,13 @@ There are 7 conversion operators: `wrap`, `extend`, `trunc`, `convert`, `demote`
 
 ```k
     rule i64 . extend_i32_u I:Int => < i64 > I
-    rule i64 . extend_i32_s I:Int => < i64 > #unsigned(i64, #signed(i32, I))
+    rule i64 . extend_i32_s I:Int => #extends(i64, 4, I)
+
+    syntax IVal ::= #extends(to: IValType, width: Int, val: Int)    [function, klabel(extends), symbol]
+ // ---------------------------------------------------------------------------------------------------
+    rule #extends(ITYPE, WIDTH, VAL) => < ITYPE > #unsigned(ITYPE, #signedWidth(WIDTH, VAL))
+      requires WIDTH <=Int #numBytes(ITYPE)
+
 ```
 
 - `convert` takes an `int` type value and convert it to the nearest `float` type value.

diff --git a/pykwasm/poetry.lock b/pykwasm/poetry.lock
diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml
@@ -15,7 +15,7 @@ python = "^3.10"
 cytoolz = "^0.12.1"
 numpy = "^1.24.2"
 pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.489" }
-py-wasm = {url = "https://github.com/runtimeverification/py-wasm/archive/refs/tags/0.1.0-alpha.0.tar.gz"}
+py-wasm = {url = "https://github.com/runtimeverification/py-wasm/archive/refs/tags/0.1.1.tar.gz"}
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"

diff --git a/pykwasm/src/pykwasm/kwasm_ast.py b/pykwasm/src/pykwasm/kwasm_ast.py
@@ -243,6 +243,11 @@ def CALL_INDIRECT(type_idx: int) -> KInner:
 I64_CLZ = KApply('aIUnOp', [i64, KApply('aClz', [])])
 I64_CTZ = KApply('aIUnOp', [i64, KApply('aCtz', [])])
 I64_POPCNT = KApply('aIUnOp', [i64, KApply('aPopcnt', [])])
+I32_EXTEND8_s = KApply('aExtendS', [i32, KApply('aExtend8_s', [])])
+I32_EXTEND16_s = KApply('aExtendS', [i32, KApply('aExtend16_s', [])])
+I64_EXTEND8_s = KApply('aExtendS', [i32, KApply('aExtend8_s', [])])
+I64_EXTEND8_s = KApply('aExtendS', [i32, KApply('aExtend16_s', [])])
+I64_EXTEND8_s = KApply('aExtendS', [i32, KApply('aExtend32_s', [])])
 
 ###############
 # Float BinOp #