Implementing callbacks in sail-riscv for state-changing events

  Pushed all the rv_enable_callbacks into the callback functions.

Makefile

@@ -287,32 +287,6 @@ rvfi: c_emulator/riscv_rvfi_$(ARCH)
 c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
  $(CC) -g $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
 
-# Note: We have to add -c_preserve since the functions might be optimized out otherwise
-rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
- -c_preserve rvfi_get_cmd \
- -c_preserve rvfi_get_insn \
- -c_preserve rvfi_get_v2_trace_size \
- -c_preserve rvfi_get_v2_support_packet \
- -c_preserve rvfi_get_exec_packet_v1 \
- -c_preserve rvfi_get_exec_packet_v2 \
- -c_preserve rvfi_get_mem_data \
- -c_preserve rvfi_get_int_data \
- -c_preserve rvfi_zero_exec_packet \
- -c_preserve rvfi_halt_exec_packet \
- -c_preserve print_rvfi_exec \
- -c_preserve print_instr_packet \
- -c_preserve print_rvfi_exec
-
-# sed -i isn't posix compliant, unfortunately
-generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile
- mkdir -p generated_definitions/c
- $(SAIL) $(c_preserve_fns) $(rvfi_preserve_fns) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@)
- sed -e '/^[[:space:]]*$$/d' $@ > $@.new
- mv $@.new $@
-
-c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
- $(CC) -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
-
 # Note: We have to add -c_preserve since the functions might be optimized out otherwise
 rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
  -c_preserve rvfi_get_cmd \
@@ -327,6 +301,7 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
  -c_preserve rvfi_halt_exec_packet \
  -c_preserve rvfi_write \
  -c_preserve rvfi_read \
+ -c_preserve rvfi_mem_exception \
  -c_preserve rvfi_wX \
  -c_preserve print_rvfi_exec \
  -c_preserve print_instr_packet \
@@ -340,7 +315,7 @@ generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main
  mv $@.new $@
 
 c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile
- gcc -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
+ $(CC) -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
 
 latex: $(SAIL_SRCS) Makefile
  mkdir -p generated_definitions/latex

c_emulator/riscv_config.h

@@ -5,3 +5,4 @@ extern bool config_print_instr;
 extern bool config_print_reg;
 extern bool config_print_mem_access;
 extern bool config_print_platform;
+extern bool rv_enable_callbacks;

c_emulator/riscv_default_callbacks.c

@@ -1,16 +1,11 @@
 /* The model assumes that these functions do not change the state of the model.
  */
-int mem_update_callback(uint64_t addr, uint64_t width, lbits value,
- bool is_exception)
-{
-}
-int mem_read_callback(uint64_t addr, uint64_t width, lbits value,
- bool is_exception)
-{
-}
-int xreg_update_callback(unsigned reg, uint64_t value) { }
-int freg_update_callback(unsigned reg, uint64_t value) { }
-int csr_update_callback(const char *reg_name, uint64_t value) { }
-int csr_read_callback(const char *reg_name, uint64_t value) { }
-int vreg_update_callback(unsigned reg, lbits value) { }
-int pc_update_callback(uint64_t value) { }
+int mem_write_callback(uint64_t addr, uint64_t width, lbits value) { }
+int mem_read_callback(uint64_t addr, uint64_t width, lbits value) { }
+int mem_exception_callback(uint64_t addr, uint64_t num_of_exception) { }
+int xreg_write_callback(unsigned reg, uint64_t value) { }
+int freg_write_callback(unsigned reg, uint64_t value) { }
+int csr_write_callback(unsigned reg, uint64_t value) { }
+int csr_read_callback(unsigned reg, uint64_t value) { }
+int vreg_write_callback(unsigned reg, lbits value) { }
+int pc_write_callback(uint64_t value) { }

c_emulator/riscv_rvfi_callbacks.c

@@ -1,27 +1,37 @@
-int zrvfi_write(uint64_t addr, int64_t width, lbits value, bool is_exception);
-int zrvfi_read(uint64_t addr, sail_int width, lbits value, bool is_exception);
+#include "riscv_config.h"
+
+int zrvfi_write(uint64_t addr, int64_t width, lbits value);
+int zrvfi_read(uint64_t addr, sail_int width, lbits value);
+int zrvfi_mem_exception(uint64_t addr);
 int zrvfi_wX(int64_t reg, uint64_t value);
 
-int mem_update_callback(uint64_t addr, uint64_t width, lbits value,
- bool is_exception)
+int mem_write_callback(uint64_t addr, uint64_t width, lbits value)
+{
+ if (rv_enable_callbacks)
+ zrvfi_write(addr, width, value);
+}
+int mem_read_callback(uint64_t addr, uint64_t width, lbits value)
 {
- zrvfi_write(addr, width, value, is_exception);
+ if (rv_enable_callbacks) {
+ sail_int len;
+ CREATE(sail_int)(&len);
+ CONVERT_OF(sail_int, mach_int)(&len, width);
+ zrvfi_read(addr, len, value);
+ KILL(sail_int)(&len);
+ }
 }
-int mem_read_callback(uint64_t addr, uint64_t width, lbits value,
- bool is_exception)
+int mem_exception_callback(uint64_t addr, uint64_t num_of_exception)
 {
- sail_int len;
- CREATE(sail_int)(&len);
- CONVERT_OF(sail_int, mach_int)(&len, width);
- zrvfi_read(addr, len, value, is_exception);
- KILL(sail_int)(&len);
+ if (rv_enable_callbacks)
+ zrvfi_mem_exception(addr);
 }
-int xreg_update_callback(unsigned reg, uint64_t value)
+int xreg_write_callback(unsigned reg, uint64_t value)
 {
- zrvfi_wX(reg, value);
+ if (rv_enable_callbacks)
+ zrvfi_wX(reg, value);
 }
-int freg_update_callback(unsigned reg, uint64_t value) { }
-int csr_update_callback(const char *reg_name, uint64_t value) { }
-int csr_read_callback(const char *reg_name, uint64_t value) { }
-int vreg_update_callback(unsigned reg, lbits value) { }
-int pc_update_callback(uint64_t value) { }
+int freg_write_callback(unsigned reg, uint64_t value) { }
+int csr_write_callback(unsigned reg, uint64_t value) { }
+int csr_read_callback(unsigned reg, uint64_t value) { }
+int vreg_write_callback(unsigned reg, lbits value) { }
+int pc_write_callback(uint64_t value) { }

c_emulator/riscv_sail.h

@@ -52,19 +52,17 @@ extern bool have_exception;
 
 /* Callbacks for state-changing events */
 
-/* Whether need to call the callback functions */
-extern bool zrv_enable_callbacks;
 /* The model assumes that these functions do not change the state of the model.
  */
-int mem_update_callback(uint64_t addr, uint64_t width, lbits value,
- bool is_exception);
-int mem_read_callback(uint64_t addr, uint64_t width, lbits value,
- bool is_exception);
-int xreg_update_callback(unsigned reg, uint64_t value);
-int freg_update_callback(unsigned reg, uint64_t value);
-int csr_update_callback(const char *reg_name, uint64_t value);
-int vreg_update_callback(unsigned reg, lbits value);
-int pc_update_callback(uint64_t value);
+int mem_write_callback(uint64_t addr, uint64_t width, lbits value);
+int mem_read_callback(uint64_t addr, uint64_t width, lbits value);
+int mem_exception_callback(uint64_t addr, uint64_t num_of_exception);
+int xreg_write_callback(unsigned reg, uint64_t value);
+int freg_write_callback(unsigned reg, uint64_t value);
+int csr_write_callback(unsigned reg, uint64_t value);
+int csr_read_callback(unsigned reg, uint64_t value);
+int vreg_write_callback(unsigned reg, lbits value);
+int pc_write_callback(uint64_t value);
 
 /* machine state */
 

c_emulator/riscv_sim.c

@@ -89,6 +89,7 @@ bool config_print_reg = true;
 bool config_print_mem_access = true;
 bool config_print_platform = true;
 bool config_print_rvfi = false;
+bool rv_enable_callbacks = true;
 
 void set_config_print(char *var, bool val)
 {
@@ -98,6 +99,7 @@ void set_config_print(char *var, bool val)
  config_print_reg = val;
  config_print_platform = val;
  config_print_rvfi = val;
+ rv_enable_callbacks = val;
  } else if (strcmp("instr", var) == 0) {
  config_print_instr = val;
  } else if (strcmp("reg", var) == 0) {

model/riscv_csr_ext.sail

@@ -22,18 +22,3 @@ end ext_read_CSR
 
 function clause ext_write_CSR (_, _) = None()
 end ext_write_CSR
-
-function ext_notification_read_CSR (csr : csreg) -> option(xlenbits) = {
- let res = ext_read_CSR(csr);
- if rv_enable_callbacks then
- match res {
- Some(value) => csr_read_callback(csr_name_map(csr), value),
- None() => (),
- };
- res
-}
-
-function ext_notification_write_CSR (csr : csreg, value : xlenbits) -> unit = {
- let res = ext_write_CSR(csr, value);
- if rv_enable_callbacks then csr_update_callback(csr_name_map(csr), value)
-}

model/riscv_fdext_regs.sail

@@ -155,7 +155,6 @@ function rF (r : regno) -> flenbits = {
 
 function wF (r : regno, in_v : flenbits) -> unit = {
  assert(sys_enable_fdext());
- if rv_enable_callbacks then freg_update_callback(regno_to_regidx(r), in_v);
  let v = fregval_into_freg(in_v);
  match r {
  0 => f0 = v,
@@ -194,6 +193,8 @@ function wF (r : regno, in_v : flenbits) -> unit = {
  };
 
  dirty_fd_context();
+
+ freg_write_callback(regno_to_regidx(r), in_v);
 }
 
 function rF_bits(i: regidx) -> flenbits = rF(unsigned(i))

model/riscv_insts_vext_mem.sail

@@ -153,22 +153,25 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
  Ext_DataAddr_Error(e) => {
  if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL }
  else {
- ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i));
+ vl = to_bits(sizeof(xlen), i);
+ csr_write_callback(csr_name_map("vl"), vl);
  trimmed = true
  }
  },
  Ext_DataAddr_OK(vaddr) => {
  if check_misaligned(vaddr, width_type) then {
  if i == 0 then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL }
  else {
- ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i));
+ vl = to_bits(sizeof(xlen), i);
+ csr_write_callback(csr_name_map("vl"), vl);
  trimmed = true
  }
  } else match translateAddr(vaddr, Read(Data)) {
  TR_Failure(e, _) => {
  if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
  else {
- ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i));
+ vl = to_bits(sizeof(xlen), i);
+ csr_write_callback(csr_name_map("vl"), vl);
  trimmed = true
  }
  },
@@ -178,7 +181,8 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
  MemException(e) => {
  if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL }
  else {
- ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), i));
+ vl = to_bits(sizeof(xlen), i);
+ csr_write_callback(csr_name_map("vl"), vl);
  trimmed = true
  }
  }

model/riscv_insts_vext_vset.sail

@@ -49,10 +49,10 @@ function handle_illegal_vtype() = {
  /* Note: Implementations can set vill or trap if the vtype setting is not supported.
  * TODO: configuration support for both solutions
  */
- let new_vtype = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
-
- ext_notification_write_CSR(csr_name_map("vtype"), new_vtype);
- ext_notification_write_CSR(csr_name_map("vl"), zeros())
+ vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */
+ vl = zeros();
+ csr_write_callback(csr_name_map("vtype"), vtype.bits);
+ csr_write_callback(csr_name_map("vl"), vl);
 }
 
 val calculate_new_vl : (int, int) -> xlenbits
@@ -77,8 +77,7 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = {
  let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori;
 
  /* set vtype */
- let new_vtype = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
- ext_notification_write_CSR(csr_name_map("vtype"), new_vtype);
+ vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
 
  /* check new SEW and LMUL are legal and calculate VLMAX */
  let VLEN_pow = get_vlen_pow();
@@ -92,11 +91,11 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = {
  if (rs1 != 0b00000) then { /* normal stripmining */
  let rs1_val = X(rs1);
  let AVL = unsigned(rs1_val);
- ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX));
+ vl = calculate_new_vl(AVL, VLMAX);
  X(rd) = vl;
  } else if (rd != 0b00000) then { /* set vl to VLMAX */
  let AVL = unsigned(ones(sizeof(xlen)));
- ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), VLMAX));
+ vl = to_bits(sizeof(xlen), VLMAX);
  X(rd) = vl;
  } else { /* keep existing vl */
  let AVL = unsigned(vl);
@@ -105,7 +104,11 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = {
  };
 
  /* reset vstart to 0 */
- ext_notification_write_CSR(csr_name_map("vstart"), zeros());
+ vstart = zeros();
+
+ csr_write_callback(csr_name_map("vtype"), vtype.bits);
+ csr_write_callback(csr_name_map("vl"), vl);
+ csr_write_callback(csr_name_map("vstart"), zero_extend(vstart));
 
  RETIRE_SUCCESS
 }
@@ -125,8 +128,7 @@ function clause execute VSETVL(rs2, rs1, rd) = {
  let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori;
 
  /* set vtype */
- let new_vtype = X(rs2);
- ext_notification_write_CSR(csr_name_map("vtype"), new_vtype);
+ vtype.bits = X(rs2);
 
  /* check new SEW and LMUL are legal and calculate VLMAX */
  let VLEN_pow = get_vlen_pow();
@@ -140,11 +142,11 @@ function clause execute VSETVL(rs2, rs1, rd) = {
  if (rs1 != 0b00000) then { /* normal stripmining */
  let rs1_val = X(rs1);
  let AVL = unsigned(rs1_val);
- ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX));
+ vl = calculate_new_vl(AVL, VLMAX);
  X(rd) = vl;
  } else if (rd != 0b00000) then { /* set vl to VLMAX */
  let AVL = unsigned(ones(sizeof(xlen)));
- ext_notification_write_CSR(csr_name_map("vl"), to_bits(sizeof(xlen), VLMAX));
+ vl = to_bits(sizeof(xlen), VLMAX);
  X(rd) = vl;
  } else { /* keep existing vl */
  let AVL = unsigned(vl);
@@ -153,7 +155,11 @@ function clause execute VSETVL(rs2, rs1, rd) = {
  };
 
  /* reset vstart to 0 */
- ext_notification_write_CSR(csr_name_map("vstart"), zeros());
+ vstart = zeros();
+
+ csr_write_callback(csr_name_map("vtype"), vtype.bits);
+ csr_write_callback(csr_name_map("vl"), vl);
+ csr_write_callback(csr_name_map("vstart"), zero_extend(vstart));
 
  RETIRE_SUCCESS
 }
@@ -169,8 +175,7 @@ mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if extensionEnable
 
 function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = {
  /* set vtype */
- let new_vtype = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
- ext_notification_write_CSR(csr_name_map("vtype"), new_vtype);
+ vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul;
 
  /* check new SEW and LMUL are legal and calculate VLMAX */
  let VLEN_pow = get_vlen_pow();
@@ -182,11 +187,15 @@ function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = {
 
  /* set vl according to VLMAX and AVL */
  let AVL = unsigned(uimm); /* AVL is encoded as 5-bit zero-extended imm in the rs1 field */
- ext_notification_write_CSR(csr_name_map("vl"), calculate_new_vl(AVL, VLMAX));
+ vl = calculate_new_vl(AVL, VLMAX);
  X(rd) = vl;
 
  /* reset vstart to 0 */
- ext_notification_write_CSR(csr_name_map("vstart"), zeros());
+ vstart = zeros();
+
+ csr_write_callback(csr_name_map("vtype"), vtype.bits);
+ csr_write_callback(csr_name_map("vl"), vl);
+ csr_write_callback(csr_name_map("vstart"), zero_extend(vstart));
 
  RETIRE_SUCCESS
 }