source: extracted/compiler.mli @ 2951

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

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