Added implementation of callbacks for trace printing in riscv_default…

…_callbacks.c.

Makefile

@@ -227,7 +227,7 @@ c_preserve_fns=-c_preserve _set_Misa_C
 
 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

c_emulator/riscv_default_callbacks.c

@@ -1,11 +1,51 @@
+#include "riscv_config.h"
+
+int zmem_write_callback_default(long unsigned int addr, long int width, lbits value);
+int zmem_read_callback_default(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(uint64_t addr, uint64_t width, lbits value) {
+  if (config_print_mem_access)
+    zmem_read_callback_default(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);

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)
   }
 }
 
@@ -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_step.sail

@@ -123,8 +123,21 @@ function loop () : unit -> unit = {
   }
 }
 
+/* It is needed to generate definitions of default callbacks for trace printing */
+function init_default_callbacks () : unit -> unit = {
+  mem_write_callback_default(zeros_implicit(), 1, 0x00);
+  mem_read_callback_default(zeros_implicit(), 1, 0x00);
+  xreg_write_callback_default(zeros_implicit(), to_bits(sizeof(xlen), 0));
+  freg_write_callback_default(zeros_implicit(), to_bits(sizeof(flen), 0));
+  csr_write_callback_default(zeros_implicit(), to_bits(sizeof(xlen), 0));
+  csr_read_callback_default(zeros_implicit(), to_bits(sizeof(xlen), 0));
+  let VLEN = unsigned(vlenb) * 8;
+  if (VLEN > 0) then vreg_write_callback_default(zeros_implicit(), zeros_implicit());
+}
+
 /* initialize model state */
 function init_model () -> unit = {
+  init_default_callbacks();
   init_platform (); /* devices */
   init_sys ();      /* processor */
   init_vmem ();     /* virtual memory */

model/riscv_types.sail

@@ -415,7 +415,7 @@ 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 */
+/* Defaults for these functions in riscv_default_callbacks.c and platform.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
@@ -425,3 +425,28 @@ val xreg_write_callback = pure {ocaml: "Platform.xreg_write_callback", c: "xreg_
 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
+
+/* 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 . (/* addr */ xlenbits, /* width */ int('n), /* value */ bits(8 * 'n)) -> unit
+function mem_read_callback_default (addr, width, value) = {
+  print_mem("mem[" ^ 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 */
+/* Default for this function in riscv_default_callbacks.c and platform.ml */
+
 val vreg_write_callback = pure {ocaml: "Platform.vreg_write_callback", 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]))
+}
+