source: driver/extracted/toCminor.mli @ 3106

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

New extraction

File size: 15.2 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
27open Exp
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75open Csyntax
76
77open TypeComparison
78
79open ClassifyOp
80
81open Fresh
82
83val gather_mem_vars_addr : Csyntax.expr -> Identifiers.identifier_set
84
85val gather_mem_vars_expr : Csyntax.expr -> Identifiers.identifier_set
86
87val gather_mem_vars_ls :
88  Csyntax.labeled_statements -> Identifiers.identifier_set
89
90val gather_mem_vars_stmt : Csyntax.statement -> Identifiers.identifier_set
91
92type var_type =
93| Global of AST.region
94| Stack of Nat.nat
95| Local
96
97val var_type_rect_Type4 :
98  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
99
100val var_type_rect_Type5 :
101  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
102
103val var_type_rect_Type3 :
104  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
105
106val var_type_rect_Type2 :
107  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
108
109val var_type_rect_Type1 :
110  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
111
112val var_type_rect_Type0 :
113  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
114
115val var_type_inv_rect_Type4 :
116  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
117  'a1) -> 'a1
118
119val var_type_inv_rect_Type3 :
120  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
121  'a1) -> 'a1
122
123val var_type_inv_rect_Type2 :
124  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
125  'a1) -> 'a1
126
127val var_type_inv_rect_Type1 :
128  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
129  'a1) -> 'a1
130
131val var_type_inv_rect_Type0 :
132  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
133  'a1) -> 'a1
134
135val var_type_discr : var_type -> var_type -> __
136
137val var_type_jmdiscr : var_type -> var_type -> __
138
139type var_types =
140  (var_type, Csyntax.type0) Types.prod Identifiers.identifier_map
141
142val lookup' :
143  var_types -> PreIdentifiers.identifier -> (var_type, Csyntax.type0)
144  Types.prod Errors.res
145
146val always_alloc : Csyntax.type0 -> Bool.bool
147
148val characterise_vars :
149  ((AST.ident, AST.region) Types.prod, Csyntax.type0) Types.prod List.list ->
150  Csyntax.function0 -> (var_types, Nat.nat) Types.prod
151
152open FrontEndVal
153
154open Hide
155
156open ByteValues
157
158open GenMem
159
160open FrontEndMem
161
162open Division
163
164open Z
165
166open BitVectorZ
167
168open Pointers
169
170open Values
171
172open FrontEndOps
173
174open Cminor_syntax
175
176val type_should_eq : Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 Errors.res
177
178val region_should_eq : AST.region -> AST.region -> 'a1 -> 'a1 Errors.res
179
180val typ_should_eq : AST.typ -> AST.typ -> 'a1 -> 'a1 Errors.res
181
182val translate_unop :
183  AST.typ -> AST.typ -> Csyntax.unary_operation ->
184  FrontEndOps.unary_operation Errors.res
185
186val fix_ptr_type :
187  Csyntax.type0 -> Nat.nat Types.option -> Cminor_syntax.expr ->
188  Cminor_syntax.expr
189
190val translate_add :
191  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
192  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
193
194val translate_sub :
195  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
196  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
197
198val translate_mul :
199  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
200  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
201
202val translate_div :
203  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
204  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
205
206val translate_mod :
207  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
208  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
209
210val translate_shr :
211  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
212  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
213
214val complete_cmp :
215  Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
216
217val translate_cmp :
218  Integers.comparison -> Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 ->
219  Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
220
221val translate_misc_aop :
222  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> (AST.intsize ->
223  AST.signedness -> FrontEndOps.binary_operation) -> Cminor_syntax.expr ->
224  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
225
226val translate_binop :
227  Csyntax.binary_operation -> Csyntax.type0 -> Cminor_syntax.expr ->
228  Csyntax.type0 -> Cminor_syntax.expr -> Csyntax.type0 -> Cminor_syntax.expr
229  Errors.res
230
231val translate_cast :
232  Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr Types.sig0 ->
233  Cminor_syntax.expr Types.sig0 Errors.res
234
235val cm_zero : AST.intsize -> AST.signedness -> Cminor_syntax.expr
236
237val cm_one : AST.intsize -> AST.signedness -> Cminor_syntax.expr
238
239val translate_addr :
240  var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res
241
242val translate_expr :
243  var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res
244
245type destination =
246| IdDest of AST.ident
247| MemDest of Cminor_syntax.expr Types.sig0
248
249val destination_rect_Type4 :
250  var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
251  Types.sig0 -> 'a1) -> destination -> 'a1
252
253val destination_rect_Type5 :
254  var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
255  Types.sig0 -> 'a1) -> destination -> 'a1
256
257val destination_rect_Type3 :
258  var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
259  Types.sig0 -> 'a1) -> destination -> 'a1
260
261val destination_rect_Type2 :
262  var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
263  Types.sig0 -> 'a1) -> destination -> 'a1
264
265val destination_rect_Type1 :
266  var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
267  Types.sig0 -> 'a1) -> destination -> 'a1
268
269val destination_rect_Type0 :
270  var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
271  Types.sig0 -> 'a1) -> destination -> 'a1
272
273val destination_inv_rect_Type4 :
274  var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
275  (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
276
277val destination_inv_rect_Type3 :
278  var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
279  (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
280
281val destination_inv_rect_Type2 :
282  var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
283  (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
284
285val destination_inv_rect_Type1 :
286  var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
287  (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
288
289val destination_inv_rect_Type0 :
290  var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
291  (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
292
293val destination_discr :
294  var_types -> AST.typ -> destination -> destination -> __
295
296val destination_jmdiscr :
297  var_types -> AST.typ -> destination -> destination -> __
298
299val translate_dest : var_types -> Csyntax.expr -> destination Errors.res
300
301type lenv = PreIdentifiers.identifier Identifiers.identifier_map
302
303val lookup_label :
304  lenv -> PreIdentifiers.identifier -> PreIdentifiers.identifier Errors.res
305
306type labgen = { labuniverse : Identifiers.universe;
307                label_genlist : PreIdentifiers.identifier List.list }
308
309val labgen_rect_Type4 :
310  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
311  -> labgen -> 'a1
312
313val labgen_rect_Type5 :
314  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
315  -> labgen -> 'a1
316
317val labgen_rect_Type3 :
318  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
319  -> labgen -> 'a1
320
321val labgen_rect_Type2 :
322  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
323  -> labgen -> 'a1
324
325val labgen_rect_Type1 :
326  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
327  -> labgen -> 'a1
328
329val labgen_rect_Type0 :
330  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
331  -> labgen -> 'a1
332
333val labuniverse : labgen -> Identifiers.universe
334
335val label_genlist : labgen -> PreIdentifiers.identifier List.list
336
337val labgen_inv_rect_Type4 :
338  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
339  __ -> __ -> 'a1) -> 'a1
340
341val labgen_inv_rect_Type3 :
342  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
343  __ -> __ -> 'a1) -> 'a1
344
345val labgen_inv_rect_Type2 :
346  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
347  __ -> __ -> 'a1) -> 'a1
348
349val labgen_inv_rect_Type1 :
350  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
351  __ -> __ -> 'a1) -> 'a1
352
353val labgen_inv_rect_Type0 :
354  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
355  __ -> __ -> 'a1) -> 'a1
356
357val labgen_discr : labgen -> labgen -> __
358
359val labgen_jmdiscr : labgen -> labgen -> __
360
361val generate_fresh_label :
362  labgen -> (PreIdentifiers.identifier, labgen) Types.prod Types.sig0
363
364val labels_defined_switch : Csyntax.labeled_statements -> AST.ident List.list
365
366val labels_defined : Csyntax.statement -> AST.ident List.list
367
368val m_option_map :
369  ('a1 -> 'a2 Errors.res) -> 'a1 Types.option -> 'a2 Types.option Errors.res
370
371val translate_expr_sigma :
372  var_types -> Csyntax.expr -> (AST.typ, Cminor_syntax.expr) Types.dPair
373  Types.sig0 Errors.res
374
375val add_tmps :
376  var_types -> (AST.ident, Csyntax.type0) Types.prod List.list -> var_types
377
378type tmpgen = { tmp_universe : Identifiers.universe;
379                tmp_env : (AST.ident, Csyntax.type0) Types.prod List.list }
380
381val tmpgen_rect_Type4 :
382  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
383  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
384
385val tmpgen_rect_Type5 :
386  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
387  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
388
389val tmpgen_rect_Type3 :
390  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
391  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
392
393val tmpgen_rect_Type2 :
394  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
395  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
396
397val tmpgen_rect_Type1 :
398  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
399  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
400
401val tmpgen_rect_Type0 :
402  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
403  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
404
405val tmp_universe : var_types -> tmpgen -> Identifiers.universe
406
407val tmp_env :
408  var_types -> tmpgen -> (AST.ident, Csyntax.type0) Types.prod List.list
409
410val tmpgen_inv_rect_Type4 :
411  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
412  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
413
414val tmpgen_inv_rect_Type3 :
415  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
416  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
417
418val tmpgen_inv_rect_Type2 :
419  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
420  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
421
422val tmpgen_inv_rect_Type1 :
423  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
424  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
425
426val tmpgen_inv_rect_Type0 :
427  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
428  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
429
430val tmpgen_discr : var_types -> tmpgen -> tmpgen -> __
431
432val tmpgen_jmdiscr : var_types -> tmpgen -> tmpgen -> __
433
434val alloc_tmp :
435  var_types -> Csyntax.type0 -> tmpgen -> (AST.ident, tmpgen) Types.prod
436
437val mklabels :
438  labgen -> ((PreIdentifiers.identifier, PreIdentifiers.identifier)
439  Types.prod, labgen) Types.prod
440
441type convert_flag =
442| DoNotConvert
443| ConvertTo of PreIdentifiers.identifier * PreIdentifiers.identifier
444
445val convert_flag_rect_Type4 :
446  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
447  convert_flag -> 'a1
448
449val convert_flag_rect_Type5 :
450  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
451  convert_flag -> 'a1
452
453val convert_flag_rect_Type3 :
454  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
455  convert_flag -> 'a1
456
457val convert_flag_rect_Type2 :
458  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
459  convert_flag -> 'a1
460
461val convert_flag_rect_Type1 :
462  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
463  convert_flag -> 'a1
464
465val convert_flag_rect_Type0 :
466  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
467  convert_flag -> 'a1
468
469val convert_flag_inv_rect_Type4 :
470  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
471  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
472
473val convert_flag_inv_rect_Type3 :
474  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
475  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
476
477val convert_flag_inv_rect_Type2 :
478  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
479  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
480
481val convert_flag_inv_rect_Type1 :
482  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
483  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
484
485val convert_flag_inv_rect_Type0 :
486  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
487  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
488
489val convert_flag_discr : convert_flag -> convert_flag -> __
490
491val convert_flag_jmdiscr : convert_flag -> convert_flag -> __
492
493val labels_of_flag : convert_flag -> PreIdentifiers.identifier List.list
494
495val translate_statement :
496  var_types -> tmpgen -> labgen -> lenv -> convert_flag -> AST.typ
497  Types.option -> Csyntax.statement -> ((tmpgen, labgen) Types.prod,
498  Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res
499
500val alloc_params_main :
501  var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag -> AST.typ
502  Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list ->
503  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 ->
504  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0
505  Errors.res
506
507val alloc_params :
508  var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag -> AST.typ
509  Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list ->
510  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 ->
511  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0
512  Errors.res
513
514val populate_lenv :
515  AST.ident List.list -> labgen -> lenv -> (lenv Types.sig0, labgen)
516  Types.prod Errors.res
517
518val build_label_env :
519  Csyntax.statement -> (lenv Types.sig0, labgen) Types.prod Errors.res
520
521val translate_function :
522  Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0)
523  Types.prod List.list -> Csyntax.function0 ->
524  Cminor_syntax.internal_function Errors.res
525
526val translate_fundef :
527  Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0)
528  Types.prod List.list -> Csyntax.clight_fundef ->
529  Cminor_syntax.internal_function AST.fundef Errors.res
530
531val map_partial_All :
532  ('a1 -> __ -> 'a2 Errors.res) -> 'a1 List.list -> 'a2 List.list Errors.res
533
534val clight_to_cminor :
535  Csyntax.clight_program -> Cminor_syntax.cminor_program Errors.res
536
Note: See TracBrowser for help on using the repository browser.