Skip to content

Commit b8bf5d2

Browse files
tothtamas28rv-auditorautomergerpr-permission-manager[bot]
authored
Implement MUL* instructions (#60)
Adds disassembler support for the (32 bit) M extension, and implements `MUL`, `MULH`, `MULHU` and `MULHSU`. --------- Co-authored-by: devops <[email protected]> Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
1 parent 79552f6 commit b8bf5d2

File tree

7 files changed

+181
-37
lines changed

7 files changed

+181
-37
lines changed

‎package/version

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.1.51
1+
0.1.52

‎pyproject.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "kriscv"
7-
version = "0.1.51"
7+
version = "0.1.52"
88
description = "K tooling for the RISC-V architecture"
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

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

+18-10
Original file line numberDiff line numberDiff line change
@@ -103,16 +103,24 @@ Finally, we can disassemble the instruction by inspecting the fields for each fo
103103
```k
104104
syntax Instruction ::= disassemble(InstructionFormat) [function, total]
105105
106-
rule disassemble(RType(OP, 0, 0, RD, RS1, RS2)) => ADD RD , RS1 , RS2
107-
rule disassemble(RType(OP, 0, 32, RD, RS1, RS2)) => SUB RD , RS1 , RS2
108-
rule disassemble(RType(OP, 1, 0, RD, RS1, RS2)) => SLL RD , RS1 , RS2
109-
rule disassemble(RType(OP, 2, 0, RD, RS1, RS2)) => SLT RD , RS1 , RS2
110-
rule disassemble(RType(OP, 3, 0, RD, RS1, RS2)) => SLTU RD , RS1 , RS2
111-
rule disassemble(RType(OP, 4, 0, RD, RS1, RS2)) => XOR RD , RS1 , RS2
112-
rule disassemble(RType(OP, 5, 0, RD, RS1, RS2)) => SRL RD , RS1 , RS2
113-
rule disassemble(RType(OP, 5, 32, RD, RS1, RS2)) => SRA RD , RS1 , RS2
114-
rule disassemble(RType(OP, 6, 0, RD, RS1, RS2)) => OR RD , RS1 , RS2
115-
rule disassemble(RType(OP, 7, 0, RD, RS1, RS2)) => AND RD , RS1 , RS2
106+
rule disassemble(RType(OP, 0, 0, RD, RS1, RS2)) => ADD RD , RS1 , RS2
107+
rule disassemble(RType(OP, 0, 32, RD, RS1, RS2)) => SUB RD , RS1 , RS2
108+
rule disassemble(RType(OP, 1, 0, RD, RS1, RS2)) => SLL RD , RS1 , RS2
109+
rule disassemble(RType(OP, 2, 0, RD, RS1, RS2)) => SLT RD , RS1 , RS2
110+
rule disassemble(RType(OP, 3, 0, RD, RS1, RS2)) => SLTU RD , RS1 , RS2
111+
rule disassemble(RType(OP, 4, 0, RD, RS1, RS2)) => XOR RD , RS1 , RS2
112+
rule disassemble(RType(OP, 5, 0, RD, RS1, RS2)) => SRL RD , RS1 , RS2
113+
rule disassemble(RType(OP, 5, 32, RD, RS1, RS2)) => SRA RD , RS1 , RS2
114+
rule disassemble(RType(OP, 6, 0, RD, RS1, RS2)) => OR RD , RS1 , RS2
115+
rule disassemble(RType(OP, 7, 0, RD, RS1, RS2)) => AND RD , RS1 , RS2
116+
rule disassemble(RType(OP, 0, 1, RD, RS1, RS2)) => MUL RD , RS1 , RS2
117+
rule disassemble(RType(OP, 1, 1, RD, RS1, RS2)) => MULH RD , RS1 , RS2
118+
rule disassemble(RType(OP, 2, 1, RD, RS1, RS2)) => MULHSU RD , RS1 , RS2
119+
rule disassemble(RType(OP, 3, 1, RD, RS1, RS2)) => MULHU RD , RS1 , RS2
120+
rule disassemble(RType(OP, 4, 1, RD, RS1, RS2)) => DIV RD , RS1 , RS2
121+
rule disassemble(RType(OP, 5, 1, RD, RS1, RS2)) => DIVU RD , RS1 , RS2
122+
rule disassemble(RType(OP, 6, 1, RD, RS1, RS2)) => REM RD , RS1 , RS2
123+
rule disassemble(RType(OP, 7, 1, RD, RS1, RS2)) => REMU RD , RS1 , RS2
116124
117125
rule disassemble(IType(OP-IMM, 0, RD, RS1, IMM)) => ADDI RD , RS1 , infSignExtend(IMM, 12)
118126
rule disassemble(IType(OP-IMM, 1, RD, RS1, IMM)) => SLLI RD , RS1 , IMM &Int 31 requires (IMM >>Int 5) &Int 127 ==Int 0

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

+18-10
Original file line numberDiff line numberDiff line change
@@ -50,16 +50,24 @@ module RISCV-INSTRUCTIONS
5050
5151
syntax RegRegRegInstr ::= RegRegRegInstrName Register "," Register "," Register [symbol(RegRegRegInstr)]
5252
syntax RegRegRegInstrName ::=
53-
"ADD" [symbol(ADD)]
54-
| "SUB" [symbol(SUB)]
55-
| "SLT" [symbol(SLT)]
56-
| "SLTU" [symbol(SLTU)]
57-
| "AND" [symbol(AND)]
58-
| "OR" [symbol(OR)]
59-
| "XOR" [symbol(XOR)]
60-
| "SLL" [symbol(SLL)]
61-
| "SRL" [symbol(SRL)]
62-
| "SRA" [symbol(SRA)]
53+
"ADD" [symbol(ADD)]
54+
| "SUB" [symbol(SUB)]
55+
| "SLT" [symbol(SLT)]
56+
| "SLTU" [symbol(SLTU)]
57+
| "AND" [symbol(AND)]
58+
| "OR" [symbol(OR)]
59+
| "XOR" [symbol(XOR)]
60+
| "SLL" [symbol(SLL)]
61+
| "SRL" [symbol(SRL)]
62+
| "SRA" [symbol(SRA)]
63+
| "MUL" [symbol(MUL)]
64+
| "MULH" [symbol(MULH)]
65+
| "MULHU" [symbol(MULHU)]
66+
| "MULHSU" [symbol(MULHSU)]
67+
| "DIV" [symbol(DIV)]
68+
| "DIVU" [symbol(DIVU)]
69+
| "REM" [symbol(REM)]
70+
| "REMU" [symbol(REMU)]
6371
6472
syntax RegImmRegInstr ::= RegImmRegInstrName Register "," Int "(" Register ")" [symbol(RegImmRegInstr)]
6573
syntax RegImmRegInstrName ::=

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

+16
Original file line numberDiff line numberDiff line change
@@ -253,6 +253,22 @@ The following instructions behave analogously to their `I`-suffixed counterparts
253253
rule <instrs> XOR RD , RS1 , RS2 => .K ...</instrs>
254254
<regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) xorWord readReg(REGS, RS2)) </regs>
255255
```
256+
`MUL` gives the lowest `XLEN` bits after multiplication.
257+
```k
258+
rule <instrs> MUL RD , RS1 , RS2 => .K ...</instrs>
259+
<regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) *Word readReg(REGS, RS2)) </regs>
260+
```
261+
`MULU`, `MULHU`, `MULHSU` give the higher `XLEN` bits after multiplication, with signedness of the operands interpreted accordingly.
262+
```k
263+
rule <instrs> MULH RD , RS1 , RS2 => .K ...</instrs>
264+
<regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) *hWord readReg(REGS, RS2)) </regs>
265+
266+
rule <instrs> MULHU RD , RS1 , RS2 => .K ...</instrs>
267+
<regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) *huWord readReg(REGS, RS2)) </regs>
268+
269+
rule <instrs> MULHSU RD , RS1 , RS2 => .K ...</instrs>
270+
<regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) *hsuWord readReg(REGS, RS2)) </regs>
271+
```
256272
`SLL`, `SRL`, and `SRA` read their shift amount fom the lowest `log_2(XLEN)` bits of `RS2`.
257273
```k
258274
rule <instrs> SLL RD , RS1 , RS2 => .K ...</instrs>

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

+16
Original file line numberDiff line numberDiff line change
@@ -69,6 +69,22 @@ Note that two's complement enables us to use a single addition or subtraction op
6969
syntax Word ::= Word "-Word" Word [function, total]
7070
rule W(I1) -Word W(I2) => chop(I1 -Int I2)
7171
```
72+
The same is true for the `XLEN` least-significant bits of the result of multiplication.
73+
```k
74+
syntax Word ::= Word "*Word" Word [function, total, symbol(mulWord)]
75+
rule W(I1) *Word W(I2) => chop(I1 *Int I2)
76+
```
77+
The value of the upper `XLEN` bits however depends on signedness of the operands, as reflected by the followig functions.
78+
```k
79+
syntax Word ::= Word "*hWord" Word [function, total, symbol(mulhWord)]
80+
rule W1 *hWord W2 => chop((Word2SInt(W1) *Int Word2SInt(W2)) >>Int XLEN)
81+
82+
syntax Word ::= Word "*huWord" Word [function, total, symbol(mulhuWord)]
83+
rule W(I1) *huWord W(I2) => chop((I1 *Int I2) >>Int XLEN)
84+
85+
syntax Word ::= Word "*hsuWord" Word [function, total, symbol(mulhsuWord)]
86+
rule W1 *hsuWord W(I2) => chop((Word2SInt(W1) *Int I2) >>Int XLEN)
87+
```
7288
Above, the `chop` utility function
7389
```k
7490
syntax Word ::= chop(Int) [function, total]

‎src/tests/integration/test_functions.py

+111-15
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
from __future__ import annotations
22

3+
from itertools import count
34
from typing import TYPE_CHECKING
45

56
import pytest
@@ -20,6 +21,27 @@ def definition_dir() -> Path:
2021
return kdist.get('riscv-semantics.func-test')
2122

2223

24+
def _test_function(definition_dir: Path, app: Pattern, res: Pattern) -> None:
25+
# Given
26+
init = config(app)
27+
expected = config(res)
28+
29+
# When
30+
actual = llvm_interpret(definition_dir, init)
31+
32+
# Then
33+
assert actual == expected
34+
35+
36+
def config(kitem: Pattern) -> App:
37+
return generated_top(
38+
(
39+
k(kseq((kitem,))),
40+
generated_counter(int_dv(0)),
41+
),
42+
)
43+
44+
2345
def sw(rs2: int, imm: int, rs1: int) -> App:
2446
return App(
2547
'LblRegImmRegInstr',
@@ -49,26 +71,100 @@ def reg(x: int) -> App:
4971
ids=[test_id for test_id, *_ in DISASSEMBLE_TEST_DATA],
5072
)
5173
def test_disassemble(definition_dir: Path, test_id: str, code: bytes, sort: SortApp, pattern: Pattern) -> None:
52-
# Given
74+
def disassemble(n: int) -> App:
75+
return App('Lbldisassemble', (), (int_dv(n),))
76+
5377
n = int.from_bytes(code, byteorder='big')
54-
init = config(inj(SortApp('SortInstruction'), SORT_K_ITEM, disassemble(n)))
55-
expected = config(inj(sort, SORT_K_ITEM, pattern))
78+
app = inj(SortApp('SortInstruction'), SORT_K_ITEM, disassemble(n))
79+
res = inj(sort, SORT_K_ITEM, pattern)
80+
_test_function(definition_dir=definition_dir, app=app, res=res)
5681

57-
# When
58-
actual = llvm_interpret(definition_dir, init)
5982

60-
# Then
61-
assert actual == expected
83+
def is_32bit(x: int) -> bool:
84+
return 0 <= x < 0x100000000
6285

6386

64-
def config(kitem: Pattern) -> App:
65-
return generated_top(
66-
(
67-
k(kseq((kitem,))),
68-
generated_counter(int_dv(0)),
69-
),
87+
def chop(x: int) -> int:
88+
return x & 0xFFFFFFFF
89+
90+
91+
def signed(x: int) -> int:
92+
assert is_32bit(x)
93+
return x if x < 0x80000000 else x - 0x100000000
94+
95+
96+
MUL_TEST_DATA: Final = (
97+
(0, 0),
98+
(0, 1),
99+
(1, 0),
100+
(1, 1),
101+
(0xFFFFFFFF, 1),
102+
(0xFFFFFFFF, 12),
103+
(0xFFFFFFFF, 0xFFFFFFFF),
104+
(0xFFFF8765, 0xFFF01234),
105+
(0xFFFF8765, 12),
106+
)
107+
108+
109+
assert all(is_32bit(op1) and is_32bit(op2) for op1, op2 in MUL_TEST_DATA)
110+
111+
112+
def _test_mul(
113+
definition_dir: Path,
114+
symbol: str,
115+
op1: int,
116+
op2: int,
117+
res: int,
118+
) -> None:
119+
def w(x: int) -> App:
120+
return App('LblW', (), (int_dv(x),))
121+
122+
_test_function(
123+
definition_dir=definition_dir,
124+
app=inj(SortApp('SortWord'), SORT_K_ITEM, App(symbol, (), (w(op1), w(op2)))),
125+
res=inj(SortApp('SortWord'), SORT_K_ITEM, w(res)),
126+
)
127+
128+
129+
@pytest.mark.parametrize('op1,op2', MUL_TEST_DATA, ids=count())
130+
def test_mul(definition_dir: Path, op1: int, op2: int) -> None:
131+
_test_mul(
132+
definition_dir=definition_dir,
133+
symbol='LblmulWord',
134+
op1=op1,
135+
op2=op2,
136+
res=chop(op1 * op2),
137+
)
138+
139+
140+
@pytest.mark.parametrize('op1,op2', MUL_TEST_DATA, ids=count())
141+
def test_mulh(definition_dir: Path, op1: int, op2: int) -> None:
142+
_test_mul(
143+
definition_dir=definition_dir,
144+
symbol='LblmulhWord',
145+
op1=op1,
146+
op2=op2,
147+
res=chop((signed(op1) * signed(op2)) >> 32),
148+
)
149+
150+
151+
@pytest.mark.parametrize('op1,op2', MUL_TEST_DATA, ids=count())
152+
def test_mulhu(definition_dir: Path, op1: int, op2: int) -> None:
153+
_test_mul(
154+
definition_dir=definition_dir,
155+
symbol='LblmulhuWord',
156+
op1=op1,
157+
op2=op2,
158+
res=chop((op1 * op2) >> 32),
70159
)
71160

72161

73-
def disassemble(n: int) -> App:
74-
return App('Lbldisassemble', (), (int_dv(n),))
162+
@pytest.mark.parametrize('op1,op2', MUL_TEST_DATA, ids=count())
163+
def test_mulhsu(definition_dir: Path, op1: int, op2: int) -> None:
164+
_test_mul(
165+
definition_dir=definition_dir,
166+
symbol='LblmulhsuWord',
167+
op1=op1,
168+
op2=op2,
169+
res=chop((signed(op1) * op2) >> 32),
170+
)

0 commit comments

Comments
 (0)