source: extracted/compiler.mli @ 2890

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

Pretty printing of object code integrated too.
A couple of axioms make execution via the preclassified_system
raise assert false.

File size: 8.4 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 Initialisation
152
153open BitVectorTrie
154
155open Graphs
156
157open Order
158
159open Registers
160
161open RTLabs_syntax
162
163open ToRTLabs
164
165open Deqsets_extra
166
167open CostMisc
168
169open Listb_extra
170
171open CostSpec
172
173open CostCheck
174
175open Executions
176
177open StructuredTraces
178
179open RTLabs_semantics
180
181open RTLabs_abstract
182
183open RTLabs_traces
184
185open CostInj
186
187open State
188
189open Bind_new
190
191open BindLists
192
193open Blocks
194
195open TranslateUtils
196
197open String
198
199open LabelledObjects
200
201open I8051
202
203open BackEndOps
204
205open Joint
206
207open RTL
208
209open RTLabsToRTL
210
211open ERTL
212
213open RegisterSet
214
215open RTLToERTL
216
217open ERTLptr
218
219open ERTLToERTLptr
220
221open Fixpoints
222
223open Set_adt
224
225open Liveness
226
227open Interference
228
229open Joint_LTL_LIN
230
231open LTL
232
233open ERTLptrToLTL
234
235open LIN
236
237open Linearise
238
239open LTLToLIN
240
241open ASM
242
243open BitVectorTrieSet
244
245open LINToASM
246
247type pass =
248| Clight_pass
249| Clight_switch_removed_pass
250| Clight_label_pass
251| Clight_simplified_pass
252| Cminor_pass
253| Rtlabs_pass
254| Rtl_separate_pass
255| Rtl_uniq_pass
256| Ertl_pass
257| Ertlptr_pass
258| Ltl_pass
259| Lin_pass
260| Assembly_pass
261| Object_code_pass
262
263val pass_rect_Type4 :
264  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
265  -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
266
267val pass_rect_Type5 :
268  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
269  -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
270
271val pass_rect_Type3 :
272  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
273  -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
274
275val pass_rect_Type2 :
276  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
277  -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
278
279val pass_rect_Type1 :
280  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
281  -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
282
283val pass_rect_Type0 :
284  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
285  -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
286
287val pass_inv_rect_Type4 :
288  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
289  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
290  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
291
292val pass_inv_rect_Type3 :
293  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
294  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
295  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
296
297val pass_inv_rect_Type2 :
298  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
299  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
300  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
301
302val pass_inv_rect_Type1 :
303  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
304  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
305  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
306
307val pass_inv_rect_Type0 :
308  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
309  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
310  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
311
312val pass_discr : pass -> pass -> __
313
314val pass_jmdiscr : pass -> pass -> __
315
316type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod
317
318type syntax_of_pass = __
319
320type observe_pass = pass -> syntax_of_pass -> Types.unit0
321
322val front_end :
323  observe_pass -> Csyntax.clight_program -> ((CostLabel.costlabel,
324  Csyntax.clight_program) Types.prod, RTLabs_syntax.rTLabs_program)
325  Types.prod Errors.res
326
327open Uses
328
329val compute_fixpoint : Fixpoints.fixpoint_computer
330
331val colour_graph : Interference.coloured_graph_computer
332
333open AssocList
334
335val lookup_stack_cost :
336  Joint.params -> Joint.joint_program -> PreIdentifiers.identifier -> Nat.nat
337  Types.option
338
339val back_end :
340  observe_pass -> RTLabs_syntax.rTLabs_program ->
341  ((ASM.pseudo_assembly_program, Joint.stack_cost_model) Types.prod, Nat.nat)
342  Types.prod Errors.res
343
344open Assembly
345
346open Status
347
348open Fetch
349
350open PolicyFront
351
352open PolicyStep
353
354open Policy
355
356val assembler :
357  observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
358  Errors.res
359
360open AbstractStatus
361
362open StatusProofs
363
364open Interpret
365
366open ASMCosts
367
368val lift_cost_map_back_to_front :
369  Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
370  CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
371  StructuredTraces.as_cost_map -> Label.clight_cost_map
372
373open UtilBranch
374
375open ASMCostsSplit
376
377type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
378                         c_stack_cost : Joint.stack_cost_model;
379                         c_max_stack : Nat.nat;
380                         c_labelled_clight : Csyntax.clight_program;
381                         c_clight_cost_map : Label.clight_cost_map }
382
383val compiler_output_rect_Type4 :
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_Type5 :
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_Type3 :
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 compiler_output_rect_Type2 :
399  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
400  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
401  -> 'a1
402
403val compiler_output_rect_Type1 :
404  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
405  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
406  -> 'a1
407
408val compiler_output_rect_Type0 :
409  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
410  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
411  -> 'a1
412
413val c_labelled_object_code : compiler_output -> ASM.labelled_object_code
414
415val c_stack_cost : compiler_output -> Joint.stack_cost_model
416
417val c_max_stack : compiler_output -> Nat.nat
418
419val c_labelled_clight : compiler_output -> Csyntax.clight_program
420
421val c_clight_cost_map : compiler_output -> Label.clight_cost_map
422
423val compiler_output_inv_rect_Type4 :
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_Type3 :
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_inv_rect_Type2 :
434  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
435  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
436  'a1
437
438val compiler_output_inv_rect_Type1 :
439  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
440  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
441  'a1
442
443val compiler_output_inv_rect_Type0 :
444  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
445  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
446  'a1
447
448val compiler_output_discr : compiler_output -> compiler_output -> __
449
450val compiler_output_jmdiscr : compiler_output -> compiler_output -> __
451
452val compile :
453  observe_pass -> Csyntax.clight_program -> compiler_output Errors.res
454
Note: See TracBrowser for help on using the repository browser.