source: extracted/compiler.ml @ 3043

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

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 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 BitVectorTrie
152
153open Graphs
154
155open Order
156
157open Registers
158
159open RTLabs_syntax
160
161open ToRTLabs
162
163open Deqsets_extra
164
165open CostMisc
166
167open Listb_extra
168
169open CostSpec
170
171open CostCheck
172
173open CostInj
174
175open State
176
177open Bind_new
178
179open BindLists
180
181open Blocks
182
183open TranslateUtils
184
185open String
186
187open LabelledObjects
188
189open I8051
190
191open BackEndOps
192
193open Joint
194
195open RTL
196
197open RTLabsToRTL
198
199open ERTL
200
201open RegisterSet
202
203open RTLToERTL
204
205open Fixpoints
206
207open Set_adt
208
209open Liveness
210
211open Interference
212
213open Joint_LTL_LIN
214
215open LTL
216
217open ERTLToLTL
218
219open LIN
220
221open Linearise
222
223open LTLToLIN
224
225open ASM
226
227open BitVectorTrieSet
228
229open LINToASM
230
231type pass =
232| Clight_pass
233| Clight_switch_removed_pass
234| Clight_label_pass
235| Clight_simplified_pass
236| Cminor_pass
237| Rtlabs_pass
238| Rtl_separate_pass
239| Rtl_uniq_pass
240| Ertl_pass
241| Ltl_pass
242| Lin_pass
243| Assembly_pass
244| Object_code_pass
245
246(** val pass_rect_Type4 :
247    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
248    -> 'a1 -> 'a1 -> pass -> 'a1 **)
249let 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
250| Clight_pass -> h_clight_pass
251| Clight_switch_removed_pass -> h_clight_switch_removed_pass
252| Clight_label_pass -> h_clight_label_pass
253| Clight_simplified_pass -> h_clight_simplified_pass
254| Cminor_pass -> h_cminor_pass
255| Rtlabs_pass -> h_rtlabs_pass
256| Rtl_separate_pass -> h_rtl_separate_pass
257| Rtl_uniq_pass -> h_rtl_uniq_pass
258| Ertl_pass -> h_ertl_pass
259| Ltl_pass -> h_ltl_pass
260| Lin_pass -> h_lin_pass
261| Assembly_pass -> h_assembly_pass
262| Object_code_pass -> h_object_code_pass
263
264(** val pass_rect_Type5 :
265    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
266    -> 'a1 -> 'a1 -> pass -> 'a1 **)
267let 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
268| Clight_pass -> h_clight_pass
269| Clight_switch_removed_pass -> h_clight_switch_removed_pass
270| Clight_label_pass -> h_clight_label_pass
271| Clight_simplified_pass -> h_clight_simplified_pass
272| Cminor_pass -> h_cminor_pass
273| Rtlabs_pass -> h_rtlabs_pass
274| Rtl_separate_pass -> h_rtl_separate_pass
275| Rtl_uniq_pass -> h_rtl_uniq_pass
276| Ertl_pass -> h_ertl_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_Type3 :
283    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
284    -> 'a1 -> 'a1 -> pass -> 'a1 **)
285let 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
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| Ltl_pass -> h_ltl_pass
296| Lin_pass -> h_lin_pass
297| Assembly_pass -> h_assembly_pass
298| Object_code_pass -> h_object_code_pass
299
300(** val pass_rect_Type2 :
301    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
302    -> 'a1 -> 'a1 -> pass -> 'a1 **)
303let 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
304| Clight_pass -> h_clight_pass
305| Clight_switch_removed_pass -> h_clight_switch_removed_pass
306| Clight_label_pass -> h_clight_label_pass
307| Clight_simplified_pass -> h_clight_simplified_pass
308| Cminor_pass -> h_cminor_pass
309| Rtlabs_pass -> h_rtlabs_pass
310| Rtl_separate_pass -> h_rtl_separate_pass
311| Rtl_uniq_pass -> h_rtl_uniq_pass
312| Ertl_pass -> h_ertl_pass
313| Ltl_pass -> h_ltl_pass
314| Lin_pass -> h_lin_pass
315| Assembly_pass -> h_assembly_pass
316| Object_code_pass -> h_object_code_pass
317
318(** val pass_rect_Type1 :
319    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
320    -> 'a1 -> 'a1 -> pass -> 'a1 **)
321let 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
322| Clight_pass -> h_clight_pass
323| Clight_switch_removed_pass -> h_clight_switch_removed_pass
324| Clight_label_pass -> h_clight_label_pass
325| Clight_simplified_pass -> h_clight_simplified_pass
326| Cminor_pass -> h_cminor_pass
327| Rtlabs_pass -> h_rtlabs_pass
328| Rtl_separate_pass -> h_rtl_separate_pass
329| Rtl_uniq_pass -> h_rtl_uniq_pass
330| Ertl_pass -> h_ertl_pass
331| Ltl_pass -> h_ltl_pass
332| Lin_pass -> h_lin_pass
333| Assembly_pass -> h_assembly_pass
334| Object_code_pass -> h_object_code_pass
335
336(** val pass_rect_Type0 :
337    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
338    -> 'a1 -> 'a1 -> pass -> 'a1 **)
339let 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
340| Clight_pass -> h_clight_pass
341| Clight_switch_removed_pass -> h_clight_switch_removed_pass
342| Clight_label_pass -> h_clight_label_pass
343| Clight_simplified_pass -> h_clight_simplified_pass
344| Cminor_pass -> h_cminor_pass
345| Rtlabs_pass -> h_rtlabs_pass
346| Rtl_separate_pass -> h_rtl_separate_pass
347| Rtl_uniq_pass -> h_rtl_uniq_pass
348| Ertl_pass -> h_ertl_pass
349| Ltl_pass -> h_ltl_pass
350| Lin_pass -> h_lin_pass
351| Assembly_pass -> h_assembly_pass
352| Object_code_pass -> h_object_code_pass
353
354(** val pass_inv_rect_Type4 :
355    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
356    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
357    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
358let pass_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
359  let hcut = pass_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
360  in
361  hcut __
362
363(** val pass_inv_rect_Type3 :
364    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
365    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
366    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
367let pass_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
368  let hcut = pass_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
369  in
370  hcut __
371
372(** val pass_inv_rect_Type2 :
373    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
374    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
375    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
376let pass_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
377  let hcut = pass_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
378  in
379  hcut __
380
381(** val pass_inv_rect_Type1 :
382    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
383    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
384    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
385let pass_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
386  let hcut = pass_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
387  in
388  hcut __
389
390(** val pass_inv_rect_Type0 :
391    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
392    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
393    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
394let pass_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
395  let hcut = pass_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
396  in
397  hcut __
398
399(** val pass_discr : pass -> pass -> __ **)
400let pass_discr x y =
401  Logic.eq_rect_Type2 x
402    (match x with
403     | Clight_pass -> Obj.magic (fun _ dH -> dH)
404     | Clight_switch_removed_pass -> Obj.magic (fun _ dH -> dH)
405     | Clight_label_pass -> Obj.magic (fun _ dH -> dH)
406     | Clight_simplified_pass -> Obj.magic (fun _ dH -> dH)
407     | Cminor_pass -> Obj.magic (fun _ dH -> dH)
408     | Rtlabs_pass -> Obj.magic (fun _ dH -> dH)
409     | Rtl_separate_pass -> Obj.magic (fun _ dH -> dH)
410     | Rtl_uniq_pass -> Obj.magic (fun _ dH -> dH)
411     | Ertl_pass -> Obj.magic (fun _ dH -> dH)
412     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
413     | Lin_pass -> Obj.magic (fun _ dH -> dH)
414     | Assembly_pass -> Obj.magic (fun _ dH -> dH)
415     | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y
416
417(** val pass_jmdiscr : pass -> pass -> __ **)
418let pass_jmdiscr x y =
419  Logic.eq_rect_Type2 x
420    (match x with
421     | Clight_pass -> Obj.magic (fun _ dH -> dH)
422     | Clight_switch_removed_pass -> Obj.magic (fun _ dH -> dH)
423     | Clight_label_pass -> Obj.magic (fun _ dH -> dH)
424     | Clight_simplified_pass -> Obj.magic (fun _ dH -> dH)
425     | Cminor_pass -> Obj.magic (fun _ dH -> dH)
426     | Rtlabs_pass -> Obj.magic (fun _ dH -> dH)
427     | Rtl_separate_pass -> Obj.magic (fun _ dH -> dH)
428     | Rtl_uniq_pass -> Obj.magic (fun _ dH -> dH)
429     | Ertl_pass -> Obj.magic (fun _ dH -> dH)
430     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
431     | Lin_pass -> Obj.magic (fun _ dH -> dH)
432     | Assembly_pass -> Obj.magic (fun _ dH -> dH)
433     | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y
434
435type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod
436
437type syntax_of_pass = __
438
439type observe_pass = pass -> syntax_of_pass -> Types.unit0
440
441(** val front_end :
442    observe_pass -> Csyntax.clight_program -> ((CostLabel.costlabel,
443    Csyntax.clight_program) Types.prod, RTLabs_syntax.rTLabs_program)
444    Types.prod Errors.res **)
445let front_end observe p =
446  let i = Obj.magic observe Clight_pass p in
447  let p0 = SwitchRemoval.program_switch_removal p in
448  let i0 = Obj.magic observe Clight_switch_removed_pass p0 in
449  let { Types.fst = p'; Types.snd = init_cost } = Label.clight_label p0 in
450  let i1 = Obj.magic observe Clight_label_pass p' in
451  let p1 = SimplifyCasts.simplify_program p' in
452  let i2 = Obj.magic observe Clight_simplified_pass p1 in
453  Obj.magic
454    (Monad.m_bind0 (Monad.max_def Errors.res0)
455      (Obj.magic (ToCminor.clight_to_cminor p1)) (fun p2 ->
456      let i3 = observe Cminor_pass p2 in
457      let p3 = ToRTLabs.cminor_to_rtlabs (Obj.magic p2) in
458      let i4 = Obj.magic observe Rtlabs_pass p3 in
459      Monad.m_bind0 (Monad.max_def Errors.res0)
460        (Obj.magic (CostCheck.check_cost_program_prf p3)) (fun _ ->
461        Monad.m_bind0 (Monad.max_def Errors.res0)
462          (Obj.magic (CostInj.check_program_cost_injectivity_prf p3))
463          (fun _ ->
464          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
465            { Types.fst = init_cost; Types.snd = p' }; Types.snd = p3 }))))
466
467open Uses
468
469(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
470let compute_fixpoint = Compute_fixpoints.compute_fixpoint
471
472(** val colour_graph : Interference.coloured_graph_computer **)
473let colour_graph = Compute_colouring.colour_graph
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 = eta2; 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 } = eta2 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_185 =
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_185
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_187 =
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_187
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_189 =
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_189
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_191 =
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_191
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_193 =
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_193
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_195 =
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_195
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.