Fix Lem generation for CHERI-MIPS and Aarch64

- Update Lem bindings and extras files
- Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's
  (used for cap_size in the CHERI spec)
- Add Lem and Isabelle Makefile targets for CHERI

1 files changed, 66 insertions, 66 deletions

diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem
index 8af9ee5d..0a6bab11 100644
--- a/aarch64/mono/aarch64_extras.lem
+++ b/aarch64/mono/aarch64_extras.lem
@@ -3,7 +3,7 @@ open import Sail_instr_kinds
 open import Sail_values
 open import Sail_operators_mwords
 open import Prompt_monad
-open import State
+open import Prompt
 
 type ty512
 instance (Size ty512) let size = 512 end
@@ -26,11 +26,6 @@ val putchar : integer -> unit
 let putchar _ = ()
 declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
 
-val uint : forall 'a. Size 'a => mword 'a -> integer
-let uint = unsigned
-val sint : forall 'a. Size 'a => mword 'a -> integer
-let sint = signed
-
 val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
 let slice v lo len =
   subrange_vec_dec v (lo + len - 1) lo
@@ -42,28 +37,28 @@ let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
 let get_slice_int_bl len n lo =
   (* TODO: Is this the intended behaviour? *)
   let hi = lo + len - 1 in
-  let bits = bits_of_int (hi + 1) n in
-  get_bits false bits hi lo
+  let bs = bools_of_int (hi + 1) n in
+  subrange_list false bs hi lo
 
 val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a
-let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo)
+let get_slice_int len n lo = of_bools (get_slice_int_bl len n lo)
 
 val set_slice_int :  forall 'a. Size 'a => integer -> integer -> integer -> mword 'a -> integer
 let set_slice_int len n lo v =
   let hi = lo + len - 1 in
-  let bits = bitlist_of_int n in
-  let len_n = max (hi + 1) (integerFromNat (List.length bits)) in
-  let ext_bits = exts_bits len_n bits in
-  signed (set_bits false ext_bits hi lo (bits_of v))
+  let bs = bool_list_of_int n in
+  let len_n = max (hi + 1) (integerFromNat (List.length bs)) in
+  let ext_bs = exts_bools len_n bs in
+  signed_of_bools (update_subrange_list false ext_bs hi lo (bitlistFromWord v))
 
-let ext_slice signed v i j =
+(*let ext_slice signed v i j =
   let len = length v in
   let bits = get_bits false (bits_of v) i j in
   of_bits (if signed then exts_bits len bits else extz_bits len bits)
 val exts_slice : list bitU -> integer -> integer -> list bitU
 let exts_slice v i j = ext_slice true v i j
 val extz_slice : list bitU -> integer -> integer -> list bitU
-let extz_slice v i j = ext_slice false v i j
+let extz_slice v i j = ext_slice false v i j*)
 
 val shr_int : ii -> ii -> ii
 let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
@@ -71,61 +66,66 @@ let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
 val shl_int : integer -> integer -> integer
 let rec shl_int i shift = if shift > 0 then 2 * shl_int i (shift - 1) else i
 
-let hexchar_to_bitlist c =
-  if c = #'0' then [B0;B0;B0;B0]
-  else if c = #'1' then [B0;B0;B0;B1]
-  else if c = #'2' then [B0;B0;B1;B0]
-  else if c = #'3' then [B0;B0;B1;B1]
-  else if c = #'4' then [B0;B1;B0;B0]
-  else if c = #'5' then [B0;B1;B0;B1]
-  else if c = #'6' then [B0;B1;B1;B0]
-  else if c = #'7' then [B0;B1;B1;B1]
-  else if c = #'8' then [B1;B0;B0;B0]
-  else if c = #'9' then [B1;B0;B0;B1]
-  else if c = #'A' then [B1;B0;B1;B0]
-  else if c = #'a' then [B1;B0;B1;B0]
-  else if c = #'B' then [B1;B0;B1;B1]
-  else if c = #'b' then [B1;B0;B1;B1]
-  else if c = #'C' then [B1;B1;B0;B0]
-  else if c = #'c' then [B1;B1;B0;B0]
-  else if c = #'D' then [B1;B1;B0;B1]
-  else if c = #'d' then [B1;B1;B0;B1]
-  else if c = #'E' then [B1;B1;B1;B0]
-  else if c = #'e' then [B1;B1;B1;B0]
-  else if c = #'F' then [B1;B1;B1;B1]
-  else if c = #'f' then [B1;B1;B1;B1]
-  else failwith "hexchar_to_bitlist given unrecognized character"
-
-let hexstring_to_bits s =
+let hexchar_to_bool_list c =
+  if c = #'0' then      Just ([false;false;false;false])
+  else if c = #'1' then Just ([false;false;false;true ])
+  else if c = #'2' then Just ([false;false;true; false])
+  else if c = #'3' then Just ([false;false;true; true ])
+  else if c = #'4' then Just ([false;true; false;false])
+  else if c = #'5' then Just ([false;true; false;true ])
+  else if c = #'6' then Just ([false;true; true; false])
+  else if c = #'7' then Just ([false;true; true; true ])
+  else if c = #'8' then Just ([true; false;false;false])
+  else if c = #'9' then Just ([true; false;false;true ])
+  else if c = #'A' then Just ([true; false;true; false])
+  else if c = #'a' then Just ([true; false;true; false])
+  else if c = #'B' then Just ([true; false;true; true ])
+  else if c = #'b' then Just ([true; false;true; true ])
+  else if c = #'C' then Just ([true; true; false;false])
+  else if c = #'c' then Just ([true; true; false;false])
+  else if c = #'D' then Just ([true; true; false;true ])
+  else if c = #'d' then Just ([true; true; false;true ])
+  else if c = #'E' then Just ([true; true; true; false])
+  else if c = #'e' then Just ([true; true; true; false])
+  else if c = #'F' then Just ([true; true; true; true ])
+  else if c = #'f' then Just ([true; true; true; true ])
+  else Nothing
+
+let hexstring_to_bools s =
   match (toCharList s) with
-  | z :: x :: hs ->
-    let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
-    List.concat (List.map hexchar_to_bitlist str)
-  | _ -> failwith "hexstring_to_bits called with unexpected string"
+    | z :: x :: hs ->
+       let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
+       Maybe.map List.concat (just_list (List.map hexchar_to_bool_list str))
+    | _ -> Nothing
   end
 
-val hex_slice : forall 'n. Size 'n => string -> integer -> integer -> mword 'n
+val hex_slice : forall 'rv 'n 'e. Size 'n => string -> integer -> integer -> monad 'rv (mword 'n) 'e
 let hex_slice v len lo =
-  let hi = len + lo - 1 in
-  let bits = extz_bits (len + lo) (hexstring_to_bits v) in
-  of_bits (get_bits false bits hi lo)
-
-let internal_pick vs = head vs
-
-let undefined_string () = ""
-let undefined_unit () = ()
-let undefined_int () = (0:ii)
-let undefined_bool () = false
-val undefined_vector : forall 'a. integer -> 'a -> list 'a
-let undefined_vector len u = repeat [u] len
-val undefined_bitvector : forall 'a. Size 'a => integer -> mword 'a
-let undefined_bitvector len = duplicate B0 len
-let undefined_bits len = undefined_bitvector len
-let undefined_bit () = B0
-let undefined_real () = realFromFrac 0 1
-let undefined_range i j = i
-let undefined_atom i = i
-let undefined_nat () = (0:ii)
+  match hexstring_to_bools v with
+    | Just bs ->
+       let hi = len + lo - 1 in
+       let bs = ext_list false (len + lo) bs in
+       return (of_bools (subrange_list false bs hi lo))
+    | Nothing -> Fail "hex_slice"
+  end
+
+let internal_pick vs = return (head vs)
+
+(* Use constants for undefined values for now *)
+let undefined_string () = return ""
+let undefined_unit () = return ()
+let undefined_int () = return (0:ii)
+val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e
+let undefined_vector len u = return (repeat [u] len)
+val undefined_bitvector : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e
+let undefined_bitvector len = return (of_bools (repeat [false] len))
+val undefined_bits : forall 'rv 'a 'e. Size 'a => integer -> monad 'rv (mword 'a) 'e
+let undefined_bits = undefined_bitvector
+let undefined_bit () = return B0
+let undefined_real () = return (realFromFrac 0 1)
+let undefined_range i j = return i
+let undefined_atom i = return i
+let undefined_nat () = return (0:ii)
 
 let write_ram addrsize size hexRAM address value =
   write_mem_ea Write_plain address size >>