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
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 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
149open BitVectorTrie
150
151open Graphs
152
153open Order
154
155open Registers
156
157open RTLabs_syntax
158
159open ToRTLabs
160
161open Deqsets_extra
162
163open CostMisc
164
165open Listb_extra
166
167open CostSpec
168
169open CostCheck
170
171open CostInj
172
173open State
174
175open Bind_new
176
177open BindLists
178
179open Blocks
180
181open TranslateUtils
182
183open String
184
185open LabelledObjects
186
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
215open ERTLToLTL
216
217open LIN
218
219open Linearise
220
221open LTLToLIN
222
223open ASM
224
225open BitVectorTrieSet
226
227open LINToASM
228
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
241| Assembly_pass
242| Object_code_pass
243
244val pass_rect_Type4 :
245  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
246  -> 'a1 -> 'a1 -> pass -> 'a1
247
248val pass_rect_Type5 :
249  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
250  -> 'a1 -> 'a1 -> pass -> 'a1
251
252val pass_rect_Type3 :
253  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
254  -> 'a1 -> 'a1 -> pass -> 'a1
255
256val pass_rect_Type2 :
257  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
258  -> 'a1 -> 'a1 -> pass -> 'a1
259
260val pass_rect_Type1 :
261  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
262  -> 'a1 -> 'a1 -> pass -> 'a1
263
264val pass_rect_Type0 :
265  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
266  -> 'a1 -> 'a1 -> pass -> 'a1
267
268val pass_inv_rect_Type4 :
269  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
270  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
271  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
272
273val pass_inv_rect_Type3 :
274  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
275  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
276  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
277
278val pass_inv_rect_Type2 :
279  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
280  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
281  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
282
283val pass_inv_rect_Type1 :
284  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
285  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
286  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
287
288val pass_inv_rect_Type0 :
289  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
290  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
291  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
292
293val pass_discr : pass -> pass -> __
294
295val pass_jmdiscr : pass -> pass -> __
296
297type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod
298
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
308open Uses
309
310val compute_fixpoint : Fixpoints.fixpoint_computer
311
312val colour_graph : Interference.coloured_graph_computer
313
314open AssocList
315
316val lookup_stack_cost :
317  Joint.params -> Joint.joint_program -> PreIdentifiers.identifier -> Nat.nat
318  Types.option
319
320val back_end :
321  observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
322  (((ASM.pseudo_assembly_program, CostLabel.costlabel) Types.prod,
323  Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res
324
325open Status
326
327open Fetch
328
329open Assembly
330
331open PolicyFront
332
333open PolicyStep
334
335open Policy
336
337val assembler :
338  observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
339  Errors.res
340
341open StructuredTraces
342
343open AbstractStatus
344
345open StatusProofs
346
347open Interpret
348
349open ASMCosts
350
351val lift_out_of_sigma :
352  'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1 -> 'a2
353
354val lift_cost_map_back_to_front :
355  ASM.labelled_object_code -> StructuredTraces.as_cost_map ->
356  Label.clight_cost_map
357
358open UtilBranch
359
360open ASMCostsSplit
361
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;
365                         c_init_costlabel : CostLabel.costlabel;
366                         c_labelled_clight : Csyntax.clight_program;
367                         c_clight_cost_map : Label.clight_cost_map }
368
369val compiler_output_rect_Type4 :
370  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
371  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
372  'a1) -> compiler_output -> 'a1
373
374val compiler_output_rect_Type5 :
375  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
376  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
377  'a1) -> compiler_output -> 'a1
378
379val compiler_output_rect_Type3 :
380  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
381  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
382  'a1) -> compiler_output -> 'a1
383
384val compiler_output_rect_Type2 :
385  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
386  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
387  'a1) -> compiler_output -> 'a1
388
389val compiler_output_rect_Type1 :
390  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
391  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
392  'a1) -> compiler_output -> 'a1
393
394val compiler_output_rect_Type0 :
395  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
396  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
397  'a1) -> compiler_output -> 'a1
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
405val c_init_costlabel : compiler_output -> CostLabel.costlabel
406
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 ->
413  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
414  Label.clight_cost_map -> __ -> 'a1) -> 'a1
415
416val compiler_output_inv_rect_Type3 :
417  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
418  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
419  Label.clight_cost_map -> __ -> 'a1) -> 'a1
420
421val compiler_output_inv_rect_Type2 :
422  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
423  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
424  Label.clight_cost_map -> __ -> 'a1) -> 'a1
425
426val compiler_output_inv_rect_Type1 :
427  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
428  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
429  Label.clight_cost_map -> __ -> 'a1) -> 'a1
430
431val compiler_output_inv_rect_Type0 :
432  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
433  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
434  Label.clight_cost_map -> __ -> 'a1) -> 'a1
435
436val compiler_output_jmdiscr : compiler_output -> compiler_output -> __
437
438val compile :
439  observe_pass -> Csyntax.clight_program -> compiler_output Errors.res
440
Note: See TracBrowser for help on using the repository browser.