Changeset 2951 for extracted/toRTLabs.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/toRTLabs.ml

    r2827 r2951  
    142142    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    143143    fixed -> 'a1 **)
    144 let rec fixed_rect_Type4 h_mk_fixed x_15486 =
     144let rec fixed_rect_Type4 h_mk_fixed x_15525 =
    145145  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    146     x_15486
     146    x_15525
    147147  in
    148148  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    151151    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    152152    fixed -> 'a1 **)
    153 let rec fixed_rect_Type5 h_mk_fixed x_15488 =
     153let rec fixed_rect_Type5 h_mk_fixed x_15527 =
    154154  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    155     x_15488
     155    x_15527
    156156  in
    157157  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    160160    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    161161    fixed -> 'a1 **)
    162 let rec fixed_rect_Type3 h_mk_fixed x_15490 =
     162let rec fixed_rect_Type3 h_mk_fixed x_15529 =
    163163  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    164     x_15490
     164    x_15529
    165165  in
    166166  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    169169    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    170170    fixed -> 'a1 **)
    171 let rec fixed_rect_Type2 h_mk_fixed x_15492 =
     171let rec fixed_rect_Type2 h_mk_fixed x_15531 =
    172172  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    173     x_15492
     173    x_15531
    174174  in
    175175  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    178178    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    179179    fixed -> 'a1 **)
    180 let rec fixed_rect_Type1 h_mk_fixed x_15494 =
     180let rec fixed_rect_Type1 h_mk_fixed x_15533 =
    181181  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    182     x_15494
     182    x_15533
    183183  in
    184184  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    187187    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    188188    fixed -> 'a1 **)
    189 let rec fixed_rect_Type0 h_mk_fixed x_15496 =
     189let rec fixed_rect_Type0 h_mk_fixed x_15535 =
    190190  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    191     x_15496
     191    x_15535
    192192  in
    193193  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    257257    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    258258    -> goto_map -> 'a1 **)
    259 let rec goto_map_rect_Type4 fx g h_mk_goto_map x_15512 =
    260   let gm_map = x_15512 in h_mk_goto_map gm_map __ __
     259let rec goto_map_rect_Type4 fx g h_mk_goto_map x_15551 =
     260  let gm_map = x_15551 in h_mk_goto_map gm_map __ __
    261261
    262262(** val goto_map_rect_Type5 :
     
    264264    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    265265    -> goto_map -> 'a1 **)
    266 let rec goto_map_rect_Type5 fx g h_mk_goto_map x_15514 =
    267   let gm_map = x_15514 in h_mk_goto_map gm_map __ __
     266let rec goto_map_rect_Type5 fx g h_mk_goto_map x_15553 =
     267  let gm_map = x_15553 in h_mk_goto_map gm_map __ __
    268268
    269269(** val goto_map_rect_Type3 :
     
    271271    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    272272    -> goto_map -> 'a1 **)
    273 let rec goto_map_rect_Type3 fx g h_mk_goto_map x_15516 =
    274   let gm_map = x_15516 in h_mk_goto_map gm_map __ __
     273let rec goto_map_rect_Type3 fx g h_mk_goto_map x_15555 =
     274  let gm_map = x_15555 in h_mk_goto_map gm_map __ __
    275275
    276276(** val goto_map_rect_Type2 :
     
    278278    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    279279    -> goto_map -> 'a1 **)
    280 let rec goto_map_rect_Type2 fx g h_mk_goto_map x_15518 =
    281   let gm_map = x_15518 in h_mk_goto_map gm_map __ __
     280let rec goto_map_rect_Type2 fx g h_mk_goto_map x_15557 =
     281  let gm_map = x_15557 in h_mk_goto_map gm_map __ __
    282282
    283283(** val goto_map_rect_Type1 :
     
    285285    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    286286    -> goto_map -> 'a1 **)
    287 let rec goto_map_rect_Type1 fx g h_mk_goto_map x_15520 =
    288   let gm_map = x_15520 in h_mk_goto_map gm_map __ __
     287let rec goto_map_rect_Type1 fx g h_mk_goto_map x_15559 =
     288  let gm_map = x_15559 in h_mk_goto_map gm_map __ __
    289289
    290290(** val goto_map_rect_Type0 :
     
    292292    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    293293    -> goto_map -> 'a1 **)
    294 let rec goto_map_rect_Type0 fx g h_mk_goto_map x_15522 =
    295   let gm_map = x_15522 in h_mk_goto_map gm_map __ __
     294let rec goto_map_rect_Type0 fx g h_mk_goto_map x_15561 =
     295  let gm_map = x_15561 in h_mk_goto_map gm_map __ __
    296296
    297297(** val gm_map :
     
    401401    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    402402    -> 'a1 **)
    403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_15540 =
     403let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_15579 =
    404404  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    405405    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    406406    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    407407    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    408     x_15540
     408    x_15579
    409409  in
    410410  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    419419    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    420420    -> 'a1 **)
    421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_15542 =
     421let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_15581 =
    422422  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    423423    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    424424    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    425425    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    426     x_15542
     426    x_15581
    427427  in
    428428  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    437437    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    438438    -> 'a1 **)
    439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_15544 =
     439let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_15583 =
    440440  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    441441    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    442442    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    443443    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    444     x_15544
     444    x_15583
    445445  in
    446446  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    455455    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    456456    -> 'a1 **)
    457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_15546 =
     457let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_15585 =
    458458  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    459459    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    460460    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    461461    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    462     x_15546
     462    x_15585
    463463  in
    464464  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    473473    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    474474    -> 'a1 **)
    475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15548 =
     475let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15587 =
    476476  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    477477    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    478478    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    479479    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    480     x_15548
     480    x_15587
    481481  in
    482482  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    491491    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    492492    -> 'a1 **)
    493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15550 =
     493let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15589 =
    494494  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    495495    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    496496    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    497497    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    498     x_15550
     498    x_15589
    499499  in
    500500  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    874874    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    875875    fn_con_because -> 'a1 **)
    876 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15626 = function
     876let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15665 = function
    877877| Fn_con_eq f -> h_fn_con_eq f
    878878| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    884884    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    885885    fn_con_because -> 'a1 **)
    886 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15633 = function
     886let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15672 = function
    887887| Fn_con_eq f -> h_fn_con_eq f
    888888| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    894894    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    895895    fn_con_because -> 'a1 **)
    896 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15640 = function
     896let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15679 = function
    897897| Fn_con_eq f -> h_fn_con_eq f
    898898| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    904904    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    905905    fn_con_because -> 'a1 **)
    906 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15647 = function
     906let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15686 = function
    907907| Fn_con_eq f -> h_fn_con_eq f
    908908| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    914914    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    915915    fn_con_because -> 'a1 **)
    916 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15654 = function
     916let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15693 = function
    917917| Fn_con_eq f -> h_fn_con_eq f
    918918| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    924924    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    925925    fn_con_because -> 'a1 **)
    926 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15661 = function
     926let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15700 = function
    927927| Fn_con_eq f -> h_fn_con_eq f
    928928| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    11631163  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
    11641164
    1165 (** val expr_is_Id :
     1165(** val expr_is_cst_ident :
    11661166    AST.typ -> Cminor_syntax.expr -> AST.ident Types.option **)
    1167 let expr_is_Id t = function
    1168 | Cminor_syntax.Id (x, id) -> Types.Some id
    1169 | Cminor_syntax.Cst (x, x0) -> Types.None
     1167let expr_is_cst_ident t = function
     1168| Cminor_syntax.Id (x, x0) -> Types.None
     1169| Cminor_syntax.Cst (x, c) ->
     1170  (match c with
     1171   | FrontEndOps.Ointconst (x0, x1, x2) -> Types.None
     1172   | FrontEndOps.Oaddrsymbol (id, n) ->
     1173     (match n with
     1174      | Nat.O -> Types.Some id
     1175      | Nat.S x0 -> Types.None)
     1176   | FrontEndOps.Oaddrstack x0 -> Types.None)
    11701177| Cminor_syntax.Op1 (x, x0, x1, x2) -> Types.None
    11711178| Cminor_syntax.Op2 (x, x0, x1, x2, x3, x4) -> Types.None
     
    12681275       in
    12691276       let f1 =
    1270          match expr_is_Id AST.ASTptr e with
     1277         match expr_is_cst_ident AST.ASTptr e with
    12711278         | Types.None ->
    12721279           let { Types.dpi1 = f1; Types.dpi2 = fnr } =
     
    13901397  RTLabs_syntax.f_exit = (Types.pi1 f1).pf_exit })) __)) __)) __
    13911398
    1392 (** val cminor_noinit_to_rtlabs :
    1393     Cminor_syntax.cminor_noinit_program -> RTLabs_syntax.rTLabs_program **)
    1394 let cminor_noinit_to_rtlabs p =
     1399(** val cminor_to_rtlabs :
     1400    Cminor_syntax.cminor_program -> RTLabs_syntax.rTLabs_program **)
     1401let cminor_to_rtlabs p =
    13951402  AST.transform_program p (fun x -> AST.transf_fundef c2ra_function)
    13961403
    1397 open Initialisation
    1398 
    1399 (** val cminor_to_rtlabs :
    1400     CostLabel.costlabel -> Cminor_syntax.cminor_program ->
    1401     RTLabs_syntax.rTLabs_program **)
    1402 let cminor_to_rtlabs init_cost p =
    1403   let p' = Initialisation.replace_init init_cost p in
    1404   cminor_noinit_to_rtlabs p'
    1405 
Note: See TracChangeset for help on using the changeset viewer.