1 | open Preamble |
---|
2 | |
---|
3 | open Bool |
---|
4 | |
---|
5 | open Relations |
---|
6 | |
---|
7 | open Nat |
---|
8 | |
---|
9 | open Hints_declaration |
---|
10 | |
---|
11 | open Core_notation |
---|
12 | |
---|
13 | open Pts |
---|
14 | |
---|
15 | open Logic |
---|
16 | |
---|
17 | open Types |
---|
18 | |
---|
19 | open List |
---|
20 | |
---|
21 | open ErrorMessages |
---|
22 | |
---|
23 | open Option |
---|
24 | |
---|
25 | open Setoids |
---|
26 | |
---|
27 | open Monad |
---|
28 | |
---|
29 | open Jmeq |
---|
30 | |
---|
31 | open Russell |
---|
32 | |
---|
33 | open Positive |
---|
34 | |
---|
35 | open PreIdentifiers |
---|
36 | |
---|
37 | open Errors |
---|
38 | |
---|
39 | open Extra_bool |
---|
40 | |
---|
41 | open Coqlib |
---|
42 | |
---|
43 | open Values |
---|
44 | |
---|
45 | open FrontEndVal |
---|
46 | |
---|
47 | open Hide |
---|
48 | |
---|
49 | open ByteValues |
---|
50 | |
---|
51 | open Division |
---|
52 | |
---|
53 | open Z |
---|
54 | |
---|
55 | open BitVectorZ |
---|
56 | |
---|
57 | open Pointers |
---|
58 | |
---|
59 | open GenMem |
---|
60 | |
---|
61 | open FrontEndMem |
---|
62 | |
---|
63 | open Proper |
---|
64 | |
---|
65 | open PositiveMap |
---|
66 | |
---|
67 | open Deqsets |
---|
68 | |
---|
69 | open Extralib |
---|
70 | |
---|
71 | open Lists |
---|
72 | |
---|
73 | open Identifiers |
---|
74 | |
---|
75 | open Arithmetic |
---|
76 | |
---|
77 | open Vector |
---|
78 | |
---|
79 | open Div_and_mod |
---|
80 | |
---|
81 | open Util |
---|
82 | |
---|
83 | open FoldStuff |
---|
84 | |
---|
85 | open BitVector |
---|
86 | |
---|
87 | open Extranat |
---|
88 | |
---|
89 | open Integers |
---|
90 | |
---|
91 | open AST |
---|
92 | |
---|
93 | open Globalenvs |
---|
94 | |
---|
95 | open CostLabel |
---|
96 | |
---|
97 | open Events |
---|
98 | |
---|
99 | open IOMonad |
---|
100 | |
---|
101 | open IO |
---|
102 | |
---|
103 | open SmallstepExec |
---|
104 | |
---|
105 | open BitVectorTrie |
---|
106 | |
---|
107 | open Graphs |
---|
108 | |
---|
109 | open Order |
---|
110 | |
---|
111 | open Registers |
---|
112 | |
---|
113 | open FrontEndOps |
---|
114 | |
---|
115 | open RTLabs_syntax |
---|
116 | |
---|
117 | type genv = RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t |
---|
118 | |
---|
119 | type frame = { func : RTLabs_syntax.internal_function; |
---|
120 | locals : Values.val0 Registers.register_env; |
---|
121 | next : Graphs.label; sp : Pointers.block; |
---|
122 | retdst : Registers.register Types.option } |
---|
123 | |
---|
124 | val frame_rect_Type4 : |
---|
125 | (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> |
---|
126 | Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> |
---|
127 | 'a1) -> frame -> 'a1 |
---|
128 | |
---|
129 | val frame_rect_Type5 : |
---|
130 | (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> |
---|
131 | Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> |
---|
132 | 'a1) -> frame -> 'a1 |
---|
133 | |
---|
134 | val frame_rect_Type3 : |
---|
135 | (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> |
---|
136 | Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> |
---|
137 | 'a1) -> frame -> 'a1 |
---|
138 | |
---|
139 | val frame_rect_Type2 : |
---|
140 | (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> |
---|
141 | Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> |
---|
142 | 'a1) -> frame -> 'a1 |
---|
143 | |
---|
144 | val frame_rect_Type1 : |
---|
145 | (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> |
---|
146 | Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> |
---|
147 | 'a1) -> frame -> 'a1 |
---|
148 | |
---|
149 | val frame_rect_Type0 : |
---|
150 | (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> |
---|
151 | Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> |
---|
152 | 'a1) -> frame -> 'a1 |
---|
153 | |
---|
154 | val func : frame -> RTLabs_syntax.internal_function |
---|
155 | |
---|
156 | val locals : frame -> Values.val0 Registers.register_env |
---|
157 | |
---|
158 | val next : frame -> Graphs.label |
---|
159 | |
---|
160 | val sp : frame -> Pointers.block |
---|
161 | |
---|
162 | val retdst : frame -> Registers.register Types.option |
---|
163 | |
---|
164 | val frame_inv_rect_Type4 : |
---|
165 | frame -> (RTLabs_syntax.internal_function -> Values.val0 |
---|
166 | Registers.register_env -> Graphs.label -> __ -> Pointers.block -> |
---|
167 | Registers.register Types.option -> __ -> 'a1) -> 'a1 |
---|
168 | |
---|
169 | val frame_inv_rect_Type3 : |
---|
170 | frame -> (RTLabs_syntax.internal_function -> Values.val0 |
---|
171 | Registers.register_env -> Graphs.label -> __ -> Pointers.block -> |
---|
172 | Registers.register Types.option -> __ -> 'a1) -> 'a1 |
---|
173 | |
---|
174 | val frame_inv_rect_Type2 : |
---|
175 | frame -> (RTLabs_syntax.internal_function -> Values.val0 |
---|
176 | Registers.register_env -> Graphs.label -> __ -> Pointers.block -> |
---|
177 | Registers.register Types.option -> __ -> 'a1) -> 'a1 |
---|
178 | |
---|
179 | val frame_inv_rect_Type1 : |
---|
180 | frame -> (RTLabs_syntax.internal_function -> Values.val0 |
---|
181 | Registers.register_env -> Graphs.label -> __ -> Pointers.block -> |
---|
182 | Registers.register Types.option -> __ -> 'a1) -> 'a1 |
---|
183 | |
---|
184 | val frame_inv_rect_Type0 : |
---|
185 | frame -> (RTLabs_syntax.internal_function -> Values.val0 |
---|
186 | Registers.register_env -> Graphs.label -> __ -> Pointers.block -> |
---|
187 | Registers.register Types.option -> __ -> 'a1) -> 'a1 |
---|
188 | |
---|
189 | val frame_jmdiscr : frame -> frame -> __ |
---|
190 | |
---|
191 | val adv : Graphs.label -> frame -> frame |
---|
192 | |
---|
193 | type state0 = |
---|
194 | | State of frame * frame List.list * GenMem.mem1 |
---|
195 | | Callstate of RTLabs_syntax.internal_function AST.fundef |
---|
196 | * Values.val0 List.list * Registers.register Types.option |
---|
197 | * frame List.list * GenMem.mem1 |
---|
198 | | Returnstate of Values.val0 Types.option * Registers.register Types.option |
---|
199 | * frame List.list * GenMem.mem1 |
---|
200 | | Finalstate of Integers.int |
---|
201 | |
---|
202 | val state_rect_Type4 : |
---|
203 | (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> |
---|
204 | (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
---|
205 | Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1) |
---|
206 | -> (Values.val0 Types.option -> Registers.register Types.option -> frame |
---|
207 | List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 |
---|
208 | |
---|
209 | val state_rect_Type5 : |
---|
210 | (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> |
---|
211 | (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
---|
212 | Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1) |
---|
213 | -> (Values.val0 Types.option -> Registers.register Types.option -> frame |
---|
214 | List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 |
---|
215 | |
---|
216 | val state_rect_Type3 : |
---|
217 | (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> |
---|
218 | (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
---|
219 | Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1) |
---|
220 | -> (Values.val0 Types.option -> Registers.register Types.option -> frame |
---|
221 | List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 |
---|
222 | |
---|
223 | val state_rect_Type2 : |
---|
224 | (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> |
---|
225 | (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
---|
226 | Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1) |
---|
227 | -> (Values.val0 Types.option -> Registers.register Types.option -> frame |
---|
228 | List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 |
---|
229 | |
---|
230 | val state_rect_Type1 : |
---|
231 | (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> |
---|
232 | (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
---|
233 | Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1) |
---|
234 | -> (Values.val0 Types.option -> Registers.register Types.option -> frame |
---|
235 | List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 |
---|
236 | |
---|
237 | val state_rect_Type0 : |
---|
238 | (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> |
---|
239 | (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
---|
240 | Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1) |
---|
241 | -> (Values.val0 Types.option -> Registers.register Types.option -> frame |
---|
242 | List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1 |
---|
243 | |
---|
244 | val state_inv_rect_Type4 : |
---|
245 | state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) -> |
---|
246 | (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
---|
247 | Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ -> |
---|
248 | 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> |
---|
249 | frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) |
---|
250 | -> 'a1 |
---|
251 | |
---|
252 | val state_inv_rect_Type3 : |
---|
253 | state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) -> |
---|
254 | (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
---|
255 | Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ -> |
---|
256 | 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> |
---|
257 | frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) |
---|
258 | -> 'a1 |
---|
259 | |
---|
260 | val state_inv_rect_Type2 : |
---|
261 | state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) -> |
---|
262 | (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
---|
263 | Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ -> |
---|
264 | 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> |
---|
265 | frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) |
---|
266 | -> 'a1 |
---|
267 | |
---|
268 | val state_inv_rect_Type1 : |
---|
269 | state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) -> |
---|
270 | (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
---|
271 | Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ -> |
---|
272 | 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> |
---|
273 | frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) |
---|
274 | -> 'a1 |
---|
275 | |
---|
276 | val state_inv_rect_Type0 : |
---|
277 | state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) -> |
---|
278 | (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> |
---|
279 | Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ -> |
---|
280 | 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> |
---|
281 | frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) |
---|
282 | -> 'a1 |
---|
283 | |
---|
284 | val state_discr : state0 -> state0 -> __ |
---|
285 | |
---|
286 | val state_jmdiscr : state0 -> state0 -> __ |
---|
287 | |
---|
288 | val build_state : |
---|
289 | frame -> frame List.list -> GenMem.mem1 -> Graphs.label -> state0 |
---|
290 | |
---|
291 | val next_instruction : frame -> RTLabs_syntax.statement |
---|
292 | |
---|
293 | val init_locals : |
---|
294 | (Registers.register, AST.typ) Types.prod List.list -> Values.val0 |
---|
295 | Registers.register_env |
---|
296 | |
---|
297 | val reg_store : |
---|
298 | PreIdentifiers.identifier -> Values.val0 -> Values.val0 |
---|
299 | Identifiers.identifier_map -> Values.val0 Identifiers.identifier_map |
---|
300 | Errors.res |
---|
301 | |
---|
302 | val params_store : |
---|
303 | (Registers.register, AST.typ) Types.prod List.list -> Values.val0 List.list |
---|
304 | -> Values.val0 Registers.register_env -> Values.val0 Registers.register_env |
---|
305 | Errors.res |
---|
306 | |
---|
307 | val reg_retrieve : |
---|
308 | Values.val0 Registers.register_env -> Registers.register -> Values.val0 |
---|
309 | Errors.res |
---|
310 | |
---|
311 | val eval_statement : |
---|
312 | genv -> state0 -> (IO.io_out, IO.io_in, (Events.trace, state0) Types.prod) |
---|
313 | IOMonad.iO |
---|
314 | |
---|
315 | val rTLabs_is_final : state0 -> Integers.int Types.option |
---|
316 | |
---|
317 | val rTLabs_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system |
---|
318 | |
---|
319 | val make_global0 : RTLabs_syntax.rTLabs_program -> genv |
---|
320 | |
---|
321 | val make_initial_state0 : RTLabs_syntax.rTLabs_program -> state0 Errors.res |
---|
322 | |
---|
323 | val rTLabs_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec |
---|
324 | |
---|
325 | val bind_ok : |
---|
326 | 'a1 Errors.res -> ('a1 -> 'a2 Errors.res) -> 'a2 -> ('a1 -> __ -> __ -> |
---|
327 | 'a3) -> 'a3 |
---|
328 | |
---|
329 | val func_block_of_exec : |
---|
330 | genv -> state0 -> Events.trace -> RTLabs_syntax.internal_function |
---|
331 | AST.fundef -> Values.val0 List.list -> Registers.register Types.option -> |
---|
332 | frame List.list -> GenMem.mem1 -> Pointers.block Types.sig0 |
---|
333 | |
---|