Merge remote-tracking branch 'origin/master' into master-cleanup

11 files changed, 37 insertions, 21 deletions

diff --git a/model/prelude.sail b/model/prelude.sail
index c09171a..22d050f 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -13,7 +13,7 @@ val string_take = "string_take" : (string, nat) -> string
 val string_length = "string_length" : string -> nat
 val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string
 
-val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq"} : forall ('a : Type). ('a, 'a) -> bool
+val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq", c: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
 
 overload operator == = {eq_string, eq_anything}
 
@@ -57,7 +57,7 @@ function cast_unit_vec b = match b {
   bitone  => 0b1
 }
 
-val string_of_int = {c: "string_of_int", ocaml: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string
+val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string
 
 val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
 
diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail
index f484d8d..09b89ad 100644
--- a/model/riscv_csr_map.sail
+++ b/model/riscv_csr_map.sail
@@ -1,6 +1,6 @@
 /* Mapping of csr addresses to their names. */
 
-val cast csr_name : csreg -> string
+val csr_name : csreg -> string
 function csr_name(csr) = {
   match (csr) {
     /* user trap setup */
@@ -76,6 +76,8 @@ function csr_name(csr) = {
   }
 }
 
+overload to_str = {csr_name}
+
 mapping csr_name_map : csreg <-> string = {
     /* user trap setup */
     0x000  <-> "ustatus",
diff --git a/model/riscv_insts_end.sail b/model/riscv_insts_end.sail
index e52f19d..f6223dd 100644
--- a/model/riscv_insts_end.sail
+++ b/model/riscv_insts_end.sail
@@ -29,9 +29,11 @@ end assembly
 end encdec
 end encdec_compressed
 
-val cast print_insn : ast -> string
+val print_insn : ast -> string
 function print_insn insn = assembly(insn)
 
+overload to_str = {print_insn}
+
 val decode : bits(32) -> ast effect pure
 function decode bv = encdec(bv)
 
diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail
index 3f2bfc2..8e54189 100644
--- a/model/riscv_insts_zicsr.sail
+++ b/model/riscv_insts_zicsr.sail
@@ -94,7 +94,7 @@ function readCSR csr : csreg -> xlenbits = {
                                     EXTZ(0x0) }
                    }
   };
-  print_reg("CSR " ^ csr ^ " -> " ^ BitStr(res));
+  print_reg("CSR " ^ to_str(csr) ^ " -> " ^ BitStr(res));
   res
 }
 
@@ -164,7 +164,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     _           => None()
   };
   match res {
-    Some(v) => print_reg("CSR " ^ csr ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"),
+    Some(v) => 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_mem.sail b/model/riscv_mem.sail
index c44be53..364c4d6 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -36,7 +36,7 @@ function phys_mem_read forall 'n, 'n > 0. (t : AccessType, addr : xlenbits, widt
     (Read,    None()) => MemException(E_Load_Access_Fault),
     (_,       None()) => MemException(E_SAMO_Access_Fault),
     (_,      Some(v)) => { if   get_config_print_mem()
-                           then print_mem("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
+                           then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v));
                            MemValue(v) }
   }
 }
diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail
index 6034aae..7fafb08 100644
--- a/model/riscv_next_control.sail
+++ b/model/riscv_next_control.sail
@@ -47,7 +47,7 @@ function write_NExt_CSR(csr : csreg, value : xlenbits) -> bool = {
     _     => None()
   };
   match res {
-    Some(v) => { print_reg("CSR " ^ csr ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")");
+    Some(v) => { print_reg("CSR " ^ to_str(csr) ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")");
                  true },
     None()  => false
   }
diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail
index 09f22ff..36f8236 100644
--- a/model/riscv_regs.sail
+++ b/model/riscv_regs.sail
@@ -143,7 +143,7 @@ overload X = {rX, wX}
 
 /* register names */
 
-val cast reg_name_abi : regidx -> string
+val reg_name_abi : regidx -> string
 
 function reg_name_abi(r) = {
   match (r) {
@@ -182,6 +182,8 @@ function reg_name_abi(r) = {
   }
 }
 
+overload to_str = {reg_name_abi}
+
 /* mappings for assembly */
 
 val reg_name : bits(5) <-> string
diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 7151b69..78fa8fa 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -33,7 +33,7 @@ function step(step_no) = {
           F_RVC(h) => {
             let ast = decodeCompressed(h);
             if get_config_print_instr() then {
-              print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast);
+              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. */
             if haveRVC() then {
@@ -47,7 +47,7 @@ function step(step_no) = {
           F_Base(w) => {
             let ast = decode(w);
             if get_config_print_instr() then {
-              print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ ast);
+              print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast));
             };
             nextPC = PC + 4;
             (execute(ext_post_decode_hook(ast)), true)
diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
index ed0a8de..e852496 100644
--- a/model/riscv_sys_control.sail
+++ b/model/riscv_sys_control.sail
@@ -296,7 +296,8 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
                      -> xlenbits = {
   rvfi_trap();
   print_platform("handling " ^ (if intr then "int#" else "exc#")
-                 ^ BitStr(c) ^ " at priv " ^ del_priv ^ " with tval " ^ BitStr(tval(info)));
+                 ^ BitStr(c) ^ " at priv " ^ to_str(del_priv)
+		 ^ " with tval " ^ BitStr(tval(info)));
 
   cancel_reservation();
 
@@ -370,8 +371,8 @@ 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 " ^ cur_priv ^ " to " ^ del_priv
-                     ^ " to handle " ^ e.trap);
+      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,7 +383,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       mstatus->MPP()  = privLevel_to_bits(if haveUsrMode() then User else Machine);
 
       print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
-      print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
+      print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
 
       cancel_reservation();
       prepare_xret_target(Machine) & pc_alignment_mask()
@@ -396,7 +397,8 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       mstatus->SPP()  = false;
 
       print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
-      print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
+      print_platform("ret-ing from " ^ to_str(prev_priv)
+                     ^ " to " ^ to_str(cur_privilege));
 
       cancel_reservation();
       prepare_xret_target(Supervisor) & pc_alignment_mask()
@@ -408,7 +410,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       cur_privilege   = User;
 
       print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()));
-      print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
+      print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
 
       cancel_reservation();
       prepare_xret_target(User) & pc_alignment_mask()
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index ef8d011..a47afc3 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -81,7 +81,7 @@ function privLevel_of_bits (p) =
     0b11 => Machine
   }
 
-val cast privLevel_to_str : Privilege -> string
+val privLevel_to_str : Privilege -> string
 function privLevel_to_str (p) =
   match (p) {
     User       => "U",
@@ -89,6 +89,8 @@ function privLevel_to_str (p) =
     Machine    => "M"
   }
 
+overload to_str = {privLevel_to_str}
+
 /* enum denoting whether an executed instruction retires */
 
 enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL}
@@ -97,7 +99,7 @@ enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL}
 
 enum AccessType = {Read, Write, ReadWrite, Execute}
 
-val cast accessType_to_str : AccessType -> string
+val accessType_to_str : AccessType -> string
 function accessType_to_str (a) =
   match (a) {
     Read      => "R",
@@ -106,6 +108,8 @@ function accessType_to_str (a) =
     Execute   => "X"
   }
 
+overload to_str = {accessType_to_str}
+
 enum word_width = {BYTE, HALF, WORD, DOUBLE}
 
 /* architectural interrupt definitions */
@@ -186,7 +190,7 @@ function exceptionType_to_bits(e) =
     E_CHERI              => 0x20    /* FIXME: this is reserved for a future standard */
   }
 
-val cast exceptionType_to_str : ExceptionType -> string
+val exceptionType_to_str : ExceptionType -> string
 function exceptionType_to_str(e) =
   match (e) {
     E_Fetch_Addr_Align   => "misaligned-fetch",
@@ -210,6 +214,8 @@ function exceptionType_to_str(e) =
     E_CHERI              => "CHERI"
   }
 
+overload to_str = {exceptionType_to_str}
+
 /* model-internal exceptions */
 
 union exception = {
diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail
index c153579..c8808f7 100644
--- a/model/riscv_vmem_common.sail
+++ b/model/riscv_vmem_common.sail
@@ -67,7 +67,7 @@ enum PTW_Error = {
   PTW_Misaligned,   /* misaligned superpage */
   PTW_PTE_Update    /* PTE update needed but not enabled */
 }
-val cast ptw_error_to_str : PTW_Error -> string
+val ptw_error_to_str : PTW_Error -> string
 function ptw_error_to_str(e) =
   match (e) {
     PTW_Access        => "mem-access-error",
@@ -77,6 +77,8 @@ function ptw_error_to_str(e) =
     PTW_PTE_Update    => "pte-update-needed"
   }
 
+overload to_str = {ptw_error_to_str}
+
 /* conversion of these translation/PTW failures into architectural exceptions */
 function translationException(a : AccessType, f : PTW_Error) -> ExceptionType = {
   let e : ExceptionType =