Changeset 2875 for extracted


Ignore:
Timestamp:
Mar 15, 2013, 1:32:50 AM (7 years ago)
Author:
sacerdot
Message:

Pretty printing of object code integrated too.
A couple of axioms make execution via the preclassified_system
raise assert false.

Location:
extracted
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.ml

    r2873 r2875  
    258258| Ltl_pass
    259259| Lin_pass
     260| Assembly_pass
     261| Object_code_pass
    260262
    261263(** val pass_rect_Type4 :
    262264    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    263     -> 'a1 -> pass -> 'a1 **)
    264 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 = function
     265    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
     266let 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
    265267| Clight_pass -> h_clight_pass
    266268| Clight_switch_removed_pass -> h_clight_switch_removed_pass
     
    275277| Ltl_pass -> h_ltl_pass
    276278| Lin_pass -> h_lin_pass
     279| Assembly_pass -> h_assembly_pass
     280| Object_code_pass -> h_object_code_pass
    277281
    278282(** val pass_rect_Type5 :
    279283    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    280     -> 'a1 -> pass -> 'a1 **)
    281 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 = function
     284    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
     285let 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
    282286| Clight_pass -> h_clight_pass
    283287| Clight_switch_removed_pass -> h_clight_switch_removed_pass
     
    292296| Ltl_pass -> h_ltl_pass
    293297| Lin_pass -> h_lin_pass
     298| Assembly_pass -> h_assembly_pass
     299| Object_code_pass -> h_object_code_pass
    294300
    295301(** val pass_rect_Type3 :
    296302    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    297     -> 'a1 -> pass -> 'a1 **)
    298 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 = function
     303    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
     304let 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
    299305| Clight_pass -> h_clight_pass
    300306| Clight_switch_removed_pass -> h_clight_switch_removed_pass
     
    309315| Ltl_pass -> h_ltl_pass
    310316| Lin_pass -> h_lin_pass
     317| Assembly_pass -> h_assembly_pass
     318| Object_code_pass -> h_object_code_pass
    311319
    312320(** val pass_rect_Type2 :
    313321    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    314     -> 'a1 -> pass -> 'a1 **)
    315 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 = function
     322    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
     323let 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
    316324| Clight_pass -> h_clight_pass
    317325| Clight_switch_removed_pass -> h_clight_switch_removed_pass
     
    326334| Ltl_pass -> h_ltl_pass
    327335| Lin_pass -> h_lin_pass
     336| Assembly_pass -> h_assembly_pass
     337| Object_code_pass -> h_object_code_pass
    328338
    329339(** val pass_rect_Type1 :
    330340    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    331     -> 'a1 -> pass -> 'a1 **)
    332 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 = function
     341    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
     342let 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
    333343| Clight_pass -> h_clight_pass
    334344| Clight_switch_removed_pass -> h_clight_switch_removed_pass
     
    343353| Ltl_pass -> h_ltl_pass
    344354| Lin_pass -> h_lin_pass
     355| Assembly_pass -> h_assembly_pass
     356| Object_code_pass -> h_object_code_pass
    345357
    346358(** val pass_rect_Type0 :
    347359    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    348     -> '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 = function
     360    -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1 **)
     361let 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
    350362| Clight_pass -> h_clight_pass
    351363| Clight_switch_removed_pass -> h_clight_switch_removed_pass
     
    360372| Ltl_pass -> h_ltl_pass
    361373| Lin_pass -> h_lin_pass
     374| Assembly_pass -> h_assembly_pass
     375| Object_code_pass -> h_object_code_pass
    362376
    363377(** val pass_inv_rect_Type4 :
    364378    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    365379    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    366     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
    367 let 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
     380    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
     381    -> 'a1 **)
     382let pass_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
     383  let hcut =
     384    pass_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
     385  in
    369386  hcut __
    370387
     
    372389    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    373390    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    374     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
    375 let 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
     391    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
     392    -> 'a1 **)
     393let pass_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
     394  let hcut =
     395    pass_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
     396  in
    377397  hcut __
    378398
     
    380400    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    381401    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    382     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
    383 let 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
     402    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
     403    -> 'a1 **)
     404let pass_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
     405  let hcut =
     406    pass_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
     407  in
    385408  hcut __
    386409
     
    388411    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    389412    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    390     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
    391 let 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
     413    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
     414    -> 'a1 **)
     415let pass_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
     416  let hcut =
     417    pass_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
     418  in
    393419  hcut __
    394420
     
    396422    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    397423    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    398     (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
    399 let 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
     424    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
     425    -> 'a1 **)
     426let pass_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 =
     427  let hcut =
     428    pass_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 hterm
     429  in
    401430  hcut __
    402431
     
    416445     | Ertlptr_pass -> Obj.magic (fun _ dH -> dH)
    417446     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
    418      | Lin_pass -> Obj.magic (fun _ dH -> dH)) y
     447     | Lin_pass -> Obj.magic (fun _ dH -> dH)
     448     | Assembly_pass -> Obj.magic (fun _ dH -> dH)
     449     | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y
    419450
    420451(** val pass_jmdiscr : pass -> pass -> __ **)
     
    433464     | Ertlptr_pass -> Obj.magic (fun _ dH -> dH)
    434465     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
    435      | Lin_pass -> Obj.magic (fun _ dH -> dH)) y
     466     | Lin_pass -> Obj.magic (fun _ dH -> dH)
     467     | Assembly_pass -> Obj.magic (fun _ dH -> dH)
     468     | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y
    436469
    437470type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod
     
    510543  let i2 = Obj.magic observe Ertlptr_pass { Types.fst = p2; Types.snd = st1 }
    511544  in
    512   let { Types.fst = eta29104; Types.snd = max_stack } =
     545  let { Types.fst = eta2; Types.snd = max_stack } =
    513546    ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
    514547  in
    515   let { Types.fst = p3; Types.snd = stack_cost } = eta29104 in
     548  let { Types.fst = p3; Types.snd = stack_cost } = eta2 in
    516549  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in
    517550  let i3 = Obj.magic observe Ltl_pass { Types.fst = p3; Types.snd = st2 } in
     
    525558        (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
    526559          (LINToASM.lin_to_asm p4))) (fun p5 ->
     560      let i5 = observe Assembly_pass p5 in
    527561      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
    528562        p5; Types.snd = stack_cost }; Types.snd = max_stack }))
     
    541575
    542576(** val assembler :
    543     ASM.pseudo_assembly_program -> ASM.labelled_object_code Errors.res **)
    544 let assembler p =
     577    observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
     578    Errors.res **)
     579let assembler observe p =
    545580  Obj.magic
    546581    (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    550585      let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
    551586      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
    552       Obj.magic (Errors.OK (Types.pi1 (Assembly.assembly p sigma pol)))))
     587      let p0 = Assembly.assembly p sigma pol in
     588      let i = Obj.magic observe Object_code_pass (Types.pi1 p0) in
     589      Obj.magic (Errors.OK (Types.pi1 p0))))
    553590
    554591open AbstractStatus
     
    586623    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    587624    compiler_output -> 'a1 **)
    588 let rec compiler_output_rect_Type4 h_mk_compiler_output x_25364 =
     625let rec compiler_output_rect_Type4 h_mk_compiler_output x_198 =
    589626  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    590627    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    591     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25364
     628    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_198
    592629  in
    593630  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    598635    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    599636    compiler_output -> 'a1 **)
    600 let rec compiler_output_rect_Type5 h_mk_compiler_output x_25366 =
     637let rec compiler_output_rect_Type5 h_mk_compiler_output x_200 =
    601638  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    602639    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    603     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25366
     640    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_200
    604641  in
    605642  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    610647    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    611648    compiler_output -> 'a1 **)
    612 let rec compiler_output_rect_Type3 h_mk_compiler_output x_25368 =
     649let rec compiler_output_rect_Type3 h_mk_compiler_output x_202 =
    613650  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    614651    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    615     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25368
     652    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_202
    616653  in
    617654  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    622659    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    623660    compiler_output -> 'a1 **)
    624 let rec compiler_output_rect_Type2 h_mk_compiler_output x_25370 =
     661let rec compiler_output_rect_Type2 h_mk_compiler_output x_204 =
    625662  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    626663    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    627     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25370
     664    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_204
    628665  in
    629666  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    634671    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    635672    compiler_output -> 'a1 **)
    636 let rec compiler_output_rect_Type1 h_mk_compiler_output x_25372 =
     673let rec compiler_output_rect_Type1 h_mk_compiler_output x_206 =
    637674  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    638675    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    639     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25372
     676    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_206
    640677  in
    641678  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    646683    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    647684    compiler_output -> 'a1 **)
    648 let rec compiler_output_rect_Type0 h_mk_compiler_output x_25374 =
     685let rec compiler_output_rect_Type0 h_mk_compiler_output x_208 =
    649686  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    650687    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    651     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25374
     688    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_208
    652689  in
    653690  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    735772      Monad.m_bind3 (Monad.max_def Errors.res0)
    736773        (Obj.magic (back_end observe p0)) (fun p1 stack_cost max_stack ->
    737         Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p1))
    738           (fun p2 ->
     774        Monad.m_bind0 (Monad.max_def Errors.res0)
     775          (Obj.magic (assembler observe p1)) (fun p2 ->
    739776          let k = ASMCostsSplit.aSM_cost_map p2 in
    740777          let k' =
  • extracted/compiler.mli

    r2842 r2875  
    258258| Ltl_pass
    259259| Lin_pass
     260| Assembly_pass
     261| Object_code_pass
    260262
    261263val pass_rect_Type4 :
    262264  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    263   -> 'a1 -> pass -> 'a1
     265  -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
    264266
    265267val pass_rect_Type5 :
    266268  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    267   -> 'a1 -> pass -> 'a1
     269  -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
    268270
    269271val pass_rect_Type3 :
    270272  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    271   -> 'a1 -> pass -> 'a1
     273  -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
    272274
    273275val pass_rect_Type2 :
    274276  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    275   -> 'a1 -> pass -> 'a1
     277  -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
    276278
    277279val pass_rect_Type1 :
    278280  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    279   -> 'a1 -> pass -> 'a1
     281  -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
    280282
    281283val pass_rect_Type0 :
    282284  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    283   -> 'a1 -> pass -> 'a1
     285  -> 'a1 -> 'a1 -> 'a1 -> pass -> 'a1
    284286
    285287val pass_inv_rect_Type4 :
    286288  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    287289  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    288   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     290  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
    289291
    290292val pass_inv_rect_Type3 :
    291293  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    292294  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    293   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     295  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
    294296
    295297val pass_inv_rect_Type2 :
    296298  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    297299  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    298   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     300  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
    299301
    300302val pass_inv_rect_Type1 :
    301303  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    302304  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    303   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     305  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
    304306
    305307val pass_inv_rect_Type0 :
    306308  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    307309  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
    308   'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     310  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
    309311
    310312val pass_discr : pass -> pass -> __
     
    353355
    354356val assembler :
    355   ASM.pseudo_assembly_program -> ASM.labelled_object_code Errors.res
     357  observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
     358  Errors.res
    356359
    357360open AbstractStatus
  • extracted/semantics.ml

    r2873 r2875  
    316316
    317317open LIN_semantics
     318
     319open Interpret2
    318320
    319321type preclassified_system_pass =
     
    324326    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    325327    preclassified_system_pass -> 'a1 **)
    326 let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_26392 =
    327   let pcs_pcs = x_26392 in h_mk_preclassified_system_pass pcs_pcs __
     328let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_3 =
     329  let pcs_pcs = x_3 in h_mk_preclassified_system_pass pcs_pcs __
    328330
    329331(** val preclassified_system_pass_rect_Type5 :
    330332    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    331333    preclassified_system_pass -> 'a1 **)
    332 let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_26394 =
    333   let pcs_pcs = x_26394 in h_mk_preclassified_system_pass pcs_pcs __
     334let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_5 =
     335  let pcs_pcs = x_5 in h_mk_preclassified_system_pass pcs_pcs __
    334336
    335337(** val preclassified_system_pass_rect_Type3 :
    336338    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    337339    preclassified_system_pass -> 'a1 **)
    338 let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_26396 =
    339   let pcs_pcs = x_26396 in h_mk_preclassified_system_pass pcs_pcs __
     340let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_7 =
     341  let pcs_pcs = x_7 in h_mk_preclassified_system_pass pcs_pcs __
    340342
    341343(** val preclassified_system_pass_rect_Type2 :
    342344    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    343345    preclassified_system_pass -> 'a1 **)
    344 let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_26398 =
    345   let pcs_pcs = x_26398 in h_mk_preclassified_system_pass pcs_pcs __
     346let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_9 =
     347  let pcs_pcs = x_9 in h_mk_preclassified_system_pass pcs_pcs __
    346348
    347349(** val preclassified_system_pass_rect_Type1 :
    348350    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    349351    preclassified_system_pass -> 'a1 **)
    350 let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_26400 =
    351   let pcs_pcs = x_26400 in h_mk_preclassified_system_pass pcs_pcs __
     352let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_11 =
     353  let pcs_pcs = x_11 in h_mk_preclassified_system_pass pcs_pcs __
    352354
    353355(** val preclassified_system_pass_rect_Type0 :
    354356    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    355357    preclassified_system_pass -> 'a1 **)
    356 let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_26402 =
    357   let pcs_pcs = x_26402 in h_mk_preclassified_system_pass pcs_pcs __
     358let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_13 =
     359  let pcs_pcs = x_13 in h_mk_preclassified_system_pass pcs_pcs __
    358360
    359361(** val pcs_pcs :
     
    405407  Measurable.pcs_exec__o__es1 (pcs_pcs x0 x1)
    406408
     409exception NotImplementedYet
     410
    407411(** val preclassified_system_of_pass :
    408     Compiler.pass -> preclassified_system_pass **)
     412    Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass **)
    409413let preclassified_system_of_pass = function
    410 | Compiler.Clight_pass -> Clight_classified_system.clight_pcs
    411 | Compiler.Clight_switch_removed_pass -> Clight_classified_system.clight_pcs
    412 | Compiler.Clight_label_pass -> Clight_classified_system.clight_pcs
    413 | Compiler.Clight_simplified_pass -> Clight_classified_system.clight_pcs
    414 | Compiler.Cminor_pass -> Cminor_classified_system.cminor_pcs
    415 | Compiler.Rtlabs_pass -> RTLabs_classified_system.rTLabs_pcs
     414| Compiler.Clight_pass -> (fun x -> Clight_classified_system.clight_pcs)
     415| Compiler.Clight_switch_removed_pass ->
     416  (fun x -> Clight_classified_system.clight_pcs)
     417| Compiler.Clight_label_pass ->
     418  (fun x -> Clight_classified_system.clight_pcs)
     419| Compiler.Clight_simplified_pass ->
     420  (fun x -> Clight_classified_system.clight_pcs)
     421| Compiler.Cminor_pass -> (fun x -> Cminor_classified_system.cminor_pcs)
     422| Compiler.Rtlabs_pass -> (fun x -> RTLabs_classified_system.rTLabs_pcs)
    416423| Compiler.Rtl_separate_pass ->
    417   Joint_fullexec.joint_preclassified_system
    418     (SemanticsUtils.sem_graph_params_to_sem_params
    419       RTL_semantics.rTL_semantics_separate)
     424  (fun x ->
     425    Joint_fullexec.joint_preclassified_system
     426      (SemanticsUtils.sem_graph_params_to_sem_params
     427        RTL_semantics.rTL_semantics_separate))
    420428| Compiler.Rtl_uniq_pass ->
    421   Joint_fullexec.joint_preclassified_system
    422     (SemanticsUtils.sem_graph_params_to_sem_params
    423       RTL_semantics.rTL_semantics_unique)
     429  (fun x ->
     430    Joint_fullexec.joint_preclassified_system
     431      (SemanticsUtils.sem_graph_params_to_sem_params
     432        RTL_semantics.rTL_semantics_unique))
    424433| Compiler.Ertl_pass ->
    425   Joint_fullexec.joint_preclassified_system
    426     (SemanticsUtils.sem_graph_params_to_sem_params
    427       ERTL_semantics.eRTL_semantics)
     434  (fun x ->
     435    Joint_fullexec.joint_preclassified_system
     436      (SemanticsUtils.sem_graph_params_to_sem_params
     437        ERTL_semantics.eRTL_semantics))
    428438| Compiler.Ertlptr_pass ->
    429   Joint_fullexec.joint_preclassified_system
    430     (SemanticsUtils.sem_graph_params_to_sem_params
    431       ERTLptr_semantics.eRTLptr_semantics)
     439  (fun x ->
     440    Joint_fullexec.joint_preclassified_system
     441      (SemanticsUtils.sem_graph_params_to_sem_params
     442        ERTLptr_semantics.eRTLptr_semantics))
    432443| Compiler.Ltl_pass ->
    433   Joint_fullexec.joint_preclassified_system
    434     (SemanticsUtils.sem_graph_params_to_sem_params
    435       LTL_semantics.lTL_semantics)
     444  (fun x ->
     445    Joint_fullexec.joint_preclassified_system
     446      (SemanticsUtils.sem_graph_params_to_sem_params
     447        LTL_semantics.lTL_semantics))
    436448| Compiler.Lin_pass ->
    437   Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics
     449  (fun x ->
     450    Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics)
     451| Compiler.Assembly_pass -> (fun prog -> raise NotImplementedYet)
     452| Compiler.Object_code_pass ->
     453  (fun prog -> Interpret2.oC_preclassified_system (Obj.magic prog))
    438454
    439455(** val run_and_print :
     
    443459    Types.unit0 **)
    444460let run_and_print pass prog n print_pass print_event print_error print_exit =
    445   let pcs = preclassified_system_of_pass pass in
     461 try
     462  let pcs = preclassified_system_of_pass pass prog in
    446463  let prog0 = prog in
    447464  let g = (pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0 in
     
    460477      | Errors.Error msg -> print_error msg)
    461478   | Errors.Error msg -> print_error msg)
    462 
     479 with
     480  NotImplementedYet -> Types.It
     481
  • extracted/semantics.mli

    r2867 r2875  
    316316
    317317open LIN_semantics
     318
     319open Interpret2
    318320
    319321type preclassified_system_pass =
     
    377379  SmallstepExec.trans_system
    378380
    379 val preclassified_system_of_pass : Compiler.pass -> preclassified_system_pass
     381val preclassified_system_of_pass :
     382  Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass
    380383
    381384val run_and_print :
Note: See TracChangeset for help on using the changeset viewer.