diff --git a/package/version b/package/version index c892edd..9c4d21f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.51 +0.1.52 diff --git a/pyproject.toml b/pyproject.toml index 2748ae1..7840602 100644 --- a/pyproject.toml +++ b/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. ", diff --git a/src/kriscv/kdist/riscv-semantics/riscv-disassemble.md b/src/kriscv/kdist/riscv-semantics/riscv-disassemble.md index f689136..9951231 100644 --- a/src/kriscv/kdist/riscv-semantics/riscv-disassemble.md +++ b/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 diff --git a/src/kriscv/kdist/riscv-semantics/riscv-instructions.md b/src/kriscv/kdist/riscv-semantics/riscv-instructions.md index 7fae1f0..3b6578b 100644 --- a/src/kriscv/kdist/riscv-semantics/riscv-instructions.md +++ b/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 ::= diff --git a/src/kriscv/kdist/riscv-semantics/riscv.md b/src/kriscv/kdist/riscv-semantics/riscv.md index 1579597..a38a14d 100644 --- a/src/kriscv/kdist/riscv-semantics/riscv.md +++ b/src/kriscv/kdist/riscv-semantics/riscv.md @@ -253,6 +253,22 @@ The following instructions behave analogously to their `I`-suffixed counterparts rule XOR RD , RS1 , RS2 => .K ... REGS => writeReg(REGS, RD, readReg(REGS, RS1) xorWord readReg(REGS, RS2)) ``` +`MUL` gives the lowest `XLEN` bits after multiplication. +```k + rule MUL RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) *Word readReg(REGS, RS2)) +``` +`MULU`, `MULHU`, `MULHSU` give the higher `XLEN` bits after multiplication, with signedness of the operands interpreted accordingly. +```k + rule MULH RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) *hWord readReg(REGS, RS2)) + + rule MULHU RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) *huWord readReg(REGS, RS2)) + + rule MULHSU RD , RS1 , RS2 => .K ... + REGS => writeReg(REGS, RD, readReg(REGS, RS1) *hsuWord 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 cbaf15d..2e807f9 100644 --- a/src/kriscv/kdist/riscv-semantics/word.md +++ b/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] diff --git a/src/tests/integration/test_functions.py b/src/tests/integration/test_functions.py index 37377bc..cbf44ad 100644 --- a/src/tests/integration/test_functions.py +++ b/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), + )