Fix Lem bindings

Also generate Lem definitions for full model by default (currently using
list representation for bitvectors).

arm-v8.5-a/Makefile

@@ -20,7 +20,7 @@ aarch64: aarch64.c
 	gcc -O2 aarch64.c $(SAIL_DIR)/lib/*.c -lgmp -lz -I $(SAIL_DIR)/lib/ -o aarch64
 
 aarch64.lem: model/*.sail
-	sail -verbose 1 $(AARCH_FLAGS) $(LEM_FLAGS) $(OPTS) -lem -lem_lib Aarch64_extras model/prelude.sail model/no_devices.sail model/aarch_types.sail model/aarch_mem.sail model/aarch64.sail -o aarch64
+	sail -verbose 1 $(AARCH_FLAGS) $(LEM_FLAGS) $(OPTS) -lem -lem_lib Aarch64_extras -o aarch64 model/prelude.sail model/$(DEVICES) model/aarch_types.sail model/aarch_mem.sail $(AARCH64_SRCS) $(AARCH32_SRCS)
 
 clean:
 	-rm -f aarch64.c.tmp

arm-v8.5-a/aarch64_extras.lem

@@ -77,14 +77,14 @@ let undefined_nat () = return (0:ii)
 val write_ram : forall 'rv 'e.
   integer -> integer -> list bitU -> list bitU -> list bitU -> monad 'rv unit 'e
 let write_ram addrsize size hexRAM address value =
-  write_mem_ea Write_plain address size >>
-  write_mem Write_plain address size value >>= fun _ ->
+  write_mem_ea Write_plain () address size >>
+  write_mem Write_plain () address size value >>= fun _ ->
   return ()
 
 val read_ram : forall 'rv 'e.
   integer -> integer -> list bitU -> list bitU -> monad 'rv (list bitU) 'e
 let read_ram addrsize size hexRAM address =
-  read_mem Read_plain address size
+  read_mem Read_plain () address size
 
 val elf_entry : unit -> integer
 let elf_entry () = 0
@@ -94,4 +94,7 @@ val hex_str : integer -> string
 let hex_str x = ""
 
 val sleep_request : forall 'rv 'e. unit -> monad 'rv unit 'e
-let sleep_request _ = return ()
+let sleep_request _ = return ()
+
+val wakeup_request : forall 'rv 'e. unit -> monad 'rv unit 'e
+let wakeup_request _ = return ()

arm-v8.5-a/model/prelude.sail

@@ -331,7 +331,7 @@ val RoundDown = {ocaml: "round_down", lem: "realFloor", c: "round_down"} : real
 
 val RoundUp = {ocaml: "round_up", lem: "realCeiling", c: "round_up"} : real -> int
 
-val abs_real = "abs_real" : real -> real
+val abs_real = {ocaml: "abs_real", lem: "realAbs", c: "abs_real"} : real -> real
 
 overload abs = {abs_int, abs_real}
 
@@ -352,13 +352,13 @@ overload operator % = {emod_int, modulus}
 
 val Real = {ocaml: "to_real", lem: "realFromInteger", c: "to_real"} : int -> real
 
-val min_nat = {ocaml: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat
+val min_nat = {ocaml: "min_int", lem: "integerMin", c: "min_int"} : (nat, nat) -> nat
 
-val min_int = {ocaml: "min_int", lem: "min", c: "min_int"} : (int, int) -> int
+val min_int = {ocaml: "min_int", lem: "integerMin", c: "min_int"} : (int, int) -> int
 
-val max_nat = {ocaml: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat
+val max_nat = {ocaml: "max_int", lem: "integerMax", c: "max_int"} : (nat, nat) -> nat
 
-val max_int = {ocaml: "max_int", lem: "max", c: "max_int"} : (int, int) -> int
+val max_int = {ocaml: "max_int", lem: "integerMax", c: "max_int"} : (int, int) -> int
 
 overload min = {min_nat, min_int}