From c3f3642dfa5647685ae3dea86beeef8abc27f026 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 4 May 2018 17:44:07 +0100
Subject: Support short-circuiting of Boolean expressions in Lem

---
 src/gen_lib/prompt.lem | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index de683047..830f2350 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -38,6 +38,12 @@ end
 
 declare {isabelle} termination_argument foreachM = automatic
 
+val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
+let and_boolM l r = l >>= (fun l -> if l then r else return false)
+
+val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
+let or_boolM l r = l >>= (fun l -> if l then return true else r)
+
 val bool_of_bitU_fail : forall 'rv 'e. bitU -> monad 'rv bool 'e
 let bool_of_bitU_fail = function
   | B0 -> return false
-- 
cgit v1.2.3


From c6710bb09c1d492b4434f0b3b375750275b4d4b5 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 4 May 2018 17:46:10 +0100
Subject: Run ARM built-in tests for Lem backend (via OCaml)

---
 src/gen_lib/sail_operators.lem          | 12 ++++++++++++
 src/gen_lib/sail_operators_bitlists.lem | 17 +++++++++++++++++
 src/gen_lib/sail_operators_mwords.lem   | 17 +++++++++++++++++
 3 files changed, 46 insertions(+)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index d4275c87..78aab65e 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -223,3 +223,15 @@ let inline ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedInteger
 
 val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool
 let inline scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r)
+
+val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
+let get_slice_int_bv len n lo =
+  let hi = lo + len - 1 in
+  let bs = bools_of_int (hi + 1) n in
+  of_bools (subrange_list false bs hi lo)
+
+val set_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a -> integer
+let set_slice_int_bv len n lo v =
+  let hi = lo + len - 1 in
+  let bs = bits_of_int (hi + 1) n in
+  maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo (bits_of v)))
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
index b0a29b5e..fed293b4 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -35,6 +35,9 @@ let zero_extend bits len = extz_bits len bits
 val sign_extend : list bitU -> integer -> list bitU
 let sign_extend bits len = exts_bits len bits
 
+val zeros : integer -> list bitU
+let zeros len = repeat [B0] len
+
 val vector_truncate : list bitU -> integer -> list bitU
 let vector_truncate bs len = extz_bv len bs
 
@@ -289,6 +292,20 @@ let duplicate_oracle b n =
 val reverse_endianness : list bitU -> list bitU
 let reverse_endianness v = reverse_endianness_list v
 
+val get_slice_int : integer -> integer -> integer -> list bitU
+let get_slice_int = get_slice_int_bv
+
+val set_slice_int : integer -> integer -> integer -> list bitU -> integer
+let set_slice_int = set_slice_int_bv
+
+val slice : list bitU -> integer -> integer -> list bitU
+let slice v lo len =
+  subrange_vec_dec v (lo + len - 1) lo
+
+val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
+let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
+  update_subrange_vec_dec out (n + slice_len - 1) n v
+
 val eq_vec    : list bitU -> list bitU -> bool
 val neq_vec   : list bitU -> list bitU -> bool
 val ult_vec   : list bitU -> list bitU -> bool
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 8bcc0319..077dfb02 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -76,6 +76,9 @@ let zero_extend w _ = Machine_word.zeroExtend w
 val sign_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
 let sign_extend w _ = Machine_word.signExtend w
 
+val zeros : forall 'a. Size 'a => integer -> mword 'a
+let zeros _ = Machine_word.wordFromNatural 0
+
 val vector_truncate : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b
 let vector_truncate w _ = Machine_word.zeroExtend w
 
@@ -310,6 +313,20 @@ let duplicate        b n = maybe_failwith (duplicate_maybe b n)
 val reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a
 let reverse_endianness v = wordFromBitlist (reverse_endianness_list (bitlistFromWord v))
 
+val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a
+let get_slice_int = get_slice_int_bv
+
+val set_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a -> integer
+let set_slice_int = set_slice_int_bv
+
+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
+
+val set_slice : forall 'a 'b. Size 'a, Size 'b => integer -> integer -> mword 'a -> integer -> mword 'b -> mword 'a
+let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
+  update_subrange_vec_dec out (n + slice_len - 1) n v
+
 val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val ult_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-- 
cgit v1.2.3


From 972d349919fc5ebe911604330ea3c80e70fdcfad Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 8 May 2018 18:48:18 +0100
Subject: Add tests for Isabelle->OCaml generation for CHERI and AArch64

---
 src/gen_lib/state_monad.lem | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index 8253b800..a2919762 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -265,3 +265,16 @@ let update_reg_field_bit regfield i reg_val bit =
   let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in
   regfield.set_field reg_val new_field_value
 let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)*)
+
+(* TODO Add Show typeclass for value and exception type *)
+val show_result : forall 'a 'e. result 'a 'e -> string
+let show_result = function
+  | Value _ -> "Value ()"
+  | Ex (Failure msg) -> "Failure " ^ msg
+  | Ex (Throw _) -> "Throw"
+end
+
+val prerr_results : forall 'a 'e 's. SetType 's => set (result 'a 'e * 's) -> unit
+let prerr_results rs =
+  let _ = Set.map (fun (r, _) -> let _ = prerr_endline (show_result r) in ()) rs in
+  ()
-- 
cgit v1.2.3


From c498c8a7f8d448dcefd1692e7562878cc6feb62b Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 9 May 2018 16:51:17 +0100
Subject: Fix printing of hex strings in Lem

---
 src/gen_lib/sail_values.lem | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 2d9eda9c..5c6dc593 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -414,6 +414,7 @@ let rec hexstring_of_bits bs = match bs with
      | (Just n, Just s) -> Just (n :: s)
      | _ -> Nothing
      end
+  | [] -> Just []
   | _ -> Nothing
   end
 declare {isabelle} termination_argument hexstring_of_bits = automatic
-- 
cgit v1.2.3


From db3b6d21c18f4ac516c2554db6890274d2b8292c Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 10 May 2018 14:23:49 +0100
Subject: Remove buggy bit list comparison functions from Lem library

Found bugs by running CHERI test suite on Isabelle-exported model:  signed
less-than for bit lists was missing negations for the two's complement, and
unsigned less-than compared the reverse lists.

Since all other backends implement this in Sail, it seems best to just remove
this code.

Also add support for infix operators to Lem backend, by z-encoding their
identifiers like the other backends do.
---
 src/gen_lib/sail_operators.lem          | 30 ------------------------------
 src/gen_lib/sail_operators_bitlists.lem | 16 ----------------
 src/gen_lib/sail_operators_mwords.lem   | 16 ----------------
 3 files changed, 62 deletions(-)

(limited to 'src/gen_lib')

diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 78aab65e..0c5da675 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -194,36 +194,6 @@ let neq_bv l r = not (eq_bv l r)
 
 let inline neq_mword l r = (l <> r)
 
-val ult_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let ult_bv l r = lexicographicLess (List.reverse (bits_of l)) (List.reverse (bits_of r))
-let ulteq_bv l r = (eq_bv l r) || (ult_bv l r)
-let ugt_bv l r = not (ulteq_bv l r)
-let ugteq_bv l r = (eq_bv l r) || (ugt_bv l r)
-
-val slt_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
-let slt_bv l r =
-  match (most_significant l, most_significant r) with
-    | (B0, B0) -> ult_bv l r
-    | (B0, B1) -> false
-    | (B1, B0) -> true
-    | (B1, B1) ->
-       let l' = add_one_bit_ignore_overflow (bits_of l) in
-       let r' = add_one_bit_ignore_overflow (bits_of r) in
-       ugt_bv l' r'
-    | (BU, BU) -> ult_bv l r
-    | (BU, _) -> true
-    | (_, BU) -> false
-  end
-let slteq_bv l r = (eq_bv l r) || (slt_bv l r)
-let sgt_bv l r = not (slteq_bv l r)
-let sgteq_bv l r = (eq_bv l r) || (sgt_bv l r)
-
-val ucmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool
-let inline ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedIntegerFromWord r)
-
-val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool
-let inline scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r)
-
 val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a
 let get_slice_int_bv len n lo =
   let hi = lo + len - 1 in
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem
index fed293b4..19e9b519 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail_operators_bitlists.lem
@@ -308,21 +308,5 @@ let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
 
 val eq_vec    : list bitU -> list bitU -> bool
 val neq_vec   : list bitU -> list bitU -> bool
-val ult_vec   : list bitU -> list bitU -> bool
-val slt_vec   : list bitU -> list bitU -> bool
-val ugt_vec   : list bitU -> list bitU -> bool
-val sgt_vec   : list bitU -> list bitU -> bool
-val ulteq_vec : list bitU -> list bitU -> bool
-val slteq_vec : list bitU -> list bitU -> bool
-val ugteq_vec : list bitU -> list bitU -> bool
-val sgteq_vec : list bitU -> list bitU -> bool
 let eq_vec    = eq_bv
 let neq_vec   = neq_bv
-let ult_vec   = ult_bv
-let slt_vec   = slt_bv
-let ugt_vec   = ugt_bv
-let sgt_vec   = sgt_bv
-let ulteq_vec = ulteq_bv
-let slteq_vec = slteq_bv
-let ugteq_vec = ugteq_bv
-let sgteq_vec = sgteq_bv
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index 077dfb02..22d5b246 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -329,21 +329,5 @@ let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
 
 val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ult_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val slt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ugt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val sgt_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
-val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 let inline eq_vec    = eq_mword
 let inline neq_vec   = neq_mword
-let inline ult_vec   = ucmp_mword (<)
-let inline slt_vec   = scmp_mword (<)
-let inline ugt_vec   = ucmp_mword (>)
-let inline sgt_vec   = scmp_mword (>)
-let inline ulteq_vec = ucmp_mword (<=)
-let inline slteq_vec = scmp_mword (<=)
-let inline ugteq_vec = ucmp_mword (>=)
-let inline sgteq_vec = scmp_mword (>=)
-- 
cgit v1.2.3