Merge branch 'sail2' into cheri-mono

In order to use up-to-date sequential CHERI model for test suite

6 files changed, 65 insertions, 61 deletions

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
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index d4275c87..0c5da675 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -194,32 +194,14 @@ 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
+  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..19e9b519 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,23 +292,21 @@ 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
-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 8bcc0319..22d5b246 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,23 +313,21 @@ 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
-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 (>=)
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
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index 781bc129..89021890 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
+  ()