Changeset 2951 for extracted/eRTL.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/eRTL.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
     
    112126    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    113127let rec move_dst_rect_Type4 h_PSD h_HDW = function
    114 | PSD x_21416 -> h_PSD x_21416
    115 | HDW x_21417 -> h_HDW x_21417
     128| PSD x_18520 -> h_PSD x_18520
     129| HDW x_18521 -> h_HDW x_18521
    116130
    117131(** val move_dst_rect_Type5 :
    118132    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    119133let rec move_dst_rect_Type5 h_PSD h_HDW = function
    120 | PSD x_21421 -> h_PSD x_21421
    121 | HDW x_21422 -> h_HDW x_21422
     134| PSD x_18525 -> h_PSD x_18525
     135| HDW x_18526 -> h_HDW x_18526
    122136
    123137(** val move_dst_rect_Type3 :
    124138    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    125139let rec move_dst_rect_Type3 h_PSD h_HDW = function
    126 | PSD x_21426 -> h_PSD x_21426
    127 | HDW x_21427 -> h_HDW x_21427
     140| PSD x_18530 -> h_PSD x_18530
     141| HDW x_18531 -> h_HDW x_18531
    128142
    129143(** val move_dst_rect_Type2 :
    130144    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    131145let rec move_dst_rect_Type2 h_PSD h_HDW = function
    132 | PSD x_21431 -> h_PSD x_21431
    133 | HDW x_21432 -> h_HDW x_21432
     146| PSD x_18535 -> h_PSD x_18535
     147| HDW x_18536 -> h_HDW x_18536
    134148
    135149(** val move_dst_rect_Type1 :
    136150    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    137151let rec move_dst_rect_Type1 h_PSD h_HDW = function
    138 | PSD x_21436 -> h_PSD x_21436
    139 | HDW x_21437 -> h_HDW x_21437
     152| PSD x_18540 -> h_PSD x_18540
     153| HDW x_18541 -> h_HDW x_18541
    140154
    141155(** val move_dst_rect_Type0 :
    142156    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    143157let rec move_dst_rect_Type0 h_PSD h_HDW = function
    144 | PSD x_21441 -> h_PSD x_21441
    145 | HDW x_21442 -> h_HDW x_21442
     158| PSD x_18545 -> h_PSD x_18545
     159| HDW x_18546 -> h_HDW x_18546
    146160
    147161(** val move_dst_inv_rect_Type4 :
     
    338352| Ertl_new_frame -> h_ertl_new_frame
    339353| Ertl_del_frame -> h_ertl_del_frame
    340 | Ertl_frame_size x_21481 -> h_ertl_frame_size x_21481
     354| Ertl_frame_size x_18585 -> h_ertl_frame_size x_18585
    341355
    342356(** val ertl_seq_rect_Type5 :
     
    345359| Ertl_new_frame -> h_ertl_new_frame
    346360| Ertl_del_frame -> h_ertl_del_frame
    347 | Ertl_frame_size x_21486 -> h_ertl_frame_size x_21486
     361| Ertl_frame_size x_18590 -> h_ertl_frame_size x_18590
    348362
    349363(** val ertl_seq_rect_Type3 :
     
    352366| Ertl_new_frame -> h_ertl_new_frame
    353367| Ertl_del_frame -> h_ertl_del_frame
    354 | Ertl_frame_size x_21491 -> h_ertl_frame_size x_21491
     368| Ertl_frame_size x_18595 -> h_ertl_frame_size x_18595
    355369
    356370(** val ertl_seq_rect_Type2 :
     
    359373| Ertl_new_frame -> h_ertl_new_frame
    360374| Ertl_del_frame -> h_ertl_del_frame
    361 | Ertl_frame_size x_21496 -> h_ertl_frame_size x_21496
     375| Ertl_frame_size x_18600 -> h_ertl_frame_size x_18600
    362376
    363377(** val ertl_seq_rect_Type1 :
     
    366380| Ertl_new_frame -> h_ertl_new_frame
    367381| Ertl_del_frame -> h_ertl_del_frame
    368 | Ertl_frame_size x_21501 -> h_ertl_frame_size x_21501
     382| Ertl_frame_size x_18605 -> h_ertl_frame_size x_18605
    369383
    370384(** val ertl_seq_rect_Type0 :
     
    373387| Ertl_new_frame -> h_ertl_new_frame
    374388| Ertl_del_frame -> h_ertl_del_frame
    375 | Ertl_frame_size x_21506 -> h_ertl_frame_size x_21506
     389| Ertl_frame_size x_18610 -> h_ertl_frame_size x_18610
    376390
    377391(** val ertl_seq_inv_rect_Type4 :
     
    660674  ertl_seq_joint x1 (Types.pi1 x2)
    661675
     676(** val eRTL_premain :
     677    ertl_program -> Joint.joint_closed_internal_function **)
     678let eRTL_premain p =
     679  let l1 = Positive.One in
     680  let l2 = Positive.P0 Positive.One in
     681  let l3 = Positive.P1 Positive.One in
     682  let res = { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0
     683    Positive.One)); Joint.joint_if_runiverse = Positive.One;
     684    Joint.joint_if_result = (Obj.magic Types.It); Joint.joint_if_params =
     685    (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))));
     686    Joint.joint_if_stacksize = Nat.O; Joint.joint_if_local_stacksize = Nat.O;
     687    Joint.joint_if_code =
     688    (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
     689    Joint.joint_if_entry = (Obj.magic l1) }
     690  in
     691  let res0 =
     692    Joint.add_graph eRTL (AST.prog_var_names p.Joint.joint_prog) l1
     693      (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
     694      (Obj.magic l2))) res
     695  in
     696  let res1 =
     697    Joint.add_graph eRTL (AST.prog_var_names p.Joint.joint_prog) l2
     698      (Joint.Sequential ((Joint.CALL ((Types.Inl
     699      p.Joint.joint_prog.AST.prog_main),
     700      (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
     701      (Obj.magic Types.It))), (Obj.magic l3))) res0
     702  in
     703  let res2 =
     704    Joint.add_graph eRTL (AST.prog_var_names p.Joint.joint_prog) l3
     705      (Joint.Final (Joint.GOTO l3)) res1
     706  in
     707  res2
     708
Note: See TracChangeset for help on using the changeset viewer.