Add signed and unsigned remainder operations for RISC-V semantics (#160)

Implement rules for `REM` and `REMU` instructions in `riscv.md`,
detailing their behavior and special cases. Update syntax definitions in
`word.md` to include remainder operations, and provide comprehensive
handling for division by zero and overflow scenarios. Adjust test
integration to utilize the `rv32em` architecture for relevant tests.


Close runtimeverification/zkevm-harness#80

---------

Co-authored-by: devops <devops@runtimeverification.com>

Author: Stevengre

package/version

@@ -1 +1 @@
-0.1.118
+0.1.119

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kriscv"
-version = "0.1.118"
+version = "0.1.119"
 description = "K tooling for the RISC-V architecture"
 readme = "README.md"
 requires-python = "~=3.10"

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

@@ -258,6 +258,14 @@ The following instructions behave analogously to their `I`-suffixed counterparts
   rule <instrs> DIVU RD , RS1 , RS2 => .K ...</instrs>
        <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) /uWord readReg(REGS, RS2)) </regs>
 ```
+`REM` and `REMU` perform signed and unsigned remainder, respectively.
+```k
+  rule <instrs> REM RD , RS1 , RS2 => .K ...</instrs>
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) %Word readReg(REGS, RS2)) </regs>
+
+  rule <instrs> REMU RD , RS1 , RS2 => .K ...</instrs>
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) %uWord 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

@@ -63,6 +63,8 @@ To avoid syntax conflicts, we define the following syntax with `left` associativ
                 | Int "*hsuWord" Int [function, total, symbol(mulhsuWord)]
                 | Int "/Word"    Int [function, total, symbol(divWord)]
                 | Int "/uWord"   Int [function, total, symbol(divuWord)]
+                | Int "%Word"    Int [function, total, symbol(remWord)]
+                | Int "%uWord"   Int [function, total, symbol(remuWord)]
                 > left:
                   Int "+Word"    Int [function, total, symbol(addWord)]
                 | Int "-Word"    Int [function, total, symbol(subWord)]
@@ -114,6 +116,26 @@ For unsigned division (`/uWord`):
   rule _  /uWord W2 => chop((2 ^Int XLEN) -Int 1) requires W2 ==Word 0
   rule W1 /uWord W2 => chop(W1 /Int W2) requires W2 =/=Word 0
 ```
+For signed remainder (`%Word`):
+- Division by zero returns the dividend
+- Signed overflow (most negative number divided by -1) returns 0
+- Normal case performs signed remainder with truncation towards zero
+```k
+  rule W1 %Word W2 => W1 requires W2 ==Word 0
+  rule W1 %Word W2 => 0 
+    requires W1 ==Word 2 ^Int (XLEN -Int 1)
+     andBool W2 ==Word chop(-1)
+  rule W1 %Word W2 => chop(Word2SInt(W1) %Int Word2SInt(W2)) 
+    requires W2 =/=Word 0 
+     andBool notBool (W1 ==Word chop(2 ^Int (XLEN -Int 1)) andBool W2 ==Word chop(-1))
+```
+For unsigned remainder (`%uWord`):
+- Division by zero returns the dividend
+- Normal case performs unsigned remainder with truncation towards zero
+```k
+  rule W1 %uWord W2 => W1 requires W2 ==Word 0
+  rule W1 %uWord W2 => chop(W1 %Int W2) requires W2 =/=Word 0
+```
 Above, the `chop` utility function
 ```k
   syntax Int ::= chop(Int) [function, total]

src/tests/integration/test_functions.py

@@ -238,3 +238,50 @@ def test_divu(definition_dir: Path, op1: int, op2: int) -> None:
         op2=op2,
         res=divu_expected(op1, op2),
     )
+
+
+def rem_expected(op1: int, op2: int) -> int:
+    # Calculate expected result according to RISC-V specification for signed remainder
+    if op2 == 0:
+        # Division by zero returns the dividend
+        expected = op1
+    elif op1 == 0x80000000 and op2 == 0xFFFFFFFF:
+        # Signed overflow: -2^31 % -1 returns 0
+        expected = 0
+    else:
+        # Normal signed remainder with truncation towards zero
+        expected = chop(signed(op1) % signed(op2))
+    return expected
+
+
+@pytest.mark.parametrize('op1,op2', DIV_TEST_DATA, ids=count())
+def test_rem(definition_dir: Path, op1: int, op2: int) -> None:
+    _test_binary_op(
+        definition_dir=definition_dir,
+        symbol='LblremWord',
+        op1=op1,
+        op2=op2,
+        res=rem_expected(op1, op2),
+    )
+
+
+def remu_expected(op1: int, op2: int) -> int:
+    # Calculate expected result according to RISC-V specification for unsigned remainder
+    if op2 == 0:
+        # Division by zero returns the dividend
+        expected = op1
+    else:
+        # Normal unsigned remainder with truncation towards zero
+        expected = op1 % op2
+    return expected
+
+
+@pytest.mark.parametrize('op1,op2', DIV_TEST_DATA, ids=count())
+def test_remu(definition_dir: Path, op1: int, op2: int) -> None:
+    _test_binary_op(
+        definition_dir=definition_dir,
+        symbol='LblremuWord',
+        op1=op1,
+        op2=op2,
+        res=remu_expected(op1, op2),
+    )

src/tests/integration/test_integration.py

@@ -123,12 +123,14 @@ def _test_simple(tools: Tools, elf_file: Path, assert_file: Path, final_config_o
 )
 def test_simple(asm_file: Path, save_final_config: bool, temp_dir: Path) -> None:
     elf_file = Path(temp_dir) / (asm_file.stem + '.elf')
+    # Use rv32em for tests that require M extension (mul/div/rem instructions)
+    arch = 'rv32em' if asm_file.stem in ['rem', 'remu'] else 'rv32e'
     compile_cmd = [
         'riscv64-unknown-elf-gcc',
         '-nostdlib',
         '-nostartfiles',
         '-static',
-        '-march=rv32e',
+        f'-march={arch}',
         '-mabi=ilp32e',
         '-mno-relax',
         '-mlittle-endian',

tests/simple/rem.S

@@ -0,0 +1,28 @@
+#include "simple.h"
+
+START_TEXT
+	// Test basic signed remainder operations
+	li x1, 17    // x1 = 17
+	li x2, 5     // x2 = 5
+	rem x3, x1, x2  // x3 = 17 % 5 = 2
+
+	// Test negative dividend
+	li x4, -17   // x4 = -17
+	rem x5, x4, x2  // x5 = -17 % 5 = -2
+
+	// Test negative divisor
+	li x6, -5    // x6 = -5
+	rem x7, x1, x6  // x7 = 17 % -5 = 2
+
+	// Test both negative
+	rem x8, x4, x6  // x8 = -17 % -5 = -2
+
+	// Test division by zero (should return dividend)
+	li x9, 0     // x9 = 0
+	rem x10, x1, x9  // x10 = 17 % 0 = 17
+
+	// Test overflow case (most negative number % -1)
+	li x11, 0x80000000  // x11 = most negative number
+	li x12, -1          // x12 = -1
+	rem x13, x11, x12   // x13 = most negative % -1 = 0
+END_TEXT

tests/simple/rem.S.assert

@@ -0,0 +1 @@
+regs: {3: 2, 5: -2, 7: 2, 8: -2, 10: 17, 13: 0}

tests/simple/remu.S

@@ -0,0 +1,27 @@
+#include "simple.h"
+
+START_TEXT
+	// Test basic unsigned remainder operations
+	li x1, 17    // x1 = 17
+	li x2, 5     // x2 = 5
+	remu x3, x1, x2  // x3 = 17 % 5 = 2
+
+	// Test large unsigned values
+	li x4, 0xFFFFFFFF  // x4 = 0xFFFFFFFF (large unsigned)
+	li x5, 10          // x5 = 10
+	remu x6, x4, x5    // x6 = 0xFFFFFFFF % 10 = 5
+
+	// Test division by zero (should return dividend)
+	li x7, 0     // x7 = 0
+	remu x8, x1, x7  // x8 = 17 % 0 = 17
+
+	// Test large divisor
+	li x9, 0x80000000  // x9 = 0x80000000
+	li x10, 0x40000000 // x10 = 0x40000000
+	remu x11, x9, x10  // x11 = 0x80000000 % 0x40000000 = 0
+
+	// Test remainder equals dividend
+	li x12, 100        // x12 = 100
+	li x13, 200        // x13 = 200
+	remu x14, x12, x13 // x14 = 100 % 200 = 100
+END_TEXT

tests/simple/remu.S.assert

@@ -0,0 +1 @@
+regs: {3: 2, 6: 5, 8: 17, 11: 0, 14: 100}