Add some missed logging guards.

6 files changed, 83 insertions, 47 deletions

diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 8e54189..ee30ec0 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -94,7 +94,8 @@ function readCSR csr : csreg -> xlenbits = {
                                     EXTZ(0x0) }
                    }
   };
-  print_reg("CSR " ^ to_str(csr) ^ " -> " ^ BitStr(res));
+  if   get_config_print_reg()
+  then print_reg("CSR " ^ to_str(csr) ^ " -> " ^ BitStr(res));
   res
 }
 
@@ -164,7 +165,8 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     _           => None()
   };
   match res {
-    Some(v) => print_reg("CSR " ^ to_str(csr) ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"),
+    Some(v) => if   get_config_print_reg()
+               then print_reg("CSR " ^ to_str(csr) ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"),
     None()  => { /* check extensions */
                  if   ext_write_CSR(csr, value)
                  then ()
diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail
index 7fafb08..13f9ae5 100644
--- a/model/riscv_next_control.sail
+++ b/model/riscv_next_control.sail
@@ -47,7 +47,8 @@ function write_NExt_CSR(csr : csreg, value : xlenbits) -> bool = {
     _     => None()
   };
   match res {
-    Some(v) => { print_reg("CSR " ^ to_str(csr) ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")");
+    Some(v) => { if   get_config_print_reg()
+                 then print_reg("CSR " ^ to_str(csr) ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")");
                  true },
     None()  => false
   }
diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
index dd8b5bc..9184f02 100644
--- a/model/riscv_platform.sail
+++ b/model/riscv_platform.sail
@@ -148,53 +148,63 @@ function clint_load(addr, width) = {
   /* FIXME: For now, only allow exact aligned access. */
   if addr == MSIP_BASE & ('n == 8 | 'n == 4)
   then {
-    print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mip.MSI()));
+    if   get_config_print_platform()
+    then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mip.MSI()));
     MemValue(sail_zero_extend(mip.MSI(), sizeof(8 * 'n)))
   }
   else if addr == MTIMECMP_BASE & ('n == 4)
   then {
-    print_platform("clint<4>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp[31..0]));
+    if   get_config_print_platform()
+    then print_platform("clint<4>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp[31..0]));
     /* FIXME: Redundant zero_extend currently required by Lem backend */
     MemValue(sail_zero_extend(mtimecmp[31..0], 32))
   }
   else if addr == MTIMECMP_BASE & ('n == 8)
   then {
-    print_platform("clint<8>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp));
+    if   get_config_print_platform()
+    then print_platform("clint<8>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp));
     /* FIXME: Redundant zero_extend currently required by Lem backend */
     MemValue(sail_zero_extend(mtimecmp, 64))
   }
   else if addr == MTIMECMP_BASE_HI & ('n == 4)
   then {
-    print_platform("clint-hi<4>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp[63..32]));
+    if   get_config_print_platform()
+    then print_platform("clint-hi<4>[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp[63..32]));
     /* FIXME: Redundant zero_extend currently required by Lem backend */
     MemValue(sail_zero_extend(mtimecmp[63..32], 32))
   }
   else if addr == MTIME_BASE & ('n == 4)
   then {
-    print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
+    if   get_config_print_platform()
+    then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
     MemValue(sail_zero_extend(mtime[31..0], 32))
   }
   else if addr == MTIME_BASE & ('n == 8)
   then {
-    print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
+    if   get_config_print_platform()
+    then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
     MemValue(sail_zero_extend(mtime, 64))
   }
   else if addr == MTIME_BASE_HI & ('n == 4)
   then {
-    print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
+    if   get_config_print_platform()
+    then print_platform("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime));
     MemValue(sail_zero_extend(mtime[63..32], 32))
   }
   else {
-    print_platform("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>");
+    if   get_config_print_platform()
+    then print_platform("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>");
     MemException(E_Load_Access_Fault)
   }
 }
 
 function clint_dispatch() -> unit = {
-  print_platform("clint::tick mtime <- " ^ BitStr(mtime));
+  if   get_config_print_platform()
+  then print_platform("clint::tick mtime <- " ^ BitStr(mtime));
   mip->MTI() = false;
   if mtimecmp <=_u mtime then {
-    print_platform(" clint timer pending at mtime " ^ BitStr(mtime));
+    if   get_config_print_platform()
+    then print_platform(" clint timer pending at mtime " ^ BitStr(mtime));
     mip->MTI() = true
   }
 }
@@ -204,27 +214,32 @@ val clint_store: forall 'n, 'n > 0. (xlenbits, int('n), bits(8 * 'n)) -> MemoryO
 function clint_store(addr, width, data) = {
   let addr = addr - plat_clint_base ();
   if addr == MSIP_BASE & ('n == 8 | 'n == 4) then {
-    print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mip.MSI <- " ^ BitStr(data[0]) ^ ")");
+    if   get_config_print_platform()
+    then print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mip.MSI <- " ^ BitStr(data[0]) ^ ")");
     mip->MSI() = data[0] == 0b1;
     clint_dispatch();
     MemValue(true)
   } else if addr == MTIMECMP_BASE & 'n == 8 then {
-    print_platform("clint<8>[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)");
+    if   get_config_print_platform()
+    then print_platform("clint<8>[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)");
     mtimecmp = sail_zero_extend(data, 64); /* FIXME: Redundant zero_extend currently required by Lem backend */
     clint_dispatch();
     MemValue(true)
   } else if addr == MTIMECMP_BASE & 'n == 4 then {
-    print_platform("clint<4>[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)");
+    if   get_config_print_platform()
+    then print_platform("clint<4>[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)");
     mtimecmp = vector_update_subrange(mtimecmp, 31, 0, sail_zero_extend(data, 32));  /* FIXME: Redundant zero_extend currently required by Lem backend */
     clint_dispatch();
     MemValue(true)
   } else if addr == MTIMECMP_BASE_HI & 'n == 4 then {
-    print_platform("clint<4>[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)");
+    if   get_config_print_platform()
+    then print_platform("clint<4>[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (mtimecmp)");
     mtimecmp = vector_update_subrange(mtimecmp, 63, 32, sail_zero_extend(data, 32)); /* FIXME: Redundant zero_extend currently required by Lem backend */
     clint_dispatch();
     MemValue(true)
   } else {
-    print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (<unmapped>)");
+    if   get_config_print_platform()
+    then print_platform("clint[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data) ^ " (<unmapped>)");
     MemException(E_SAMO_Access_Fault)
   }
 }
@@ -261,8 +276,8 @@ register htif_exit_code : bits(64)
 
 val htif_load : forall 'n, 'n > 0. (xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg}
 function htif_load(addr, width) = {
-  if get_config_print_platform() then
-    print_platform("htif[" ^ BitStr(addr) ^ "] -> " ^ BitStr(htif_tohost));
+  if   get_config_print_platform()
+  then print_platform("htif[" ^ BitStr(addr) ^ "] -> " ^ BitStr(htif_tohost));
   /* FIXME: For now, only allow the expected access widths. */
   if      width == 8 & (addr == plat_htif_tohost())
   then    MemValue(sail_zero_extend(htif_tohost, 64))         /* FIXME: Redundant zero_extend currently required by Lem backend */
@@ -276,7 +291,8 @@ function htif_load(addr, width) = {
 /* The rreg,wreg effects are an artifact of using 'register' to implement device state. */
 val htif_store: forall 'n, 0 < 'n <= 8. (xlenbits, int('n), bits(8 * 'n)) -> MemoryOpResult(bool) effect {rreg,wreg}
 function htif_store(addr, width, data) = {
-  print_platform("htif[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
+  if   get_config_print_platform()
+  then print_platform("htif[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
   /* Store the written value so that we can ack it later. */
   if      width == 8
   then    { htif_tohost = EXTZ(data) }
@@ -290,8 +306,9 @@ function htif_store(addr, width, data) = {
   let cmd = Mk_htif_cmd(htif_tohost);
   match cmd.device() {
     0x00 => { /* syscall-proxy */
-      print_platform("htif-syscall-proxy cmd: " ^ BitStr(cmd.payload()));
-      if cmd.payload()[0] == 0b1
+      if   get_config_print_platform()
+      then print_platform("htif-syscall-proxy cmd: " ^ BitStr(cmd.payload()));
+      if   cmd.payload()[0] == 0b1
       then {
            htif_done = true;
            htif_exit_code = (sail_zero_extend(cmd.payload(), 64) >> 1)
@@ -299,7 +316,8 @@ function htif_store(addr, width, data) = {
       else ()
     },
     0x01 => { /* terminal */
-      print_platform("htif-term cmd: " ^ BitStr(cmd.payload()));
+      if   get_config_print_platform()
+      then print_platform("htif-term cmd: " ^ BitStr(cmd.payload()));
       match cmd.cmd() {
         0x00 => /* TODO: terminal input handling */ (),
         0x01 => plat_term_write(cmd.payload()[7..0]),
@@ -313,7 +331,8 @@ function htif_store(addr, width, data) = {
 
 val htif_tick : unit -> unit effect {rreg, wreg}
 function htif_tick() = {
-  print_platform("htif::tick " ^ BitStr(htif_tohost));
+  if   get_config_print_platform()
+  then print_platform("htif::tick " ^ BitStr(htif_tohost));
   htif_tohost = EXTZ(0b0)  /* htif ack */
 }
 
diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail
index 36f8236..c852677 100644
--- a/model/riscv_regs.sail
+++ b/model/riscv_regs.sail
@@ -134,8 +134,8 @@ function wX (r, in_v) = {
   };
   if (r != 0) then {
      rvfi_wX(r, in_v);
-     if get_config_print_reg() then
-       print_reg("x" ^ string_of_int(r) ^ " <- " ^ RegStr(v));
+     if   get_config_print_reg()
+     then print_reg("x" ^ string_of_int(r) ^ " <- " ^ RegStr(v));
   }
 }
 
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 78fa8fa..2d3adf6 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -10,8 +10,8 @@ function step(step_no) = {
   let (retired, stepped) : (Retired, bool) =
     match dispatchInterrupt(cur_privilege) {
       Some(intr, priv) => {
-        if get_config_print_instr() then 
-          print_bits("Handling interrupt: ", intr);
+        if   get_config_print_instr()
+        then print_bits("Handling interrupt: ", intr);
         handle_interrupt(intr, priv);
         (RETIRE_FAIL, false)
       },
@@ -32,7 +32,8 @@ function step(step_no) = {
           /* non-error cases: */
           F_RVC(h) => {
             let ast = decodeCompressed(h);
-            if get_config_print_instr() then {
+            if   get_config_print_instr()
+            then {
               print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast));
             };
             /* check for RVC once here instead of every RVC execute clause. */
@@ -46,7 +47,8 @@ function step(step_no) = {
           },
           F_Base(w) => {
             let ast = decode(w);
-            if get_config_print_instr() then {
+            if   get_config_print_instr()
+            then {
               print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast));
             };
             nextPC = PC + 4;
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index e852496..a8029a4 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -295,9 +295,10 @@ $endif
 function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits), ext : option(ext_exception))
                      -> xlenbits = {
   rvfi_trap();
-  print_platform("handling " ^ (if intr then "int#" else "exc#")
-                 ^ BitStr(c) ^ " at priv " ^ to_str(del_priv)
-		 ^ " with tval " ^ BitStr(tval(info)));
+  if   get_config_print_platform()
+  then print_platform("handling " ^ (if intr then "int#" else "exc#")
+                      ^ BitStr(c) ^ " at priv " ^ to_str(del_priv)
+                      ^ " with tval " ^ BitStr(tval(info)));
 
   cancel_reservation();
 
@@ -316,7 +317,8 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
 
        handle_trap_extension(del_priv, pc, ext);
 
-       print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
+       if   get_config_print_reg()
+       then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
 
        prepare_trap_vector(del_priv, mcause)
     },
@@ -340,7 +342,8 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
 
        handle_trap_extension(del_priv, pc, ext);
 
-       print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
+       if   get_config_print_reg()
+       then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
 
        prepare_trap_vector(del_priv, scause)
     },
@@ -359,7 +362,8 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
 
        handle_trap_extension(del_priv, pc, ext);
 
-       print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
+       if   get_config_print_reg()
+       then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
 
        prepare_trap_vector(del_priv, ucause)
     }
@@ -371,8 +375,9 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
   match (cur_priv, ctl) {
     (_, CTL_TRAP(e)) => {
       let del_priv = exception_delegatee(e.trap, cur_priv);
-      print_platform("trapping from " ^ to_str(cur_priv) ^ " to " ^ to_str(del_priv)
-                     ^ " to handle " ^ to_str(e.trap));
+      if   get_config_print_platform()
+      then print_platform("trapping from " ^ to_str(cur_priv) ^ " to " ^ to_str(del_priv)
+                          ^ " to handle " ^ to_str(e.trap));
       trap_handler(del_priv, false, e.trap, pc, e.excinfo, e.ext)
     },
     (_, CTL_MRET())  => {
@@ -382,8 +387,10 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       cur_privilege   = privLevel_of_bits(mstatus.MPP());
       mstatus->MPP()  = privLevel_to_bits(if haveUsrMode() then User else Machine);
 
-      print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
-      print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
+      if   get_config_print_reg()
+      then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
+      if   get_config_print_platform()
+      then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
 
       cancel_reservation();
       prepare_xret_target(Machine) & pc_alignment_mask()
@@ -396,9 +403,11 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       /* S-mode implies that U-mode is supported (issue 331 on riscv-isa-manual). */
       mstatus->SPP()  = false;
 
-      print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
-      print_platform("ret-ing from " ^ to_str(prev_priv)
-                     ^ " to " ^ to_str(cur_privilege));
+      if   get_config_print_reg()
+      then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
+      if   get_config_print_platform()
+      then print_platform("ret-ing from " ^ to_str(prev_priv)
+                          ^ " to " ^ to_str(cur_privilege));
 
       cancel_reservation();
       prepare_xret_target(Supervisor) & pc_alignment_mask()
@@ -409,8 +418,10 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       mstatus->UPIE() = true;
       cur_privilege   = User;
 
-      print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
-      print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
+      if   get_config_print_reg()
+      then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
+      if   get_config_print_platform()
+      then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
 
       cancel_reservation();
       prepare_xret_target(User) & pc_alignment_mask()
@@ -468,7 +479,8 @@ function init_sys() -> unit = {
   init_pmp();
 
   // log compatibility with spike
-  print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(EXTZ(0b0) : xlenbits) ^ ")")
+  if   get_config_print_reg()
+  then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(EXTZ(0b0) : xlenbits) ^ ")")
 }
 
 /* memory access exceptions, defined here for use by the platform model. */