source: extracted/toCminor.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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