Implement LUI instruction

runtimeverification · Jul 15, 2024 · e297b6b · e297b6b
1 parent e781825
commit e297b6b
Show file tree

Hide file tree

Showing 5 changed files with 74 additions and 0 deletions.
diff --git a/src/kriscv/kdist/riscv-semantics/riscv.md b/src/kriscv/kdist/riscv-semantics/riscv.md
@@ -93,5 +93,9 @@ module RISCV
   rule <instrs> ADDI RD , RS , IMM => .K ...</instrs>
        <regs> REGS => writeReg(REGS, RD, chopAndExtend(readReg(REGS, RS) +Int IMM, XLEN())) </regs>
        <pc> PC => wrapAddr(PC +Int 4) </pc>
+
+  rule <instrs> LUI RD , IMM => .K ...</instrs>
+       <regs> REGS => writeReg(REGS, RD, chopAndExtend(IMM <<Int 12, XLEN())) </regs>
+       <pc> PC => wrapAddr(PC +Int 4) </pc>
 endmodule
 ```
diff --git a/tests/simple/addi-overflow.S b/tests/simple/addi-overflow.S
@@ -0,0 +1,13 @@
+.text
+.globl _start	
+_start:
+	lui x1, 0x7FFFF
+	addi x1, x1, 2047
+	addi x1, x1, 2047
+	addi x1, x1, 1
+	// x1 contains 2^31 - 1, the largest 32-bit two's complement integer.
+	// Setting x2 = x1 + 1 should overflow
+	addi x2, x1, 1
+.globl _halt
+_halt:
+	nop
diff --git a/tests/simple/addi-overflow.S.out b/tests/simple/addi-overflow.S.out
@@ -0,0 +1,24 @@
+<generatedTop>
+  <riscv>
+    <instrs>
+      .K
+    </instrs>
+    <mem>
+      [ 65536 , 65644 ) r|-> b"\x7fELF\x01\x01\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02\x00\xf3\x00\x01\x00\x00\x00T\x00\x01\x004\x00\x00\x00\xd0\x01\x00\x00\x08\x00\x00\x004\x00 \x00\x01\x00(\x00\x05\x00\x04\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x01\x00l\x00\x00\x00l\x00\x00\x00\x05\x00\x00\x00\x00\x10\x00\x00\xb7\xf0\xff\x7f\x93\x80\xf0\x7f\x93\x80\xf0\x7f\x93\x80\x10\x00\x13\x81\x10\x00\x13\x00\x00\x00"
+    </mem>
+    <regs>
+      1 |-> 2147483647 2 |-> -2147483648
+    </regs>
+    <pc>
+      65640
+    </pc>
+  </riscv>
+  <test>
+    <halt>
+      ADDRESS ( 65640 )
+    </halt>
+  </test>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>
diff --git a/tests/simple/lui.S b/tests/simple/lui.S
@@ -0,0 +1,9 @@
+.text
+.globl _start	
+_start:
+	lui x0, 0x10
+	lui x1, 0x80000
+	lui x2, 0x70000
+.globl _halt
+_halt:
+	nop
diff --git a/tests/simple/lui.S.out b/tests/simple/lui.S.out
@@ -0,0 +1,24 @@
+<generatedTop>
+  <riscv>
+    <instrs>
+      .K
+    </instrs>
+    <mem>
+      [ 65536 , 65636 ) r|-> b"\x7fELF\x01\x01\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02\x00\xf3\x00\x01\x00\x00\x00T\x00\x01\x004\x00\x00\x00\xc8\x01\x00\x00\x08\x00\x00\x004\x00 \x00\x01\x00(\x00\x05\x00\x04\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x01\x00d\x00\x00\x00d\x00\x00\x00\x05\x00\x00\x00\x00\x10\x00\x007\x00\x01\x00\xb7\x00\x00\x807\x01\x00p\x13\x00\x00\x00"
+    </mem>
+    <regs>
+      1 |-> -2147483648 2 |-> 1879048192
+    </regs>
+    <pc>
+      65632
+    </pc>
+  </riscv>
+  <test>
+    <halt>
+      ADDRESS ( 65632 )
+    </halt>
+  </test>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>