diff --git a/Makefile b/Makefile index 3f33425ec..6513af121 100644 --- a/Makefile +++ b/Makefile @@ -103,9 +103,11 @@ SAIL_ARCH_SRCS = $(PRELUDE) SAIL_ARCH_SRCS += riscv_types_common.sail riscv_types_ext.sail riscv_types.sail SAIL_ARCH_SRCS += riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail SAIL_ARCH_SRCS += riscv_mem.sail $(SAIL_VM_SRCS) +SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types_common.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS) riscv_types_kext.sail SAIL_ARCH_SRCS += riscv_types_kext.sail # Shared/common code for the cryptography extension. SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail +RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail SAIL_OTHER_SRCS = $(SAIL_STEP_SRCS) ifeq ($(ARCH),RV32) @@ -117,6 +119,7 @@ endif PRELUDE_SRCS = $(addprefix model/,$(PRELUDE)) SAIL_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_SRCS)) SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_RMEM_INST_SRCS) $(SAIL_OTHER_SRCS)) +SAIL_RVFI_SRCS = $(addprefix model/,$(SAIL_ARCH_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) $(RVFI_STEP_SRCS)) SAIL_COQ_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_COQ_SRCS)) PLATFORM_OCAML_SRCS = $(addprefix ocaml_emulator/,platform.ml platform_impl.ml softfloat.ml riscv_ocaml_sim.ml) @@ -271,10 +274,41 @@ $(SOFTFLOAT_LIBS): csim: c_emulator/riscv_sim_$(ARCH) .PHONY: osim osim: ocaml_emulator/riscv_ocaml_sim_$(ARCH) +.PHONY: rvfi +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 gcc -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 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) @@ -453,7 +487,7 @@ clean: -rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/* -rm -rf generated_definitions/for-rmem/* -$(MAKE) -C $(SOFTFLOAT_LIBDIR) clean - -rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 + -rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 c_emulator/riscv_rvfi_RV32 c_emulator/riscv_rvfi_RV64 -rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 ocaml_emulator/tracecmp -rm -f *.gcno *.gcda -rm -f z3_problems diff --git a/c_emulator/riscv_default_callbacks.c b/c_emulator/riscv_default_callbacks.c index 6967ab862..d4600321c 100644 --- a/c_emulator/riscv_default_callbacks.c +++ b/c_emulator/riscv_default_callbacks.c @@ -1,18 +1,16 @@ /* The model assumes that these functions do not change the state of the model. */ -int __attribute__((weak)) -mem_update_callback(uint64_t addr, uint64_t width, lbits data) +int mem_update_callback(uint64_t addr, uint64_t width, lbits value, + bool is_exception) { } -int __attribute__((weak)) xreg_update_callback(unsigned reg, uint64_t value) { } -int __attribute__((weak)) freg_update_callback(unsigned reg, uint64_t value) { } -int __attribute__((weak)) -csr_update_callback(const char *reg_name, uint64_t value) +int mem_read_callback(uint64_t addr, uint64_t width, lbits value, + bool is_exception) { } -int __attribute__((weak)) -csr_read_callback(const char *reg_name, uint64_t value) -{ -} -int __attribute__((weak)) vreg_update_callback(unsigned reg, lbits value) { } -int __attribute__((weak)) pc_update_callback(uint64_t value) { } +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 b72496ff3..5944b346f 100644 --- a/c_emulator/riscv_sail.h +++ b/c_emulator/riscv_sail.h @@ -23,6 +23,28 @@ unit z_set_Misa_C(struct zMisa *, mach_bits); unit z_set_Misa_D(struct zMisa *, mach_bits); unit z_set_Misa_F(struct zMisa *, mach_bits); +#ifdef RVFI_DII +unit zext_rvfi_init(unit); +unit zrvfi_set_instr_packet(mach_bits); +mach_bits zrvfi_get_cmd(unit); +mach_bits zrvfi_get_insn(unit); +bool zrvfi_step(sail_int); +unit zrvfi_zzero_exec_packet(unit); +unit zrvfi_halt_exec_packet(unit); +void zrvfi_get_exec_packet_v1(sail_bits *rop, unit); +void zrvfi_get_exec_packet_v2(sail_bits *rop, unit); +extern bool zrvfi_int_data_present; +void zrvfi_get_int_data(sail_bits *rop, unit); +extern bool zrvfi_mem_data_present; +void zrvfi_get_mem_data(sail_bits *rop, unit); +mach_bits zrvfi_get_v2_trace_sizze(unit); +void zrvfi_get_v2_support_packet(sail_bits *rop, unit); + +// Debugging prints +unit zprint_rvfi_exec(unit); +unit zprint_instr_packet(uint64_t); +#endif + extern mach_bits zxlen_val; extern bool zhtif_done; extern mach_bits zhtif_exit_code; @@ -34,11 +56,14 @@ extern bool have_exception; 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 data); +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); +int vreg_update_callback(unsigned reg, lbits value); int pc_update_callback(uint64_t value); /* machine state */ diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index f30baa260..3a9bfc08d 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -65,6 +65,14 @@ FILE *trace_log = NULL; char *dtb_file = NULL; unsigned char *dtb = NULL; size_t dtb_len = 0; +#ifdef RVFI_DII +static bool rvfi_dii = false; +/* Needs to be global to avoid the needed for a set-version packet on each trace + */ +static unsigned rvfi_trace_version = 1; +static int rvfi_dii_port; +static int rvfi_dii_sock; +#endif unsigned char *spike_dtb = NULL; size_t spike_dtb_len = 0; @@ -129,6 +137,9 @@ static struct option options[] = { {"report-arch", no_argument, 0, 'a' }, {"test-signature", required_argument, 0, 'T' }, {"signature-granularity", required_argument, 0, 'g' }, +#ifdef RVFI_DII + {"rvfi-dii", required_argument, 0, 'r' }, +#endif {"help", no_argument, 0, 'h' }, {"trace", optional_argument, 0, 'v' }, {"no-trace", optional_argument, 0, 'V' }, @@ -147,6 +158,9 @@ static struct option options[] = { static void print_usage(const char *argv0, int ec) { fprintf(stdout, "Usage: %s [options] [ ...]\n", argv0); +#ifdef RVFI_DII + fprintf(stdout, " %s [options] -r \n", argv0); +#endif struct option *opt = options; while (opt->name) { if (isprint(opt->val)) @@ -251,6 +265,9 @@ static int process_args(int argc, char **argv) "T:" "g:" "h" +#ifdef RVFI_DII + "r:" +#endif #ifdef SAILCOV "c:" #endif @@ -357,6 +374,13 @@ static int process_args(int argc, char **argv) case 'h': print_usage(argv[0], 0); break; +#ifdef RVFI_DII + case 'r': + rvfi_dii = true; + rvfi_dii_port = atoi(optarg); + fprintf(stderr, "using %d as RVFI port.\n", rvfi_dii_port); + break; +#endif case 'V': set_config_print(optarg, false); break; @@ -391,14 +415,22 @@ static int process_args(int argc, char **argv) } if (do_dump_dts) dump_dts(); +#ifdef RVFI_DII + if (optind > argc || (optind == argc && !rvfi_dii)) + print_usage(argv[0], 0); +#else if (optind >= argc) { fprintf(stderr, "No elf file provided.\n"); print_usage(argv[0], 0); } +#endif if (dtb_file) read_dtb(dtb_file); - fprintf(stdout, "Running file %s.\n", argv[optind]); +#ifdef RVFI_DII + if (!rvfi_dii) +#endif + fprintf(stdout, "Running file %s.\n", argv[optind]); return optind; } @@ -583,7 +615,20 @@ void preinit_sail() void init_sail(uint64_t elf_entry) { zinit_model(UNIT); - init_sail_reset_vector(elf_entry); +#ifdef RVFI_DII + if (rvfi_dii) { + zext_rvfi_init(UNIT); + rv_ram_base = UINT64_C(0x80000000); + rv_ram_size = UINT64_C(0x800000); + rv_rom_base = UINT64_C(0); + rv_rom_size = UINT64_C(0); + rv_clint_base = UINT64_C(0); + rv_clint_size = UINT64_C(0); + rv_htif_tohost = UINT64_C(0); + zPC = elf_entry; + } else +#endif + init_sail_reset_vector(elf_entry); // this is probably unnecessary now; remove if (!rv_enable_rvc) @@ -747,6 +792,66 @@ void flush_logs(void) } } +#ifdef RVFI_DII + +typedef void (*packet_reader_fn)(lbits *rop, unit); +static void get_and_send_rvfi_packet(packet_reader_fn reader) +{ + lbits packet; + CREATE(lbits)(&packet); + reader(&packet, UNIT); + /* Note: packet.len is the size in bits, not bytes. */ + if (packet.len % 8 != 0) { + fprintf(stderr, "RVFI-DII trace packet not byte aligned: %d\n", + (int)packet.len); + exit(1); + } + const size_t send_size = packet.len / 8; + if (config_print_rvfi) { + print_bits("packet = ", packet); + fprintf(stderr, "Sending packet with length %zd... ", send_size); + } + if (send_size > 4096) { + fprintf(stderr, "Unexpected large packet size (> 4KB): %zd\n", send_size); + exit(1); + } + unsigned char bytes[send_size]; + /* mpz_export might not write all of the null bytes */ + memset(bytes, 0, sizeof(bytes)); + mpz_export(bytes, NULL, -1, 1, 0, 0, *(packet.bits)); + /* Ensure that we can send a full packet */ + if (write(rvfi_dii_sock, bytes, send_size) != send_size) { + fprintf(stderr, "Writing RVFI DII trace failed: %s\n", strerror(errno)); + exit(1); + } + if (config_print_rvfi) { + fprintf(stderr, "Wrote %zd byte response to socket.\n", send_size); + } + KILL(lbits)(&packet); +} + +void rvfi_send_trace(unsigned version) +{ + if (config_print_rvfi) { + fprintf(stderr, "Sending v%d trace response...\n", version); + } + if (version == 1) { + get_and_send_rvfi_packet(zrvfi_get_exec_packet_v1); + } else if (version == 2) { + mach_bits trace_size = zrvfi_get_v2_trace_sizze(UNIT); + get_and_send_rvfi_packet(zrvfi_get_exec_packet_v2); + if (zrvfi_int_data_present) + get_and_send_rvfi_packet(zrvfi_get_int_data); + if (zrvfi_mem_data_present) + get_and_send_rvfi_packet(zrvfi_get_mem_data); + } else { + fprintf(stderr, "Sending v%d packets not implemented yet!\n", version); + abort(); + } +} + +#endif + void run_sail(void) { bool spike_done; @@ -756,6 +861,9 @@ void run_sail(void) /* initialize the step number */ mach_int step_no = 0; int insn_cnt = 0; +#ifdef RVFI_DII + bool need_instr = true; +#endif struct timeval interval_start; if (gettimeofday(&interval_start, NULL) < 0) { @@ -764,6 +872,105 @@ void run_sail(void) } while (!zhtif_done && (insn_limit == 0 || total_insns < insn_limit)) { +#ifdef RVFI_DII + if (rvfi_dii) { + mach_bits instr_bits; + if (config_print_rvfi) { + fprintf(stderr, "Waiting for cmd packet... "); + } + int res = read(rvfi_dii_sock, &instr_bits, sizeof(instr_bits)); + if (config_print_rvfi) { + fprintf(stderr, "Read cmd packet: %016jx\n", (intmax_t)instr_bits); + zprint_instr_packet(instr_bits); + } + if (res == 0) { + if (config_print_rvfi) { + fprintf(stderr, "Got EOF, exiting... "); + } + rvfi_dii = false; + return; + } + if (res == -1) { + fprintf(stderr, "Reading RVFI DII command failed: %s", strerror(errno)); + exit(1); + } + if (res < sizeof(instr_bits)) { + fprintf(stderr, "Reading RVFI DII command failed: insufficient input"); + exit(1); + } + zrvfi_set_instr_packet(instr_bits); + zrvfi_zzero_exec_packet(UNIT); + mach_bits cmd = zrvfi_get_cmd(UNIT); + switch (cmd) { + case 0: { /* EndOfTrace */ + if (config_print_rvfi) { + fprintf(stderr, "Got EndOfTrace packet.\n"); + } + mach_bits insn = zrvfi_get_insn(UNIT); + if (insn == (('V' << 24) | ('E' << 16) | ('R' << 8) | 'S')) { + /* + * Reset with insn set to 'VERS' is a version negotiation request + * and not a actual reset request. Respond with a message say that + * we support version 2. + */ + if (config_print_rvfi) { + fprintf(stderr, + "EndOfTrace was actually a version negotiation packet.\n"); + } + get_and_send_rvfi_packet(&zrvfi_get_v2_support_packet); + continue; + } else { + zrvfi_halt_exec_packet(UNIT); + rvfi_send_trace(rvfi_trace_version); + return; + } + } + case 1: /* Instruction */ + break; + case 'v': { /* Set wire format version */ + mach_bits insn = zrvfi_get_insn(UNIT); + if (config_print_rvfi) { + fprintf(stderr, "Got request for v%jd trace format!\n", + (intmax_t)insn); + } + if (insn == 1) { + fprintf(stderr, "Requested trace in legacy format!\n"); + } else if (insn == 2) { + fprintf(stderr, "Requested trace in v2 format!\n"); + } else { + fprintf(stderr, "Requested trace in unsupported format %jd!\n", + (intmax_t)insn); + exit(1); + } + rvfi_trace_version + = insn; // From now on send traces in the requested format + struct { + char msg[8]; + uint64_t version; + } version_response = {"version=", rvfi_trace_version}; + if (write(rvfi_dii_sock, &version_response, sizeof(version_response)) + != sizeof(version_response)) { + fprintf(stderr, "Sending version response failed: %s\n", + strerror(errno)); + exit(1); + } + continue; + } + default: + fprintf(stderr, "Unknown RVFI-DII command: %#02x\n", (int)cmd); + exit(1); + } + sail_int sail_step; + CREATE(sail_int)(&sail_step); + CONVERT_OF(sail_int, mach_int)(&sail_step, step_no); + stepped = zstep(sail_step); + if (have_exception) + goto step_exception; + flush_logs(); + KILL(sail_int)(&sail_step); + rvfi_send_trace(rvfi_trace_version); + } else /* if (!rvfi_dii) */ +#endif { /* run a Sail step */ sail_int sail_step; CREATE(sail_int)(&sail_step); @@ -893,7 +1100,68 @@ int main(int argc, char **argv) exit(1); } +#ifdef RVFI_DII + uint64_t entry; + if (rvfi_dii) { + entry = 0x80000000; + int listen_sock = socket(AF_INET, SOCK_STREAM, 0); + if (listen_sock == -1) { + fprintf(stderr, "Unable to create socket: %s\n", strerror(errno)); + return 1; + } + int reuseaddr = 1; + if (setsockopt(listen_sock, SOL_SOCKET, SO_REUSEADDR, &reuseaddr, + sizeof(reuseaddr)) + == -1) { + fprintf(stderr, "Unable to set reuseaddr on socket: %s\n", + strerror(errno)); + return 1; + } + struct sockaddr_in addr = {.sin_family = AF_INET, + .sin_addr.s_addr = htonl(INADDR_LOOPBACK), + .sin_port = htons(rvfi_dii_port)}; + if (bind(listen_sock, (struct sockaddr *)&addr, sizeof(addr)) == -1) { + fprintf(stderr, "Unable to set bind socket: %s\n", strerror(errno)); + return 1; + } + if (listen(listen_sock, 1) == -1) { + fprintf(stderr, "Unable to listen on socket: %s\n", strerror(errno)); + return 1; + } + socklen_t addrlen = sizeof(addr); + if (getsockname(listen_sock, (struct sockaddr *)&addr, &addrlen) == -1) { + fprintf(stderr, "Unable to getsockname() on socket: %s\n", + strerror(errno)); + return 1; + } + printf("Waiting for connection on port %d.\n", ntohs(addr.sin_port)); + rvfi_dii_sock = accept(listen_sock, NULL, NULL); + if (rvfi_dii_sock == -1) { + fprintf(stderr, "Unable to accept connection on socket: %s\n", + strerror(errno)); + return 1; + } + close(listen_sock); + // Ensure that the socket is blocking + int fd_flags = fcntl(rvfi_dii_sock, F_GETFL); + if (fd_flags == -1) { + fprintf(stderr, "Failed to get file descriptor flags for socket!\n"); + return 1; + } + if (config_print_rvfi) { + fprintf(stderr, "RVFI socket fd flags=%d, nonblocking=%d\n", fd_flags, + (fd_flags & O_NONBLOCK) != 0); + } + if (fd_flags & O_NONBLOCK) { + fprintf(stderr, "Socket was non-blocking, this will not work!\n"); + return 1; + } + printf("Connected\n"); + } else + entry = load_sail(initial_elf_file, /*main_file=*/true); +#else uint64_t entry = load_sail(initial_elf_file, /*main_file=*/true); +#endif /* Load any additional ELF files into memory */ for (int i = files_start + 1; i < argc; i++) { fprintf(stdout, "Loading additional ELF file %s.\n", argv[i]); @@ -914,8 +1182,17 @@ int main(int argc, char **argv) exit(1); } - run_sail(); - + do { + run_sail(); +#ifndef RVFI_DII + } while (0); +#else + if (rvfi_dii) { + /* Reset for next test */ + reinit_sail(entry); + } + } while (rvfi_dii); +#endif model_fini(); flush_logs(); close_logs(); diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail index 1bdb26d82..0f5aba103 100644 --- a/model/riscv_ext_regs.sail +++ b/model/riscv_ext_regs.sail @@ -13,6 +13,15 @@ val ext_init_regs : unit -> unit function ext_init_regs () = () +/*! +This function is called after above when running rvfi and allows the model +to be initialised differently (e.g. CHERI cap regs are initialised +to omnipotent instead of null). + */ +val ext_rvfi_init : unit -> unit +function ext_rvfi_init () = { + x1 = x1 // to avoid hook being optimized out +} /*! THIS(csrno, priv, isWrite) allows an extension to block access to csrno, diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail new file mode 100644 index 000000000..d25237572 --- /dev/null +++ b/model/riscv_fetch_rvfi.sail @@ -0,0 +1,45 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +function fetch() -> FetchResult = { + rvfi_inst_data[rvfi_order] = minstret; + rvfi_pc_data[rvfi_pc_rdata] = zero_extend(get_arch_pc()); + rvfi_inst_data[rvfi_mode] = zero_extend(privLevel_to_bits(cur_privilege)); + rvfi_inst_data[rvfi_ixl] = zero_extend(misa[MXL]); + + /* First allow extensions to check pc */ + match ext_fetch_check_pc(PC, PC) { + Ext_FetchAddr_Error(e) => F_Ext_Error(e), + Ext_FetchAddr_OK(use_pc) => { + /* then check PC alignment */ + if (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(haveRVC()))) + then F_Error(E_Fetch_Addr_Align(), PC) + else match translateAddr(use_pc, Execute()) { + TR_Failure(e, _) => F_Error(e, PC), + TR_Address(_, _) => { + let i = rvfi_instruction[rvfi_insn]; + rvfi_inst_data->rvfi_insn() = zero_extend(i); + if (i[1 .. 0] != 0b11) + then F_RVC(i[15 .. 0]) + else { + /* fetch PC check for the next instruction granule */ + PC_hi : xlenbits = PC + 2; + match ext_fetch_check_pc(PC, PC_hi) { + Ext_FetchAddr_Error(e) => F_Ext_Error(e), + Ext_FetchAddr_OK(use_pc_hi) => + match translateAddr(use_pc_hi, Execute()) { + TR_Failure(e, _) => F_Error(e, PC), + TR_Address(_, _) => F_Base(i) + } + } + } + } + } + } + } +} diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index c6324764b..097669db7 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -132,6 +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) }; + 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 } @@ -201,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); - if rv_enable_callbacks then mem_update_callback(paddr, width, value); + 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_platform.sail b/model/riscv_platform.sail index 030e1ee5b..19e3d30ae 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -384,11 +384,19 @@ function htif_tick() = { } /* Top-level MMIO dispatch */ +$ifndef RVFI_DII function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = within_clint(addr, width) | (within_htif_readable(addr, width) & 1 <= 'n) +$else +function within_mmio_readable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = false +$endif +$ifndef RVFI_DII function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = within_clint(addr, width) | (within_htif_writable(addr, width) & 'n <= 8) +$else +function within_mmio_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlenbits, width : int('n)) -> bool = false +$endif function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_access_type), paddr : xlenbits, width : int('n)) -> MemoryOpResult(bits(8 * 'n)) = if within_clint(paddr, width) diff --git a/model/riscv_step_rvfi.sail b/model/riscv_step_rvfi.sail new file mode 100644 index 000000000..caa0d8d80 --- /dev/null +++ b/model/riscv_step_rvfi.sail @@ -0,0 +1,28 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* Step hooks for rvfi. */ + +function ext_fetch_hook(f : FetchResult) -> FetchResult = f + +function ext_pre_step_hook() -> unit = () + +function ext_post_step_hook() -> unit = { + /* record the next pc */ + rvfi_pc_data->rvfi_pc_wdata() = zero_extend(get_arch_pc()) +} + +val ext_init : unit -> unit +function ext_init() = { + init_base_regs(); + init_fdext_regs(); + /* these are here so that the C backend doesn't prune them out. */ + // let _ = rvfi_step(0); + ext_rvfi_init(); + () +} diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 2dbadb1be..c794616ce 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -303,10 +303,21 @@ function tval(excinfo : option(xlenbits)) -> xlenbits = { } } +$ifdef RVFI_DII +val rvfi_trap : unit -> unit +// TODO: record rvfi_trap_data +function rvfi_trap () = + rvfi_inst_data[rvfi_trap] = 0x01 +$else +val rvfi_trap : unit -> unit +function rvfi_trap () = () +$endif + /* handle exceptional ctl flow by updating nextPC and operating privilege */ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits), ext : option(ext_exception)) -> xlenbits = { + rvfi_trap(); if get_config_print_platform() then print_platform("handling " ^ (if intr then "int#" else "exc#") ^ BitStr(c) ^ " at priv " ^ to_str(del_priv) diff --git a/model/riscv_types.sail b/model/riscv_types.sail index c90bd94ae..e0a92f82b 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -415,11 +415,16 @@ 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), /* data */ bits(8 * 'n)) -> unit +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 diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail new file mode 100644 index 000000000..5afb685fb --- /dev/null +++ b/model/rvfi_dii.sail @@ -0,0 +1,370 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +// "RISC-V Formal Interface - Direct Instruction Injection" support +// For use with https://github.com/CTSRD-CHERI/TestRIG + +$define RVFI_DII + +bitfield RVFI_DII_Instruction_Packet : bits(64) = { + padding : 63 .. 56, // [7] + rvfi_cmd : 55 .. 48, // [6] This token is a trace command. For example, reset device under test. + rvfi_time : 47 .. 32, // [5 - 4] Time to inject token. The difference between this and the previous + // instruction time gives a delay before injecting this instruction. + // This can be ignored for models but gives repeatability for implementations + // while shortening counterexamples. + rvfi_insn : 31 .. 0, // [0 - 3] Instruction word: 32-bit instruction or command. The lower 16-bits + // may decode to a 16-bit compressed instruction. +} + +register rvfi_instruction : RVFI_DII_Instruction_Packet + +val rvfi_set_instr_packet : bits(64) -> unit + +function rvfi_set_instr_packet(p) = + rvfi_instruction = Mk_RVFI_DII_Instruction_Packet(p) + +val rvfi_get_cmd : unit -> bits(8) + +function rvfi_get_cmd () = rvfi_instruction[rvfi_cmd] + +val rvfi_get_insn : unit -> bits(32) + +function rvfi_get_insn () = rvfi_instruction[rvfi_insn] + +val print_instr_packet : bits(64) -> unit + +function print_instr_packet(bs) = { + let p = Mk_RVFI_DII_Instruction_Packet(bs); + print_bits("command ", p[rvfi_cmd]); + print_bits("instruction ", p[rvfi_insn]) +} + +bitfield RVFI_DII_Execution_Packet_V1 : bits(704) = { + rvfi_intr : 703 .. 696, // [87] Trap handler: Set for first instruction in trap handler. + rvfi_halt : 695 .. 688, // [86] Halt indicator: Marks the last instruction retired + // before halting execution. + rvfi_trap : 687 .. 680, // [85] Trap indicator: Invalid decode, misaligned access or + // jump command to misaligned address. + rvfi_rd_addr : 679 .. 672, // [84] Write register address: MUST be 0 if not used. + rvfi_rs2_addr : 671 .. 664, // [83] otherwise set as decoded. + rvfi_rs1_addr : 663 .. 656, // [82] Read register addresses: Can be arbitrary when not used, + rvfi_mem_wmask : 655 .. 648, // [81] Write mask: Indicates valid bytes written. 0 if unused. + rvfi_mem_rmask : 647 .. 640, // [80] Read mask: Indicates valid bytes read. 0 if unused. + rvfi_mem_wdata : 639 .. 576, // [72 - 79] Write data: Data written to memory by this command. + rvfi_mem_rdata : 575 .. 512, // [64 - 71] Read data: Data read from mem_addr (i.e. before write) + rvfi_mem_addr : 511 .. 448, // [56 - 63] Memory access addr: Points to byte address (aligned if define + // is set). *Should* be straightforward. + // 0 if unused. + rvfi_rd_wdata : 447 .. 384, // [48 - 55] Write register value: MUST be 0 if rd_ is 0. + rvfi_rs2_data : 383 .. 320, // [40 - 47] above. Must be 0 if register ID is 0. + rvfi_rs1_data : 319 .. 256, // [32 - 39] Read register values: Values as read from registers named + rvfi_insn : 255 .. 192, // [24 - 31] Instruction word: 32-bit command value. + rvfi_pc_wdata : 191 .. 128, // [16 - 23] PC after instr: Following PC - either PC + 4 or jump/trap target. + rvfi_pc_rdata : 127 .. 64, // [08 - 15] PC before instr: PC for current instruction + rvfi_order : 63 .. 0, // [00 - 07] Instruction number: INSTRET value after completion. +} + +bitfield RVFI_DII_Execution_Packet_InstMetaData : bits(192) = { + /// The rvfi_order field must be set to the instruction index. No indices + /// must be used twice and there must be no gaps. Instructions may be + /// retired in a reordered fashion, as long as causality is preserved + /// (register and memory write operations must be retired before the read + /// operations that depend on them). + rvfi_order : 63 .. 0, + /// rvfi_insn is the instruction word for the retired instruction. In case + /// of an instruction with fewer than ILEN bits, the upper bits of this + /// output must be all zero. For compressed instructions the compressed + /// instruction word must be output on this port. For fused instructions the + /// complete fused instruction sequence must be output. + rvfi_insn : 127 .. 64, + /// rvfi_trap must be set for an instruction that cannot be decoded as a + /// legal instruction, such as 0x00000000. + /// In addition, rvfi_trap must be set for a misaligned memory read or + /// write in PMAs that don't allow misaligned access, or other memory + /// access violations. rvfi_trap must also be set for a jump instruction + /// that jumps to a misaligned instruction. + rvfi_trap : 135 .. 128, + /// The signal rvfi_halt must be set when the instruction is the last + /// instruction that the core retires before halting execution. It should not + /// be set for an instruction that triggers a trap condition if the CPU + /// reacts to the trap by executing a trap handler. This signal enables + /// verification of liveness properties. + rvfi_halt : 143 .. 136, + /// rvfi_intr must be set for the first instruction that is part of a trap + /// handler, i.e. an instruction that has a rvfi_pc_rdata that does not + /// match the rvfi_pc_wdata of the previous instruction. + rvfi_intr : 151 .. 144, + /// rvfi_mode must be set to the current privilege level, using the following + /// encoding: 0=U-Mode, 1=S-Mode, 2=Reserved, 3=M-Mode + rvfi_mode : 159 .. 152, + /// rvfi_ixl must be set to the value of MXL/SXL/UXL in the current privilege level, + /// using the following encoding: 1=32, 2=64 + rvfi_ixl : 167 .. 160, + + /// When the core retires an instruction, it asserts the rvfi_valid signal + /// and uses the signals described below to output the details of the + /// retired instruction. The signals below are only valid during such a + /// cycle and can be driven to arbitrary values in a cycle in which + /// rvfi_valid is not asserted. + rvfi_valid : 175 .. 168, + // Note: since we only send these packets in the valid state, we could + // omit the valid signal, but we need 3 bytes of padding after ixl anyway + // so we might as well include it + padding : 191 .. 176, +} + +bitfield RVFI_DII_Execution_Packet_PC : bits(128) = { + /// This is the program counter (pc) before (rvfi_pc_rdata) and after + /// (rvfi_pc_wdata) execution of this instruction. I.e. this is the address + /// of the retired instruction and the address of the next instruction. + rvfi_pc_rdata : 63 .. 0, + rvfi_pc_wdata : 127 .. 64, +} + +bitfield RVFI_DII_Execution_Packet_Ext_Integer : bits(320) = { + magic : 63 .. 0, // must be "int-data" + /// rvfi_rd_wdata is the value of the x register addressed by rd after + /// execution of this instruction. This output must be zero when rd is zero. + rvfi_rd_wdata : 127 .. 64, + /// rvfi_rs1_rdata/rvfi_rs2_rdata is the value of the x register addressed + /// by rs1/rs2 before execution of this instruction. This output must be + /// zero when rs1/rs2 is zero. + rvfi_rs1_rdata : 191 .. 128, + rvfi_rs2_rdata : 255 .. 192, + /// rvfi_rd_addr is the decoded rd register address for the retired + /// instruction. For an instruction that writes no rd register, this output + /// must always be zero. + rvfi_rd_addr : 263 .. 256, + /// rvfi_rs1_addr and rvfi_rs2_addr are the decoded rs1 and rs1 register + /// addresses for the retired instruction. For an instruction that reads no + /// rs1/rs2 register, this output can have an arbitrary value. However, if + /// this output is nonzero then rvfi_rs1_rdata must carry the value stored + /// in that register in the pre-state. + rvfi_rs1_addr : 271 .. 264, + rvfi_rs2_addr : 279 .. 272, + padding : 319 .. 280, +} + +bitfield RVFI_DII_Execution_Packet_Ext_MemAccess : bits(704) = { + magic : 63 .. 0, // must be "mem-data" + /// rvfi_mem_rdata is the pre-state data read from rvfi_mem_addr. + /// rvfi_mem_rmask specifies which bytes are valid. + /// CHERI-extension: widened to 32 bytes to allow reporting 129 bits + rvfi_mem_rdata : 319 .. 64, + /// rvfi_mem_wdata is the post-state data written to rvfi_mem_addr. + /// rvfi_mem_wmask specifies which bytes are valid. + /// CHERI-extension: widened to 32 bytes to allow reporting 129 bits + rvfi_mem_wdata : 575 .. 320, + /// rvfi_mem_rmask is a bitmask that specifies which bytes in rvfi_mem_rdata + /// contain valid read data from rvfi_mem_addr. + /// CHERI-extension: we extend rmask+wmask to 32 bits to allow reporting the + /// mask for CHERI/RV128 accesses here. + rvfi_mem_rmask : 607 .. 576, + /// rvfi_mem_wmask is a bitmask that specifies which bytes in rvfi_mem_wdata + /// contain valid data that is written to rvfi_mem_addr. + /// CHERI-extension: widened to 32 bits + rvfi_mem_wmask : 639 .. 608, + /// For memory operations (rvfi_mem_rmask and/or rvfi_mem_wmask are + /// non-zero), rvfi_mem_addr holds the accessed memory location. + rvfi_mem_addr : 703 .. 640, +} + +bitfield RVFI_DII_Execution_PacketV2 : bits(512) = { + magic : 63 .. 0, // must be set to 'trace-v2' + trace_size : 127 .. 64, // total size of the trace packet + extensions + basic_data : 319 .. 128, // RVFI_DII_Execution_Packet_InstMetaData + pc_data : 447 .. 320, // RVFI_DII_Execution_Packet_PC + // available_fields : 511 .. 448, + integer_data_available: 448, // Followed by RVFI_DII_Execution_Packet_Ext_Integer if set + memory_access_data_available: 449, // Followed by R VFI_DII_Execution_Packet_Ext_MemAccess if set + floating_point_data_available: 450, // TODO: Followed by RVFI_DII_Execution_Packet_Ext_FP if set + csr_read_write_data_available: 451, // TODO: Followed by RVFI_DII_Execution_Packet_Ext_CSR if set + cheri_data_available: 452, // TODO: Followed by RVFI_DII_Execution_Packet_Ext_CHERI if set + cheri_scr_read_write_data_available: 453, // TODO: Followed by RVFI_DII_Execution_Packet_Ext_CHERI_SCR if set + trap_data_available: 454, // TODO: Followed by RVFI_DII_Execution_Packet_Ext_Trap if set + unused_data_available_fields : 511 .. 455, // To be used for additional RVFI_DII_Execution_Packet_Ext_* structs +} + +register rvfi_inst_data : RVFI_DII_Execution_Packet_InstMetaData +register rvfi_pc_data : RVFI_DII_Execution_Packet_PC +register rvfi_int_data : RVFI_DII_Execution_Packet_Ext_Integer +register rvfi_int_data_present : bool +register rvfi_mem_data : RVFI_DII_Execution_Packet_Ext_MemAccess +register rvfi_mem_data_present : bool + +// Reset the trace +val rvfi_zero_exec_packet : unit -> unit + +function rvfi_zero_exec_packet () = { + rvfi_inst_data = Mk_RVFI_DII_Execution_Packet_InstMetaData(zero_extend(0b0)); + rvfi_pc_data = Mk_RVFI_DII_Execution_Packet_PC(zero_extend(0b0)); + rvfi_int_data = Mk_RVFI_DII_Execution_Packet_Ext_Integer(zero_extend(0x0)); + // magic = "int-data" -> 0x617461642d746e69 (big-endian) + rvfi_int_data = update_magic(rvfi_int_data, 0x617461642d746e69); + rvfi_int_data_present = false; + rvfi_mem_data = Mk_RVFI_DII_Execution_Packet_Ext_MemAccess(zero_extend(0x0)); + // magic = "mem-data" -> 0x617461642d6d656d (big-endian) + rvfi_mem_data = update_magic(rvfi_mem_data, 0x617461642d6d656d); + rvfi_mem_data_present = false; +} + +// FIXME: most of these will no longer be necessary once we use the c2 sail backend. + +val rvfi_halt_exec_packet : unit -> unit + +function rvfi_halt_exec_packet () = + rvfi_inst_data->rvfi_halt() = 0x01 + +val rvfi_get_v2_support_packet : unit -> bits(704) +function rvfi_get_v2_support_packet () = { + let rvfi_exec = Mk_RVFI_DII_Execution_Packet_V1(zero_extend(0b0)); + // Returning 0x3 (using the unused high bits) in halt instead of 0x1 means + // that we support the version 2 wire format. This is required to keep + // backwards compatibility with old implementations that do not support + // the new trace format. + let rvfi_exec = update_rvfi_halt(rvfi_exec, 0x03); + return rvfi_exec.bits; +} + +val rvfi_get_exec_packet_v1 : unit -> bits(704) +function rvfi_get_exec_packet_v1 () = { + let v1_packet = Mk_RVFI_DII_Execution_Packet_V1(zero_extend(0b0)); + // Convert the v2 packet to a v1 packet + let v1_packet = update_rvfi_intr(v1_packet, rvfi_inst_data[rvfi_intr]); + let v1_packet = update_rvfi_halt(v1_packet, rvfi_inst_data[rvfi_halt]); + let v1_packet = update_rvfi_trap(v1_packet, rvfi_inst_data[rvfi_trap]); + let v1_packet = update_rvfi_insn(v1_packet, rvfi_inst_data[rvfi_insn]); + let v1_packet = update_rvfi_order(v1_packet, rvfi_inst_data[rvfi_order]); + + let v1_packet = update_rvfi_pc_wdata(v1_packet, rvfi_pc_data[rvfi_pc_wdata]); + let v1_packet = update_rvfi_pc_rdata(v1_packet, rvfi_pc_data[rvfi_pc_rdata]); + + let v1_packet = update_rvfi_rd_addr(v1_packet, rvfi_int_data[rvfi_rd_addr]); + let v1_packet = update_rvfi_rs2_addr(v1_packet, rvfi_int_data.rvfi_rs2_addr()); + let v1_packet = update_rvfi_rs1_addr(v1_packet, rvfi_int_data.rvfi_rs1_addr()); + let v1_packet = update_rvfi_rd_wdata(v1_packet, rvfi_int_data[rvfi_rd_wdata]); + let v1_packet = update_rvfi_rs2_data(v1_packet, rvfi_int_data.rvfi_rs2_rdata()); + let v1_packet = update_rvfi_rs1_data(v1_packet, rvfi_int_data.rvfi_rs1_rdata()); + + let v1_packet = update_rvfi_mem_wmask(v1_packet, truncate(rvfi_mem_data[rvfi_mem_wmask], 8)); + let v1_packet = update_rvfi_mem_rmask(v1_packet, truncate(rvfi_mem_data[rvfi_mem_rmask], 8)); + let v1_packet = update_rvfi_mem_wdata(v1_packet, truncate(rvfi_mem_data[rvfi_mem_wdata], 64)); + let v1_packet = update_rvfi_mem_rdata(v1_packet, truncate(rvfi_mem_data[rvfi_mem_rdata], 64)); + let v1_packet = update_rvfi_mem_addr(v1_packet, rvfi_mem_data[rvfi_mem_addr]); + + return v1_packet.bits; +} + +val rvfi_get_v2_trace_size : unit -> bits(64) +function rvfi_get_v2_trace_size () = { + let trace_size : bits(64) = to_bits(64, 512); + let trace_size = if (rvfi_int_data_present) then trace_size + 320 else trace_size; + let trace_size = if (rvfi_mem_data_present) then trace_size + 704 else trace_size; + return trace_size >> 3; // we have to return bytes not bits +} + +val rvfi_get_exec_packet_v2 : unit -> bits(512) +function rvfi_get_exec_packet_v2 () = { + // TODO: add the other data + // TODO: find a way to return a variable-length bitvector + let packet = Mk_RVFI_DII_Execution_PacketV2(zero_extend(0b0)); + let packet = update_magic(packet, 0x32762d6563617274); // ASCII "trace-v2" (BE) + let packet = update_basic_data(packet, rvfi_inst_data.bits); + let packet = update_pc_data(packet, rvfi_pc_data.bits); + let packet = update_integer_data_available(packet, bool_to_bits(rvfi_int_data_present)); + let packet = update_memory_access_data_available(packet, bool_to_bits(rvfi_mem_data_present)); + // To simplify the implementation (so that we can return a fixed-size vector) + // we always return a max-size packet from this function, and the C emulator + // ensures that only trace_size bits are sent over the socket. + let packet = update_trace_size(packet, rvfi_get_v2_trace_size()); + return packet.bits; +} + +val rvfi_get_int_data : unit -> bits(320) +function rvfi_get_int_data () = { + assert(rvfi_int_data_present, "reading uninitialized data"); + return rvfi_int_data.bits; +} + +val rvfi_get_mem_data : unit -> bits(704) +function rvfi_get_mem_data () = { + assert(rvfi_mem_data_present, "reading uninitialized data"); + return rvfi_mem_data.bits; +} + +val rvfi_encode_width_mask : forall 'n, 0 < 'n <= 32. int('n) -> bits(32) + +function rvfi_encode_width_mask(width) = + (0xFFFFFFFF >> (32 - width)) + +val print_rvfi_exec : unit -> unit + +function print_rvfi_exec () = { + print_bits("rvfi_intr : ", rvfi_inst_data[rvfi_intr]); + print_bits("rvfi_halt : ", rvfi_inst_data[rvfi_halt]); + print_bits("rvfi_trap : ", rvfi_inst_data[rvfi_trap]); + print_bits("rvfi_rd_addr : ", rvfi_int_data[rvfi_rd_addr]); + print_bits("rvfi_rs2_addr : ", rvfi_int_data.rvfi_rs2_addr()); + print_bits("rvfi_rs1_addr : ", rvfi_int_data.rvfi_rs1_addr()); + print_bits("rvfi_mem_wmask: ", rvfi_mem_data[rvfi_mem_wmask]); + print_bits("rvfi_mem_rmask: ", rvfi_mem_data[rvfi_mem_rmask]); + print_bits("rvfi_mem_wdata: ", rvfi_mem_data[rvfi_mem_wdata]); + print_bits("rvfi_mem_rdata: ", rvfi_mem_data[rvfi_mem_rdata]); + print_bits("rvfi_mem_addr : ", rvfi_mem_data[rvfi_mem_addr]); + print_bits("rvfi_rd_wdata : ", rvfi_int_data[rvfi_rd_wdata]); + print_bits("rvfi_rs2_data : ", rvfi_int_data.rvfi_rs2_rdata()); + print_bits("rvfi_rs1_data : ", rvfi_int_data.rvfi_rs1_rdata()); + print_bits("rvfi_insn : ", rvfi_inst_data[rvfi_insn]); + print_bits("rvfi_pc_wdata : ", rvfi_pc_data[rvfi_pc_wdata]); + 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 4053f9094..28adc50cd 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -24,7 +24,8 @@ 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, data) = () +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) = () diff --git a/test/run_tests.sh b/test/run_tests.sh old mode 100755 new mode 100644 index f37f0e638..8c0f03f2f --- a/test/run_tests.sh +++ b/test/run_tests.sh @@ -143,6 +143,28 @@ for test in $DIR/riscv-tests/rv64*.elf; do done finish_suite "64-bit RISCV C tests" +# Do 'make clean' to avoid cross-arch pollution. +make clean + +if ARCH=RV32 make c_emulator/riscv_rvfi_RV32; +then + green "Building 32-bit RISCV RVFI C emulator" "ok" +else + red "Building 32-bit RISCV RVFI C emulator" "fail" +fi +finish_suite "32-bit RISCV RVFI C tests" + +# Do 'make clean' to avoid cross-arch pollution. +make clean + +if ARCH=RV64 make c_emulator/riscv_rvfi_RV64; +then + green "Building 64-bit RISCV RVFI C emulator" "ok" +else + red "Building 64-bit RISCV RVFI C emulator" "fail" +fi +finish_suite "64-bit RISCV RVFI C tests" + printf "Passed ${all_pass} out of $(( all_pass + all_fail ))\n\n" XML="\n$SUITES_XML\n" printf "$XML" > $DIR/tests.xml