Implementing callbacks in sail-riscv for state-changing events

1. Added implementation of callbacks for RVFI records in riscv_rvfi_callbacks.c.
riscv · Jul 1, 2024 · 10ae49b · 10ae49b
1 parent 2f11108
commit 10ae49b
Show file tree

Hide file tree

Showing 15 changed files with 891 additions and 22 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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 */