diff --git a/package/version b/package/version index 1fcba8fa..841597f0 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.118 +0.1.119 diff --git a/pyproject.toml b/pyproject.toml index 9af66d9e..fa241252 100644 --- a/pyproject.toml +++ b/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" diff --git a/src/kriscv/kdist/riscv-semantics/riscv.md b/src/kriscv/kdist/riscv-semantics/riscv.md index 8e62e2fb..4cffaa53 100644 --- a/src/kriscv/kdist/riscv-semantics/riscv.md +++ b/src/kriscv/kdist/riscv-semantics/riscv.md @@ -258,6 +258,14 @@ The following instructions behave analogously to their `I`-suffixed counterparts rule DIVU RD , RS1 , RS2 => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS1) /uWord readReg(REGS, RS2)) ``` +`REM` and `REMU` perform signed and unsigned remainder, respectively. +```k + rule REM RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) %Word readReg(REGS, RS2)) + + rule REMU RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) %uWord readReg(REGS, RS2)) +``` `SLL`, `SRL`, and `SRA` read their shift amount fom the lowest `log_2(XLEN)` bits of `RS2`. ```k rule SLL RD , RS1 , RS2 => .K ... diff --git a/src/kriscv/kdist/riscv-semantics/word.md b/src/kriscv/kdist/riscv-semantics/word.md index 038ee337..fbb39efb 100644 --- a/src/kriscv/kdist/riscv-semantics/word.md +++ b/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] diff --git a/src/tests/integration/test_functions.py b/src/tests/integration/test_functions.py index cfc32b03..ca75be90 100644 --- a/src/tests/integration/test_functions.py +++ b/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), + ) diff --git a/src/tests/integration/test_integration.py b/src/tests/integration/test_integration.py index c602d2bd..400b0268 100644 --- a/src/tests/integration/test_integration.py +++ b/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', diff --git a/tests/simple/rem.S b/tests/simple/rem.S new file mode 100644 index 00000000..49877423 --- /dev/null +++ b/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 diff --git a/tests/simple/rem.S.assert b/tests/simple/rem.S.assert new file mode 100644 index 00000000..6e3cb37f --- /dev/null +++ b/tests/simple/rem.S.assert @@ -0,0 +1 @@ +regs: {3: 2, 5: -2, 7: 2, 8: -2, 10: 17, 13: 0} diff --git a/tests/simple/remu.S b/tests/simple/remu.S new file mode 100644 index 00000000..043bd2b6 --- /dev/null +++ b/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 diff --git a/tests/simple/remu.S.assert b/tests/simple/remu.S.assert new file mode 100644 index 00000000..34576373 --- /dev/null +++ b/tests/simple/remu.S.assert @@ -0,0 +1 @@ +regs: {3: 2, 6: 5, 8: 17, 11: 0, 14: 100} diff --git a/uv.lock b/uv.lock index 1b71ab05..a16b3ed0 100644 --- a/uv.lock +++ b/uv.lock @@ -420,7 +420,7 @@ name = "exceptiongroup" version = "1.3.0" source = { registry = "https://pypi.org/simple" } dependencies = [ - { name = "typing-extensions", marker = "python_full_version < '3.13'" }, + { name = "typing-extensions", marker = "python_full_version < '3.11'" }, ] sdist = { url = "https://files.pythonhosted.org/packages/0b/9f/a65090624ecf468cdca03533906e7c69ed7588582240cfe7cc9e770b50eb/exceptiongroup-1.3.0.tar.gz", hash = "sha256:b241f5885f560bc56a59ee63ca4c6a8bfa46ae4ad651af316d4e81817bb9fd88", size = 29749, upload-time = "2025-05-10T17:42:51.123Z" } wheels = [ @@ -631,7 +631,7 @@ wheels = [ [[package]] name = "kriscv" -version = "0.1.118" +version = "0.1.119" source = { editable = "." } dependencies = [ { name = "filelock" },