diff --git a/model/riscv_insts_zicbom.sail b/model/riscv_insts_zicbom.sail index c659ee5fd..dcf82fa74 100644 --- a/model/riscv_insts_zicbom.sail +++ b/model/riscv_insts_zicbom.sail @@ -32,6 +32,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 = RISCV_ZICBOM(cbop, rs1) <-> cbop_mnemonic(cbop) ^ spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")" @@ -40,6 +48,7 @@ function process_clean_inval(rs1, cbop) = { let rs1_val = X(rs1); let cache_block_size_exp = plat_cache_block_size_exp(); let cache_block_size = 2 ^ 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. @@ -48,10 +57,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_handle_data_check_error(e); RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => { - let res : option(ExceptionType) = match translateAddr(vaddr, Read(Data)) { + let res : option(ExceptionType) = match translateAddr(vaddr, access_type) { TR_Address(paddr, _) => { // "A cache-block management instruction is permitted to access the // specified cache block whenever a load instruction or store instruction diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index 62cd060c0..e2640d69f 100644 --- a/model/riscv_pmp_control.sail +++ b/model/riscv_pmp_control.sail @@ -45,6 +45,7 @@ function pmpCheckRWX(ent, acc) = Write(_) => ent[W] == 0b1, ReadWrite(_) => ent[R] == 0b1 & ent[W] == 0b1, Execute() => ent[X] == 0b1, + Cache(_) => ent[R] == 0b1 & ent[W] == 0b1, } @@ -98,6 +99,7 @@ function accessToFault(acc : AccessType(ext_access_type)) -> ExceptionType = Write(_) => E_SAMO_Access_Fault(), ReadWrite(_) => E_SAMO_Access_Fault(), Execute() => E_Fetch_Access_Fault(), + Cache(_) => E_SAMO_Access_Fault(), } function pmpCheck forall 'n, 'n > 0. (addr: physaddr, width: int('n), acc: AccessType(ext_access_type), priv: Privilege) diff --git a/model/riscv_types.sail b/model/riscv_types.sail index c5ed7107f..7c2ad69d2 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -116,11 +116,18 @@ enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL} /* memory access types */ +enum CacheAccessType = { + CleanFlush, + Inval, + Zero, +} + union AccessType ('a : Type) = { Read : 'a, Write : 'a, ReadWrite : ('a, 'a), - Execute : unit + Execute : unit, + Cache : CacheAccessType, } enum word_width = {BYTE, HALF, WORD, DOUBLE} diff --git a/model/riscv_vmem_pte.sail b/model/riscv_vmem_pte.sail index ce5b19d7a..b22e53f86 100644 --- a/model/riscv_vmem_pte.sail +++ b/model/riscv_vmem_pte.sail @@ -118,6 +118,8 @@ function check_PTE_permission(ac : AccessType(ext_access_type), & (pte_W == 0b1) & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)), (Execute(), User) => (pte_U == 0b1) & (pte_X == 0b1), + (Cache(_), User) => (pte_U == 0b1) + & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)), (Read(_), Supervisor) => ((pte_U == 0b0) | do_sum) & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)), (Write(_), Supervisor) => ((pte_U == 0b0) | do_sum) @@ -127,6 +129,8 @@ function check_PTE_permission(ac : AccessType(ext_access_type), & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)), (Execute(), Supervisor) => (pte_U == 0b0) & (pte_X == 0b1), + (Cache(_), Supervisor) => ((pte_U == 0b0) | do_sum) + & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)), (_, Machine) => internal_error(__FILE__, __LINE__, "m-mode mem perm check")}; if success then PTE_Check_Success(()) @@ -147,7 +151,8 @@ function update_PTE_Bits forall 'pte_size, 'pte_size in {32, 64} . ( Execute() => false, Read(_) => false, Write(_) => true, - ReadWrite(_, _) => true + ReadWrite(_, _) => true, + Cache(_) => false, }); // Update 'accessed'-bit? let update_a = (pte_flags[A] == 0b0); diff --git a/model/riscv_vmem_ptw.sail b/model/riscv_vmem_ptw.sail index ab73b1909..175a26e98 100644 --- a/model/riscv_vmem_ptw.sail +++ b/model/riscv_vmem_ptw.sail @@ -61,6 +61,8 @@ function translationException(a : AccessType(ext_access_type), (Write(_), PTW_Access()) => E_SAMO_Access_Fault(), (Write(_), _) => E_SAMO_Page_Fault(), (Execute(), PTW_Access()) => E_Fetch_Access_Fault(), - (Execute(), _) => E_Fetch_Page_Fault() + (Execute(), _) => E_Fetch_Page_Fault(), + (Cache(_), PTW_Access()) => E_SAMO_Access_Fault(), + (Cache(_), _) => E_SAMO_Page_Fault(), } } diff --git a/model/riscv_vmem_types.sail b/model/riscv_vmem_types.sail index d2808ac69..bad59b7d5 100644 --- a/model/riscv_vmem_types.sail +++ b/model/riscv_vmem_types.sail @@ -43,7 +43,8 @@ function accessType_to_str (a) = Read(_) => "R", Write(_) => "W", ReadWrite(_, _) => "RW", - Execute() => "X" + Execute() => "X", + Cache(_) => "C", } overload to_str = {accessType_to_str}