source: extracted/compiler.ml @ 2829

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

Semantics files committed.

File size: 21.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 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 init_cost (Obj.magic p2) in
458      let i4 = Obj.magic observe Rtlabs_pass p3 in
459      (match CostCheck.check_cost_program p3 with
460       | Bool.True ->
461         (match CostInj.check_program_cost_injectivity p3 with
462          | Bool.True ->
463            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
464              { Types.fst = init_cost; Types.snd = p' }; Types.snd = p3 }
465          | Bool.False ->
466            Obj.magic (Errors.Error
467              (Errors.msg ErrorMessages.RepeatedCostLabel0)))
468       | Bool.False ->
469         Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadCostLabelling)))))
470
471(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
472let compute_fixpoint = Compute_fixpoints.compute_fixpoint
473
474(** val colour_graph : Interference.coloured_graph_computer **)
475let colour_graph = Compute_colouring.colour_graph
476
477(** val back_end :
478    observe_pass -> RTLabs_syntax.rTLabs_program ->
479    ((ASM.pseudo_assembly_program, Joint.stack_cost_model) Types.prod,
480    Nat.nat) Types.prod Errors.res **)
481let back_end observe p =
482  let p0 = RTLabsToRTL.rtlabs_to_rtl p in
483  let i = Obj.magic observe Rtl_separate_pass p0 in
484  let i0 = Obj.magic observe Rtl_uniq_pass p0 in
485  let p1 = RTLToERTL.rtl_to_ertl p0 in
486  let i1 = Obj.magic observe Ertl_pass p1 in
487  let p2 = ERTLToERTLptr.ertl_to_ertlptr p1 in
488  let i2 = Obj.magic observe Ertlptr_pass p2 in
489  let { Types.fst = eta2; Types.snd = max_stack } =
490    ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
491  in
492  let { Types.fst = p3; Types.snd = stack_cost } = eta2 in
493  let i3 = Obj.magic observe Ltl_pass p3 in
494  let p4 = LTLToLIN.ltl_to_lin p3 in
495  let i4 = Obj.magic observe Lin_pass p4 in
496  Obj.magic
497    (Monad.m_bind0 (Monad.max_def Errors.res0)
498      (Obj.magic
499        (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
500          (LINToASM.lin_to_asm p4))) (fun p5 ->
501      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
502        p5; Types.snd = stack_cost }; Types.snd = max_stack }))
503
504open Assembly
505
506open Status
507
508open Fetch
509
510open PolicyFront
511
512open PolicyStep
513
514open Policy
515
516(** val assembler :
517    ASM.pseudo_assembly_program -> ASM.labelled_object_code Errors.res **)
518let assembler p =
519  Obj.magic
520    (Monad.m_bind0 (Monad.max_def Errors.res0)
521      (Obj.magic
522        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
523          (Policy.jump_expansion' p))) (fun sigma_pol ->
524      let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
525      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
526      Obj.magic (Errors.OK (Types.pi1 (Assembly.assembly p sigma pol)))))
527
528open AbstractStatus
529
530open StatusProofs
531
532open Interpret
533
534open ASMCosts
535
536(** val lift_cost_map_back_to_front :
537    Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
538    CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
539    StructuredTraces.as_cost_map -> Label.clight_cost_map **)
540let lift_cost_map_back_to_front clight code_memory lbls k asm_cost_map =
541  StructuredTraces.lift_sigma_map_id Nat.O
542    (BitVectorTrie.strong_decidable_in_codomain
543      (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S (Nat.S
544      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
545      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) (Obj.magic lbls))
546    (Obj.magic k) (Obj.magic asm_cost_map)
547
548open UtilBranch
549
550open ASMCostsSplit
551
552type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
553                         c_stack_cost : Joint.stack_cost_model;
554                         c_max_stack : Nat.nat;
555                         c_labelled_clight : Csyntax.clight_program;
556                         c_clight_cost_map : Label.clight_cost_map }
557
558(** val compiler_output_rect_Type4 :
559    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
560    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
561    compiler_output -> 'a1 **)
562let rec compiler_output_rect_Type4 h_mk_compiler_output x_172 =
563  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
564    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
565    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_172
566  in
567  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
568    c_labelled_clight0 c_clight_cost_map0
569
570(** val compiler_output_rect_Type5 :
571    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
572    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
573    compiler_output -> 'a1 **)
574let rec compiler_output_rect_Type5 h_mk_compiler_output x_174 =
575  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
576    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
577    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_174
578  in
579  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
580    c_labelled_clight0 c_clight_cost_map0
581
582(** val compiler_output_rect_Type3 :
583    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
584    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
585    compiler_output -> 'a1 **)
586let rec compiler_output_rect_Type3 h_mk_compiler_output x_176 =
587  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
588    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
589    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_176
590  in
591  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
592    c_labelled_clight0 c_clight_cost_map0
593
594(** val compiler_output_rect_Type2 :
595    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
596    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
597    compiler_output -> 'a1 **)
598let rec compiler_output_rect_Type2 h_mk_compiler_output x_178 =
599  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
600    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
601    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_178
602  in
603  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
604    c_labelled_clight0 c_clight_cost_map0
605
606(** val compiler_output_rect_Type1 :
607    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
608    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
609    compiler_output -> 'a1 **)
610let rec compiler_output_rect_Type1 h_mk_compiler_output x_180 =
611  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
612    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
613    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_180
614  in
615  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
616    c_labelled_clight0 c_clight_cost_map0
617
618(** val compiler_output_rect_Type0 :
619    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
620    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
621    compiler_output -> 'a1 **)
622let rec compiler_output_rect_Type0 h_mk_compiler_output x_182 =
623  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
624    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
625    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_182
626  in
627  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
628    c_labelled_clight0 c_clight_cost_map0
629
630(** val c_labelled_object_code :
631    compiler_output -> ASM.labelled_object_code **)
632let rec c_labelled_object_code xxx =
633  xxx.c_labelled_object_code
634
635(** val c_stack_cost : compiler_output -> Joint.stack_cost_model **)
636let rec c_stack_cost xxx =
637  xxx.c_stack_cost
638
639(** val c_max_stack : compiler_output -> Nat.nat **)
640let rec c_max_stack xxx =
641  xxx.c_max_stack
642
643(** val c_labelled_clight : compiler_output -> Csyntax.clight_program **)
644let rec c_labelled_clight xxx =
645  xxx.c_labelled_clight
646
647(** val c_clight_cost_map : compiler_output -> Label.clight_cost_map **)
648let rec c_clight_cost_map xxx =
649  xxx.c_clight_cost_map
650
651(** val compiler_output_inv_rect_Type4 :
652    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
653    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
654    -> 'a1 **)
655let compiler_output_inv_rect_Type4 hterm h1 =
656  let hcut = compiler_output_rect_Type4 h1 hterm in hcut __
657
658(** val compiler_output_inv_rect_Type3 :
659    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
660    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
661    -> 'a1 **)
662let compiler_output_inv_rect_Type3 hterm h1 =
663  let hcut = compiler_output_rect_Type3 h1 hterm in hcut __
664
665(** val compiler_output_inv_rect_Type2 :
666    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
667    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
668    -> 'a1 **)
669let compiler_output_inv_rect_Type2 hterm h1 =
670  let hcut = compiler_output_rect_Type2 h1 hterm in hcut __
671
672(** val compiler_output_inv_rect_Type1 :
673    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
674    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
675    -> 'a1 **)
676let compiler_output_inv_rect_Type1 hterm h1 =
677  let hcut = compiler_output_rect_Type1 h1 hterm in hcut __
678
679(** val compiler_output_inv_rect_Type0 :
680    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
681    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
682    -> 'a1 **)
683let compiler_output_inv_rect_Type0 hterm h1 =
684  let hcut = compiler_output_rect_Type0 h1 hterm in hcut __
685
686(** val compiler_output_discr : compiler_output -> compiler_output -> __ **)
687let compiler_output_discr x y =
688  Logic.eq_rect_Type2 x
689    (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
690       c_labelled_clight = a3; c_clight_cost_map = a4 } = x
691     in
692    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
693
694(** val compiler_output_jmdiscr :
695    compiler_output -> compiler_output -> __ **)
696let compiler_output_jmdiscr x y =
697  Logic.eq_rect_Type2 x
698    (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
699       c_labelled_clight = a3; c_clight_cost_map = a4 } = x
700     in
701    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
702
703(** val compile :
704    observe_pass -> Csyntax.clight_program -> compiler_output Errors.res **)
705let compile observe p =
706  Obj.magic
707    (Monad.m_bind3 (Monad.max_def Errors.res0)
708      (Obj.magic (front_end observe p)) (fun init_cost p' p0 ->
709      Monad.m_bind3 (Monad.max_def Errors.res0)
710        (Obj.magic (back_end observe p0)) (fun p1 stack_cost max_stack ->
711        Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p1))
712          (fun p2 ->
713          let k = ASMCostsSplit.aSM_cost_map p2 in
714          let k' =
715            lift_cost_map_back_to_front p' (Fetch.load_code_memory p2.ASM.oc)
716              p2.ASM.costlabels k
717          in
718          Monad.m_return0 (Monad.max_def Errors.res0)
719            { c_labelled_object_code = p2; c_stack_cost = stack_cost;
720            c_max_stack = max_stack; c_labelled_clight = p';
721            c_clight_cost_map = k' }))))
722
Note: See TracBrowser for help on using the repository browser.