From 97abd354d62abdab64fb0164ea79bbff3ed2443a Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Tue, 10 Oct 2023 12:41:22 +0100 Subject: [PATCH] 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. --- model/prelude.sail | 8 ++------ model/riscv_fdext_regs.sail | 2 +- model/riscv_regs.sail | 2 +- model/riscv_step.sail | 4 ++-- model/riscv_types.sail | 8 ++++---- model/riscv_vext_regs.sail | 2 +- model/riscv_vmem_sv32.sail | 4 ++-- model/riscv_vmem_sv39.sail | 4 ++-- model/riscv_vmem_sv48.sail | 4 ++-- 9 files changed, 17 insertions(+), 21 deletions(-) diff --git a/model/prelude.sail b/model/prelude.sail index c5eb94fba..3edec051d 100644 --- 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 index d7786f33b..479348600 100644 --- 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 index 7890a11fa..aa1d5e635 100644 --- 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 index a71d85561..ec7d58e3a 100644 --- 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 index 14916c7ef..2f46156cf 100644 --- 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 index b74e081ec..9b81e32e9 100644 --- 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 index 3b3ce1c9e..15e8ef258 100644 --- 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 index 058d749cc..51e4946d9 100644 --- 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 index 51eab1413..4c23e49b0 100644 --- 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)