Skip to content

Commit d5e89a7

Browse files
Timmmmbillmcspadden-riscv
Timmmm
authored and
billmcspadden-riscv
committed
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.
1 parent 23f1820 commit d5e89a7

File tree

9 files changed

+17
-21
lines changed

9 files changed

+17
-21
lines changed

‎model/prelude.sail‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -94,17 +94,13 @@ overload operator & = {and_vec}
9494

9595
overload operator | = {or_vec}
9696

97-
val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string
98-
99-
val "string_of_bits" : forall 'n. bits('n) -> string
100-
101-
function string_of_bit(b: bit) -> string =
97+
function bit_str(b: bit) -> string =
10298
match b {
10399
bitzero => "0b0",
104100
bitone => "0b1"
105101
}
106102

107-
overload BitStr = {string_of_bits, string_of_bit}
103+
overload BitStr = {bits_str, bit_str}
108104

109105
val int_power = {ocaml: "int_power", interpreter: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int
110106

‎model/riscv_fdext_regs.sail‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -261,7 +261,7 @@ function wF (r, in_v) = {
261261
if get_config_print_reg()
262262
then
263263
/* TODO: will only print bits; should we print in floating point format? */
264-
print_reg("f" ^ string_of_int(r) ^ " <- " ^ FRegStr(v));
264+
print_reg("f" ^ dec_str(r) ^ " <- " ^ FRegStr(v));
265265
}
266266

267267
function rF_bits(i: bits(5)) -> flenbits = rF(unsigned(i))

‎model/riscv_regs.sail‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -204,7 +204,7 @@ function wX (r, in_v) = {
204204
if (r != 0) then {
205205
rvfi_wX(r, in_v);
206206
if get_config_print_reg()
207-
then print_reg("x" ^ string_of_int(r) ^ " <- " ^ RegStr(v));
207+
then print_reg("x" ^ dec_str(r) ^ " <- " ^ RegStr(v));
208208
}
209209
}
210210

‎model/riscv_step.sail‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -113,7 +113,7 @@ function step(step_no : int) -> bool = {
113113
let ast = ext_decode_compressed(h);
114114
if get_config_print_instr()
115115
then {
116-
print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast));
116+
print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ to_str(ast));
117117
};
118118
/* check for RVC once here instead of every RVC execute clause. */
119119
if haveRVC() then {
@@ -129,7 +129,7 @@ function step(step_no : int) -> bool = {
129129
let ast = ext_decode(w);
130130
if get_config_print_instr()
131131
then {
132-
print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast));
132+
print_instr("[" ^ dec_str(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast));
133133
};
134134
nextPC = PC + 4;
135135
(execute(ast), true)

‎model/riscv_types.sail‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -143,7 +143,7 @@ function not_implemented message = throw(Error_not_implemented(message))
143143

144144
val internal_error : forall ('a : Type). (string, int, string) -> 'a
145145
function internal_error(file, line, s) = {
146-
assert (false, file ^ ":" ^ string_of_int(line) ^ ": " ^ s);
146+
assert (false, file ^ ":" ^ dec_str(line) ^ ": " ^ s);
147147
throw Error_internal_error()
148148
}
149149

@@ -469,9 +469,9 @@ function report_invalid_width(f , l, w, k) -> 'a = {
469469
* and remove the rest of the function.
470470
*/
471471
// internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^
472-
// " with xlen=" ^ string_of_int(sizeof(xlen)));
473-
assert (false, f ^ ":" ^ string_of_int(l) ^ ": " ^ "Invalid width, "
472+
// " with xlen=" ^ dec_str(sizeof(xlen)));
473+
assert (false, f ^ ":" ^ dec_str(l) ^ ": " ^ "Invalid width, "
474474
^ size_mnemonic(w) ^ ", for " ^ k ^ " with xlen="
475-
^ string_of_int(sizeof(xlen)));
475+
^ dec_str(sizeof(xlen)));
476476
throw Error_internal_error()
477477
}

‎model/riscv_vext_regs.sail‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -202,7 +202,7 @@ function wV (r, in_v) = {
202202
let VLEN = unsigned(vlenb) * 8;
203203
assert(0 < VLEN & VLEN <= sizeof(vlenmax));
204204
if get_config_print_reg()
205-
then print_reg("v" ^ string_of_int(r) ^ " <- " ^ BitStr(v[VLEN - 1 .. 0]));
205+
then print_reg("v" ^ dec_str(r) ^ " <- " ^ BitStr(v[VLEN - 1 .. 0]));
206206
}
207207

208208
function rV_bits(i: bits(5)) -> vregtype = rV(unsigned(i))

‎model/riscv_vmem_sv32.sail‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
8484
let pte_addr = ptb + pt_ofs;
8585
match (mem_read_priv(Read(Data), Supervisor, to_phys_addr(pte_addr), 4, false, false, false)) {
8686
MemException(_) => {
87-
/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
87+
/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
8888
^ " pt_base=" ^ BitStr(to_phys_addr(ptb))
8989
^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs))
9090
^ " 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) = {
9797
let ext_pte : extPte = default_sv32_ext_pte;
9898
let pattr = Mk_PTE_Bits(pbits);
9999
let is_global = global | (pattr[G] == 0b1);
100-
/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
100+
/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
101101
^ " pt_base=" ^ BitStr(to_phys_addr(ptb))
102102
^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs))
103103
^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr))

‎model/riscv_vmem_sv39.sail‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
7878
let pte_addr = ptb + pt_ofs;
7979
match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) {
8080
MemException(_) => {
81-
/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
81+
/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
8282
^ " pt_base=" ^ BitStr(ptb)
8383
^ " pt_ofs=" ^ BitStr(pt_ofs)
8484
^ " pte_addr=" ^ BitStr(pte_addr)
@@ -91,7 +91,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
9191
let ext_pte = pte[Ext];
9292
let pattr = Mk_PTE_Bits(pbits);
9393
let is_global = global | (pattr[G] == 0b1);
94-
/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
94+
/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
9595
^ " pt_base=" ^ BitStr(ptb)
9696
^ " pt_ofs=" ^ BitStr(pt_ofs)
9797
^ " pte_addr=" ^ BitStr(pte_addr)

‎model/riscv_vmem_sv48.sail‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -78,7 +78,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
7878
let pte_addr = ptb + pt_ofs;
7979
match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) {
8080
MemException(_) => {
81-
/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
81+
/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
8282
^ " pt_base=" ^ BitStr(ptb)
8383
^ " pt_ofs=" ^ BitStr(pt_ofs)
8484
^ " pte_addr=" ^ BitStr(pte_addr)
@@ -91,7 +91,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
9191
let ext_pte = pte[Ext];
9292
let pattr = Mk_PTE_Bits(pbits);
9393
let is_global = global | (pattr[G] == 0b1);
94-
/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)
94+
/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
9595
^ " pt_base=" ^ BitStr(ptb)
9696
^ " pt_ofs=" ^ BitStr(pt_ofs)
9797
^ " pte_addr=" ^ BitStr(pte_addr)

0 commit comments

Comments
 (0)