Skip to content

Commit 6e0f187

Browse files
kseniadobrovolskayakseniadobrovolskaya
committed
Implementing callbacks in sail-riscv for state-changing events
1. Added implementation of callbacks for RVFI records in riscv_rvfi_callbacks.c.
1 parent 2f11108 commit 6e0f187

15 files changed

+892
-22
lines changed

‎Makefile‎

Lines changed: 35 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -103,9 +103,11 @@ SAIL_ARCH_SRCS = $(PRELUDE)
103103
SAIL_ARCH_SRCS += riscv_types_common.sail riscv_types_ext.sail riscv_types.sail
104104
SAIL_ARCH_SRCS += riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail
105105
SAIL_ARCH_SRCS += riscv_mem.sail $(SAIL_VM_SRCS)
106+
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
106107
SAIL_ARCH_SRCS += riscv_types_kext.sail # Shared/common code for the cryptography extension.
107108

108109
SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail
110+
RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail
109111

110112
SAIL_OTHER_SRCS = $(SAIL_STEP_SRCS)
111113
ifeq ($(ARCH),RV32)
@@ -117,6 +119,7 @@ endif
117119
PRELUDE_SRCS = $(addprefix model/,$(PRELUDE))
118120
SAIL_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_SRCS))
119121
SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_RMEM_INST_SRCS) $(SAIL_OTHER_SRCS))
122+
SAIL_RVFI_SRCS = $(addprefix model/,$(SAIL_ARCH_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) $(RVFI_STEP_SRCS))
120123
SAIL_COQ_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_COQ_SRCS))
121124

122125
PLATFORM_OCAML_SRCS = $(addprefix ocaml_emulator/,platform.ml platform_impl.ml softfloat.ml riscv_ocaml_sim.ml)
@@ -271,10 +274,41 @@ $(SOFTFLOAT_LIBS):
271274
csim: c_emulator/riscv_sim_$(ARCH)
272275
.PHONY: osim
273276
osim: ocaml_emulator/riscv_ocaml_sim_$(ARCH)
277+
.PHONY: rvfi
278+
rvfi: c_emulator/riscv_rvfi_$(ARCH)
274279

275280
c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
276281
gcc -g $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
277282

283+
# Note: We have to add -c_preserve since the functions might be optimized out otherwise
284+
rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
285+
-c_preserve rvfi_get_cmd \
286+
-c_preserve rvfi_get_insn \
287+
-c_preserve rvfi_get_v2_trace_size \
288+
-c_preserve rvfi_get_v2_support_packet \
289+
-c_preserve rvfi_get_exec_packet_v1 \
290+
-c_preserve rvfi_get_exec_packet_v2 \
291+
-c_preserve rvfi_get_mem_data \
292+
-c_preserve rvfi_get_int_data \
293+
-c_preserve rvfi_zero_exec_packet \
294+
-c_preserve rvfi_halt_exec_packet \
295+
-c_preserve rvfi_write \
296+
-c_preserve rvfi_read \
297+
-c_preserve rvfi_wX \
298+
-c_preserve print_rvfi_exec \
299+
-c_preserve print_instr_packet \
300+
-c_preserve print_rvfi_exec
301+
302+
# sed -i isn't posix compliant, unfortunately
303+
generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile
304+
mkdir -p generated_definitions/c
305+
$(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 $@)
306+
sed -e '/^[[:space:]]*$$/d' $@ > $@.new
307+
mv $@.new $@
308+
309+
c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
310+
gcc -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
311+
278312
latex: $(SAIL_SRCS) Makefile
279313
mkdir -p generated_definitions/latex
280314
$(SAIL) -latex -latex_prefix sail -o generated_definitions/latex $(SAIL_SRCS)
@@ -453,7 +487,7 @@ clean:
453487
-rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/*
454488
-rm -rf generated_definitions/for-rmem/*
455489
-$(MAKE) -C $(SOFTFLOAT_LIBDIR) clean
456-
-rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64
490+
-rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 c_emulator/riscv_rvfi_RV32 c_emulator/riscv_rvfi_RV64
457491
-rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 ocaml_emulator/tracecmp
458492
-rm -f *.gcno *.gcda
459493
-rm -f z3_problems

‎c_emulator/riscv_default_callbacks.c‎

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,16 @@
11
/* The model assumes that these functions do not change the state of the model.
22
*/
3-
int __attribute__((weak))
4-
mem_update_callback(uint64_t addr, uint64_t width, lbits data)
3+
int mem_update_callback(uint64_t addr, uint64_t width, lbits value,
4+
bool is_exception)
55
{
66
}
7-
int __attribute__((weak)) xreg_update_callback(unsigned reg, uint64_t value) { }
8-
int __attribute__((weak)) freg_update_callback(unsigned reg, uint64_t value) { }
9-
int __attribute__((weak))
10-
csr_update_callback(const char *reg_name, uint64_t value)
7+
int mem_read_callback(uint64_t addr, uint64_t width, lbits value,
8+
bool is_exception)
119
{
1210
}
13-
int __attribute__((weak))
14-
csr_read_callback(const char *reg_name, uint64_t value)
15-
{
16-
}
17-
int __attribute__((weak)) vreg_update_callback(unsigned reg, lbits value) { }
18-
int __attribute__((weak)) pc_update_callback(uint64_t value) { }
11+
int xreg_update_callback(unsigned reg, uint64_t value) { }
12+
int freg_update_callback(unsigned reg, uint64_t value) { }
13+
int csr_update_callback(const char *reg_name, uint64_t value) { }
14+
int csr_read_callback(const char *reg_name, uint64_t value) { }
15+
int vreg_update_callback(unsigned reg, lbits value) { }
16+
int pc_update_callback(uint64_t value) { }

‎c_emulator/riscv_rvfi_callbacks.c‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
int zrvfi_write(uint64_t addr, int64_t width, lbits value, bool is_exception);
2+
int zrvfi_read(uint64_t addr, sail_int width, lbits value, bool is_exception);
3+
int zrvfi_wX(int64_t reg, uint64_t value);
4+
5+
int mem_update_callback(uint64_t addr, uint64_t width, lbits value,
6+
bool is_exception)
7+
{
8+
zrvfi_write(addr, width, value, is_exception);
9+
}
10+
int mem_read_callback(uint64_t addr, uint64_t width, lbits value,
11+
bool is_exception)
12+
{
13+
sail_int len;
14+
CREATE(sail_int)(&len);
15+
CONVERT_OF(sail_int, mach_int)(&len, width);
16+
zrvfi_read(addr, len, value, is_exception);
17+
KILL(sail_int)(&len);
18+
}
19+
int xreg_update_callback(unsigned reg, uint64_t value)
20+
{
21+
zrvfi_wX(reg, value);
22+
}
23+
int freg_update_callback(unsigned reg, uint64_t value) { }
24+
int csr_update_callback(const char *reg_name, uint64_t value) { }
25+
int csr_read_callback(const char *reg_name, uint64_t value) { }
26+
int vreg_update_callback(unsigned reg, lbits value) { }
27+
int pc_update_callback(uint64_t value) { }

‎c_emulator/riscv_sail.h‎

Lines changed: 27 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,28 @@ unit z_set_Misa_C(struct zMisa *, mach_bits);
2323
unit z_set_Misa_D(struct zMisa *, mach_bits);
2424
unit z_set_Misa_F(struct zMisa *, mach_bits);
2525

26+
#ifdef RVFI_DII
27+
unit zext_rvfi_init(unit);
28+
unit zrvfi_set_instr_packet(mach_bits);
29+
mach_bits zrvfi_get_cmd(unit);
30+
mach_bits zrvfi_get_insn(unit);
31+
bool zrvfi_step(sail_int);
32+
unit zrvfi_zzero_exec_packet(unit);
33+
unit zrvfi_halt_exec_packet(unit);
34+
void zrvfi_get_exec_packet_v1(sail_bits *rop, unit);
35+
void zrvfi_get_exec_packet_v2(sail_bits *rop, unit);
36+
extern bool zrvfi_int_data_present;
37+
void zrvfi_get_int_data(sail_bits *rop, unit);
38+
extern bool zrvfi_mem_data_present;
39+
void zrvfi_get_mem_data(sail_bits *rop, unit);
40+
mach_bits zrvfi_get_v2_trace_sizze(unit);
41+
void zrvfi_get_v2_support_packet(sail_bits *rop, unit);
42+
43+
// Debugging prints
44+
unit zprint_rvfi_exec(unit);
45+
unit zprint_instr_packet(uint64_t);
46+
#endif
47+
2648
extern mach_bits zxlen_val;
2749
extern bool zhtif_done;
2850
extern mach_bits zhtif_exit_code;
@@ -34,11 +56,14 @@ extern bool have_exception;
3456
extern bool zrv_enable_callbacks;
3557
/* The model assumes that these functions do not change the state of the model.
3658
*/
37-
int mem_update_callback(uint64_t addr, uint64_t width, lbits data);
59+
int mem_update_callback(uint64_t addr, uint64_t width, lbits value,
60+
bool is_exception);
61+
int mem_read_callback(uint64_t addr, uint64_t width, lbits value,
62+
bool is_exception);
3863
int xreg_update_callback(unsigned reg, uint64_t value);
3964
int freg_update_callback(unsigned reg, uint64_t value);
4065
int csr_update_callback(const char *reg_name, uint64_t value);
41-
int vreg_update_callback(unsigned reg);
66+
int vreg_update_callback(unsigned reg, lbits value);
4267
int pc_update_callback(uint64_t value);
4368

4469
/* machine state */

0 commit comments

Comments
 (0)