|
| 1 | +/*=======================================================================================*/ |
| 2 | +/* This Sail RISC-V architecture model, comprising all files and */ |
| 3 | +/* directories except where otherwise noted is subject the BSD */ |
| 4 | +/* two-clause license in the LICENSE file. */ |
| 5 | +/* */ |
| 6 | +/* SPDX-License-Identifier: BSD-2-Clause */ |
| 7 | +/*=======================================================================================*/ |
| 8 | + |
| 9 | +// Cache Block Operations - Management |
| 10 | + |
| 11 | +function cbo_clean_flush_enabled(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBCFE][0], senvcfg[CBCFE][0]) |
| 12 | +function cbo_inval_enabled(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBIE][0], senvcfg[CBIE][0]) |
| 13 | +function cbo_inval_as_inval(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBIE][1], senvcfg[CBIE][1]) |
| 14 | + |
| 15 | +/* ****************************************************************** */ |
| 16 | +union clause ast = RISCV_ZICBOM : (cbop_zicbom, regidx) |
| 17 | + |
| 18 | +mapping encdec_cbop : cbop_zicbom <-> bits(12) = { |
| 19 | + CBO_CLEAN <-> 0b000000000001, |
| 20 | + CBO_FLUSH <-> 0b000000000010, |
| 21 | + CBO_INVAL <-> 0b000000000000, |
| 22 | +} |
| 23 | + |
| 24 | +mapping clause encdec = RISCV_ZICBOM(cbop, rs1) if haveZicbom() |
| 25 | + <-> encdec_cbop(cbop) @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 if haveZicbom() |
| 26 | + |
| 27 | +mapping cbop_mnemonic : cbop_zicbom <-> string = { |
| 28 | + CBO_CLEAN <-> "cbo.clean", |
| 29 | + CBO_FLUSH <-> "cbo.flush", |
| 30 | + CBO_INVAL <-> "cbo.inval" |
| 31 | +} |
| 32 | + |
| 33 | +mapping clause assembly = RISCV_ZICBOM(cbop, rs1) |
| 34 | + <-> cbop_mnemonic(cbop) ^ spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")" |
| 35 | + |
| 36 | +val process_clean_inval : (regidx, cbop_zicbom) -> Retired |
| 37 | +function process_clean_inval(rs1, cbop) = { |
| 38 | + let rs1_val = X(rs1); |
| 39 | + let cache_block_size_exp = plat_cache_block_size_exp(); |
| 40 | + let cache_block_size = 2 ^ cache_block_size_exp; |
| 41 | + |
| 42 | + // Offset from rs1 to the beginning of the cache block. This is 0 if rs1 |
| 43 | + // is aligned to the cache block, or negative if rs1 is misaligned. |
| 44 | + let offset = (rs1_val & ~(zero_extend(ones(cache_block_size_exp)))) - rs1_val; |
| 45 | + |
| 46 | + // TODO: This is incorrect since CHERI only requires at least one byte |
| 47 | + // to be in bounds here, whereas `ext_data_get_addr()` checks that all bytes |
| 48 | + // are in bounds. We will need to add a new function, parameter or access type. |
| 49 | + match ext_data_get_addr(rs1, offset, Read(Data), cache_block_size) { |
| 50 | + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, |
| 51 | + Ext_DataAddr_OK(vaddr) => { |
| 52 | + let res: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) { |
| 53 | + TR_Address(paddr, _) => { |
| 54 | + // "A cache-block management instruction is permitted to access the |
| 55 | + // specified cache block whenever a load instruction or store instruction |
| 56 | + // is permitted to access the corresponding physical addresses. If |
| 57 | + // neither a load instruction nor store instruction is permitted to |
| 58 | + // access the physical addresses, but an instruction fetch is permitted |
| 59 | + // to access the physical addresses, whether a cache-block management |
| 60 | + // instruction is permitted to access the cache block is UNSPECIFIED." |
| 61 | + // |
| 62 | + // In this implementation we currently don't allow access for fetches. |
| 63 | + let exc_read = phys_access_check(Read(Data), cur_privilege, paddr, cache_block_size); |
| 64 | + let exc_write = phys_access_check(Write(Data), cur_privilege, paddr, cache_block_size); |
| 65 | + match (exc_read, exc_write) { |
| 66 | + // Access is permitted if read OR write are allowed. If neither |
| 67 | + // are allowed then we always report a store exception. |
| 68 | + (Some(exc_read), Some(exc_write)) => Some(exc_write), |
| 69 | + _ => None(), |
| 70 | + } |
| 71 | + }, |
| 72 | + TR_Failure(e, _) => Some(e) |
| 73 | + }; |
| 74 | + // "If access to the cache block is not permitted, a cache-block management |
| 75 | + // instruction raises a store page fault or store guest-page fault exception |
| 76 | + // if address translation does not permit any access or raises a store access |
| 77 | + // fault exception otherwise." |
| 78 | + match res { |
| 79 | + // The model has no caches so there's no action required. |
| 80 | + None() => RETIRE_SUCCESS, |
| 81 | + Some(e) => { |
| 82 | + let e : ExceptionType = match e { |
| 83 | + E_Load_Access_Fault() => E_SAMO_Access_Fault(), |
| 84 | + E_SAMO_Access_Fault() => E_SAMO_Access_Fault(), |
| 85 | + E_Load_Page_Fault() => E_SAMO_Page_Fault(), |
| 86 | + E_SAMO_Page_Fault() => E_SAMO_Page_Fault(), |
| 87 | + // No other exceptions should be generated since we're not checking |
| 88 | + // for fetch access and it's can't be misaligned. |
| 89 | + _ => internal_error(__FILE__, __LINE__, "unexpected exception for cmo.clean/inval"), |
| 90 | + }; |
| 91 | + handle_mem_exception(vaddr, e); |
| 92 | + RETIRE_FAIL |
| 93 | + } |
| 94 | + } |
| 95 | + } |
| 96 | + } |
| 97 | +} |
| 98 | + |
| 99 | +function clause execute(RISCV_ZICBOM(cbop, rs1)) = |
| 100 | + match cbop { |
| 101 | + CBO_CLEAN if cbo_clean_flush_enabled(cur_privilege) => |
| 102 | + process_clean_inval(rs1, cbop), |
| 103 | + CBO_FLUSH if cbo_clean_flush_enabled(cur_privilege) => |
| 104 | + process_clean_inval(rs1, cbop), |
| 105 | + CBO_INVAL if cbo_inval_enabled(cur_privilege) => |
| 106 | + process_clean_inval(rs1, if cbo_inval_as_inval(cur_privilege) then CBO_INVAL else CBO_FLUSH), |
| 107 | + _ => { |
| 108 | + handle_illegal(); |
| 109 | + RETIRE_FAIL |
| 110 | + }, |
| 111 | + } |
0 commit comments