Changeset 2951 for extracted/eRTLptr.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/eRTLptr.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
     
    116130    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    117131let rec ertlptr_seq_rect_Type4 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    118 | Ertlptr_ertl x_21550 -> h_ertlptr_ertl x_21550
    119 | LOW_ADDRESS (x_21552, x_21551) -> h_LOW_ADDRESS x_21552 x_21551
    120 | HIGH_ADDRESS (x_21554, x_21553) -> h_HIGH_ADDRESS x_21554 x_21553
     132| Ertlptr_ertl x_18654 -> h_ertlptr_ertl x_18654
     133| LOW_ADDRESS (x_18656, x_18655) -> h_LOW_ADDRESS x_18656 x_18655
     134| HIGH_ADDRESS (x_18658, x_18657) -> h_HIGH_ADDRESS x_18658 x_18657
    121135
    122136(** val ertlptr_seq_rect_Type5 :
     
    124138    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    125139let rec ertlptr_seq_rect_Type5 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    126 | Ertlptr_ertl x_21559 -> h_ertlptr_ertl x_21559
    127 | LOW_ADDRESS (x_21561, x_21560) -> h_LOW_ADDRESS x_21561 x_21560
    128 | HIGH_ADDRESS (x_21563, x_21562) -> h_HIGH_ADDRESS x_21563 x_21562
     140| Ertlptr_ertl x_18663 -> h_ertlptr_ertl x_18663
     141| LOW_ADDRESS (x_18665, x_18664) -> h_LOW_ADDRESS x_18665 x_18664
     142| HIGH_ADDRESS (x_18667, x_18666) -> h_HIGH_ADDRESS x_18667 x_18666
    129143
    130144(** val ertlptr_seq_rect_Type3 :
     
    132146    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    133147let rec ertlptr_seq_rect_Type3 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    134 | Ertlptr_ertl x_21568 -> h_ertlptr_ertl x_21568
    135 | LOW_ADDRESS (x_21570, x_21569) -> h_LOW_ADDRESS x_21570 x_21569
    136 | HIGH_ADDRESS (x_21572, x_21571) -> h_HIGH_ADDRESS x_21572 x_21571
     148| Ertlptr_ertl x_18672 -> h_ertlptr_ertl x_18672
     149| LOW_ADDRESS (x_18674, x_18673) -> h_LOW_ADDRESS x_18674 x_18673
     150| HIGH_ADDRESS (x_18676, x_18675) -> h_HIGH_ADDRESS x_18676 x_18675
    137151
    138152(** val ertlptr_seq_rect_Type2 :
     
    140154    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    141155let rec ertlptr_seq_rect_Type2 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    142 | Ertlptr_ertl x_21577 -> h_ertlptr_ertl x_21577
    143 | LOW_ADDRESS (x_21579, x_21578) -> h_LOW_ADDRESS x_21579 x_21578
    144 | HIGH_ADDRESS (x_21581, x_21580) -> h_HIGH_ADDRESS x_21581 x_21580
     156| Ertlptr_ertl x_18681 -> h_ertlptr_ertl x_18681
     157| LOW_ADDRESS (x_18683, x_18682) -> h_LOW_ADDRESS x_18683 x_18682
     158| HIGH_ADDRESS (x_18685, x_18684) -> h_HIGH_ADDRESS x_18685 x_18684
    145159
    146160(** val ertlptr_seq_rect_Type1 :
     
    148162    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    149163let rec ertlptr_seq_rect_Type1 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    150 | Ertlptr_ertl x_21586 -> h_ertlptr_ertl x_21586
    151 | LOW_ADDRESS (x_21588, x_21587) -> h_LOW_ADDRESS x_21588 x_21587
    152 | HIGH_ADDRESS (x_21590, x_21589) -> h_HIGH_ADDRESS x_21590 x_21589
     164| Ertlptr_ertl x_18690 -> h_ertlptr_ertl x_18690
     165| LOW_ADDRESS (x_18692, x_18691) -> h_LOW_ADDRESS x_18692 x_18691
     166| HIGH_ADDRESS (x_18694, x_18693) -> h_HIGH_ADDRESS x_18694 x_18693
    153167
    154168(** val ertlptr_seq_rect_Type0 :
     
    156170    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    157171let rec ertlptr_seq_rect_Type0 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    158 | Ertlptr_ertl x_21595 -> h_ertlptr_ertl x_21595
    159 | LOW_ADDRESS (x_21597, x_21596) -> h_LOW_ADDRESS x_21597 x_21596
    160 | HIGH_ADDRESS (x_21599, x_21598) -> h_HIGH_ADDRESS x_21599 x_21598
     172| Ertlptr_ertl x_18699 -> h_ertlptr_ertl x_18699
     173| LOW_ADDRESS (x_18701, x_18700) -> h_LOW_ADDRESS x_18701 x_18700
     174| HIGH_ADDRESS (x_18703, x_18702) -> h_HIGH_ADDRESS x_18703 x_18702
    161175
    162176(** val ertlptr_seq_inv_rect_Type4 :
     
    325339  ertlptr_seq_joint x1 (Types.pi1 x2)
    326340
     341(** val eRTLptr_premain :
     342    ertlptr_program -> Joint.joint_closed_internal_function **)
     343let eRTLptr_premain p =
     344  let l1 = Positive.One in
     345  let l2 = Positive.P0 Positive.One in
     346  let l3 = Positive.P1 Positive.One in
     347  let res = { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0
     348    Positive.One)); Joint.joint_if_runiverse = Positive.One;
     349    Joint.joint_if_result = (Obj.magic Types.It); Joint.joint_if_params =
     350    (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))));
     351    Joint.joint_if_stacksize = Nat.O; Joint.joint_if_local_stacksize = Nat.O;
     352    Joint.joint_if_code =
     353    (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
     354    Joint.joint_if_entry = (Obj.magic l1) }
     355  in
     356  let res0 =
     357    Joint.add_graph eRTLptr (AST.prog_var_names p.Joint.joint_prog) l1
     358      (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
     359      (Obj.magic l2))) res
     360  in
     361  let res1 =
     362    Joint.add_graph eRTLptr (AST.prog_var_names p.Joint.joint_prog) l2
     363      (Joint.Sequential ((Joint.CALL ((Types.Inl
     364      p.Joint.joint_prog.AST.prog_main),
     365      (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
     366      (Obj.magic Types.It))), (Obj.magic l3))) res0
     367  in
     368  let res2 =
     369    Joint.add_graph eRTLptr (AST.prog_var_names p.Joint.joint_prog) l3
     370      (Joint.Final (Joint.GOTO l3)) res1
     371  in
     372  res2
     373
Note: See TracChangeset for help on using the changeset viewer.