From 2258d7d974a560a7bc385446d619047c542c6db1 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 28 Jun 2019 03:45:36 +0100 Subject: Avoid implicit casts to string Can have unintended consequences, due to how overloading interacts with casts. For example, x : X == y : X can be interpreted as eq_string(cast(x), cast(y)) if x and y are both castable to string, even when there is an equality function (X, X) -> bool. Sail->SMT can't handle strings very well so it's best to just ensure that this can never occur. Rather than implicitly casting in logging statements like: print("xyz" ^ x ^ " foo " ^ y) it's now print("xyz" ^ to_str(x) ^ " foo " ^ to_str(y)) which ensures that the conversion to strings only happens where intended. I also added a warning to Sail itself to try to catch these cases in future. --- model/prelude.sail | 2 +- model/riscv_csr_map.sail | 4 +++- model/riscv_insts_end.sail | 4 +++- model/riscv_insts_zicsr.sail | 4 ++-- model/riscv_mem.sail | 2 +- model/riscv_next_control.sail | 2 +- model/riscv_regs.sail | 4 +++- model/riscv_step.sail | 4 ++-- model/riscv_sys_control.sail | 14 ++++++++------ model/riscv_types.sail | 12 +++++++++--- model/riscv_vmem_common.sail | 4 +++- 11 files changed, 36 insertions(+), 20 deletions(-) diff --git a/model/prelude.sail b/model/prelude.sail index 4c232e4..819c789 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -13,7 +13,7 @@ val string_take = "string_take" : (string, nat) -> string val string_length = "string_length" : string -> nat val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string -val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq"} : forall ('a : Type). ('a, 'a) -> bool +val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq", c: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool overload operator == = {eq_string, eq_anything} diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index f484d8d..09b89ad 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -1,6 +1,6 @@ /* Mapping of csr addresses to their names. */ -val cast csr_name : csreg -> string +val csr_name : csreg -> string function csr_name(csr) = { match (csr) { /* user trap setup */ @@ -76,6 +76,8 @@ function csr_name(csr) = { } } +overload to_str = {csr_name} + mapping csr_name_map : csreg <-> string = { /* user trap setup */ 0x000 <-> "ustatus", diff --git a/model/riscv_insts_end.sail b/model/riscv_insts_end.sail index e52f19d..f6223dd 100644 --- a/model/riscv_insts_end.sail +++ b/model/riscv_insts_end.sail @@ -29,9 +29,11 @@ end assembly end encdec end encdec_compressed -val cast print_insn : ast -> string +val print_insn : ast -> string function print_insn insn = assembly(insn) +overload to_str = {print_insn} + val decode : bits(32) -> ast effect pure function decode bv = encdec(bv) diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 3f2bfc2..8e54189 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -94,7 +94,7 @@ function readCSR csr : csreg -> xlenbits = { EXTZ(0x0) } } }; - print_reg("CSR " ^ csr ^ " -> " ^ BitStr(res)); + print_reg("CSR " ^ to_str(csr) ^ " -> " ^ BitStr(res)); res } @@ -164,7 +164,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { _ => None() }; match res { - Some(v) => print_reg("CSR " ^ csr ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"), + Some(v) => print_reg("CSR " ^ to_str(csr) ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"), None() => { /* check extensions */ if ext_write_CSR(csr, value) then () diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 256d6de..db83d7b 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -36,7 +36,7 @@ function phys_mem_read forall 'n, 'n > 0. (t : AccessType, addr : xlenbits, widt (Read, None()) => MemException(E_Load_Access_Fault), (_, None()) => MemException(E_SAMO_Access_Fault), (_, Some(v)) => { if get_config_print_mem() - then print_mem("mem[" ^ t ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v)); + then print_mem("mem[" ^ to_str(t) ^ "," ^ BitStr(addr) ^ "] -> " ^ BitStr(v)); MemValue(v) } } } diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail index 6034aae..7fafb08 100644 --- a/model/riscv_next_control.sail +++ b/model/riscv_next_control.sail @@ -47,7 +47,7 @@ function write_NExt_CSR(csr : csreg, value : xlenbits) -> bool = { _ => None() }; match res { - Some(v) => { print_reg("CSR " ^ csr ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"); + Some(v) => { print_reg("CSR " ^ to_str(csr) ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"); true }, None() => false } diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail index eacc645..17d9552 100644 --- a/model/riscv_regs.sail +++ b/model/riscv_regs.sail @@ -143,7 +143,7 @@ overload X = {rX, wX} /* register names */ -val cast reg_name_abi : regidx -> string +val reg_name_abi : regidx -> string function reg_name_abi(r) = { match (r) { @@ -182,6 +182,8 @@ function reg_name_abi(r) = { } } +overload to_str = {reg_name_abi} + /* mappings for assembly */ val reg_name : bits(5) <-> string diff --git a/model/riscv_step.sail b/model/riscv_step.sail index 7151b69..78fa8fa 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -33,7 +33,7 @@ function step(step_no) = { F_RVC(h) => { let ast = decodeCompressed(h); if get_config_print_instr() then { - print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast); + print_instr("[" ^ string_of_int(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 { @@ -47,7 +47,7 @@ function step(step_no) = { F_Base(w) => { let ast = decode(w); if get_config_print_instr() then { - print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ ast); + print_instr("[" ^ string_of_int(step_no) ^ "] [" ^ to_str(cur_privilege) ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(w) ^ ") " ^ to_str(ast)); }; nextPC = PC + 4; (execute(ext_post_decode_hook(ast)), true) diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index ed0a8de..e852496 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -296,7 +296,8 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen -> xlenbits = { rvfi_trap(); print_platform("handling " ^ (if intr then "int#" else "exc#") - ^ BitStr(c) ^ " at priv " ^ del_priv ^ " with tval " ^ BitStr(tval(info))); + ^ BitStr(c) ^ " at priv " ^ to_str(del_priv) + ^ " with tval " ^ BitStr(tval(info))); cancel_reservation(); @@ -370,8 +371,8 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, match (cur_priv, ctl) { (_, CTL_TRAP(e)) => { let del_priv = exception_delegatee(e.trap, cur_priv); - print_platform("trapping from " ^ cur_priv ^ " to " ^ del_priv - ^ " to handle " ^ e.trap); + print_platform("trapping from " ^ to_str(cur_priv) ^ " to " ^ to_str(del_priv) + ^ " to handle " ^ to_str(e.trap)); trap_handler(del_priv, false, e.trap, pc, e.excinfo, e.ext) }, (_, CTL_MRET()) => { @@ -382,7 +383,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, mstatus->MPP() = privLevel_to_bits(if haveUsrMode() then User else Machine); print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); - print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); + print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); cancel_reservation(); prepare_xret_target(Machine) & pc_alignment_mask() @@ -396,7 +397,8 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, mstatus->SPP() = false; print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); - print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); + print_platform("ret-ing from " ^ to_str(prev_priv) + ^ " to " ^ to_str(cur_privilege)); cancel_reservation(); prepare_xret_target(Supervisor) & pc_alignment_mask() @@ -408,7 +410,7 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result, cur_privilege = User; print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits())); - print_platform("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege); + print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege)); cancel_reservation(); prepare_xret_target(User) & pc_alignment_mask() diff --git a/model/riscv_types.sail b/model/riscv_types.sail index ef8d011..a47afc3 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -81,7 +81,7 @@ function privLevel_of_bits (p) = 0b11 => Machine } -val cast privLevel_to_str : Privilege -> string +val privLevel_to_str : Privilege -> string function privLevel_to_str (p) = match (p) { User => "U", @@ -89,6 +89,8 @@ function privLevel_to_str (p) = Machine => "M" } +overload to_str = {privLevel_to_str} + /* enum denoting whether an executed instruction retires */ enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL} @@ -97,7 +99,7 @@ enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL} enum AccessType = {Read, Write, ReadWrite, Execute} -val cast accessType_to_str : AccessType -> string +val accessType_to_str : AccessType -> string function accessType_to_str (a) = match (a) { Read => "R", @@ -106,6 +108,8 @@ function accessType_to_str (a) = Execute => "X" } +overload to_str = {accessType_to_str} + enum word_width = {BYTE, HALF, WORD, DOUBLE} /* architectural interrupt definitions */ @@ -186,7 +190,7 @@ function exceptionType_to_bits(e) = E_CHERI => 0x20 /* FIXME: this is reserved for a future standard */ } -val cast exceptionType_to_str : ExceptionType -> string +val exceptionType_to_str : ExceptionType -> string function exceptionType_to_str(e) = match (e) { E_Fetch_Addr_Align => "misaligned-fetch", @@ -210,6 +214,8 @@ function exceptionType_to_str(e) = E_CHERI => "CHERI" } +overload to_str = {exceptionType_to_str} + /* model-internal exceptions */ union exception = { diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail index c153579..c8808f7 100644 --- a/model/riscv_vmem_common.sail +++ b/model/riscv_vmem_common.sail @@ -67,7 +67,7 @@ enum PTW_Error = { PTW_Misaligned, /* misaligned superpage */ PTW_PTE_Update /* PTE update needed but not enabled */ } -val cast ptw_error_to_str : PTW_Error -> string +val ptw_error_to_str : PTW_Error -> string function ptw_error_to_str(e) = match (e) { PTW_Access => "mem-access-error", @@ -77,6 +77,8 @@ function ptw_error_to_str(e) = PTW_PTE_Update => "pte-update-needed" } +overload to_str = {ptw_error_to_str} + /* conversion of these translation/PTW failures into architectural exceptions */ function translationException(a : AccessType, f : PTW_Error) -> ExceptionType = { let e : ExceptionType = -- cgit v1.1 From 0fbfc08351dfdc2f57c57f78632ce9bef64d109a Mon Sep 17 00:00:00 2001 From: Jon French Date: Fri, 28 Jun 2019 10:11:41 +0100 Subject: add interpreter extern for string_of_int --- model/prelude.sail | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/model/prelude.sail b/model/prelude.sail index 819c789..cea3d52 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -57,7 +57,7 @@ function cast_unit_vec b = match b { bitone => 0b1 } -val string_of_int = {c: "string_of_int", ocaml: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string +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 BitStr = "string_of_bits" : forall 'n. bits('n) -> string -- cgit v1.1