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/translateUtils.ml

    r2873 r2951  
    11open Preamble
     2
     3open Extra_bool
     4
     5open Coqlib
     6
     7open Values
     8
     9open FrontEndVal
     10
     11open GenMem
     12
     13open FrontEndMem
     14
     15open Globalenvs
    216
    317open String
     
    268282    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    269283    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    270 let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_21201 =
     284let rec b_graph_translate_data_rect_Type4 src dst globals h_mk_b_graph_translate_data x_18305 =
    271285  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    272286    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    273     f_step = f_step0; f_fin = f_fin0 } = x_21201
     287    f_step = f_step0; f_fin = f_fin0 } = x_18305
    274288  in
    275289  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    282296    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    283297    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    284 let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_21203 =
     298let rec b_graph_translate_data_rect_Type5 src dst globals h_mk_b_graph_translate_data x_18307 =
    285299  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    286300    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    287     f_step = f_step0; f_fin = f_fin0 } = x_21203
     301    f_step = f_step0; f_fin = f_fin0 } = x_18307
    288302  in
    289303  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    296310    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    297311    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    298 let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_21205 =
     312let rec b_graph_translate_data_rect_Type3 src dst globals h_mk_b_graph_translate_data x_18309 =
    299313  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    300314    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    301     f_step = f_step0; f_fin = f_fin0 } = x_21205
     315    f_step = f_step0; f_fin = f_fin0 } = x_18309
    302316  in
    303317  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    310324    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    311325    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    312 let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_21207 =
     326let rec b_graph_translate_data_rect_Type2 src dst globals h_mk_b_graph_translate_data x_18311 =
    313327  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    314328    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    315     f_step = f_step0; f_fin = f_fin0 } = x_21207
     329    f_step = f_step0; f_fin = f_fin0 } = x_18311
    316330  in
    317331  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    324338    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    325339    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    326 let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_21209 =
     340let rec b_graph_translate_data_rect_Type1 src dst globals h_mk_b_graph_translate_data x_18313 =
    327341  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    328342    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    329     f_step = f_step0; f_fin = f_fin0 } = x_21209
     343    f_step = f_step0; f_fin = f_fin0 } = x_18313
    330344  in
    331345  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    338352    -> (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __
    339353    -> __ -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1 **)
    340 let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_21211 =
     354let rec b_graph_translate_data_rect_Type0 src dst globals h_mk_b_graph_translate_data x_18315 =
    341355  let { init_ret = init_ret0; init_params = init_params0; init_stack_size =
    342356    init_stack_size0; added_prologue = added_prologue0; new_regs = new_regs0;
    343     f_step = f_step0; f_fin = f_fin0 } = x_21211
     357    f_step = f_step0; f_fin = f_fin0 } = x_18315
    344358  in
    345359  h_mk_b_graph_translate_data init_ret0 init_params0 init_stack_size0
     
    652666    Joint.joint_program -> Joint.joint_program **)
    653667let b_graph_transform_program src dst init p =
    654   AST.transform_program p (fun varnames ->
    655     AST.transf_fundef (fun def_in ->
    656       Types.pi1
    657         (b_graph_translate src dst varnames (init varnames def_in) def_in)))
     668  { Joint.joint_prog =
     669    (AST.transform_program p.Joint.joint_prog (fun varnames ->
     670      AST.transf_fundef (fun def_in ->
     671        Types.pi1
     672          (b_graph_translate src dst varnames (init varnames def_in) def_in))));
     673    Joint.init_cost_label = p.Joint.init_cost_label }
    658674
    659675(** val added_registers :
Note: See TracChangeset for help on using the changeset viewer.