source: extracted/compiler.ml @ 2842

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

The compiler can now show all back-end traces too (assembly and object code
are excluded ATM).

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