Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Rename string_of_int to dec_str #317

Merged
merged 1 commit into from
Feb 5, 2024
Merged

Rename string_of_int to dec_str #317

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 2 additions & 6 deletions model/prelude.sail
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading