diff --git a/Makefile b/Makefile index 1f8c8320c..349e7194e 100644 --- a/Makefile +++ b/Makefile @@ -57,6 +57,8 @@ SAIL_DEFAULT_INST += riscv_insts_vext_mem.sail SAIL_DEFAULT_INST += riscv_insts_vext_mask.sail SAIL_DEFAULT_INST += riscv_insts_vext_vm.sail SAIL_DEFAULT_INST += riscv_insts_vext_red.sail +SAIL_DEFAULT_INST += riscv_insts_zicbom.sail +SAIL_DEFAULT_INST += riscv_insts_zicboz.sail SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 644cb1e8d..29266c224 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -112,6 +112,11 @@ mach_bits plat_rom_size(unit u) return rv_rom_size; } +mach_bits plat_cache_block_size_exp() +{ + return rv_cache_block_size_exp; +} + // Provides entropy for the scalar cryptography extension. mach_bits plat_get_16_random_bits(unit u) { diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 450a64eba..049f5a47e 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -26,6 +26,8 @@ bool within_phys_mem(mach_bits, sail_int); mach_bits plat_rom_base(unit); mach_bits plat_rom_size(unit); +mach_bits plat_cache_block_size_exp(unit); + // Provides entropy for the scalar cryptography extension. mach_bits plat_get_16_random_bits(unit); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index cad634ef2..a25c0df26 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -27,6 +27,9 @@ uint64_t rv_ram_size = UINT64_C(0x4000000); uint64_t rv_rom_base = UINT64_C(0x1000); uint64_t rv_rom_size = UINT64_C(0x100); +// Default 64, which is mandated by RVA22. +uint64_t rv_cache_block_size_exp = UINT64_C(6); + // Provides entropy for the scalar cryptography extension. uint64_t rv_16_random_bits(void) { diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index 111090d39..558a20bc5 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -31,6 +31,8 @@ extern uint64_t rv_ram_size; extern uint64_t rv_rom_base; extern uint64_t rv_rom_size; +extern uint64_t rv_cache_block_size_exp; + // Provides entropy for the scalar cryptography extension. extern uint64_t rv_16_random_bits(void); diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 913543144..9213e3cda 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -56,6 +56,7 @@ enum { OPT_PMP_GRAIN, OPT_ENABLE_SVINVAL, OPT_ENABLE_ZCB, + OPT_CACHE_BLOCK_SIZE, }; static bool do_dump_dts = false; @@ -154,6 +155,7 @@ static struct option options[] = { #ifdef SAILCOV {"sailcov-file", required_argument, 0, 'c' }, #endif + {"cache-block-size", required_argument, 0, OPT_CACHE_BLOCK_SIZE }, {0, 0, 0, 0 } }; @@ -234,6 +236,17 @@ static void read_dtb(const char *path) fprintf(stdout, "Read %zd bytes of DTB from %s.\n", dtb_len, path); } +// Return log2(x), or -1 if x is not a power of 2. +static int ilog2(uint64_t x) +{ + for (unsigned i = 0; i < sizeof(x) * 8; ++i) { + if ((1ull << i) == x) { + return i; + } + } + return -1; +} + /** * Parses the command line arguments and returns the argv index for the first * ELF file that should be loaded. As getopt transforms the argv array, all @@ -247,6 +260,7 @@ static int process_args(int argc, char **argv) uint64_t ram_size = 0; uint64_t pmp_count = 0; uint64_t pmp_grain = 0; + uint64_t block_size_exp = 0; while (true) { c = getopt_long(argc, argv, "a" @@ -414,6 +428,17 @@ static int process_args(int argc, char **argv) case OPT_TRACE_OUTPUT: trace_log_path = optarg; fprintf(stderr, "using %s for trace output.\n", trace_log_path); + case OPT_CACHE_BLOCK_SIZE: + block_size_exp = ilog2(atol(optarg)); + + if (block_size_exp < 0 || block_size_exp > 12) { + fprintf(stderr, "invalid cache-block-size '%s' provided.\n", optarg); + exit(1); + } + + fprintf(stderr, "setting cache-block-size to 2^%" PRIu64 " = %u B\n", + block_size_exp, 1 << block_size_exp); + rv_cache_block_size_exp = block_size_exp; break; case '?': print_usage(argv[0], 1); diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 4bc330020..245a7fe80 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -193,6 +193,10 @@ val plat_rom_size : unit -> bitvector let plat_rom_size () = [] declare ocaml target_rep function plat_rom_size = `Platform.rom_size` +val plat_cache_block_size_exp : unit -> bitvector +let plat_cache_block_size_exp () = [] +declare ocaml target_rep function plat_cache_block_size_exp = `Platform.cache_block_size_exp` + val plat_clint_base : unit -> bitvector let plat_clint_base () = [] declare ocaml target_rep function plat_clint_base = `Platform.clint_base` diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index d1139081d..5ffe482cd 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -173,6 +173,10 @@ val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a let plat_rom_size () = wordFromInteger 0 declare ocaml target_rep function plat_rom_size = `Platform.rom_size` +val plat_cache_block_size_exp : unit -> integer +let plat_cache_block_size_exp () = wordFromInteger 0 +declare ocaml target_rep function plat_cache_block_size_exp = `Platform.cache_block_size_exp` + val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_clint_base () = wordFromInteger 0 declare ocaml target_rep function plat_clint_base = `Platform.clint_base` diff --git a/model/riscv_insts_zicbom.sail b/model/riscv_insts_zicbom.sail new file mode 100644 index 000000000..b865bc252 --- /dev/null +++ b/model/riscv_insts_zicbom.sail @@ -0,0 +1,111 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +// Cache Block Operations - Management + +function cbo_clean_flush_enabled(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBCFE][0], senvcfg[CBCFE][0]) +function cbo_inval_enabled(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBIE][0], senvcfg[CBIE][0]) +function cbo_inval_as_inval(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBIE][1], senvcfg[CBIE][1]) + +/* ****************************************************************** */ +union clause ast = RISCV_ZICBOM : (cbop_zicbom, regidx) + +mapping encdec_cbop : cbop_zicbom <-> bits(12) = { + CBO_CLEAN <-> 0b000000000001, + CBO_FLUSH <-> 0b000000000010, + CBO_INVAL <-> 0b000000000000, +} + +mapping clause encdec = RISCV_ZICBOM(cbop, rs1) if haveZicbom() + <-> encdec_cbop(cbop) @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 if haveZicbom() + +mapping cbop_mnemonic : cbop_zicbom <-> string = { + CBO_CLEAN <-> "cbo.clean", + CBO_FLUSH <-> "cbo.flush", + CBO_INVAL <-> "cbo.inval" +} + +mapping clause assembly = RISCV_ZICBOM(cbop, rs1) + <-> cbop_mnemonic(cbop) ^ spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")" + +val process_clean_inval : (regidx, cbop_zicbom) -> Retired +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; + + // 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. + let offset = (rs1_val & ~(zero_extend(ones(cache_block_size_exp)))) - rs1_val; + + // 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, offset, Read(Data), 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)) { + TR_Address(paddr, _) => { + // "A cache-block management instruction is permitted to access the + // specified cache block whenever a load instruction or store instruction + // is permitted to access the corresponding physical addresses. If + // neither a load instruction nor store instruction is permitted to + // access the physical addresses, but an instruction fetch is permitted + // to access the physical addresses, whether a cache-block management + // instruction is permitted to access the cache block is UNSPECIFIED." + // + // In this implementation we currently don't allow access for fetches. + let exc_read = phys_access_check(Read(Data), cur_privilege, paddr, cache_block_size); + let exc_write = phys_access_check(Write(Data), cur_privilege, paddr, cache_block_size); + match (exc_read, exc_write) { + // Access is permitted if read OR write are allowed. If neither + // are allowed then we always report a store exception. + (Some(exc_read), Some(exc_write)) => Some(exc_write), + _ => None(), + } + }, + TR_Failure(e, _) => Some(e) + }; + // "If access to the cache block is not permitted, a cache-block management + // instruction raises a store page fault or store guest-page fault exception + // if address translation does not permit any access or raises a store access + // fault exception otherwise." + match res { + // The model has no caches so there's no action required. + None() => RETIRE_SUCCESS, + Some(e) => { + let e : ExceptionType = match e { + E_Load_Access_Fault() => E_SAMO_Access_Fault(), + E_SAMO_Access_Fault() => E_SAMO_Access_Fault(), + E_Load_Page_Fault() => E_SAMO_Page_Fault(), + E_SAMO_Page_Fault() => E_SAMO_Page_Fault(), + // No other exceptions should be generated since we're not checking + // for fetch access and it's can't be misaligned. + _ => internal_error(__FILE__, __LINE__, "unexpected exception for cmo.clean/inval"), + }; + handle_mem_exception(vaddr, e); + RETIRE_FAIL + } + } + } + } +} + +function clause execute(RISCV_ZICBOM(cbop, rs1)) = + match cbop { + CBO_CLEAN if cbo_clean_flush_enabled(cur_privilege) => + process_clean_inval(rs1, cbop), + CBO_FLUSH if cbo_clean_flush_enabled(cur_privilege) => + process_clean_inval(rs1, cbop), + CBO_INVAL if cbo_inval_enabled(cur_privilege) => + process_clean_inval(rs1, if cbo_inval_as_inval(cur_privilege) then CBO_INVAL else CBO_FLUSH), + _ => { + handle_illegal(); + RETIRE_FAIL + }, + } diff --git a/model/riscv_insts_zicboz.sail b/model/riscv_insts_zicboz.sail new file mode 100644 index 000000000..d2aeb24cf --- /dev/null +++ b/model/riscv_insts_zicboz.sail @@ -0,0 +1,64 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +// Cache Block Operations - Zero + +function cbo_zero_enabled(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBZE][0], senvcfg[CBZE][0]) + +/* ****************************************************************** */ +union clause ast = RISCV_ZICBOZ : (regidx) + +mapping clause encdec = RISCV_ZICBOZ(rs1) if haveZicboz() + <-> 0b000000000100 @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 if haveZicboz() + +mapping clause assembly = RISCV_ZICBOZ(rs1) + <-> "cbo.zero" ^ spc() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")" + +function clause execute(RISCV_ZICBOZ(rs1)) = { + if cbo_zero_enabled(cur_privilege) then { + let rs1_val = X(rs1); + let cache_block_size_exp = plat_cache_block_size_exp(); + let cache_block_size = 2 ^ cache_block_size_exp; + + // 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. + let offset = (rs1_val & ~(zero_extend(ones(cache_block_size_exp)))) - rs1_val; + + // TODO: This is not correct since CHERI treats CBO operations + // differently to normal accesses with respect to bounds checks. + match ext_data_get_addr(rs1, offset, Write(Data), cache_block_size) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => { + // "An implementation may update the bytes in any order and with any granularity + // and atomicity, including individual bytes." + // + // This implementation does a single atomic write. + match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, cache_block_size, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemValue(_) => { + let res : MemoryOpResult(bool) = mem_write_value(paddr, cache_block_size, zeros(), false, false, false); + match (res) { + MemValue(true) => RETIRE_SUCCESS, + MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + } + } + } + } + } + }, + } + } else { + handle_illegal(); + RETIRE_FAIL + } +} diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 6c64b5928..1bfb2548a 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -26,6 +26,11 @@ val elf_entry = { c: "elf_entry" } : unit -> int +// Cache block size is 2^cache_block_size_exp. Max is `max_mem_access` (4096) +// because this model performs `cbo.zero` with a single write, and the behaviour +// with cache blocks larger than a page is not clearly defined. +val plat_cache_block_size_exp = {c: "plat_cache_block_size_exp", ocaml: "Platform.cache_block_size_exp", interpreter: "Platform.cache_block_size_exp", lem: "plat_cache_block_size_exp"} : unit -> range(0, 12) + /* Main memory */ val plat_ram_base = {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits val plat_ram_size = {c: "plat_ram_size", ocaml: "Platform.dram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 5bf2ce90d..881ad368b 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -101,6 +101,14 @@ function check_CSR_access(csrrw, csrpr, p, isWrite) = function check_TVM_SATP(csr : csreg, p : Privilege) -> bool = not(csr == 0x180 & p == Supervisor & mstatus[TVM] == 0b1) +// There are several features that are controlled by machine/supervisor enable +// bits (m/senvcfg, m/scounteren, etc.). This abstracts that logic. +function feature_enabled_for_priv(p : Privilege, machine_enable_bit : bit, supervisor_enable_bit : bit) -> bool = match p { + Machine => true, + Supervisor => machine_enable_bit == bitone, + User => machine_enable_bit == bitone & (not(haveSupMode()) | supervisor_enable_bit == bitone), +} + function check_Counteren(csr : csreg, p : Privilege) -> bool = match(csr, p) { (0xC00, Supervisor) => mcounteren[CY] == 0b1, diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 6eb174189..3ccaa5c8f 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -108,6 +108,14 @@ val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: " /* whether misa.b was enabled at boot */ val sys_enable_bext = {c: "sys_enable_bext", ocaml: "Platform.enable_bext", _: "sys_enable_bext"} : unit -> bool +// CBO extensions. Zicbop cannot be enabled/disabled because it has no effect +// at all on this model. +// TODO: Add command line flags. +// val sys_enable_zicbom = {c: "sys_enable_zicbom", ocaml: "Platform.enable_zicbom", _: "sys_enable_zicbom"} : unit -> bool +// val sys_enable_zicboz = {c: "sys_enable_zicboz", ocaml: "Platform.enable_zicboz", _: "sys_enable_zicboz"} : unit -> bool +function sys_enable_zicbom() -> bool = true +function sys_enable_zicboz() -> bool = true + /* This function allows an extension to veto a write to Misa if it would violate an alignment restriction on unsetting C. If it returns true the write will have no effect. */ @@ -175,6 +183,10 @@ function haveZicond() -> bool = true /* Zabha extension support */ function haveZabha() -> bool = true +/* Cache Management Operations extension support. */ +function haveZicbom() -> bool = sys_enable_zicbom() +function haveZicboz() -> bool = sys_enable_zicboz() + /* * Illegal values legalized to least privileged mode supported. * Note: the only valid combinations of supported modes are M, M+U, M+S+U. diff --git a/model/riscv_types.sail b/model/riscv_types.sail index f6e2d1ced..8b09ea417 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -335,6 +335,8 @@ enum amoop = {AMOSWAP, AMOADD, AMOXOR, AMOAND, AMOOR, AMOMIN, AMOMAX, AMOMINU, AMOMAXU} /* AMO ops */ enum csrop = {CSRRW, CSRRS, CSRRC} /* CSR ops */ +enum cbop_zicbom = {CBO_CLEAN, CBO_FLUSH, CBO_INVAL} /* Zicbom ops */ + enum brop_zba = {RISCV_SH1ADD, RISCV_SH2ADD, RISCV_SH3ADD} enum brop_zbb = {RISCV_ANDN, RISCV_ORN, RISCV_XNOR, RISCV_MAX, diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index d10029a8b..ad96cb92f 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -105,6 +105,8 @@ let rom_size () = arch_bits_of_int !rom_size_ref let dram_base () = arch_bits_of_int64 P.dram_base let dram_size () = arch_bits_of_int64 !P.dram_size_ref +let cache_block_size_exp () = Big_int.of_int64 !P.cache_block_size_exp_ref + let clint_base () = arch_bits_of_int64 P.clint_base let clint_size () = arch_bits_of_int64 P.clint_size diff --git a/ocaml_emulator/platform_impl.ml b/ocaml_emulator/platform_impl.ml index 39de43776..2732d9468 100644 --- a/ocaml_emulator/platform_impl.ml +++ b/ocaml_emulator/platform_impl.ml @@ -57,6 +57,9 @@ let rom_base = 0x00001000L;; (* Spike::DEFAULT_RSTVEC *) let dram_size_ref = ref (Int64.(shift_left 64L 20)) +(* Default 64, which is mandated by RVA22. *) +let cache_block_size_exp_ref = ref (Int64.(6L)) + type mem_region = { addr : Int64.t; size : Int64.t @@ -144,6 +147,20 @@ let set_dtc path = let set_dram_size mb = dram_size_ref := Int64.(shift_left (Int64.of_int mb) 20) +(* Calculate x=log2(n) and return Some(x) if n is a power of 2, otherwise None. *) +let log2 n = + let rec loop i = + if i >= Sys.int_size - 1 then None + else if (1 lsl i) = n then Some i + else loop (i + 1) + in + if n <= 0 then None else loop 0 + +let set_cache_block_size b = + match log2 b with + | Some(block_size_exp) -> cache_block_size_exp_ref := Int64.(Int64.of_int block_size_exp) + | None -> (Printf.eprintf "Invalid cache block size provided."; exit 1) + let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *) try let cmd = Printf.sprintf "%s -I dts" !dtc_path in diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index 344d1d272..ac7282062 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -77,6 +77,9 @@ let options = Arg.align ([("-dump-dts", ("-ram-size", Arg.Int PI.set_dram_size, " size of physical ram memory to use (in MB)"); + ("-cache-block-size", + Arg.Int PI.set_cache_block_size, + " cache block size of the cache block size (default 64; max 4096)"); ("-report-arch", Arg.Unit report_arch, " report model architecture (RV32 or RV64)");