Changeset 2842


Ignore:
Timestamp:
Mar 11, 2013, 12:41:33 PM (4 years ago)
Author:
sacerdot
Message:

The compiler can now show all back-end traces too (assembly and object code
are excluded ATM).

Location:
extracted
Files:
2 added
2 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.ml

    r2829 r2842  
    434434     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
    435435     | Lin_pass -> Obj.magic (fun _ dH -> dH)) y
     436
     437type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod
    436438
    437439type syntax_of_pass = __
     
    469471         Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadCostLabelling)))))
    470472
     473open Uses
     474
    471475(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
    472476let compute_fixpoint = Compute_fixpoints.compute_fixpoint
     
    474478(** val colour_graph : Interference.coloured_graph_computer **)
    475479let colour_graph = Compute_colouring.colour_graph
     480
     481open AssocList
     482
     483(** val lookup_stack_cost :
     484    Joint.params -> Joint.joint_program -> PreIdentifiers.identifier ->
     485    Nat.nat Types.option **)
     486let lookup_stack_cost p p0 id =
     487  AssocList.assoc_list_lookup id
     488    (Identifiers.eq_identifier PreIdentifiers.SymbolTag)
     489    (Joint.stack_cost p p0)
    476490
    477491(** val back_end :
     
    481495let back_end observe p =
    482496  let p0 = RTLabsToRTL.rtlabs_to_rtl p in
    483   let i = Obj.magic observe Rtl_separate_pass p0 in
    484   let i0 = Obj.magic observe Rtl_uniq_pass p0 in
     497  let st = lookup_stack_cost (Joint.graph_params_to_params RTL.rTL) p0 in
     498  let i =
     499    Obj.magic observe Rtl_separate_pass { Types.fst = p0; Types.snd = st }
     500  in
     501  let i0 = Obj.magic observe Rtl_uniq_pass { Types.fst = p0; Types.snd = st }
     502  in
    485503  let p1 = RTLToERTL.rtl_to_ertl p0 in
    486   let i1 = Obj.magic observe Ertl_pass p1 in
     504  let st0 = lookup_stack_cost (Joint.graph_params_to_params ERTL.eRTL) p1 in
     505  let i1 = Obj.magic observe Ertl_pass { Types.fst = p1; Types.snd = st0 } in
    487506  let p2 = ERTLToERTLptr.ertl_to_ertlptr p1 in
    488   let i2 = Obj.magic observe Ertlptr_pass p2 in
    489   let { Types.fst = eta2; Types.snd = max_stack } =
     507  let st1 =
     508    lookup_stack_cost (Joint.graph_params_to_params ERTLptr.eRTLptr) p2
     509  in
     510  let i2 = Obj.magic observe Ertlptr_pass { Types.fst = p2; Types.snd = st1 }
     511  in
     512  let { Types.fst = eta20; Types.snd = max_stack } =
    490513    ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
    491514  in
    492   let { Types.fst = p3; Types.snd = stack_cost } = eta2 in
    493   let i3 = Obj.magic observe Ltl_pass p3 in
     515  let { Types.fst = p3; Types.snd = stack_cost0 } = eta20 in
     516  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in
     517  let i3 = Obj.magic observe Ltl_pass { Types.fst = p3; Types.snd = st2 } in
     518  let st3 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in
    494519  let p4 = LTLToLIN.ltl_to_lin p3 in
    495   let i4 = Obj.magic observe Lin_pass p4 in
     520  let st4 = lookup_stack_cost (Joint.lin_params_to_params LIN.lIN) p4 in
     521  let i4 = Obj.magic observe Lin_pass { Types.fst = p4; Types.snd = st4 } in
    496522  Obj.magic
    497523    (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    500526          (LINToASM.lin_to_asm p4))) (fun p5 ->
    501527      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
    502         p5; Types.snd = stack_cost }; Types.snd = max_stack }))
     528        p5; Types.snd = stack_cost0 }; Types.snd = max_stack }))
    503529
    504530open Assembly
     
    708734      (Obj.magic (front_end observe p)) (fun init_cost p' p0 ->
    709735      Monad.m_bind3 (Monad.max_def Errors.res0)
    710         (Obj.magic (back_end observe p0)) (fun p1 stack_cost max_stack ->
     736        (Obj.magic (back_end observe p0)) (fun p1 stack_cost0 max_stack ->
    711737        Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p1))
    712738          (fun p2 ->
     
    717743          in
    718744          Monad.m_return0 (Monad.max_def Errors.res0)
    719             { c_labelled_object_code = p2; c_stack_cost = stack_cost;
     745            { c_labelled_object_code = p2; c_stack_cost = stack_cost0;
    720746            c_max_stack = max_stack; c_labelled_clight = p';
    721747            c_clight_cost_map = k' }))))
  • extracted/compiler.mli

    r2829 r2842  
    312312val pass_jmdiscr : pass -> pass -> __
    313313
     314type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod
     315
    314316type syntax_of_pass = __
    315317
     
    321323  Types.prod Errors.res
    322324
     325open Uses
     326
    323327val compute_fixpoint : Fixpoints.fixpoint_computer
    324328
    325329val colour_graph : Interference.coloured_graph_computer
     330
     331open AssocList
     332
     333val lookup_stack_cost :
     334  Joint.params -> Joint.joint_program -> PreIdentifiers.identifier -> Nat.nat
     335  Types.option
    326336
    327337val back_end :
Note: See TracChangeset for help on using the changeset viewer.