Rename string_of_int to dec_str

And string_of_bits to bits_str. These are the names that Sail uses so it makes sense to use them.
riscv · Feb 5, 2024 · d5e89a7 · d5e89a7
1 parent 23f1820
commit d5e89a7
Show file tree

Hide file tree

Showing 9 changed files with 17 additions and 21 deletions.
diff --git a/model/prelude.sail b/model/prelude.sail
@@ -94,17 +94,13 @@ overload operator & = {and_vec}
 
 overload operator | = {or_vec}
 
-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 "string_of_bits" : forall 'n. bits('n) -> string
-
-function string_of_bit(b: bit) -> string =
+function bit_str(b: bit) -> string =
   match b {
     bitzero => "0b0",
     bitone => "0b1"
   }
 
-overload BitStr = {string_of_bits, string_of_bit}
+overload BitStr = {bits_str, bit_str}
 
 val int_power = {ocaml: "int_power", interpreter: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int
 

diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail
@@ -261,7 +261,7 @@ function wF (r, in_v) = {
   if   get_config_print_reg()
   then
       /* TODO: will only print bits; should we print in floating point format? */
-      print_reg("f" ^ string_of_int(r) ^ " <- " ^ FRegStr(v));
+      print_reg("f" ^ dec_str(r) ^ " <- " ^ FRegStr(v));
 }
 
 function rF_bits(i: bits(5)) -> flenbits = rF(unsigned(i))

diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail
@@ -204,7 +204,7 @@ 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));
+     then print_reg("x" ^ dec_str(r) ^ " <- " ^ RegStr(v));
   }
 }
 

diff --git a/model/riscv_step.sail b/model/riscv_step.sail
@@ -113,7 +113,7 @@ function step(step_no : int) -> bool = {
             let ast = ext_decode_compressed(h);
             if   get_config_print_instr()
             then {
-              print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast));
+              print_instr("[" ^ dec_str(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 {
@@ -129,7 +129,7 @@ function step(step_no : int) -> bool = {
             let ast = ext_decode(w);
             if   get_config_print_instr()
             then {
-              print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast));
+              print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast));
             };
             nextPC = PC + 4;
             (execute(ast), true)

diff --git a/model/riscv_types.sail b/model/riscv_types.sail
@@ -143,7 +143,7 @@ function not_implemented message = throw(Error_not_implemented(message))
 
 val internal_error : forall ('a : Type). (string, int, string) -> 'a
 function internal_error(file, line, s) = {
-    assert (false, file ^ ":" ^ string_of_int(line) ^ ": " ^ s);
+    assert (false, file ^ ":" ^ dec_str(line) ^ ": " ^ s);
     throw Error_internal_error()
 }
 
@@ -469,9 +469,9 @@ function report_invalid_width(f , l, w, k) -> 'a = {
    * and remove the rest of the function.
    */
   // internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^
-  //   " with xlen=" ^ string_of_int(sizeof(xlen)));
-  assert (false, f ^ ":" ^ string_of_int(l) ^ ": " ^ "Invalid width, "
+  //   " with xlen=" ^ dec_str(sizeof(xlen)));
+  assert (false, f ^ ":" ^ dec_str(l) ^ ": " ^ "Invalid width, "
     ^ size_mnemonic(w) ^ ", for " ^ k ^ " with xlen="
-    ^ string_of_int(sizeof(xlen)));
+    ^ dec_str(sizeof(xlen)));
   throw Error_internal_error()
 }
diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail
@@ -202,7 +202,7 @@ function wV (r, in_v) = {
   let VLEN = unsigned(vlenb) * 8;
   assert(0 < VLEN & VLEN <= sizeof(vlenmax));
   if   get_config_print_reg()
-  then print_reg("v" ^ string_of_int(r) ^ " <- " ^ BitStr(v[VLEN - 1 .. 0]));
+  then print_reg("v" ^ dec_str(r) ^ " <- " ^ BitStr(v[VLEN - 1 .. 0]));
 }
 
 function rV_bits(i: bits(5)) -> vregtype = rV(unsigned(i))

diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail
@@ -84,7 +84,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
   let pte_addr = ptb + pt_ofs;
   match (mem_read_priv(Read(Data), Supervisor, to_phys_addr(pte_addr), 4, false, false, false)) {
     MemException(_) => {
-/*    print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
+/*    print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
             ^ " pt_base=" ^ BitStr(to_phys_addr(ptb))
             ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs))
             ^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr))
@@ -97,7 +97,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
       let ext_pte : extPte = default_sv32_ext_pte;
       let pattr = Mk_PTE_Bits(pbits);
       let is_global = global | (pattr[G] == 0b1);
-/*    print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
+/*    print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
             ^ " pt_base=" ^ BitStr(to_phys_addr(ptb))
             ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs))
             ^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr))

diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
@@ -78,7 +78,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
   let pte_addr = ptb + pt_ofs;
   match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) {
     MemException(_) => {
-/*    print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
+/*    print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
             ^ " pt_base=" ^ BitStr(ptb)
             ^ " pt_ofs=" ^ BitStr(pt_ofs)
             ^ " pte_addr=" ^ BitStr(pte_addr)
@@ -91,7 +91,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
       let ext_pte = pte[Ext];
       let pattr = Mk_PTE_Bits(pbits);
       let is_global = global | (pattr[G] == 0b1);
-/*    print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
+/*    print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
             ^ " pt_base=" ^ BitStr(ptb)
             ^ " pt_ofs=" ^ BitStr(pt_ofs)
             ^ " pte_addr=" ^ BitStr(pte_addr)

diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail
@@ -78,7 +78,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
   let pte_addr = ptb + pt_ofs;
   match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) {
     MemException(_) => {
-/*    print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
+/*    print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
             ^ " pt_base=" ^ BitStr(ptb)
             ^ " pt_ofs=" ^ BitStr(pt_ofs)
             ^ " pte_addr=" ^ BitStr(pte_addr)
@@ -91,7 +91,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
       let ext_pte = pte[Ext];
       let pattr = Mk_PTE_Bits(pbits);
       let is_global = global | (pattr[G] == 0b1);
-/*    print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
+/*    print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
             ^ " pt_base=" ^ BitStr(ptb)
             ^ " pt_ofs=" ^ BitStr(pt_ofs)
             ^ " pte_addr=" ^ BitStr(pte_addr)