Add division operations for RISC-V semantics (#146)

Implement signed (`/Word`) and unsigned (`/uWord`) division rules in the
RISC-V semantics. Update the handling of special cases for division by
zero and signed overflow. Refactor test functions to include
comprehensive test cases for both division operations, ensuring
compliance with RISC-V specifications.

- Added rules for `DIV` and `DIVU` instructions in `riscv.md`.
- Updated syntax definitions in `word.md` for division operations.
- Introduced new test cases for division in `test_functions.py` to
validate expected behavior.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>

Author: 4 people

package/version

@@ -1 +1 @@
-0.1.110
+0.1.111

pyproject.toml

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

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

@@ -250,6 +250,14 @@ The following instructions behave analogously to their `I`-suffixed counterparts
   rule <instrs> MULHSU RD , RS1 , RS2 => .K ...</instrs>
        <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) *hsuWord readReg(REGS, RS2)) </regs>
 ```
+`DIV` and `DIVU` perform signed and unsigned division, respectively.
+```k
+  rule <instrs> DIV RD , RS1 , RS2 => .K ...</instrs>
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) /Word readReg(REGS, RS2)) </regs>
+
+  rule <instrs> DIVU 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

@@ -61,6 +61,8 @@ To avoid syntax conflicts, we define the following syntax with `left` associativ
                 | Int "*hWord"   Int [function, total, symbol(mulhWord)]
                 | Int "*huWord"  Int [function, total, symbol(mulhuWord)]
                 | Int "*hsuWord" Int [function, total, symbol(mulhsuWord)]
+                | Int "/Word"    Int [function, total, symbol(divWord)]
+                | Int "/uWord"   Int [function, total, symbol(divuWord)]
                 > left:
                   Int "+Word"    Int [function, total, symbol(addWord)]
                 | Int "-Word"    Int [function, total, symbol(subWord)]
@@ -75,7 +77,6 @@ To avoid syntax conflicts, we define the following syntax with `left` associativ
                 > left:
                   Int "|Word"    Int [function, total, symbol(orWord)]
 ```
-
 Note that two's complement enables us to use a single addition or subtraction operation for both signed and unsigned values.
 ```k
   rule W1 +Word W2 => chop(W1 +Int W2)
@@ -91,6 +92,28 @@ The value of the upper `XLEN` bits however depends on signedness of the operands
   rule W1 *huWord W2 => chop((W1 *Int W2) >>Int XLEN)
   rule W1 *hsuWord W2 => chop((Word2SInt(W1) *Int W2) >>Int XLEN)
 ```
+Division operations follow RISC-V specification requirements for handling special cases.
+
+For signed division (`/Word`):
+- Division by zero returns -1 (all bits set)
+- Signed overflow (most negative number divided by -1) returns the dividend unchanged
+- Normal case performs signed division with truncation towards zero
+```k
+  rule _  /Word W2 => chop(-1) requires W2 ==Word 0
+  rule W1 /Word W2 => W1 
+    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 division (`/uWord`):
+- Division by zero returns 2^XLEN - 1 (all bits set)
+- Normal case performs unsigned division with truncation towards zero
+```k
+  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
+```
 Above, the `chop` utility function
 ```k
   syntax Int ::= chop(Int) [function, total]

src/tests/integration/test_functions.py

@@ -109,7 +109,7 @@ def signed(x: int) -> int:
 assert all(is_32bit(op1) and is_32bit(op2) for op1, op2 in MUL_TEST_DATA)
 
 
-def _test_mul(
+def _test_binary_op(
     definition_dir: Path,
     symbol: str,
     op1: int,
@@ -125,7 +125,7 @@ def _test_mul(
 
 @pytest.mark.parametrize('op1,op2', MUL_TEST_DATA, ids=count())
 def test_mul(definition_dir: Path, op1: int, op2: int) -> None:
-    _test_mul(
+    _test_binary_op(
         definition_dir=definition_dir,
         symbol='LblmulWord',
         op1=op1,
@@ -136,7 +136,7 @@ def test_mul(definition_dir: Path, op1: int, op2: int) -> None:
 
 @pytest.mark.parametrize('op1,op2', MUL_TEST_DATA, ids=count())
 def test_mulh(definition_dir: Path, op1: int, op2: int) -> None:
-    _test_mul(
+    _test_binary_op(
         definition_dir=definition_dir,
         symbol='LblmulhWord',
         op1=op1,
@@ -147,7 +147,7 @@ def test_mulh(definition_dir: Path, op1: int, op2: int) -> None:
 
 @pytest.mark.parametrize('op1,op2', MUL_TEST_DATA, ids=count())
 def test_mulhu(definition_dir: Path, op1: int, op2: int) -> None:
-    _test_mul(
+    _test_binary_op(
         definition_dir=definition_dir,
         symbol='LblmulhuWord',
         op1=op1,
@@ -158,10 +158,83 @@ def test_mulhu(definition_dir: Path, op1: int, op2: int) -> None:
 
 @pytest.mark.parametrize('op1,op2', MUL_TEST_DATA, ids=count())
 def test_mulhsu(definition_dir: Path, op1: int, op2: int) -> None:
-    _test_mul(
+    _test_binary_op(
         definition_dir=definition_dir,
         symbol='LblmulhsuWord',
         op1=op1,
         op2=op2,
         res=chop((signed(op1) * op2) >> 32),
     )
+
+
+DIV_TEST_DATA: Final = (
+    # Normal division cases
+    (10, 3),
+    (100, 7),
+    (0xFFFFFFFF, 1),  # -1 / 1 = -1
+    (0xFFFFFFFE, 2),  # -2 / 2 = -1
+    (0x80000000, 2),  # -2^31 / 2 = -2^30
+    (15, 4),
+    (0x7FFFFFFF, 3),  # 2^31-1 / 3
+    # Division by zero cases
+    (0, 0),
+    (1, 0),
+    (0xFFFFFFFF, 0),  # -1 / 0
+    (0x80000000, 0),  # -2^31 / 0
+    (0x7FFFFFFF, 0),  # 2^31-1 / 0
+    # Signed overflow case: -2^31 / -1
+    (0x80000000, 0xFFFFFFFF),  # -2^31 / -1 should return -2^31
+    # Additional edge cases
+    (0x80000001, 0xFFFFFFFF),  # (-2^31+1) / -1 = 2^31-1
+    (0x7FFFFFFF, 0xFFFFFFFF),  # (2^31-1) / -1 = -(2^31-1)
+)
+
+
+assert all(is_32bit(op1) and is_32bit(op2) for op1, op2 in DIV_TEST_DATA)
+
+
+def div_expected(op1: int, op2: int) -> int:
+    # Calculate expected result according to RISC-V specification
+    if op2 == 0:
+        # Division by zero returns -1 (all bits set)
+        expected = 0xFFFFFFFF
+    elif op1 == 0x80000000 and op2 == 0xFFFFFFFF:
+        # Signed overflow: -2^31 / -1 returns the dividend (-2^31)
+        expected = 0x80000000
+    else:
+        # Normal signed division with truncation towards zero
+        expected = chop(signed(op1) // signed(op2))
+    return expected
+
+
+@pytest.mark.parametrize('op1,op2', DIV_TEST_DATA, ids=count())
+def test_div(definition_dir: Path, op1: int, op2: int) -> None:
+    _test_binary_op(
+        definition_dir=definition_dir,
+        symbol='LbldivWord',
+        op1=op1,
+        op2=op2,
+        res=div_expected(op1, op2),
+    )
+
+
+def divu_expected(op1: int, op2: int) -> int:
+    # Calculate expected result according to RISC-V specification
+    if op2 == 0:
+        # Division by zero returns 2^32 - 1 (all bits set)
+        expected = 0xFFFFFFFF
+    else:
+        # Normal unsigned division with truncation towards zero
+        expected = op1 // op2
+    return expected
+
+
+@pytest.mark.parametrize('op1,op2', DIV_TEST_DATA, ids=count())
+def test_divu(definition_dir: Path, op1: int, op2: int) -> None:
+    _test_binary_op(
+        definition_dir=definition_dir,
+        symbol='LbldivuWord',
+        op1=op1,
+        op2=op2,
+        res=divu_expected(op1, op2),
+    )