Fixed typo in RISC-V step theory, updates to RISC-V selftest

kth-step · Jan 9, 2025 · 7342846 · 7342846
1 parent f51a82a
commit 7342846
Show file tree

Hide file tree

Showing 3 changed files with 36 additions and 13 deletions.
diff --git a/src/shared/l3-machine-code/riscv/step/riscv_stepScript.sml b/src/shared/l3-machine-code/riscv/step/riscv_stepScript.sml
@@ -835,6 +835,7 @@ in
   val () = utilsLib.reset_thms()
   fun class args avoid n =
     let
+      val is_csr = Lib.mem n ["CSRRW", "CSRRS", "CSRRC", "CSRRWI", "CSRRSI", "CSRRCI"]
       val name = "dfn'" ^ n
       val read = if Lib.mem n ["LD"] then [address_aligned3] else []
       val (write, n) =
@@ -844,7 +845,7 @@ in
           ([write'GPR], n)
       (* These rewrites should be done for all CSR instructions *)
       val csr =
-        if Lib.mem n ["CSRRW", "CSRRS", "CSRRC", "CSRRWI", "CSRRSI", "CSRRCI"]
+        if is_csr
         then [checkCSROp, check_CSR_access, CSR, privLevel, csrRW, csrPR]
         else []
       val thms = DB.fetch "riscv" (name ^ "_def") :: write @ read @ csr
@@ -948,14 +949,14 @@ val SW  = store [] "SW"
 val SH  = store [] "SH"
 val SB  = store [] "SB"
 
-val csrinst = class `(rd, rs1, csr)`
+val csrinst = class_rd0 `(rd, rs1, csr)`
 
 (* TODO: How to handle privilege level? Currently, machine mode is always assumed *)
 val CSRRW_M = csrinst [[``^privilege_level = 3w``, ``^archbase <> 0w``]] "CSRRW"
 val CSRRS_M = csrinst [[``^privilege_level = 3w``, ``^archbase <> 0w``]] "CSRRS"
 val CSRRC_M = csrinst [[``^privilege_level = 3w``, ``^archbase <> 0w``]] "CSRRC"
 
-val csrinsti = class `(rd, imm, csr)`
+val csrinsti = class_rd0 `(rd, imm, csr)`
 
 val CSRRWI_M = csrinsti [[``^privilege_level = 3w``, ``^archbase <> 0w``]] "CSRRWI"
 val CSRRSI_M = csrinsti [[``^privilege_level = 3w``, ``^archbase <> 0w``]] "CSRRSI"

diff --git a/src/tools/lifter/selftest_riscv.log b/src/tools/lifter/selftest_riscv.log
@@ -945,6 +945,34 @@ CSRRW x1, mscratch(0x340), x2: 340110F3 @ 0x10030 - OK
            bb_last_statement :=
              BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
 
+CSRW mie(0x304), 0: 30405073 @ 0x10030 - OK
+ []
+|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
+     (0x10030w,[115w; 80w; 64w; 48w])
+     (BirProgram
+        [<|bb_label := BL_Address_HC (Imm64 0x10030w) "30405073";
+           bb_statements :=
+             [BStmt_Assert
+                (BExp_BinPred BIExp_Equal
+                   (BExp_Den (BVar "MPRV" (BType_Imm Bit8)))
+                   (BExp_Const (Imm8 3w)))];
+           bb_last_statement :=
+             BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
+
+CSRW mstatus(0x300), 0: 30005073 @ 0x10030 - OK
+ []
+|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
+     (0x10030w,[115w; 80w; 0w; 48w])
+     (BirProgram
+        [<|bb_label := BL_Address_HC (Imm64 0x10030w) "30005073";
+           bb_statements :=
+             [BStmt_Assert
+                (BExp_BinPred BIExp_Equal
+                   (BExp_Den (BVar "MPRV" (BType_Imm Bit8)))
+                   (BExp_Const (Imm8 3w)))];
+           bb_last_statement :=
+             BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
+
 CSRRS x1, mscratch(0x340), x2: 340120F3 @ 0x10030 - OK
  []
 |- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
@@ -1474,7 +1502,7 @@ REMUW x5, x6, x7: 027372BB @ 0x10030 - OK
 SUMMARY FAILING HEXCODES RISC-V
 
 
-Instructions FAILED: 4/82
+Instructions FAILED: 4/84
 
    "0881008F" (* bmr_step_hex failed *),
    "00000073" (* bmr_step_hex failed *),

diff --git a/src/tools/lifter/selftest_riscv.sml b/src/tools/lifter/selftest_riscv.sml
@@ -311,6 +311,9 @@ val _ = print_msg "\n\n";
  * (see bottom of riscv_stepScript.sml) *)
 (* CSRRW x1, mscratch(0x340), x2 : 001101000000    00010 001000011110011 *)
 val _ = riscv_test_hex_print_asm "CSRRW x1, mscratch(0x340), x2" "340110F3";
+val _ = riscv_test_hex_print_asm "CSRW mie(0x304), 0" "30405073";
+val _ = riscv_test_hex_print_asm "CSRW mstatus(0x300), 0" "30005073";
+
 (* CSRRS x1, mscratch(0x340), x2 : 001101000000    00010 010000011110011 *)
 val _ = riscv_test_hex_print_asm "CSRRS x1, mscratch(0x340), x2" "340120F3";
 (* CSRRC x1, mscratch(0x340), x2 : 001101000000    00010 011000011110011 *)
@@ -332,15 +335,6 @@ val _ = riscv_test_hex_print_asm "CSRR a5, mtval(0x343)" "343027F3";
 
 val _ = riscv_test_hex_print_asm "CSRR a5, mip(0x344)" "344027F3";
 
-(* TODO: These fail in riscv_stepLib for some reason...
-
-val _ = riscv_test_hex_print_asm "CSRW mie(0x304), 0" "30405073";
-val _ = riscv_test_hex_print_asm "CSRW mstatus(0x300), 0" "30005073";
-
-open riscv_stepLib;
-val _ = riscv_step_hex "30405073";
-
-*)
 
 val _ = print_msg "\n";
 val _ = print_header "RV64M Standard Extension (instructions inherited from RV32M)";