Changeset 2829


Ignore:
Timestamp:
Mar 8, 2013, 11:18:50 PM (6 years ago)
Author:
sacerdot
Message:

Semantics files committed.

Location:
extracted
Files:
30 added
2 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.ml

    r2827 r2829  
    185185open CostInj
    186186
     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
    187441(** val front_end :
    188     Csyntax.clight_program -> ((CostLabel.costlabel, Csyntax.clight_program)
    189     Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res **)
    190 let front_end p =
     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
    191447  let p0 = SwitchRemoval.program_switch_removal p in
     448  let i0 = Obj.magic observe Clight_switch_removed_pass p0 in
    192449  let { Types.fst = p'; Types.snd = init_cost } = Label.clight_label p0 in
     450  let i1 = Obj.magic observe Clight_label_pass p' in
    193451  let p1 = SimplifyCasts.simplify_program p' in
     452  let i2 = Obj.magic observe Clight_simplified_pass p1 in
    194453  Obj.magic
    195454    (Monad.m_bind0 (Monad.max_def Errors.res0)
    196455      (Obj.magic (ToCminor.clight_to_cminor p1)) (fun p2 ->
    197       let p3 = ToRTLabs.cminor_to_rtlabs init_cost p2 in
     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
    198459      (match CostCheck.check_cost_program p3 with
    199460       | Bool.True ->
     
    208469         Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadCostLabelling)))))
    209470
    210 open State
    211 
    212 open Bind_new
    213 
    214 open BindLists
    215 
    216 open Blocks
    217 
    218 open TranslateUtils
    219 
    220 open String
    221 
    222 open LabelledObjects
    223 
    224 open I8051
    225 
    226 open BackEndOps
    227 
    228 open Joint
    229 
    230 open RTL
    231 
    232 open RTLabsToRTL
    233 
    234 open ERTL
    235 
    236 open RegisterSet
    237 
    238 open RTLToERTL
    239 
    240 open ERTLptr
    241 
    242 open ERTLToERTLptr
    243 
    244 open Fixpoints
    245 
    246 open Set_adt
    247 
    248 open Liveness
    249 
    250 open Interference
    251 
    252 open Joint_LTL_LIN
    253 
    254 open LTL
    255 
    256 open ERTLptrToLTL
    257 
    258 open LIN
    259 
    260 open Linearise
    261 
    262 open LTLToLIN
    263 
    264 open ASM
    265 
    266 open BitVectorTrieSet
    267 
    268 open LINToASM
    269 
    270471(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
    271472let compute_fixpoint = Compute_fixpoints.compute_fixpoint
     
    275476
    276477(** val back_end :
    277     RTLabs_syntax.rTLabs_program -> ((ASM.pseudo_assembly_program,
    278     Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res **)
    279 let back_end p =
     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 =
    280482  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
    281485  let p1 = RTLToERTL.rtl_to_ertl p0 in
     486  let i1 = Obj.magic observe Ertl_pass p1 in
    282487  let p2 = ERTLToERTLptr.ertl_to_ertlptr p1 in
    283   let { Types.fst = eta29084; Types.snd = max_stack } =
     488  let i2 = Obj.magic observe Ertlptr_pass p2 in
     489  let { Types.fst = eta2; Types.snd = max_stack } =
    284490    ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
    285491  in
    286   let { Types.fst = p3; Types.snd = stack_cost } = eta29084 in
     492  let { Types.fst = p3; Types.snd = stack_cost } = eta2 in
     493  let i3 = Obj.magic observe Ltl_pass p3 in
    287494  let p4 = LTLToLIN.ltl_to_lin p3 in
     495  let i4 = Obj.magic observe Lin_pass p4 in
    288496  Obj.magic
    289497    (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    352560    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    353561    compiler_output -> 'a1 **)
    354 let rec compiler_output_rect_Type4 h_mk_compiler_output x_25025 =
     562let rec compiler_output_rect_Type4 h_mk_compiler_output x_172 =
    355563  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    356564    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    357     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25025
     565    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_172
    358566  in
    359567  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    364572    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    365573    compiler_output -> 'a1 **)
    366 let rec compiler_output_rect_Type5 h_mk_compiler_output x_25027 =
     574let rec compiler_output_rect_Type5 h_mk_compiler_output x_174 =
    367575  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    368576    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    369     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25027
     577    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_174
    370578  in
    371579  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    376584    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    377585    compiler_output -> 'a1 **)
    378 let rec compiler_output_rect_Type3 h_mk_compiler_output x_25029 =
     586let rec compiler_output_rect_Type3 h_mk_compiler_output x_176 =
    379587  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    380588    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    381     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25029
     589    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_176
    382590  in
    383591  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    388596    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    389597    compiler_output -> 'a1 **)
    390 let rec compiler_output_rect_Type2 h_mk_compiler_output x_25031 =
     598let rec compiler_output_rect_Type2 h_mk_compiler_output x_178 =
    391599  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    392600    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    393     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25031
     601    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_178
    394602  in
    395603  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    400608    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    401609    compiler_output -> 'a1 **)
    402 let rec compiler_output_rect_Type1 h_mk_compiler_output x_25033 =
     610let rec compiler_output_rect_Type1 h_mk_compiler_output x_180 =
    403611  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    404612    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    405     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25033
     613    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_180
    406614  in
    407615  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    412620    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    413621    compiler_output -> 'a1 **)
    414 let rec compiler_output_rect_Type0 h_mk_compiler_output x_25035 =
     622let rec compiler_output_rect_Type0 h_mk_compiler_output x_182 =
    415623  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    416624    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    417     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25035
     625    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_182
    418626  in
    419627  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    493701    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
    494702
    495 (** val compile : Csyntax.clight_program -> compiler_output Errors.res **)
    496 let compile p =
     703(** val compile :
     704    observe_pass -> Csyntax.clight_program -> compiler_output Errors.res **)
     705let compile observe p =
    497706  Obj.magic
    498     (Monad.m_bind3 (Monad.max_def Errors.res0) (Obj.magic (front_end p))
    499       (fun init_cost p' p0 ->
    500       Monad.m_bind3 (Monad.max_def Errors.res0) (Obj.magic (back_end p0))
    501         (fun p1 stack_cost max_stack ->
     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 ->
    502711        Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p1))
    503712          (fun p2 ->
  • extracted/compiler.mli

    r2775 r2829  
    185185open CostInj
    186186
     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
     261val pass_rect_Type4 :
     262  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
     263  -> 'a1 -> pass -> 'a1
     264
     265val pass_rect_Type5 :
     266  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
     267  -> 'a1 -> pass -> 'a1
     268
     269val pass_rect_Type3 :
     270  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
     271  -> 'a1 -> pass -> 'a1
     272
     273val pass_rect_Type2 :
     274  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
     275  -> 'a1 -> pass -> 'a1
     276
     277val pass_rect_Type1 :
     278  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
     279  -> 'a1 -> pass -> 'a1
     280
     281val pass_rect_Type0 :
     282  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
     283  -> 'a1 -> pass -> 'a1
     284
     285val pass_inv_rect_Type4 :
     286  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     287  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     288  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     289
     290val pass_inv_rect_Type3 :
     291  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     292  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     293  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     294
     295val pass_inv_rect_Type2 :
     296  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     297  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     298  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     299
     300val pass_inv_rect_Type1 :
     301  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     302  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     303  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     304
     305val pass_inv_rect_Type0 :
     306  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     307  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     308  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     309
     310val pass_discr : pass -> pass -> __
     311
     312val pass_jmdiscr : pass -> pass -> __
     313
     314type syntax_of_pass = __
     315
     316type observe_pass = pass -> syntax_of_pass -> Types.unit0
     317
    187318val front_end :
    188   Csyntax.clight_program -> ((CostLabel.costlabel, Csyntax.clight_program)
    189   Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res
    190 
    191 open State
    192 
    193 open Bind_new
    194 
    195 open BindLists
    196 
    197 open Blocks
    198 
    199 open TranslateUtils
    200 
    201 open String
    202 
    203 open LabelledObjects
    204 
    205 open I8051
    206 
    207 open BackEndOps
    208 
    209 open Joint
    210 
    211 open RTL
    212 
    213 open RTLabsToRTL
    214 
    215 open ERTL
    216 
    217 open RegisterSet
    218 
    219 open RTLToERTL
    220 
    221 open ERTLptr
    222 
    223 open ERTLToERTLptr
    224 
    225 open Fixpoints
    226 
    227 open Set_adt
    228 
    229 open Liveness
    230 
    231 open Interference
    232 
    233 open Joint_LTL_LIN
    234 
    235 open LTL
    236 
    237 open ERTLptrToLTL
    238 
    239 open LIN
    240 
    241 open Linearise
    242 
    243 open LTLToLIN
    244 
    245 open ASM
    246 
    247 open BitVectorTrieSet
    248 
    249 open LINToASM
     319  observe_pass -> Csyntax.clight_program -> ((CostLabel.costlabel,
     320  Csyntax.clight_program) Types.prod, RTLabs_syntax.rTLabs_program)
     321  Types.prod Errors.res
    250322
    251323val compute_fixpoint : Fixpoints.fixpoint_computer
     
    254326
    255327val back_end :
    256   RTLabs_syntax.rTLabs_program -> ((ASM.pseudo_assembly_program,
    257   Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res
     328  observe_pass -> RTLabs_syntax.rTLabs_program ->
     329  ((ASM.pseudo_assembly_program, Joint.stack_cost_model) Types.prod, Nat.nat)
     330  Types.prod Errors.res
    258331
    259332open Assembly
     
    364437val compiler_output_jmdiscr : compiler_output -> compiler_output -> __
    365438
    366 val compile : Csyntax.clight_program -> compiler_output Errors.res
    367 
     439val compile :
     440  observe_pass -> Csyntax.clight_program -> compiler_output Errors.res
     441
Note: See TracChangeset for help on using the changeset viewer.