Changeset 2875


Ignore:
Timestamp:
Mar 15, 2013, 1:32:50 AM (5 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.

Files:
11 edited

Legend:

Unmodified
Added
Removed

  • driver/backendPrinter.ml

    r2868 r2875  
    221221
    222222let print_program pass (program : Extracted.Preamble.__) =
     223 let beprint pcs =
     224  print_graph (pcs (Extracted.Types.fst (Obj.magic program))) in
    223225 let lines =
    224226  match pass with
    225227   | Extracted.Compiler.Rtl_separate_pass ->
    226       Extracted.RTL_printer.print_RTL_program rTL_printing_params
     228      beprint (Extracted.RTL_printer.print_RTL_program rTL_printing_params)
    227229   | Extracted.Compiler.Rtl_uniq_pass ->
    228       Extracted.RTL_printer.print_RTL_program rTL_printing_params
     230      beprint (Extracted.RTL_printer.print_RTL_program rTL_printing_params)
    229231   | Extracted.Compiler.Ertl_pass ->
    230       Extracted.ERTL_printer.print_ERTL_program eRTL_printing_params
     232      beprint (Extracted.ERTL_printer.print_ERTL_program eRTL_printing_params)
    231233   | Extracted.Compiler.Ertlptr_pass ->
    232       Extracted.ERTLptr_printer.print_ERTLptr_program eRTLptr_printing_params
     234      beprint
     235       (Extracted.ERTLptr_printer.print_ERTLptr_program eRTLptr_printing_params)
    233236   | Extracted.Compiler.Ltl_pass ->
    234       Extracted.LTL_printer.print_LTL_program joint_LTL_LIN_printing_params
    235    | _ -> (fun _ -> Extracted.List.Nil)
     237      beprint
     238       (Extracted.LTL_printer.print_LTL_program joint_LTL_LIN_printing_params)
     239   | Extracted.Compiler.Object_code_pass ->
     240      ASMPrinter.print_program (Extracted.ASM.oc (Obj.magic program))
     241   | _ -> ""
    236242 in
    237   "\n" ^ print_graph (lines (Extracted.Types.fst (Obj.magic program))) ^ "\n"
     243  "\n" ^ lines ^ "\n"

  • driver/build

    r2856 r2875  
    1212ocamlc -I ../Deliverables/D2.2/8051/lib -c -g error.ml
    1313ocamlc -I ../Deliverables/D2.2/8051/lib -c -g *.ml
    14 ocamlc -custom -g -I ../Deliverables/D2.2/8051/lib extracted.cmo  ../Deliverables/D2.2/8051/lib/libcparser.a ../Deliverables/D2.2/8051/lib/cparser.cma clightFromC.cmo clightParser.cmo IntelHex.cmo clightPrinter.cmo backendPrinter.cmo ASMPrinter.cmo error.cmo cerco.cmo -o cerco
     14ocamlc -custom -g -I ../Deliverables/D2.2/8051/lib extracted.cmo  ../Deliverables/D2.2/8051/lib/libcparser.a ../Deliverables/D2.2/8051/lib/cparser.cma clightFromC.cmo clightParser.cmo IntelHex.cmo clightPrinter.cmo ASMPrinter.cmo backendPrinter.cmo error.cmo cerco.cmo -o cerco

  • driver/cerco.ml

    r2874 r2875  
    2929 | Extracted.Compiler.Ltl_pass                   -> "Ltl_pass"
    3030 | Extracted.Compiler.Lin_pass                   -> "Lin_pass"
     31 | Extracted.Compiler.Assembly_pass              -> "Assembly_pass"
     32 | Extracted.Compiler.Object_code_pass           -> "Object_code_pass"
    3133;;
    3234

  • 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 :

  • src/ASM/Interpret2.ma

    r2764 r2875  
    1717
    1818definition mk_fullexec_of_abstract_status:
    19  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in
    20 ≝ λS,as_eval,as_init.
    21    mk_fullexec ?? unit (mk_trans_system_of_abstract_status S as_eval) (λ_.it)
     19 ∀program: Type[0].
     20  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in
     21≝ λprogram,S,as_eval,as_init.
     22   mk_fullexec ?? program (mk_trans_system_of_abstract_status S as_eval) (λ_.it)
    2223    (λ_.return as_init).
    2324
    2425definition mk_preclassified_system_of_abstract_status:
    25  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system
    26 ≝ λS,as_eval,as_init.
     26 ∀program: Type[0].
     27  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system
     28≝ λprogram,S,as_eval,as_init.
    2729   mk_preclassified_system
    28     (mk_fullexec_of_abstract_status S as_eval as_init)
     30    (mk_fullexec_of_abstract_status program S as_eval as_init)
    2931    (λ_.λst. ¬(is_none … (as_label … st)))
    3032    (λ_.as_classify S)
    … …  
    3941  let cm ≝ load_code_memory (oc c) in
    4042  mk_preclassified_system_of_abstract_status
     43   labelled_object_code
    4144   (ASM_abstract_status cm (costlabels c))
    4245   (λst. return (execute_1 … st))

  • src/compiler.ma

    r2841 r2875  
    2929 | ertlptr_pass: pass
    3030 | ltl_pass: pass
    31  | lin_pass: pass.
     31 | lin_pass: pass
     32 | assembly_pass: pass
     33 | object_code_pass: pass.
    3234
    3335definition with_stack_model : Type[0] → Type[0] ≝
    … …  
    4850  | ertlptr_pass ⇒ with_stack_model ertlptr_program
    4951  | ltl_pass ⇒ with_stack_model ltl_program
    50   | lin_pass ⇒ with_stack_model lin_program ].
     52  | lin_pass ⇒ with_stack_model lin_program
     53  | assembly_pass ⇒ pseudo_assembly_program
     54  | object_code_pass ⇒ labelled_object_code ].
    5155
    5256definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit.
    … …  
    109113  let st ≝ lookup_stack_cost … p in
    110114  let i ≝ observe lin_pass 〈p,st〉 in
    111    ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
     115   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
     116  let i ≝ observe assembly_pass p in
    112117   return 〈p,stack_cost,max_stack〉.
    113118
    … …  
    115120include "ASM/Policy.ma".
    116121
    117 definition assembler : pseudo_assembly_program → res labelled_object_code ≝
    118 λp.
     122definition assembler :
     123 observe_pass → pseudo_assembly_program → res labelled_object_code ≝
     124λobserve,p.
    119125  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p);
    120126  let sigma ≝ λppc. \fst sigma_pol ppc in
    121127  let pol ≝ λppc. \snd sigma_pol ppc in
    122   OK ? (assembly p sigma pol).
     128  let p ≝ assembly p sigma pol in
     129  let i ≝ observe object_code_pass p in
     130  OK ? p.
    123131
    124132(* Cost lifting *)
    … …  
    148156  ! 〈init_cost,p',p〉 ← front_end observe p;
    149157  ! 〈p,stack_cost,max_stack〉 ← back_end observe p;
    150   ! p ← assembler p;
     158  ! p ← assembler observe p;
    151159  let k ≝ ASM_cost_map p in
    152160  let k' ≝

  • src/correctness.ma

    r2852 r2875  
    109109  ∃n1,n2.
    110110   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
    111    observables (OC_preclassified_system (c_labelled_object_code … p)) it n1 n2
     111   observables (OC_preclassified_system (c_labelled_object_code … p))
     112    (c_labelled_object_code … p) n1 n2
    112113  ∧
    113114   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).

  • src/semantics.ma

    r2841 r2875  
    99include "LTL/LTL_semantics.ma".
    1010include "LIN/LIN_semantics.ma".
     11include "ASM/Interpret2.ma".
    1112
    1213record preclassified_system_pass (P:pass) : Type[2] ≝
    … …  
    1617
    1718definition preclassified_system_of_pass:
    18  ∀pass. preclassified_system_pass pass ≝
     19 ∀pass. syntax_of_pass pass → preclassified_system_pass pass ≝
    1920 λpass.
    20   match pass with
    21   [ clight_pass ⇒ mk_preclassified_system_pass … Clight_pcs …
    22   | clight_switch_removed_pass ⇒ mk_preclassified_system_pass … Clight_pcs …
    23   | clight_label_pass ⇒ mk_preclassified_system_pass … Clight_pcs …
    24   | clight_simplified_pass ⇒ mk_preclassified_system_pass … Clight_pcs …
    25   | cminor_pass ⇒ mk_preclassified_system_pass … Cminor_pcs …
    26   | rtlabs_pass ⇒ mk_preclassified_system_pass … RTLabs_pcs …
     21  match pass return λpass.syntax_of_pass pass → preclassified_system_pass pass with
     22  [ clight_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
     23  | clight_switch_removed_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
     24  | clight_label_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
     25  | clight_simplified_pass ⇒ λ_.mk_preclassified_system_pass … Clight_pcs …
     26  | cminor_pass ⇒ λ_.mk_preclassified_system_pass … Cminor_pcs …
     27  | rtlabs_pass ⇒ λ_.mk_preclassified_system_pass … RTLabs_pcs …
    2728  | rtl_separate_pass ⇒
    28      mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_separate) …
     29     λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_separate) …
    2930  | rtl_uniq_pass ⇒
    30      mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) …
     31     λ_.mk_preclassified_system_pass … (joint_preclassified_system RTL_semantics_unique) …
    3132  | ertl_pass ⇒
    32      mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …
     33     λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTL_semantics) …
    3334  | ertlptr_pass ⇒
    34      mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) …
     35     λ_.mk_preclassified_system_pass … (joint_preclassified_system ERTLptr_semantics) …
    3536  | ltl_pass ⇒
    36      mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
     37     λ_.mk_preclassified_system_pass … (joint_preclassified_system LTL_semantics) …
    3738  | lin_pass ⇒
    38      mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
     39     λ_.mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ?
     40  | assembly_pass ⇒
     41     ?
     42  | object_code_pass ⇒
     43     λprog. mk_preclassified_system_pass ? (OC_preclassified_system prog) …
    3944  ].
    40 %
     45try % cases daemon
    4146qed.
    4247
    … …  
    4651≝
    4752 λpass,prog,n,print_pass,print_event,print_error,print_exit.
    48  let pcs ≝ preclassified_system_of_pass pass in
     53 let pcs ≝ preclassified_system_of_pass pass prog in
    4954  let prog ≝ prog⌈syntax_of_pass pass ↦ ?⌉ in
    5055  let g ≝ make_global … pcs prog in
Note: See TracChangeset for help on using the changeset viewer.