From ec4652a740eb998766f8ee60b2fbaafc3d5dd4e4 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 22 May 2018 11:00:36 +0100
Subject: Fix Lem build for RISC-V

---
 riscv/riscv_extras.lem    | 29 +++++++++++++++++++++++------
 riscv/riscv_platform.sail | 12 ++++++------
 2 files changed, 29 insertions(+), 12 deletions(-)

diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index 491dd56d..b93073de 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -44,12 +44,29 @@ let read_ram addrsize size hexRAM address =
 
 let speculate_conditional_success () = excl_result ()
 
-val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> bitvector 'a
-let get_slice_int len n lo =
-  (* TODO: Is this the intended behaviour? *)
-  let hi = lo + len - 1 in
-  let bits = bits_of_int (hi + 1) n in
-  of_bits_failwith (subrange_list false bits hi lo)
+val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_ram_base () = wordFromInteger 0
+declare ocaml target_rep function plat_ram_base = `Platform.dram_base`
+
+val plat_ram_size : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_ram_size () = wordFromInteger 0
+declare ocaml target_rep function plat_ram_size = `Platform.dram_size`
+
+val plat_rom_base : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_rom_base () = wordFromInteger 0
+declare ocaml target_rep function plat_rom_base = `Platform.rom_base`
+
+val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_rom_size () = wordFromInteger 0
+declare ocaml target_rep function plat_rom_size = `Platform.rom_size`
+
+val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_clint_base () = wordFromInteger 0
+declare ocaml target_rep function plat_clint_base = `Platform.clint_base`
+
+val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a
+let plat_clint_size () = wordFromInteger 0
+declare ocaml target_rep function plat_clint_size = `Platform.clint_size`
 
 val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
 let shift_bits_right v m = shiftr v (uint m)
diff --git a/riscv/riscv_platform.sail b/riscv/riscv_platform.sail
index 75cf9b03..009090f1 100644
--- a/riscv/riscv_platform.sail
+++ b/riscv/riscv_platform.sail
@@ -7,16 +7,16 @@
 */
 
 /* Main memory */
-val plat_ram_base = {ocaml: "Platform.dram_base"} : unit -> xlenbits
-val plat_ram_size = {ocaml: "Platform.dram_size"} : unit -> xlenbits
+val plat_ram_base = {ocaml: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits
+val plat_ram_size = {ocaml: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits
 
 /* ROM holding reset vector and device-tree DTB */
-val plat_rom_base = {ocaml: "Platform.rom_base"} : unit -> xlenbits
-val plat_rom_size = {ocaml: "Platform.rom_size"} : unit -> xlenbits
+val plat_rom_base = {ocaml: "Platform.rom_base", lem: "plat_rom_base"} : unit -> xlenbits
+val plat_rom_size = {ocaml: "Platform.rom_size", lem: "plat_rom_size"} : unit -> xlenbits
 
 /* Location of clock-interface, which should match with the spec in the DTB */
-val plat_clint_base = {ocaml: "Platform.clint_base"} : unit -> xlenbits
-val plat_clint_size = {ocaml: "Platform.clint_size"} : unit -> xlenbits
+val plat_clint_base = {ocaml: "Platform.clint_base", lem: "plat_clint_base"} : unit -> xlenbits
+val plat_clint_size = {ocaml: "Platform.clint_size", lem: "plat_clint_size"} : unit -> xlenbits
 
 val phys_mem_segments : unit -> (xlenbits, xlenbits)
 function phys_mem_segments() =
-- 
cgit v1.2.3