source: extracted/toCminor.mli @ 2960

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

New extraction, it diverges in RTL execution now.

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 * Csyntax.type0
247| MemDest of Cminor_syntax.expr Types.sig0
248
249val destination_rect_Type4 :
250  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
251  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
252
253val destination_rect_Type5 :
254  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
255  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
256
257val destination_rect_Type3 :
258  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
259  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
260
261val destination_rect_Type2 :
262  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
263  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
264
265val destination_rect_Type1 :
266  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
267  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
268
269val destination_rect_Type0 :
270  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
271  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
272
273val destination_inv_rect_Type4 :
274  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
275  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
276
277val destination_inv_rect_Type3 :
278  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
279  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
280
281val destination_inv_rect_Type2 :
282  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
283  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
284
285val destination_inv_rect_Type1 :
286  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
287  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
288
289val destination_inv_rect_Type0 :
290  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
291  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
292
293val destination_discr : var_types -> destination -> destination -> __
294
295val destination_jmdiscr : var_types -> destination -> destination -> __
296
297val translate_dest : var_types -> Csyntax.expr -> __
298
299type lenv = PreIdentifiers.identifier Identifiers.identifier_map
300
301val lookup_label :
302  lenv -> PreIdentifiers.identifier -> PreIdentifiers.identifier Errors.res
303
304type labgen = { labuniverse : Identifiers.universe;
305                label_genlist : PreIdentifiers.identifier List.list }
306
307val labgen_rect_Type4 :
308  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
309  -> labgen -> 'a1
310
311val labgen_rect_Type5 :
312  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
313  -> labgen -> 'a1
314
315val labgen_rect_Type3 :
316  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
317  -> labgen -> 'a1
318
319val labgen_rect_Type2 :
320  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
321  -> labgen -> 'a1
322
323val labgen_rect_Type1 :
324  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
325  -> labgen -> 'a1
326
327val labgen_rect_Type0 :
328  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
329  -> labgen -> 'a1
330
331val labuniverse : labgen -> Identifiers.universe
332
333val label_genlist : labgen -> PreIdentifiers.identifier List.list
334
335val labgen_inv_rect_Type4 :
336  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
337  __ -> __ -> 'a1) -> 'a1
338
339val labgen_inv_rect_Type3 :
340  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
341  __ -> __ -> 'a1) -> 'a1
342
343val labgen_inv_rect_Type2 :
344  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
345  __ -> __ -> 'a1) -> 'a1
346
347val labgen_inv_rect_Type1 :
348  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
349  __ -> __ -> 'a1) -> 'a1
350
351val labgen_inv_rect_Type0 :
352  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
353  __ -> __ -> 'a1) -> 'a1
354
355val labgen_discr : labgen -> labgen -> __
356
357val labgen_jmdiscr : labgen -> labgen -> __
358
359val generate_fresh_label :
360  labgen -> (PreIdentifiers.identifier, labgen) Types.prod Types.sig0
361
362val labels_defined_switch : Csyntax.labeled_statements -> AST.ident List.list
363
364val labels_defined : Csyntax.statement -> AST.ident List.list
365
366val m_option_map :
367  ('a1 -> 'a2 Errors.res) -> 'a1 Types.option -> 'a2 Types.option Errors.res
368
369val translate_expr_sigma :
370  var_types -> Csyntax.expr -> (AST.typ, Cminor_syntax.expr) Types.dPair
371  Types.sig0 Errors.res
372
373val add_tmps :
374  var_types -> (AST.ident, Csyntax.type0) Types.prod List.list -> var_types
375
376type tmpgen = { tmp_universe : Identifiers.universe;
377                tmp_env : (AST.ident, Csyntax.type0) Types.prod List.list }
378
379val tmpgen_rect_Type4 :
380  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
381  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
382
383val tmpgen_rect_Type5 :
384  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
385  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
386
387val tmpgen_rect_Type3 :
388  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
389  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
390
391val tmpgen_rect_Type2 :
392  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
393  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
394
395val tmpgen_rect_Type1 :
396  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
397  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
398
399val tmpgen_rect_Type0 :
400  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
401  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1
402
403val tmp_universe : var_types -> tmpgen -> Identifiers.universe
404
405val tmp_env :
406  var_types -> tmpgen -> (AST.ident, Csyntax.type0) Types.prod List.list
407
408val tmpgen_inv_rect_Type4 :
409  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
410  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
411
412val tmpgen_inv_rect_Type3 :
413  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
414  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
415
416val tmpgen_inv_rect_Type2 :
417  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
418  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
419
420val tmpgen_inv_rect_Type1 :
421  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
422  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
423
424val tmpgen_inv_rect_Type0 :
425  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
426  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1
427
428val tmpgen_discr : var_types -> tmpgen -> tmpgen -> __
429
430val tmpgen_jmdiscr : var_types -> tmpgen -> tmpgen -> __
431
432val alloc_tmp :
433  var_types -> Csyntax.type0 -> tmpgen -> (AST.ident, tmpgen) Types.prod
434
435val mklabels :
436  labgen -> ((PreIdentifiers.identifier, PreIdentifiers.identifier)
437  Types.prod, labgen) Types.prod
438
439type convert_flag =
440| DoNotConvert
441| ConvertTo of PreIdentifiers.identifier * PreIdentifiers.identifier
442
443val convert_flag_rect_Type4 :
444  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
445  convert_flag -> 'a1
446
447val convert_flag_rect_Type5 :
448  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
449  convert_flag -> 'a1
450
451val convert_flag_rect_Type3 :
452  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
453  convert_flag -> 'a1
454
455val convert_flag_rect_Type2 :
456  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
457  convert_flag -> 'a1
458
459val convert_flag_rect_Type1 :
460  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
461  convert_flag -> 'a1
462
463val convert_flag_rect_Type0 :
464  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
465  convert_flag -> 'a1
466
467val convert_flag_inv_rect_Type4 :
468  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
469  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
470
471val convert_flag_inv_rect_Type3 :
472  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
473  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
474
475val convert_flag_inv_rect_Type2 :
476  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
477  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
478
479val convert_flag_inv_rect_Type1 :
480  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
481  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
482
483val convert_flag_inv_rect_Type0 :
484  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
485  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1
486
487val convert_flag_discr : convert_flag -> convert_flag -> __
488
489val convert_flag_jmdiscr : convert_flag -> convert_flag -> __
490
491val labels_of_flag : convert_flag -> PreIdentifiers.identifier List.list
492
493val translate_statement :
494  var_types -> tmpgen -> labgen -> lenv -> convert_flag -> AST.typ
495  Types.option -> Csyntax.statement -> ((tmpgen, labgen) Types.prod,
496  Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res
497
498val alloc_params_main :
499  var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag -> AST.typ
500  Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list ->
501  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 ->
502  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0
503  Errors.res
504
505val alloc_params :
506  var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag -> AST.typ
507  Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list ->
508  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 ->
509  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0
510  Errors.res
511
512val populate_lenv :
513  AST.ident List.list -> labgen -> lenv -> (lenv Types.sig0, labgen)
514  Types.prod Errors.res
515
516val build_label_env :
517  Csyntax.statement -> (lenv Types.sig0, labgen) Types.prod Errors.res
518
519val translate_function :
520  Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0)
521  Types.prod List.list -> Csyntax.function0 ->
522  Cminor_syntax.internal_function Errors.res
523
524val translate_fundef :
525  Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0)
526  Types.prod List.list -> Csyntax.clight_fundef ->
527  Cminor_syntax.internal_function AST.fundef Errors.res
528
529val map_partial_All :
530  ('a1 -> __ -> 'a2 Errors.res) -> 'a1 List.list -> 'a2 List.list Errors.res
531
532val clight_to_cminor :
533  Csyntax.clight_program -> Cminor_syntax.cminor_program Errors.res
534
Note: See TracBrowser for help on using the repository browser.