Skip to content

Commit

Permalink
Rename string_of_int to dec_str
Browse files Browse the repository at this point in the history 
And string_of_bits to bits_str. These are the names that Sail uses so it makes sense to use them.
  • Loading branch information
@Timmmm
Timmmm committed Feb 2, 2024
1 parent 23f1820 commit 97abd35
Show file tree
Hide file tree
Showing 9 changed files with 17 additions and 21 deletions.
8 changes: 2 additions & 6 deletions model/prelude.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion model/riscv_fdext_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));
}
}

Expand Down
4 changes: 2 additions & 2 deletions model/riscv_step.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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)
Expand Down
8 changes: 4 additions & 4 deletions model/riscv_types.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()
}

Expand Down Expand Up @@ -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()
}
2 changes: 1 addition & 1 deletion model/riscv_vext_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_vmem_sv32.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand All @@ -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))
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_vmem_sv39.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_vmem_sv48.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand Down

0 comments on commit 97abd35

Please sign in to comment.