source: extracted/compiler.mli @ 3069

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

New extraction

File size: 8.1 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, Joint.stack_cost_model) Types.prod, Nat.nat)
323  Types.prod Errors.res
324
325open Assembly
326
327open Status
328
329open Fetch
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_labelled_clight : Csyntax.clight_program;
366                         c_clight_cost_map : Label.clight_cost_map }
367
368val compiler_output_rect_Type4 :
369  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
370  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
371  -> 'a1
372
373val compiler_output_rect_Type5 :
374  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
375  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
376  -> 'a1
377
378val compiler_output_rect_Type3 :
379  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
380  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
381  -> 'a1
382
383val compiler_output_rect_Type2 :
384  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
385  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
386  -> 'a1
387
388val compiler_output_rect_Type1 :
389  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
390  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
391  -> 'a1
392
393val compiler_output_rect_Type0 :
394  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
395  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
396  -> 'a1
397
398val c_labelled_object_code : compiler_output -> ASM.labelled_object_code
399
400val c_stack_cost : compiler_output -> Joint.stack_cost_model
401
402val c_max_stack : compiler_output -> Nat.nat
403
404val c_labelled_clight : compiler_output -> Csyntax.clight_program
405
406val c_clight_cost_map : compiler_output -> Label.clight_cost_map
407
408val compiler_output_inv_rect_Type4 :
409  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
410  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
411  'a1
412
413val compiler_output_inv_rect_Type3 :
414  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
415  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
416  'a1
417
418val compiler_output_inv_rect_Type2 :
419  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
420  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
421  'a1
422
423val compiler_output_inv_rect_Type1 :
424  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
425  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
426  'a1
427
428val compiler_output_inv_rect_Type0 :
429  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
430  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
431  'a1
432
433val compiler_output_discr : compiler_output -> compiler_output -> __
434
435val compiler_output_jmdiscr : compiler_output -> compiler_output -> __
436
437val compile :
438  observe_pass -> Csyntax.clight_program -> compiler_output Errors.res
439
Note: See TracBrowser for help on using the repository browser.