source: extracted/toCminor.mli @ 2716

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

...

File size: 14.9 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 Setoids
22
23open Monad
24
25open Option
26
27open Lists
28
29open Positive
30
31open Identifiers
32
33open Arithmetic
34
35open Vector
36
37open Div_and_mod
38
39open Jmeq
40
41open Russell
42
43open List
44
45open Util
46
47open FoldStuff
48
49open BitVector
50
51open Extranat
52
53open Bool
54
55open Relations
56
57open Nat
58
59open Integers
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Types
70
71open AST
72
73open Csyntax
74
75open TypeComparison
76
77open ClassifyOp
78
79open Fresh
80
81val gather_mem_vars_addr : Csyntax.expr -> Identifiers.identifier_set
82
83val gather_mem_vars_expr : Csyntax.expr -> Identifiers.identifier_set
84
85val gather_mem_vars_ls :
86  Csyntax.labeled_statements -> Identifiers.identifier_set
87
88val gather_mem_vars_stmt : Csyntax.statement -> Identifiers.identifier_set
89
90type var_type =
91| Global of AST.region
92| Stack of Nat.nat
93| Local
94
95val var_type_rect_Type4 :
96  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
97
98val var_type_rect_Type5 :
99  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
100
101val var_type_rect_Type3 :
102  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
103
104val var_type_rect_Type2 :
105  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
106
107val var_type_rect_Type1 :
108  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
109
110val var_type_rect_Type0 :
111  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1
112
113val var_type_inv_rect_Type4 :
114  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
115  'a1) -> 'a1
116
117val var_type_inv_rect_Type3 :
118  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
119  'a1) -> 'a1
120
121val var_type_inv_rect_Type2 :
122  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
123  'a1) -> 'a1
124
125val var_type_inv_rect_Type1 :
126  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
127  'a1) -> 'a1
128
129val var_type_inv_rect_Type0 :
130  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
131  'a1) -> 'a1
132
133val var_type_discr : var_type -> var_type -> __
134
135val var_type_jmdiscr : var_type -> var_type -> __
136
137type var_types =
138  (var_type, Csyntax.type0) Types.prod Identifiers.identifier_map
139
140val lookup' :
141  var_types -> PreIdentifiers.identifier -> (var_type, Csyntax.type0)
142  Types.prod Errors.res
143
144val always_alloc : Csyntax.type0 -> Bool.bool
145
146val characterise_vars :
147  ((AST.ident, AST.region) Types.prod, Csyntax.type0) Types.prod List.list ->
148  Csyntax.function0 -> (var_types, Nat.nat) Types.prod
149
150open FrontEndVal
151
152open Hide
153
154open ByteValues
155
156open GenMem
157
158open FrontEndMem
159
160open Division
161
162open Z
163
164open BitVectorZ
165
166open Pointers
167
168open Values
169
170open FrontEndOps
171
172open Cminor_syntax
173
174val type_should_eq : Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 Errors.res
175
176val region_should_eq : AST.region -> AST.region -> 'a1 -> 'a1 Errors.res
177
178val typ_should_eq : AST.typ -> AST.typ -> 'a1 -> 'a1 Errors.res
179
180val translate_unop :
181  AST.typ -> AST.typ -> Csyntax.unary_operation ->
182  FrontEndOps.unary_operation Errors.res
183
184val fix_ptr_type :
185  Csyntax.type0 -> Nat.nat Types.option -> Cminor_syntax.expr ->
186  Cminor_syntax.expr
187
188val translate_add :
189  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
190  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
191
192val translate_sub :
193  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
194  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
195
196val translate_mul :
197  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
198  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
199
200val translate_div :
201  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
202  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
203
204val translate_mod :
205  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
206  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
207
208val translate_shr :
209  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
210  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
211
212val complete_cmp :
213  Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
214
215val translate_cmp :
216  Integers.comparison -> Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 ->
217  Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
218
219val translate_misc_aop :
220  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> (AST.intsize ->
221  AST.signedness -> FrontEndOps.binary_operation) -> Cminor_syntax.expr ->
222  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res
223
224val translate_binop :
225  Csyntax.binary_operation -> Csyntax.type0 -> Cminor_syntax.expr ->
226  Csyntax.type0 -> Cminor_syntax.expr -> Csyntax.type0 -> Cminor_syntax.expr
227  Errors.res
228
229val translate_cast :
230  Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr Types.sig0 ->
231  Cminor_syntax.expr Types.sig0 Errors.res
232
233val cm_zero : AST.intsize -> AST.signedness -> Cminor_syntax.expr
234
235val cm_one : AST.intsize -> AST.signedness -> Cminor_syntax.expr
236
237val translate_addr :
238  var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res
239
240val translate_expr :
241  var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res
242
243type destination =
244| IdDest of AST.ident * Csyntax.type0
245| MemDest of Cminor_syntax.expr Types.sig0
246
247val destination_rect_Type4 :
248  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
249  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
250
251val destination_rect_Type5 :
252  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
253  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
254
255val destination_rect_Type3 :
256  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
257  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
258
259val destination_rect_Type2 :
260  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
261  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
262
263val destination_rect_Type1 :
264  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
265  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
266
267val destination_rect_Type0 :
268  var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
269  (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1
270
271val destination_inv_rect_Type4 :
272  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
273  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
274
275val destination_inv_rect_Type3 :
276  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
277  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
278
279val destination_inv_rect_Type2 :
280  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
281  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
282
283val destination_inv_rect_Type1 :
284  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
285  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
286
287val destination_inv_rect_Type0 :
288  var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> 'a1)
289  -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1
290
291val destination_discr : var_types -> destination -> destination -> __
292
293val destination_jmdiscr : var_types -> destination -> destination -> __
294
295val translate_dest : var_types -> Csyntax.expr -> __
296
297type lenv = PreIdentifiers.identifier Identifiers.identifier_map
298
299val lookup_label :
300  lenv -> PreIdentifiers.identifier -> PreIdentifiers.identifier Errors.res
301
302type fresh_list_for_univ = __
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 :
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 populate_lenv :
506  AST.ident List.list -> labgen -> lenv -> (lenv Types.sig0, labgen)
507  Types.prod Errors.res
508
509val build_label_env :
510  Csyntax.statement -> (lenv Types.sig0, labgen) Types.prod Errors.res
511
512val translate_function :
513  Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0)
514  Types.prod List.list -> Csyntax.function0 ->
515  Cminor_syntax.internal_function Errors.res
516
517val translate_fundef :
518  Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0)
519  Types.prod List.list -> Csyntax.clight_fundef ->
520  Cminor_syntax.internal_function AST.fundef Errors.res
521
522val map_partial_All :
523  ('a1 -> __ -> 'a2 Errors.res) -> 'a1 List.list -> 'a2 List.list Errors.res
524
525val clight_to_cminor :
526  Csyntax.clight_program -> Cminor_syntax.cminor_program Errors.res
527
Note: See TracBrowser for help on using the repository browser.