source: driver/extracted/cminor_semantics.mli @ 3106

Last change on this file since 3106 was 2810, checked in by sacerdot, 7 years ago

Cminor semantics exported.

File size: 11.1 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 Exp
24
25open Arithmetic
26
27open Extranat
28
29open Vector
30
31open FoldStuff
32
33open BitVector
34
35open Z
36
37open BitVectorZ
38
39open Pointers
40
41open ErrorMessages
42
43open Option
44
45open Setoids
46
47open Monad
48
49open Positive
50
51open PreIdentifiers
52
53open Errors
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Util
62
63open Bool
64
65open Relations
66
67open Nat
68
69open List
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Types
80
81open Coqlib
82
83open Values
84
85open Events
86
87open FrontEndVal
88
89open Hide
90
91open ByteValues
92
93open GenMem
94
95open FrontEndMem
96
97open IOMonad
98
99open IO
100
101open Extra_bool
102
103open Globalenvs
104
105open SmallstepExec
106
107open FrontEndOps
108
109open Cminor_syntax
110
111type env = Values.val0 Identifiers.identifier_map
112
113type genv = Cminor_syntax.internal_function AST.fundef Globalenvs.genv_t
114
115type cont =
116| Kend
117| Kseq of Cminor_syntax.stmt * cont
118| Kblock of cont
119
120val cont_rect_Type4 :
121  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
122  -> cont -> 'a1
123
124val cont_rect_Type3 :
125  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
126  -> cont -> 'a1
127
128val cont_rect_Type2 :
129  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
130  -> cont -> 'a1
131
132val cont_rect_Type1 :
133  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
134  -> cont -> 'a1
135
136val cont_rect_Type0 :
137  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
138  -> cont -> 'a1
139
140val cont_inv_rect_Type4 :
141  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
142  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
143
144val cont_inv_rect_Type3 :
145  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
146  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
147
148val cont_inv_rect_Type2 :
149  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
150  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
151
152val cont_inv_rect_Type1 :
153  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
154  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
155
156val cont_inv_rect_Type0 :
157  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
158  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
159
160val cont_discr : cont -> cont -> __
161
162val cont_jmdiscr : cont -> cont -> __
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 state =
223| State of Cminor_syntax.internal_function * Cminor_syntax.stmt * env
224   * GenMem.mem * Pointers.block * cont * stack
225| Callstate of AST.ident * Cminor_syntax.internal_function AST.fundef
226   * Values.val0 List.list * GenMem.mem * stack
227| Returnstate of Values.val0 Types.option * GenMem.mem * stack
228| Finalstate of Integers.int
229
230val state_rect_Type4 :
231  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
232  -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
233  (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
234  List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
235  GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
236
237val state_rect_Type5 :
238  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
239  -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
240  (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
241  List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
242  GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
243
244val state_rect_Type3 :
245  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
246  -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
247  (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
248  List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
249  GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
250
251val state_rect_Type2 :
252  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
253  -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
254  (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
255  List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
256  GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
257
258val state_rect_Type1 :
259  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
260  -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
261  (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
262  List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
263  GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
264
265val state_rect_Type0 :
266  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
267  -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
268  (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
269  List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
270  GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
271
272val state_inv_rect_Type4 :
273  state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
274  __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
275  'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
276  Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
277  Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
278  'a1) -> 'a1
279
280val state_inv_rect_Type3 :
281  state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
282  __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
283  'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
284  Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
285  Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
286  'a1) -> 'a1
287
288val state_inv_rect_Type2 :
289  state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
290  __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
291  'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
292  Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
293  Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
294  'a1) -> 'a1
295
296val state_inv_rect_Type1 :
297  state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
298  __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
299  'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
300  Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
301  Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
302  'a1) -> 'a1
303
304val state_inv_rect_Type0 :
305  state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
306  __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
307  'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
308  Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
309  Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
310  'a1) -> 'a1
311
312val state_jmdiscr : state -> state -> __
313
314val eval_expr :
315  genv -> AST.typ -> Cminor_syntax.expr -> env -> Pointers.block ->
316  GenMem.mem -> (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 -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod)
348  IOMonad.iO
349
350val is_final : state -> Integers.int Types.option
351
352val cminor_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
353
354val make_global : Cminor_syntax.cminor_program -> genv
355
356val make_initial_state : Cminor_syntax.cminor_program -> state 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 -> state 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.