Implement MULH, MULHU, MULHSU

Author: tothtamas28

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

@@ -258,6 +258,17 @@ The following instructions behave analogously to their `I`-suffixed counterparts
   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

@@ -74,6 +74,17 @@ The same is true for the `XLEN` least-significant bits of the result of multipli
   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

@@ -21,6 +21,18 @@ 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(
         (
@@ -59,20 +71,13 @@ 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
-    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))
-
-    # When
-    actual = llvm_interpret(definition_dir, init)
-
-    # Then
-    assert actual == expected
-
+    def disassemble(n: int) -> App:
+        return App('Lbldisassemble', (), (int_dv(n),))
 
-def disassemble(n: int) -> App:
-    return App('Lbldisassemble', (), (int_dv(n),))
+    n = int.from_bytes(code, byteorder='big')
+    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)
 
 
 def is_32bit(x: int) -> bool:
@@ -104,19 +109,62 @@ def signed(x: int) -> int:
 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:
-    # Given
-    init = config(inj(SortApp('SortWord'), SORT_K_ITEM, App('LblmulWord', (), (w(op1), w(op2)))))
-    res = chop(op1 * op2)
-    expected = config(inj(SortApp('SortWord'), SORT_K_ITEM, w(res)))
+    _test_mul(
+        definition_dir=definition_dir,
+        symbol='LblmulWord',
+        op1=op1,
+        op2=op2,
+        res=chop(op1 * op2),
+    )
 
-    # When
-    actual = llvm_interpret(definition_dir, init)
 
-    # Then
-    assert actual == expected
+@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),
+    )
 
 
-def w(x: int) -> App:
-    return App('LblW', (), (int_dv(x),))
+@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),
+    )
+
+
+@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),
+    )