-
Notifications
You must be signed in to change notification settings - Fork 122
/
Copy pathRiscv_extras.thy
239 lines (164 loc) · 13 KB
/
Riscv_extras.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
chapter \<open>Generated by Lem from \<open>riscv_extras.lem\<close>.\<close>
theory "Riscv_extras"
imports
Main
"LEM.Lem_pervasives"
"LEM.Lem_pervasives_extra"
"Sail.Sail2_instr_kinds"
"Sail.Sail2_values"
"Sail.Sail2_operators_mwords"
"Sail.Sail2_prompt_monad"
"Sail.Sail2_prompt"
begin
(*open import Pervasives*)
(*open import Pervasives_extra*)
(*open import Sail2_instr_kinds*)
(*open import Sail2_values*)
(*open import Sail2_operators_mwords*)
(*open import Sail2_prompt_monad*)
(*open import Sail2_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_w_rw :: " unit \<Rightarrow>('b,(unit),'a)monad " where
" MEM_fence_w_rw _ = ( barrier Barrier_RISCV_w_rw )"
definition MEM_fence_rw_r :: " unit \<Rightarrow>('b,(unit),'a)monad " where
" MEM_fence_rw_r _ = ( barrier Barrier_RISCV_rw_r )"
definition MEM_fence_r_w :: " unit \<Rightarrow>('b,(unit),'a)monad " where
" MEM_fence_r_w _ = ( barrier Barrier_RISCV_r_w )"
definition MEM_fence_w_r :: " unit \<Rightarrow>('b,(unit),'a)monad " where
" MEM_fence_w_r _ = ( barrier Barrier_RISCV_w_r )"
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_Sail2_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_Sail2_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_Sail2_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_Sail2_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_Sail2_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_Sail2_values_Bitvector_Machine_word_mword_dict Write_RISCV_conditional_strong_release addr size1 )"
(*val MEMr : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e*)
(*val MEMr_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e*)
(*val MEMr_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e*)
(*val MEMr_reserved : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e*)
(*val MEMr_reserved_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e*)
(*val MEMr_reserved_strong_acquire : forall 'rv 'a 'b 'e. Size 'a, Size 'b => integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e*)
definition MEMr :: " int \<Rightarrow> int \<Rightarrow>('a::len)Word.word \<Rightarrow>('a::len)Word.word \<Rightarrow>('rv,(('b::len)Word.word),'e)monad " where
" MEMr addrsize size1 hexRAM addr = ( read_mem
instance_Sail2_values_Bitvector_Machine_word_mword_dict instance_Sail2_values_Bitvector_Machine_word_mword_dict Read_plain addr size1 )"
definition MEMr_acquire :: " int \<Rightarrow> int \<Rightarrow>('a::len)Word.word \<Rightarrow>('a::len)Word.word \<Rightarrow>('rv,(('b::len)Word.word),'e)monad " where
" MEMr_acquire addrsize size1 hexRAM addr = ( read_mem
instance_Sail2_values_Bitvector_Machine_word_mword_dict instance_Sail2_values_Bitvector_Machine_word_mword_dict Read_RISCV_acquire addr size1 )"
definition MEMr_strong_acquire :: " int \<Rightarrow> int \<Rightarrow>('a::len)Word.word \<Rightarrow>('a::len)Word.word \<Rightarrow>('rv,(('b::len)Word.word),'e)monad " where
" MEMr_strong_acquire addrsize size1 hexRAM addr = ( read_mem
instance_Sail2_values_Bitvector_Machine_word_mword_dict instance_Sail2_values_Bitvector_Machine_word_mword_dict Read_RISCV_strong_acquire addr size1 )"
definition MEMr_reserved :: " int \<Rightarrow> int \<Rightarrow>('a::len)Word.word \<Rightarrow>('a::len)Word.word \<Rightarrow>('rv,(('b::len)Word.word),'e)monad " where
" MEMr_reserved addrsize size1 hexRAM addr = ( read_mem
instance_Sail2_values_Bitvector_Machine_word_mword_dict instance_Sail2_values_Bitvector_Machine_word_mword_dict Read_RISCV_reserved addr size1 )"
definition MEMr_reserved_acquire :: " int \<Rightarrow> int \<Rightarrow>('a::len)Word.word \<Rightarrow>('a::len)Word.word \<Rightarrow>('rv,(('b::len)Word.word),'e)monad " where
" MEMr_reserved_acquire addrsize size1 hexRAM addr = ( read_mem
instance_Sail2_values_Bitvector_Machine_word_mword_dict instance_Sail2_values_Bitvector_Machine_word_mword_dict Read_RISCV_reserved_acquire addr size1 )"
definition MEMr_reserved_strong_acquire :: " int \<Rightarrow> int \<Rightarrow>('a::len)Word.word \<Rightarrow>('a::len)Word.word \<Rightarrow>('rv,(('b::len)Word.word),'e)monad " where
" MEMr_reserved_strong_acquire addrsize size1 hexRAM addr = ( read_mem
instance_Sail2_values_Bitvector_Machine_word_mword_dict instance_Sail2_values_Bitvector_Machine_word_mword_dict Read_RISCV_reserved_strong_acquire addr size1 )"
(*val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv bool 'e*)
definition write_ram :: " int \<Rightarrow> int \<Rightarrow>('a::len)Word.word \<Rightarrow>('a::len)Word.word \<Rightarrow>('b::len)Word.word \<Rightarrow>('rv,(bool),'e)monad " where
" write_ram addrsize size1 hexRAM address value1 = (
write_mem_val instance_Sail2_values_Bitvector_Machine_word_mword_dict value1 )"
(*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_Sail2_values_Bitvector_Machine_word_mword_dict instance_Sail2_values_Bitvector_Machine_word_mword_dict Read_plain address size1 )"
(*val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit*)
definition load_reservation :: "('a::len)Word.word \<Rightarrow> unit " where
" load_reservation addr = ( () )"
definition speculate_conditional_success :: " 'c \<Rightarrow>('b,(bool),'a)monad " where
" speculate_conditional_success _ = ( excl_result () )"
definition cancel_reservation :: " unit \<Rightarrow> unit " where
" cancel_reservation _ = ( () )"
(*val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a*)
definition plat_ram_base :: " unit \<Rightarrow>('a::len)Word.word " where
" plat_ram_base _ = ( Word.word_of_int(( 0 :: int)))"
(*val plat_ram_size : forall 'a. Size 'a => unit -> bitvector 'a*)
definition plat_ram_size :: " unit \<Rightarrow>('a::len)Word.word " where
" plat_ram_size _ = ( Word.word_of_int(( 0 :: int)))"
(*val plat_rom_base : forall 'a. Size 'a => unit -> bitvector 'a*)
definition plat_rom_base :: " unit \<Rightarrow>('a::len)Word.word " where
" plat_rom_base _ = ( Word.word_of_int(( 0 :: int)))"
(*val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a*)
definition plat_rom_size :: " unit \<Rightarrow>('a::len)Word.word " where
" plat_rom_size _ = ( Word.word_of_int(( 0 :: int)))"
(*val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a*)
definition plat_clint_base :: " unit \<Rightarrow>('a::len)Word.word " where
" plat_clint_base _ = ( Word.word_of_int(( 0 :: int)))"
(*val plat_clint_size : forall 'a. Size 'a => unit -> bitvector 'a*)
definition plat_clint_size :: " unit \<Rightarrow>('a::len)Word.word " where
" plat_clint_size _ = ( Word.word_of_int(( 0 :: int)))"
(*val plat_enable_dirty_update : unit -> bool*)
definition plat_enable_dirty_update :: " unit \<Rightarrow> bool " where
" plat_enable_dirty_update _ = ( False )"
(*val plat_enable_misaligned_access : unit -> bool*)
definition plat_enable_misaligned_access :: " unit \<Rightarrow> bool " where
" plat_enable_misaligned_access _ = ( False )"
(*val plat_insns_per_tick : unit -> integer*)
definition plat_insns_per_tick :: " unit \<Rightarrow> int " where
" plat_insns_per_tick _ = (( 1 :: int))"
(*val plat_htif_tohost : forall 'a. Size 'a => unit -> bitvector 'a*)
definition plat_htif_tohost :: " unit \<Rightarrow>('a::len)Word.word " where
" plat_htif_tohost _ = ( Word.word_of_int(( 0 :: int)))"
(*val plat_term_write : forall 'a. Size 'a => bitvector 'a -> unit*)
definition plat_term_write :: "('a::len)Word.word \<Rightarrow> unit " where
" plat_term_write _ = ( () )"
(*val plat_term_read : forall 'a. Size 'a => unit -> bitvector 'a*)
definition plat_term_read :: " unit \<Rightarrow>('a::len)Word.word " where
" plat_term_read _ = ( Word.word_of_int(( 0 :: int)))"
(*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 = ( () )"
(* print_endline (msg ^ s) *)
(*val prerr_string : string -> string -> unit*)
definition prerr_string :: " string \<Rightarrow> string \<Rightarrow> unit " where
" prerr_string msg s = ( prerr_endline (msg @ s))"
(*val prerr_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit*)
definition prerr_bits :: " string \<Rightarrow>('a::len)Word.word \<Rightarrow> unit " where
" prerr_bits msg bs = ( prerr_endline (msg @ (show_bitlist (List.map bitU_of_bool (Word.to_bl bs)))))"
(*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 = ( () )"
(* print_endline (msg ^ (show_bitlist (bits_of bs))) *)
end