diff options
| -rw-r--r-- | riscv/prelude.sail | 4 | ||||
| -rw-r--r-- | riscv/riscv_platform.sail | 8 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 3 |
3 files changed, 10 insertions, 5 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index d5c133fc..88bc00fb 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -496,3 +496,7 @@ function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) = function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) = let v64 : bits(64) = EXTS(v) in (v64 >> shift)[31..0] + +/* Special version of zero_extend that the Lem back-end knows will be at a + case split on 'm and uses a more generic type for. (Temporary hack, honest) */ +val zero_extend_type_hack = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail index 6e3dee93..08c88b38 100644 --- a/riscv/riscv_platform.sail +++ b/riscv/riscv_platform.sail @@ -92,17 +92,17 @@ function clint_load(addr, width) = { if addr == MSIP_BASE & ('n == 8 | 'n == 4) then { print("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mip.MSI())); - MemValue(zero_extend(mip.MSI(), sizeof(8 * 'n))) + MemValue(zero_extend_type_hack(mip.MSI(), sizeof(8 * 'n))) } else if addr == MTIMECMP_BASE & ('n == 8) then { print("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtimecmp)); - MemValue(zero_extend(mtimecmp, 64)) /* FIXME: Redundant zero_extend currently required by Lem backend */ + MemValue(zero_extend_type_hack(mtimecmp, 64)) /* FIXME: Redundant zero_extend currently required by Lem backend */ } else if addr == MTIME_BASE & ('n == 8) then { print("clint[" ^ BitStr(addr) ^ "] -> " ^ BitStr(mtime)); - MemValue(zero_extend(mtime, 64)) + MemValue(zero_extend_type_hack(mtime, 64)) } else { print("clint[" ^ BitStr(addr) ^ "] -> <not-mapped>"); @@ -174,7 +174,7 @@ function htif_load(addr, width) = { print("htif[" ^ BitStr(addr) ^ "] -> " ^ BitStr(htif_tohost)); /* FIXME: For now, only allow the expected access widths. */ if width == 8 - then MemValue(zero_extend(htif_tohost, 64)) /* FIXME: Redundant zero_extend currently required by Lem backend */ + then MemValue(zero_extend_type_hack(htif_tohost, 64)) /* FIXME: Redundant zero_extend currently required by Lem backend */ else MemException(E_Load_Access_Fault) } diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index d300f699..7c1b42ad 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -767,7 +767,8 @@ let doc_exp_lem, doc_let_lem = let t = Env.expand_synonyms env (typ_of full_exp) in let eff = effect_of full_exp in if typ_needs_printed t then - if Id.compare f (mk_id "bitvector_cast_out") <> 0 + if Id.compare f (mk_id "bitvector_cast_out") <> 0 && + Id.compare f (mk_id "zero_extend_type_hack") <> 0 then (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env (effectful eff) t))), true) (* TODO: coordinate with the code in monomorphise.ml to find the correct typing environment to use *) |