diff --git a/model/prelude.sail b/model/prelude.sail index bec76d645..70418ed40 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -126,17 +126,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 6a40606cf..8d43bf945 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 15e7613f0..ae012769d 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 550f11a4a..b32a53927 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 b9402864b..8698bf817 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() } @@ -474,9 +474,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_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index 72def151a..b696a24ed 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 25378a8dc..dc0de390e 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 64c7a542a..26e46f886 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)