Ignore:
Timestamp:
Mar 5, 2013, 9:52:39 PM (7 years ago)
Author:
sacerdot
Message:

The compiler now computes also the stack cost model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabs_syntax.ml

    r2773 r2775  
    139139    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    140140let rec statement_rect_Type4 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    141 | St_skip x_9946 -> h_St_skip x_9946
    142 | St_cost (x_9948, x_9947) -> h_St_cost x_9948 x_9947
    143 | St_const (t, x_9951, x_9950, x_9949) -> h_St_const t x_9951 x_9950 x_9949
    144 | St_op1 (t', t, x_9955, x_9954, x_9953, x_9952) ->
    145   h_St_op1 t' t x_9955 x_9954 x_9953 x_9952
    146 | St_op2 (t', t1, t2, x_9960, x_9959, x_9958, x_9957, x_9956) ->
    147   h_St_op2 t' t1 t2 x_9960 x_9959 x_9958 x_9957 x_9956
    148 | St_load (x_9964, x_9963, x_9962, x_9961) ->
    149   h_St_load x_9964 x_9963 x_9962 x_9961
    150 | St_store (x_9968, x_9967, x_9966, x_9965) ->
    151   h_St_store x_9968 x_9967 x_9966 x_9965
    152 | St_call_id (x_9972, x_9971, x_9970, x_9969) ->
    153   h_St_call_id x_9972 x_9971 x_9970 x_9969
    154 | St_call_ptr (x_9976, x_9975, x_9974, x_9973) ->
    155   h_St_call_ptr x_9976 x_9975 x_9974 x_9973
    156 | St_cond (x_9979, x_9978, x_9977) -> h_St_cond x_9979 x_9978 x_9977
     141| St_skip x_14777 -> h_St_skip x_14777
     142| St_cost (x_14779, x_14778) -> h_St_cost x_14779 x_14778
     143| St_const (t, x_14782, x_14781, x_14780) ->
     144  h_St_const t x_14782 x_14781 x_14780
     145| St_op1 (t', t, x_14786, x_14785, x_14784, x_14783) ->
     146  h_St_op1 t' t x_14786 x_14785 x_14784 x_14783
     147| St_op2 (t', t1, t2, x_14791, x_14790, x_14789, x_14788, x_14787) ->
     148  h_St_op2 t' t1 t2 x_14791 x_14790 x_14789 x_14788 x_14787
     149| St_load (x_14795, x_14794, x_14793, x_14792) ->
     150  h_St_load x_14795 x_14794 x_14793 x_14792
     151| St_store (x_14799, x_14798, x_14797, x_14796) ->
     152  h_St_store x_14799 x_14798 x_14797 x_14796
     153| St_call_id (x_14803, x_14802, x_14801, x_14800) ->
     154  h_St_call_id x_14803 x_14802 x_14801 x_14800
     155| St_call_ptr (x_14807, x_14806, x_14805, x_14804) ->
     156  h_St_call_ptr x_14807 x_14806 x_14805 x_14804
     157| St_cond (x_14810, x_14809, x_14808) -> h_St_cond x_14810 x_14809 x_14808
    157158| St_return -> h_St_return
    158159
     
    173174    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    174175let rec statement_rect_Type5 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    175 | St_skip x_9992 -> h_St_skip x_9992
    176 | St_cost (x_9994, x_9993) -> h_St_cost x_9994 x_9993
    177 | St_const (t, x_9997, x_9996, x_9995) -> h_St_const t x_9997 x_9996 x_9995
    178 | St_op1 (t', t, x_10001, x_10000, x_9999, x_9998) ->
    179   h_St_op1 t' t x_10001 x_10000 x_9999 x_9998
    180 | St_op2 (t', t1, t2, x_10006, x_10005, x_10004, x_10003, x_10002) ->
    181   h_St_op2 t' t1 t2 x_10006 x_10005 x_10004 x_10003 x_10002
    182 | St_load (x_10010, x_10009, x_10008, x_10007) ->
    183   h_St_load x_10010 x_10009 x_10008 x_10007
    184 | St_store (x_10014, x_10013, x_10012, x_10011) ->
    185   h_St_store x_10014 x_10013 x_10012 x_10011
    186 | St_call_id (x_10018, x_10017, x_10016, x_10015) ->
    187   h_St_call_id x_10018 x_10017 x_10016 x_10015
    188 | St_call_ptr (x_10022, x_10021, x_10020, x_10019) ->
    189   h_St_call_ptr x_10022 x_10021 x_10020 x_10019
    190 | St_cond (x_10025, x_10024, x_10023) -> h_St_cond x_10025 x_10024 x_10023
     176| St_skip x_14823 -> h_St_skip x_14823
     177| St_cost (x_14825, x_14824) -> h_St_cost x_14825 x_14824
     178| St_const (t, x_14828, x_14827, x_14826) ->
     179  h_St_const t x_14828 x_14827 x_14826
     180| St_op1 (t', t, x_14832, x_14831, x_14830, x_14829) ->
     181  h_St_op1 t' t x_14832 x_14831 x_14830 x_14829
     182| St_op2 (t', t1, t2, x_14837, x_14836, x_14835, x_14834, x_14833) ->
     183  h_St_op2 t' t1 t2 x_14837 x_14836 x_14835 x_14834 x_14833
     184| St_load (x_14841, x_14840, x_14839, x_14838) ->
     185  h_St_load x_14841 x_14840 x_14839 x_14838
     186| St_store (x_14845, x_14844, x_14843, x_14842) ->
     187  h_St_store x_14845 x_14844 x_14843 x_14842
     188| St_call_id (x_14849, x_14848, x_14847, x_14846) ->
     189  h_St_call_id x_14849 x_14848 x_14847 x_14846
     190| St_call_ptr (x_14853, x_14852, x_14851, x_14850) ->
     191  h_St_call_ptr x_14853 x_14852 x_14851 x_14850
     192| St_cond (x_14856, x_14855, x_14854) -> h_St_cond x_14856 x_14855 x_14854
    191193| St_return -> h_St_return
    192194
     
    207209    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    208210let rec statement_rect_Type3 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    209 | St_skip x_10038 -> h_St_skip x_10038
    210 | St_cost (x_10040, x_10039) -> h_St_cost x_10040 x_10039
    211 | St_const (t, x_10043, x_10042, x_10041) ->
    212   h_St_const t x_10043 x_10042 x_10041
    213 | St_op1 (t', t, x_10047, x_10046, x_10045, x_10044) ->
    214   h_St_op1 t' t x_10047 x_10046 x_10045 x_10044
    215 | St_op2 (t', t1, t2, x_10052, x_10051, x_10050, x_10049, x_10048) ->
    216   h_St_op2 t' t1 t2 x_10052 x_10051 x_10050 x_10049 x_10048
    217 | St_load (x_10056, x_10055, x_10054, x_10053) ->
    218   h_St_load x_10056 x_10055 x_10054 x_10053
    219 | St_store (x_10060, x_10059, x_10058, x_10057) ->
    220   h_St_store x_10060 x_10059 x_10058 x_10057
    221 | St_call_id (x_10064, x_10063, x_10062, x_10061) ->
    222   h_St_call_id x_10064 x_10063 x_10062 x_10061
    223 | St_call_ptr (x_10068, x_10067, x_10066, x_10065) ->
    224   h_St_call_ptr x_10068 x_10067 x_10066 x_10065
    225 | St_cond (x_10071, x_10070, x_10069) -> h_St_cond x_10071 x_10070 x_10069
     211| St_skip x_14869 -> h_St_skip x_14869
     212| St_cost (x_14871, x_14870) -> h_St_cost x_14871 x_14870
     213| St_const (t, x_14874, x_14873, x_14872) ->
     214  h_St_const t x_14874 x_14873 x_14872
     215| St_op1 (t', t, x_14878, x_14877, x_14876, x_14875) ->
     216  h_St_op1 t' t x_14878 x_14877 x_14876 x_14875
     217| St_op2 (t', t1, t2, x_14883, x_14882, x_14881, x_14880, x_14879) ->
     218  h_St_op2 t' t1 t2 x_14883 x_14882 x_14881 x_14880 x_14879
     219| St_load (x_14887, x_14886, x_14885, x_14884) ->
     220  h_St_load x_14887 x_14886 x_14885 x_14884
     221| St_store (x_14891, x_14890, x_14889, x_14888) ->
     222  h_St_store x_14891 x_14890 x_14889 x_14888
     223| St_call_id (x_14895, x_14894, x_14893, x_14892) ->
     224  h_St_call_id x_14895 x_14894 x_14893 x_14892
     225| St_call_ptr (x_14899, x_14898, x_14897, x_14896) ->
     226  h_St_call_ptr x_14899 x_14898 x_14897 x_14896
     227| St_cond (x_14902, x_14901, x_14900) -> h_St_cond x_14902 x_14901 x_14900
    226228| St_return -> h_St_return
    227229
     
    242244    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    243245let rec statement_rect_Type2 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    244 | St_skip x_10084 -> h_St_skip x_10084
    245 | St_cost (x_10086, x_10085) -> h_St_cost x_10086 x_10085
    246 | St_const (t, x_10089, x_10088, x_10087) ->
    247   h_St_const t x_10089 x_10088 x_10087
    248 | St_op1 (t', t, x_10093, x_10092, x_10091, x_10090) ->
    249   h_St_op1 t' t x_10093 x_10092 x_10091 x_10090
    250 | St_op2 (t', t1, t2, x_10098, x_10097, x_10096, x_10095, x_10094) ->
    251   h_St_op2 t' t1 t2 x_10098 x_10097 x_10096 x_10095 x_10094
    252 | St_load (x_10102, x_10101, x_10100, x_10099) ->
    253   h_St_load x_10102 x_10101 x_10100 x_10099
    254 | St_store (x_10106, x_10105, x_10104, x_10103) ->
    255   h_St_store x_10106 x_10105 x_10104 x_10103
    256 | St_call_id (x_10110, x_10109, x_10108, x_10107) ->
    257   h_St_call_id x_10110 x_10109 x_10108 x_10107
    258 | St_call_ptr (x_10114, x_10113, x_10112, x_10111) ->
    259   h_St_call_ptr x_10114 x_10113 x_10112 x_10111
    260 | St_cond (x_10117, x_10116, x_10115) -> h_St_cond x_10117 x_10116 x_10115
     246| St_skip x_14915 -> h_St_skip x_14915
     247| St_cost (x_14917, x_14916) -> h_St_cost x_14917 x_14916
     248| St_const (t, x_14920, x_14919, x_14918) ->
     249  h_St_const t x_14920 x_14919 x_14918
     250| St_op1 (t', t, x_14924, x_14923, x_14922, x_14921) ->
     251  h_St_op1 t' t x_14924 x_14923 x_14922 x_14921
     252| St_op2 (t', t1, t2, x_14929, x_14928, x_14927, x_14926, x_14925) ->
     253  h_St_op2 t' t1 t2 x_14929 x_14928 x_14927 x_14926 x_14925
     254| St_load (x_14933, x_14932, x_14931, x_14930) ->
     255  h_St_load x_14933 x_14932 x_14931 x_14930
     256| St_store (x_14937, x_14936, x_14935, x_14934) ->
     257  h_St_store x_14937 x_14936 x_14935 x_14934
     258| St_call_id (x_14941, x_14940, x_14939, x_14938) ->
     259  h_St_call_id x_14941 x_14940 x_14939 x_14938
     260| St_call_ptr (x_14945, x_14944, x_14943, x_14942) ->
     261  h_St_call_ptr x_14945 x_14944 x_14943 x_14942
     262| St_cond (x_14948, x_14947, x_14946) -> h_St_cond x_14948 x_14947 x_14946
    261263| St_return -> h_St_return
    262264
     
    277279    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    278280let rec statement_rect_Type1 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    279 | St_skip x_10130 -> h_St_skip x_10130
    280 | St_cost (x_10132, x_10131) -> h_St_cost x_10132 x_10131
    281 | St_const (t, x_10135, x_10134, x_10133) ->
    282   h_St_const t x_10135 x_10134 x_10133
    283 | St_op1 (t', t, x_10139, x_10138, x_10137, x_10136) ->
    284   h_St_op1 t' t x_10139 x_10138 x_10137 x_10136
    285 | St_op2 (t', t1, t2, x_10144, x_10143, x_10142, x_10141, x_10140) ->
    286   h_St_op2 t' t1 t2 x_10144 x_10143 x_10142 x_10141 x_10140
    287 | St_load (x_10148, x_10147, x_10146, x_10145) ->
    288   h_St_load x_10148 x_10147 x_10146 x_10145
    289 | St_store (x_10152, x_10151, x_10150, x_10149) ->
    290   h_St_store x_10152 x_10151 x_10150 x_10149
    291 | St_call_id (x_10156, x_10155, x_10154, x_10153) ->
    292   h_St_call_id x_10156 x_10155 x_10154 x_10153
    293 | St_call_ptr (x_10160, x_10159, x_10158, x_10157) ->
    294   h_St_call_ptr x_10160 x_10159 x_10158 x_10157
    295 | St_cond (x_10163, x_10162, x_10161) -> h_St_cond x_10163 x_10162 x_10161
     281| St_skip x_14961 -> h_St_skip x_14961
     282| St_cost (x_14963, x_14962) -> h_St_cost x_14963 x_14962
     283| St_const (t, x_14966, x_14965, x_14964) ->
     284  h_St_const t x_14966 x_14965 x_14964
     285| St_op1 (t', t, x_14970, x_14969, x_14968, x_14967) ->
     286  h_St_op1 t' t x_14970 x_14969 x_14968 x_14967
     287| St_op2 (t', t1, t2, x_14975, x_14974, x_14973, x_14972, x_14971) ->
     288  h_St_op2 t' t1 t2 x_14975 x_14974 x_14973 x_14972 x_14971
     289| St_load (x_14979, x_14978, x_14977, x_14976) ->
     290  h_St_load x_14979 x_14978 x_14977 x_14976
     291| St_store (x_14983, x_14982, x_14981, x_14980) ->
     292  h_St_store x_14983 x_14982 x_14981 x_14980
     293| St_call_id (x_14987, x_14986, x_14985, x_14984) ->
     294  h_St_call_id x_14987 x_14986 x_14985 x_14984
     295| St_call_ptr (x_14991, x_14990, x_14989, x_14988) ->
     296  h_St_call_ptr x_14991 x_14990 x_14989 x_14988
     297| St_cond (x_14994, x_14993, x_14992) -> h_St_cond x_14994 x_14993 x_14992
    296298| St_return -> h_St_return
    297299
     
    312314    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    313315let rec statement_rect_Type0 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    314 | St_skip x_10176 -> h_St_skip x_10176
    315 | St_cost (x_10178, x_10177) -> h_St_cost x_10178 x_10177
    316 | St_const (t, x_10181, x_10180, x_10179) ->
    317   h_St_const t x_10181 x_10180 x_10179
    318 | St_op1 (t', t, x_10185, x_10184, x_10183, x_10182) ->
    319   h_St_op1 t' t x_10185 x_10184 x_10183 x_10182
    320 | St_op2 (t', t1, t2, x_10190, x_10189, x_10188, x_10187, x_10186) ->
    321   h_St_op2 t' t1 t2 x_10190 x_10189 x_10188 x_10187 x_10186
    322 | St_load (x_10194, x_10193, x_10192, x_10191) ->
    323   h_St_load x_10194 x_10193 x_10192 x_10191
    324 | St_store (x_10198, x_10197, x_10196, x_10195) ->
    325   h_St_store x_10198 x_10197 x_10196 x_10195
    326 | St_call_id (x_10202, x_10201, x_10200, x_10199) ->
    327   h_St_call_id x_10202 x_10201 x_10200 x_10199
    328 | St_call_ptr (x_10206, x_10205, x_10204, x_10203) ->
    329   h_St_call_ptr x_10206 x_10205 x_10204 x_10203
    330 | St_cond (x_10209, x_10208, x_10207) -> h_St_cond x_10209 x_10208 x_10207
     316| St_skip x_15007 -> h_St_skip x_15007
     317| St_cost (x_15009, x_15008) -> h_St_cost x_15009 x_15008
     318| St_const (t, x_15012, x_15011, x_15010) ->
     319  h_St_const t x_15012 x_15011 x_15010
     320| St_op1 (t', t, x_15016, x_15015, x_15014, x_15013) ->
     321  h_St_op1 t' t x_15016 x_15015 x_15014 x_15013
     322| St_op2 (t', t1, t2, x_15021, x_15020, x_15019, x_15018, x_15017) ->
     323  h_St_op2 t' t1 t2 x_15021 x_15020 x_15019 x_15018 x_15017
     324| St_load (x_15025, x_15024, x_15023, x_15022) ->
     325  h_St_load x_15025 x_15024 x_15023 x_15022
     326| St_store (x_15029, x_15028, x_15027, x_15026) ->
     327  h_St_store x_15029 x_15028 x_15027 x_15026
     328| St_call_id (x_15033, x_15032, x_15031, x_15030) ->
     329  h_St_call_id x_15033 x_15032 x_15031 x_15030
     330| St_call_ptr (x_15037, x_15036, x_15035, x_15034) ->
     331  h_St_call_ptr x_15037 x_15036 x_15035 x_15034
     332| St_cond (x_15040, x_15039, x_15038) -> h_St_cond x_15040 x_15039 x_15038
    331333| St_return -> h_St_return
    332334
     
    464466    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    465467    internal_function -> 'a1 **)
    466 let rec internal_function_rect_Type4 h_mk_internal_function x_10499 =
     468let rec internal_function_rect_Type4 h_mk_internal_function x_15330 =
    467469  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    468470    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    469     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_10499
     471    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15330
    470472  in
    471473  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    479481    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    480482    internal_function -> 'a1 **)
    481 let rec internal_function_rect_Type5 h_mk_internal_function x_10501 =
     483let rec internal_function_rect_Type5 h_mk_internal_function x_15332 =
    482484  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    483485    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    484     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_10501
     486    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15332
    485487  in
    486488  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    494496    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    495497    internal_function -> 'a1 **)
    496 let rec internal_function_rect_Type3 h_mk_internal_function x_10503 =
     498let rec internal_function_rect_Type3 h_mk_internal_function x_15334 =
    497499  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    498500    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    499     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_10503
     501    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15334
    500502  in
    501503  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    509511    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    510512    internal_function -> 'a1 **)
    511 let rec internal_function_rect_Type2 h_mk_internal_function x_10505 =
     513let rec internal_function_rect_Type2 h_mk_internal_function x_15336 =
    512514  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    513515    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    514     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_10505
     516    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15336
    515517  in
    516518  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    524526    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    525527    internal_function -> 'a1 **)
    526 let rec internal_function_rect_Type1 h_mk_internal_function x_10507 =
     528let rec internal_function_rect_Type1 h_mk_internal_function x_15338 =
    527529  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    528530    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    529     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_10507
     531    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15338
    530532  in
    531533  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    539541    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    540542    internal_function -> 'a1 **)
    541 let rec internal_function_rect_Type0 h_mk_internal_function x_10509 =
     543let rec internal_function_rect_Type0 h_mk_internal_function x_15340 =
    542544  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    543545    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    544     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_10509
     546    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15340
    545547  in
    546548  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
Note: See TracChangeset for help on using the changeset viewer.