Added support for more CSR registers in RISC-V lifter and backlifter

kth-step · Dec 5, 2024 · 9a76df9 · 9a76df9
1 parent f922ca7
commit 9a76df9
Show file tree

Hide file tree

Showing 5 changed files with 192 additions and 37 deletions.
diff --git a/src/theory/tools/backlifter/bir_riscv_backlifterScript.sml b/src/theory/tools/backlifter/bir_riscv_backlifterScript.sml
@@ -410,16 +410,26 @@ End
 
 Definition default_riscv_bir_env_CSRS_def:
  default_riscv_bir_env_CSRS ms env_map =
-  ("MPRV"   =+ SOME (BVal_Imm (Imm8 (  w2w((ms.c_MCSR ms.procID).mstatus.MPRV)  ))))
+  ("mhartid"   =+ SOME (BVal_Imm (Imm64 ( ((ms.c_MCSR ms.procID).mhartid) ))))
+  (("MPRV"   =+ SOME (BVal_Imm (Imm8 (  w2w((ms.c_MCSR ms.procID).mstatus.MPRV)  ))))
   (("mscratch"   =+ SOME (BVal_Imm (Imm64 ( (ms.c_MCSR ms.procID).mscratch  ))))
-  env_map)
+  (("mepc"   =+ SOME (BVal_Imm (Imm64 ( (ms.c_MCSR ms.procID).mepc  ))))
+  (("mcause"   =+ SOME (BVal_Imm (Imm64 ( reg'mcause $ (ms.c_MCSR ms.procID).mcause  ))))
+  (("mtval"   =+ SOME (BVal_Imm (Imm64 ( (ms.c_MCSR ms.procID).mtval  ))))
+  (("mip"   =+ SOME (BVal_Imm (Imm64 ( reg'mip $ (ms.c_MCSR ms.procID).mip  ))))
+  env_map))))))
 End
 
 Definition default_riscv_bir_env_CSRS_tmp_def:
  default_riscv_bir_env_CSRS_tmp ms env_map =
-  ("tmp_MPRV"   =+ SOME (BVal_Imm (Imm8 (  w2w((ms.c_MCSR ms.procID).mstatus.MPRV)  ))))
+  ("tmp_mhartid"   =+ SOME (BVal_Imm (Imm64 ( ((ms.c_MCSR ms.procID).mhartid) ))))
+  (("tmp_MPRV"   =+ SOME (BVal_Imm (Imm8 (  w2w((ms.c_MCSR ms.procID).mstatus.MPRV)  ))))
   (("tmp_mscratch"   =+ SOME (BVal_Imm (Imm64 ( (ms.c_MCSR ms.procID).mscratch  ))))
-  env_map)
+  (("tmp_mepc"   =+ SOME (BVal_Imm (Imm64 ( (ms.c_MCSR ms.procID).mepc  ))))
+  (("tmp_mcause"   =+ SOME (BVal_Imm (Imm64 ( reg'mcause $ (ms.c_MCSR ms.procID).mcause  ))))
+  (("tmp_mtval"   =+ SOME (BVal_Imm (Imm64 ( (ms.c_MCSR ms.procID).mtval  ))))
+  (("tmp_mip"   =+ SOME (BVal_Imm (Imm64 ( reg'mip $ (ms.c_MCSR ms.procID).mip  ))))
+  env_map))))))
 End
 
 Definition default_riscv_bir_state_def:
@@ -1099,10 +1109,20 @@ QED
 
 Theorem default_riscv_bir_state_MCSRS_read[local]:
  !ms.
+  bir_env_read (BVar "mhartid" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
+   SOME (BVal_Imm (Imm64 (ms.c_MCSR ms.procID).mhartid)) /\
   bir_env_read (BVar "MPRV" (BType_Imm Bit8)) (default_riscv_bir_state ms).bst_environ =
    SOME (BVal_Imm (Imm8 (w2w (ms.c_MCSR ms.procID).mstatus.MPRV))) /\
   bir_env_read (BVar "mscratch" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
-   SOME (BVal_Imm (Imm64 (ms.c_MCSR ms.procID).mscratch))
+   SOME (BVal_Imm (Imm64 (ms.c_MCSR ms.procID).mscratch)) /\
+  bir_env_read (BVar "mepc" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
+   SOME (BVal_Imm (Imm64 (ms.c_MCSR ms.procID).mepc)) /\
+  bir_env_read (BVar "mcause" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
+   SOME (BVal_Imm (Imm64 $ reg'mcause (ms.c_MCSR ms.procID).mcause)) /\
+  bir_env_read (BVar "mtval" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
+   SOME (BVal_Imm (Imm64 (ms.c_MCSR ms.procID).mtval)) /\
+  bir_env_read (BVar "mip" (BType_Imm Bit64)) (default_riscv_bir_state ms).bst_environ =
+   SOME (BVal_Imm (Imm64 $ reg'mip  (ms.c_MCSR ms.procID).mip))
 Proof
   rw [default_riscv_bir_state_def,
       default_riscv_bir_env_CSRS_def,
@@ -1121,10 +1141,20 @@ QED
 
 Theorem default_riscv_bir_state_MCSRS_lookup_type[local]:
   !ms.
+  bir_env_lookup_type "mhartid" (default_riscv_bir_state ms).bst_environ =
+   SOME (bir_var_type (BVar "mhartid" (BType_Imm Bit64))) /\
   bir_env_lookup_type "MPRV" (default_riscv_bir_state ms).bst_environ =
-   SOME (bir_var_type (BVar "MPRV" (BType_Imm Bit8)))  /\
+   SOME (bir_var_type (BVar "MPRV" (BType_Imm Bit8))) /\
   bir_env_lookup_type "mscratch" (default_riscv_bir_state ms).bst_environ =
-   SOME (bir_var_type (BVar "mscratch" (BType_Imm Bit64)))
+   SOME (bir_var_type (BVar "mscratch" (BType_Imm Bit64))) /\
+  bir_env_lookup_type "mepc" (default_riscv_bir_state ms).bst_environ =
+   SOME (bir_var_type (BVar "mepc" (BType_Imm Bit64))) /\
+  bir_env_lookup_type "mcause" (default_riscv_bir_state ms).bst_environ =
+   SOME (bir_var_type (BVar "mcause" (BType_Imm Bit64))) /\
+  bir_env_lookup_type "mtval" (default_riscv_bir_state ms).bst_environ =
+   SOME (bir_var_type (BVar "mtval" (BType_Imm Bit64))) /\
+  bir_env_lookup_type "mip" (default_riscv_bir_state ms).bst_environ =
+   SOME (bir_var_type (BVar "mip" (BType_Imm Bit64)))
 Proof
   rw [default_riscv_bir_state_def,
       default_riscv_bir_env_CSRS_def,
@@ -1145,10 +1175,20 @@ QED
 
 Theorem default_riscv_bir_state_MCSRS_lookup_type_tmp[local]:
   !ms.
+  bir_env_lookup_type "tmp_mhartid" (default_riscv_bir_state ms).bst_environ =
+   SOME (bir_var_type (BVar "tmp_mhartid" (BType_Imm Bit64))) /\
   bir_env_lookup_type "tmp_MPRV" (default_riscv_bir_state ms).bst_environ =
-   SOME (bir_var_type (BVar "tmp_MPRV" (BType_Imm Bit8)))  /\
+   SOME (bir_var_type (BVar "tmp_MPRV" (BType_Imm Bit8))) /\
   bir_env_lookup_type "tmp_mscratch" (default_riscv_bir_state ms).bst_environ =
-   SOME (bir_var_type (BVar "tmp_mscratch" (BType_Imm Bit64)))
+   SOME (bir_var_type (BVar "tmp_mscratch" (BType_Imm Bit64))) /\
+  bir_env_lookup_type "tmp_mepc" (default_riscv_bir_state ms).bst_environ =
+   SOME (bir_var_type (BVar "tmp_mepc" (BType_Imm Bit64))) /\
+  bir_env_lookup_type "tmp_mcause" (default_riscv_bir_state ms).bst_environ =
+   SOME (bir_var_type (BVar "tmp_mcause" (BType_Imm Bit64))) /\
+  bir_env_lookup_type "tmp_mtval" (default_riscv_bir_state ms).bst_environ =
+   SOME (bir_var_type (BVar "tmp_mtval" (BType_Imm Bit64))) /\
+  bir_env_lookup_type "tmp_mip" (default_riscv_bir_state ms).bst_environ =
+   SOME (bir_var_type (BVar "tmp_mip" (BType_Imm Bit64)))
 Proof
   rw [default_riscv_bir_state_def,
       default_riscv_bir_env_CSRS_def,

diff --git a/src/theory/tools/lifter/bir_lifting_machinesScript.sml b/src/theory/tools/lifter/bir_lifting_machinesScript.sml
@@ -1029,13 +1029,28 @@ Theorem riscv_FPRS_lifted_imms_LIST_EVAL = EVAL ``riscv_FPRS_lifted_imms_LIST``
  * be represented as one immediate), we do so here as well. *)
 val riscv_sysregs_lifted_imms_LIST_def = Define `
   riscv_sysregs_lifted_imms_LIST = [
+    (BMLI (BVar "mhartid" (BType_Imm Bit64))
+          (\ms:riscv_state. Imm64 ((ms.c_MCSR ms.procID).mhartid))
+    );
     (* MPRV (from the mstatus register) is really a 2-bit value,
      * but is represented as an 8-bit immediate *)
     (BMLI (BVar "MPRV" (BType_Imm Bit8))
           (\ms:riscv_state. Imm8 (w2w((ms.c_MCSR ms.procID).mstatus.MPRV)))
     );
     (BMLI (BVar "mscratch" (BType_Imm Bit64))
           (\ms:riscv_state. Imm64 ((ms.c_MCSR ms.procID).mscratch))
+    );
+    (BMLI (BVar "mepc" (BType_Imm Bit64))
+          (\ms:riscv_state. Imm64 ((ms.c_MCSR ms.procID).mepc))
+    );
+    (BMLI (BVar "mcause" (BType_Imm Bit64))
+          (\ms:riscv_state. Imm64 $ reg'mcause ((ms.c_MCSR ms.procID).mcause))
+    );
+    (BMLI (BVar "mtval" (BType_Imm Bit64))
+          (\ms:riscv_state. Imm64 ((ms.c_MCSR ms.procID).mtval))
+    );
+    (BMLI (BVar "mip" (BType_Imm Bit64))
+          (\ms:riscv_state. Imm64 $ reg'mip ((ms.c_MCSR ms.procID).mip))
     )
   ]
 `;

diff --git a/src/tools/lifter/examples/Holmakefile b/src/tools/lifter/examples/Holmakefile
@@ -1,4 +1,4 @@
-INCLUDES = 
+INCLUDES = ..
 
 all: $(DEFAULT_TARGETS)
 .PHONY: all
diff --git a/src/tools/lifter/selftest_riscv.log b/src/tools/lifter/selftest_riscv.log
@@ -929,10 +929,10 @@ RV64 Zicsr Standard Extension
 
 CSRRW x1, mscratch(0x340), x2: 340110F3 @ 0x10030 - OK
  []
-|- bir_is_lifted_inst_prog riscv_bmr (Imm64 65584w) (WI_end 0w 16777216w)
-     (65584w,[243w; 16w; 1w; 52w])
+|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
+     (0x10030w,[243w; 16w; 1w; 52w])
      (BirProgram
-        [<|bb_label := BL_Address_HC (Imm64 65584w) "340110F3";
+        [<|bb_label := BL_Address_HC (Imm64 0x10030w) "340110F3";
            bb_statements :=
              [BStmt_Assert
                 (BExp_BinPred BIExp_Equal
@@ -943,14 +943,14 @@ CSRRW x1, mscratch(0x340), x2: 340110F3 @ 0x10030 - OK
               BStmt_Assign (BVar "mscratch" (BType_Imm Bit64))
                 (BExp_Den (BVar "x2" (BType_Imm Bit64)))];
            bb_last_statement :=
-             BStmt_Jmp (BLE_Label (BL_Address (Imm64 65588w)))|>])
+             BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
 
 CSRRS x1, mscratch(0x340), x2: 340120F3 @ 0x10030 - OK
  []
-|- bir_is_lifted_inst_prog riscv_bmr (Imm64 65584w) (WI_end 0w 16777216w)
-     (65584w,[243w; 32w; 1w; 52w])
+|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
+     (0x10030w,[243w; 32w; 1w; 52w])
      (BirProgram
-        [<|bb_label := BL_Address_HC (Imm64 65584w) "340120F3";
+        [<|bb_label := BL_Address_HC (Imm64 0x10030w) "340120F3";
            bb_statements :=
              [BStmt_Assert
                 (BExp_BinPred BIExp_Equal
@@ -963,14 +963,14 @@ CSRRS x1, mscratch(0x340), x2: 340120F3 @ 0x10030 - OK
                    (BExp_Den (BVar "mscratch" (BType_Imm Bit64)))
                    (BExp_Den (BVar "x2" (BType_Imm Bit64))))];
            bb_last_statement :=
-             BStmt_Jmp (BLE_Label (BL_Address (Imm64 65588w)))|>])
+             BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
 
 CSRRC x1, mscratch(0x340), x2: 340130F3 @ 0x10030 - OK
  []
-|- bir_is_lifted_inst_prog riscv_bmr (Imm64 65584w) (WI_end 0w 16777216w)
-     (65584w,[243w; 48w; 1w; 52w])
+|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
+     (0x10030w,[243w; 48w; 1w; 52w])
      (BirProgram
-        [<|bb_label := BL_Address_HC (Imm64 65584w) "340130F3";
+        [<|bb_label := BL_Address_HC (Imm64 0x10030w) "340130F3";
            bb_statements :=
              [BStmt_Assert
                 (BExp_BinPred BIExp_Equal
@@ -983,18 +983,18 @@ CSRRC x1, mscratch(0x340), x2: 340130F3 @ 0x10030 - OK
                    (BExp_Den (BVar "mscratch" (BType_Imm Bit64)))
                    (BExp_BinExp BIExp_Minus
                       (BExp_BinExp BIExp_Mult
-                         (BExp_Const (Imm64 18446744073709551615w))
+                         (BExp_Const (Imm64 0xFFFFFFFFFFFFFFFFw))
                          (BExp_Den (BVar "x2" (BType_Imm Bit64))))
                       (BExp_Const (Imm64 1w))))];
            bb_last_statement :=
-             BStmt_Jmp (BLE_Label (BL_Address (Imm64 65588w)))|>])
+             BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
 
 CSRRWI x1, mscratch(0x340), 0x1: 3400D0F3 @ 0x10030 - OK
  []
-|- bir_is_lifted_inst_prog riscv_bmr (Imm64 65584w) (WI_end 0w 16777216w)
-     (65584w,[243w; 208w; 0w; 52w])
+|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
+     (0x10030w,[243w; 208w; 0w; 52w])
      (BirProgram
-        [<|bb_label := BL_Address_HC (Imm64 65584w) "3400D0F3";
+        [<|bb_label := BL_Address_HC (Imm64 0x10030w) "3400D0F3";
            bb_statements :=
              [BStmt_Assert
                 (BExp_BinPred BIExp_Equal
@@ -1005,14 +1005,14 @@ CSRRWI x1, mscratch(0x340), 0x1: 3400D0F3 @ 0x10030 - OK
               BStmt_Assign (BVar "mscratch" (BType_Imm Bit64))
                 (BExp_Const (Imm64 1w))];
            bb_last_statement :=
-             BStmt_Jmp (BLE_Label (BL_Address (Imm64 65588w)))|>])
+             BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
 
 CSRRSI x1, mscratch(0x340), 0x1: 3400E0F3 @ 0x10030 - OK
  []
-|- bir_is_lifted_inst_prog riscv_bmr (Imm64 65584w) (WI_end 0w 16777216w)
-     (65584w,[243w; 224w; 0w; 52w])
+|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
+     (0x10030w,[243w; 224w; 0w; 52w])
      (BirProgram
-        [<|bb_label := BL_Address_HC (Imm64 65584w) "3400E0F3";
+        [<|bb_label := BL_Address_HC (Imm64 0x10030w) "3400E0F3";
            bb_statements :=
              [BStmt_Assert
                 (BExp_BinPred BIExp_Equal
@@ -1025,14 +1025,14 @@ CSRRSI x1, mscratch(0x340), 0x1: 3400E0F3 @ 0x10030 - OK
                    (BExp_Den (BVar "mscratch" (BType_Imm Bit64)))
                    (BExp_Const (Imm64 1w)))];
            bb_last_statement :=
-             BStmt_Jmp (BLE_Label (BL_Address (Imm64 65588w)))|>])
+             BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
 
 CSRRCI x1, mscratch(0x340), 0x1: 3400F0F3 @ 0x10030 - OK
  []
-|- bir_is_lifted_inst_prog riscv_bmr (Imm64 65584w) (WI_end 0w 16777216w)
-     (65584w,[243w; 240w; 0w; 52w])
+|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
+     (0x10030w,[243w; 240w; 0w; 52w])
      (BirProgram
-        [<|bb_label := BL_Address_HC (Imm64 65584w) "3400F0F3";
+        [<|bb_label := BL_Address_HC (Imm64 0x10030w) "3400F0F3";
            bb_statements :=
              [BStmt_Assert
                 (BExp_BinPred BIExp_Equal
@@ -1042,10 +1042,90 @@ CSRRCI x1, mscratch(0x340), 0x1: 3400F0F3 @ 0x10030 - OK
                 (BExp_Den (BVar "mscratch" (BType_Imm Bit64)));
               BStmt_Assign (BVar "mscratch" (BType_Imm Bit64))
                 (BExp_BinExp BIExp_And
-                   (BExp_Const (Imm64 18446744073709551614w))
+                   (BExp_Const (Imm64 0xFFFFFFFFFFFFFFFEw))
                    (BExp_Den (BVar "mscratch" (BType_Imm Bit64))))];
            bb_last_statement :=
-             BStmt_Jmp (BLE_Label (BL_Address (Imm64 65588w)))|>])
+             BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
+
+CSRR a2, mhartid(0xF14): F1402673 @ 0x10030 - OK
+ []
+|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
+     (0x10030w,[115w; 38w; 64w; 241w])
+     (BirProgram
+        [<|bb_label := BL_Address_HC (Imm64 0x10030w) "F1402673";
+           bb_statements :=
+             [BStmt_Assert
+                (BExp_BinPred BIExp_Equal
+                   (BExp_Den (BVar "MPRV" (BType_Imm Bit8)))
+                   (BExp_Const (Imm8 3w)));
+              BStmt_Assign (BVar "x12" (BType_Imm Bit64))
+                (BExp_Den (BVar "mhartid" (BType_Imm Bit64)))];
+           bb_last_statement :=
+             BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
+
+CSRR a5, mepc(0x341): 341027F3 @ 0x10030 - OK
+ []
+|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
+     (0x10030w,[243w; 39w; 16w; 52w])
+     (BirProgram
+        [<|bb_label := BL_Address_HC (Imm64 0x10030w) "341027F3";
+           bb_statements :=
+             [BStmt_Assert
+                (BExp_BinPred BIExp_Equal
+                   (BExp_Den (BVar "MPRV" (BType_Imm Bit8)))
+                   (BExp_Const (Imm8 3w)));
+              BStmt_Assign (BVar "x15" (BType_Imm Bit64))
+                (BExp_Den (BVar "mepc" (BType_Imm Bit64)))];
+           bb_last_statement :=
+             BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
+
+CSRR a5, mcause(0x342): 342027F3 @ 0x10030 - OK
+ []
+|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
+     (0x10030w,[243w; 39w; 32w; 52w])
+     (BirProgram
+        [<|bb_label := BL_Address_HC (Imm64 0x10030w) "342027F3";
+           bb_statements :=
+             [BStmt_Assert
+                (BExp_BinPred BIExp_Equal
+                   (BExp_Den (BVar "MPRV" (BType_Imm Bit8)))
+                   (BExp_Const (Imm8 3w)));
+              BStmt_Assign (BVar "x15" (BType_Imm Bit64))
+                (BExp_Den (BVar "mcause" (BType_Imm Bit64)))];
+           bb_last_statement :=
+             BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
+
+CSRR a5, mtval(0x343): 343027F3 @ 0x10030 - OK
+ []
+|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
+     (0x10030w,[243w; 39w; 48w; 52w])
+     (BirProgram
+        [<|bb_label := BL_Address_HC (Imm64 0x10030w) "343027F3";
+           bb_statements :=
+             [BStmt_Assert
+                (BExp_BinPred BIExp_Equal
+                   (BExp_Den (BVar "MPRV" (BType_Imm Bit8)))
+                   (BExp_Const (Imm8 3w)));
+              BStmt_Assign (BVar "x15" (BType_Imm Bit64))
+                (BExp_Den (BVar "mtval" (BType_Imm Bit64)))];
+           bb_last_statement :=
+             BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
+
+CSRR a5, mip(0x344): 344027F3 @ 0x10030 - OK
+ []
+|- bir_is_lifted_inst_prog riscv_bmr (Imm64 0x10030w) (WI_end 0w 0x1000000w)
+     (0x10030w,[243w; 39w; 64w; 52w])
+     (BirProgram
+        [<|bb_label := BL_Address_HC (Imm64 0x10030w) "344027F3";
+           bb_statements :=
+             [BStmt_Assert
+                (BExp_BinPred BIExp_Equal
+                   (BExp_Den (BVar "MPRV" (BType_Imm Bit8)))
+                   (BExp_Const (Imm8 3w)));
+              BStmt_Assign (BVar "x15" (BType_Imm Bit64))
+                (BExp_Den (BVar "mip" (BType_Imm Bit64)))];
+           bb_last_statement :=
+             BStmt_Jmp (BLE_Label (BL_Address (Imm64 0x10034w)))|>])
 
 
 RV64M Standard Extension (instructions inherited from RV32M)
@@ -1394,7 +1474,7 @@ REMUW x5, x6, x7: 027372BB @ 0x10030 - OK
 SUMMARY FAILING HEXCODES RISC-V
 
 
-Instructions FAILED: 4/72
+Instructions FAILED: 4/82
 
    "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
@@ -322,6 +322,26 @@ val _ = riscv_test_hex_print_asm "CSRRSI x1, mscratch(0x340), 0x1" "3400E0F3";
 (* CSRRCI x1, mscratch(0x340), 0x1 : 001101000000    00001 111 000011110011 *)
 val _ = riscv_test_hex_print_asm "CSRRCI x1, mscratch(0x340), 0x1" "3400F0F3";
 
+val _ = riscv_test_hex_print_asm "CSRR a2, mhartid(0xF14)" "F1402673";
+
+val _ = riscv_test_hex_print_asm "CSRR a5, mepc(0x341)" "341027F3";
+
+val _ = riscv_test_hex_print_asm "CSRR a5, mcause(0x342)" "342027F3";
+
+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)";
 val _ = print_msg "\n\n";