source: extracted/cminor_semantics.mli @ 2636

Last change on this file since 2636 was 2636, checked in by campbell, 7 years ago

Extracted front-end.

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