Changeset 3019


Ignore:
Timestamp:
Mar 28, 2013, 5:27:46 PM (4 years ago)
Author:
sacerdot
Message:

New extraction after ERTLptr abortion.

Location:
extracted
Files:
2 added
10 deleted
15 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.ml

    r3001 r3019  
    203203open RTLToERTL
    204204
    205 open ERTLptr
    206 
    207 open ERTLToERTLptr
    208 
    209205open Fixpoints
    210206
     
    219215open LTL
    220216
    221 open ERTLptrToLTL
     217open ERTLToLTL
    222218
    223219open LIN
     
    243239| Rtl_uniq_pass
    244240| Ertl_pass
    245 | Ertlptr_pass
    246241| Ltl_pass
    247242| Lin_pass
     
    251246(** val pass_rect_Type4 :
    252247    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    253     -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
    254 let 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
     248    -> 'a1 -> 'a1 -> pass -> 'a1 **)
     249let rec pass_rect_Type4 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
    255250| Clight_pass -> h_clight_pass
    256251| Clight_switch_removed_pass -> h_clight_switch_removed_pass
     
    262257| Rtl_uniq_pass -> h_rtl_uniq_pass
    263258| Ertl_pass -> h_ertl_pass
    264 | Ertlptr_pass -> h_ertlptr_pass
    265259| Ltl_pass -> h_ltl_pass
    266260| Lin_pass -> h_lin_pass
     
    270264(** val pass_rect_Type5 :
    271265    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    272     -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
    273 let 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
     266    -> 'a1 -> 'a1 -> pass -> 'a1 **)
     267let rec pass_rect_Type5 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
    274268| Clight_pass -> h_clight_pass
    275269| Clight_switch_removed_pass -> h_clight_switch_removed_pass
     
    281275| Rtl_uniq_pass -> h_rtl_uniq_pass
    282276| Ertl_pass -> h_ertl_pass
    283 | Ertlptr_pass -> h_ertlptr_pass
    284277| Ltl_pass -> h_ltl_pass
    285278| Lin_pass -> h_lin_pass
     
    289282(** val pass_rect_Type3 :
    290283    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    291     -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
    292 let 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
     284    -> 'a1 -> 'a1 -> pass -> 'a1 **)
     285let rec pass_rect_Type3 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
    293286| Clight_pass -> h_clight_pass
    294287| Clight_switch_removed_pass -> h_clight_switch_removed_pass
     
    300293| Rtl_uniq_pass -> h_rtl_uniq_pass
    301294| Ertl_pass -> h_ertl_pass
    302 | Ertlptr_pass -> h_ertlptr_pass
    303295| Ltl_pass -> h_ltl_pass
    304296| Lin_pass -> h_lin_pass
     
    308300(** val pass_rect_Type2 :
    309301    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    310     -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
    311 let 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
     302    -> 'a1 -> 'a1 -> pass -> 'a1 **)
     303let rec pass_rect_Type2 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
    312304| Clight_pass -> h_clight_pass
    313305| Clight_switch_removed_pass -> h_clight_switch_removed_pass
     
    319311| Rtl_uniq_pass -> h_rtl_uniq_pass
    320312| Ertl_pass -> h_ertl_pass
    321 | Ertlptr_pass -> h_ertlptr_pass
    322313| Ltl_pass -> h_ltl_pass
    323314| Lin_pass -> h_lin_pass
     
    327318(** val pass_rect_Type1 :
    328319    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    329     -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
    330 let 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
     320    -> 'a1 -> 'a1 -> pass -> 'a1 **)
     321let rec pass_rect_Type1 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
    331322| Clight_pass -> h_clight_pass
    332323| Clight_switch_removed_pass -> h_clight_switch_removed_pass
     
    338329| Rtl_uniq_pass -> h_rtl_uniq_pass
    339330| Ertl_pass -> h_ertl_pass
    340 | Ertlptr_pass -> h_ertlptr_pass
    341331| Ltl_pass -> h_ltl_pass
    342332| Lin_pass -> h_lin_pass
     
    346336(** val pass_rect_Type0 :
    347337    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    348     -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
    349 let 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
     338    -> 'a1 -> 'a1 -> pass -> 'a1 **)
     339let rec pass_rect_Type0 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
    350340| Clight_pass -> h_clight_pass
    351341| Clight_switch_removed_pass -> h_clight_switch_removed_pass
     
    357347| Rtl_uniq_pass -> h_rtl_uniq_pass
    358348| Ertl_pass -> h_ertl_pass
    359 | Ertlptr_pass -> h_ertlptr_pass
    360349| Ltl_pass -> h_ltl_pass
    361350| Lin_pass -> h_lin_pass
     
    366355    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    367356    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    368     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    369     -> 'a1 **)
    370 let 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
     357    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     358let pass_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
     359  let hcut = pass_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
    373360  in
    374361  hcut __
     
    377364    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    378365    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    379     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    380     -> 'a1 **)
    381 let 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
     366    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     367let pass_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
     368  let hcut = pass_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
    384369  in
    385370  hcut __
     
    388373    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    389374    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    390     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    391     -> 'a1 **)
    392 let 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
     375    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     376let pass_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
     377  let hcut = pass_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
    395378  in
    396379  hcut __
     
    399382    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    400383    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    401     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    402     -> 'a1 **)
    403 let 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
     384    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     385let pass_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
     386  let hcut = pass_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
    406387  in
    407388  hcut __
     
    410391    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    411392    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    412     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
    413     -> 'a1 **)
    414 let 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
     393    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     394let pass_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
     395  let hcut = pass_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
    417396  in
    418397  hcut __
     
    431410     | Rtl_uniq_pass -> Obj.magic (fun _ dH -> dH)
    432411     | Ertl_pass -> Obj.magic (fun _ dH -> dH)
    433      | Ertlptr_pass -> Obj.magic (fun _ dH -> dH)
    434412     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
    435413     | Lin_pass -> Obj.magic (fun _ dH -> dH)
     
    450428     | Rtl_uniq_pass -> Obj.magic (fun _ dH -> dH)
    451429     | Ertl_pass -> Obj.magic (fun _ dH -> dH)
    452      | Ertlptr_pass -> Obj.magic (fun _ dH -> dH)
    453430     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
    454431     | Lin_pass -> Obj.magic (fun _ dH -> dH)
     
    525502  let st0 = lookup_stack_cost (Joint.graph_params_to_params ERTL.eRTL) p1 in
    526503  let i1 = Obj.magic observe Ertl_pass { Types.fst = p1; Types.snd = st0 } in
    527   let p2 = ERTLToERTLptr.ertl_to_ertlptr p1 in
    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
    533   let { Types.fst = eta29478; Types.snd = max_stack } =
    534     ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
    535   in
    536   let { Types.fst = p3; Types.snd = stack_cost } = eta29478 in
    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
    540   let p4 = LTLToLIN.ltl_to_lin p3 in
    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
     504  let { Types.fst = eta2; Types.snd = max_stack } =
     505    ERTLToLTL.ertl_to_ltl compute_fixpoint colour_graph p1
     506  in
     507  let { Types.fst = p2; Types.snd = stack_cost } = eta2 in
     508  let st1 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p2 in
     509  let i2 = Obj.magic observe Ltl_pass { Types.fst = p2; Types.snd = st1 } in
     510  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p2 in
     511  let p3 = LTLToLIN.ltl_to_lin p2 in
     512  let st3 = lookup_stack_cost (Joint.lin_params_to_params LIN.lIN) p3 in
     513  let i3 = Obj.magic observe Lin_pass { Types.fst = p3; Types.snd = st3 } in
    543514  Obj.magic
    544515    (Monad.m_bind0 (Monad.max_def Errors.res0)
    545516      (Obj.magic
    546517        (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
    547           (LINToASM.lin_to_asm p4))) (fun p5 ->
     518          (LINToASM.lin_to_asm p3))) (fun p4 ->
    548519      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
    549         p5; Types.snd = stack_cost }; Types.snd = max_stack }))
     520        p4; Types.snd = stack_cost }; Types.snd = max_stack }))
    550521
    551522open Assembly
     
    615586    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    616587    compiler_output -> 'a1 **)
    617 let rec compiler_output_rect_Type4 h_mk_compiler_output x_15313 =
     588let rec compiler_output_rect_Type4 h_mk_compiler_output x_185 =
    618589  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    619590    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    620     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_15313
     591    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_185
    621592  in
    622593  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    627598    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    628599    compiler_output -> 'a1 **)
    629 let rec compiler_output_rect_Type5 h_mk_compiler_output x_15315 =
     600let rec compiler_output_rect_Type5 h_mk_compiler_output x_187 =
    630601  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    631602    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    632     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_15315
     603    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_187
    633604  in
    634605  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    639610    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    640611    compiler_output -> 'a1 **)
    641 let rec compiler_output_rect_Type3 h_mk_compiler_output x_15317 =
     612let rec compiler_output_rect_Type3 h_mk_compiler_output x_189 =
    642613  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    643614    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    644     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_15317
     615    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_189
    645616  in
    646617  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    651622    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    652623    compiler_output -> 'a1 **)
    653 let rec compiler_output_rect_Type2 h_mk_compiler_output x_15319 =
     624let rec compiler_output_rect_Type2 h_mk_compiler_output x_191 =
    654625  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    655626    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    656     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_15319
     627    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_191
    657628  in
    658629  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    663634    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    664635    compiler_output -> 'a1 **)
    665 let rec compiler_output_rect_Type1 h_mk_compiler_output x_15321 =
     636let rec compiler_output_rect_Type1 h_mk_compiler_output x_193 =
    666637  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    667638    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    668     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_15321
     639    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_193
    669640  in
    670641  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    675646    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    676647    compiler_output -> 'a1 **)
    677 let rec compiler_output_rect_Type0 h_mk_compiler_output x_15323 =
     648let rec compiler_output_rect_Type0 h_mk_compiler_output x_195 =
    678649  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    679650    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    680     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_15323
     651    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_195
    681652  in
    682653  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
  • extracted/compiler.mli

    r2951 r3019  
    203203open RTLToERTL
    204204
    205 open ERTLptr
    206 
    207 open ERTLToERTLptr
    208 
    209205open Fixpoints
    210206
     
    219215open LTL
    220216
    221 open ERTLptrToLTL
     217open ERTLToLTL
    222218
    223219open LIN
     
    243239| Rtl_uniq_pass
    244240| Ertl_pass
    245 | Ertlptr_pass
    246241| Ltl_pass
    247242| Lin_pass
     
    251246val pass_rect_Type4 :
    252247  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    253   -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
     248  -> 'a1 -> 'a1 -> pass -> 'a1
    254249
    255250val pass_rect_Type5 :
    256251  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    257   -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
     252  -> 'a1 -> 'a1 -> pass -> 'a1
    258253
    259254val pass_rect_Type3 :
    260255  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    261   -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
     256  -> 'a1 -> 'a1 -> pass -> 'a1
    262257
    263258val pass_rect_Type2 :
    264259  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    265   -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
     260  -> 'a1 -> 'a1 -> pass -> 'a1
    266261
    267262val pass_rect_Type1 :
    268263  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    269   -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
     264  -> 'a1 -> 'a1 -> pass -> 'a1
    270265
    271266val pass_rect_Type0 :
    272267  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    273   -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
     268  -> 'a1 -> 'a1 -> pass -> 'a1
    274269
    275270val pass_inv_rect_Type4 :
    276271  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    277272  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    278   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     273  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
    279274
    280275val pass_inv_rect_Type3 :
    281276  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    282277  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    283   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     278  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
    284279
    285280val pass_inv_rect_Type2 :
    286281  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    287282  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    288   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     283  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
    289284
    290285val pass_inv_rect_Type1 :
    291286  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    292287  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    293   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     288  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
    294289
    295290val pass_inv_rect_Type0 :
    296291  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    297292  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    298   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     293  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
    299294
    300295val pass_discr : pass -> pass -> __
  • extracted/interference.ml

    r3001 r3019  
    9898
    9999open ERTL
    100 
    101 open ERTLptr
    102100
    103101open Div_and_mod
     
    136134    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    137135let rec decision_rect_Type4 h_decision_spill h_decision_colour = function
    138 | Decision_spill x_5765 -> h_decision_spill x_5765
    139 | Decision_colour x_5766 -> h_decision_colour x_5766
     136| Decision_spill x_7 -> h_decision_spill x_7
     137| Decision_colour x_8 -> h_decision_colour x_8
    140138
    141139(** val decision_rect_Type5 :
    142140    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    143141let rec decision_rect_Type5 h_decision_spill h_decision_colour = function
    144 | Decision_spill x_5770 -> h_decision_spill x_5770
    145 | Decision_colour x_5771 -> h_decision_colour x_5771
     142| Decision_spill x_12 -> h_decision_spill x_12
     143| Decision_colour x_13 -> h_decision_colour x_13
    146144
    147145(** val decision_rect_Type3 :
    148146    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    149147let rec decision_rect_Type3 h_decision_spill h_decision_colour = function
    150 | Decision_spill x_5775 -> h_decision_spill x_5775
    151 | Decision_colour x_5776 -> h_decision_colour x_5776
     148| Decision_spill x_17 -> h_decision_spill x_17
     149| Decision_colour x_18 -> h_decision_colour x_18
    152150
    153151(** val decision_rect_Type2 :
    154152    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    155153let rec decision_rect_Type2 h_decision_spill h_decision_colour = function
    156 | Decision_spill x_5780 -> h_decision_spill x_5780
    157 | Decision_colour x_5781 -> h_decision_colour x_5781
     154| Decision_spill x_22 -> h_decision_spill x_22
     155| Decision_colour x_23 -> h_decision_colour x_23
    158156
    159157(** val decision_rect_Type1 :
    160158    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    161159let rec decision_rect_Type1 h_decision_spill h_decision_colour = function
    162 | Decision_spill x_5785 -> h_decision_spill x_5785
    163 | Decision_colour x_5786 -> h_decision_colour x_5786
     160| Decision_spill x_27 -> h_decision_spill x_27
     161| Decision_colour x_28 -> h_decision_colour x_28
    164162
    165163(** val decision_rect_Type0 :
    166164    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    167165let rec decision_rect_Type0 h_decision_spill h_decision_colour = function
    168 | Decision_spill x_5790 -> h_decision_spill x_5790
    169 | Decision_colour x_5791 -> h_decision_colour x_5791
     166| Decision_spill x_32 -> h_decision_spill x_32
     167| Decision_colour x_33 -> h_decision_colour x_33
    170168
    171169(** val decision_inv_rect_Type4 :
     
    219217    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    220218    __ -> 'a1) -> coloured_graph -> 'a1 **)
    221 let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_5826 =
    222   let { colouring = colouring0; spilled_no = spilled_no0 } = x_5826 in
     219let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_68 =
     220  let { colouring = colouring0; spilled_no = spilled_no0 } = x_68 in
    223221  h_mk_coloured_graph colouring0 spilled_no0 __ __
    224222
     
    226224    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    227225    __ -> 'a1) -> coloured_graph -> 'a1 **)
    228 let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_5828 =
    229   let { colouring = colouring0; spilled_no = spilled_no0 } = x_5828 in
     226let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_70 =
     227  let { colouring = colouring0; spilled_no = spilled_no0 } = x_70 in
    230228  h_mk_coloured_graph colouring0 spilled_no0 __ __
    231229
     
    233231    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    234232    __ -> 'a1) -> coloured_graph -> 'a1 **)
    235 let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_5830 =
    236   let { colouring = colouring0; spilled_no = spilled_no0 } = x_5830 in
     233let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_72 =
     234  let { colouring = colouring0; spilled_no = spilled_no0 } = x_72 in
    237235  h_mk_coloured_graph colouring0 spilled_no0 __ __
    238236
     
    240238    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    241239    __ -> 'a1) -> coloured_graph -> 'a1 **)
    242 let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_5832 =
    243   let { colouring = colouring0; spilled_no = spilled_no0 } = x_5832 in
     240let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_74 =
     241  let { colouring = colouring0; spilled_no = spilled_no0 } = x_74 in
    244242  h_mk_coloured_graph colouring0 spilled_no0 __ __
    245243
     
    247245    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    248246    __ -> 'a1) -> coloured_graph -> 'a1 **)
    249 let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_5834 =
    250   let { colouring = colouring0; spilled_no = spilled_no0 } = x_5834 in
     247let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_76 =
     248  let { colouring = colouring0; spilled_no = spilled_no0 } = x_76 in
    251249  h_mk_coloured_graph colouring0 spilled_no0 __ __
    252250
     
    254252    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    255253    __ -> 'a1) -> coloured_graph -> 'a1 **)
    256 let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_5836 =
    257   let { colouring = colouring0; spilled_no = spilled_no0 } = x_5836 in
     254let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_78 =
     255  let { colouring = colouring0; spilled_no = spilled_no0 } = x_78 in
    258256  h_mk_coloured_graph colouring0 spilled_no0 __ __
    259257
  • extracted/interference.mli

    r2951 r3019  
    9898
    9999open ERTL
    100 
    101 open ERTLptr
    102100
    103101open Div_and_mod
  • extracted/joint_LTL_LIN.ml

    r3001 r3019  
    130130    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    131131let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    132 | From_acc (x_5280, x_5279) -> h_from_acc x_5280 x_5279
    133 | To_acc (x_5282, x_5281) -> h_to_acc x_5282 x_5281
    134 | Int_to_reg (x_5284, x_5283) -> h_int_to_reg x_5284 x_5283
    135 | Int_to_acc (x_5286, x_5285) -> h_int_to_acc x_5286 x_5285
     132| From_acc (x_16, x_15) -> h_from_acc x_16 x_15
     133| To_acc (x_18, x_17) -> h_to_acc x_18 x_17
     134| Int_to_reg (x_20, x_19) -> h_int_to_reg x_20 x_19
     135| Int_to_acc (x_22, x_21) -> h_int_to_acc x_22 x_21
    136136
    137137(** val registers_move_rect_Type5 :
     
    140140    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    141141let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    142 | From_acc (x_5293, x_5292) -> h_from_acc x_5293 x_5292
    143 | To_acc (x_5295, x_5294) -> h_to_acc x_5295 x_5294
    144 | Int_to_reg (x_5297, x_5296) -> h_int_to_reg x_5297 x_5296
    145 | Int_to_acc (x_5299, x_5298) -> h_int_to_acc x_5299 x_5298
     142| From_acc (x_29, x_28) -> h_from_acc x_29 x_28
     143| To_acc (x_31, x_30) -> h_to_acc x_31 x_30
     144| Int_to_reg (x_33, x_32) -> h_int_to_reg x_33 x_32
     145| Int_to_acc (x_35, x_34) -> h_int_to_acc x_35 x_34
    146146
    147147(** val registers_move_rect_Type3 :
     
    150150    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    151151let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    152 | From_acc (x_5306, x_5305) -> h_from_acc x_5306 x_5305
    153 | To_acc (x_5308, x_5307) -> h_to_acc x_5308 x_5307
    154 | Int_to_reg (x_5310, x_5309) -> h_int_to_reg x_5310 x_5309
    155 | Int_to_acc (x_5312, x_5311) -> h_int_to_acc x_5312 x_5311
     152| From_acc (x_42, x_41) -> h_from_acc x_42 x_41
     153| To_acc (x_44, x_43) -> h_to_acc x_44 x_43
     154| Int_to_reg (x_46, x_45) -> h_int_to_reg x_46 x_45
     155| Int_to_acc (x_48, x_47) -> h_int_to_acc x_48 x_47
    156156
    157157(** val registers_move_rect_Type2 :
     
    160160    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    161161let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    162 | From_acc (x_5319, x_5318) -> h_from_acc x_5319 x_5318
    163 | To_acc (x_5321, x_5320) -> h_to_acc x_5321 x_5320
    164 | Int_to_reg (x_5323, x_5322) -> h_int_to_reg x_5323 x_5322
    165 | Int_to_acc (x_5325, x_5324) -> h_int_to_acc x_5325 x_5324
     162| From_acc (x_55, x_54) -> h_from_acc x_55 x_54
     163| To_acc (x_57, x_56) -> h_to_acc x_57 x_56
     164| Int_to_reg (x_59, x_58) -> h_int_to_reg x_59 x_58
     165| Int_to_acc (x_61, x_60) -> h_int_to_acc x_61 x_60
    166166
    167167(** val registers_move_rect_Type1 :
     
    170170    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    171171let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    172 | From_acc (x_5332, x_5331) -> h_from_acc x_5332 x_5331
    173 | To_acc (x_5334, x_5333) -> h_to_acc x_5334 x_5333
    174 | Int_to_reg (x_5336, x_5335) -> h_int_to_reg x_5336 x_5335
    175 | Int_to_acc (x_5338, x_5337) -> h_int_to_acc x_5338 x_5337
     172| From_acc (x_68, x_67) -> h_from_acc x_68 x_67
     173| To_acc (x_70, x_69) -> h_to_acc x_70 x_69
     174| Int_to_reg (x_72, x_71) -> h_int_to_reg x_72 x_71
     175| Int_to_acc (x_74, x_73) -> h_int_to_acc x_74 x_73
    176176
    177177(** val registers_move_rect_Type0 :
     
    180180    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    181181let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    182 | From_acc (x_5345, x_5344) -> h_from_acc x_5345 x_5344
    183 | To_acc (x_5347, x_5346) -> h_to_acc x_5347 x_5346
    184 | Int_to_reg (x_5349, x_5348) -> h_int_to_reg x_5349 x_5348
    185 | Int_to_acc (x_5351, x_5350) -> h_int_to_acc x_5351 x_5350
     182| From_acc (x_81, x_80) -> h_from_acc x_81 x_80
     183| To_acc (x_83, x_82) -> h_to_acc x_83 x_82
     184| Int_to_reg (x_85, x_84) -> h_int_to_reg x_85 x_84
     185| Int_to_acc (x_87, x_86) -> h_int_to_acc x_87 x_86
    186186
    187187(** val registers_move_inv_rect_Type4 :
     
    246246| SAVE_CARRY
    247247| RESTORE_CARRY
    248 | LOW_ADDRESS of I8051.register * Graphs.label
    249 | HIGH_ADDRESS of I8051.register * Graphs.label
     248| LOW_ADDRESS of Graphs.label
     249| HIGH_ADDRESS of Graphs.label
    250250
    251251(** val ltl_lin_seq_rect_Type4 :
    252     'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
    253     -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
     252    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
     253    ltl_lin_seq -> 'a1 **)
    254254let rec ltl_lin_seq_rect_Type4 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
    255255| SAVE_CARRY -> h_SAVE_CARRY
    256256| RESTORE_CARRY -> h_RESTORE_CARRY
    257 | LOW_ADDRESS (x_5445, x_5444) -> h_LOW_ADDRESS x_5445 x_5444
    258 | HIGH_ADDRESS (x_5447, x_5446) -> h_HIGH_ADDRESS x_5447 x_5446
     257| LOW_ADDRESS x_178 -> h_LOW_ADDRESS x_178
     258| HIGH_ADDRESS x_179 -> h_HIGH_ADDRESS x_179
    259259
    260260(** val ltl_lin_seq_rect_Type5 :
    261     'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
    262     -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
     261    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
     262    ltl_lin_seq -> 'a1 **)
    263263let rec ltl_lin_seq_rect_Type5 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
    264264| SAVE_CARRY -> h_SAVE_CARRY
    265265| RESTORE_CARRY -> h_RESTORE_CARRY
    266 | LOW_ADDRESS (x_5454, x_5453) -> h_LOW_ADDRESS x_5454 x_5453
    267 | HIGH_ADDRESS (x_5456, x_5455) -> h_HIGH_ADDRESS x_5456 x_5455
     266| LOW_ADDRESS x_185 -> h_LOW_ADDRESS x_185
     267| HIGH_ADDRESS x_186 -> h_HIGH_ADDRESS x_186
    268268
    269269(** val ltl_lin_seq_rect_Type3 :
    270     'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
    271     -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
     270    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
     271    ltl_lin_seq -> 'a1 **)
    272272let rec ltl_lin_seq_rect_Type3 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
    273273| SAVE_CARRY -> h_SAVE_CARRY
    274274| RESTORE_CARRY -> h_RESTORE_CARRY
    275 | LOW_ADDRESS (x_5463, x_5462) -> h_LOW_ADDRESS x_5463 x_5462
    276 | HIGH_ADDRESS (x_5465, x_5464) -> h_HIGH_ADDRESS x_5465 x_5464
     275| LOW_ADDRESS x_192 -> h_LOW_ADDRESS x_192
     276| HIGH_ADDRESS x_193 -> h_HIGH_ADDRESS x_193
    277277
    278278(** val ltl_lin_seq_rect_Type2 :
    279     'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
    280     -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
     279    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
     280    ltl_lin_seq -> 'a1 **)
    281281let rec ltl_lin_seq_rect_Type2 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
    282282| SAVE_CARRY -> h_SAVE_CARRY
    283283| RESTORE_CARRY -> h_RESTORE_CARRY
    284 | LOW_ADDRESS (x_5472, x_5471) -> h_LOW_ADDRESS x_5472 x_5471
    285 | HIGH_ADDRESS (x_5474, x_5473) -> h_HIGH_ADDRESS x_5474 x_5473
     284| LOW_ADDRESS x_199 -> h_LOW_ADDRESS x_199
     285| HIGH_ADDRESS x_200 -> h_HIGH_ADDRESS x_200
    286286
    287287(** val ltl_lin_seq_rect_Type1 :
    288     'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
    289     -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
     288    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
     289    ltl_lin_seq -> 'a1 **)
    290290let rec ltl_lin_seq_rect_Type1 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
    291291| SAVE_CARRY -> h_SAVE_CARRY
    292292| RESTORE_CARRY -> h_RESTORE_CARRY
    293 | LOW_ADDRESS (x_5481, x_5480) -> h_LOW_ADDRESS x_5481 x_5480
    294 | HIGH_ADDRESS (x_5483, x_5482) -> h_HIGH_ADDRESS x_5483 x_5482
     293| LOW_ADDRESS x_206 -> h_LOW_ADDRESS x_206
     294| HIGH_ADDRESS x_207 -> h_HIGH_ADDRESS x_207
    295295
    296296(** val ltl_lin_seq_rect_Type0 :
    297     'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register
    298     -> Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1 **)
     297    'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) ->
     298    ltl_lin_seq -> 'a1 **)
    299299let rec ltl_lin_seq_rect_Type0 h_SAVE_CARRY h_RESTORE_CARRY h_LOW_ADDRESS h_HIGH_ADDRESS = function
    300300| SAVE_CARRY -> h_SAVE_CARRY
    301301| RESTORE_CARRY -> h_RESTORE_CARRY
    302 | LOW_ADDRESS (x_5490, x_5489) -> h_LOW_ADDRESS x_5490 x_5489
    303 | HIGH_ADDRESS (x_5492, x_5491) -> h_HIGH_ADDRESS x_5492 x_5491
     302| LOW_ADDRESS x_213 -> h_LOW_ADDRESS x_213
     303| HIGH_ADDRESS x_214 -> h_HIGH_ADDRESS x_214
    304304
    305305(** val ltl_lin_seq_inv_rect_Type4 :
    306     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    307     Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
    308     'a1) -> 'a1 **)
     306    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
     307    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
    309308let ltl_lin_seq_inv_rect_Type4 hterm h1 h2 h3 h4 =
    310309  let hcut = ltl_lin_seq_rect_Type4 h1 h2 h3 h4 hterm in hcut __
    311310
    312311(** val ltl_lin_seq_inv_rect_Type3 :
    313     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    314     Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
    315     'a1) -> 'a1 **)
     312    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
     313    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
    316314let ltl_lin_seq_inv_rect_Type3 hterm h1 h2 h3 h4 =
    317315  let hcut = ltl_lin_seq_rect_Type3 h1 h2 h3 h4 hterm in hcut __
    318316
    319317(** val ltl_lin_seq_inv_rect_Type2 :
    320     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    321     Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
    322     'a1) -> 'a1 **)
     318    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
     319    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
    323320let ltl_lin_seq_inv_rect_Type2 hterm h1 h2 h3 h4 =
    324321  let hcut = ltl_lin_seq_rect_Type2 h1 h2 h3 h4 hterm in hcut __
    325322
    326323(** val ltl_lin_seq_inv_rect_Type1 :
    327     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    328     Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
    329     'a1) -> 'a1 **)
     324    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
     325    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
    330326let ltl_lin_seq_inv_rect_Type1 hterm h1 h2 h3 h4 =
    331327  let hcut = ltl_lin_seq_rect_Type1 h1 h2 h3 h4 hterm in hcut __
    332328
    333329(** val ltl_lin_seq_inv_rect_Type0 :
    334     ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    335     Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ ->
    336     'a1) -> 'a1 **)
     330    ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1)
     331    -> (Graphs.label -> __ -> 'a1) -> 'a1 **)
    337332let ltl_lin_seq_inv_rect_Type0 hterm h1 h2 h3 h4 =
    338333  let hcut = ltl_lin_seq_rect_Type0 h1 h2 h3 h4 hterm in hcut __
     
    344339     | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
    345340     | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
    346      | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
    347      | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
     341     | LOW_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)
     342     | HIGH_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)) y
    348343
    349344(** val ltl_lin_seq_jmdiscr : ltl_lin_seq -> ltl_lin_seq -> __ **)
     
    353348     | SAVE_CARRY -> Obj.magic (fun _ dH -> dH)
    354349     | RESTORE_CARRY -> Obj.magic (fun _ dH -> dH)
    355      | LOW_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
    356      | HIGH_ADDRESS (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
     350     | LOW_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)
     351     | HIGH_ADDRESS a0 -> Obj.magic (fun _ dH -> dH __)) y
    357352
    358353(** val ltl_lin_seq_labels : ltl_lin_seq -> Graphs.label List.list **)
     
    360355| SAVE_CARRY -> List.Nil
    361356| RESTORE_CARRY -> List.Nil
    362 | LOW_ADDRESS (x, lbl) -> List.Cons (lbl, List.Nil)
    363 | HIGH_ADDRESS (x, lbl) -> List.Cons (lbl, List.Nil)
     357| LOW_ADDRESS lbl -> List.Cons (lbl, List.Nil)
     358| HIGH_ADDRESS lbl -> List.Cons (lbl, List.Nil)
    364359
    365360(** val lTL_LIN_uns : Joint.unserialized_params **)
  • extracted/joint_LTL_LIN.mli

    r2951 r3019  
    192192| SAVE_CARRY
    193193| RESTORE_CARRY
    194 | LOW_ADDRESS of I8051.register * Graphs.label
    195 | HIGH_ADDRESS of I8051.register * Graphs.label
     194| LOW_ADDRESS of Graphs.label
     195| HIGH_ADDRESS of Graphs.label
    196196
    197197val ltl_lin_seq_rect_Type4 :
    198   'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
    199   Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
     198  'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
     199  -> 'a1
    200200
    201201val ltl_lin_seq_rect_Type5 :
    202   'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
    203   Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
     202  'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
     203  -> 'a1
    204204
    205205val ltl_lin_seq_rect_Type3 :
    206   'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
    207   Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
     206  'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
     207  -> 'a1
    208208
    209209val ltl_lin_seq_rect_Type2 :
    210   'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
    211   Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
     210  'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
     211  -> 'a1
    212212
    213213val ltl_lin_seq_rect_Type1 :
    214   'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
    215   Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
     214  'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
     215  -> 'a1
    216216
    217217val ltl_lin_seq_rect_Type0 :
    218   'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
    219   Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
     218  'a1 -> 'a1 -> (Graphs.label -> 'a1) -> (Graphs.label -> 'a1) -> ltl_lin_seq
     219  -> 'a1
    220220
    221221val ltl_lin_seq_inv_rect_Type4 :
    222   ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    223   Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
    224   -> 'a1
     222  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
     223  (Graphs.label -> __ -> 'a1) -> 'a1
    225224
    226225val ltl_lin_seq_inv_rect_Type3 :
    227   ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    228   Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
    229   -> 'a1
     226  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
     227  (Graphs.label -> __ -> 'a1) -> 'a1
    230228
    231229val ltl_lin_seq_inv_rect_Type2 :
    232   ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    233   Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
    234   -> 'a1
     230  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
     231  (Graphs.label -> __ -> 'a1) -> 'a1
    235232
    236233val ltl_lin_seq_inv_rect_Type1 :
    237   ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    238   Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
    239   -> 'a1
     234  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
     235  (Graphs.label -> __ -> 'a1) -> 'a1
    240236
    241237val ltl_lin_seq_inv_rect_Type0 :
    242   ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
    243   Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
    244   -> 'a1
     238  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Graphs.label -> __ -> 'a1) ->
     239  (Graphs.label -> __ -> 'a1) -> 'a1
    245240
    246241val ltl_lin_seq_discr : ltl_lin_seq -> ltl_lin_seq -> __
  • extracted/joint_LTL_LIN_semantics.ml

    r2997 r3019  
    235235      (Monad.m_return0 (Monad.max_def Errors.res0)
    236236        (Joint_semantics.set_carry lTL_LIN_state carry st))
    237   | Joint_LTL_LIN.LOW_ADDRESS (r, l) ->
     237  | Joint_LTL_LIN.LOW_ADDRESS l ->
    238238    Obj.magic
    239239      (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    244244        in
    245245        let regs =
    246           SemanticsUtils.hwreg_store r addrl
     246          SemanticsUtils.hwreg_store I8051.RegisterA addrl
    247247            (Obj.magic st.Joint_semantics.regs)
    248248        in
    249249        Monad.m_return0 (Monad.max_def Errors.res0)
    250250          (Joint_semantics.set_regs lTL_LIN_state (Obj.magic regs) st)))
    251   | Joint_LTL_LIN.HIGH_ADDRESS (r, l) ->
     251  | Joint_LTL_LIN.HIGH_ADDRESS l ->
    252252    Obj.magic
    253253      (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    258258        in
    259259        let regs =
    260           SemanticsUtils.hwreg_store r addrh
     260          SemanticsUtils.hwreg_store I8051.RegisterA addrh
    261261            (Obj.magic st.Joint_semantics.regs)
    262262        in
  • extracted/lINToASM.ml

    r3001 r3019  
    143143    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    144144    -> 'a1 **)
    145 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_5553 =
     145let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_263 =
    146146  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    147147    ident_map0; label_map = label_map0; address_map = address_map0;
    148     fresh_cost_label = fresh_cost_label0 } = x_5553
     148    fresh_cost_label = fresh_cost_label0 } = x_263
    149149  in
    150150  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    157157    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    158158    -> 'a1 **)
    159 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_5555 =
     159let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_265 =
    160160  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    161161    ident_map0; label_map = label_map0; address_map = address_map0;
    162     fresh_cost_label = fresh_cost_label0 } = x_5555
     162    fresh_cost_label = fresh_cost_label0 } = x_265
    163163  in
    164164  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    171171    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    172172    -> 'a1 **)
    173 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_5557 =
     173let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_267 =
    174174  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    175175    ident_map0; label_map = label_map0; address_map = address_map0;
    176     fresh_cost_label = fresh_cost_label0 } = x_5557
     176    fresh_cost_label = fresh_cost_label0 } = x_267
    177177  in
    178178  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    185185    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    186186    -> 'a1 **)
    187 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_5559 =
     187let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_269 =
    188188  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    189189    ident_map0; label_map = label_map0; address_map = address_map0;
    190     fresh_cost_label = fresh_cost_label0 } = x_5559
     190    fresh_cost_label = fresh_cost_label0 } = x_269
    191191  in
    192192  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    199199    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    200200    -> 'a1 **)
    201 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_5561 =
     201let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_271 =
    202202  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    203203    ident_map0; label_map = label_map0; address_map = address_map0;
    204     fresh_cost_label = fresh_cost_label0 } = x_5561
     204    fresh_cost_label = fresh_cost_label0 } = x_271
    205205  in
    206206  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    213213    Identifiers.identifier_map -> __ -> Positive.pos -> 'a1) -> aSM_universe
    214214    -> 'a1 **)
    215 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_5563 =
     215let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_273 =
    216216  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    217217    ident_map0; label_map = label_map0; address_map = address_map0;
    218     fresh_cost_label = fresh_cost_label0 } = x_5563
     218    fresh_cost_label = fresh_cost_label0 } = x_273
    219219  in
    220220  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    320320  let globals_addr_internal = fun res_offset x_size ->
    321321    let { Types.fst = res; Types.snd = offset } = res_offset in
    322     let { Types.fst = eta27394; Types.snd = data } = x_size in
    323     let { Types.fst = x; Types.snd = region } = eta27394 in
     322    let { Types.fst = eta11; Types.snd = data } = x_size in
     323    let { Types.fst = x; Types.snd = region } = eta11 in
    324324    { Types.fst =
    325325    (Identifiers.add PreIdentifiers.SymbolTag res x
     
    333333      (Identifiers.empty_map PreIdentifiers.SymbolTag); Types.snd =
    334334      (Z.zopp
    335         (Z.z_of_nat
    336           (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p))) }
     335        (Z.z_of_nat (Nat.S
     336          (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p)))) }
    337337      (AST.prog_vars p.Joint.joint_prog)
    338338  in
     
    352352        (Identifiers.empty_map PreIdentifiers.LabelTag)
    353353    in
    354     let { Types.fst = eta27395; Types.snd = lmap0 } =
     354    let { Types.fst = eta12; Types.snd = lmap0 } =
    355355      match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
    356356      | Types.None ->
     
    364364          lmap }
    365365    in
    366     let { Types.fst = id; Types.snd = univ } = eta27395 in
     366    let { Types.fst = id; Types.snd = univ } = eta12 in
    367367    { Types.fst = { id_univ = univ; current_funct = current; ident_map =
    368368    u.ident_map; label_map =
     
    377377  Obj.magic (fun u ->
    378378    let imap = u.ident_map in
    379     let { Types.fst = eta27396; Types.snd = imap0 } =
     379    let { Types.fst = eta13; Types.snd = imap0 } =
    380380      match Identifiers.lookup PreIdentifiers.SymbolTag imap i with
    381381      | Types.None ->
     
    389389          imap }
    390390    in
    391     let { Types.fst = id; Types.snd = univ } = eta27396 in
     391    let { Types.fst = id; Types.snd = univ } = eta13 in
    392392    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
    393393    ident_map = imap0; label_map = u.label_map; address_map = u.address_map;
     
    990990             (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inr { Types.fst =
    991991             ASM.CARRY; Types.snd = asm_other_bit }))))
    992          | Joint_LTL_LIN.LOW_ADDRESS (reg, lbl) ->
     992         | Joint_LTL_LIN.LOW_ADDRESS lbl ->
    993993           Monad.m_bind0 (Monad.smax_def State.state_monad)
    994994             (identifier_of_label globals lbl) (fun lbl' ->
    995995             Monad.m_return0 (Monad.smax_def State.state_monad)
    996                (ASM.MovSuccessor ((register_address reg), ASM.LOW, lbl')))
    997          | Joint_LTL_LIN.HIGH_ADDRESS (reg, lbl) ->
     996               (ASM.MovSuccessor ((register_address I8051.RegisterA),
     997               ASM.LOW, lbl')))
     998         | Joint_LTL_LIN.HIGH_ADDRESS lbl ->
    998999           Monad.m_bind0 (Monad.smax_def State.state_monad)
    9991000             (identifier_of_label globals lbl) (fun lbl' ->
    10001001             Monad.m_return0 (Monad.smax_def State.state_monad)
    1001                (ASM.MovSuccessor ((register_address reg), ASM.HIGH, lbl'))))))
     1002               (ASM.MovSuccessor ((register_address I8051.RegisterA),
     1003               ASM.HIGH, lbl'))))))
    10021004| Joint.Final instr ->
    10031005  (match instr with
     
    10761078    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    10771079    -> 'a1 **)
    1078 let rec init_mutable_rect_Type4 h_mk_init_mutable x_5580 =
     1080let rec init_mutable_rect_Type4 h_mk_init_mutable x_290 =
    10791081  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1080     built0 } = x_5580
     1082    built0 } = x_290
    10811083  in
    10821084  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    10851087    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    10861088    -> 'a1 **)
    1087 let rec init_mutable_rect_Type5 h_mk_init_mutable x_5582 =
     1089let rec init_mutable_rect_Type5 h_mk_init_mutable x_292 =
    10881090  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1089     built0 } = x_5582
     1091    built0 } = x_292
    10901092  in
    10911093  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    10941096    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    10951097    -> 'a1 **)
    1096 let rec init_mutable_rect_Type3 h_mk_init_mutable x_5584 =
     1098let rec init_mutable_rect_Type3 h_mk_init_mutable x_294 =
    10971099  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1098     built0 } = x_5584
     1100    built0 } = x_294
    10991101  in
    11001102  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    11031105    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    11041106    -> 'a1 **)
    1105 let rec init_mutable_rect_Type2 h_mk_init_mutable x_5586 =
     1107let rec init_mutable_rect_Type2 h_mk_init_mutable x_296 =
    11061108  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1107     built0 } = x_5586
     1109    built0 } = x_296
    11081110  in
    11091111  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    11121114    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    11131115    -> 'a1 **)
    1114 let rec init_mutable_rect_Type1 h_mk_init_mutable x_5588 =
     1116let rec init_mutable_rect_Type1 h_mk_init_mutable x_298 =
    11151117  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1116     built0 } = x_5588
     1118    built0 } = x_298
    11171119  in
    11181120  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    11211123    (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
    11221124    -> 'a1 **)
    1123 let rec init_mutable_rect_Type0 h_mk_init_mutable x_5590 =
     1125let rec init_mutable_rect_Type0 h_mk_init_mutable x_300 =
    11241126  let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built =
    1125     built0 } = x_5590
     1127    built0 } = x_300
    11261128  in
    11271129  h_mk_init_mutable virtual_dptr0 actual_dptr0 built0
     
    12951297      let start_sp =
    12961298        Z.zopp
    1297           (Z.z_of_nat
    1298             (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p))
     1299          (Z.z_of_nat (Nat.S
     1300            (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p)))
    12991301      in
    13001302      let { Types.fst = sph; Types.snd = spl } =
  • extracted/liveness.ml

    r3009 r3019  
    120120
    121121open ERTL
    122 
    123 open ERTLptr
    124122
    125123open Set_adt
     
    226224      | Joint.Extension_seq ext ->
    227225        (match Obj.magic ext with
    228          | ERTLptr.Ertlptr_ertl ext' ->
    229            (match ext' with
    230             | ERTL.Ertl_new_frame ->
    231               rl_join (rl_hsingleton I8051.registerSPL)
    232                 (rl_hsingleton I8051.registerSPH)
    233             | ERTL.Ertl_del_frame ->
    234               rl_join (rl_hsingleton I8051.registerSPL)
    235                 (rl_hsingleton I8051.registerSPH)
    236             | ERTL.Ertl_frame_size r -> rl_psingleton r)
    237          | ERTLptr.LOW_ADDRESS (r1, l0) -> rl_psingleton r1
    238          | ERTLptr.HIGH_ADDRESS (r1, l0) -> rl_psingleton r1)))
     226         | ERTL.Ertl_new_frame ->
     227           rl_join (rl_hsingleton I8051.registerSPL)
     228             (rl_hsingleton I8051.registerSPH)
     229         | ERTL.Ertl_del_frame ->
     230           rl_join (rl_hsingleton I8051.registerSPL)
     231             (rl_hsingleton I8051.registerSPH)
     232         | ERTL.Ertl_frame_size r -> rl_psingleton r)))
    239233| Joint.Final x -> rl_bottom
    240234| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
     
    306300      | Joint.Extension_seq ext ->
    307301        (match Obj.magic ext with
    308          | ERTLptr.Ertlptr_ertl ext' ->
    309            (match ext' with
    310             | ERTL.Ertl_new_frame ->
    311               Obj.magic
    312                 (rl_join (rl_hsingleton I8051.registerSPL)
    313                   (rl_hsingleton I8051.registerSPH))
    314             | ERTL.Ertl_del_frame ->
    315               Obj.magic
    316                 (rl_join (rl_hsingleton I8051.registerSPL)
    317                   (rl_hsingleton I8051.registerSPH))
    318             | ERTL.Ertl_frame_size r -> Obj.magic rl_bottom)
    319          | ERTLptr.LOW_ADDRESS (r1, l0) -> Obj.magic rl_bottom
    320          | ERTLptr.HIGH_ADDRESS (r1, l0) -> Obj.magic rl_bottom)))
     302         | ERTL.Ertl_new_frame ->
     303           Obj.magic
     304             (rl_join (rl_hsingleton I8051.registerSPL)
     305               (rl_hsingleton I8051.registerSPH))
     306         | ERTL.Ertl_del_frame ->
     307           Obj.magic
     308             (rl_join (rl_hsingleton I8051.registerSPL)
     309               (rl_hsingleton I8051.registerSPH))
     310         | ERTL.Ertl_frame_size r -> Obj.magic rl_bottom)))
    321311| Joint.Final fin ->
    322312  (match fin with
     
    407397      | Joint.Extension_seq ext ->
    408398        (match Obj.magic ext with
    409          | ERTLptr.Ertlptr_ertl ext' ->
    410            (match ext' with
    411             | ERTL.Ertl_new_frame -> Bool.False
    412             | ERTL.Ertl_del_frame -> Bool.False
    413             | ERTL.Ertl_frame_size r ->
    414               Bool.notb
    415                 (Set_adt.set_member
    416                   (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r
    417                   pliveafter))
    418          | ERTLptr.LOW_ADDRESS (r1, l') ->
     399         | ERTL.Ertl_new_frame -> Bool.False
     400         | ERTL.Ertl_del_frame -> Bool.False
     401         | ERTL.Ertl_frame_size r ->
    419402           Bool.notb
    420403             (Set_adt.set_member
    421                (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r1
    422                pliveafter)
    423          | ERTLptr.HIGH_ADDRESS (r1, l') ->
    424            Bool.notb
    425              (Set_adt.set_member
    426                (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r1
     404               (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r
    427405               pliveafter))))
    428406
     
    465443    List.fold rl_join rl_bottom (fun successor -> Bool.True)
    466444      (fun successor -> livebefore globals int_fun liveafter0 successor)
    467       (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars ERTLptr.eRTLptr);
     445      (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars ERTL.eRTL);
    468446        Joint.succ_label = (Obj.magic (fun x -> Types.Some x));
    469447        Joint.has_fcond = Bool.False } globals stmt)
  • extracted/liveness.mli

    r2951 r3019  
    121121open ERTL
    122122
    123 open ERTLptr
    124 
    125123open Set_adt
    126124
  • extracted/semantics.ml

    r3001 r3019  
    5555open LTL
    5656
    57 open ERTLptrToLTL
    58 
    59 open ERTLptr
    60 
    61 open ERTLToERTLptr
     57open ERTLToLTL
    6258
    6359open ERTL
     
    306302
    307303open ERTL_semantics
    308 
    309 open ERTLptr_semantics
    310304
    311305open Joint_LTL_LIN_semantics
     
    324318    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    325319    preclassified_system_pass -> 'a1 **)
    326 let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_16776 =
    327   let pcs_pcs = x_16776 in h_mk_preclassified_system_pass pcs_pcs __
     320let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_211 =
     321  let pcs_pcs = x_211 in h_mk_preclassified_system_pass pcs_pcs __
    328322
    329323(** val preclassified_system_pass_rect_Type5 :
    330324    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    331325    preclassified_system_pass -> 'a1 **)
    332 let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_16778 =
    333   let pcs_pcs = x_16778 in h_mk_preclassified_system_pass pcs_pcs __
     326let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_213 =
     327  let pcs_pcs = x_213 in h_mk_preclassified_system_pass pcs_pcs __
    334328
    335329(** val preclassified_system_pass_rect_Type3 :
    336330    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    337331    preclassified_system_pass -> 'a1 **)
    338 let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_16780 =
    339   let pcs_pcs = x_16780 in h_mk_preclassified_system_pass pcs_pcs __
     332let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_215 =
     333  let pcs_pcs = x_215 in h_mk_preclassified_system_pass pcs_pcs __
    340334
    341335(** val preclassified_system_pass_rect_Type2 :
    342336    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    343337    preclassified_system_pass -> 'a1 **)
    344 let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_16782 =
    345   let pcs_pcs = x_16782 in h_mk_preclassified_system_pass pcs_pcs __
     338let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_217 =
     339  let pcs_pcs = x_217 in h_mk_preclassified_system_pass pcs_pcs __
    346340
    347341(** val preclassified_system_pass_rect_Type1 :
    348342    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    349343    preclassified_system_pass -> 'a1 **)
    350 let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_16784 =
    351   let pcs_pcs = x_16784 in h_mk_preclassified_system_pass pcs_pcs __
     344let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_219 =
     345  let pcs_pcs = x_219 in h_mk_preclassified_system_pass pcs_pcs __
    352346
    353347(** val preclassified_system_pass_rect_Type0 :
    354348    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    355349    preclassified_system_pass -> 'a1 **)
    356 let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_16786 =
    357   let pcs_pcs = x_16786 in h_mk_preclassified_system_pass pcs_pcs __
     350let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_221 =
     351  let pcs_pcs = x_221 in h_mk_preclassified_system_pass pcs_pcs __
    358352
    359353(** val pcs_pcs :
     
    432426      (SemanticsUtils.sem_graph_params_to_sem_params
    433427        ERTL_semantics.eRTL_semantics))
    434 | Compiler.Ertlptr_pass ->
    435   (fun x ->
    436     Joint_fullexec.joint_preclassified_system
    437       (SemanticsUtils.sem_graph_params_to_sem_params
    438         ERTLptr_semantics.eRTLptr_semantics))
    439428| Compiler.Ltl_pass ->
    440429  (fun x ->
     
    447436| Compiler.Assembly_pass ->
    448437  (fun prog ->
    449     let { Types.fst = eta29797; Types.snd = policy } = Obj.magic prog in
    450     let { Types.fst = code; Types.snd = sigma } = eta29797 in
     438    let { Types.fst = eta19; Types.snd = policy } = Obj.magic prog in
     439    let { Types.fst = code; Types.snd = sigma } = eta19 in
    451440    Interpret2.aSM_preclassified_system code sigma policy)
    452441| Compiler.Object_code_pass ->
  • extracted/semantics.mli

    r2951 r3019  
    5555open LTL
    5656
    57 open ERTLptrToLTL
    58 
    59 open ERTLptr
    60 
    61 open ERTLToERTLptr
     57open ERTLToLTL
    6258
    6359open ERTL
     
    306302
    307303open ERTL_semantics
    308 
    309 open ERTLptr_semantics
    310304
    311305open Joint_LTL_LIN_semantics
  • extracted/traces.ml

    r3001 r3019  
    157157    Joint_semantics.sem_params -> (AST.ident List.list ->
    158158    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    159 let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_15969 =
    160   let { globals = globals0; ev_genv = ev_genv0 } = x_15969 in
     159let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_316 =
     160  let { globals = globals0; ev_genv = ev_genv0 } = x_316 in
    161161  h_mk_evaluation_params globals0 ev_genv0
    162162
     
    164164    Joint_semantics.sem_params -> (AST.ident List.list ->
    165165    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    166 let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_15971 =
    167   let { globals = globals0; ev_genv = ev_genv0 } = x_15971 in
     166let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_318 =
     167  let { globals = globals0; ev_genv = ev_genv0 } = x_318 in
    168168  h_mk_evaluation_params globals0 ev_genv0
    169169
     
    171171    Joint_semantics.sem_params -> (AST.ident List.list ->
    172172    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    173 let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_15973 =
    174   let { globals = globals0; ev_genv = ev_genv0 } = x_15973 in
     173let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_320 =
     174  let { globals = globals0; ev_genv = ev_genv0 } = x_320 in
    175175  h_mk_evaluation_params globals0 ev_genv0
    176176
     
    178178    Joint_semantics.sem_params -> (AST.ident List.list ->
    179179    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    180 let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_15975 =
    181   let { globals = globals0; ev_genv = ev_genv0 } = x_15975 in
     180let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_322 =
     181  let { globals = globals0; ev_genv = ev_genv0 } = x_322 in
    182182  h_mk_evaluation_params globals0 ev_genv0
    183183
     
    185185    Joint_semantics.sem_params -> (AST.ident List.list ->
    186186    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    187 let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_15977 =
    188   let { globals = globals0; ev_genv = ev_genv0 } = x_15977 in
     187let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_324 =
     188  let { globals = globals0; ev_genv = ev_genv0 } = x_324 in
    189189  h_mk_evaluation_params globals0 ev_genv0
    190190
     
    192192    Joint_semantics.sem_params -> (AST.ident List.list ->
    193193    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    194 let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_15979 =
    195   let { globals = globals0; ev_genv = ev_genv0 } = x_15979 in
     194let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_326 =
     195  let { globals = globals0; ev_genv = ev_genv0 } = x_326 in
    196196  h_mk_evaluation_params globals0 ev_genv0
    197197
     
    336336    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    337337    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    338 let rec prog_params_rect_Type4 h_mk_prog_params x_15995 =
     338let rec prog_params_rect_Type4 h_mk_prog_params x_342 =
    339339  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    340     stack_sizes0 } = x_15995
     340    stack_sizes0 } = x_342
    341341  in
    342342  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    345345    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    346346    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    347 let rec prog_params_rect_Type5 h_mk_prog_params x_15997 =
     347let rec prog_params_rect_Type5 h_mk_prog_params x_344 =
    348348  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    349     stack_sizes0 } = x_15997
     349    stack_sizes0 } = x_344
    350350  in
    351351  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    354354    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    355355    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    356 let rec prog_params_rect_Type3 h_mk_prog_params x_15999 =
     356let rec prog_params_rect_Type3 h_mk_prog_params x_346 =
    357357  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    358     stack_sizes0 } = x_15999
     358    stack_sizes0 } = x_346
    359359  in
    360360  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    363363    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    364364    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    365 let rec prog_params_rect_Type2 h_mk_prog_params x_16001 =
     365let rec prog_params_rect_Type2 h_mk_prog_params x_348 =
    366366  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    367     stack_sizes0 } = x_16001
     367    stack_sizes0 } = x_348
    368368  in
    369369  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    372372    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    373373    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    374 let rec prog_params_rect_Type1 h_mk_prog_params x_16003 =
     374let rec prog_params_rect_Type1 h_mk_prog_params x_350 =
    375375  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    376     stack_sizes0 } = x_16003
     376    stack_sizes0 } = x_350
    377377  in
    378378  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    381381    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    382382    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    383 let rec prog_params_rect_Type0 h_mk_prog_params x_16005 =
     383let rec prog_params_rect_Type0 h_mk_prog_params x_352 =
    384384  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    385     stack_sizes0 } = x_16005
     385    stack_sizes0 } = x_352
    386386  in
    387387  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    523523        (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    524524          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    525           (Nat.S Nat.O)))))))))))))))) (Z.zopp (Z.z_of_nat globals_size))) }
     525          (Nat.S Nat.O))))))))))))))))
     526          (Z.zopp (Z.z_of_nat (Nat.S globals_size)))) }
    526527      in
    527528      let main = AST.prog_main p.Joint.joint_prog in
  • extracted/uses.ml

    r3011 r3019  
    121121open ERTL
    122122
    123 open ERTLptr
    124 
    125123(** val examine_internal :
    126124    AST.ident List.list -> Joint.joint_internal_function -> Positive.pos
     
    183181          | Joint.Extension_seq s1 ->
    184182            (match Obj.magic s1 with
    185              | ERTLptr.Ertlptr_ertl s2 ->
    186                (match s2 with
    187                 | ERTL.Ertl_new_frame -> map
    188                 | ERTL.Ertl_del_frame -> map
    189                 | ERTL.Ertl_frame_size r -> incr r map)
    190              | ERTLptr.LOW_ADDRESS (r, x1) -> incr r map
    191              | ERTLptr.HIGH_ADDRESS (r, x1) -> incr r map)))
     183             | ERTL.Ertl_new_frame -> map
     184             | ERTL.Ertl_del_frame -> map
     185             | ERTL.Ertl_frame_size r -> incr r map)))
    192186    | Joint.Final x0 -> map
    193187    | Joint.FCOND (x0, x1, x2) -> assert false (* absurd case *)
  • extracted/uses.mli

    r2951 r3019  
    121121open ERTL
    122122
    123 open ERTLptr
    124 
    125123val examine_internal :
    126124  AST.ident List.list -> Joint.joint_internal_function -> Positive.pos
Note: See TracChangeset for help on using the changeset viewer.