Fix access checks to riscv CSRs.

3 files changed, 69 insertions, 26 deletions

diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index e5380bd2..0747d077 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -502,30 +502,6 @@ function clause decode csr : bits(12) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0
 function clause decode csr : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, true,  CSRRS))
 function clause decode csr : bits(12) @ rs1 : regbits @ 0b111 @ rd : regbits @ 0b1110011 = Some(CSR (csr, rs1, rd, true,  CSRRC))
 
-val isCSRImplemented : bits(12) -> bool
-function isCSRImplemented csr : bits(12) -> bool =
-  match csr {
-    0xf11 => true, // mvendorid
-    0xf12 => true, // marchdid
-    0xf13 => true, // mimpid
-    0xf14 => true, // mhartid
-    0x300 => true, // mstatus
-    0x301 => true, // misa
-    0x302 => true, // medeleg
-    0x303 => true, // mideleg
-    0x304 => true, // mie
-    0x305 => true, // mtvec
-    0x306 => true, // mcounteren
-    0x340 => true, // mscratch
-    0x341 => true, // mepc
-    0x342 => true, // mcause
-    0x343 => true, // mtval
-    0x344 => true, // mip
-
-    // for riscv-tests
-    0x180 => true, // satp
-    _     => false
-  }
 
 function readCSR csr: bits(12) -> xlenbits =
   match csr {
@@ -611,7 +587,7 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) =
     CSRRW  => true,
     _      => if is_imm then unsigned(rs1_val) != 0 else unsigned(rs1) != 0
   } in
-  if ~ (isCSRImplemented(csr) & haveCSRPriv(csr, isWrite)) then {
+  if ~ (check_CSR(csr, cur_privilege, isWrite)) then {
     let instr : xlenbits = EXTZ(__RISCV_read(PC, 4));
     let t : sync_exception =
     struct { trap = E_Illegal_Instr,
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index dfad6f51..b3ded01e 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -196,6 +196,67 @@ register scause : Mcause
 register stval : xlenbits
 register satp : xlenbits
 
+/* csr access control */
+
+function csrAccess(csr : csreg) -> csrRW = csr[11..10]
+function csrPriv(csr : csreg) -> priv_level = csr[9..8]
+
+function is_CSR_defined (csr : bits(12), p : Privilege) -> bool =
+  match (csr) {
+    /* machine mode: informational */
+    0xf11 => p == Machine, // mvendorid
+    0xf12 => p == Machine, // marchdid
+    0xf13 => p == Machine, // mimpid
+    0xf14 => p == Machine, // mhartid
+    /* machine mode: trap setup */
+    0x300 => p == Machine, // mstatus
+    0x301 => p == Machine, // misa
+    0x302 => p == Machine, // medeleg
+    0x303 => p == Machine, // mideleg
+    0x304 => p == Machine, // mie
+    0x305 => p == Machine, // mtvec
+    0x306 => p == Machine, // mcounteren
+    /* machine mode: trap handling */
+    0x340 => p == Machine, // mscratch
+    0x341 => p == Machine, // mepc
+    0x342 => p == Machine, // mcause
+    0x343 => p == Machine, // mtval
+    0x344 => p == Machine, // mip
+
+    /* supervisor mode: trap setup */
+    0x100 => p == Machine | p == Supervisor, // sstatus
+    0x102 => p == Machine | p == Supervisor, // sedeleg
+    0x103 => p == Machine | p == Supervisor, // sideleg
+    0x104 => p == Machine | p == Supervisor, // sie
+    0x105 => p == Machine | p == Supervisor, // stvec
+    0x106 => p == Machine | p == Supervisor, // scounteren
+
+    /* supervisor mode: trap handling */
+    0x140 => p == Machine | p == Supervisor, // sscratch
+    0x141 => p == Machine | p == Supervisor, // sepc
+    0x142 => p == Machine | p == Supervisor, // scause
+    0x143 => p == Machine | p == Supervisor, // stval
+    0x144 => p == Machine | p == Supervisor, // sip
+
+    /* supervisor mode: address translation */
+    0x180 => p == Machine | p == Supervisor, // satp
+
+    _     => false
+  }
+
+val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool
+function check_CSR_access(csrrw, csrpr, p, isWrite) =
+    (~ (isWrite == true & csrrw == 0b11))  /* read/write */
+  & (privLevel_to_bits(p) >=_u csrpr)      /* privilege */
+
+function check_TVM_SATP(csr : csreg, p : Privilege) -> bool =
+  ~ (csr == 0x180 & p == Supervisor & mstatus.TVM() == true)
+
+function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
+    is_CSR_defined(csr, p)
+  & check_CSR_access(csrAccess(csr), csrPriv(csr), p, isWrite)
+  & check_TVM_SATP(csr, p)
+
 /* instruction control flow */
 
 struct sync_exception = {
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index a858c317..f64eb5a9 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -9,6 +9,7 @@ let xlen_min_signed = 0 - 2 ^ (xlen - 1)
 type regno ('n : Int), 0 <= 'n < 32 = atom('n)
 type regbits = bits(5)
 type cregbits = bits(3)
+type csreg = bits(12)
 
 val cast regbits_to_regno : bits(5) -> {'n, 0 <= 'n < 32. regno('n)}
 function regbits_to_regno b = let 'r = unsigned(b) in r
@@ -55,7 +56,6 @@ enum Architecture = {RV32, RV64, RV128}
 /* privilege levels */
 
 type priv_level = bits(2)
-
 enum Privilege = {User, Supervisor, Machine}
 
 val cast privLevel_to_bits : Privilege -> priv_level
@@ -85,6 +85,10 @@ function privLevel_to_str (p) = {
   }
 }
 
+/* access types */
+enum AccessType = {Read, Write, ReadWrite, Execute}
+enum ReadType   = {Instruction, Data}
+
 /* architectural exception and interrupt definitions */
 
 type exc_code = bits(4)
@@ -323,6 +327,8 @@ val MEM_fence_r_r   = {ocaml: "skip", lem: "MEM_fence_r_r"}   : unit -> unit eff
 val MEM_fence_rw_w  = {ocaml: "skip", lem: "MEM_fence_rw_w"}  : unit -> unit effect {barr}
 val MEM_fence_w_w   = {ocaml: "skip", lem: "MEM_fence_w_w"}   : unit -> unit effect {barr}
 val MEM_fence_i     = {ocaml: "skip", lem: "MEM_fence_i"}     : unit -> unit effect {barr}
+/* CSR access control bits (from CSR addresses) */
+type csrRW = bits(2)  /* read/write */
 
 enum uop = {RISCV_LUI, RISCV_AUIPC} /* upper immediate ops */
 enum bop = {RISCV_BEQ, RISCV_BNE, RISCV_BLT, RISCV_BGE, RISCV_BLTU, RISCV_BGEU} /* branch ops */