diff options
Diffstat (limited to 'snapshots/isabelle/riscv/Riscv_extras.thy')
| -rw-r--r-- | snapshots/isabelle/riscv/Riscv_extras.thy | 126 |
1 files changed, 126 insertions, 0 deletions
diff --git a/snapshots/isabelle/riscv/Riscv_extras.thy b/snapshots/isabelle/riscv/Riscv_extras.thy new file mode 100644 index 00000000..fc83385b --- /dev/null +++ b/snapshots/isabelle/riscv/Riscv_extras.thy @@ -0,0 +1,126 @@ +chapter \<open>Generated by Lem from riscv_extras.lem.\<close> + +theory "Riscv_extras" + +imports + Main + "Lem_pervasives" + "Lem_pervasives_extra" + "Sail_instr_kinds" + "Sail_values" + "Sail_operators_mwords" + "Prompt_monad" + "Prompt" + +begin + +(*open import Pervasives*) +(*open import Pervasives_extra*) +(*open import Sail_instr_kinds*) +(*open import Sail_values*) +(*open import Sail_operators_mwords*) +(*open import Prompt_monad*) +(*open import Prompt*) + +type_synonym 'a bitvector =" ( 'a::len)Word.word " + +definition MEM_fence_rw_rw :: " unit \<Rightarrow>('b,(unit),'a)monad " where + " MEM_fence_rw_rw _ = ( barrier Barrier_RISCV_rw_rw )" + +definition MEM_fence_r_rw :: " unit \<Rightarrow>('b,(unit),'a)monad " where + " MEM_fence_r_rw _ = ( barrier Barrier_RISCV_r_rw )" + +definition MEM_fence_r_r :: " unit \<Rightarrow>('b,(unit),'a)monad " where + " MEM_fence_r_r _ = ( barrier Barrier_RISCV_r_r )" + +definition MEM_fence_rw_w :: " unit \<Rightarrow>('b,(unit),'a)monad " where + " MEM_fence_rw_w _ = ( barrier Barrier_RISCV_rw_w )" + +definition MEM_fence_w_w :: " unit \<Rightarrow>('b,(unit),'a)monad " where + " MEM_fence_w_w _ = ( barrier Barrier_RISCV_w_w )" + +definition MEM_fence_i :: " unit \<Rightarrow>('b,(unit),'a)monad " where + " MEM_fence_i _ = ( barrier Barrier_RISCV_i )" + + +(*val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e*) +(*val MEMea_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e*) +(*val MEMea_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e*) +(*val MEMea_conditional : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e*) +(*val MEMea_conditional_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e*) +(*val MEMea_conditional_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e*) + +definition MEMea :: "('a::len)Word.word \<Rightarrow> int \<Rightarrow>('rv,(unit),'e)monad " where + " MEMea addr size1 = ( write_mem_ea + instance_Sail_values_Bitvector_Machine_word_mword_dict Write_plain addr size1 )" + +definition MEMea_release :: "('a::len)Word.word \<Rightarrow> int \<Rightarrow>('rv,(unit),'e)monad " where + " MEMea_release addr size1 = ( write_mem_ea + instance_Sail_values_Bitvector_Machine_word_mword_dict Write_RISCV_release addr size1 )" + +definition MEMea_strong_release :: "('a::len)Word.word \<Rightarrow> int \<Rightarrow>('rv,(unit),'e)monad " where + " MEMea_strong_release addr size1 = ( write_mem_ea + instance_Sail_values_Bitvector_Machine_word_mword_dict Write_RISCV_strong_release addr size1 )" + +definition MEMea_conditional :: "('a::len)Word.word \<Rightarrow> int \<Rightarrow>('rv,(unit),'e)monad " where + " MEMea_conditional addr size1 = ( write_mem_ea + instance_Sail_values_Bitvector_Machine_word_mword_dict Write_RISCV_conditional addr size1 )" + +definition MEMea_conditional_release :: "('a::len)Word.word \<Rightarrow> int \<Rightarrow>('rv,(unit),'e)monad " where + " MEMea_conditional_release addr size1 = ( write_mem_ea + instance_Sail_values_Bitvector_Machine_word_mword_dict Write_RISCV_conditional_release addr size1 )" + +definition MEMea_conditional_strong_release :: "('a::len)Word.word \<Rightarrow> int \<Rightarrow>('rv,(unit),'e)monad " + where + " MEMea_conditional_strong_release addr size1 + = ( write_mem_ea + instance_Sail_values_Bitvector_Machine_word_mword_dict Write_RISCV_conditional_strong_release addr size1 )" + + +(*val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => + integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv unit 'e*) +definition write_ram :: " int \<Rightarrow> int \<Rightarrow>('a::len)Word.word \<Rightarrow>('a::len)Word.word \<Rightarrow>('b::len)Word.word \<Rightarrow>('rv,(unit),'e)monad " where + " write_ram addrsize size1 hexRAM address value1 = ( + (write_mem_ea instance_Sail_values_Bitvector_Machine_word_mword_dict Write_plain address size1 \<then> + write_mem_val instance_Sail_values_Bitvector_Machine_word_mword_dict value1) \<bind> (\<lambda>x . (case x of _ => return () )) )" + + +(*val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b => + integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e*) +definition read_ram :: " int \<Rightarrow> int \<Rightarrow>('a::len)Word.word \<Rightarrow>('a::len)Word.word \<Rightarrow>('rv,(('b::len)Word.word),'e)monad " where + " read_ram addrsize size1 hexRAM address = ( + read_mem instance_Sail_values_Bitvector_Machine_word_mword_dict instance_Sail_values_Bitvector_Machine_word_mword_dict Read_plain address size1 )" + + +definition speculate_conditional_success :: " unit \<Rightarrow>('b,(bool),'a)monad " where + " speculate_conditional_success _ = ( excl_result () )" + + +(*val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> bitvector 'a*) +definition get_slice_int0 :: " int \<Rightarrow> int \<Rightarrow> int \<Rightarrow>('a::len)Word.word " where + " get_slice_int0 len n lo = ( + (* TODO: Is this the intended behaviour? *) + (let hi = ((lo + len) -( 1 :: int)) in + (let bits = (bits_of_int (hi +( 1 :: int)) n) in + of_bits_failwith instance_Sail_values_Bitvector_Machine_word_mword_dict (subrange_list False bits hi lo))))" + + +(*val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a*) +definition shift_bits_right :: "('a::len)Word.word \<Rightarrow>('b::len)Word.word \<Rightarrow>('a::len)Word.word " where + " shift_bits_right v m = ( shiftr v (Word.uint m))" + +(*val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a*) +definition shift_bits_left :: "('a::len)Word.word \<Rightarrow>('b::len)Word.word \<Rightarrow>('a::len)Word.word " where + " shift_bits_left v m = ( shiftl v (Word.uint m))" + + +(*val print_string : string -> string -> unit*) +definition print_string :: " string \<Rightarrow> string \<Rightarrow> unit " where + " print_string msg s = ( prerr_endline (msg @ s))" + + +(*val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit*) +definition print_bits :: " string \<Rightarrow>('a::len)Word.word \<Rightarrow> unit " where + " print_bits msg bs = ( prerr_endline (msg @ (show_bitlist (List.map bitU_of_bool (Word.to_bl bs)))))" + +end |