From 0f53467512be36536b63a0eb1a944f95b13d8bb4 Mon Sep 17 00:00:00 2001 From: Ksenia Dobrovolskaya Date: Tue, 11 Jun 2024 14:48:28 +0300 Subject: [PATCH 1/2] Implementing callbacks in sail-riscv for state-changing events 1. Added callback functions for XRegs, FRegs, VRegs, PC, CSR, memory writes and CSR, memory reads. 2. Added implementation of callbacks for RVFI records in riscv_rvfi_callbacks.c. 3. Added default callback OCaml-implementations in the file platform.ml. --- Makefile | 33 +++++++++++++++-- c_emulator/riscv_default_callbacks.c | 16 +++++++++ c_emulator/riscv_rvfi_callbacks.c | 27 ++++++++++++++ c_emulator/riscv_sail.h | 16 +++++++++ model/prelude.sail | 3 -- model/riscv_csr_ext.sail | 15 ++++++++ model/riscv_fdext_regs.sail | 6 +--- model/riscv_insts_vext_mem.sail | 12 +++---- model/riscv_insts_vext_vset.sail | 45 ++++++++++------------- model/riscv_insts_zicsr.sail | 10 ++---- model/riscv_mem.sail | 53 ++++++---------------------- model/riscv_pc_access.sail | 1 + model/riscv_regs.sail | 14 +------- model/riscv_sys_control.sail | 22 ++++-------- model/riscv_types.sail | 22 ++++++++++++ model/riscv_vext_regs.sail | 3 +- model/riscv_vreg_type.sail | 5 +++ model/rvfi_dii.sail | 43 ++++++++++++++++++++++ ocaml_emulator/platform.ml | 11 ++++++ test/run_tests.sh | 0 20 files changed, 231 insertions(+), 126 deletions(-) create mode 100644 c_emulator/riscv_default_callbacks.c create mode 100644 c_emulator/riscv_rvfi_callbacks.c mode change 100755 => 100644 test/run_tests.sh diff --git a/Makefile b/Makefile index 268e36b9b..36c3ad7d1 100644 --- a/Makefile +++ b/Makefile @@ -267,11 +267,11 @@ c_preserve_fns=-c_preserve _set_Misa_C generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile mkdir -p generated_definitions/c - $(SAIL) $(SAIL_FLAGS) $(c_preserve_fns) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@) + $(SAIL) $(SAIL_FLAGS) $(c_preserve_fns) -O -Oconstant_fold -memo_z3 -c -c_include riscv_default_callbacks.c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@) generated_definitions/c2/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Makefile mkdir -p generated_definitions/c2 - $(SAIL) $(SAIL_FLAGS) -no_warn -memo_z3 -config c_emulator/config.json -c2 $(SAIL_SRCS) -o $(basename $@) + $(SAIL) $(SAIL_FLAGS) -no_warn -memo_z3 -config c_emulator/config.json -c2 -c_include riscv_default_callbacks.c $(SAIL_SRCS) -o $(basename $@) $(SOFTFLOAT_LIBS): $(MAKE) SPECIALIZE_TYPE=$(SOFTFLOAT_SPECIALIZE_TYPE) -C $(SOFTFLOAT_LIBDIR) @@ -313,6 +313,35 @@ generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile $(CC) -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ +# Note: We have to add -c_preserve since the functions might be optimized out otherwise +rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \ + -c_preserve rvfi_get_cmd \ + -c_preserve rvfi_get_insn \ + -c_preserve rvfi_get_v2_trace_size \ + -c_preserve rvfi_get_v2_support_packet \ + -c_preserve rvfi_get_exec_packet_v1 \ + -c_preserve rvfi_get_exec_packet_v2 \ + -c_preserve rvfi_get_mem_data \ + -c_preserve rvfi_get_int_data \ + -c_preserve rvfi_zero_exec_packet \ + -c_preserve rvfi_halt_exec_packet \ + -c_preserve rvfi_write \ + -c_preserve rvfi_read \ + -c_preserve rvfi_wX \ + -c_preserve print_rvfi_exec \ + -c_preserve print_instr_packet \ + -c_preserve print_rvfi_exec + +# sed -i isn't posix compliant, unfortunately +generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile + mkdir -p generated_definitions/c + $(SAIL) $(c_preserve_fns) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) -c_include riscv_rvfi_callbacks.c model/main.sail -o $(basename $@) + sed -e '/^[[:space:]]*$$/d' $@ > $@.new + mv $@.new $@ + +c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile + gcc -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ + latex: $(SAIL_SRCS) Makefile mkdir -p generated_definitions/latex $(SAIL) -latex -latex_prefix sail -o generated_definitions/latex $(SAIL_SRCS) diff --git a/c_emulator/riscv_default_callbacks.c b/c_emulator/riscv_default_callbacks.c new file mode 100644 index 000000000..d4600321c --- /dev/null +++ b/c_emulator/riscv_default_callbacks.c @@ -0,0 +1,16 @@ +/* The model assumes that these functions do not change the state of the model. + */ +int mem_update_callback(uint64_t addr, uint64_t width, lbits value, + bool is_exception) +{ +} +int mem_read_callback(uint64_t addr, uint64_t width, lbits value, + bool is_exception) +{ +} +int xreg_update_callback(unsigned reg, uint64_t value) { } +int freg_update_callback(unsigned reg, uint64_t value) { } +int csr_update_callback(const char *reg_name, uint64_t value) { } +int csr_read_callback(const char *reg_name, uint64_t value) { } +int vreg_update_callback(unsigned reg, lbits value) { } +int pc_update_callback(uint64_t value) { } diff --git a/c_emulator/riscv_rvfi_callbacks.c b/c_emulator/riscv_rvfi_callbacks.c new file mode 100644 index 000000000..44048bf28 --- /dev/null +++ b/c_emulator/riscv_rvfi_callbacks.c @@ -0,0 +1,27 @@ +int zrvfi_write(uint64_t addr, int64_t width, lbits value, bool is_exception); +int zrvfi_read(uint64_t addr, sail_int width, lbits value, bool is_exception); +int zrvfi_wX(int64_t reg, uint64_t value); + +int mem_update_callback(uint64_t addr, uint64_t width, lbits value, + bool is_exception) +{ + zrvfi_write(addr, width, value, is_exception); +} +int mem_read_callback(uint64_t addr, uint64_t width, lbits value, + bool is_exception) +{ + sail_int len; + CREATE(sail_int)(&len); + CONVERT_OF(sail_int, mach_int)(&len, width); + zrvfi_read(addr, len, value, is_exception); + KILL(sail_int)(&len); +} +int xreg_update_callback(unsigned reg, uint64_t value) +{ + zrvfi_wX(reg, value); +} +int freg_update_callback(unsigned reg, uint64_t value) { } +int csr_update_callback(const char *reg_name, uint64_t value) { } +int csr_read_callback(const char *reg_name, uint64_t value) { } +int vreg_update_callback(unsigned reg, lbits value) { } +int pc_update_callback(uint64_t value) { } diff --git a/c_emulator/riscv_sail.h b/c_emulator/riscv_sail.h index da29c2ba9..5944b346f 100644 --- a/c_emulator/riscv_sail.h +++ b/c_emulator/riscv_sail.h @@ -50,6 +50,22 @@ extern bool zhtif_done; extern mach_bits zhtif_exit_code; extern bool have_exception; +/* Callbacks for state-changing events */ + +/* Whether need to call the callback functions */ +extern bool zrv_enable_callbacks; +/* The model assumes that these functions do not change the state of the model. + */ +int mem_update_callback(uint64_t addr, uint64_t width, lbits value, + bool is_exception); +int mem_read_callback(uint64_t addr, uint64_t width, lbits value, + bool is_exception); +int xreg_update_callback(unsigned reg, uint64_t value); +int freg_update_callback(unsigned reg, uint64_t value); +int csr_update_callback(const char *reg_name, uint64_t value); +int vreg_update_callback(unsigned reg, lbits value); +int pc_update_callback(uint64_t value); + /* machine state */ extern uint32_t zcur_privilege; diff --git a/model/prelude.sail b/model/prelude.sail index 45d49c0ed..e44326e40 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -71,18 +71,15 @@ val print = "print_endline" : string -> unit val print_string = "print_string" : (string, string) -> unit val print_instr = {ocaml: "Platform.print_instr", interpreter: "print_endline", c: "print_instr", lem: "print_dbg", _: "print_endline"} : string -> unit -val print_reg = {ocaml: "Platform.print_reg", interpreter: "print_endline", c: "print_reg", lem: "print_dbg", _: "print_endline"} : string -> unit val print_mem = {ocaml: "Platform.print_mem_access", interpreter: "print_endline", c: "print_mem_access", lem: "print_dbg", _: "print_endline"} : string -> unit val print_platform = {ocaml: "Platform.print_platform", interpreter: "print_endline", c: "print_platform", lem: "print_dbg", _: "print_endline"} : string -> unit val get_config_print_instr = {ocaml: "Platform.get_config_print_instr", c:"get_config_print_instr"} : unit -> bool -val get_config_print_reg = {ocaml: "Platform.get_config_print_reg", c:"get_config_print_reg"} : unit -> bool val get_config_print_mem = {ocaml: "Platform.get_config_print_mem", c:"get_config_print_mem"} : unit -> bool val get_config_print_platform = {ocaml: "Platform.get_config_print_platform", c:"get_config_print_platform"} : unit -> bool // defaults for other backends function get_config_print_instr () = false -function get_config_print_reg () = false function get_config_print_mem () = false function get_config_print_platform () = false diff --git a/model/riscv_csr_ext.sail b/model/riscv_csr_ext.sail index f034460d6..757c32a49 100644 --- a/model/riscv_csr_ext.sail +++ b/model/riscv_csr_ext.sail @@ -22,3 +22,18 @@ end ext_read_CSR function clause ext_write_CSR (_, _) = None() end ext_write_CSR + +function ext_notification_read_CSR (csr : csreg) -> option(xlenbits) = { + let res = ext_read_CSR(csr); + if rv_enable_callbacks then + match res { + Some(value) => csr_read_callback(csr_name_map(csr), value), + None() => (), + }; + res +} + +function ext_notification_write_CSR (csr : csreg, value : xlenbits) -> unit = { + let res = ext_write_CSR(csr, value); + if rv_enable_callbacks then csr_update_callback(csr_name_map(csr), value) +} diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index 63652da88..6c710b02e 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -155,6 +155,7 @@ function rF (r : regno) -> flenbits = { function wF (r : regno, in_v : flenbits) -> unit = { assert(sys_enable_fdext()); + if rv_enable_callbacks then freg_update_callback(regno_to_regidx(r), in_v); let v = fregval_into_freg(in_v); match r { 0 => f0 = v, @@ -193,11 +194,6 @@ function wF (r : regno, in_v : flenbits) -> unit = { }; dirty_fd_context(); - - if get_config_print_reg() - then - /* TODO: will only print bits; should we print in floating point format? */ - print_reg("f" ^ dec_str(r) ^ " <- " ^ FRegStr(v)); } function rF_bits(i: regidx) -> flenbits = rF(unsigned(i)) diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 9ffb56eff..1228cb307 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -153,8 +153,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) Ext_DataAddr_Error(e) => { if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL } else { - vl = to_bits(sizeof(xlen), i); - print_reg("CSR vl <- " ^ BitStr(vl)); + ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i)); trimmed = true } }, @@ -162,16 +161,14 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) if check_misaligned(vaddr, width_type) then { if i == 0 then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else { - vl = to_bits(sizeof(xlen), i); - print_reg("CSR vl <- " ^ BitStr(vl)); + ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i)); trimmed = true } } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } else { - vl = to_bits(sizeof(xlen), i); - print_reg("CSR vl <- " ^ BitStr(vl)); + ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i)); trimmed = true } }, @@ -181,8 +178,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) MemException(e) => { if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } else { - vl = to_bits(sizeof(xlen), i); - print_reg("CSR vl <- " ^ BitStr(vl)); + ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i)); trimmed = true } } diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 16adf2806..f4861ee10 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -49,10 +49,10 @@ function handle_illegal_vtype() = { /* Note: Implementations can set vill or trap if the vtype setting is not supported. * TODO: configuration support for both solutions */ - vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ - vl = zeros(); - print_reg("CSR vtype <- " ^ BitStr(vtype.bits)); - print_reg("CSR vl <- " ^ BitStr(vl)) + let new_vtype = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ + + ext_notification_write_CSR(csr_name_map("vtype"), new_vtype); + ext_notification_write_CSR(csr_name_map("vl"), zeros()) } val calculate_new_vl : (int, int) -> xlenbits @@ -77,7 +77,8 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = { let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori; /* set vtype */ - vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; + let new_vtype = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; + ext_notification_write_CSR(csr_name_map("vtype"), new_vtype); /* check new SEW and LMUL are legal and calculate VLMAX */ let VLEN_pow = get_vlen_pow(); @@ -91,11 +92,11 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = { if (rs1 != 0b00000) then { /* normal stripmining */ let rs1_val = X(rs1); let AVL = unsigned(rs1_val); - vl = calculate_new_vl(AVL, VLMAX); + ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX)); X(rd) = vl; } else if (rd != 0b00000) then { /* set vl to VLMAX */ let AVL = unsigned(ones(sizeof(xlen))); - vl = to_bits(sizeof(xlen), VLMAX); + ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), VLMAX)); X(rd) = vl; } else { /* keep existing vl */ let AVL = unsigned(vl); @@ -104,11 +105,7 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = { }; /* reset vstart to 0 */ - vstart = zeros(); - - print_reg("CSR vtype <- " ^ BitStr(vtype.bits)); - print_reg("CSR vl <- " ^ BitStr(vl)); - print_reg("CSR vstart <- " ^ BitStr(vstart)); + ext_notification_write_CSR(csr_name_map("vstart"), zeros()); RETIRE_SUCCESS } @@ -128,7 +125,8 @@ function clause execute VSETVL(rs2, rs1, rd) = { let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori; /* set vtype */ - vtype.bits = X(rs2); + let new_vtype = X(rs2); + ext_notification_write_CSR(csr_name_map("vtype"), new_vtype); /* check new SEW and LMUL are legal and calculate VLMAX */ let VLEN_pow = get_vlen_pow(); @@ -142,11 +140,11 @@ function clause execute VSETVL(rs2, rs1, rd) = { if (rs1 != 0b00000) then { /* normal stripmining */ let rs1_val = X(rs1); let AVL = unsigned(rs1_val); - vl = calculate_new_vl(AVL, VLMAX); + ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX)); X(rd) = vl; } else if (rd != 0b00000) then { /* set vl to VLMAX */ let AVL = unsigned(ones(sizeof(xlen))); - vl = to_bits(sizeof(xlen), VLMAX); + ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), VLMAX)); X(rd) = vl; } else { /* keep existing vl */ let AVL = unsigned(vl); @@ -155,11 +153,7 @@ function clause execute VSETVL(rs2, rs1, rd) = { }; /* reset vstart to 0 */ - vstart = zeros(); - - print_reg("CSR vtype <- " ^ BitStr(vtype.bits)); - print_reg("CSR vl <- " ^ BitStr(vl)); - print_reg("CSR vstart <- " ^ BitStr(vstart)); + ext_notification_write_CSR(csr_name_map("vstart"), zeros()); RETIRE_SUCCESS } @@ -175,7 +169,8 @@ mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if extensionEnable function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = { /* set vtype */ - vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; + let new_vtype = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; + ext_notification_write_CSR(csr_name_map("vtype"), new_vtype); /* check new SEW and LMUL are legal and calculate VLMAX */ let VLEN_pow = get_vlen_pow(); @@ -187,15 +182,11 @@ function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = { /* set vl according to VLMAX and AVL */ let AVL = unsigned(uimm); /* AVL is encoded as 5-bit zero-extended imm in the rs1 field */ - vl = calculate_new_vl(AVL, VLMAX); + ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX)); X(rd) = vl; /* reset vstart to 0 */ - vstart = zeros(); - - print_reg("CSR vtype <- " ^ BitStr(vtype.bits)); - print_reg("CSR vl <- " ^ BitStr(vl)); - print_reg("CSR vstart <- " ^ BitStr(vstart)); + ext_notification_write_CSR(csr_name_map("vstart"), zeros()); RETIRE_SUCCESS } diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index f2980fb9e..c69500a0e 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -101,18 +101,17 @@ function readCSR csr : csreg -> xlenbits = { (0x015, _) => read_seed_csr(), _ => /* check extensions */ - match ext_read_CSR(csr) { + match ext_notification_read_CSR(csr) { Some(res) => res, None() => { print_bits("unhandled read to CSR ", csr); zero_extend(0x0) } } }; - if get_config_print_reg() - then print_reg("CSR " ^ to_str(csr) ^ " -> " ^ BitStr(res)); res } function writeCSR (csr : csreg, value : xlenbits) -> unit = { + if rv_enable_callbacks then csr_update_callback(csr_name_map(csr), value); let res : option(xlenbits) = match (csr, sizeof(xlen)) { /* machine mode */ @@ -184,11 +183,6 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { _ => ext_write_CSR(csr, value) }; - match res { - Some(v) => if get_config_print_reg() - then print_reg("CSR " ^ to_str(csr) ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"), - None() => print_bits("unhandled write to CSR ", csr) - } } function clause execute CSR(csr, rs1, rd, is_imm, op) = { diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 82227ad7e..097669db7 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -117,25 +117,6 @@ function checked_mem_read forall 'n, 0 < 'n <= max_mem_access . ( /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */ -$ifdef RVFI_DII -val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit -function rvfi_read (addr, width, result) = { - rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); - rvfi_mem_data_present = true; - match result { - /* TODO: report tag bit for capability writes and extend mask by one bit. */ - MemValue(v, _) => if width <= 16 - then { rvfi_mem_data[rvfi_mem_rdata] = sail_zero_extend(v, 256); - rvfi_mem_data[rvfi_mem_rmask] = rvfi_encode_width_mask(width) } - else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!") }, - MemException(_) => () - }; -} -$else -val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit -function rvfi_read (addr, width, result) = () -$endif - val mem_read : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) val mem_read_priv : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), Privilege, xlenbits, int('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) val mem_read_meta : forall 'n, 0 < 'n <= max_mem_access . (AccessType(ext_access_type), xlenbits, int('n), bool, bool, bool, bool) -> MemoryOpResult((bits(8 * 'n), mem_meta)) @@ -151,7 +132,11 @@ function mem_read_priv_meta (typ, priv, paddr, width, aq, rl, res, meta) = { (false, true, true) => throw(Error_not_implemented("lr.rl")), (_, _, _) => checked_mem_read(typ, priv, paddr, width, aq, rl, res, meta) }; - rvfi_read(paddr, width, result); + if rv_enable_callbacks then + match result { + MemValue(value, _) => mem_read_callback(paddr, width, value, /* is_exception */ false), + MemException(_) => mem_read_callback(paddr, width, zeros(), /* is_exception */ true) + }; result } @@ -172,28 +157,6 @@ function mem_write_ea (addr, width, aq, rl, con) = then MemException(E_SAMO_Addr_Align()) else MemValue(write_ram_ea(write_kind_of_flags(aq, rl, con), addr, width)) -$ifdef RVFI_DII -val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit -function rvfi_write (addr, width, value, meta, result) = { - rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); - rvfi_mem_data_present = true; - match result { - /* Log only the memory address (without the value) if the write fails. */ - MemValue(_) => if width <= 16 then { - /* TODO: report tag bit for capability writes and extend mask by one bit. */ - rvfi_mem_data[rvfi_mem_wdata] = sail_zero_extend(value,256); - rvfi_mem_data[rvfi_mem_wmask] = rvfi_encode_width_mask(width); - } else { - internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!"); - }, - MemException(_) => () - } -} -$else -val rvfi_write : forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit -function rvfi_write (addr, width, value, meta, result) = () -$endif - // only used for actual memory regions, to avoid MMIO effects function phys_mem_write forall 'n, 0 < 'n <= max_mem_access . (wk : write_kind, paddr : xlenbits, width : int('n), data : bits(8 * 'n), meta : mem_meta) -> MemoryOpResult(bool) = { let result = MemValue(write_ram(wk, paddr, width, data, meta)); @@ -243,7 +206,11 @@ function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl then MemException(E_SAMO_Addr_Align()) else { let result = checked_mem_write(paddr, width, value, typ, priv, meta, aq, rl, con); - rvfi_write(paddr, width, value, meta, result); + if rv_enable_callbacks then + match result { + MemValue(_) => mem_update_callback(paddr, width, value, /* is_exception */ false), + MemException(_) => mem_update_callback(paddr, width, value, /* is_exception */ true) + }; result } } diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail index a17e86d32..4c8c43389 100644 --- a/model/riscv_pc_access.sail +++ b/model/riscv_pc_access.sail @@ -28,5 +28,6 @@ function set_next_pc(pc) = { val tick_pc : unit -> unit function tick_pc() = { + if rv_enable_callbacks then pc_update_callback(PC); PC = nextPC } diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail index 26faef210..13dd2cc04 100644 --- a/model/riscv_regs.sail +++ b/model/riscv_regs.sail @@ -88,16 +88,6 @@ function rX (r : regno) -> xlenbits = { regval_from_reg(v) } -$ifdef RVFI_DII -function rvfi_wX (r : regno, v : xlenbits) -> unit = { - rvfi_int_data[rvfi_rd_wdata] = zero_extend(v); - rvfi_int_data[rvfi_rd_addr] = to_bits(8,r); - rvfi_int_data_present = true; -} -$else -function rvfi_wX (r : regno, v : xlenbits) -> unit = () -$endif - function wX (r : regno, in_v : xlenbits) -> unit = { let v = regval_into_reg(in_v); match r { @@ -136,9 +126,7 @@ function wX (r : regno, in_v : xlenbits) -> unit = { _ => assert(false, "invalid register number") }; if (r != 0) then { - rvfi_wX(r, in_v); - if get_config_print_reg() - then print_reg("x" ^ dec_str(r) ^ " <- " ^ RegStr(v)); + if rv_enable_callbacks then xreg_update_callback(regno_to_regidx(r), in_v); } } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 4f7b3540b..40a763bad 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -340,8 +340,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); - if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); + if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); prepare_trap_vector(del_priv, mcause) }, @@ -365,8 +364,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); - if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); + if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); prepare_trap_vector(del_priv, scause) }, @@ -385,8 +383,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); - if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); + if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); prepare_trap_vector(del_priv, ucause) } @@ -412,8 +409,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, if cur_privilege != Machine then mstatus[MPRV] = 0b0; - if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); + if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -428,8 +424,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, if cur_privilege != Machine then mstatus[MPRV] = 0b0; - if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); + if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -442,8 +437,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, mstatus[UPIE] = 0b1; cur_privilege = User; - if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits)); + if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -550,9 +544,7 @@ function init_sys() -> unit = { // PMP's L and A fields are set to 0 on reset. init_pmp(); - // log compatibility with spike - if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits) ^ " (input: " ^ BitStr(zero_extend(0b0) : xlenbits) ^ ")") + if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); } /* memory access exceptions, defined here for use by the platform model. */ diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 166aee072..03dc464ad 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -43,6 +43,9 @@ type regno = range(0, 31) function regidx_to_regno (b : regidx) -> regno = unsigned(b) +val regno_to_regidx : {'n, 0 <= 'n < 32. regno('n)} -> bits(5) +function regno_to_regidx b = let 'r = to_bits(5, b) in r + /* mapping RVC register indices into normal indices */ val creg2reg_idx : cregidx -> regidx function creg2reg_idx(creg) = 0b01 @ creg @@ -408,3 +411,22 @@ function report_invalid_width(f , l, w, k) -> 'a = { internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^ " with xlen=" ^ dec_str(sizeof(xlen))) } + +/* Callbacks for state-changing events */ + +/* Whether need to call the callback functions */ +$ifdef RVFI_DII +register rv_enable_callbacks : bool = true +$else +register rv_enable_callbacks : bool = false +$endif + +/* Defaults for these functions in riscv_default_callbacks.c and platform_impl.ml */ + +val mem_update_callback = pure {ocaml: "Platform.mem_update_callback", c: "mem_update_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n), /* is exception */ bool) -> unit +val mem_read_callback = pure {ocaml: "Platform.mem_read_callback", c: "mem_read_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n), /* is exception */ bool) -> unit +val pc_update_callback = pure {ocaml: "Platform.pc_update_callback", c: "pc_update_callback"} : xlenbits -> unit +val xreg_update_callback = pure {ocaml: "Platform.xreg_update_callback", c: "xreg_update_callback"} : (regidx, xlenbits) -> unit +val freg_update_callback = pure {ocaml: "Platform.freg_update_callback", c: "freg_update_callback"} : (regidx, flenbits) -> unit +val csr_update_callback = pure {ocaml: "Platform.csr_update_callback", c: "csr_update_callback"} : (/* name from the csr_name_map */ string, xlenbits) -> unit +val csr_read_callback = pure {ocaml: "Platform.csr_read_callback", c: "csr_read_callback"} : (/* name from the csr_name_map */ string, xlenbits) -> unit diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index 8d96f12a0..a80e4eba4 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -169,8 +169,7 @@ function wV (r : regno, in_v : vregtype) -> unit = { let VLEN = unsigned(vlenb) * 8; assert(0 < VLEN & VLEN <= sizeof(vlenmax)); - if get_config_print_reg() - then print_reg("v" ^ dec_str(r) ^ " <- " ^ BitStr(v[VLEN - 1 .. 0])); + if rv_enable_callbacks then vreg_update_callback(regno_to_regidx(r), v); } function rV_bits(i: regidx) -> vregtype = rV(unsigned(i)) diff --git a/model/riscv_vreg_type.sail b/model/riscv_vreg_type.sail index 2ab211b8c..79190955c 100755 --- a/model/riscv_vreg_type.sail +++ b/model/riscv_vreg_type.sail @@ -146,3 +146,8 @@ enum fwffunct6 = { FWF_VADD, FWF_VSUB } enum fvfmfunct6 = { VFM_VMFEQ, VFM_VMFLE, VFM_VMFLT, VFM_VMFNE, VFM_VMFGT, VFM_VMFGE } enum vmlsop = { VLM, VSM } + +/* Callbacks for vregs state-changing events */ + +/* Default for this function in riscv_default_callbacks.c and platform_impl.ml */ +val vreg_update_callback = pure {ocaml: "Platform.vreg_update_callback", c: "vreg_update_callback"} : (regidx, vregtype) -> unit diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail index d1ad480df..5afb685fb 100644 --- a/model/rvfi_dii.sail +++ b/model/rvfi_dii.sail @@ -325,3 +325,46 @@ function print_rvfi_exec () = { print_bits("rvfi_pc_rdata : ", rvfi_pc_data[rvfi_pc_rdata]); print_bits("rvfi_order : ", rvfi_inst_data[rvfi_order]); } + +/* RVFI records */ + +val internal_error : forall ('a : Type). (string, int, string) -> 'a + +val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), bool) -> unit +function rvfi_write (addr, width, value, is_exception) = { + rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); + rvfi_mem_data_present = true; + /* Log only the memory address (without the value) if the write fails. */ + if is_exception == false then { + if width <= 16 then { + /* TODO: report tag bit for capability writes and extend mask by one bit. */ + rvfi_mem_data[rvfi_mem_wdata] = sail_zero_extend(value, 256); + rvfi_mem_data[rvfi_mem_wmask] = rvfi_encode_width_mask(width); + } else { + internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!"); + }; + }; +} + +val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n), bool) -> unit +function rvfi_read (addr, width, value, is_exception) = { + rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); + rvfi_mem_data_present = true; + /* Log only the memory address (without the value) if the write fails. */ + if is_exception == false then { + if width <= 16 then { + /* TODO: report tag bit for capability writes and extend mask by one bit. */ + rvfi_mem_data[rvfi_mem_rdata] = sail_zero_extend(value, 256); + rvfi_mem_data[rvfi_mem_rmask] = rvfi_encode_width_mask(width) + } else { + internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!") + }; + }; +} + +val rvfi_wX : forall 'n, 0 <= 'n < 32. (int('n), xlenbits) -> unit +function rvfi_wX (r,v) = { + rvfi_int_data[rvfi_rd_wdata] = zero_extend(v); + rvfi_int_data[rvfi_rd_addr] = to_bits(8, r); + rvfi_int_data_present = true; +} diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index d10029a8b..8a6632c9b 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -23,6 +23,17 @@ let set_config_pmp_grain x = config_pmp_grain := Big_int.of_int x let platform_arch = ref P.RV64 +(* Defaults for callbacks functions. + The model assumes that these functions do not change the state of the model. *) +let mem_update_callback (addr, width, value, is_exception) = () +let mem_read_callback (addr, width, value, is_exception) = () +let pc_update_callback value = () +let xreg_update_callback (reg, value) = () +let freg_update_callback (reg, value) = () +let csr_update_callback (reg_name, value) = () +let csr_read_callback (reg_name, value) = () +let vreg_update_callback (reg, value) = () + (* logging *) let config_print_instr = ref true diff --git a/test/run_tests.sh b/test/run_tests.sh old mode 100755 new mode 100644 From be696b8e426dbcb1fe892cc528556299ffb7b2a1 Mon Sep 17 00:00:00 2001 From: Ksenia Dobrovolskaya Date: Wed, 24 Jul 2024 18:09:33 +0300 Subject: [PATCH 2/2] Implementing callbacks in sail-riscv for state-changing events Pushed all the rv_enable_callbacks into the callback functions. --- Makefile | 29 ++--------------- c_emulator/riscv_config.h | 1 + c_emulator/riscv_default_callbacks.c | 23 ++++++------- c_emulator/riscv_rvfi_callbacks.c | 48 +++++++++++++++++----------- c_emulator/riscv_sail.h | 20 ++++++------ c_emulator/riscv_sim.c | 2 ++ model/riscv_csr_ext.sail | 15 --------- model/riscv_fdext_regs.sail | 3 +- model/riscv_insts_vext_mem.sail | 12 ++++--- model/riscv_insts_vext_vset.sail | 45 +++++++++++++++----------- model/riscv_insts_zicsr.sail | 8 +++-- model/riscv_mem.sail | 18 +++++------ model/riscv_pc_access.sail | 2 +- model/riscv_regs.sail | 2 +- model/riscv_sys_control.sail | 14 ++++---- model/riscv_types.sail | 25 ++++++--------- model/riscv_vext_regs.sail | 2 +- model/riscv_vreg_type.sail | 2 +- model/rvfi_dii.sail | 21 ++++++------ ocaml_emulator/platform.ml | 17 +++++----- 20 files changed, 143 insertions(+), 166 deletions(-) diff --git a/Makefile b/Makefile index 36c3ad7d1..1a434aa5d 100644 --- a/Makefile +++ b/Makefile @@ -287,32 +287,6 @@ rvfi: c_emulator/riscv_rvfi_$(ARCH) c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile $(CC) -g $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ -# Note: We have to add -c_preserve since the functions might be optimized out otherwise -rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \ - -c_preserve rvfi_get_cmd \ - -c_preserve rvfi_get_insn \ - -c_preserve rvfi_get_v2_trace_size \ - -c_preserve rvfi_get_v2_support_packet \ - -c_preserve rvfi_get_exec_packet_v1 \ - -c_preserve rvfi_get_exec_packet_v2 \ - -c_preserve rvfi_get_mem_data \ - -c_preserve rvfi_get_int_data \ - -c_preserve rvfi_zero_exec_packet \ - -c_preserve rvfi_halt_exec_packet \ - -c_preserve print_rvfi_exec \ - -c_preserve print_instr_packet \ - -c_preserve print_rvfi_exec - -# sed -i isn't posix compliant, unfortunately -generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile - mkdir -p generated_definitions/c - $(SAIL) $(c_preserve_fns) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@) - sed -e '/^[[:space:]]*$$/d' $@ > $@.new - mv $@.new $@ - -c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile - $(CC) -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ - # Note: We have to add -c_preserve since the functions might be optimized out otherwise rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \ -c_preserve rvfi_get_cmd \ @@ -327,6 +301,7 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \ -c_preserve rvfi_halt_exec_packet \ -c_preserve rvfi_write \ -c_preserve rvfi_read \ + -c_preserve rvfi_mem_exception \ -c_preserve rvfi_wX \ -c_preserve print_rvfi_exec \ -c_preserve print_instr_packet \ @@ -340,7 +315,7 @@ generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main mv $@.new $@ c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile - gcc -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ + $(CC) -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ latex: $(SAIL_SRCS) Makefile mkdir -p generated_definitions/latex diff --git a/c_emulator/riscv_config.h b/c_emulator/riscv_config.h index f8f3eb30d..285ff0421 100644 --- a/c_emulator/riscv_config.h +++ b/c_emulator/riscv_config.h @@ -5,3 +5,4 @@ extern bool config_print_instr; extern bool config_print_reg; extern bool config_print_mem_access; extern bool config_print_platform; +extern bool rv_enable_callbacks; diff --git a/c_emulator/riscv_default_callbacks.c b/c_emulator/riscv_default_callbacks.c index d4600321c..fd7fa3e84 100644 --- a/c_emulator/riscv_default_callbacks.c +++ b/c_emulator/riscv_default_callbacks.c @@ -1,16 +1,11 @@ /* The model assumes that these functions do not change the state of the model. */ -int mem_update_callback(uint64_t addr, uint64_t width, lbits value, - bool is_exception) -{ -} -int mem_read_callback(uint64_t addr, uint64_t width, lbits value, - bool is_exception) -{ -} -int xreg_update_callback(unsigned reg, uint64_t value) { } -int freg_update_callback(unsigned reg, uint64_t value) { } -int csr_update_callback(const char *reg_name, uint64_t value) { } -int csr_read_callback(const char *reg_name, uint64_t value) { } -int vreg_update_callback(unsigned reg, lbits value) { } -int pc_update_callback(uint64_t value) { } +int mem_write_callback(uint64_t addr, uint64_t width, lbits value) { } +int mem_read_callback(uint64_t addr, uint64_t width, lbits value) { } +int mem_exception_callback(uint64_t addr, uint64_t num_of_exception) { } +int xreg_write_callback(unsigned reg, uint64_t value) { } +int freg_write_callback(unsigned reg, uint64_t value) { } +int csr_write_callback(unsigned reg, uint64_t value) { } +int csr_read_callback(unsigned reg, uint64_t value) { } +int vreg_write_callback(unsigned reg, lbits value) { } +int pc_write_callback(uint64_t value) { } diff --git a/c_emulator/riscv_rvfi_callbacks.c b/c_emulator/riscv_rvfi_callbacks.c index 44048bf28..77cd37e8e 100644 --- a/c_emulator/riscv_rvfi_callbacks.c +++ b/c_emulator/riscv_rvfi_callbacks.c @@ -1,27 +1,37 @@ -int zrvfi_write(uint64_t addr, int64_t width, lbits value, bool is_exception); -int zrvfi_read(uint64_t addr, sail_int width, lbits value, bool is_exception); +#include "riscv_config.h" + +int zrvfi_write(uint64_t addr, int64_t width, lbits value); +int zrvfi_read(uint64_t addr, sail_int width, lbits value); +int zrvfi_mem_exception(uint64_t addr); int zrvfi_wX(int64_t reg, uint64_t value); -int mem_update_callback(uint64_t addr, uint64_t width, lbits value, - bool is_exception) +int mem_write_callback(uint64_t addr, uint64_t width, lbits value) +{ + if (rv_enable_callbacks) + zrvfi_write(addr, width, value); +} +int mem_read_callback(uint64_t addr, uint64_t width, lbits value) { - zrvfi_write(addr, width, value, is_exception); + if (rv_enable_callbacks) { + sail_int len; + CREATE(sail_int)(&len); + CONVERT_OF(sail_int, mach_int)(&len, width); + zrvfi_read(addr, len, value); + KILL(sail_int)(&len); + } } -int mem_read_callback(uint64_t addr, uint64_t width, lbits value, - bool is_exception) +int mem_exception_callback(uint64_t addr, uint64_t num_of_exception) { - sail_int len; - CREATE(sail_int)(&len); - CONVERT_OF(sail_int, mach_int)(&len, width); - zrvfi_read(addr, len, value, is_exception); - KILL(sail_int)(&len); + if (rv_enable_callbacks) + zrvfi_mem_exception(addr); } -int xreg_update_callback(unsigned reg, uint64_t value) +int xreg_write_callback(unsigned reg, uint64_t value) { - zrvfi_wX(reg, value); + if (rv_enable_callbacks) + zrvfi_wX(reg, value); } -int freg_update_callback(unsigned reg, uint64_t value) { } -int csr_update_callback(const char *reg_name, uint64_t value) { } -int csr_read_callback(const char *reg_name, uint64_t value) { } -int vreg_update_callback(unsigned reg, lbits value) { } -int pc_update_callback(uint64_t value) { } +int freg_write_callback(unsigned reg, uint64_t value) { } +int csr_write_callback(unsigned reg, uint64_t value) { } +int csr_read_callback(unsigned reg, uint64_t value) { } +int vreg_write_callback(unsigned reg, lbits value) { } +int pc_write_callback(uint64_t value) { } diff --git a/c_emulator/riscv_sail.h b/c_emulator/riscv_sail.h index 5944b346f..e7247fc58 100644 --- a/c_emulator/riscv_sail.h +++ b/c_emulator/riscv_sail.h @@ -52,19 +52,17 @@ extern bool have_exception; /* Callbacks for state-changing events */ -/* Whether need to call the callback functions */ -extern bool zrv_enable_callbacks; /* The model assumes that these functions do not change the state of the model. */ -int mem_update_callback(uint64_t addr, uint64_t width, lbits value, - bool is_exception); -int mem_read_callback(uint64_t addr, uint64_t width, lbits value, - bool is_exception); -int xreg_update_callback(unsigned reg, uint64_t value); -int freg_update_callback(unsigned reg, uint64_t value); -int csr_update_callback(const char *reg_name, uint64_t value); -int vreg_update_callback(unsigned reg, lbits value); -int pc_update_callback(uint64_t value); +int mem_write_callback(uint64_t addr, uint64_t width, lbits value); +int mem_read_callback(uint64_t addr, uint64_t width, lbits value); +int mem_exception_callback(uint64_t addr, uint64_t num_of_exception); +int xreg_write_callback(unsigned reg, uint64_t value); +int freg_write_callback(unsigned reg, uint64_t value); +int csr_write_callback(unsigned reg, uint64_t value); +int csr_read_callback(unsigned reg, uint64_t value); +int vreg_write_callback(unsigned reg, lbits value); +int pc_write_callback(uint64_t value); /* machine state */ diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 913543144..dccb57775 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -89,6 +89,7 @@ bool config_print_reg = true; bool config_print_mem_access = true; bool config_print_platform = true; bool config_print_rvfi = false; +bool rv_enable_callbacks = true; void set_config_print(char *var, bool val) { @@ -98,6 +99,7 @@ void set_config_print(char *var, bool val) config_print_reg = val; config_print_platform = val; config_print_rvfi = val; + rv_enable_callbacks = val; } else if (strcmp("instr", var) == 0) { config_print_instr = val; } else if (strcmp("reg", var) == 0) { diff --git a/model/riscv_csr_ext.sail b/model/riscv_csr_ext.sail index 757c32a49..f034460d6 100644 --- a/model/riscv_csr_ext.sail +++ b/model/riscv_csr_ext.sail @@ -22,18 +22,3 @@ end ext_read_CSR function clause ext_write_CSR (_, _) = None() end ext_write_CSR - -function ext_notification_read_CSR (csr : csreg) -> option(xlenbits) = { - let res = ext_read_CSR(csr); - if rv_enable_callbacks then - match res { - Some(value) => csr_read_callback(csr_name_map(csr), value), - None() => (), - }; - res -} - -function ext_notification_write_CSR (csr : csreg, value : xlenbits) -> unit = { - let res = ext_write_CSR(csr, value); - if rv_enable_callbacks then csr_update_callback(csr_name_map(csr), value) -} diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index 6c710b02e..de6118b75 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -155,7 +155,6 @@ function rF (r : regno) -> flenbits = { function wF (r : regno, in_v : flenbits) -> unit = { assert(sys_enable_fdext()); - if rv_enable_callbacks then freg_update_callback(regno_to_regidx(r), in_v); let v = fregval_into_freg(in_v); match r { 0 => f0 = v, @@ -194,6 +193,8 @@ function wF (r : regno, in_v : flenbits) -> unit = { }; dirty_fd_context(); + + freg_write_callback(regno_to_regidx(r), in_v); } function rF_bits(i: regidx) -> flenbits = rF(unsigned(i)) diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index 1228cb307..bf8b63591 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -153,7 +153,8 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) Ext_DataAddr_Error(e) => { if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL } else { - ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i)); + vl = to_bits(sizeof(xlen), i); + csr_write_callback(csr_name_map("vl"), vl); trimmed = true } }, @@ -161,14 +162,16 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) if check_misaligned(vaddr, width_type) then { if i == 0 then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else { - ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i)); + vl = to_bits(sizeof(xlen), i); + csr_write_callback(csr_name_map("vl"), vl); trimmed = true } } else match translateAddr(vaddr, Read(Data)) { TR_Failure(e, _) => { if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } else { - ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i)); + vl = to_bits(sizeof(xlen), i); + csr_write_callback(csr_name_map("vl"), vl); trimmed = true } }, @@ -178,7 +181,8 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) MemException(e) => { if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } else { - ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i)); + vl = to_bits(sizeof(xlen), i); + csr_write_callback(csr_name_map("vl"), vl); trimmed = true } } diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index f4861ee10..774f27522 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -49,10 +49,10 @@ function handle_illegal_vtype() = { /* Note: Implementations can set vill or trap if the vtype setting is not supported. * TODO: configuration support for both solutions */ - let new_vtype = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ - - ext_notification_write_CSR(csr_name_map("vtype"), new_vtype); - ext_notification_write_CSR(csr_name_map("vl"), zeros()) + vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ + vl = zeros(); + csr_write_callback(csr_name_map("vtype"), vtype.bits); + csr_write_callback(csr_name_map("vl"), vl); } val calculate_new_vl : (int, int) -> xlenbits @@ -77,8 +77,7 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = { let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori; /* set vtype */ - let new_vtype = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; - ext_notification_write_CSR(csr_name_map("vtype"), new_vtype); + vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; /* check new SEW and LMUL are legal and calculate VLMAX */ let VLEN_pow = get_vlen_pow(); @@ -92,11 +91,11 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = { if (rs1 != 0b00000) then { /* normal stripmining */ let rs1_val = X(rs1); let AVL = unsigned(rs1_val); - ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX)); + vl = calculate_new_vl(AVL, VLMAX); X(rd) = vl; } else if (rd != 0b00000) then { /* set vl to VLMAX */ let AVL = unsigned(ones(sizeof(xlen))); - ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), VLMAX)); + vl = to_bits(sizeof(xlen), VLMAX); X(rd) = vl; } else { /* keep existing vl */ let AVL = unsigned(vl); @@ -105,7 +104,11 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = { }; /* reset vstart to 0 */ - ext_notification_write_CSR(csr_name_map("vstart"), zeros()); + vstart = zeros(); + + csr_write_callback(csr_name_map("vtype"), vtype.bits); + csr_write_callback(csr_name_map("vl"), vl); + csr_write_callback(csr_name_map("vstart"), zero_extend(vstart)); RETIRE_SUCCESS } @@ -125,8 +128,7 @@ function clause execute VSETVL(rs2, rs1, rd) = { let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori; /* set vtype */ - let new_vtype = X(rs2); - ext_notification_write_CSR(csr_name_map("vtype"), new_vtype); + vtype.bits = X(rs2); /* check new SEW and LMUL are legal and calculate VLMAX */ let VLEN_pow = get_vlen_pow(); @@ -140,11 +142,11 @@ function clause execute VSETVL(rs2, rs1, rd) = { if (rs1 != 0b00000) then { /* normal stripmining */ let rs1_val = X(rs1); let AVL = unsigned(rs1_val); - ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX)); + vl = calculate_new_vl(AVL, VLMAX); X(rd) = vl; } else if (rd != 0b00000) then { /* set vl to VLMAX */ let AVL = unsigned(ones(sizeof(xlen))); - ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), VLMAX)); + vl = to_bits(sizeof(xlen), VLMAX); X(rd) = vl; } else { /* keep existing vl */ let AVL = unsigned(vl); @@ -153,7 +155,11 @@ function clause execute VSETVL(rs2, rs1, rd) = { }; /* reset vstart to 0 */ - ext_notification_write_CSR(csr_name_map("vstart"), zeros()); + vstart = zeros(); + + csr_write_callback(csr_name_map("vtype"), vtype.bits); + csr_write_callback(csr_name_map("vl"), vl); + csr_write_callback(csr_name_map("vstart"), zero_extend(vstart)); RETIRE_SUCCESS } @@ -169,8 +175,7 @@ mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if extensionEnable function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = { /* set vtype */ - let new_vtype = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; - ext_notification_write_CSR(csr_name_map("vtype"), new_vtype); + vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; /* check new SEW and LMUL are legal and calculate VLMAX */ let VLEN_pow = get_vlen_pow(); @@ -182,11 +187,15 @@ function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = { /* set vl according to VLMAX and AVL */ let AVL = unsigned(uimm); /* AVL is encoded as 5-bit zero-extended imm in the rs1 field */ - ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX)); + vl = calculate_new_vl(AVL, VLMAX); X(rd) = vl; /* reset vstart to 0 */ - ext_notification_write_CSR(csr_name_map("vstart"), zeros()); + vstart = zeros(); + + csr_write_callback(csr_name_map("vtype"), vtype.bits); + csr_write_callback(csr_name_map("vl"), vl); + csr_write_callback(csr_name_map("vstart"), zero_extend(vstart)); RETIRE_SUCCESS } diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index c69500a0e..4334df551 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -101,17 +101,17 @@ function readCSR csr : csreg -> xlenbits = { (0x015, _) => read_seed_csr(), _ => /* check extensions */ - match ext_notification_read_CSR(csr) { + match ext_read_CSR(csr) { Some(res) => res, None() => { print_bits("unhandled read to CSR ", csr); zero_extend(0x0) } } }; + csr_read_callback(csr, res); res } function writeCSR (csr : csreg, value : xlenbits) -> unit = { - if rv_enable_callbacks then csr_update_callback(csr_name_map(csr), value); let res : option(xlenbits) = match (csr, sizeof(xlen)) { /* machine mode */ @@ -183,6 +183,10 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { _ => ext_write_CSR(csr, value) }; + match res { + Some(v) => csr_write_callback(csr, v), + None() => print_bits("unhandled write to CSR ", csr) + } } function clause execute CSR(csr, rs1, rd, is_imm, op) = { diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 097669db7..3468ce702 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -132,11 +132,10 @@ function mem_read_priv_meta (typ, priv, paddr, width, aq, rl, res, meta) = { (false, true, true) => throw(Error_not_implemented("lr.rl")), (_, _, _) => checked_mem_read(typ, priv, paddr, width, aq, rl, res, meta) }; - if rv_enable_callbacks then - match result { - MemValue(value, _) => mem_read_callback(paddr, width, value, /* is_exception */ false), - MemException(_) => mem_read_callback(paddr, width, zeros(), /* is_exception */ true) - }; + match result { + MemValue(value, _) => mem_read_callback(paddr, width, value), + MemException(e) => mem_exception_callback(paddr, num_of_ExceptionType(e)) + }; result } @@ -206,11 +205,10 @@ function mem_write_value_priv_meta (paddr, width, value, typ, priv, meta, aq, rl then MemException(E_SAMO_Addr_Align()) else { let result = checked_mem_write(paddr, width, value, typ, priv, meta, aq, rl, con); - if rv_enable_callbacks then - match result { - MemValue(_) => mem_update_callback(paddr, width, value, /* is_exception */ false), - MemException(_) => mem_update_callback(paddr, width, value, /* is_exception */ true) - }; + match result { + MemValue(_) => mem_write_callback(paddr, width, value), + MemException(e) => mem_exception_callback(paddr, num_of_ExceptionType(e)) + }; result } } diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail index 4c8c43389..f69266328 100644 --- a/model/riscv_pc_access.sail +++ b/model/riscv_pc_access.sail @@ -28,6 +28,6 @@ function set_next_pc(pc) = { val tick_pc : unit -> unit function tick_pc() = { - if rv_enable_callbacks then pc_update_callback(PC); + pc_write_callback(PC); PC = nextPC } diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail index 13dd2cc04..6d18e468e 100644 --- a/model/riscv_regs.sail +++ b/model/riscv_regs.sail @@ -126,7 +126,7 @@ function wX (r : regno, in_v : xlenbits) -> unit = { _ => assert(false, "invalid register number") }; if (r != 0) then { - if rv_enable_callbacks then xreg_update_callback(regno_to_regidx(r), in_v); + xreg_write_callback(regno_to_regidx(r), in_v); } } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 40a763bad..ece9b1d3c 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -340,7 +340,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); prepare_trap_vector(del_priv, mcause) }, @@ -364,7 +364,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); prepare_trap_vector(del_priv, scause) }, @@ -383,7 +383,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen handle_trap_extension(del_priv, pc, ext); - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); prepare_trap_vector(del_priv, ucause) } @@ -409,7 +409,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, if cur_privilege != Machine then mstatus[MPRV] = 0b0; - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -424,7 +424,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, if cur_privilege != Machine then mstatus[MPRV] = 0b0; - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -437,7 +437,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, mstatus[UPIE] = 0b1; cur_privilege = User; - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); if get_config_print_platform() then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); @@ -544,7 +544,7 @@ function init_sys() -> unit = { // PMP's L and A fields are set to 0 on reset. init_pmp(); - if rv_enable_callbacks then csr_update_callback("mstatus", mstatus.bits); + csr_write_callback(csr_name_map("mstatus"), mstatus.bits); } /* memory access exceptions, defined here for use by the platform model. */ diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 03dc464ad..58178ae3a 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -43,8 +43,7 @@ type regno = range(0, 31) function regidx_to_regno (b : regidx) -> regno = unsigned(b) -val regno_to_regidx : {'n, 0 <= 'n < 32. regno('n)} -> bits(5) -function regno_to_regidx b = let 'r = to_bits(5, b) in r +function regno_to_regidx (b : regno) -> regidx = to_bits(5, b) /* mapping RVC register indices into normal indices */ val creg2reg_idx : cregidx -> regidx @@ -414,19 +413,13 @@ function report_invalid_width(f , l, w, k) -> 'a = { /* Callbacks for state-changing events */ -/* Whether need to call the callback functions */ -$ifdef RVFI_DII -register rv_enable_callbacks : bool = true -$else -register rv_enable_callbacks : bool = false -$endif - /* Defaults for these functions in riscv_default_callbacks.c and platform_impl.ml */ -val mem_update_callback = pure {ocaml: "Platform.mem_update_callback", c: "mem_update_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n), /* is exception */ bool) -> unit -val mem_read_callback = pure {ocaml: "Platform.mem_read_callback", c: "mem_read_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n), /* is exception */ bool) -> unit -val pc_update_callback = pure {ocaml: "Platform.pc_update_callback", c: "pc_update_callback"} : xlenbits -> unit -val xreg_update_callback = pure {ocaml: "Platform.xreg_update_callback", c: "xreg_update_callback"} : (regidx, xlenbits) -> unit -val freg_update_callback = pure {ocaml: "Platform.freg_update_callback", c: "freg_update_callback"} : (regidx, flenbits) -> unit -val csr_update_callback = pure {ocaml: "Platform.csr_update_callback", c: "csr_update_callback"} : (/* name from the csr_name_map */ string, xlenbits) -> unit -val csr_read_callback = pure {ocaml: "Platform.csr_read_callback", c: "csr_read_callback"} : (/* name from the csr_name_map */ string, xlenbits) -> unit +val mem_write_callback = pure {ocaml: "Platform.mem_write_callback", c: "mem_write_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> unit +val mem_read_callback = pure {ocaml: "Platform.mem_read_callback", c: "mem_read_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> unit +val mem_exception_callback = pure {ocaml: "Platform.mem_exception_callback", c: "mem_exception_callback"} : forall 'n, 0 <= 'n < xlen . (/* addr */ xlenbits, /* num_of_ExceptionType */ int('n)) -> unit +val pc_write_callback = pure {ocaml: "Platform.pc_write_callback", c: "pc_write_callback"} : xlenbits -> unit +val xreg_write_callback = pure {ocaml: "Platform.xreg_write_callback", c: "xreg_write_callback"} : (regidx, xlenbits) -> unit +val freg_write_callback = pure {ocaml: "Platform.freg_write_callback", c: "freg_write_callback"} : (regidx, flenbits) -> unit +val csr_write_callback = pure {ocaml: "Platform.csr_write_callback", c: "csr_write_callback"} : (csreg, xlenbits) -> unit +val csr_read_callback = pure {ocaml: "Platform.csr_read_callback", c: "csr_read_callback"} : (csreg, xlenbits) -> unit diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index a80e4eba4..60198d4ae 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -169,7 +169,7 @@ function wV (r : regno, in_v : vregtype) -> unit = { let VLEN = unsigned(vlenb) * 8; assert(0 < VLEN & VLEN <= sizeof(vlenmax)); - if rv_enable_callbacks then vreg_update_callback(regno_to_regidx(r), v); + vreg_write_callback(regno_to_regidx(r), v); } function rV_bits(i: regidx) -> vregtype = rV(unsigned(i)) diff --git a/model/riscv_vreg_type.sail b/model/riscv_vreg_type.sail index 79190955c..5ab69305a 100755 --- a/model/riscv_vreg_type.sail +++ b/model/riscv_vreg_type.sail @@ -150,4 +150,4 @@ enum vmlsop = { VLM, VSM } /* Callbacks for vregs state-changing events */ /* Default for this function in riscv_default_callbacks.c and platform_impl.ml */ -val vreg_update_callback = pure {ocaml: "Platform.vreg_update_callback", c: "vreg_update_callback"} : (regidx, vregtype) -> unit +val vreg_write_callback = pure {ocaml: "Platform.vreg_write_callback", c: "vreg_write_callback"} : (regidx, vregtype) -> unit diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail index 5afb685fb..99b88a70e 100644 --- a/model/rvfi_dii.sail +++ b/model/rvfi_dii.sail @@ -330,12 +330,10 @@ function print_rvfi_exec () = { val internal_error : forall ('a : Type). (string, int, string) -> 'a -val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n), bool) -> unit -function rvfi_write (addr, width, value, is_exception) = { +val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, int('n), bits(8 * 'n)) -> unit +function rvfi_write (addr, width, value) = { rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; - /* Log only the memory address (without the value) if the write fails. */ - if is_exception == false then { if width <= 16 then { /* TODO: report tag bit for capability writes and extend mask by one bit. */ rvfi_mem_data[rvfi_mem_wdata] = sail_zero_extend(value, 256); @@ -343,15 +341,12 @@ function rvfi_write (addr, width, value, is_exception) = { } else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!"); }; - }; } -val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n), bool) -> unit -function rvfi_read (addr, width, value, is_exception) = { +val rvfi_read : forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> unit +function rvfi_read (addr, width, value) = { rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); rvfi_mem_data_present = true; - /* Log only the memory address (without the value) if the write fails. */ - if is_exception == false then { if width <= 16 then { /* TODO: report tag bit for capability writes and extend mask by one bit. */ rvfi_mem_data[rvfi_mem_rdata] = sail_zero_extend(value, 256); @@ -359,7 +354,13 @@ function rvfi_read (addr, width, value, is_exception) = { } else { internal_error(__FILE__, __LINE__, "Expected at most 16 bytes here!") }; - }; +} + +val rvfi_mem_exception : xlenbits -> unit +function rvfi_mem_exception (addr) = { + /* Log only the memory address (without the value) if the write fails. */ + rvfi_mem_data[rvfi_mem_addr] = zero_extend(addr); + rvfi_mem_data_present = true; } val rvfi_wX : forall 'n, 0 <= 'n < 32. (int('n), xlenbits) -> unit diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 8a6632c9b..0c8422641 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -25,14 +25,15 @@ let platform_arch = ref P.RV64 (* Defaults for callbacks functions. The model assumes that these functions do not change the state of the model. *) -let mem_update_callback (addr, width, value, is_exception) = () -let mem_read_callback (addr, width, value, is_exception) = () -let pc_update_callback value = () -let xreg_update_callback (reg, value) = () -let freg_update_callback (reg, value) = () -let csr_update_callback (reg_name, value) = () -let csr_read_callback (reg_name, value) = () -let vreg_update_callback (reg, value) = () +let mem_write_callback (addr, width, value) = () +let mem_read_callback (addr, width, value) = () +let mem_exception_callback (addr, num_of_exception) = () +let pc_write_callback value = () +let xreg_write_callback (reg, value) = () +let freg_write_callback (reg, value) = () +let csr_write_callback (reg, value) = () +let csr_read_callback (reg, value) = () +let vreg_write_callback (reg, value) = () (* logging *)