Extend access type to cache accesses

model/riscv_insts_zaamo.sail

@@ -52,19 +52,19 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
   /* Get the address, X(rs1) (no offset).
     * Some extensions perform additional checks on address validity.
     */
-  match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width_bytes) {
+  match ext_data_get_addr(rs1, zeros(), AMOAccess(op, aq, rl, Data, Data), width_bytes) {
     Ext_DataAddr_Error(e)  => Ext_DataAddr_Check_Failure(e),
     Ext_DataAddr_OK(vaddr) => {
       if not(is_aligned_addr(bits_of(vaddr), width))
       then Memory_Exception(vaddr, E_SAMO_Addr_Align())
-      else match translateAddr(vaddr, ReadWrite(Data, Data)) {
+      else match translateAddr(vaddr, AMOAccess(op, aq, rl, Data, Data)) {
         Err(e, _) => Memory_Exception(vaddr, e),
         Ok(addr, _) => {
           let rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0];
           match mem_write_ea(addr, width_bytes, aq & rl, rl, true) {
             Err(e) => Memory_Exception(vaddr, e),
             Ok(_) => {
-              match mem_read(ReadWrite(Data, Data), addr, width_bytes, aq, aq & rl, true) {
+              match mem_read(AMOAccess(op, aq, rl, Data, Data), addr, width_bytes, aq, aq & rl, true) {
                 Err(e)     => Memory_Exception(vaddr, e),
                 Ok(loaded) => {
                   let result : bits('width_bytes * 8) =

model/riscv_insts_zalrsc.sail

@@ -40,8 +40,10 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
 
   // This is checked during decoding.
   assert(width_bytes <= xlen_bytes);
-
-  match vmem_read(rs1, zeros(), width_bytes, Read(Data), aq, aq & rl, true) {
+  /* TODO: The aq and rl patterns in Access Type is for not passing it into vmem_write etc.
+   * And may need to change the Access Type Read and Write.The same as StoreConditional.
+   */
+  match vmem_read(rs1, zeros(), width_bytes, LoadReserved(aq, rl, Data), aq, aq & rl, true) {
     Ok(data) => {
       X(rd) = sign_extend(data);
       RETIRE_SUCCESS
@@ -72,7 +74,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
    * RMEM: SC is allowed to succeed (but might fail later)
    */
   let data = X(rs2)[width_bytes * 8 - 1 .. 0];
-  match vmem_write(rs1, zeros(), width_bytes, data, Write(Data), aq & rl, rl, true) {
+  match vmem_write(rs1, zeros(), width_bytes, data, StoreConditional(aq, rl, Data), aq & rl, rl, true) {
     Ok(b) => {
       X(rd) = zero_extend(bool_bits(~(b)));
       cancel_reservation();

model/riscv_insts_zicbom.sail

@@ -31,6 +31,14 @@ mapping cbop_mnemonic : cbop_zicbom <-> string = {
   CBO_INVAL <-> "cbo.inval"
 }
 
+function cbop_to_access_type(cbop) : cbop_zicbom -> AccessType(ext_access_type) = {
+  match cbop {
+    CBO_CLEAN => Cache(CleanFlush),
+    CBO_FLUSH => Cache(CleanFlush),
+    CBO_INVAL => Cache(Inval),
+  }
+}
+
 mapping clause assembly = ZICBOM(cbop, rs1)
   <-> cbop_mnemonic(cbop) ^ spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"
 
@@ -67,6 +75,7 @@ val process_clean_inval : (regidx, cbop_zicbom) -> ExecutionResult
 function process_clean_inval(rs1, cbop) = {
   let rs1_val = X(rs1);
   let cache_block_size = 2 ^ plat_cache_block_size_exp;
+  let access_type = cbop_to_access_type(cbop);
 
   // Offset from rs1 to the beginning of the cache block. This is 0 if rs1
   // is aligned to the cache block, or negative if rs1 is misaligned.
@@ -75,10 +84,10 @@ function process_clean_inval(rs1, cbop) = {
   // TODO: This is incorrect since CHERI only requires at least one byte
   // to be in bounds here, whereas `ext_data_get_addr()` checks that all bytes
   // are in bounds. We will need to add a new function, parameter or access type.
-  match ext_data_get_addr(rs1, negative_offset, Read(Data), cache_block_size) {
+  match ext_data_get_addr(rs1, negative_offset, access_type, cache_block_size) {
     Ext_DataAddr_Error(e) => Ext_DataAddr_Check_Failure(e),
     Ext_DataAddr_OK(vaddr) => {
-      let res : option(ExceptionType) = match translateAddr(vaddr, Read(Data)) {
+      let res : option(ExceptionType) = match translateAddr(vaddr, access_type) {
         Ok(paddr, _) => {
           // "A cache-block management instruction is permitted to access the
           // specified cache block whenever a load instruction or store instruction

model/riscv_pmp_control.sail

@@ -14,8 +14,13 @@ function pmpCheckRWX(ent, acc) =
   match acc {
     Read(_)      => ent[R] == 0b1,
     Write(_)     => ent[W] == 0b1,
-    ReadWrite(_) => ent[R] == 0b1 & ent[W] == 0b1,
+    AMOAccess(_, _, _, _, _) => ent[R] == 0b1 & ent[W] == 0b1,
+    LoadReserved(_, _, _) => ent[R] == 0b1,
+    StoreConditional(_, _, _) => ent[W] == 0b1,
     InstructionFetch() => ent[X] == 0b1,
+    Cache(Zero)     => ent[W] == 0b1,
+    Cache(_)        => internal_error(__FILE__, __LINE__,
+                                      "Invalid CacheAccessType; Inval, Clean and Flush check Read/Write permissions."),
   }
 
 
@@ -85,8 +90,11 @@ function accessToFault(acc : AccessType(ext_access_type)) -> ExceptionType =
   match acc {
     Read(_)      => E_Load_Access_Fault(),
     Write(_)     => E_SAMO_Access_Fault(),
-    ReadWrite(_) => E_SAMO_Access_Fault(),
+    AMOAccess(_, _, _, _, _) => E_SAMO_Access_Fault(),
+    LoadReserved(_, _, _) => E_Load_Access_Fault(),
+    StoreConditional(_, _, _) => E_SAMO_Access_Fault(),
     InstructionFetch() => E_Fetch_Access_Fault(),
+    Cache(_)     => E_SAMO_Access_Fault(),
   }
 
 function pmpCheck forall 'n, 0 < 'n <= max_mem_access . (

model/riscv_types.sail

@@ -76,15 +76,6 @@ function privLevel_to_str (p : Privilege) -> string =
 
 overload to_str = {privLevel_to_str}
 
-/* memory access types */
-
-union AccessType ('a : Type) = {
-  Read      : 'a,
-  Write     : 'a,
-  ReadWrite : ('a, 'a),
-  InstructionFetch : unit
-}
-
 enum word_width = {BYTE, HALF, WORD, DOUBLE}
 
 type is_mem_width('w) = 'w in {1, 2, 4, 8}
@@ -335,3 +326,21 @@ struct mul_op = {
   signed_rs1 : bool,
   signed_rs2 : bool
 }
+
+/* memory access types */
+
+enum CacheAccessType = {
+  CleanFlush,
+  Inval,
+  Zero,
+}
+
+union AccessType ('a : Type) = {
+  Read      : 'a,
+  Write     : 'a,
+  AMOAccess       : (amoop, bool, bool, 'a, 'a),
+  LoadReserved     : (bool, bool, 'a),
+  StoreConditional : (bool, bool, 'a),
+  InstructionFetch : unit,
+  Cache     : CacheAccessType,
+}

model/riscv_vmem_pte.sail

@@ -112,23 +112,41 @@ function check_PTE_permission(ac        : AccessType(ext_access_type),
     match (ac, priv) {
       // Steps 6 and 8 of VATP, roughly (see riscv_vmem.sail).
       // (TODO: Step 7 awaits shadow stack implementation (Zicfiss).)
-      (Read(_),         User)       => (pte_U == 0b1)
+      (Read(_), User)                => (pte_U == 0b1)
                                        & ((pte_R == 0b1)
-                                          | ((pte_X == 0b1 & mxr))),
-      (Write(_),        User)       => (pte_U == 0b1) & (pte_W == 0b1),
-      (ReadWrite(_, _), User)       => (pte_U == 0b1)
+                                       | ((pte_X == 0b1 & mxr))),
+      (Write(_), User)               => (pte_U == 0b1)
+                                       & (pte_W == 0b1),
+      (AMOAccess(_, _, _, _, _), User)       => (pte_U == 0b1)
                                        & (pte_W == 0b1)
                                        & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)),
-      (InstructionFetch(),    User) => (pte_U == 0b1) & (pte_X == 0b1),
-      (Read(_),         Supervisor) => ((pte_U == 0b0) | do_sum)
+      (LoadReserved(_, _, _), User)  => (pte_U == 0b1)
                                        & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)),
-      (Write(_),        Supervisor) => ((pte_U == 0b0) | do_sum)
+      (StoreConditional(_, _, _), User) => (pte_U == 0b1)
+                                       & (pte_W == 0b1),
+      (InstructionFetch(),    User) => (pte_U == 0b1) & (pte_X == 0b1),
+      (Cache(Zero),  User)       => (pte_U == 0b1) & (pte_W == 0b1),
+      (Cache(_),     User)       => internal_error(__FILE__, __LINE__,
+                                        "Invalid CacheAccessType; Inval, Clean and Flush check Read/Write permissions."),
+      (Read(_), Supervisor)         => ((pte_U == 0b0) | do_sum)
+                                       & ((pte_R == 0b1)
+                                       | ((pte_X == 0b1) & mxr)),
+      (Write(_), Supervisor)        => ((pte_U == 0b0) | do_sum)
                                        & (pte_W == 0b1),
-      (ReadWrite(_, _), Supervisor) => ((pte_U == 0b0) | do_sum)
+      (AMOAccess(_, _, _, _, _), Supervisor) => ((pte_U == 0b0) | do_sum)
                                        & (pte_W == 0b1)
                                        & ((pte_R == 0b1)
-                                          | ((pte_X == 0b1) & mxr)),
+                                       | ((pte_X == 0b1) & mxr)),
+      (LoadReserved(_, _, _), Supervisor) => ((pte_U == 0b0) | do_sum)
+                                       & ((pte_R == 0b1)
+                                       | ((pte_X == 0b1) & mxr)),
+      (StoreConditional(_, _, _), Supervisor) => ((pte_U == 0b0) | do_sum)
+                                        & (pte_W == 0b1),
       (InstructionFetch(),Supervisor) => (pte_U == 0b0) & (pte_X == 0b1),
+      (Cache(Zero),  Supervisor) => ((pte_U == 0b0) | do_sum)
+                                  & (pte_W == 0b1),
+      (Cache(_),     _)          => internal_error(__FILE__, __LINE__,
+                                        "Invalid CacheAccessType; Inval, Clean and Flush check Read/Write permissions."),
       (_,               Machine)    => internal_error(__FILE__, __LINE__,
                                                       "m-mode mem perm check")};
   if success then PTE_Check_Success(())
@@ -149,7 +167,10 @@ function update_PTE_Bits forall 'pte_size, 'pte_size in {32, 64} . (
                              InstructionFetch() => false,
                              Read(_)         => false,
                              Write(_)        => true,
-                             ReadWrite(_, _) => true
+                             AMOAccess(_, _, _, _, _) => true,
+                             LoadReserved(_, _, _) => false,
+                             StoreConditional(_, _, _) => true,
+                             Cache(_)        => false,
                            });
   // Update 'accessed'-bit?
   let update_a = (pte_flags[A] == 0b0);

model/riscv_vmem_ptw.sail

@@ -54,13 +54,19 @@ function translationException(a : AccessType(ext_access_type),
                              -> ExceptionType = {
   match (a, f) {
     (_, PTW_Ext_Error(e))        => E_Extension(ext_translate_exception(e)),
-    (ReadWrite(_), PTW_Access()) => E_SAMO_Access_Fault(),
-    (ReadWrite(_), _)            => E_SAMO_Page_Fault(),
+    (AMOAccess(_, _, _, _, _), PTW_Access()) => E_SAMO_Access_Fault(),
+    (AMOAccess(_, _, _, _, _), _)            => E_SAMO_Page_Fault(),
     (Read(_), PTW_Access())      => E_Load_Access_Fault(),
     (Read(_), _)                 => E_Load_Page_Fault(),
     (Write(_), PTW_Access())     => E_SAMO_Access_Fault(),
     (Write(_), _)                => E_SAMO_Page_Fault(),
+    (LoadReserved(_, _, _), PTW_Access()) => E_Load_Access_Fault(),
+    (LoadReserved(_, _, _), _)          => E_Load_Page_Fault(),
+    (StoreConditional(_, _, _), PTW_Access()) => E_SAMO_Access_Fault(),
+    (StoreConditional(_, _, _), _)        => E_SAMO_Page_Fault(),
     (InstructionFetch(), PTW_Access()) => E_Fetch_Access_Fault(),
-    (InstructionFetch(), _)            => E_Fetch_Page_Fault()
+    (InstructionFetch(), _)            => E_Fetch_Page_Fault(),
+    (Cache(_), PTW_Access())     => E_SAMO_Access_Fault(),
+    (Cache(_), _)                => E_SAMO_Page_Fault(),
   }
 }

model/riscv_vmem_types.sail

@@ -42,8 +42,11 @@ function accessType_to_str (a) =
   match (a) {
     Read(_)            => "R",
     Write(_)           => "W",
-    ReadWrite(_, _)    => "RW",
+    AMOAccess(_, _, _, _, _)    => "A",
     InstructionFetch() => "X",
+    Cache(_)           => "C",
+    LoadReserved(_, _, _) => "LR",
+    StoreConditional(_, _, _) => "SC",
   }
 
 overload to_str = {accessType_to_str}