forked from rems-project/sail
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Mips_extras.thy
248 lines (174 loc) · 14.2 KB
/
Mips_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
240
241
242
243
244
245
246
247
248
chapter \<open>Generated by Lem from \<open>/auto/homes/tb592/REMS/sail/mips/mips_extras.lem\<close>.\<close>
theory "Mips_extras"
imports
Main
"LEM.Lem_pervasives"
"LEM.Lem_pervasives_extra"
"Sail.Sail2_instr_kinds"
"Sail.Sail2_values"
"Sail.Sail2_prompt_monad"
"Sail.Sail2_prompt"
"Sail.Sail2_operators"
begin
(*open import Pervasives*)
(*open import Pervasives_extra*)
(*open import Sail2_instr_kinds*)
(*open import Sail2_values*)
(*open import Sail2_operators*)
(*open import Sail2_prompt_monad*)
(*open import Sail2_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_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 = ( read_mem
dict_Sail2_values_Bitvector_a dict_Sail2_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_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 = ( read_mem
dict_Sail2_values_Bitvector_a dict_Sail2_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_Sail2_values_Bitvector_a addr = (
read_tag dict_Sail2_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_Sail2_values_Bitvector_a addr t = ( write_tag
dict_Sail2_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_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 = (
read_mem dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b Read_plain addr size1 \<bind> (\<lambda> v .
read_tag_bool dict_Sail2_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_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 = (
read_mem dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b Read_plain addr size1 \<bind> (\<lambda> v .
read_tag_bool dict_Sail2_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_Sail2_values_Bitvector_a addr size1 = ( write_mem_ea
dict_Sail2_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_Sail2_values_Bitvector_a addr size1 = ( write_mem_ea
dict_Sail2_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_Sail2_values_Bitvector_a addr size1 = ( write_mem_ea
dict_Sail2_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_Sail2_values_Bitvector_a addr size1 = ( write_mem_ea
dict_Sail2_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_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b _ size1 v = ( write_mem_val
dict_Sail2_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_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b _ size1 v = ( write_mem_val
dict_Sail2_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_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 t v = ( write_mem_val
dict_Sail2_values_Bitvector_b v \<bind> (\<lambda>x . (case x of
_ => write_tag_bool dict_Sail2_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_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 t v = ( write_mem_val
dict_Sail2_values_Bitvector_b v \<bind> (\<lambda> b . write_tag_bool
dict_Sail2_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_Sail2_values_Bitvector_a len n lo = (
(of_bools_method dict_Sail2_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_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b _ size1 _ addr data = (
MEMea dict_Sail2_values_Bitvector_b addr size1 \<then>
MEMval dict_Sail2_values_Bitvector_b dict_Sail2_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_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_c _ size1 _ addr = ( MEMr
dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_c addr size1 )"
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 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_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_d dict_Sail2_values_Bitvector_e v n = (
(let r = (Option.bind (
(unsigned_method dict_Sail2_values_Bitvector_e) n) (\<lambda> n . (of_bits_method dict_Sail2_values_Bitvector_b) (shiftl_bv dict_Sail2_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_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_d dict_Sail2_values_Bitvector_e v n = (
(let r = (Option.bind (
(unsigned_method dict_Sail2_values_Bitvector_e) n) (\<lambda> n . (of_bits_method dict_Sail2_values_Bitvector_b) (shiftr_bv dict_Sail2_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_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_d dict_Sail2_values_Bitvector_e v n = (
(let r = (Option.bind (
(unsigned_method dict_Sail2_values_Bitvector_e) n) (\<lambda> n . (of_bits_method dict_Sail2_values_Bitvector_b) (arith_shiftr_bv dict_Sail2_values_Bitvector_d v n))) in
maybe_fail (''shift_bits_right_arith'') r))"
(* Use constants for undefined values for now *)
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_Sail2_values_Bitvector_a len = ( return (
(of_bools_method dict_Sail2_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_Sail2_values_Bitvector_a = (
undefined_bitvector dict_Sail2_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_Sail2_values_Bitvector_a msg bs = ( print_endline (msg @ (string_of_bv
dict_Sail2_values_Bitvector_a bs)))"
definition prerr_bits :: " 'a Bitvector_class \<Rightarrow> string \<Rightarrow> 'a \<Rightarrow> unit " where
" prerr_bits dict_Sail2_values_Bitvector_a msg bs = ( prerr_endline (msg @ (string_of_bv
dict_Sail2_values_Bitvector_a bs)))"
(*val prerr_string : string -> unit*)
definition prerr_string :: " string \<Rightarrow> unit " where
" prerr_string _ = ( () )"
(*val get_time_ns : unit -> integer*)
definition get_time_ns :: " unit \<Rightarrow> int " where
" get_time_ns _ = (( 0 :: int))"
(*val cycle_count : unit -> unit*)
definition cycle_count :: " unit \<Rightarrow> unit " where
" cycle_count _ = ( () )"
end