source: extracted/compiler.ml @ 2649

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

...

File size: 3.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 Setoids
22
23open Monad
24
25open Option
26
27open Lists
28
29open Positive
30
31open Identifiers
32
33open Arithmetic
34
35open Vector
36
37open Div_and_mod
38
39open Jmeq
40
41open Russell
42
43open List
44
45open Util
46
47open FoldStuff
48
49open BitVector
50
51open Extranat
52
53open Bool
54
55open Relations
56
57open Nat
58
59open Integers
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Types
70
71open AST
72
73open Csyntax
74
75open Label
76
77open Sets
78
79open Listb
80
81open Star
82
83open Frontend_misc
84
85open CexecInd
86
87open CexecSound
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 Initialisation
150
151open BitVectorTrie
152
153open Graphs
154
155open Order
156
157open Registers
158
159open RTLabs_syntax
160
161open ToRTLabs
162
163(** val front_end :
164    Csyntax.clight_program -> ((CostLabel.costlabel, Csyntax.clight_program)
165    Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res **)
166let front_end p =
167  let p0 = SwitchRemoval.program_switch_removal p in
168  let { Types.fst = p'; Types.snd = init_cost } = Label.clight_label p0 in
169  let p3 = SimplifyCasts.simplify_program p' in
170  Obj.magic
171    (Monad.m_bind0 (Monad.max_def Errors.res0)
172      (Obj.magic (ToCminor.clight_to_cminor p3)) (fun p4 ->
173      let p5 = ToRTLabs.cminor_to_rtlabs init_cost p4 in
174      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
175        init_cost; Types.snd = p' }; Types.snd = p5 }))
176
177open String
178
179open LabelledObjects
180
181open ASM
182
183(** val back_end :
184    RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program **)
185let back_end x =
186  failwith "AXIOM TO BE REALIZED"
187
188type object_code = BitVector.byte List.list
189
190type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
191
192(** val assembler :
193    ASM.pseudo_assembly_program -> (object_code, costlabel_map) Types.prod
194    Errors.res **)
195let assembler x =
196  failwith "AXIOM TO BE REALIZED"
197
198open StructuredTraces
199
200open AbstractStatus
201
202open Status
203
204open StatusProofs
205
206open Interpret
207
208open Fetch
209
210open ASMCosts
211
212(** val lift_cost_map_back_to_front :
213    Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
214    CostLabel.costlabel BitVectorTrie.bitVectorTrie -> (CostLabel.costlabel
215    -> (__, __) Types.sum) -> StructuredTraces.as_cost_map ->
216    Label.clight_cost_map **)
217let lift_cost_map_back_to_front clight code_memory lbls dec k asm_cost_map =
218  StructuredTraces.lift_sigma_map_id Nat.O dec k asm_cost_map
219
220open UtilBranch
221
222open ASMCostsSplit
223
224(** val compile :
225    Csyntax.clight_program -> ((object_code, costlabel_map) Types.prod,
226    (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
227    Errors.res **)
228let compile p =
229  Obj.magic
230    (Monad.m_bind3 (Monad.max_def Errors.res0) (Obj.magic (front_end p))
231      (fun init_cost p' p0 ->
232      let p3 = back_end p0 in
233      Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p3))
234        (fun p4 ->
235        let k = ASMCostsSplit.aSM_cost_map p4 in
236        let k' =
237          lift_cost_map_back_to_front p'
238            (Fetch.load_code_memory p4.Types.fst) p4.Types.snd (assert false
239            (* absurd case *)) k
240        in
241        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = p4;
242          Types.snd = { Types.dpi1 = p'; Types.dpi2 = k' } })))
243
Note: See TracBrowser for help on using the repository browser.