diff options
| author | Alasdair <alasdair.armstrong@gmail.com> | 2019-06-28 03:45:36 +0100 |
|---|---|---|
| committer | Alasdair <alasdair.armstrong@gmail.com> | 2019-06-28 03:45:36 +0100 |
| commit | 2258d7d974a560a7bc385446d619047c542c6db1 (patch) | |
| tree | 5a0af4b52a7e01713846f0477bc4c3f1df4442dc /model/riscv_insts_end.sail | |
| parent | 83c3ec61ffb62d618cdf5c1682bb605c4887584b (diff) | |
| download | sail-riscv-2258d7d974a560a7bc385446d619047c542c6db1.zip sail-riscv-2258d7d974a560a7bc385446d619047c542c6db1.tar.gz sail-riscv-2258d7d974a560a7bc385446d619047c542c6db1.tar.bz2 | |
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.
Diffstat (limited to 'model/riscv_insts_end.sail')
| -rw-r--r-- | model/riscv_insts_end.sail | 4 |
1 files changed, 3 insertions, 1 deletions
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) |