source: extracted/compiler.ml @ 3001

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

New extraction.

File size: 24.2 KB
RevLine 
[2601]1open Preamble
2
3open CostLabel
4
[2649]5open Coqlib
6
[2601]7open Proper
8
9open PositiveMap
10
11open Deqsets
12
[2649]13open ErrorMessages
14
[2601]15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
[2717]27open Exp
28
[2601]29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
[2773]35open Util
36
37open FoldStuff
38
39open BitVector
40
[2601]41open Jmeq
42
43open Russell
44
45open List
46
[2773]47open Setoids
[2601]48
[2773]49open Monad
[2601]50
[2773]51open Option
[2601]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
[2773]151open BitVectorTrie
152
[2601]153open Graphs
154
155open Order
156
157open Registers
158
159open RTLabs_syntax
160
161open ToRTLabs
162
[2730]163open Deqsets_extra
164
165open CostMisc
166
[2743]167open Listb_extra
[2730]168
169open CostSpec
170
171open CostCheck
172
173open CostInj
174
[2717]175open State
176
177open Bind_new
178
179open BindLists
180
181open Blocks
182
183open TranslateUtils
184
[2649]185open String
186
[2601]187open LabelledObjects
188
[2717]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 ERTLptr
206
207open ERTLToERTLptr
208
209open Fixpoints
210
211open Set_adt
212
213open Liveness
214
215open Interference
216
217open Joint_LTL_LIN
218
219open LTL
220
221open ERTLptrToLTL
222
223open LIN
224
225open Linearise
226
227open LTLToLIN
228
[2601]229open ASM
230
[2717]231open BitVectorTrieSet
232
233open LINToASM
234
[2829]235type pass =
236| Clight_pass
237| Clight_switch_removed_pass
238| Clight_label_pass
239| Clight_simplified_pass
240| Cminor_pass
241| Rtlabs_pass
242| Rtl_separate_pass
243| Rtl_uniq_pass
244| Ertl_pass
245| Ertlptr_pass
246| Ltl_pass
247| Lin_pass
[2875]248| Assembly_pass
249| Object_code_pass
[2829]250
251(** val pass_rect_Type4 :
252    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
[2875]253    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
254let 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 h_assembly_pass h_object_code_pass = function
[2829]255| Clight_pass -> h_clight_pass
256| Clight_switch_removed_pass -> h_clight_switch_removed_pass
257| Clight_label_pass -> h_clight_label_pass
258| Clight_simplified_pass -> h_clight_simplified_pass
259| Cminor_pass -> h_cminor_pass
260| Rtlabs_pass -> h_rtlabs_pass
261| Rtl_separate_pass -> h_rtl_separate_pass
262| Rtl_uniq_pass -> h_rtl_uniq_pass
263| Ertl_pass -> h_ertl_pass
264| Ertlptr_pass -> h_ertlptr_pass
265| Ltl_pass -> h_ltl_pass
266| Lin_pass -> h_lin_pass
[2875]267| Assembly_pass -> h_assembly_pass
268| Object_code_pass -> h_object_code_pass
[2829]269
270(** val pass_rect_Type5 :
271    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
[2875]272    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
273let 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 h_assembly_pass h_object_code_pass = function
[2829]274| Clight_pass -> h_clight_pass
275| Clight_switch_removed_pass -> h_clight_switch_removed_pass
276| Clight_label_pass -> h_clight_label_pass
277| Clight_simplified_pass -> h_clight_simplified_pass
278| Cminor_pass -> h_cminor_pass
279| Rtlabs_pass -> h_rtlabs_pass
280| Rtl_separate_pass -> h_rtl_separate_pass
281| Rtl_uniq_pass -> h_rtl_uniq_pass
282| Ertl_pass -> h_ertl_pass
283| Ertlptr_pass -> h_ertlptr_pass
284| Ltl_pass -> h_ltl_pass
285| Lin_pass -> h_lin_pass
[2875]286| Assembly_pass -> h_assembly_pass
287| Object_code_pass -> h_object_code_pass
[2829]288
289(** val pass_rect_Type3 :
290    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
[2875]291    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
292let 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 h_assembly_pass h_object_code_pass = function
[2829]293| Clight_pass -> h_clight_pass
294| Clight_switch_removed_pass -> h_clight_switch_removed_pass
295| Clight_label_pass -> h_clight_label_pass
296| Clight_simplified_pass -> h_clight_simplified_pass
297| Cminor_pass -> h_cminor_pass
298| Rtlabs_pass -> h_rtlabs_pass
299| Rtl_separate_pass -> h_rtl_separate_pass
300| Rtl_uniq_pass -> h_rtl_uniq_pass
301| Ertl_pass -> h_ertl_pass
302| Ertlptr_pass -> h_ertlptr_pass
303| Ltl_pass -> h_ltl_pass
304| Lin_pass -> h_lin_pass
[2875]305| Assembly_pass -> h_assembly_pass
306| Object_code_pass -> h_object_code_pass
[2829]307
308(** val pass_rect_Type2 :
309    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
[2875]310    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
311let 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 h_assembly_pass h_object_code_pass = function
[2829]312| Clight_pass -> h_clight_pass
313| Clight_switch_removed_pass -> h_clight_switch_removed_pass
314| Clight_label_pass -> h_clight_label_pass
315| Clight_simplified_pass -> h_clight_simplified_pass
316| Cminor_pass -> h_cminor_pass
317| Rtlabs_pass -> h_rtlabs_pass
318| Rtl_separate_pass -> h_rtl_separate_pass
319| Rtl_uniq_pass -> h_rtl_uniq_pass
320| Ertl_pass -> h_ertl_pass
321| Ertlptr_pass -> h_ertlptr_pass
322| Ltl_pass -> h_ltl_pass
323| Lin_pass -> h_lin_pass
[2875]324| Assembly_pass -> h_assembly_pass
325| Object_code_pass -> h_object_code_pass
[2829]326
327(** val pass_rect_Type1 :
328    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
[2875]329    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
330let 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 h_assembly_pass h_object_code_pass = function
[2829]331| Clight_pass -> h_clight_pass
332| Clight_switch_removed_pass -> h_clight_switch_removed_pass
333| Clight_label_pass -> h_clight_label_pass
334| Clight_simplified_pass -> h_clight_simplified_pass
335| Cminor_pass -> h_cminor_pass
336| Rtlabs_pass -> h_rtlabs_pass
337| Rtl_separate_pass -> h_rtl_separate_pass
338| Rtl_uniq_pass -> h_rtl_uniq_pass
339| Ertl_pass -> h_ertl_pass
340| Ertlptr_pass -> h_ertlptr_pass
341| Ltl_pass -> h_ltl_pass
342| Lin_pass -> h_lin_pass
[2875]343| Assembly_pass -> h_assembly_pass
344| Object_code_pass -> h_object_code_pass
[2829]345
346(** val pass_rect_Type0 :
347    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
[2875]348    -> 'a1 -> 'a1 -> '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 h_assembly_pass h_object_code_pass = function
[2829]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
[2875]362| Assembly_pass -> h_assembly_pass
363| Object_code_pass -> h_object_code_pass
[2829]364
365(** val pass_inv_rect_Type4 :
366    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
367    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
[2875]368    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
369    -> 'a1 **)
370let pass_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
371  let hcut =
372    pass_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
373  in
[2829]374  hcut __
375
376(** val pass_inv_rect_Type3 :
377    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
378    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
[2875]379    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
380    -> 'a1 **)
381let pass_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
382  let hcut =
383    pass_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
384  in
[2829]385  hcut __
386
387(** val pass_inv_rect_Type2 :
388    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
389    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
[2875]390    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
391    -> 'a1 **)
392let pass_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
393  let hcut =
394    pass_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
395  in
[2829]396  hcut __
397
398(** val pass_inv_rect_Type1 :
399    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
400    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
[2875]401    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
402    -> 'a1 **)
403let pass_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
404  let hcut =
405    pass_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
406  in
[2829]407  hcut __
408
409(** val pass_inv_rect_Type0 :
410    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
411    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
[2875]412    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
413    -> 'a1 **)
414let pass_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
415  let hcut =
416    pass_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
417  in
[2829]418  hcut __
419
420(** val pass_discr : pass -> pass -> __ **)
421let pass_discr 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)
[2875]435     | Lin_pass -> Obj.magic (fun _ dH -> dH)
436     | Assembly_pass -> Obj.magic (fun _ dH -> dH)
437     | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y
[2829]438
439(** val pass_jmdiscr : pass -> pass -> __ **)
440let pass_jmdiscr x y =
441  Logic.eq_rect_Type2 x
442    (match x with
443     | Clight_pass -> Obj.magic (fun _ dH -> dH)
444     | Clight_switch_removed_pass -> Obj.magic (fun _ dH -> dH)
445     | Clight_label_pass -> Obj.magic (fun _ dH -> dH)
446     | Clight_simplified_pass -> Obj.magic (fun _ dH -> dH)
447     | Cminor_pass -> Obj.magic (fun _ dH -> dH)
448     | Rtlabs_pass -> Obj.magic (fun _ dH -> dH)
449     | Rtl_separate_pass -> Obj.magic (fun _ dH -> dH)
450     | Rtl_uniq_pass -> Obj.magic (fun _ dH -> dH)
451     | Ertl_pass -> Obj.magic (fun _ dH -> dH)
452     | Ertlptr_pass -> Obj.magic (fun _ dH -> dH)
453     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
[2875]454     | Lin_pass -> Obj.magic (fun _ dH -> dH)
455     | Assembly_pass -> Obj.magic (fun _ dH -> dH)
456     | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y
[2829]457
[2842]458type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod
459
[2829]460type syntax_of_pass = __
461
462type observe_pass = pass -> syntax_of_pass -> Types.unit0
463
464(** val front_end :
465    observe_pass -> Csyntax.clight_program -> ((CostLabel.costlabel,
466    Csyntax.clight_program) Types.prod, RTLabs_syntax.rTLabs_program)
467    Types.prod Errors.res **)
468let front_end observe p =
469  let i = Obj.magic observe Clight_pass p in
470  let p0 = SwitchRemoval.program_switch_removal p in
471  let i0 = Obj.magic observe Clight_switch_removed_pass p0 in
472  let { Types.fst = p'; Types.snd = init_cost } = Label.clight_label p0 in
473  let i1 = Obj.magic observe Clight_label_pass p' in
474  let p1 = SimplifyCasts.simplify_program p' in
475  let i2 = Obj.magic observe Clight_simplified_pass p1 in
476  Obj.magic
477    (Monad.m_bind0 (Monad.max_def Errors.res0)
478      (Obj.magic (ToCminor.clight_to_cminor p1)) (fun p2 ->
479      let i3 = observe Cminor_pass p2 in
[2951]480      let p3 = ToRTLabs.cminor_to_rtlabs (Obj.magic p2) in
[2829]481      let i4 = Obj.magic observe Rtlabs_pass p3 in
482      (match CostCheck.check_cost_program p3 with
483       | Bool.True ->
484         (match CostInj.check_program_cost_injectivity p3 with
485          | Bool.True ->
486            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
487              { Types.fst = init_cost; Types.snd = p' }; Types.snd = p3 }
488          | Bool.False ->
489            Obj.magic (Errors.Error
490              (Errors.msg ErrorMessages.RepeatedCostLabel0)))
491       | Bool.False ->
492         Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadCostLabelling)))))
493
[2842]494open Uses
495
[2717]496(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
[2736]497let compute_fixpoint = Compute_fixpoints.compute_fixpoint
[2960]498 
[2717]499(** val colour_graph : Interference.coloured_graph_computer **)
[2738]500let colour_graph = Compute_colouring.colour_graph
[2717]501
[2842]502open AssocList
503
504(** val lookup_stack_cost :
505    Joint.params -> Joint.joint_program -> PreIdentifiers.identifier ->
506    Nat.nat Types.option **)
507let lookup_stack_cost p p0 id =
508  AssocList.assoc_list_lookup id
509    (Identifiers.eq_identifier PreIdentifiers.SymbolTag)
510    (Joint.stack_cost p p0)
511
[2601]512(** val back_end :
[2951]513    observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
[2829]514    ((ASM.pseudo_assembly_program, Joint.stack_cost_model) Types.prod,
515    Nat.nat) Types.prod Errors.res **)
[2951]516let back_end observe init_cost p =
517  let p0 = RTLabsToRTL.rtlabs_to_rtl init_cost p in
[2842]518  let st = lookup_stack_cost (Joint.graph_params_to_params RTL.rTL) p0 in
519  let i =
520    Obj.magic observe Rtl_separate_pass { Types.fst = p0; Types.snd = st }
521  in
522  let i0 = Obj.magic observe Rtl_uniq_pass { Types.fst = p0; Types.snd = st }
523  in
[2773]524  let p1 = RTLToERTL.rtl_to_ertl p0 in
[2842]525  let st0 = lookup_stack_cost (Joint.graph_params_to_params ERTL.eRTL) p1 in
526  let i1 = Obj.magic observe Ertl_pass { Types.fst = p1; Types.snd = st0 } in
[2773]527  let p2 = ERTLToERTLptr.ertl_to_ertlptr p1 in
[2842]528  let st1 =
529    lookup_stack_cost (Joint.graph_params_to_params ERTLptr.eRTLptr) p2
530  in
531  let i2 = Obj.magic observe Ertlptr_pass { Types.fst = p2; Types.snd = st1 }
532  in
[3001]533  let { Types.fst = eta29478; Types.snd = max_stack } =
[2775]534    ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
535  in
[3001]536  let { Types.fst = p3; Types.snd = stack_cost } = eta29478 in
[2842]537  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in
538  let i3 = Obj.magic observe Ltl_pass { Types.fst = p3; Types.snd = st2 } in
539  let st3 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in
[2773]540  let p4 = LTLToLIN.ltl_to_lin p3 in
[2842]541  let st4 = lookup_stack_cost (Joint.lin_params_to_params LIN.lIN) p4 in
542  let i4 = Obj.magic observe Lin_pass { Types.fst = p4; Types.snd = st4 } in
[2797]543  Obj.magic
544    (Monad.m_bind0 (Monad.max_def Errors.res0)
545      (Obj.magic
546        (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
547          (LINToASM.lin_to_asm p4))) (fun p5 ->
548      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
[2854]549        p5; Types.snd = stack_cost }; Types.snd = max_stack }))
[2601]550
[2717]551open Assembly
552
553open Status
554
555open Fetch
556
557open PolicyFront
558
559open PolicyStep
560
561open Policy
562
[2601]563(** val assembler :
[2875]564    observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
565    Errors.res **)
566let assembler observe p =
[2717]567  Obj.magic
568    (Monad.m_bind0 (Monad.max_def Errors.res0)
569      (Obj.magic
570        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
[2773]571          (Policy.jump_expansion' p))) (fun sigma_pol ->
572      let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
[2717]573      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
[2905]574      let i =
575        Obj.magic observe Assembly_pass { Types.fst = { Types.fst = p;
576          Types.snd = sigma }; Types.snd = pol }
577      in
[2875]578      let p0 = Assembly.assembly p sigma pol in
[2905]579      let i0 = Obj.magic observe Object_code_pass (Types.pi1 p0) in
[2875]580      Obj.magic (Errors.OK (Types.pi1 p0))))
[2601]581
[2951]582open StructuredTraces
583
[2601]584open AbstractStatus
585
586open StatusProofs
587
588open Interpret
589
590open ASMCosts
591
592(** val lift_cost_map_back_to_front :
[2909]593    Csyntax.clight_program -> ASM.labelled_object_code ->
[2773]594    StructuredTraces.as_cost_map -> Label.clight_cost_map **)
[2909]595let lift_cost_map_back_to_front clight oc k asm_cost_map =
[2773]596  StructuredTraces.lift_sigma_map_id Nat.O
597    (BitVectorTrie.strong_decidable_in_codomain
598      (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S (Nat.S
599      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
[2909]600      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))
601      (Obj.magic oc.ASM.costlabels)) (Obj.magic k) (Obj.magic asm_cost_map)
[2601]602
603open UtilBranch
604
605open ASMCostsSplit
606
[2775]607type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
608                         c_stack_cost : Joint.stack_cost_model;
609                         c_max_stack : Nat.nat;
610                         c_labelled_clight : Csyntax.clight_program;
611                         c_clight_cost_map : Label.clight_cost_map }
612
613(** val compiler_output_rect_Type4 :
614    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
615    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
616    compiler_output -> 'a1 **)
[3001]617let rec compiler_output_rect_Type4 h_mk_compiler_output x_15313 =
[2775]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 =
[3001]620    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_15313
[2775]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_Type5 :
626    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
627    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
628    compiler_output -> 'a1 **)
[3001]629let rec compiler_output_rect_Type5 h_mk_compiler_output x_15315 =
[2775]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 =
[3001]632    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_15315
[2775]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_Type3 :
638    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
639    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
640    compiler_output -> 'a1 **)
[3001]641let rec compiler_output_rect_Type3 h_mk_compiler_output x_15317 =
[2775]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 =
[3001]644    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_15317
[2775]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_Type2 :
650    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
651    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
652    compiler_output -> 'a1 **)
[3001]653let rec compiler_output_rect_Type2 h_mk_compiler_output x_15319 =
[2775]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 =
[3001]656    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_15319
[2775]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 compiler_output_rect_Type1 :
662    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
663    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
664    compiler_output -> 'a1 **)
[3001]665let rec compiler_output_rect_Type1 h_mk_compiler_output x_15321 =
[2775]666  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
667    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
[3001]668    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_15321
[2775]669  in
670  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
671    c_labelled_clight0 c_clight_cost_map0
672
673(** val compiler_output_rect_Type0 :
674    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
675    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
676    compiler_output -> 'a1 **)
[3001]677let rec compiler_output_rect_Type0 h_mk_compiler_output x_15323 =
[2775]678  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
679    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
[3001]680    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_15323
[2775]681  in
682  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
683    c_labelled_clight0 c_clight_cost_map0
684
685(** val c_labelled_object_code :
686    compiler_output -> ASM.labelled_object_code **)
687let rec c_labelled_object_code xxx =
688  xxx.c_labelled_object_code
689
690(** val c_stack_cost : compiler_output -> Joint.stack_cost_model **)
691let rec c_stack_cost xxx =
692  xxx.c_stack_cost
693
694(** val c_max_stack : compiler_output -> Nat.nat **)
695let rec c_max_stack xxx =
696  xxx.c_max_stack
697
698(** val c_labelled_clight : compiler_output -> Csyntax.clight_program **)
699let rec c_labelled_clight xxx =
700  xxx.c_labelled_clight
701
702(** val c_clight_cost_map : compiler_output -> Label.clight_cost_map **)
703let rec c_clight_cost_map xxx =
704  xxx.c_clight_cost_map
705
706(** val compiler_output_inv_rect_Type4 :
707    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
708    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
709    -> 'a1 **)
710let compiler_output_inv_rect_Type4 hterm h1 =
711  let hcut = compiler_output_rect_Type4 h1 hterm in hcut __
712
713(** val compiler_output_inv_rect_Type3 :
714    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
715    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
716    -> 'a1 **)
717let compiler_output_inv_rect_Type3 hterm h1 =
718  let hcut = compiler_output_rect_Type3 h1 hterm in hcut __
719
720(** val compiler_output_inv_rect_Type2 :
721    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
722    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
723    -> 'a1 **)
724let compiler_output_inv_rect_Type2 hterm h1 =
725  let hcut = compiler_output_rect_Type2 h1 hterm in hcut __
726
727(** val compiler_output_inv_rect_Type1 :
728    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
729    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
730    -> 'a1 **)
731let compiler_output_inv_rect_Type1 hterm h1 =
732  let hcut = compiler_output_rect_Type1 h1 hterm in hcut __
733
734(** val compiler_output_inv_rect_Type0 :
735    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
736    Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
737    -> 'a1 **)
738let compiler_output_inv_rect_Type0 hterm h1 =
739  let hcut = compiler_output_rect_Type0 h1 hterm in hcut __
740
741(** val compiler_output_discr : compiler_output -> compiler_output -> __ **)
742let compiler_output_discr x y =
743  Logic.eq_rect_Type2 x
744    (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
745       c_labelled_clight = a3; c_clight_cost_map = a4 } = x
746     in
747    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
748
749(** val compiler_output_jmdiscr :
750    compiler_output -> compiler_output -> __ **)
751let compiler_output_jmdiscr x y =
752  Logic.eq_rect_Type2 x
753    (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
754       c_labelled_clight = a3; c_clight_cost_map = a4 } = x
755     in
756    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
757
[2829]758(** val compile :
759    observe_pass -> Csyntax.clight_program -> compiler_output Errors.res **)
760let compile observe p =
[2601]761  Obj.magic
[2829]762    (Monad.m_bind3 (Monad.max_def Errors.res0)
763      (Obj.magic (front_end observe p)) (fun init_cost p' p0 ->
764      Monad.m_bind3 (Monad.max_def Errors.res0)
[2951]765        (Obj.magic (back_end observe init_cost p0))
766        (fun p1 stack_cost max_stack ->
[2875]767        Monad.m_bind0 (Monad.max_def Errors.res0)
768          (Obj.magic (assembler observe p1)) (fun p2 ->
[2773]769          let k = ASMCostsSplit.aSM_cost_map p2 in
[2909]770          let k' = lift_cost_map_back_to_front p' p2 k in
[2775]771          Monad.m_return0 (Monad.max_def Errors.res0)
[2854]772            { c_labelled_object_code = p2; c_stack_cost = stack_cost;
[2775]773            c_max_stack = max_stack; c_labelled_clight = p';
774            c_clight_cost_map = k' }))))
[2601]775
Note: See TracBrowser for help on using the repository browser.