Implement MUL* instructions

package/version

@@ -1 +1 @@
-0.1.51
+0.1.52

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.51"
+version = "0.1.52"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/kriscv/kdist/riscv-semantics/riscv-disassemble.md

@@ -103,16 +103,24 @@ Finally, we can disassemble the instruction by inspecting the fields for each fo
 ```k
   syntax Instruction ::= disassemble(InstructionFormat) [function, total]
 
-  rule disassemble(RType(OP, 0, 0,  RD, RS1, RS2)) => ADD  RD , RS1 , RS2
-  rule disassemble(RType(OP, 0, 32, RD, RS1, RS2)) => SUB  RD , RS1 , RS2
-  rule disassemble(RType(OP, 1, 0,  RD, RS1, RS2)) => SLL  RD , RS1 , RS2
-  rule disassemble(RType(OP, 2, 0,  RD, RS1, RS2)) => SLT  RD , RS1 , RS2
-  rule disassemble(RType(OP, 3, 0,  RD, RS1, RS2)) => SLTU RD , RS1 , RS2
-  rule disassemble(RType(OP, 4, 0,  RD, RS1, RS2)) => XOR  RD , RS1 , RS2
-  rule disassemble(RType(OP, 5, 0,  RD, RS1, RS2)) => SRL  RD , RS1 , RS2
-  rule disassemble(RType(OP, 5, 32, RD, RS1, RS2)) => SRA  RD , RS1 , RS2
-  rule disassemble(RType(OP, 6, 0,  RD, RS1, RS2)) => OR   RD , RS1 , RS2
-  rule disassemble(RType(OP, 7, 0,  RD, RS1, RS2)) => AND  RD , RS1 , RS2
+  rule disassemble(RType(OP, 0, 0,  RD, RS1, RS2)) => ADD    RD , RS1 , RS2
+  rule disassemble(RType(OP, 0, 32, RD, RS1, RS2)) => SUB    RD , RS1 , RS2
+  rule disassemble(RType(OP, 1, 0,  RD, RS1, RS2)) => SLL    RD , RS1 , RS2
+  rule disassemble(RType(OP, 2, 0,  RD, RS1, RS2)) => SLT    RD , RS1 , RS2
+  rule disassemble(RType(OP, 3, 0,  RD, RS1, RS2)) => SLTU   RD , RS1 , RS2
+  rule disassemble(RType(OP, 4, 0,  RD, RS1, RS2)) => XOR    RD , RS1 , RS2
+  rule disassemble(RType(OP, 5, 0,  RD, RS1, RS2)) => SRL    RD , RS1 , RS2
+  rule disassemble(RType(OP, 5, 32, RD, RS1, RS2)) => SRA    RD , RS1 , RS2
+  rule disassemble(RType(OP, 6, 0,  RD, RS1, RS2)) => OR     RD , RS1 , RS2
+  rule disassemble(RType(OP, 7, 0,  RD, RS1, RS2)) => AND    RD , RS1 , RS2
+  rule disassemble(RType(OP, 0, 1,  RD, RS1, RS2)) => MUL    RD , RS1 , RS2
+  rule disassemble(RType(OP, 1, 1,  RD, RS1, RS2)) => MULH   RD , RS1 , RS2
+  rule disassemble(RType(OP, 2, 1,  RD, RS1, RS2)) => MULHSU RD , RS1 , RS2
+  rule disassemble(RType(OP, 3, 1,  RD, RS1, RS2)) => MULHU  RD , RS1 , RS2
+  rule disassemble(RType(OP, 4, 1,  RD, RS1, RS2)) => DIV    RD , RS1 , RS2
+  rule disassemble(RType(OP, 5, 1,  RD, RS1, RS2)) => DIVU   RD , RS1 , RS2
+  rule disassemble(RType(OP, 6, 1,  RD, RS1, RS2)) => REM    RD , RS1 , RS2
+  rule disassemble(RType(OP, 7, 1,  RD, RS1, RS2)) => REMU   RD , RS1 , RS2
 
   rule disassemble(IType(OP-IMM, 0, RD, RS1, IMM)) => ADDI  RD , RS1 , infSignExtend(IMM, 12)
   rule disassemble(IType(OP-IMM, 1, RD, RS1, IMM)) => SLLI  RD , RS1 , IMM &Int 31 requires (IMM >>Int 5) &Int 127 ==Int 0

src/kriscv/kdist/riscv-semantics/riscv-instructions.md

@@ -50,16 +50,24 @@ module RISCV-INSTRUCTIONS
 
   syntax RegRegRegInstr ::= RegRegRegInstrName Register "," Register "," Register [symbol(RegRegRegInstr)]
   syntax RegRegRegInstrName ::=
-      "ADD"  [symbol(ADD)]
-    | "SUB"  [symbol(SUB)]
-    | "SLT"  [symbol(SLT)]
-    | "SLTU" [symbol(SLTU)]
-    | "AND"  [symbol(AND)]
-    | "OR"   [symbol(OR)]
-    | "XOR"  [symbol(XOR)]
-    | "SLL"  [symbol(SLL)]
-    | "SRL"  [symbol(SRL)]
-    | "SRA"  [symbol(SRA)]
+      "ADD"    [symbol(ADD)]
+    | "SUB"    [symbol(SUB)]
+    | "SLT"    [symbol(SLT)]
+    | "SLTU"   [symbol(SLTU)]
+    | "AND"    [symbol(AND)]
+    | "OR"     [symbol(OR)]
+    | "XOR"    [symbol(XOR)]
+    | "SLL"    [symbol(SLL)]
+    | "SRL"    [symbol(SRL)]
+    | "SRA"    [symbol(SRA)]
+    | "MUL"    [symbol(MUL)]
+    | "MULH"   [symbol(MULH)]
+    | "MULHU"  [symbol(MULHU)]
+    | "MULHSU" [symbol(MULHSU)]
+    | "DIV"    [symbol(DIV)]
+    | "DIVU"   [symbol(DIVU)]
+    | "REM"    [symbol(REM)]
+    | "REMU"   [symbol(REMU)]
 
   syntax RegImmRegInstr ::= RegImmRegInstrName Register "," Int "(" Register ")" [symbol(RegImmRegInstr)]
   syntax RegImmRegInstrName ::=

src/kriscv/kdist/riscv-semantics/riscv.md

@@ -253,6 +253,22 @@ The following instructions behave analogously to their `I`-suffixed counterparts
   rule <instrs> XOR RD , RS1 , RS2 => .K ...</instrs>
        <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) xorWord readReg(REGS, RS2)) </regs>
 ```
+`MUL` gives the lowest `XLEN` bits after multiplication.
+```k
+  rule <instrs> MUL RD , RS1 , RS2 => .K ...</instrs>
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) *Word readReg(REGS, RS2)) </regs>
+```
+`MULU`, `MULHU`, `MULHSU` give the higher `XLEN` bits after multiplication, with signedness of the operands interpreted accordingly.
+```k
+  rule <instrs> MULH RD , RS1 , RS2 => .K ...</instrs>
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) *hWord readReg(REGS, RS2)) </regs>
+
+  rule <instrs> MULHU RD , RS1 , RS2 => .K ...</instrs>
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) *huWord readReg(REGS, RS2)) </regs>
+
+  rule <instrs> MULHSU RD , RS1 , RS2 => .K ...</instrs>
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) *hsuWord readReg(REGS, RS2)) </regs>
+```
 `SLL`, `SRL`, and `SRA` read their shift amount fom the lowest `log_2(XLEN)` bits of `RS2`.
 ```k
   rule <instrs> SLL RD , RS1 , RS2 => .K ...</instrs>

src/kriscv/kdist/riscv-semantics/word.md

@@ -69,6 +69,22 @@ Note that two's complement enables us to use a single addition or subtraction op
   syntax Word ::= Word "-Word" Word [function, total]
   rule W(I1) -Word W(I2) => chop(I1 -Int I2)
 ```
+The same is true for the `XLEN` least-significant bits of the result of multiplication.
+```k
+  syntax Word ::= Word "*Word" Word [function, total, symbol(mulWord)]
+  rule W(I1) *Word W(I2) => chop(I1 *Int I2)
+```
+The value of the upper `XLEN` bits however depends on signedness of the operands, as reflected by the followig functions.
+```k
+  syntax Word ::= Word "*hWord" Word [function, total, symbol(mulhWord)]
+  rule W1 *hWord W2 => chop((Word2SInt(W1) *Int Word2SInt(W2)) >>Int XLEN)
+
+  syntax Word ::= Word "*huWord" Word [function, total, symbol(mulhuWord)]
+  rule W(I1) *huWord W(I2) => chop((I1 *Int I2) >>Int XLEN)
+
+  syntax Word ::= Word "*hsuWord" Word [function, total, symbol(mulhsuWord)]
+  rule W1 *hsuWord W(I2) => chop((Word2SInt(W1) *Int I2) >>Int XLEN)
+```
 Above, the `chop` utility function
 ```k
   syntax Word ::= chop(Int) [function, total]

src/tests/integration/test_functions.py

@@ -1,5 +1,6 @@
 from __future__ import annotations
 
+from itertools import count
 from typing import TYPE_CHECKING
 
 import pytest
@@ -20,6 +21,27 @@ def definition_dir() -> Path:
     return kdist.get('riscv-semantics.func-test')
 
 
+def _test_function(definition_dir: Path, app: Pattern, res: Pattern) -> None:
+    # Given
+    init = config(app)
+    expected = config(res)
+
+    # When
+    actual = llvm_interpret(definition_dir, init)
+
+    # Then
+    assert actual == expected
+
+
+def config(kitem: Pattern) -> App:
+    return generated_top(
+        (
+            k(kseq((kitem,))),
+            generated_counter(int_dv(0)),
+        ),
+    )
+
+
 def sw(rs2: int, imm: int, rs1: int) -> App:
     return App(
         'LblRegImmRegInstr',
@@ -49,26 +71,100 @@ def reg(x: int) -> App:
     ids=[test_id for test_id, *_ in DISASSEMBLE_TEST_DATA],
 )
 def test_disassemble(definition_dir: Path, test_id: str, code: bytes, sort: SortApp, pattern: Pattern) -> None:
-    # Given
+    def disassemble(n: int) -> App:
+        return App('Lbldisassemble', (), (int_dv(n),))
+
     n = int.from_bytes(code, byteorder='big')
-    init = config(inj(SortApp('SortInstruction'), SORT_K_ITEM, disassemble(n)))
-    expected = config(inj(sort, SORT_K_ITEM, pattern))
+    app = inj(SortApp('SortInstruction'), SORT_K_ITEM, disassemble(n))
+    res = inj(sort, SORT_K_ITEM, pattern)
+    _test_function(definition_dir=definition_dir, app=app, res=res)
 
-    # When
-    actual = llvm_interpret(definition_dir, init)
 
-    # Then
-    assert actual == expected
+def is_32bit(x: int) -> bool:
+    return 0 <= x < 0x100000000
 
 
-def config(kitem: Pattern) -> App:
-    return generated_top(
-        (
-            k(kseq((kitem,))),
-            generated_counter(int_dv(0)),
-        ),
+def chop(x: int) -> int:
+    return x & 0xFFFFFFFF
+
+
+def signed(x: int) -> int:
+    assert is_32bit(x)
+    return x if x < 0x80000000 else x - 0x100000000
+
+
+MUL_TEST_DATA: Final = (
+    (0, 0),
+    (0, 1),
+    (1, 0),
+    (1, 1),
+    (0xFFFFFFFF, 1),
+    (0xFFFFFFFF, 12),
+    (0xFFFFFFFF, 0xFFFFFFFF),
+    (0xFFFF8765, 0xFFF01234),
+    (0xFFFF8765, 12),
+)
+
+
+assert all(is_32bit(op1) and is_32bit(op2) for op1, op2 in MUL_TEST_DATA)
+
+
+def _test_mul(
+    definition_dir: Path,
+    symbol: str,
+    op1: int,
+    op2: int,
+    res: int,
+) -> None:
+    def w(x: int) -> App:
+        return App('LblW', (), (int_dv(x),))
+
+    _test_function(
+        definition_dir=definition_dir,
+        app=inj(SortApp('SortWord'), SORT_K_ITEM, App(symbol, (), (w(op1), w(op2)))),
+        res=inj(SortApp('SortWord'), SORT_K_ITEM, w(res)),
+    )
+
+
+@pytest.mark.parametrize('op1,op2', MUL_TEST_DATA, ids=count())
+def test_mul(definition_dir: Path, op1: int, op2: int) -> None:
+    _test_mul(
+        definition_dir=definition_dir,
+        symbol='LblmulWord',
+        op1=op1,
+        op2=op2,
+        res=chop(op1 * op2),
+    )
+
+
+@pytest.mark.parametrize('op1,op2', MUL_TEST_DATA, ids=count())
+def test_mulh(definition_dir: Path, op1: int, op2: int) -> None:
+    _test_mul(
+        definition_dir=definition_dir,
+        symbol='LblmulhWord',
+        op1=op1,
+        op2=op2,
+        res=chop((signed(op1) * signed(op2)) >> 32),
+    )
+
+
+@pytest.mark.parametrize('op1,op2', MUL_TEST_DATA, ids=count())
+def test_mulhu(definition_dir: Path, op1: int, op2: int) -> None:
+    _test_mul(
+        definition_dir=definition_dir,
+        symbol='LblmulhuWord',
+        op1=op1,
+        op2=op2,
+        res=chop((op1 * op2) >> 32),
     )
 
 
-def disassemble(n: int) -> App:
-    return App('Lbldisassemble', (), (int_dv(n),))
+@pytest.mark.parametrize('op1,op2', MUL_TEST_DATA, ids=count())
+def test_mulhsu(definition_dir: Path, op1: int, op2: int) -> None:
+    _test_mul(
+        definition_dir=definition_dir,
+        symbol='LblmulhsuWord',
+        op1=op1,
+        op2=op2,
+        res=chop((signed(op1) * op2) >> 32),
+    )