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/joint_LTL_LIN.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    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    117131let rec registers_move_rect_Type4 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    118 | From_acc (x_21672, x_21671) -> h_from_acc x_21672 x_21671
    119 | To_acc (x_21674, x_21673) -> h_to_acc x_21674 x_21673
    120 | Int_to_reg (x_21676, x_21675) -> h_int_to_reg x_21676 x_21675
    121 | Int_to_acc (x_21678, x_21677) -> h_int_to_acc x_21678 x_21677
     132| From_acc (x_18776, x_18775) -> h_from_acc x_18776 x_18775
     133| To_acc (x_18778, x_18777) -> h_to_acc x_18778 x_18777
     134| Int_to_reg (x_18780, x_18779) -> h_int_to_reg x_18780 x_18779
     135| Int_to_acc (x_18782, x_18781) -> h_int_to_acc x_18782 x_18781
    122136
    123137(** val registers_move_rect_Type5 :
     
    126140    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    127141let rec registers_move_rect_Type5 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    128 | From_acc (x_21685, x_21684) -> h_from_acc x_21685 x_21684
    129 | To_acc (x_21687, x_21686) -> h_to_acc x_21687 x_21686
    130 | Int_to_reg (x_21689, x_21688) -> h_int_to_reg x_21689 x_21688
    131 | Int_to_acc (x_21691, x_21690) -> h_int_to_acc x_21691 x_21690
     142| From_acc (x_18789, x_18788) -> h_from_acc x_18789 x_18788
     143| To_acc (x_18791, x_18790) -> h_to_acc x_18791 x_18790
     144| Int_to_reg (x_18793, x_18792) -> h_int_to_reg x_18793 x_18792
     145| Int_to_acc (x_18795, x_18794) -> h_int_to_acc x_18795 x_18794
    132146
    133147(** val registers_move_rect_Type3 :
     
    136150    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    137151let rec registers_move_rect_Type3 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    138 | From_acc (x_21698, x_21697) -> h_from_acc x_21698 x_21697
    139 | To_acc (x_21700, x_21699) -> h_to_acc x_21700 x_21699
    140 | Int_to_reg (x_21702, x_21701) -> h_int_to_reg x_21702 x_21701
    141 | Int_to_acc (x_21704, x_21703) -> h_int_to_acc x_21704 x_21703
     152| From_acc (x_18802, x_18801) -> h_from_acc x_18802 x_18801
     153| To_acc (x_18804, x_18803) -> h_to_acc x_18804 x_18803
     154| Int_to_reg (x_18806, x_18805) -> h_int_to_reg x_18806 x_18805
     155| Int_to_acc (x_18808, x_18807) -> h_int_to_acc x_18808 x_18807
    142156
    143157(** val registers_move_rect_Type2 :
     
    146160    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    147161let rec registers_move_rect_Type2 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    148 | From_acc (x_21711, x_21710) -> h_from_acc x_21711 x_21710
    149 | To_acc (x_21713, x_21712) -> h_to_acc x_21713 x_21712
    150 | Int_to_reg (x_21715, x_21714) -> h_int_to_reg x_21715 x_21714
    151 | Int_to_acc (x_21717, x_21716) -> h_int_to_acc x_21717 x_21716
     162| From_acc (x_18815, x_18814) -> h_from_acc x_18815 x_18814
     163| To_acc (x_18817, x_18816) -> h_to_acc x_18817 x_18816
     164| Int_to_reg (x_18819, x_18818) -> h_int_to_reg x_18819 x_18818
     165| Int_to_acc (x_18821, x_18820) -> h_int_to_acc x_18821 x_18820
    152166
    153167(** val registers_move_rect_Type1 :
     
    156170    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    157171let rec registers_move_rect_Type1 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    158 | From_acc (x_21724, x_21723) -> h_from_acc x_21724 x_21723
    159 | To_acc (x_21726, x_21725) -> h_to_acc x_21726 x_21725
    160 | Int_to_reg (x_21728, x_21727) -> h_int_to_reg x_21728 x_21727
    161 | Int_to_acc (x_21730, x_21729) -> h_int_to_acc x_21730 x_21729
     172| From_acc (x_18828, x_18827) -> h_from_acc x_18828 x_18827
     173| To_acc (x_18830, x_18829) -> h_to_acc x_18830 x_18829
     174| Int_to_reg (x_18832, x_18831) -> h_int_to_reg x_18832 x_18831
     175| Int_to_acc (x_18834, x_18833) -> h_int_to_acc x_18834 x_18833
    162176
    163177(** val registers_move_rect_Type0 :
     
    166180    BitVector.byte -> 'a1) -> registers_move -> 'a1 **)
    167181let rec registers_move_rect_Type0 h_from_acc h_to_acc h_int_to_reg h_int_to_acc = function
    168 | From_acc (x_21737, x_21736) -> h_from_acc x_21737 x_21736
    169 | To_acc (x_21739, x_21738) -> h_to_acc x_21739 x_21738
    170 | Int_to_reg (x_21741, x_21740) -> h_int_to_reg x_21741 x_21740
    171 | Int_to_acc (x_21743, x_21742) -> h_int_to_acc x_21743 x_21742
     182| From_acc (x_18841, x_18840) -> h_from_acc x_18841 x_18840
     183| To_acc (x_18843, x_18842) -> h_to_acc x_18843 x_18842
     184| Int_to_reg (x_18845, x_18844) -> h_int_to_reg x_18845 x_18844
     185| Int_to_acc (x_18847, x_18846) -> h_int_to_acc x_18847 x_18846
    172186
    173187(** val registers_move_inv_rect_Type4 :
     
    241255| SAVE_CARRY -> h_SAVE_CARRY
    242256| RESTORE_CARRY -> h_RESTORE_CARRY
    243 | LOW_ADDRESS (x_21837, x_21836) -> h_LOW_ADDRESS x_21837 x_21836
    244 | HIGH_ADDRESS (x_21839, x_21838) -> h_HIGH_ADDRESS x_21839 x_21838
     257| LOW_ADDRESS (x_18941, x_18940) -> h_LOW_ADDRESS x_18941 x_18940
     258| HIGH_ADDRESS (x_18943, x_18942) -> h_HIGH_ADDRESS x_18943 x_18942
    245259
    246260(** val ltl_lin_seq_rect_Type5 :
     
    250264| SAVE_CARRY -> h_SAVE_CARRY
    251265| RESTORE_CARRY -> h_RESTORE_CARRY
    252 | LOW_ADDRESS (x_21846, x_21845) -> h_LOW_ADDRESS x_21846 x_21845
    253 | HIGH_ADDRESS (x_21848, x_21847) -> h_HIGH_ADDRESS x_21848 x_21847
     266| LOW_ADDRESS (x_18950, x_18949) -> h_LOW_ADDRESS x_18950 x_18949
     267| HIGH_ADDRESS (x_18952, x_18951) -> h_HIGH_ADDRESS x_18952 x_18951
    254268
    255269(** val ltl_lin_seq_rect_Type3 :
     
    259273| SAVE_CARRY -> h_SAVE_CARRY
    260274| RESTORE_CARRY -> h_RESTORE_CARRY
    261 | LOW_ADDRESS (x_21855, x_21854) -> h_LOW_ADDRESS x_21855 x_21854
    262 | HIGH_ADDRESS (x_21857, x_21856) -> h_HIGH_ADDRESS x_21857 x_21856
     275| LOW_ADDRESS (x_18959, x_18958) -> h_LOW_ADDRESS x_18959 x_18958
     276| HIGH_ADDRESS (x_18961, x_18960) -> h_HIGH_ADDRESS x_18961 x_18960
    263277
    264278(** val ltl_lin_seq_rect_Type2 :
     
    268282| SAVE_CARRY -> h_SAVE_CARRY
    269283| RESTORE_CARRY -> h_RESTORE_CARRY
    270 | LOW_ADDRESS (x_21864, x_21863) -> h_LOW_ADDRESS x_21864 x_21863
    271 | HIGH_ADDRESS (x_21866, x_21865) -> h_HIGH_ADDRESS x_21866 x_21865
     284| LOW_ADDRESS (x_18968, x_18967) -> h_LOW_ADDRESS x_18968 x_18967
     285| HIGH_ADDRESS (x_18970, x_18969) -> h_HIGH_ADDRESS x_18970 x_18969
    272286
    273287(** val ltl_lin_seq_rect_Type1 :
     
    277291| SAVE_CARRY -> h_SAVE_CARRY
    278292| RESTORE_CARRY -> h_RESTORE_CARRY
    279 | LOW_ADDRESS (x_21873, x_21872) -> h_LOW_ADDRESS x_21873 x_21872
    280 | HIGH_ADDRESS (x_21875, x_21874) -> h_HIGH_ADDRESS x_21875 x_21874
     293| LOW_ADDRESS (x_18977, x_18976) -> h_LOW_ADDRESS x_18977 x_18976
     294| HIGH_ADDRESS (x_18979, x_18978) -> h_HIGH_ADDRESS x_18979 x_18978
    281295
    282296(** val ltl_lin_seq_rect_Type0 :
     
    286300| SAVE_CARRY -> h_SAVE_CARRY
    287301| RESTORE_CARRY -> h_RESTORE_CARRY
    288 | LOW_ADDRESS (x_21882, x_21881) -> h_LOW_ADDRESS x_21882 x_21881
    289 | HIGH_ADDRESS (x_21884, x_21883) -> h_HIGH_ADDRESS x_21884 x_21883
     302| LOW_ADDRESS (x_18986, x_18985) -> h_LOW_ADDRESS x_18986 x_18985
     303| HIGH_ADDRESS (x_18988, x_18987) -> h_HIGH_ADDRESS x_18988 x_18987
    290304
    291305(** val ltl_lin_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.