source: extracted/compiler.ml @ 2904

Last change on this file since 2904 was 2904, checked in by sacerdot, 6 years ago
  1. Algorithm modified by hand to make it run faster. The trusted code needs to be changed once and for all.
  2. pretty-printing code to understand slowness added
File size: 24.5 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
263(** val pass_rect_Type4 :
264    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
265    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
266let rec pass_rect_Type4 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
267| Clight_pass -> h_clight_pass
268| Clight_switch_removed_pass -> h_clight_switch_removed_pass
269| Clight_label_pass -> h_clight_label_pass
270| Clight_simplified_pass -> h_clight_simplified_pass
271| Cminor_pass -> h_cminor_pass
272| Rtlabs_pass -> h_rtlabs_pass
273| Rtl_separate_pass -> h_rtl_separate_pass
274| Rtl_uniq_pass -> h_rtl_uniq_pass
275| Ertl_pass -> h_ertl_pass
276| Ertlptr_pass -> h_ertlptr_pass
277| Ltl_pass -> h_ltl_pass
278| Lin_pass -> h_lin_pass
279| Assembly_pass -> h_assembly_pass
280| Object_code_pass -> h_object_code_pass
281
282(** val pass_rect_Type5 :
283    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
284    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
285let rec pass_rect_Type5 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
286| Clight_pass -> h_clight_pass
287| Clight_switch_removed_pass -> h_clight_switch_removed_pass
288| Clight_label_pass -> h_clight_label_pass
289| Clight_simplified_pass -> h_clight_simplified_pass
290| Cminor_pass -> h_cminor_pass
291| Rtlabs_pass -> h_rtlabs_pass
292| Rtl_separate_pass -> h_rtl_separate_pass
293| Rtl_uniq_pass -> h_rtl_uniq_pass
294| Ertl_pass -> h_ertl_pass
295| Ertlptr_pass -> h_ertlptr_pass
296| Ltl_pass -> h_ltl_pass
297| Lin_pass -> h_lin_pass
298| Assembly_pass -> h_assembly_pass
299| Object_code_pass -> h_object_code_pass
300
301(** val pass_rect_Type3 :
302    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
303    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
304let rec pass_rect_Type3 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
305| Clight_pass -> h_clight_pass
306| Clight_switch_removed_pass -> h_clight_switch_removed_pass
307| Clight_label_pass -> h_clight_label_pass
308| Clight_simplified_pass -> h_clight_simplified_pass
309| Cminor_pass -> h_cminor_pass
310| Rtlabs_pass -> h_rtlabs_pass
311| Rtl_separate_pass -> h_rtl_separate_pass
312| Rtl_uniq_pass -> h_rtl_uniq_pass
313| Ertl_pass -> h_ertl_pass
314| Ertlptr_pass -> h_ertlptr_pass
315| Ltl_pass -> h_ltl_pass
316| Lin_pass -> h_lin_pass
317| Assembly_pass -> h_assembly_pass
318| Object_code_pass -> h_object_code_pass
319
320(** val pass_rect_Type2 :
321    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
322    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
323let rec pass_rect_Type2 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
324| Clight_pass -> h_clight_pass
325| Clight_switch_removed_pass -> h_clight_switch_removed_pass
326| Clight_label_pass -> h_clight_label_pass
327| Clight_simplified_pass -> h_clight_simplified_pass
328| Cminor_pass -> h_cminor_pass
329| Rtlabs_pass -> h_rtlabs_pass
330| Rtl_separate_pass -> h_rtl_separate_pass
331| Rtl_uniq_pass -> h_rtl_uniq_pass
332| Ertl_pass -> h_ertl_pass
333| Ertlptr_pass -> h_ertlptr_pass
334| Ltl_pass -> h_ltl_pass
335| Lin_pass -> h_lin_pass
336| Assembly_pass -> h_assembly_pass
337| Object_code_pass -> h_object_code_pass
338
339(** val pass_rect_Type1 :
340    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
341    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
342let rec pass_rect_Type1 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
343| Clight_pass -> h_clight_pass
344| Clight_switch_removed_pass -> h_clight_switch_removed_pass
345| Clight_label_pass -> h_clight_label_pass
346| Clight_simplified_pass -> h_clight_simplified_pass
347| Cminor_pass -> h_cminor_pass
348| Rtlabs_pass -> h_rtlabs_pass
349| Rtl_separate_pass -> h_rtl_separate_pass
350| Rtl_uniq_pass -> h_rtl_uniq_pass
351| Ertl_pass -> h_ertl_pass
352| Ertlptr_pass -> h_ertlptr_pass
353| Ltl_pass -> h_ltl_pass
354| Lin_pass -> h_lin_pass
355| Assembly_pass -> h_assembly_pass
356| Object_code_pass -> h_object_code_pass
357
358(** val pass_rect_Type0 :
359    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
360    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
361let rec pass_rect_Type0 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ertlptr_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
362| Clight_pass -> h_clight_pass
363| Clight_switch_removed_pass -> h_clight_switch_removed_pass
364| Clight_label_pass -> h_clight_label_pass
365| Clight_simplified_pass -> h_clight_simplified_pass
366| Cminor_pass -> h_cminor_pass
367| Rtlabs_pass -> h_rtlabs_pass
368| Rtl_separate_pass -> h_rtl_separate_pass
369| Rtl_uniq_pass -> h_rtl_uniq_pass
370| Ertl_pass -> h_ertl_pass
371| Ertlptr_pass -> h_ertlptr_pass
372| Ltl_pass -> h_ltl_pass
373| Lin_pass -> h_lin_pass
374| Assembly_pass -> h_assembly_pass
375| Object_code_pass -> h_object_code_pass
376
377(** val pass_inv_rect_Type4 :
378    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
379    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
380    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
381    -> 'a1 **)
382let pass_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
383  let hcut =
384    pass_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
385  in
386  hcut __
387
388(** val pass_inv_rect_Type3 :
389    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
390    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
391    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
392    -> 'a1 **)
393let pass_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
394  let hcut =
395    pass_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
396  in
397  hcut __
398
399(** val pass_inv_rect_Type2 :
400    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
401    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
402    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
403    -> 'a1 **)
404let pass_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
405  let hcut =
406    pass_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
407  in
408  hcut __
409
410(** val pass_inv_rect_Type1 :
411    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
412    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
413    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
414    -> 'a1 **)
415let pass_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
416  let hcut =
417    pass_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
418  in
419  hcut __
420
421(** val pass_inv_rect_Type0 :
422    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
423    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
424    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
425    -> 'a1 **)
426let pass_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
427  let hcut =
428    pass_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
429  in
430  hcut __
431
432(** val pass_discr : pass -> pass -> __ **)
433let pass_discr x y =
434  Logic.eq_rect_Type2 x
435    (match x with
436     | Clight_pass -> Obj.magic (fun _ dH -> dH)
437     | Clight_switch_removed_pass -> Obj.magic (fun _ dH -> dH)
438     | Clight_label_pass -> Obj.magic (fun _ dH -> dH)
439     | Clight_simplified_pass -> Obj.magic (fun _ dH -> dH)
440     | Cminor_pass -> Obj.magic (fun _ dH -> dH)
441     | Rtlabs_pass -> Obj.magic (fun _ dH -> dH)
442     | Rtl_separate_pass -> Obj.magic (fun _ dH -> dH)
443     | Rtl_uniq_pass -> Obj.magic (fun _ dH -> dH)
444     | Ertl_pass -> Obj.magic (fun _ dH -> dH)
445     | Ertlptr_pass -> Obj.magic (fun _ dH -> dH)
446     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
447     | Lin_pass -> Obj.magic (fun _ dH -> dH)
448     | Assembly_pass -> Obj.magic (fun _ dH -> dH)
449     | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y
450
451(** val pass_jmdiscr : pass -> pass -> __ **)
452let pass_jmdiscr x y =
453  Logic.eq_rect_Type2 x
454    (match x with
455     | Clight_pass -> Obj.magic (fun _ dH -> dH)
456     | Clight_switch_removed_pass -> Obj.magic (fun _ dH -> dH)
457     | Clight_label_pass -> Obj.magic (fun _ dH -> dH)
458     | Clight_simplified_pass -> Obj.magic (fun _ dH -> dH)
459     | Cminor_pass -> Obj.magic (fun _ dH -> dH)
460     | Rtlabs_pass -> Obj.magic (fun _ dH -> dH)
461     | Rtl_separate_pass -> Obj.magic (fun _ dH -> dH)
462     | Rtl_uniq_pass -> Obj.magic (fun _ dH -> dH)
463     | Ertl_pass -> Obj.magic (fun _ dH -> dH)
464     | Ertlptr_pass -> Obj.magic (fun _ dH -> dH)
465     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
466     | Lin_pass -> Obj.magic (fun _ dH -> dH)
467     | Assembly_pass -> Obj.magic (fun _ dH -> dH)
468     | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y
469
470type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod
471
472type syntax_of_pass = __
473
474type observe_pass = pass -> syntax_of_pass -> Types.unit0
475
476(** val front_end :
477    observe_pass -> Csyntax.clight_program -> ((CostLabel.costlabel,
478    Csyntax.clight_program) Types.prod, RTLabs_syntax.rTLabs_program)
479    Types.prod Errors.res **)
480let front_end observe p =
481  let i = Obj.magic observe Clight_pass p in
482  let p0 = SwitchRemoval.program_switch_removal p in
483  let i0 = Obj.magic observe Clight_switch_removed_pass p0 in
484  let { Types.fst = p'; Types.snd = init_cost } = Label.clight_label p0 in
485  let i1 = Obj.magic observe Clight_label_pass p' in
486  let p1 = SimplifyCasts.simplify_program p' in
487  let i2 = Obj.magic observe Clight_simplified_pass p1 in
488  Obj.magic
489    (Monad.m_bind0 (Monad.max_def Errors.res0)
490      (Obj.magic (ToCminor.clight_to_cminor p1)) (fun p2 ->
491      let i3 = observe Cminor_pass p2 in
492      let p3 = ToRTLabs.cminor_to_rtlabs init_cost (Obj.magic p2) in
493      let i4 = Obj.magic observe Rtlabs_pass p3 in
494      (match CostCheck.check_cost_program p3 with
495       | Bool.True ->
496         (match CostInj.check_program_cost_injectivity p3 with
497          | Bool.True ->
498            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
499              { Types.fst = init_cost; Types.snd = p' }; Types.snd = p3 }
500          | Bool.False ->
501            Obj.magic (Errors.Error
502              (Errors.msg ErrorMessages.RepeatedCostLabel0)))
503       | Bool.False ->
504         Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadCostLabelling)))))
505
506open Uses
507
508(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
509let compute_fixpoint = Compute_fixpoints.compute_fixpoint
510
511(** val colour_graph : Interference.coloured_graph_computer **)
512let colour_graph = Compute_colouring.colour_graph
513
514open AssocList
515
516(** val lookup_stack_cost :
517    Joint.params -> Joint.joint_program -> PreIdentifiers.identifier ->
518    Nat.nat Types.option **)
519let lookup_stack_cost p p0 id =
520  AssocList.assoc_list_lookup id
521    (Identifiers.eq_identifier PreIdentifiers.SymbolTag)
522    (Joint.stack_cost p p0)
523
524(** val back_end :
525    observe_pass -> RTLabs_syntax.rTLabs_program ->
526    ((ASM.pseudo_assembly_program, Joint.stack_cost_model) Types.prod,
527    Nat.nat) Types.prod Errors.res **)
528let back_end observe p =
529  let p0 = RTLabsToRTL.rtlabs_to_rtl p in
530  let st = lookup_stack_cost (Joint.graph_params_to_params RTL.rTL) p0 in
531  let i =
532    Obj.magic observe Rtl_separate_pass { Types.fst = p0; Types.snd = st }
533  in
534  let i0 = Obj.magic observe Rtl_uniq_pass { Types.fst = p0; Types.snd = st }
535  in
536  let p1 = RTLToERTL.rtl_to_ertl p0 in
537  let st0 = lookup_stack_cost (Joint.graph_params_to_params ERTL.eRTL) p1 in
538  let i1 = Obj.magic observe Ertl_pass { Types.fst = p1; Types.snd = st0 } in
539  let p2 = ERTLToERTLptr.ertl_to_ertlptr p1 in
540  let st1 =
541    lookup_stack_cost (Joint.graph_params_to_params ERTLptr.eRTLptr) p2
542  in
543  let i2 = Obj.magic observe Ertlptr_pass { Types.fst = p2; Types.snd = st1 }
544  in
545  let { Types.fst = eta2; Types.snd = max_stack } =
546    ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
547  in
548  let { Types.fst = p3; Types.snd = stack_cost } = eta2 in
549  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in
550  let i3 = Obj.magic observe Ltl_pass { Types.fst = p3; Types.snd = st2 } in
551  let st3 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in
552  let p4 = LTLToLIN.ltl_to_lin p3 in
553  let st4 = lookup_stack_cost (Joint.lin_params_to_params LIN.lIN) p4 in
554  let i4 = Obj.magic observe Lin_pass { Types.fst = p4; Types.snd = st4 } in
555  Obj.magic
556    (Monad.m_bind0 (Monad.max_def Errors.res0)
557      (Obj.magic
558        (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
559          (LINToASM.lin_to_asm p4))) (fun p5 ->
560      let i5 = observe Assembly_pass p5 in
561      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
562        p5; Types.snd = stack_cost }; Types.snd = max_stack }))
563
564open Assembly
565
566open Status
567
568open Fetch
569
570open PolicyFront
571
572open PolicyStep
573
574open Policy
575
576(** val assembler :
577    observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
578    Errors.res **)
579let assembler observe p =
580prerr_endline "ASSEMBLY0";
581  Obj.magic
582    (Monad.m_bind0 (Monad.max_def Errors.res0)
583      (Obj.magic
584        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
585          (Policy.jump_expansion' p))) (fun sigma_pol ->
586prerr_endline "ASSEMBLY1";
587      let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
588      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
589      let p0 = Assembly.assembly p sigma pol in
590      let i = Obj.magic observe Object_code_pass (Types.pi1 p0) in
591prerr_endline "ASSEMBLY2";
592      Obj.magic (Errors.OK (Types.pi1 p0))))
593
594open AbstractStatus
595
596open StatusProofs
597
598open Interpret
599
600open ASMCosts
601
602(** val lift_cost_map_back_to_front :
603    Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
604    CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
605    StructuredTraces.as_cost_map -> Label.clight_cost_map **)
606let lift_cost_map_back_to_front clight code_memory lbls k asm_cost_map =
607  StructuredTraces.lift_sigma_map_id Nat.O
608    (BitVectorTrie.strong_decidable_in_codomain
609      (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S (Nat.S
610      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
611      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) (Obj.magic lbls))
612    (Obj.magic k) (Obj.magic asm_cost_map)
613
614open UtilBranch
615
616open ASMCostsSplit
617
618type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
619                         c_stack_cost : Joint.stack_cost_model;
620                         c_max_stack : Nat.nat;
621                         c_labelled_clight : Csyntax.clight_program;
622                         c_clight_cost_map : Label.clight_cost_map }
623
624(** val compiler_output_rect_Type4 :
625    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
626    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
627    compiler_output -> 'a1 **)
628let rec compiler_output_rect_Type4 h_mk_compiler_output x_198 =
629  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
630    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
631    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_198
632  in
633  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
634    c_labelled_clight0 c_clight_cost_map0
635
636(** val compiler_output_rect_Type5 :
637    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
638    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
639    compiler_output -> 'a1 **)
640let rec compiler_output_rect_Type5 h_mk_compiler_output x_200 =
641  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
642    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
643    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_200
644  in
645  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
646    c_labelled_clight0 c_clight_cost_map0
647
648(** val compiler_output_rect_Type3 :
649    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
650    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
651    compiler_output -> 'a1 **)
652let rec compiler_output_rect_Type3 h_mk_compiler_output x_202 =
653  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
654    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
655    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_202
656  in
657  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
658    c_labelled_clight0 c_clight_cost_map0
659
660(** val compiler_output_rect_Type2 :
661    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
662    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
663    compiler_output -> 'a1 **)
664let rec compiler_output_rect_Type2 h_mk_compiler_output x_204 =
665  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
666    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
667    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_204
668  in
669  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
670    c_labelled_clight0 c_clight_cost_map0
671
672(** val compiler_output_rect_Type1 :
673    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
674    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
675    compiler_output -> 'a1 **)
676let rec compiler_output_rect_Type1 h_mk_compiler_output x_206 =
677  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
678    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
679    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_206
680  in
681  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
682    c_labelled_clight0 c_clight_cost_map0
683
684(** val compiler_output_rect_Type0 :
685    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
686    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
687    compiler_output -> 'a1 **)
688let rec compiler_output_rect_Type0 h_mk_compiler_output x_208 =
689  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
690    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
691    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_208
692  in
693  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
694    c_labelled_clight0 c_clight_cost_map0
695
696(** val c_labelled_object_code :
697    compiler_output -> ASM.labelled_object_code **)
698let rec c_labelled_object_code xxx =
699  xxx.c_labelled_object_code
700
701(** val c_stack_cost : compiler_output -> Joint.stack_cost_model **)
702let rec c_stack_cost xxx =
703  xxx.c_stack_cost
704
705(** val c_max_stack : compiler_output -> Nat.nat **)
706let rec c_max_stack xxx =
707  xxx.c_max_stack
708
709(** val c_labelled_clight : compiler_output -> Csyntax.clight_program **)
710let rec c_labelled_clight xxx =
711  xxx.c_labelled_clight
712
713(** val c_clight_cost_map : compiler_output -> Label.clight_cost_map **)
714let rec c_clight_cost_map xxx =
715  xxx.c_clight_cost_map
716
717(** val compiler_output_inv_rect_Type4 :
718    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
719    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
720    -> 'a1 **)
721let compiler_output_inv_rect_Type4 hterm h1 =
722  let hcut = compiler_output_rect_Type4 h1 hterm in hcut __
723
724(** val compiler_output_inv_rect_Type3 :
725    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
726    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
727    -> 'a1 **)
728let compiler_output_inv_rect_Type3 hterm h1 =
729  let hcut = compiler_output_rect_Type3 h1 hterm in hcut __
730
731(** val compiler_output_inv_rect_Type2 :
732    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
733    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
734    -> 'a1 **)
735let compiler_output_inv_rect_Type2 hterm h1 =
736  let hcut = compiler_output_rect_Type2 h1 hterm in hcut __
737
738(** val compiler_output_inv_rect_Type1 :
739    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
740    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
741    -> 'a1 **)
742let compiler_output_inv_rect_Type1 hterm h1 =
743  let hcut = compiler_output_rect_Type1 h1 hterm in hcut __
744
745(** val compiler_output_inv_rect_Type0 :
746    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
747    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
748    -> 'a1 **)
749let compiler_output_inv_rect_Type0 hterm h1 =
750  let hcut = compiler_output_rect_Type0 h1 hterm in hcut __
751
752(** val compiler_output_discr : compiler_output -> compiler_output -> __ **)
753let compiler_output_discr x y =
754  Logic.eq_rect_Type2 x
755    (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
756       c_labelled_clight = a3; c_clight_cost_map = a4 } = x
757     in
758    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
759
760(** val compiler_output_jmdiscr :
761    compiler_output -> compiler_output -> __ **)
762let compiler_output_jmdiscr x y =
763  Logic.eq_rect_Type2 x
764    (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
765       c_labelled_clight = a3; c_clight_cost_map = a4 } = x
766     in
767    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
768
769(** val compile :
770    observe_pass -> Csyntax.clight_program -> compiler_output Errors.res **)
771let compile observe p =
772  Obj.magic
773    (Monad.m_bind3 (Monad.max_def Errors.res0)
774      (Obj.magic (front_end observe p)) (fun init_cost p' p0 ->
775      Monad.m_bind3 (Monad.max_def Errors.res0)
776        (Obj.magic (back_end observe p0)) (fun p1 stack_cost max_stack ->
777        Monad.m_bind0 (Monad.max_def Errors.res0)
778          (Obj.magic (assembler observe p1)) (fun p2 ->
779prerr_endline "COMPUTE_COST_MAP";
780          let k = ASMCostsSplit.aSM_cost_map p2 in
781prerr_endline "LIFT_COST_MAP";
782          let k' =
783            lift_cost_map_back_to_front p' (Fetch.load_code_memory p2.ASM.oc)
784              p2.ASM.costlabels k
785          in
786prerr_endline "END";
787          Monad.m_return0 (Monad.max_def Errors.res0)
788            { c_labelled_object_code = p2; c_stack_cost = stack_cost;
789            c_max_stack = max_stack; c_labelled_clight = p';
790            c_clight_cost_map = k' }))))
791
Note: See TracBrowser for help on using the repository browser.