Changeset 2951 for extracted/compiler.ml


Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.ml

    r2909 r2951  
    149149open ToCminor
    150150
    151 open Initialisation
    152 
    153151open BitVectorTrie
    154152
     
    172170
    173171open CostCheck
    174 
    175 open Executions
    176 
    177 open StructuredTraces
    178 
    179 open RTLabs_semantics
    180 
    181 open RTLabs_abstract
    182 
    183 open RTLabs_traces
    184172
    185173open CostInj
     
    490478      (Obj.magic (ToCminor.clight_to_cminor p1)) (fun p2 ->
    491479      let i3 = observe Cminor_pass p2 in
    492       let p3 = ToRTLabs.cminor_to_rtlabs init_cost (Obj.magic p2) in
     480      let p3 = ToRTLabs.cminor_to_rtlabs (Obj.magic p2) in
    493481      let i4 = Obj.magic observe Rtlabs_pass p3 in
    494482      (match CostCheck.check_cost_program p3 with
     
    523511
    524512(** val back_end :
    525     observe_pass -> RTLabs_syntax.rTLabs_program ->
     513    observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
    526514    ((ASM.pseudo_assembly_program, Joint.stack_cost_model) Types.prod,
    527515    Nat.nat) Types.prod Errors.res **)
    528 let back_end observe p =
    529   let p0 = RTLabsToRTL.rtlabs_to_rtl p in
     516let back_end observe init_cost p =
     517  let p0 = RTLabsToRTL.rtlabs_to_rtl init_cost p in
    530518  let st = lookup_stack_cost (Joint.graph_params_to_params RTL.rTL) p0 in
    531519  let i =
     
    543531  let i2 = Obj.magic observe Ertlptr_pass { Types.fst = p2; Types.snd = st1 }
    544532  in
    545   let { Types.fst = eta29116; Types.snd = max_stack } =
     533  let { Types.fst = eta24710; Types.snd = max_stack } =
    546534    ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
    547535  in
    548   let { Types.fst = p3; Types.snd = stack_cost } = eta29116 in
     536  let { Types.fst = p3; Types.snd = stack_cost } = eta24710 in
    549537  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in
    550538  let i3 = Obj.magic observe Ltl_pass { Types.fst = p3; Types.snd = st2 } in
     
    592580      Obj.magic (Errors.OK (Types.pi1 p0))))
    593581
     582open StructuredTraces
     583
    594584open AbstractStatus
    595585
     
    625615    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    626616    compiler_output -> 'a1 **)
    627 let rec compiler_output_rect_Type4 h_mk_compiler_output x_25390 =
     617let rec compiler_output_rect_Type4 h_mk_compiler_output x_4341 =
    628618  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    629619    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    630     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25390
     620    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4341
    631621  in
    632622  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    637627    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    638628    compiler_output -> 'a1 **)
    639 let rec compiler_output_rect_Type5 h_mk_compiler_output x_25392 =
     629let rec compiler_output_rect_Type5 h_mk_compiler_output x_4343 =
    640630  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    641631    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    642     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25392
     632    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4343
    643633  in
    644634  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    649639    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    650640    compiler_output -> 'a1 **)
    651 let rec compiler_output_rect_Type3 h_mk_compiler_output x_25394 =
     641let rec compiler_output_rect_Type3 h_mk_compiler_output x_4345 =
    652642  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    653643    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    654     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25394
     644    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4345
    655645  in
    656646  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    661651    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    662652    compiler_output -> 'a1 **)
    663 let rec compiler_output_rect_Type2 h_mk_compiler_output x_25396 =
     653let rec compiler_output_rect_Type2 h_mk_compiler_output x_4347 =
    664654  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    665655    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    666     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25396
     656    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4347
    667657  in
    668658  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    673663    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    674664    compiler_output -> 'a1 **)
    675 let rec compiler_output_rect_Type1 h_mk_compiler_output x_25398 =
     665let rec compiler_output_rect_Type1 h_mk_compiler_output x_4349 =
    676666  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    677667    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    678     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25398
     668    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4349
    679669  in
    680670  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    685675    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    686676    compiler_output -> 'a1 **)
    687 let rec compiler_output_rect_Type0 h_mk_compiler_output x_25400 =
     677let rec compiler_output_rect_Type0 h_mk_compiler_output x_4351 =
    688678  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    689679    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    690     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25400
     680    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4351
    691681  in
    692682  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    773763      (Obj.magic (front_end observe p)) (fun init_cost p' p0 ->
    774764      Monad.m_bind3 (Monad.max_def Errors.res0)
    775         (Obj.magic (back_end observe p0)) (fun p1 stack_cost max_stack ->
     765        (Obj.magic (back_end observe init_cost p0))
     766        (fun p1 stack_cost max_stack ->
    776767        Monad.m_bind0 (Monad.max_def Errors.res0)
    777768          (Obj.magic (assembler observe p1)) (fun p2 ->
Note: See TracChangeset for help on using the changeset viewer.