Changeset 2905 for extracted/compiler.ml


Ignore:
Timestamp:
Mar 19, 2013, 8:42:43 AM (7 years ago)
Author:
sacerdot
Message:

Semantics of ASM in place (up to return values and function call names).
The test example badly diverges in ASM after being ok in LIN.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.ml

    r2904 r2905  
    543543  let i2 = Obj.magic observe Ertlptr_pass { Types.fst = p2; Types.snd = st1 }
    544544  in
    545   let { Types.fst = eta2; Types.snd = max_stack } =
     545  let { Types.fst = eta29116; Types.snd = max_stack } =
    546546    ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
    547547  in
    548   let { Types.fst = p3; Types.snd = stack_cost } = eta2 in
     548  let { Types.fst = p3; Types.snd = stack_cost } = eta29116 in
    549549  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in
    550550  let i3 = Obj.magic observe Ltl_pass { Types.fst = p3; Types.snd = st2 } in
     
    558558        (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
    559559          (LINToASM.lin_to_asm p4))) (fun p5 ->
    560       let i5 = observe Assembly_pass p5 in
    561560      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
    562561        p5; Types.snd = stack_cost }; Types.snd = max_stack }))
     
    578577    Errors.res **)
    579578let assembler observe p =
    580 prerr_endline "ASSEMBLY0";
    581579  Obj.magic
    582580    (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    584582        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
    585583          (Policy.jump_expansion' p))) (fun sigma_pol ->
    586 prerr_endline "ASSEMBLY1";
    587584      let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
    588585      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
     586      let i =
     587        Obj.magic observe Assembly_pass { Types.fst = { Types.fst = p;
     588          Types.snd = sigma }; Types.snd = pol }
     589      in
    589590      let p0 = Assembly.assembly p sigma pol in
    590       let i = Obj.magic observe Object_code_pass (Types.pi1 p0) in
    591 prerr_endline "ASSEMBLY2";
     591      let i0 = Obj.magic observe Object_code_pass (Types.pi1 p0) in
    592592      Obj.magic (Errors.OK (Types.pi1 p0))))
    593593
     
    626626    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    627627    compiler_output -> 'a1 **)
    628 let rec compiler_output_rect_Type4 h_mk_compiler_output x_198 =
     628let rec compiler_output_rect_Type4 h_mk_compiler_output x_25390 =
    629629  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    630630    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    631     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_198
     631    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25390
    632632  in
    633633  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    638638    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    639639    compiler_output -> 'a1 **)
    640 let rec compiler_output_rect_Type5 h_mk_compiler_output x_200 =
     640let rec compiler_output_rect_Type5 h_mk_compiler_output x_25392 =
    641641  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    642642    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    643     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_200
     643    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25392
    644644  in
    645645  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    650650    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    651651    compiler_output -> 'a1 **)
    652 let rec compiler_output_rect_Type3 h_mk_compiler_output x_202 =
     652let rec compiler_output_rect_Type3 h_mk_compiler_output x_25394 =
    653653  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    654654    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    655     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_202
     655    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25394
    656656  in
    657657  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    662662    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    663663    compiler_output -> 'a1 **)
    664 let rec compiler_output_rect_Type2 h_mk_compiler_output x_204 =
     664let rec compiler_output_rect_Type2 h_mk_compiler_output x_25396 =
    665665  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    666666    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    667     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_204
     667    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25396
    668668  in
    669669  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    674674    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    675675    compiler_output -> 'a1 **)
    676 let rec compiler_output_rect_Type1 h_mk_compiler_output x_206 =
     676let rec compiler_output_rect_Type1 h_mk_compiler_output x_25398 =
    677677  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    678678    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    679     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_206
     679    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25398
    680680  in
    681681  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    686686    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    687687    compiler_output -> 'a1 **)
    688 let rec compiler_output_rect_Type0 h_mk_compiler_output x_208 =
     688let rec compiler_output_rect_Type0 h_mk_compiler_output x_25400 =
    689689  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    690690    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    691     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_208
     691    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_25400
    692692  in
    693693  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
Note: See TracChangeset for help on using the changeset viewer.