source: driver/extracted/compiler.mli @ 3106

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

New extraction.

File size: 8.5 KB
RevLine 
[2601]1open Preamble
2
3open CostLabel
4
[2649]5open Coqlib
6
[2601]7open Proper
8
9open PositiveMap
10
11open Deqsets
12
[2649]13open ErrorMessages
14
[2601]15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
[2717]27open Exp
28
[2601]29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
[2773]35open Util
36
37open FoldStuff
38
39open BitVector
40
[2601]41open Jmeq
42
43open Russell
44
45open List
46
[2773]47open Setoids
[2601]48
[2773]49open Monad
[2601]50
[2773]51open Option
[2601]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 Label
78
79open Sets
80
81open Listb
82
83open Star
84
85open Frontend_misc
86
87open CexecInd
88
89open Casts
90
91open ClassifyOp
92
93open Smallstep
94
95open Extra_bool
96
97open FrontEndVal
98
99open Hide
100
101open ByteValues
102
103open GenMem
104
105open FrontEndMem
106
107open Globalenvs
108
109open Csem
110
111open SmallstepExec
112
113open Division
114
115open Z
116
117open BitVectorZ
118
119open Pointers
120
121open Values
122
123open Events
124
125open IOMonad
126
127open IO
128
129open Cexec
130
131open TypeComparison
132
133open SimplifyCasts
134
135open MemProperties
136
137open MemoryInjections
138
139open Fresh
140
141open SwitchRemoval
142
143open FrontEndOps
144
145open Cminor_syntax
146
147open ToCminor
148
[2773]149open BitVectorTrie
150
[2601]151open Graphs
152
153open Order
154
155open Registers
156
157open RTLabs_syntax
158
159open ToRTLabs
160
[2730]161open Deqsets_extra
162
163open CostMisc
164
[2743]165open Listb_extra
[2730]166
167open CostSpec
168
169open CostCheck
170
171open CostInj
172
[2717]173open State
174
175open Bind_new
176
177open BindLists
178
179open Blocks
180
181open TranslateUtils
182
[2649]183open String
184
[2601]185open LabelledObjects
186
[2717]187open I8051
188
189open BackEndOps
190
191open Joint
192
193open RTL
194
195open RTLabsToRTL
196
197open ERTL
198
199open RegisterSet
200
201open RTLToERTL
202
203open Fixpoints
204
205open Set_adt
206
207open Liveness
208
209open Interference
210
211open Joint_LTL_LIN
212
213open LTL
214
[3019]215open ERTLToLTL
[2717]216
217open LIN
218
219open Linearise
220
221open LTLToLIN
222
[2601]223open ASM
224
[2717]225open BitVectorTrieSet
226
227open LINToASM
228
[2829]229type pass =
230| Clight_pass
231| Clight_switch_removed_pass
232| Clight_label_pass
233| Clight_simplified_pass
234| Cminor_pass
235| Rtlabs_pass
236| Rtl_separate_pass
237| Rtl_uniq_pass
238| Ertl_pass
239| Ltl_pass
240| Lin_pass
[2875]241| Assembly_pass
242| Object_code_pass
[2829]243
244val pass_rect_Type4 :
245  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
[3019]246  -> 'a1 -> 'a1 -> pass -> 'a1
[2829]247
248val pass_rect_Type5 :
249  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
[3019]250  -> 'a1 -> 'a1 -> pass -> 'a1
[2829]251
252val pass_rect_Type3 :
253  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
[3019]254  -> 'a1 -> 'a1 -> pass -> 'a1
[2829]255
256val pass_rect_Type2 :
257  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
[3019]258  -> 'a1 -> 'a1 -> pass -> 'a1
[2829]259
260val pass_rect_Type1 :
261  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
[3019]262  -> 'a1 -> 'a1 -> pass -> 'a1
[2829]263
264val pass_rect_Type0 :
265  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
[3019]266  -> 'a1 -> 'a1 -> pass -> 'a1
[2829]267
268val pass_inv_rect_Type4 :
269  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
270  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
[3019]271  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
[2829]272
273val pass_inv_rect_Type3 :
274  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
275  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
[3019]276  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
[2829]277
278val pass_inv_rect_Type2 :
279  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
280  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
[3019]281  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
[2829]282
283val pass_inv_rect_Type1 :
284  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
285  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
[3019]286  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
[2829]287
288val pass_inv_rect_Type0 :
289  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
290  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
[3019]291  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
[2829]292
293val pass_discr : pass -> pass -> __
294
295val pass_jmdiscr : pass -> pass -> __
296
[2842]297type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod
298
[2829]299type syntax_of_pass = __
300
301type observe_pass = pass -> syntax_of_pass -> Types.unit0
302
303val front_end :
304  observe_pass -> Csyntax.clight_program -> ((CostLabel.costlabel,
305  Csyntax.clight_program) Types.prod, RTLabs_syntax.rTLabs_program)
306  Types.prod Errors.res
307
[2842]308open Uses
309
[2717]310val compute_fixpoint : Fixpoints.fixpoint_computer
311
312val colour_graph : Interference.coloured_graph_computer
313
[2842]314open AssocList
315
316val lookup_stack_cost :
317  Joint.params -> Joint.joint_program -> PreIdentifiers.identifier -> Nat.nat
318  Types.option
319
[2773]320val back_end :
[2951]321  observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
[3083]322  (((ASM.pseudo_assembly_program, CostLabel.costlabel) Types.prod,
323  Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res
[2601]324
[2717]325open Status
326
327open Fetch
328
[3106]329open Assembly
330
[2717]331open PolicyFront
332
333open PolicyStep
334
335open Policy
336
[2601]337val assembler :
[2875]338  observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
339  Errors.res
[2601]340
[2951]341open StructuredTraces
342
[2601]343open AbstractStatus
344
345open StatusProofs
346
347open Interpret
348
349open ASMCosts
350
[3043]351val lift_out_of_sigma :
352  'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1 -> 'a2
353
[2601]354val lift_cost_map_back_to_front :
[3043]355  ASM.labelled_object_code -> StructuredTraces.as_cost_map ->
356  Label.clight_cost_map
[2601]357
358open UtilBranch
359
360open ASMCostsSplit
361
[2775]362type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
363                         c_stack_cost : Joint.stack_cost_model;
364                         c_max_stack : Nat.nat;
[3083]365                         c_init_costlabel : CostLabel.costlabel;
[2775]366                         c_labelled_clight : Csyntax.clight_program;
367                         c_clight_cost_map : Label.clight_cost_map }
[2601]368
[2775]369val compiler_output_rect_Type4 :
370  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
[3083]371  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
372  'a1) -> compiler_output -> 'a1
[2775]373
374val compiler_output_rect_Type5 :
375  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
[3083]376  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
377  'a1) -> compiler_output -> 'a1
[2775]378
379val compiler_output_rect_Type3 :
380  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
[3083]381  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
382  'a1) -> compiler_output -> 'a1
[2775]383
384val compiler_output_rect_Type2 :
385  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
[3083]386  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
387  'a1) -> compiler_output -> 'a1
[2775]388
389val compiler_output_rect_Type1 :
390  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
[3083]391  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
392  'a1) -> compiler_output -> 'a1
[2775]393
394val compiler_output_rect_Type0 :
395  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
[3083]396  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
397  'a1) -> compiler_output -> 'a1
[2775]398
399val c_labelled_object_code : compiler_output -> ASM.labelled_object_code
400
401val c_stack_cost : compiler_output -> Joint.stack_cost_model
402
403val c_max_stack : compiler_output -> Nat.nat
404
[3083]405val c_init_costlabel : compiler_output -> CostLabel.costlabel
406
[2775]407val c_labelled_clight : compiler_output -> Csyntax.clight_program
408
409val c_clight_cost_map : compiler_output -> Label.clight_cost_map
410
411val compiler_output_inv_rect_Type4 :
412  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
[3083]413  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
414  Label.clight_cost_map -> __ -> 'a1) -> 'a1
[2775]415
416val compiler_output_inv_rect_Type3 :
417  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
[3083]418  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
419  Label.clight_cost_map -> __ -> 'a1) -> 'a1
[2775]420
421val compiler_output_inv_rect_Type2 :
422  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
[3083]423  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
424  Label.clight_cost_map -> __ -> 'a1) -> 'a1
[2775]425
426val compiler_output_inv_rect_Type1 :
427  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
[3083]428  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
429  Label.clight_cost_map -> __ -> 'a1) -> 'a1
[2775]430
431val compiler_output_inv_rect_Type0 :
432  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
[3083]433  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
434  Label.clight_cost_map -> __ -> 'a1) -> 'a1
[2775]435
436val compiler_output_jmdiscr : compiler_output -> compiler_output -> __
437
[2829]438val compile :
439  observe_pass -> Csyntax.clight_program -> compiler_output Errors.res
[2775]440
Note: See TracBrowser for help on using the repository browser.