source: extracted/compiler.mli @ 2775

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

The compiler now computes also the stack cost model.

File size: 5.7 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
187val front_end :
188  Csyntax.clight_program -> ((CostLabel.costlabel, Csyntax.clight_program)
189  Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res
190
191open State
192
193open Bind_new
194
195open BindLists
196
197open Blocks
198
199open TranslateUtils
200
201open String
202
203open LabelledObjects
204
205open I8051
206
207open BackEndOps
208
209open Joint
210
211open RTL
212
213open RTLabsToRTL
214
215open ERTL
216
217open RegisterSet
218
219open RTLToERTL
220
221open ERTLptr
222
223open ERTLToERTLptr
224
225open Fixpoints
226
227open Set_adt
228
229open Liveness
230
231open Interference
232
233open Joint_LTL_LIN
234
235open LTL
236
237open ERTLptrToLTL
238
239open LIN
240
241open Linearise
242
243open LTLToLIN
244
245open ASM
246
247open BitVectorTrieSet
248
249open LINToASM
250
251val compute_fixpoint : Fixpoints.fixpoint_computer
252
253val colour_graph : Interference.coloured_graph_computer
254
255val back_end :
256  RTLabs_syntax.rTLabs_program -> ((ASM.pseudo_assembly_program,
257  Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res
258
259open Assembly
260
261open Status
262
263open Fetch
264
265open PolicyFront
266
267open PolicyStep
268
269open Policy
270
271val assembler :
272  ASM.pseudo_assembly_program -> ASM.labelled_object_code Errors.res
273
274open AbstractStatus
275
276open StatusProofs
277
278open Interpret
279
280open ASMCosts
281
282val lift_cost_map_back_to_front :
283  Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
284  CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
285  StructuredTraces.as_cost_map -> Label.clight_cost_map
286
287open UtilBranch
288
289open ASMCostsSplit
290
291type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
292                         c_stack_cost : Joint.stack_cost_model;
293                         c_max_stack : Nat.nat;
294                         c_labelled_clight : Csyntax.clight_program;
295                         c_clight_cost_map : Label.clight_cost_map }
296
297val compiler_output_rect_Type4 :
298  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
299  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
300  -> 'a1
301
302val compiler_output_rect_Type5 :
303  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
304  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
305  -> 'a1
306
307val compiler_output_rect_Type3 :
308  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
309  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
310  -> 'a1
311
312val compiler_output_rect_Type2 :
313  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
314  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
315  -> 'a1
316
317val compiler_output_rect_Type1 :
318  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
319  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
320  -> 'a1
321
322val compiler_output_rect_Type0 :
323  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
324  Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
325  -> 'a1
326
327val c_labelled_object_code : compiler_output -> ASM.labelled_object_code
328
329val c_stack_cost : compiler_output -> Joint.stack_cost_model
330
331val c_max_stack : compiler_output -> Nat.nat
332
333val c_labelled_clight : compiler_output -> Csyntax.clight_program
334
335val c_clight_cost_map : compiler_output -> Label.clight_cost_map
336
337val compiler_output_inv_rect_Type4 :
338  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
339  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
340  'a1
341
342val compiler_output_inv_rect_Type3 :
343  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
344  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
345  'a1
346
347val compiler_output_inv_rect_Type2 :
348  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
349  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
350  'a1
351
352val compiler_output_inv_rect_Type1 :
353  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
354  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
355  'a1
356
357val compiler_output_inv_rect_Type0 :
358  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
359  Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
360  'a1
361
362val compiler_output_discr : compiler_output -> compiler_output -> __
363
364val compiler_output_jmdiscr : compiler_output -> compiler_output -> __
365
366val compile : Csyntax.clight_program -> compiler_output Errors.res
367
Note: See TracBrowser for help on using the repository browser.