source: extracted/compiler.ml @ 3069

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

New extraction

File size: 23.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 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 BitVectorTrie
150
151open Graphs
152
153open Order
154
155open Registers
156
157open RTLabs_syntax
158
159open ToRTLabs
160
161open Deqsets_extra
162
163open CostMisc
164
165open Listb_extra
166
167open CostSpec
168
169open CostCheck
170
171open CostInj
172
173open State
174
175open Bind_new
176
177open BindLists
178
179open Blocks
180
181open TranslateUtils
182
183open String
184
185open LabelledObjects
186
187open I8051
188
189open BackEndOps
190
191open Joint
192
193open RTL
194
195open RTLabsToRTL
196
197open ERTL
198
199open RegisterSet
200
201open RTLToERTL
202
203open Fixpoints
204
205open Set_adt
206
207open Liveness
208
209open Interference
210
211open Joint_LTL_LIN
212
213open LTL
214
215open ERTLToLTL
216
217open LIN
218
219open Linearise
220
221open LTLToLIN
222
223open ASM
224
225open BitVectorTrieSet
226
227open LINToASM
228
229type pass =
230| Clight_pass
231| Clight_switch_removed_pass
232| Clight_label_pass
233| Clight_simplified_pass
234| Cminor_pass
235| Rtlabs_pass
236| Rtl_separate_pass
237| Rtl_uniq_pass
238| Ertl_pass
239| Ltl_pass
240| Lin_pass
241| Assembly_pass
242| Object_code_pass
243
244(** val pass_rect_Type4 :
245    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
246    -> 'a1 -> 'a1 -> pass -> 'a1 **)
247let 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_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
248| Clight_pass -> h_clight_pass
249| Clight_switch_removed_pass -> h_clight_switch_removed_pass
250| Clight_label_pass -> h_clight_label_pass
251| Clight_simplified_pass -> h_clight_simplified_pass
252| Cminor_pass -> h_cminor_pass
253| Rtlabs_pass -> h_rtlabs_pass
254| Rtl_separate_pass -> h_rtl_separate_pass
255| Rtl_uniq_pass -> h_rtl_uniq_pass
256| Ertl_pass -> h_ertl_pass
257| Ltl_pass -> h_ltl_pass
258| Lin_pass -> h_lin_pass
259| Assembly_pass -> h_assembly_pass
260| Object_code_pass -> h_object_code_pass
261
262(** val pass_rect_Type5 :
263    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
264    -> 'a1 -> 'a1 -> pass -> 'a1 **)
265let 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_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
266| Clight_pass -> h_clight_pass
267| Clight_switch_removed_pass -> h_clight_switch_removed_pass
268| Clight_label_pass -> h_clight_label_pass
269| Clight_simplified_pass -> h_clight_simplified_pass
270| Cminor_pass -> h_cminor_pass
271| Rtlabs_pass -> h_rtlabs_pass
272| Rtl_separate_pass -> h_rtl_separate_pass
273| Rtl_uniq_pass -> h_rtl_uniq_pass
274| Ertl_pass -> h_ertl_pass
275| Ltl_pass -> h_ltl_pass
276| Lin_pass -> h_lin_pass
277| Assembly_pass -> h_assembly_pass
278| Object_code_pass -> h_object_code_pass
279
280(** val pass_rect_Type3 :
281    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
282    -> 'a1 -> 'a1 -> pass -> 'a1 **)
283let 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_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
284| Clight_pass -> h_clight_pass
285| Clight_switch_removed_pass -> h_clight_switch_removed_pass
286| Clight_label_pass -> h_clight_label_pass
287| Clight_simplified_pass -> h_clight_simplified_pass
288| Cminor_pass -> h_cminor_pass
289| Rtlabs_pass -> h_rtlabs_pass
290| Rtl_separate_pass -> h_rtl_separate_pass
291| Rtl_uniq_pass -> h_rtl_uniq_pass
292| Ertl_pass -> h_ertl_pass
293| Ltl_pass -> h_ltl_pass
294| Lin_pass -> h_lin_pass
295| Assembly_pass -> h_assembly_pass
296| Object_code_pass -> h_object_code_pass
297
298(** val pass_rect_Type2 :
299    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
300    -> 'a1 -> 'a1 -> pass -> 'a1 **)
301let 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_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
302| Clight_pass -> h_clight_pass
303| Clight_switch_removed_pass -> h_clight_switch_removed_pass
304| Clight_label_pass -> h_clight_label_pass
305| Clight_simplified_pass -> h_clight_simplified_pass
306| Cminor_pass -> h_cminor_pass
307| Rtlabs_pass -> h_rtlabs_pass
308| Rtl_separate_pass -> h_rtl_separate_pass
309| Rtl_uniq_pass -> h_rtl_uniq_pass
310| Ertl_pass -> h_ertl_pass
311| Ltl_pass -> h_ltl_pass
312| Lin_pass -> h_lin_pass
313| Assembly_pass -> h_assembly_pass
314| Object_code_pass -> h_object_code_pass
315
316(** val pass_rect_Type1 :
317    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
318    -> 'a1 -> 'a1 -> pass -> 'a1 **)
319let 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_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
320| Clight_pass -> h_clight_pass
321| Clight_switch_removed_pass -> h_clight_switch_removed_pass
322| Clight_label_pass -> h_clight_label_pass
323| Clight_simplified_pass -> h_clight_simplified_pass
324| Cminor_pass -> h_cminor_pass
325| Rtlabs_pass -> h_rtlabs_pass
326| Rtl_separate_pass -> h_rtl_separate_pass
327| Rtl_uniq_pass -> h_rtl_uniq_pass
328| Ertl_pass -> h_ertl_pass
329| Ltl_pass -> h_ltl_pass
330| Lin_pass -> h_lin_pass
331| Assembly_pass -> h_assembly_pass
332| Object_code_pass -> h_object_code_pass
333
334(** val pass_rect_Type0 :
335    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
336    -> 'a1 -> 'a1 -> pass -> 'a1 **)
337let 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_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
338| Clight_pass -> h_clight_pass
339| Clight_switch_removed_pass -> h_clight_switch_removed_pass
340| Clight_label_pass -> h_clight_label_pass
341| Clight_simplified_pass -> h_clight_simplified_pass
342| Cminor_pass -> h_cminor_pass
343| Rtlabs_pass -> h_rtlabs_pass
344| Rtl_separate_pass -> h_rtl_separate_pass
345| Rtl_uniq_pass -> h_rtl_uniq_pass
346| Ertl_pass -> h_ertl_pass
347| Ltl_pass -> h_ltl_pass
348| Lin_pass -> h_lin_pass
349| Assembly_pass -> h_assembly_pass
350| Object_code_pass -> h_object_code_pass
351
352(** val pass_inv_rect_Type4 :
353    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
354    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
355    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
356let pass_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
357  let hcut = pass_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
358  in
359  hcut __
360
361(** val pass_inv_rect_Type3 :
362    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
363    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
364    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
365let pass_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
366  let hcut = pass_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
367  in
368  hcut __
369
370(** val pass_inv_rect_Type2 :
371    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
372    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
373    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
374let pass_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
375  let hcut = pass_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
376  in
377  hcut __
378
379(** val pass_inv_rect_Type1 :
380    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
381    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
382    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
383let pass_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
384  let hcut = pass_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
385  in
386  hcut __
387
388(** val pass_inv_rect_Type0 :
389    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
390    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
391    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
392let pass_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
393  let hcut = pass_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
394  in
395  hcut __
396
397(** val pass_discr : pass -> pass -> __ **)
398let pass_discr x y =
399  Logic.eq_rect_Type2 x
400    (match x with
401     | Clight_pass -> Obj.magic (fun _ dH -> dH)
402     | Clight_switch_removed_pass -> Obj.magic (fun _ dH -> dH)
403     | Clight_label_pass -> Obj.magic (fun _ dH -> dH)
404     | Clight_simplified_pass -> Obj.magic (fun _ dH -> dH)
405     | Cminor_pass -> Obj.magic (fun _ dH -> dH)
406     | Rtlabs_pass -> Obj.magic (fun _ dH -> dH)
407     | Rtl_separate_pass -> Obj.magic (fun _ dH -> dH)
408     | Rtl_uniq_pass -> Obj.magic (fun _ dH -> dH)
409     | Ertl_pass -> Obj.magic (fun _ dH -> dH)
410     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
411     | Lin_pass -> Obj.magic (fun _ dH -> dH)
412     | Assembly_pass -> Obj.magic (fun _ dH -> dH)
413     | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y
414
415(** val pass_jmdiscr : pass -> pass -> __ **)
416let pass_jmdiscr x y =
417  Logic.eq_rect_Type2 x
418    (match x with
419     | Clight_pass -> Obj.magic (fun _ dH -> dH)
420     | Clight_switch_removed_pass -> Obj.magic (fun _ dH -> dH)
421     | Clight_label_pass -> Obj.magic (fun _ dH -> dH)
422     | Clight_simplified_pass -> Obj.magic (fun _ dH -> dH)
423     | Cminor_pass -> Obj.magic (fun _ dH -> dH)
424     | Rtlabs_pass -> Obj.magic (fun _ dH -> dH)
425     | Rtl_separate_pass -> Obj.magic (fun _ dH -> dH)
426     | Rtl_uniq_pass -> Obj.magic (fun _ dH -> dH)
427     | Ertl_pass -> Obj.magic (fun _ dH -> dH)
428     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
429     | Lin_pass -> Obj.magic (fun _ dH -> dH)
430     | Assembly_pass -> Obj.magic (fun _ dH -> dH)
431     | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y
432
433type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod
434
435type syntax_of_pass = __
436
437type observe_pass = pass -> syntax_of_pass -> Types.unit0
438
439(** val front_end :
440    observe_pass -> Csyntax.clight_program -> ((CostLabel.costlabel,
441    Csyntax.clight_program) Types.prod, RTLabs_syntax.rTLabs_program)
442    Types.prod Errors.res **)
443let front_end observe p =
444  let i = Obj.magic observe Clight_pass p in
445  let p0 = SwitchRemoval.program_switch_removal p in
446  let i0 = Obj.magic observe Clight_switch_removed_pass p0 in
447  let { Types.fst = p'; Types.snd = init_cost } = Label.clight_label p0 in
448  let i1 = Obj.magic observe Clight_label_pass p' in
449  let p1 = SimplifyCasts.simplify_program p' in
450  let i2 = Obj.magic observe Clight_simplified_pass p1 in
451  Obj.magic
452    (Monad.m_bind0 (Monad.max_def Errors.res0)
453      (Obj.magic (ToCminor.clight_to_cminor p1)) (fun p2 ->
454      let i3 = observe Cminor_pass p2 in
455      let p3 = ToRTLabs.cminor_to_rtlabs (Obj.magic p2) in
456      let i4 = Obj.magic observe Rtlabs_pass p3 in
457      Monad.m_bind0 (Monad.max_def Errors.res0)
458        (Obj.magic (CostCheck.check_cost_program_prf p3)) (fun _ ->
459        Monad.m_bind0 (Monad.max_def Errors.res0)
460          (Obj.magic (CostInj.check_program_cost_injectivity_prf p3))
461          (fun _ ->
462          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
463            { Types.fst = init_cost; Types.snd = p' }; Types.snd = p3 }))))
464
465open Uses
466
467(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
468let compute_fixpoint = Compute_fixpoints.compute_fixpoint
469 
470(** val colour_graph : Interference.coloured_graph_computer **)
471let colour_graph = Compute_colouring.colour_graph
472 
473
474
475open AssocList
476
477(** val lookup_stack_cost :
478    Joint.params -> Joint.joint_program -> PreIdentifiers.identifier ->
479    Nat.nat Types.option **)
480let lookup_stack_cost p p0 id =
481  AssocList.assoc_list_lookup id
482    (Identifiers.eq_identifier PreIdentifiers.SymbolTag)
483    (Joint.stack_cost p p0)
484
485(** val back_end :
486    observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
487    ((ASM.pseudo_assembly_program, Joint.stack_cost_model) Types.prod,
488    Nat.nat) Types.prod Errors.res **)
489let back_end observe init_cost p =
490  let p0 = RTLabsToRTL.rtlabs_to_rtl init_cost p in
491  let st = lookup_stack_cost (Joint.graph_params_to_params RTL.rTL) p0 in
492  let i =
493    Obj.magic observe Rtl_separate_pass { Types.fst = p0; Types.snd = st }
494  in
495  let i0 = Obj.magic observe Rtl_uniq_pass { Types.fst = p0; Types.snd = st }
496  in
497  let p1 = RTLToERTL.rtl_to_ertl p0 in
498  let st0 = lookup_stack_cost (Joint.graph_params_to_params ERTL.eRTL) p1 in
499  let i1 = Obj.magic observe Ertl_pass { Types.fst = p1; Types.snd = st0 } in
500  let { Types.fst = eta28675; Types.snd = max_stack } =
501    ERTLToLTL.ertl_to_ltl compute_fixpoint colour_graph p1
502  in
503  let { Types.fst = p2; Types.snd = stack_cost } = eta28675 in
504  let st1 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p2 in
505  let i2 = Obj.magic observe Ltl_pass { Types.fst = p2; Types.snd = st1 } in
506  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p2 in
507  let p3 = LTLToLIN.ltl_to_lin p2 in
508  let st3 = lookup_stack_cost (Joint.lin_params_to_params LIN.lIN) p3 in
509  let i3 = Obj.magic observe Lin_pass { Types.fst = p3; Types.snd = st3 } in
510  Obj.magic
511    (Monad.m_bind0 (Monad.max_def Errors.res0)
512      (Obj.magic
513        (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
514          (LINToASM.lin_to_asm p3))) (fun p4 ->
515      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
516        p4; Types.snd = stack_cost }; Types.snd = max_stack }))
517
518open Assembly
519
520open Status
521
522open Fetch
523
524open PolicyFront
525
526open PolicyStep
527
528open Policy
529
530(** val assembler :
531    observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
532    Errors.res **)
533let assembler observe p =
534  Obj.magic
535    (Monad.m_bind0 (Monad.max_def Errors.res0)
536      (Obj.magic
537        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
538          (Policy.jump_expansion' p))) (fun sigma_pol ->
539      let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
540      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
541      let i =
542        Obj.magic observe Assembly_pass { Types.fst = { Types.fst = p;
543          Types.snd = sigma }; Types.snd = pol }
544      in
545      let p0 = Assembly.assembly p sigma pol in
546      let i0 = Obj.magic observe Object_code_pass (Types.pi1 p0) in
547      Obj.magic (Errors.OK (Types.pi1 p0))))
548
549open StructuredTraces
550
551open AbstractStatus
552
553open StatusProofs
554
555open Interpret
556
557open ASMCosts
558
559(** val lift_out_of_sigma :
560    'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1 ->
561    'a2 **)
562let lift_out_of_sigma dflt dec m a_sig =
563  match dec a_sig with
564  | Types.Inl _ -> m a_sig
565  | Types.Inr _ -> dflt
566
567(** val lift_cost_map_back_to_front :
568    ASM.labelled_object_code -> StructuredTraces.as_cost_map ->
569    Label.clight_cost_map **)
570let lift_cost_map_back_to_front oc asm_cost_map =
571  lift_out_of_sigma Nat.O
572    (Obj.magic
573      (BitVectorTrie.strong_decidable_in_codomain
574        (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S (Nat.S
575        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
576        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
577        (Obj.magic oc.ASM.costlabels))) asm_cost_map
578
579open UtilBranch
580
581open ASMCostsSplit
582
583type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
584                         c_stack_cost : Joint.stack_cost_model;
585                         c_max_stack : Nat.nat;
586                         c_labelled_clight : Csyntax.clight_program;
587                         c_clight_cost_map : Label.clight_cost_map }
588
589(** val compiler_output_rect_Type4 :
590    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
591    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
592    compiler_output -> 'a1 **)
593let rec compiler_output_rect_Type4 h_mk_compiler_output x_23441 =
594  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
595    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
596    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_23441
597  in
598  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
599    c_labelled_clight0 c_clight_cost_map0
600
601(** val compiler_output_rect_Type5 :
602    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
603    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
604    compiler_output -> 'a1 **)
605let rec compiler_output_rect_Type5 h_mk_compiler_output x_23443 =
606  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
607    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
608    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_23443
609  in
610  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
611    c_labelled_clight0 c_clight_cost_map0
612
613(** val compiler_output_rect_Type3 :
614    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
615    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
616    compiler_output -> 'a1 **)
617let rec compiler_output_rect_Type3 h_mk_compiler_output x_23445 =
618  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
619    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
620    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_23445
621  in
622  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
623    c_labelled_clight0 c_clight_cost_map0
624
625(** val compiler_output_rect_Type2 :
626    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
627    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
628    compiler_output -> 'a1 **)
629let rec compiler_output_rect_Type2 h_mk_compiler_output x_23447 =
630  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
631    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
632    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_23447
633  in
634  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
635    c_labelled_clight0 c_clight_cost_map0
636
637(** val compiler_output_rect_Type1 :
638    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
639    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
640    compiler_output -> 'a1 **)
641let rec compiler_output_rect_Type1 h_mk_compiler_output x_23449 =
642  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
643    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
644    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_23449
645  in
646  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
647    c_labelled_clight0 c_clight_cost_map0
648
649(** val compiler_output_rect_Type0 :
650    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
651    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
652    compiler_output -> 'a1 **)
653let rec compiler_output_rect_Type0 h_mk_compiler_output x_23451 =
654  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
655    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
656    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_23451
657  in
658  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
659    c_labelled_clight0 c_clight_cost_map0
660
661(** val c_labelled_object_code :
662    compiler_output -> ASM.labelled_object_code **)
663let rec c_labelled_object_code xxx =
664  xxx.c_labelled_object_code
665
666(** val c_stack_cost : compiler_output -> Joint.stack_cost_model **)
667let rec c_stack_cost xxx =
668  xxx.c_stack_cost
669
670(** val c_max_stack : compiler_output -> Nat.nat **)
671let rec c_max_stack xxx =
672  xxx.c_max_stack
673
674(** val c_labelled_clight : compiler_output -> Csyntax.clight_program **)
675let rec c_labelled_clight xxx =
676  xxx.c_labelled_clight
677
678(** val c_clight_cost_map : compiler_output -> Label.clight_cost_map **)
679let rec c_clight_cost_map xxx =
680  xxx.c_clight_cost_map
681
682(** val compiler_output_inv_rect_Type4 :
683    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
684    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
685    -> 'a1 **)
686let compiler_output_inv_rect_Type4 hterm h1 =
687  let hcut = compiler_output_rect_Type4 h1 hterm in hcut __
688
689(** val compiler_output_inv_rect_Type3 :
690    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
691    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
692    -> 'a1 **)
693let compiler_output_inv_rect_Type3 hterm h1 =
694  let hcut = compiler_output_rect_Type3 h1 hterm in hcut __
695
696(** val compiler_output_inv_rect_Type2 :
697    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
698    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
699    -> 'a1 **)
700let compiler_output_inv_rect_Type2 hterm h1 =
701  let hcut = compiler_output_rect_Type2 h1 hterm in hcut __
702
703(** val compiler_output_inv_rect_Type1 :
704    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
705    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
706    -> 'a1 **)
707let compiler_output_inv_rect_Type1 hterm h1 =
708  let hcut = compiler_output_rect_Type1 h1 hterm in hcut __
709
710(** val compiler_output_inv_rect_Type0 :
711    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
712    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
713    -> 'a1 **)
714let compiler_output_inv_rect_Type0 hterm h1 =
715  let hcut = compiler_output_rect_Type0 h1 hterm in hcut __
716
717(** val compiler_output_discr : compiler_output -> compiler_output -> __ **)
718let compiler_output_discr x y =
719  Logic.eq_rect_Type2 x
720    (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
721       c_labelled_clight = a3; c_clight_cost_map = a4 } = x
722     in
723    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
724
725(** val compiler_output_jmdiscr :
726    compiler_output -> compiler_output -> __ **)
727let compiler_output_jmdiscr x y =
728  Logic.eq_rect_Type2 x
729    (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
730       c_labelled_clight = a3; c_clight_cost_map = a4 } = x
731     in
732    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
733
734(** val compile :
735    observe_pass -> Csyntax.clight_program -> compiler_output Errors.res **)
736let compile observe p =
737  Obj.magic
738    (Monad.m_bind3 (Monad.max_def Errors.res0)
739      (Obj.magic (front_end observe p)) (fun init_cost p' p0 ->
740      Monad.m_bind3 (Monad.max_def Errors.res0)
741        (Obj.magic (back_end observe init_cost p0))
742        (fun p1 stack_cost max_stack ->
743        Monad.m_bind0 (Monad.max_def Errors.res0)
744          (Obj.magic (assembler observe p1)) (fun p2 ->
745          let k = ASMCostsSplit.aSM_cost_map p2 in
746          let k' = lift_cost_map_back_to_front p2 k in
747          Monad.m_return0 (Monad.max_def Errors.res0)
748            { c_labelled_object_code = p2; c_stack_cost = stack_cost;
749            c_max_stack = max_stack; c_labelled_clight = p';
750            c_clight_cost_map = k' }))))
751
Note: See TracBrowser for help on using the repository browser.