source: extracted/compiler.ml @ 3083

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

The cost and stack* variables are now initialized with the cost of
the pre-main and the size of globals.

File size: 24.1 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 
473open AssocList
474
475(** val lookup_stack_cost :
476    Joint.params -> Joint.joint_program -> PreIdentifiers.identifier ->
477    Nat.nat Types.option **)
478let lookup_stack_cost p p0 id =
479  AssocList.assoc_list_lookup id
480    (Identifiers.eq_identifier PreIdentifiers.SymbolTag)
481    (Joint.stack_cost p p0)
482
483(** val back_end :
484    observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
485    (((ASM.pseudo_assembly_program, CostLabel.costlabel) Types.prod,
486    Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res **)
487let back_end observe init_cost p =
488  let p0 = RTLabsToRTL.rtlabs_to_rtl init_cost p in
489  let st = lookup_stack_cost (Joint.graph_params_to_params RTL.rTL) p0 in
490  let i =
491    Obj.magic observe Rtl_separate_pass { Types.fst = p0; Types.snd = st }
492  in
493  let i0 = Obj.magic observe Rtl_uniq_pass { Types.fst = p0; Types.snd = st }
494  in
495  let p1 = RTLToERTL.rtl_to_ertl p0 in
496  let st0 = lookup_stack_cost (Joint.graph_params_to_params ERTL.eRTL) p1 in
497  let i1 = Obj.magic observe Ertl_pass { Types.fst = p1; Types.snd = st0 } in
498  let { Types.fst = eta2; Types.snd = max_stack } =
499    ERTLToLTL.ertl_to_ltl compute_fixpoint colour_graph p1
500  in
501  let { Types.fst = p2; Types.snd = stack_cost } = eta2 in
502  let st1 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p2 in
503  let i2 = Obj.magic observe Ltl_pass { Types.fst = p2; Types.snd = st1 } in
504  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p2 in
505  let p3 = LTLToLIN.ltl_to_lin p2 in
506  let st3 = lookup_stack_cost (Joint.lin_params_to_params LIN.lIN) p3 in
507  let i3 = Obj.magic observe Lin_pass { Types.fst = p3; Types.snd = st3 } in
508  Obj.magic
509    (Monad.m_bind0 (Monad.max_def Errors.res0)
510      (Obj.magic
511        (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
512          (LINToASM.lin_to_asm p3))) (fun p4 ->
513      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
514        { Types.fst = p4; Types.snd = init_cost }; Types.snd = stack_cost };
515        Types.snd = max_stack }))
516
517open Assembly
518
519open Status
520
521open Fetch
522
523open PolicyFront
524
525open PolicyStep
526
527open Policy
528
529(** val assembler :
530    observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
531    Errors.res **)
532let assembler observe p =
533  Obj.magic
534    (Monad.m_bind0 (Monad.max_def Errors.res0)
535      (Obj.magic
536        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
537          (Policy.jump_expansion' p))) (fun sigma_pol ->
538      let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
539      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
540      let i =
541        Obj.magic observe Assembly_pass { Types.fst = { Types.fst = p;
542          Types.snd = sigma }; Types.snd = pol }
543      in
544      let p0 = Assembly.assembly p sigma pol in
545      let i0 = Obj.magic observe Object_code_pass (Types.pi1 p0) in
546      Obj.magic (Errors.OK (Types.pi1 p0))))
547
548open StructuredTraces
549
550open AbstractStatus
551
552open StatusProofs
553
554open Interpret
555
556open ASMCosts
557
558(** val lift_out_of_sigma :
559    'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1 ->
560    'a2 **)
561let lift_out_of_sigma dflt dec m a_sig =
562  match dec a_sig with
563  | Types.Inl _ -> m a_sig
564  | Types.Inr _ -> dflt
565
566(** val lift_cost_map_back_to_front :
567    ASM.labelled_object_code -> StructuredTraces.as_cost_map ->
568    Label.clight_cost_map **)
569let lift_cost_map_back_to_front oc asm_cost_map =
570  lift_out_of_sigma Nat.O
571    (Obj.magic
572      (BitVectorTrie.strong_decidable_in_codomain
573        (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S (Nat.S
574        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
575        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
576        (Obj.magic oc.ASM.costlabels))) asm_cost_map
577
578open UtilBranch
579
580open ASMCostsSplit
581
582type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
583                         c_stack_cost : Joint.stack_cost_model;
584                         c_max_stack : Nat.nat;
585                         c_init_costlabel : CostLabel.costlabel;
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    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
592    'a1) -> 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_init_costlabel =
596    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
597    c_clight_cost_map = c_clight_cost_map0 } = x_185
598  in
599  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
600    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
601
602(** val compiler_output_rect_Type5 :
603    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
604    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
605    'a1) -> compiler_output -> 'a1 **)
606let rec compiler_output_rect_Type5 h_mk_compiler_output x_187 =
607  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
608    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
609    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
610    c_clight_cost_map = c_clight_cost_map0 } = x_187
611  in
612  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
613    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
614
615(** val compiler_output_rect_Type3 :
616    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
617    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
618    'a1) -> compiler_output -> 'a1 **)
619let rec compiler_output_rect_Type3 h_mk_compiler_output x_189 =
620  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
621    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
622    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
623    c_clight_cost_map = c_clight_cost_map0 } = x_189
624  in
625  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
626    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
627
628(** val compiler_output_rect_Type2 :
629    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
630    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
631    'a1) -> compiler_output -> 'a1 **)
632let rec compiler_output_rect_Type2 h_mk_compiler_output x_191 =
633  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
634    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
635    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
636    c_clight_cost_map = c_clight_cost_map0 } = x_191
637  in
638  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
639    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
640
641(** val compiler_output_rect_Type1 :
642    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
643    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
644    'a1) -> compiler_output -> 'a1 **)
645let rec compiler_output_rect_Type1 h_mk_compiler_output x_193 =
646  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
647    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
648    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
649    c_clight_cost_map = c_clight_cost_map0 } = x_193
650  in
651  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
652    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
653
654(** val compiler_output_rect_Type0 :
655    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
656    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
657    'a1) -> compiler_output -> 'a1 **)
658let rec compiler_output_rect_Type0 h_mk_compiler_output x_195 =
659  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
660    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
661    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
662    c_clight_cost_map = c_clight_cost_map0 } = x_195
663  in
664  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
665    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
666
667(** val c_labelled_object_code :
668    compiler_output -> ASM.labelled_object_code **)
669let rec c_labelled_object_code xxx =
670  xxx.c_labelled_object_code
671
672(** val c_stack_cost : compiler_output -> Joint.stack_cost_model **)
673let rec c_stack_cost xxx =
674  xxx.c_stack_cost
675
676(** val c_max_stack : compiler_output -> Nat.nat **)
677let rec c_max_stack xxx =
678  xxx.c_max_stack
679
680(** val c_init_costlabel : compiler_output -> CostLabel.costlabel **)
681let rec c_init_costlabel xxx =
682  xxx.c_init_costlabel
683
684(** val c_labelled_clight : compiler_output -> Csyntax.clight_program **)
685let rec c_labelled_clight xxx =
686  xxx.c_labelled_clight
687
688(** val c_clight_cost_map : compiler_output -> Label.clight_cost_map **)
689let rec c_clight_cost_map xxx =
690  xxx.c_clight_cost_map
691
692(** val compiler_output_inv_rect_Type4 :
693    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
694    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
695    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
696let compiler_output_inv_rect_Type4 hterm h1 =
697  let hcut = compiler_output_rect_Type4 h1 hterm in hcut __
698
699(** val compiler_output_inv_rect_Type3 :
700    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
701    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
702    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
703let compiler_output_inv_rect_Type3 hterm h1 =
704  let hcut = compiler_output_rect_Type3 h1 hterm in hcut __
705
706(** val compiler_output_inv_rect_Type2 :
707    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
708    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
709    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
710let compiler_output_inv_rect_Type2 hterm h1 =
711  let hcut = compiler_output_rect_Type2 h1 hterm in hcut __
712
713(** val compiler_output_inv_rect_Type1 :
714    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
715    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
716    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
717let compiler_output_inv_rect_Type1 hterm h1 =
718  let hcut = compiler_output_rect_Type1 h1 hterm in hcut __
719
720(** val compiler_output_inv_rect_Type0 :
721    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
722    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
723    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
724let compiler_output_inv_rect_Type0 hterm h1 =
725  let hcut = compiler_output_rect_Type0 h1 hterm in hcut __
726
727(** val compiler_output_jmdiscr :
728    compiler_output -> compiler_output -> __ **)
729let compiler_output_jmdiscr x y =
730  Logic.eq_rect_Type2 x
731    (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
732       c_init_costlabel = a3; c_labelled_clight = a4; c_clight_cost_map =
733       a5 } = x
734     in
735    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
736
737(** val compile :
738    observe_pass -> Csyntax.clight_program -> compiler_output Errors.res **)
739let compile observe p =
740  Obj.magic
741    (Monad.m_bind3 (Monad.max_def Errors.res0)
742      (Obj.magic (front_end observe p)) (fun init_cost p' p0 ->
743      Monad.m_bind3 (Monad.max_def Errors.res0)
744        (Obj.magic (back_end observe init_cost p0))
745        (fun p_init_costlabel stack_cost max_stack ->
746        let { Types.fst = p1; Types.snd = init_costlabel } = p_init_costlabel
747        in
748        Monad.m_bind0 (Monad.max_def Errors.res0)
749          (Obj.magic (assembler observe p1)) (fun p2 ->
750          let k = ASMCostsSplit.aSM_cost_map p2 in
751          let k' = lift_cost_map_back_to_front p2 k in
752          Monad.m_return0 (Monad.max_def Errors.res0)
753            { c_labelled_object_code = p2; c_stack_cost = stack_cost;
754            c_max_stack = max_stack; c_init_costlabel = init_costlabel;
755            c_labelled_clight = p'; c_clight_cost_map = k' }))))
756
Note: See TracBrowser for help on using the repository browser.