Need to separate out the 0.10 lem library from upcoming 0.11

Unlike the prompt-monad change I don't see a way to do this easily
purely on the model side

Make sure a64_barrier_type and domain aren't visible for RISC-V
isabelle build

1 files changed, 207 insertions, 0 deletions

diff --git a/src/gen_lib/0.11/sail2_operators.lem b/src/gen_lib/0.11/sail2_operators.lem
new file mode 100644
index 00000000..43a9812e
--- /dev/null
+++ b/src/gen_lib/0.11/sail2_operators.lem
@@ -0,0 +1,207 @@
+open import Pervasives_extra
+open import Machine_word
+open import Sail2_values
+
+(*** Bit vector operations *)
+
+val concat_bv : forall 'a 'b. Bitvector 'a, Bitvector 'b => 'a -> 'b -> list bitU
+let concat_bv l r = (bits_of l ++ bits_of r)
+
+val cons_bv : forall 'a. Bitvector 'a => bitU -> 'a -> list bitU
+let cons_bv b v = b :: bits_of v
+
+val cast_unit_bv : bitU -> list bitU
+let cast_unit_bv b = [b]
+
+val bv_of_bit : integer -> bitU -> list bitU
+let bv_of_bit len b = extz_bits len [b]
+
+let most_significant v = match bits_of v with
+  | b :: _ -> b
+  | _ -> B0 (* Treat empty bitvector as all zeros *)
+  end
+
+let get_max_representable_in sign (n : integer) : integer =
+  if (n = 64) then match sign with | true -> max_64 | false -> max_64u end
+  else if (n=32) then match sign with | true -> max_32 | false -> max_32u end
+  else if (n=8) then max_8
+  else if (n=5) then max_5
+  else match sign with | true -> integerPow 2 ((natFromInteger n) -1)
+                       | false -> integerPow 2 (natFromInteger n)
+       end
+
+let get_min_representable_in _ (n : integer) : integer =
+  if n = 64 then min_64
+  else if n = 32 then min_32
+  else if n = 8 then min_8
+  else if n = 5 then min_5
+  else 0 - (integerPow 2 (natFromInteger n))
+
+val arith_op_bv_int : forall 'a 'b. Bitvector 'a =>
+  (integer -> integer -> integer) -> bool -> 'a -> integer -> 'a
+let arith_op_bv_int op sign l r =
+  let r' = of_int (length l) r in
+  arith_op_bv op sign l r'
+
+val arith_op_int_bv : forall 'a 'b. Bitvector 'a =>
+  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a
+let arith_op_int_bv op sign l r =
+  let l' = of_int (length r) l in
+  arith_op_bv op sign l' r
+
+let arith_op_bv_bool op sign l r = arith_op_bv_int op sign l (if r then 1 else 0)
+let arith_op_bv_bit op sign l r = Maybe.map (arith_op_bv_bool op sign l) (bool_of_bitU r)
+
+(* TODO (or just omit and define it per spec if needed)
+val arith_op_overflow_bv : forall 'a. Bitvector 'a =>
+  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> (list bitU * bitU * bitU)
+let arith_op_overflow_bv op sign size l r =
+  let len = length l in
+  let act_size = len * size in
+  match (int_of_bv sign l, int_of_bv sign r, int_of_bv false l, int_of_bv false r) with
+    | (Just l_sign, Just r_sign, Just l_unsign, Just r_unsign) ->
+       let n = op l_sign r_sign in
+       let n_unsign = op l_unsign r_unsign in
+       let correct_size = of_int act_size n in
+       let one_more_size_u = bits_of_int (act_size + 1) n_unsign in
+       let overflow =
+         if n <= get_max_representable_in sign len &&
+              n >= get_min_representable_in sign len
+         then B0 else B1 in
+       let c_out = most_significant one_more_size_u in
+       (correct_size,overflow,c_out)
+    | (_, _, _, _) ->
+       (repeat [BU] act_size, BU, BU)
+  end
+
+let add_overflow_bv = arith_op_overflow_bv integerAdd false 1
+let adds_overflow_bv = arith_op_overflow_bv integerAdd true 1
+let sub_overflow_bv = arith_op_overflow_bv integerMinus false 1
+let subs_overflow_bv = arith_op_overflow_bv integerMinus true 1
+let mult_overflow_bv = arith_op_overflow_bv integerMult false 2
+let mults_overflow_bv = arith_op_overflow_bv integerMult true 2
+
+val arith_op_overflow_bv_bit : forall 'a. Bitvector 'a =>
+  (integer -> integer -> integer) -> bool -> integer -> 'a -> bitU -> (list bitU * bitU * bitU)
+let arith_op_overflow_bv_bit op sign size l r_bit =
+  let act_size = length l * size in
+  match (int_of_bv sign l, int_of_bv false l, r_bit = BU) with
+    | (Just l', Just l_u, false) ->
+       let (n, nu, changed) = match r_bit with
+         | B1 -> (op l' 1, op l_u 1, true)
+         | B0 -> (l', l_u, false)
+         | BU -> (* unreachable due to check above *)
+            failwith "arith_op_overflow_bv_bit applied to undefined bit"
+         end in
+       let correct_size = of_int act_size n in
+       let one_larger = bits_of_int (act_size + 1) nu in
+       let overflow =
+         if changed
+         then
+           if n <= get_max_representable_in sign act_size && n >= get_min_representable_in sign act_size
+           then B0 else B1
+         else B0 in
+       (correct_size, overflow, most_significant one_larger)
+    | (_, _, _) ->
+       (repeat [BU] act_size, BU, BU)
+  end
+
+let add_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd false 1
+let adds_overflow_bv_bit = arith_op_overflow_bv_bit integerAdd true 1
+let sub_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus false 1
+let subs_overflow_bv_bit = arith_op_overflow_bv_bit integerMinus true 1*)
+
+type shift = LL_shift | RR_shift | RR_shift_arith | LL_rot | RR_rot
+
+let invert_shift = function
+  | LL_shift -> RR_shift
+  | RR_shift -> LL_shift
+  | RR_shift_arith -> LL_shift
+  | LL_rot -> RR_rot
+  | RR_rot -> LL_rot
+end
+
+val shift_op_bv : forall 'a. Bitvector 'a => shift -> 'a -> integer -> list bitU
+let shift_op_bv op v n =
+  let v = bits_of v in
+  if n = 0 then v else
+  let (op, n) = if n > 0 then (op, n) else (invert_shift op, ~n) in
+  match op with
+  | LL_shift ->
+     subrange_list true v n (length v - 1) ++ repeat [B0] n
+  | RR_shift ->
+     repeat [B0] n ++ subrange_list true v 0 (length v - n - 1)
+  | RR_shift_arith ->
+     repeat [most_significant v] n ++ subrange_list true v 0 (length v - n - 1)
+  | LL_rot ->
+     subrange_list true v n (length v - 1) ++ subrange_list true v 0 (n - 1)
+  | RR_rot ->
+     subrange_list false v 0 (n - 1) ++ subrange_list false v n (length v - 1)
+  end
+
+let shiftl_bv = shift_op_bv LL_shift (*"<<"*)
+let shiftr_bv = shift_op_bv RR_shift (*">>"*)
+let arith_shiftr_bv = shift_op_bv RR_shift_arith
+let rotl_bv = shift_op_bv LL_rot (*"<<<"*)
+let rotr_bv = shift_op_bv LL_rot (*">>>"*)
+
+let shiftl_mword w n = Machine_word.shiftLeft w (nat_of_int n)
+let shiftr_mword w n = Machine_word.shiftRight w (nat_of_int n)
+let arith_shiftr_mword w n = Machine_word.arithShiftRight w (nat_of_int n)
+let rotl_mword w n = Machine_word.rotateLeft (nat_of_int n) w
+let rotr_mword w n = Machine_word.rotateRight (nat_of_int n) w
+
+let rec arith_op_no0 (op : integer -> integer -> integer) l r =
+  if r = 0
+  then Nothing
+  else Just (op l r)
+
+val arith_op_bv_no0 : forall 'a 'b. Bitvector 'a, Bitvector 'b =>
+  (integer -> integer -> integer) -> bool -> integer -> 'a -> 'a -> maybe 'b
+let arith_op_bv_no0 op sign size l r =
+  Maybe.bind (int_of_bv sign l) (fun l' ->
+  Maybe.bind (int_of_bv sign r) (fun r' ->
+  if r' = 0 then Nothing else Just (of_int (length l * size) (op l' r'))))
+
+let mod_bv = arith_op_bv_no0 tmod_int false 1
+let quot_bv = arith_op_bv_no0 tdiv_int false 1
+let quots_bv = arith_op_bv_no0 tdiv_int true 1
+
+let mod_mword = Machine_word.modulo
+let quot_mword = Machine_word.unsignedDivide
+let quots_mword = Machine_word.signedDivide
+
+let arith_op_bv_int_no0 op sign size l r =
+  arith_op_bv_no0 op sign size l (of_int (length l) r)
+
+let quot_bv_int = arith_op_bv_int_no0 tdiv_int false 1
+let mod_bv_int = arith_op_bv_int_no0 tmod_int false 1
+
+let mod_mword_int l r = Machine_word.modulo l (wordFromInteger r)
+let quot_mword_int l r = Machine_word.unsignedDivide l (wordFromInteger r)
+let quots_mword_int l r = Machine_word.signedDivide l (wordFromInteger r)
+
+let replicate_bits_bv v count = repeat (bits_of v) count
+let duplicate_bit_bv bit len = replicate_bits_bv [bit] len
+
+val eq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
+let eq_bv l r = (bits_of l = bits_of r)
+
+let inline eq_mword l r = (l = r)
+
+val neq_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool
+let neq_bv l r = not (eq_bv l r)
+
+let inline neq_mword l r = (l <> 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)))