source: extracted/cminor_semantics.mli @ 2746

Last change on this file since 2746 was 2649, checked in by sacerdot, 7 years ago

...

File size: 11.0 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open Extralib
12
13open Lists
14
15open Identifiers
16
17open Integers
18
19open AST
20
21open Division
22
23open Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
39open ErrorMessages
40
41open Option
42
43open Setoids
44
45open Monad
46
47open Positive
48
49open PreIdentifiers
50
51open Errors
52
53open Div_and_mod
54
55open Jmeq
56
57open Russell
58
59open Util
60
61open Bool
62
63open Relations
64
65open Nat
66
67open List
68
69open Hints_declaration
70
71open Core_notation
72
73open Pts
74
75open Logic
76
77open Types
78
79open Coqlib
80
81open Values
82
83open Events
84
85open FrontEndVal
86
87open Hide
88
89open ByteValues
90
91open GenMem
92
93open FrontEndMem
94
95open IOMonad
96
97open IO
98
99open Extra_bool
100
101open Globalenvs
102
103open SmallstepExec
104
105open FrontEndOps
106
107open Cminor_syntax
108
109type env = Values.val0 Identifiers.identifier_map
110
111type genv = Cminor_syntax.internal_function AST.fundef Globalenvs.genv_t
112
113type cont =
114| Kend
115| Kseq of Cminor_syntax.stmt * cont
116| Kblock of cont
117
118val cont_rect_Type4 :
119  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
120  -> cont -> 'a1
121
122val cont_rect_Type3 :
123  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
124  -> cont -> 'a1
125
126val cont_rect_Type2 :
127  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
128  -> cont -> 'a1
129
130val cont_rect_Type1 :
131  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
132  -> cont -> 'a1
133
134val cont_rect_Type0 :
135  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
136  -> cont -> 'a1
137
138val cont_inv_rect_Type4 :
139  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
140  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
141
142val cont_inv_rect_Type3 :
143  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
144  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
145
146val cont_inv_rect_Type2 :
147  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
148  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
149
150val cont_inv_rect_Type1 :
151  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
152  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
153
154val cont_inv_rect_Type0 :
155  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
156  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
157
158val cont_discr : cont -> cont -> __
159
160val cont_jmdiscr : cont -> cont -> __
161
162type cont_inv = __
163
164type stack =
165| SStop
166| Scall of (AST.ident, AST.typ) Types.prod Types.option
167   * Cminor_syntax.internal_function * Pointers.block * env * cont * 
168   stack
169
170val stack_rect_Type4 :
171  'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
172  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
173  cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
174
175val stack_rect_Type3 :
176  'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
177  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
178  cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
179
180val stack_rect_Type2 :
181  'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
182  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
183  cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
184
185val stack_rect_Type1 :
186  'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
187  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
188  cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
189
190val stack_rect_Type0 :
191  'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
192  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
193  cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1
194
195val stack_inv_rect_Type4 :
196  stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
197  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
198  cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
199
200val stack_inv_rect_Type3 :
201  stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
202  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
203  cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
204
205val stack_inv_rect_Type2 :
206  stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
207  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
208  cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
209
210val stack_inv_rect_Type1 :
211  stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
212  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
213  cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
214
215val stack_inv_rect_Type0 :
216  stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
217  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
218  cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
219
220val stack_jmdiscr : stack -> stack -> __
221
222type state0 =
223| State of Cminor_syntax.internal_function * Cminor_syntax.stmt * env
224   * GenMem.mem1 * Pointers.block * cont * stack
225| Callstate of Cminor_syntax.internal_function AST.fundef
226   * Values.val0 List.list * GenMem.mem1 * stack
227| Returnstate of Values.val0 Types.option * GenMem.mem1 * stack
228| Finalstate of Integers.int
229
230val state_rect_Type4 :
231  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
232  -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
233  (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list ->
234  GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1 ->
235  stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
236
237val state_rect_Type5 :
238  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
239  -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
240  (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list ->
241  GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1 ->
242  stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
243
244val state_rect_Type3 :
245  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
246  -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
247  (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list ->
248  GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1 ->
249  stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
250
251val state_rect_Type2 :
252  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
253  -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
254  (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list ->
255  GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1 ->
256  stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
257
258val state_rect_Type1 :
259  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
260  -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
261  (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list ->
262  GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1 ->
263  stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
264
265val state_rect_Type0 :
266  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
267  -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
268  (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list ->
269  GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1 ->
270  stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
271
272val state_inv_rect_Type4 :
273  state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
274  __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __ ->
275  'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0
276  List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0
277  Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __
278  -> 'a1) -> 'a1
279
280val state_inv_rect_Type3 :
281  state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
282  __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __ ->
283  'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0
284  List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0
285  Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __
286  -> 'a1) -> 'a1
287
288val state_inv_rect_Type2 :
289  state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
290  __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __ ->
291  'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0
292  List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0
293  Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __
294  -> 'a1) -> 'a1
295
296val state_inv_rect_Type1 :
297  state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
298  __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __ ->
299  'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0
300  List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0
301  Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __
302  -> 'a1) -> 'a1
303
304val state_inv_rect_Type0 :
305  state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
306  __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __ ->
307  'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0
308  List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0
309  Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __
310  -> 'a1) -> 'a1
311
312val state_jmdiscr : state0 -> state0 -> __
313
314val eval_expr :
315  genv -> AST.typ -> Cminor_syntax.expr -> env -> Pointers.block ->
316  GenMem.mem1 -> (Events.trace, Values.val0) Types.prod Errors.res
317
318val k_exit :
319  Nat.nat -> cont -> Cminor_syntax.internal_function -> env -> cont
320  Types.sig0 Errors.res
321
322val find_case :
323  AST.intsize -> AST.bvint -> (AST.bvint, 'a1) Types.prod List.list -> 'a1 ->
324  'a1
325
326val find_label :
327  PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
328  Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
329  Types.prod Types.sig0 Types.option
330
331val find_label_always :
332  PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
333  Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
334  Types.prod Types.sig0
335
336val bind_params :
337  Values.val0 List.list -> (AST.ident, AST.typ) Types.prod List.list -> env
338  Types.sig0 Errors.res
339
340val init_locals : env -> (AST.ident, AST.typ) Types.prod List.list -> env
341
342val trace_map_inv :
343  ('a1 -> __ -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list
344  -> (Events.trace, 'a2 List.list) Types.prod Errors.res
345
346val eval_step :
347  genv -> state0 -> (IO.io_out, IO.io_in, (Events.trace, state0) Types.prod)
348  IOMonad.iO
349
350val is_final0 : state0 -> Integers.int Types.option
351
352val cminor_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
353
354val make_global0 : Cminor_syntax.cminor_program -> genv
355
356val make_initial_state0 : Cminor_syntax.cminor_program -> state0 Errors.res
357
358val cminor_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
359
360val make_noinit_global : Cminor_syntax.cminor_noinit_program -> genv
361
362val make_initial_noinit_state :
363  Cminor_syntax.cminor_noinit_program -> state0 Errors.res
364
365val cminor_noinit_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
366
Note: See TracBrowser for help on using the repository browser.