summaryrefslogtreecommitdiff
path: root/snapshots/isabelle/cheri/Mips_extras.thy
diff options
context:
space:
mode:
Diffstat (limited to 'snapshots/isabelle/cheri/Mips_extras.thy')
-rw-r--r--snapshots/isabelle/cheri/Mips_extras.thy251
1 files changed, 251 insertions, 0 deletions
diff --git a/snapshots/isabelle/cheri/Mips_extras.thy b/snapshots/isabelle/cheri/Mips_extras.thy
new file mode 100644
index 00000000..c0379d3a
--- /dev/null
+++ b/snapshots/isabelle/cheri/Mips_extras.thy
@@ -0,0 +1,251 @@
+chapter \<open>Generated by Lem from /auto/homes/tb592/REMS/rems/sail/mips/mips_extras.lem.\<close>
+
+theory "Mips_extras"
+
+imports
+ Main
+ "Lem_pervasives"
+ "Lem_pervasives_extra"
+ "Sail_instr_kinds"
+ "Sail_values"
+ "Prompt_monad"
+ "Prompt"
+ "Sail_operators"
+
+begin
+
+(*open import Pervasives*)
+(*open import Pervasives_extra*)
+(*open import Sail_instr_kinds*)
+(*open import Sail_values*)
+(*open import Sail_operators*)
+(*open import Prompt_monad*)
+(*open import Prompt*)
+
+(*val MEMr : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e*)
+(*val MEMr_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e*)
+(*val MEMr_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e*)
+(*val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e*)
+
+definition MEMr :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,'b,'e)monad " where
+ " MEMr dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b addr size1 = ( read_mem
+ dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b Read_plain addr size1 )"
+
+definition MEMr_reserve :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,'b,'e)monad " where
+ " MEMr_reserve dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b addr size1 = ( read_mem
+ dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b Read_reserve addr size1 )"
+
+
+(*val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monad 'regval bool 'e*)
+definition read_tag_bool :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow>('regval,(bool),'e)monad " where
+ " read_tag_bool dict_Sail_values_Bitvector_a addr = (
+ read_tag dict_Sail_values_Bitvector_a addr \<bind> (\<lambda> t .
+ maybe_fail (''read_tag_bool'') (bool_of_bitU t)))"
+
+
+(*val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monad 'regval unit 'e*)
+definition write_tag_bool :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow>('regval,(unit),'e)monad " where
+ " write_tag_bool dict_Sail_values_Bitvector_a addr t = ( write_tag
+ dict_Sail_values_Bitvector_a addr (bitU_of_bool t) \<bind>
+ (\<lambda>x . (case x of _ => return () )) )"
+
+
+definition MEMr_tag :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(bool*'b),'e)monad " where
+ " MEMr_tag dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b addr size1 = (
+ read_mem dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b Read_plain addr size1 \<bind> (\<lambda> v .
+ read_tag_bool dict_Sail_values_Bitvector_a addr \<bind> (\<lambda> t .
+ return (t, v))))"
+
+
+definition MEMr_tag_reserve :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(bool*'b),'e)monad " where
+ " MEMr_tag_reserve dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b addr size1 = (
+ read_mem dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b Read_plain addr size1 \<bind> (\<lambda> v .
+ read_tag_bool dict_Sail_values_Bitvector_a addr \<bind> (\<lambda> t .
+ return (t, v))))"
+
+
+
+(*val MEMea : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e*)
+(*val MEMea_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e*)
+(*val MEMea_tag : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e*)
+(*val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e*)
+
+definition MEMea :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(unit),'e)monad " where
+ " MEMea dict_Sail_values_Bitvector_a addr size1 = ( write_mem_ea
+ dict_Sail_values_Bitvector_a Write_plain addr size1 )"
+
+definition MEMea_conditional :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(unit),'e)monad " where
+ " MEMea_conditional dict_Sail_values_Bitvector_a addr size1 = ( write_mem_ea
+ dict_Sail_values_Bitvector_a Write_conditional addr size1 )"
+
+
+definition MEMea_tag :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(unit),'e)monad " where
+ " MEMea_tag dict_Sail_values_Bitvector_a addr size1 = ( write_mem_ea
+ dict_Sail_values_Bitvector_a Write_plain addr size1 )"
+
+definition MEMea_tag_conditional :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(unit),'e)monad " where
+ " MEMea_tag_conditional dict_Sail_values_Bitvector_a addr size1 = ( write_mem_ea
+ dict_Sail_values_Bitvector_a Write_conditional addr size1 )"
+
+
+
+(*val MEMval : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval unit 'e*)
+(*val MEMval_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval bool 'e*)
+(*val MEMval_tag : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval unit 'e*)
+(*val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval bool 'e*)
+
+definition MEMval :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'b \<Rightarrow>('regval,(unit),'e)monad " where
+ " MEMval dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b _ size1 v = ( write_mem_val
+ dict_Sail_values_Bitvector_b v \<bind> (\<lambda>x . (case x of _ => return () )) )"
+
+definition MEMval_conditional :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'b \<Rightarrow>('regval,(bool),'e)monad " where
+ " MEMval_conditional dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b _ size1 v = ( write_mem_val
+ dict_Sail_values_Bitvector_b v \<bind> (\<lambda> b . return (if b then True else False)))"
+
+definition MEMval_tag :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> bool \<Rightarrow> 'b \<Rightarrow>('regval,(unit),'e)monad " where
+ " MEMval_tag dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b addr size1 t v = ( write_mem_val
+ dict_Sail_values_Bitvector_b v \<bind> (\<lambda>x . (case x of
+ _ => write_tag_bool dict_Sail_values_Bitvector_a addr t
+ \<bind>
+ (\<lambda>x . (case x of _ => return () ))
+ )) )"
+
+definition MEMval_tag_conditional :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> bool \<Rightarrow> 'b \<Rightarrow>('regval,(bool),'e)monad " where
+ " MEMval_tag_conditional dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b addr size1 t v = ( write_mem_val
+ dict_Sail_values_Bitvector_b v \<bind> (\<lambda> b . write_tag_bool
+ dict_Sail_values_Bitvector_a addr t \<bind> (\<lambda>x . (case x of _ => return (if b then True else False) ))))"
+
+
+(*val MEM_sync : forall 'regval 'e. unit -> monad 'regval unit 'e*)
+
+definition MEM_sync :: " unit \<Rightarrow>('regval,(unit),'e)monad " where
+ " MEM_sync _ = ( barrier Barrier_MIPS_SYNC )"
+
+
+(* Some wrappers copied from aarch64_extras *)
+(* TODO: Harmonise into a common library *)
+
+definition get_slice_int_bl :: " int \<Rightarrow> int \<Rightarrow> int \<Rightarrow>(bool)list " where
+ " get_slice_int_bl len n lo = (
+ (* TODO: Is this the intended behaviour? *)
+ (let hi = ((lo + len) -( 1 :: int)) in
+ (let bs = (bools_of_int (hi +( 1 :: int)) n) in
+ subrange_list False bs hi lo)))"
+
+
+(*val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a*)
+definition get_slice_int0 :: " 'a Bitvector_class \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a " where
+ " get_slice_int0 dict_Sail_values_Bitvector_a len n lo = (
+ (of_bools_method dict_Sail_values_Bitvector_a) (get_slice_int_bl len n lo))"
+
+
+definition write_ram :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'e \<Rightarrow> int \<Rightarrow> 'f \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>('d,(unit),'c)monad " where
+ " write_ram dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b _ size1 _ addr data = (
+ MEMea dict_Sail_values_Bitvector_b addr size1 \<then>
+ MEMval dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_a addr size1 data )"
+
+
+definition read_ram :: " 'a Bitvector_class \<Rightarrow> 'c Bitvector_class \<Rightarrow> 'e \<Rightarrow> int \<Rightarrow> 'f \<Rightarrow> 'a \<Rightarrow>('d,'c,'b)monad " where
+ " read_ram dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_c _ size1 _ addr = ( MEMr
+ dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_c addr size1 )"
+
+
+definition string_of_bits :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> string " where
+ " string_of_bits dict_Sail_values_Bitvector_a bs = ( string_of_bv
+ (instance_Sail_values_Bitvector_list_dict
+ instance_Sail_values_BitU_Sail_values_bitU_dict) ((bits_of_method dict_Sail_values_Bitvector_a) bs))"
+
+definition string_of_int :: " 'a Show_class \<Rightarrow> 'a \<Rightarrow> string " where
+ " string_of_int dict_Show_Show_a = ((show_method dict_Show_Show_a))"
+
+
+definition sign_extend0 :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'b " where
+ " sign_extend0 dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b bits len = ( maybe_failwith (
+ (of_bits_method dict_Sail_values_Bitvector_b) (exts_bv dict_Sail_values_Bitvector_a len bits)))"
+
+definition zero_extend0 :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'b " where
+ " zero_extend0 dict_Sail_values_Bitvector_a dict_Sail_values_Bitvector_b bits len = ( maybe_failwith (
+ (of_bits_method dict_Sail_values_Bitvector_b) (extz_bv dict_Sail_values_Bitvector_a len bits)))"
+
+
+definition shift_bits_left :: " 'b Bitvector_class \<Rightarrow> 'd Bitvector_class \<Rightarrow> 'e Bitvector_class \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow>('c,'b,'a)monad " where
+ " shift_bits_left dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_d dict_Sail_values_Bitvector_e v n = (
+ (let r = (Option.bind (
+ (unsigned_method dict_Sail_values_Bitvector_e) n) (\<lambda> n . (of_bits_method dict_Sail_values_Bitvector_b) (shiftl_bv dict_Sail_values_Bitvector_d v n))) in
+ maybe_fail (''shift_bits_left'') r))"
+
+definition shift_bits_right :: " 'b Bitvector_class \<Rightarrow> 'd Bitvector_class \<Rightarrow> 'e Bitvector_class \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow>('c,'b,'a)monad " where
+ " shift_bits_right dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_d dict_Sail_values_Bitvector_e v n = (
+ (let r = (Option.bind (
+ (unsigned_method dict_Sail_values_Bitvector_e) n) (\<lambda> n . (of_bits_method dict_Sail_values_Bitvector_b) (shiftr_bv dict_Sail_values_Bitvector_d v n))) in
+ maybe_fail (''shift_bits_right'') r))"
+
+definition shift_bits_right_arith :: " 'b Bitvector_class \<Rightarrow> 'd Bitvector_class \<Rightarrow> 'e Bitvector_class \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow>('c,'b,'a)monad " where
+ " shift_bits_right_arith dict_Sail_values_Bitvector_b dict_Sail_values_Bitvector_d dict_Sail_values_Bitvector_e v n = (
+ (let r = (Option.bind (
+ (unsigned_method dict_Sail_values_Bitvector_e) n) (\<lambda> n . (of_bits_method dict_Sail_values_Bitvector_b) (arith_shiftr_bv dict_Sail_values_Bitvector_d v n))) in
+ maybe_fail (''shift_bits_right_arith'') r))"
+
+
+(* Use constants for undefined values for now *)
+definition internal_pick :: " 'a list \<Rightarrow>('c,'a,'b)monad " where
+ " internal_pick vs = ( return (List.hd vs))"
+
+definition undefined_string :: " unit \<Rightarrow>('b,(string),'a)monad " where
+ " undefined_string _ = ( return (''''))"
+
+definition undefined_unit :: " unit \<Rightarrow>('b,(unit),'a)monad " where
+ " undefined_unit _ = ( return () )"
+
+definition undefined_int :: " unit \<Rightarrow>('b,(int),'a)monad " where
+ " undefined_int _ = ( return (( 0 :: int)::ii))"
+
+(*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*)
+definition undefined_vector :: " int \<Rightarrow> 'a \<Rightarrow>('rv,('a list),'e)monad " where
+ " undefined_vector len u = ( return (repeat [u] len))"
+
+(*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
+definition undefined_bitvector :: " 'a Bitvector_class \<Rightarrow> int \<Rightarrow>('rv,'a,'e)monad " where
+ " undefined_bitvector dict_Sail_values_Bitvector_a len = ( return (
+ (of_bools_method dict_Sail_values_Bitvector_a) (repeat [False] len)))"
+
+(*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
+definition undefined_bits :: " 'a Bitvector_class \<Rightarrow> int \<Rightarrow>('rv,'a,'e)monad " where
+ " undefined_bits dict_Sail_values_Bitvector_a = (
+ undefined_bitvector dict_Sail_values_Bitvector_a )"
+
+definition undefined_bit :: " unit \<Rightarrow>('b,(bitU),'a)monad " where
+ " undefined_bit _ = ( return B0 )"
+
+definition undefined_real :: " unit \<Rightarrow>('b,(real),'a)monad " where
+ " undefined_real _ = ( return (realFromFrac(( 0 :: int))(( 1 :: int))))"
+
+definition undefined_range :: " 'a \<Rightarrow> 'd \<Rightarrow>('c,'a,'b)monad " where
+ " undefined_range i j = ( return i )"
+
+definition undefined_atom :: " 'a \<Rightarrow>('c,'a,'b)monad " where
+ " undefined_atom i = ( return i )"
+
+definition undefined_nat :: " unit \<Rightarrow>('b,(int),'a)monad " where
+ " undefined_nat _ = ( return (( 0 :: int)::ii))"
+
+
+definition skip :: " unit \<Rightarrow>('b,(unit),'a)monad " where
+ " skip _ = ( return () )"
+
+
+(*val elf_entry : unit -> integer*)
+definition elf_entry :: " unit \<Rightarrow> int " where
+ " elf_entry _ = (( 0 :: int))"
+
+
+definition print_bits :: " 'a Bitvector_class \<Rightarrow> string \<Rightarrow> 'a \<Rightarrow> unit " where
+ " print_bits dict_Sail_values_Bitvector_a msg bs = ( prerr_endline (msg @ (string_of_bits
+ dict_Sail_values_Bitvector_a bs)))"
+
+
+(*val get_time_ns : unit -> integer*)
+definition get_time_ns :: " unit \<Rightarrow> int " where
+ " get_time_ns _ = (( 0 :: int))"
+
+end
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 02:10:18 +0000