Avoid ambiguity for Word expressions (#97)

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

Author: Stevengre

package/version

@@ -1 +1 @@
-0.1.73
+0.1.74

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.73"
+version = "0.1.74"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

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

@@ -197,15 +197,15 @@ We then provide rules to consume and execute each instruction from the top of th
 `SLLI`, `SRLI`, and `SRAI` perform logical left, logical right, and arithmetic right shifts respectively.
 ```k
   rule <instrs> SLLI RD , RS , SHAMT => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS) <<Word SHAMT) </regs>
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS) <<Word W(SHAMT)) </regs>
     requires 0 <=Int SHAMT
 
   rule <instrs> SRLI RD , RS , SHAMT => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS) >>lWord SHAMT) </regs>
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS) >>lWord W(SHAMT)) </regs>
     requires 0 <=Int SHAMT
 
   rule <instrs> SRAI RD , RS , SHAMT => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS) >>aWord SHAMT) </regs>
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS) >>aWord W(SHAMT)) </regs>
     requires 0 <=Int SHAMT
 ```
 `LUI` builds a 32-bit constant from the 20-bit immediate by setting the 12 least-significant bits to `0`, then sign extends to `XLEN` bits and places the result in register `RD`.
@@ -261,13 +261,13 @@ The following instructions behave analogously to their `I`-suffixed counterparts
 `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>
-       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) <<Word Word2UInt(readReg(REGS, RS2) &Word W(XLEN -Int 1))) </regs>
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) <<Word (readReg(REGS, RS2) &Word W(XLEN -Int 1))) </regs>
 
   rule <instrs> SRL RD , RS1 , RS2 => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) >>lWord Word2UInt(readReg(REGS, RS2) &Word W(XLEN -Int 1))) </regs>
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) >>lWord (readReg(REGS, RS2) &Word W(XLEN -Int 1))) </regs>
 
   rule <instrs> SRA RD , RS1 , RS2 => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) >>aWord Word2UInt(readReg(REGS, RS2) &Word W(XLEN -Int 1))) </regs>
+       <regs> REGS => writeReg(REGS, RD, readReg(REGS, RS1) >>aWord (readReg(REGS, RS2) &Word W(XLEN -Int 1))) </regs>
 ```
 `JAL` stores `PC + 4` in `RD`, then increments `PC` by `OFFSET`.
 ```k

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

@@ -61,28 +61,41 @@ The `s` prefix denotes a signed operation while `u` denotes an unsigned operatio
   syntax Bool ::= Word ">=uWord" Word [function, total]
   rule W(I1) >=uWord W(I2) => I1 >=Int I2
 ```
+To avoid syntax conflicts, we define the following syntax with `left` associativity and clear precedence over the bitwise operations.
+```k
+  syntax Word ::= left:
+                  Word "*Word"    Word [function, total, symbol(mulWord)]
+                | Word "*hWord"   Word [function, total, symbol(mulhWord)]
+                | Word "*huWord"  Word [function, total, symbol(mulhuWord)]
+                | Word "*hsuWord" Word [function, total, symbol(mulhsuWord)]
+                > left:
+                  Word "+Word"    Word [function, total, symbol(addWord)]
+                | Word "-Word"    Word [function, total, symbol(subWord)]
+                > left:
+                  Word ">>lWord"  Word [function, total, symbol(rshWord)]
+                | Word ">>aWord"  Word [function, total, symbol(ashWord)]
+                | Word "<<Word"   Word [function, total, symbol(lshWord)]
+                > left:
+                  Word "&Word"    Word [function, total, symbol(andWord)]
+                > left:
+                  Word "xorWord"  Word [function, total, symbol(xorWord)]
+                > left:
+                  Word "|Word"    Word [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
-  syntax Word ::= Word "+Word" Word [function, total]
   rule W(I1) +Word W(I2) => chop(I1 +Int I2)
-
-  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
@@ -92,18 +105,14 @@ Above, the `chop` utility function
 ```
 is used to zero-out all but the least-significant `XLEN`-bits in case of overflow.
 ```k
-  syntax Word ::= Word "&Word" Word [function, total]
   rule W(I1) &Word W(I2) => W(I1 &Int I2)
 
-  syntax Word ::= Word "|Word" Word [function, total]
   rule W(I1) |Word W(I2) => W(I1 |Int I2)
 
-  syntax Word ::= Word "xorWord" Word [function, total]
   rule W(I1) xorWord W(I2) => W(I1 xorInt I2)
 
-  syntax Word ::= Word "<<Word" Int [function, total]
-  rule W(I1) <<Word I2 => chop(I1 <<Int I2) requires 0 <=Int I2
-  rule _     <<Word I2 => W(0)              requires I2 <Int 0
+  rule W(I1) <<Word W(I2) => chop(I1 <<Int I2) requires 0 <=Int I2
+  rule _     <<Word W(I2) => W(0)              requires I2 <Int 0
 ```
 For right shifts, we provide both arithmetic and logical variants.
 
@@ -114,14 +123,12 @@ Counterintuitively, we use the arithmetic right shift operator `>>Int` for `Int`
 
 That is, for any `I:Int` underlying some `W(I):Word`, applying `>>Int` will always pad with `0`s, correctly implementing a logical right shift.
 ```k
-  syntax Word ::= Word ">>lWord" Int [function, total]
-  rule W(I1) >>lWord I2 => W(I1 >>Int I2) requires 0 <=Int I2
-  rule _     >>lWord I2 => W(0)           requires I2 <Int 0
+  rule W(I1) >>lWord W(I2) => W(I1 >>Int I2) requires 0 <=Int I2
+  rule _     >>lWord W(I2) => W(0)           requires I2 <Int 0
 ```
 To actually perform an arithmetic shift over `Word`, we first convert to an infinitely sign-extended `Int` of equal value using `Word2SInt`, ensuring `>>Int` will pad with `1`s for a negative `Word`. The final result will still be infinitely sign-extended, so we must `chop` it back to a `Word`.
 ```k
-  syntax Word ::= Word ">>aWord" Int [function, total]
-  rule W1 >>aWord I2 => chop(Word2SInt(W1) >>Int I2) requires 0 <=Int I2
-  rule _  >>aWord I2 => W(0)                         requires I2 <Int 0
+  rule W1 >>aWord W(I2) => chop(Word2SInt(W1) >>Int I2) requires 0 <=Int I2
+  rule _  >>aWord W(I2) => W(0)                         requires I2 <Int 0
 endmodule
 ```