Added implementation of callbacks for trace printing in riscv_default…

…_callbacks.c.

Makefile

@@ -223,15 +223,22 @@ cloc:
 gcovr:
 	gcovr -r . --html --html-detail -o index.html
 
-c_preserve_fns=-c_preserve _set_Misa_C
+c_preserve_fns=-c_preserve _set_Misa_C \
+  -c_preserve mem_write_callback_default \
+  -c_preserve mem_read_callback_default \
+  -c_preserve xreg_write_callback_default \
+  -c_preserve freg_write_callback_default \
+  -c_preserve csr_write_callback_default \
+  -c_preserve csr_read_callback_default \
+  -c_preserve vreg_write_callback_default
 
 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_default_callbacks.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_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) -c_include riscv_default_callbacks.c 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 -c_include riscv_default_callbacks.c $(SAIL_SRCS) -o $(basename $@)
+	$(SAIL) $(SAIL_FLAGS) -no_warn -memo_z3 -config c_emulator/config.json -c2 $(SAIL_SRCS) -o $(basename $@)
 
 $(SOFTFLOAT_LIBS):
 	$(MAKE) SPECIALIZE_TYPE=$(SOFTFLOAT_SPECIALIZE_TYPE) -C $(SOFTFLOAT_LIBDIR)
@@ -261,7 +268,6 @@ rvfi_preserve_fns=-c_preserve rvfi_set_instr_packet \
   -c_preserve rvfi_read \
   -c_preserve rvfi_mem_exception \
   -c_preserve rvfi_wX \
-  -c_preserve print_rvfi_exec \
   -c_preserve print_instr_packet \
   -c_preserve print_rvfi_exec
 

c_emulator/riscv_default_callbacks.c

@@ -1,11 +1,54 @@
+#include "riscv_config.h"
+
+int zmem_write_callback_default(long unsigned int addr, long int width, lbits value);
+int zmem_read_callback_default(const char *type, long unsigned int addr,
+                               long int width, lbits value);
+int zxreg_write_callback_default(long unsigned int reg, long unsigned int value);
+int zfreg_write_callback_default(long unsigned int reg, long unsigned int value);
+int zcsr_write_callback_default(long unsigned int reg, long unsigned int value);
+int zcsr_read_callback_default(long unsigned int reg, long unsigned int value);
+int zvreg_write_callback_default(long unsigned int reg, lbits value);
+
 /* The model assumes that these functions do not change the state of the model.
  */
-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_write_callback(uint64_t addr, uint64_t width, lbits value) {
+  if (config_print_mem_access)
+    zmem_write_callback_default(addr, width, value);
+}
+
+int mem_read_callback(const char *type, uint64_t addr, uint64_t width,
+                      lbits value)
+{
+  if (config_print_mem_access)
+    zmem_read_callback_default(type, addr, width, 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 xreg_write_callback(unsigned reg, uint64_t value) { 
+  if (config_print_reg)
+    zxreg_write_callback_default(reg, value);
+}
+
+int freg_write_callback(unsigned reg, uint64_t value) {
+  /* TODO: will only print bits; should we print in floating point format? */
+  if (config_print_reg)
+    zfreg_write_callback_default(reg, value);
+}
+
+int csr_write_callback(unsigned reg, uint64_t value) {
+  if (config_print_reg)
+    zcsr_write_callback_default(reg, value);
+}
+
+int csr_read_callback(unsigned reg, uint64_t value) {
+  if (config_print_reg)
+    zcsr_read_callback_default(reg, value);
+}
+
+int vreg_write_callback(unsigned reg, lbits value) {
+  if (config_print_reg)
+    zvreg_write_callback_default(reg, value);
+}
+
 int pc_write_callback(uint64_t value) { }

c_emulator/riscv_prelude.h

@@ -12,6 +12,4 @@ unit print_mem_access(sail_string s);
 unit print_platform(sail_string s);
 
 bool get_config_print_instr(unit u);
-bool get_config_print_reg(unit u);
-bool get_config_print_mem(unit u);
 bool get_config_print_platform(unit u);

c_emulator/riscv_rvfi_callbacks.c

@@ -10,7 +10,8 @@ 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)
+int mem_read_callback(const char *type, uint64_t addr, uint64_t width,
+                      lbits value)
 {
   if (rv_enable_callbacks) {
     sail_int len;

model/prelude.sail

@@ -76,7 +76,6 @@ val get_config_print_mem = pure {c:"get_config_print_mem"} : unit -> bool
 val get_config_print_platform = pure {c:"get_config_print_platform"} : unit -> bool
 // defaults for other backends
 function get_config_print_instr () = false
-function get_config_print_mem () = false
 function get_config_print_platform () = false
 
 val sign_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)

model/riscv_csr_begin.sail

@@ -349,3 +349,17 @@ scattered function read_CSR
 /* returns new value (after legalisation) if the CSR is defined */
 val write_CSR : (csreg, xlenbits) -> xlenbits
 scattered function write_CSR
+
+
+/* Implementations of default callbacks for trace printing */
+
+val csr_write_callback_default : (csreg, xlenbits) -> unit
+function csr_write_callback_default (csr, value) = {
+  print_reg("csr " ^ csr_name_map(csr) ^ " <- " ^ BitStr(value) ^ " (input: " ^ BitStr(value) ^ ")")
+}
+
+val csr_read_callback_default : (csreg, xlenbits) -> unit
+function csr_read_callback_default (csr, value) = {
+  print_reg("csr " ^ csr_name_map(csr) ^ " -> " ^ BitStr(value))
+}
+

model/riscv_insts_vext_mem.sail

@@ -183,7 +183,6 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
                       else {
                         vl = to_bits(xlen, i);
                         csr_write_callback(csr_name_map("vl"), vl);
->>>>>>> cb0b429d (Implementing callbacks in sail-riscv for state-changing events)
                         trimmed = true
                       }
                     }

model/riscv_mem.sail

@@ -73,9 +73,7 @@ function phys_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext
     (Execute(),  None()) => MemException(E_Fetch_Access_Fault()),
     (Read(Data), None()) => MemException(E_Load_Access_Fault()),
     (_,          None()) => MemException(E_SAMO_Access_Fault()),
-    (_,      Some(v, m)) => { if   get_config_print_mem()
-                              then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(paddr) ^ "] -> " ^ BitStr(v));
-                              MemValue(v, m) }
+    (_,      Some(v, m)) => MemValue(v, m)
   }
 }
 
@@ -133,7 +131,7 @@ function mem_read_priv_meta (typ, priv, paddr, width, aq, rl, res, meta) = {
       (_, _, _)             => checked_mem_read(typ, priv, paddr, width, aq, rl, res, meta)
     };
   match result {
-    MemValue(value, _) => mem_read_callback(paddr, width, value),
+    MemValue(value, _) => mem_read_callback(to_str(typ), paddr, width, value),
     MemException(e) => mem_exception_callback(paddr, num_of_ExceptionType(e))
   };
   result
@@ -158,10 +156,7 @@ function mem_write_ea (addr, width, aq, rl, con) =
 
 // 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));
-  if   get_config_print_mem()
-  then print_mem("mem[" ^ BitStr(paddr) ^ "] <- " ^ BitStr(data));
-  result
+  MemValue(write_ram(wk, paddr, width, data, meta));
 }
 
 /* dispatches to MMIO regions or physical memory regions depending on physical memory map */

model/riscv_regs.sail

@@ -125,9 +125,7 @@ function wX (r : regno, in_v : xlenbits) -> unit = {
     31 => x31 = v,
     _  => assert(false, "invalid register number")
   };
-  if (r != 0) then {
-    xreg_write_callback(regno_to_regidx(r), in_v);
-  }
+  if (r != 0) then xreg_write_callback(regno_to_regidx(r), in_v)
 }
 
 function rX_bits(i: regidx) -> xlenbits = rX(unsigned(i))

model/riscv_types.sail

@@ -415,13 +415,38 @@ function report_invalid_width(f , l, w, k) -> 'a = {
 
 /* Callbacks for state-changing events */
 
-/* Defaults for these functions in riscv_default_callbacks.c and platform_impl.ml */
-
-val mem_write_callback = pure {ocaml: "Platform.mem_write_callback", c: "mem_write_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> 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)) -> unit
-val mem_exception_callback = pure {ocaml: "Platform.mem_exception_callback", c: "mem_exception_callback"} : forall 'n, 0 <= 'n < xlen . (/* addr */ xlenbits, /* num_of_ExceptionType */ int('n)) -> unit
-val pc_write_callback = pure {ocaml: "Platform.pc_write_callback", c: "pc_write_callback"} : xlenbits -> unit
-val xreg_write_callback = pure {ocaml: "Platform.xreg_write_callback", c: "xreg_write_callback"} : (regidx, xlenbits) -> unit
-val freg_write_callback = pure {ocaml: "Platform.freg_write_callback", c: "freg_write_callback"} : (regidx, flenbits) -> unit
-val csr_write_callback = pure {ocaml: "Platform.csr_write_callback", c: "csr_write_callback"} : (csreg, xlenbits) -> unit
-val csr_read_callback = pure {ocaml: "Platform.csr_read_callback", c: "csr_read_callback"} : (csreg, xlenbits) -> unit
+/* Defaults for these functions in riscv_default_callbacks.c */
+
+val mem_write_callback = pure {c: "mem_write_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> unit
+val mem_read_callback = pure {c: "mem_read_callback"} : forall 'n, 0 < 'n <= max_mem_access . (/* access type */ string, /* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> unit
+val mem_exception_callback = pure {c: "mem_exception_callback"} : forall 'n, 0 <= 'n < xlen . (/* addr */ xlenbits, /* num_of_ExceptionType */ int('n)) -> unit
+val pc_write_callback = pure {c: "pc_write_callback"} : xlenbits -> unit
+val xreg_write_callback = pure {c: "xreg_write_callback"} : (regidx, xlenbits) -> unit
+val freg_write_callback = pure {c: "freg_write_callback"} : (regidx, flenbits) -> unit
+val csr_write_callback = pure {c: "csr_write_callback"} : (csreg, xlenbits) -> unit
+val csr_read_callback = pure {c: "csr_read_callback"} : (csreg, xlenbits) -> unit
+
+/* Implementations of default callbacks for trace printing */
+
+val mem_write_callback_default : forall 'n, 0 < 'n <= max_mem_access . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> unit
+function mem_write_callback_default (addr, width, value) = {
+  print_mem("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(value))
+}
+
+val mem_read_callback_default : forall 'n, 0 < 'n <= max_mem_access . (/* access type */ string, /* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> unit
+function mem_read_callback_default (t, addr, width, value) = {
+  print_mem("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(value))
+}
+
+val xreg_write_callback_default : (regidx, xlenbits) -> unit
+function xreg_write_callback_default (reg, value) = {
+  print_reg("x" ^ dec_str(regidx_to_regno(reg)) ^ " <- " ^ BitStr(value))
+}
+
+val freg_write_callback_default : (regidx, flenbits) -> unit
+function freg_write_callback_default (reg, value) = {
+  /* todo: will only print bits; should we print in floating point format? */
+  print_reg("f" ^ dec_str(regidx_to_regno(reg)) ^ " <- " ^ BitStr(value))
+}
+
+

model/riscv_vreg_type.sail

@@ -149,5 +149,16 @@ 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_write_callback = pure {ocaml: "Platform.vreg_write_callback", c: "vreg_write_callback"} : (regidx, vregtype) -> unit
+/* Default for this function in riscv_default_callbacks.c */
+
+val vreg_write_callback = pure {c: "vreg_write_callback"} : (regidx, vregtype) -> unit
+
+/* Implementations of default callbacks for trace printing */
+
+val vreg_write_callback_default : (regidx, vregtype) -> unit
+function vreg_write_callback_default (reg, value) = {
+  let VLEN = unsigned(vlenb) * 8;
+  assert(0 < VLEN & VLEN <= sizeof(vlenmax));
+  print_reg("v" ^ dec_str(regidx_to_regno(reg)) ^ " <- " ^ BitStr(value[VLEN - 1 .. 0]))
+}
+