Temporary fix for RISC-V Lem generation

2 files changed, 8 insertions, 4 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)
 }