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