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/rTLabs_syntax.ml

    r2827 r2951  
    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_14907 -> h_St_skip x_14907
    142 | St_cost (x_14909, x_14908) -> h_St_cost x_14909 x_14908
    143 | St_const (t, x_14912, x_14911, x_14910) ->
    144   h_St_const t x_14912 x_14911 x_14910
    145 | St_op1 (t', t, x_14916, x_14915, x_14914, x_14913) ->
    146   h_St_op1 t' t x_14916 x_14915 x_14914 x_14913
    147 | St_op2 (t', t1, t2, x_14921, x_14920, x_14919, x_14918, x_14917) ->
    148   h_St_op2 t' t1 t2 x_14921 x_14920 x_14919 x_14918 x_14917
    149 | St_load (x_14925, x_14924, x_14923, x_14922) ->
    150   h_St_load x_14925 x_14924 x_14923 x_14922
    151 | St_store (x_14929, x_14928, x_14927, x_14926) ->
    152   h_St_store x_14929 x_14928 x_14927 x_14926
    153 | St_call_id (x_14933, x_14932, x_14931, x_14930) ->
    154   h_St_call_id x_14933 x_14932 x_14931 x_14930
    155 | St_call_ptr (x_14937, x_14936, x_14935, x_14934) ->
    156   h_St_call_ptr x_14937 x_14936 x_14935 x_14934
    157 | St_cond (x_14940, x_14939, x_14938) -> h_St_cond x_14940 x_14939 x_14938
     141| St_skip x_14946 -> h_St_skip x_14946
     142| St_cost (x_14948, x_14947) -> h_St_cost x_14948 x_14947
     143| St_const (t, x_14951, x_14950, x_14949) ->
     144  h_St_const t x_14951 x_14950 x_14949
     145| St_op1 (t', t, x_14955, x_14954, x_14953, x_14952) ->
     146  h_St_op1 t' t x_14955 x_14954 x_14953 x_14952
     147| St_op2 (t', t1, t2, x_14960, x_14959, x_14958, x_14957, x_14956) ->
     148  h_St_op2 t' t1 t2 x_14960 x_14959 x_14958 x_14957 x_14956
     149| St_load (x_14964, x_14963, x_14962, x_14961) ->
     150  h_St_load x_14964 x_14963 x_14962 x_14961
     151| St_store (x_14968, x_14967, x_14966, x_14965) ->
     152  h_St_store x_14968 x_14967 x_14966 x_14965
     153| St_call_id (x_14972, x_14971, x_14970, x_14969) ->
     154  h_St_call_id x_14972 x_14971 x_14970 x_14969
     155| St_call_ptr (x_14976, x_14975, x_14974, x_14973) ->
     156  h_St_call_ptr x_14976 x_14975 x_14974 x_14973
     157| St_cond (x_14979, x_14978, x_14977) -> h_St_cond x_14979 x_14978 x_14977
    158158| St_return -> h_St_return
    159159
     
    174174    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    175175let 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
    176 | St_skip x_14953 -> h_St_skip x_14953
    177 | St_cost (x_14955, x_14954) -> h_St_cost x_14955 x_14954
    178 | St_const (t, x_14958, x_14957, x_14956) ->
    179   h_St_const t x_14958 x_14957 x_14956
    180 | St_op1 (t', t, x_14962, x_14961, x_14960, x_14959) ->
    181   h_St_op1 t' t x_14962 x_14961 x_14960 x_14959
    182 | St_op2 (t', t1, t2, x_14967, x_14966, x_14965, x_14964, x_14963) ->
    183   h_St_op2 t' t1 t2 x_14967 x_14966 x_14965 x_14964 x_14963
    184 | St_load (x_14971, x_14970, x_14969, x_14968) ->
    185   h_St_load x_14971 x_14970 x_14969 x_14968
    186 | St_store (x_14975, x_14974, x_14973, x_14972) ->
    187   h_St_store x_14975 x_14974 x_14973 x_14972
    188 | St_call_id (x_14979, x_14978, x_14977, x_14976) ->
    189   h_St_call_id x_14979 x_14978 x_14977 x_14976
    190 | St_call_ptr (x_14983, x_14982, x_14981, x_14980) ->
    191   h_St_call_ptr x_14983 x_14982 x_14981 x_14980
    192 | St_cond (x_14986, x_14985, x_14984) -> h_St_cond x_14986 x_14985 x_14984
     176| St_skip x_14992 -> h_St_skip x_14992
     177| St_cost (x_14994, x_14993) -> h_St_cost x_14994 x_14993
     178| St_const (t, x_14997, x_14996, x_14995) ->
     179  h_St_const t x_14997 x_14996 x_14995
     180| St_op1 (t', t, x_15001, x_15000, x_14999, x_14998) ->
     181  h_St_op1 t' t x_15001 x_15000 x_14999 x_14998
     182| St_op2 (t', t1, t2, x_15006, x_15005, x_15004, x_15003, x_15002) ->
     183  h_St_op2 t' t1 t2 x_15006 x_15005 x_15004 x_15003 x_15002
     184| St_load (x_15010, x_15009, x_15008, x_15007) ->
     185  h_St_load x_15010 x_15009 x_15008 x_15007
     186| St_store (x_15014, x_15013, x_15012, x_15011) ->
     187  h_St_store x_15014 x_15013 x_15012 x_15011
     188| St_call_id (x_15018, x_15017, x_15016, x_15015) ->
     189  h_St_call_id x_15018 x_15017 x_15016 x_15015
     190| St_call_ptr (x_15022, x_15021, x_15020, x_15019) ->
     191  h_St_call_ptr x_15022 x_15021 x_15020 x_15019
     192| St_cond (x_15025, x_15024, x_15023) -> h_St_cond x_15025 x_15024 x_15023
    193193| St_return -> h_St_return
    194194
     
    209209    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    210210let 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
    211 | St_skip x_14999 -> h_St_skip x_14999
    212 | St_cost (x_15001, x_15000) -> h_St_cost x_15001 x_15000
    213 | St_const (t, x_15004, x_15003, x_15002) ->
    214   h_St_const t x_15004 x_15003 x_15002
    215 | St_op1 (t', t, x_15008, x_15007, x_15006, x_15005) ->
    216   h_St_op1 t' t x_15008 x_15007 x_15006 x_15005
    217 | St_op2 (t', t1, t2, x_15013, x_15012, x_15011, x_15010, x_15009) ->
    218   h_St_op2 t' t1 t2 x_15013 x_15012 x_15011 x_15010 x_15009
    219 | St_load (x_15017, x_15016, x_15015, x_15014) ->
    220   h_St_load x_15017 x_15016 x_15015 x_15014
    221 | St_store (x_15021, x_15020, x_15019, x_15018) ->
    222   h_St_store x_15021 x_15020 x_15019 x_15018
    223 | St_call_id (x_15025, x_15024, x_15023, x_15022) ->
    224   h_St_call_id x_15025 x_15024 x_15023 x_15022
    225 | St_call_ptr (x_15029, x_15028, x_15027, x_15026) ->
    226   h_St_call_ptr x_15029 x_15028 x_15027 x_15026
    227 | St_cond (x_15032, x_15031, x_15030) -> h_St_cond x_15032 x_15031 x_15030
     211| St_skip x_15038 -> h_St_skip x_15038
     212| St_cost (x_15040, x_15039) -> h_St_cost x_15040 x_15039
     213| St_const (t, x_15043, x_15042, x_15041) ->
     214  h_St_const t x_15043 x_15042 x_15041
     215| St_op1 (t', t, x_15047, x_15046, x_15045, x_15044) ->
     216  h_St_op1 t' t x_15047 x_15046 x_15045 x_15044
     217| St_op2 (t', t1, t2, x_15052, x_15051, x_15050, x_15049, x_15048) ->
     218  h_St_op2 t' t1 t2 x_15052 x_15051 x_15050 x_15049 x_15048
     219| St_load (x_15056, x_15055, x_15054, x_15053) ->
     220  h_St_load x_15056 x_15055 x_15054 x_15053
     221| St_store (x_15060, x_15059, x_15058, x_15057) ->
     222  h_St_store x_15060 x_15059 x_15058 x_15057
     223| St_call_id (x_15064, x_15063, x_15062, x_15061) ->
     224  h_St_call_id x_15064 x_15063 x_15062 x_15061
     225| St_call_ptr (x_15068, x_15067, x_15066, x_15065) ->
     226  h_St_call_ptr x_15068 x_15067 x_15066 x_15065
     227| St_cond (x_15071, x_15070, x_15069) -> h_St_cond x_15071 x_15070 x_15069
    228228| St_return -> h_St_return
    229229
     
    244244    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    245245let 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
    246 | St_skip x_15045 -> h_St_skip x_15045
    247 | St_cost (x_15047, x_15046) -> h_St_cost x_15047 x_15046
    248 | St_const (t, x_15050, x_15049, x_15048) ->
    249   h_St_const t x_15050 x_15049 x_15048
    250 | St_op1 (t', t, x_15054, x_15053, x_15052, x_15051) ->
    251   h_St_op1 t' t x_15054 x_15053 x_15052 x_15051
    252 | St_op2 (t', t1, t2, x_15059, x_15058, x_15057, x_15056, x_15055) ->
    253   h_St_op2 t' t1 t2 x_15059 x_15058 x_15057 x_15056 x_15055
    254 | St_load (x_15063, x_15062, x_15061, x_15060) ->
    255   h_St_load x_15063 x_15062 x_15061 x_15060
    256 | St_store (x_15067, x_15066, x_15065, x_15064) ->
    257   h_St_store x_15067 x_15066 x_15065 x_15064
    258 | St_call_id (x_15071, x_15070, x_15069, x_15068) ->
    259   h_St_call_id x_15071 x_15070 x_15069 x_15068
    260 | St_call_ptr (x_15075, x_15074, x_15073, x_15072) ->
    261   h_St_call_ptr x_15075 x_15074 x_15073 x_15072
    262 | St_cond (x_15078, x_15077, x_15076) -> h_St_cond x_15078 x_15077 x_15076
     246| St_skip x_15084 -> h_St_skip x_15084
     247| St_cost (x_15086, x_15085) -> h_St_cost x_15086 x_15085
     248| St_const (t, x_15089, x_15088, x_15087) ->
     249  h_St_const t x_15089 x_15088 x_15087
     250| St_op1 (t', t, x_15093, x_15092, x_15091, x_15090) ->
     251  h_St_op1 t' t x_15093 x_15092 x_15091 x_15090
     252| St_op2 (t', t1, t2, x_15098, x_15097, x_15096, x_15095, x_15094) ->
     253  h_St_op2 t' t1 t2 x_15098 x_15097 x_15096 x_15095 x_15094
     254| St_load (x_15102, x_15101, x_15100, x_15099) ->
     255  h_St_load x_15102 x_15101 x_15100 x_15099
     256| St_store (x_15106, x_15105, x_15104, x_15103) ->
     257  h_St_store x_15106 x_15105 x_15104 x_15103
     258| St_call_id (x_15110, x_15109, x_15108, x_15107) ->
     259  h_St_call_id x_15110 x_15109 x_15108 x_15107
     260| St_call_ptr (x_15114, x_15113, x_15112, x_15111) ->
     261  h_St_call_ptr x_15114 x_15113 x_15112 x_15111
     262| St_cond (x_15117, x_15116, x_15115) -> h_St_cond x_15117 x_15116 x_15115
    263263| St_return -> h_St_return
    264264
     
    279279    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    280280let 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
    281 | St_skip x_15091 -> h_St_skip x_15091
    282 | St_cost (x_15093, x_15092) -> h_St_cost x_15093 x_15092
    283 | St_const (t, x_15096, x_15095, x_15094) ->
    284   h_St_const t x_15096 x_15095 x_15094
    285 | St_op1 (t', t, x_15100, x_15099, x_15098, x_15097) ->
    286   h_St_op1 t' t x_15100 x_15099 x_15098 x_15097
    287 | St_op2 (t', t1, t2, x_15105, x_15104, x_15103, x_15102, x_15101) ->
    288   h_St_op2 t' t1 t2 x_15105 x_15104 x_15103 x_15102 x_15101
    289 | St_load (x_15109, x_15108, x_15107, x_15106) ->
    290   h_St_load x_15109 x_15108 x_15107 x_15106
    291 | St_store (x_15113, x_15112, x_15111, x_15110) ->
    292   h_St_store x_15113 x_15112 x_15111 x_15110
    293 | St_call_id (x_15117, x_15116, x_15115, x_15114) ->
    294   h_St_call_id x_15117 x_15116 x_15115 x_15114
    295 | St_call_ptr (x_15121, x_15120, x_15119, x_15118) ->
    296   h_St_call_ptr x_15121 x_15120 x_15119 x_15118
    297 | St_cond (x_15124, x_15123, x_15122) -> h_St_cond x_15124 x_15123 x_15122
     281| St_skip x_15130 -> h_St_skip x_15130
     282| St_cost (x_15132, x_15131) -> h_St_cost x_15132 x_15131
     283| St_const (t, x_15135, x_15134, x_15133) ->
     284  h_St_const t x_15135 x_15134 x_15133
     285| St_op1 (t', t, x_15139, x_15138, x_15137, x_15136) ->
     286  h_St_op1 t' t x_15139 x_15138 x_15137 x_15136
     287| St_op2 (t', t1, t2, x_15144, x_15143, x_15142, x_15141, x_15140) ->
     288  h_St_op2 t' t1 t2 x_15144 x_15143 x_15142 x_15141 x_15140
     289| St_load (x_15148, x_15147, x_15146, x_15145) ->
     290  h_St_load x_15148 x_15147 x_15146 x_15145
     291| St_store (x_15152, x_15151, x_15150, x_15149) ->
     292  h_St_store x_15152 x_15151 x_15150 x_15149
     293| St_call_id (x_15156, x_15155, x_15154, x_15153) ->
     294  h_St_call_id x_15156 x_15155 x_15154 x_15153
     295| St_call_ptr (x_15160, x_15159, x_15158, x_15157) ->
     296  h_St_call_ptr x_15160 x_15159 x_15158 x_15157
     297| St_cond (x_15163, x_15162, x_15161) -> h_St_cond x_15163 x_15162 x_15161
    298298| St_return -> h_St_return
    299299
     
    314314    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    315315let 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
    316 | St_skip x_15137 -> h_St_skip x_15137
    317 | St_cost (x_15139, x_15138) -> h_St_cost x_15139 x_15138
    318 | St_const (t, x_15142, x_15141, x_15140) ->
    319   h_St_const t x_15142 x_15141 x_15140
    320 | St_op1 (t', t, x_15146, x_15145, x_15144, x_15143) ->
    321   h_St_op1 t' t x_15146 x_15145 x_15144 x_15143
    322 | St_op2 (t', t1, t2, x_15151, x_15150, x_15149, x_15148, x_15147) ->
    323   h_St_op2 t' t1 t2 x_15151 x_15150 x_15149 x_15148 x_15147
    324 | St_load (x_15155, x_15154, x_15153, x_15152) ->
    325   h_St_load x_15155 x_15154 x_15153 x_15152
    326 | St_store (x_15159, x_15158, x_15157, x_15156) ->
    327   h_St_store x_15159 x_15158 x_15157 x_15156
    328 | St_call_id (x_15163, x_15162, x_15161, x_15160) ->
    329   h_St_call_id x_15163 x_15162 x_15161 x_15160
    330 | St_call_ptr (x_15167, x_15166, x_15165, x_15164) ->
    331   h_St_call_ptr x_15167 x_15166 x_15165 x_15164
    332 | St_cond (x_15170, x_15169, x_15168) -> h_St_cond x_15170 x_15169 x_15168
     316| St_skip x_15176 -> h_St_skip x_15176
     317| St_cost (x_15178, x_15177) -> h_St_cost x_15178 x_15177
     318| St_const (t, x_15181, x_15180, x_15179) ->
     319  h_St_const t x_15181 x_15180 x_15179
     320| St_op1 (t', t, x_15185, x_15184, x_15183, x_15182) ->
     321  h_St_op1 t' t x_15185 x_15184 x_15183 x_15182
     322| St_op2 (t', t1, t2, x_15190, x_15189, x_15188, x_15187, x_15186) ->
     323  h_St_op2 t' t1 t2 x_15190 x_15189 x_15188 x_15187 x_15186
     324| St_load (x_15194, x_15193, x_15192, x_15191) ->
     325  h_St_load x_15194 x_15193 x_15192 x_15191
     326| St_store (x_15198, x_15197, x_15196, x_15195) ->
     327  h_St_store x_15198 x_15197 x_15196 x_15195
     328| St_call_id (x_15202, x_15201, x_15200, x_15199) ->
     329  h_St_call_id x_15202 x_15201 x_15200 x_15199
     330| St_call_ptr (x_15206, x_15205, x_15204, x_15203) ->
     331  h_St_call_ptr x_15206 x_15205 x_15204 x_15203
     332| St_cond (x_15209, x_15208, x_15207) -> h_St_cond x_15209 x_15208 x_15207
    333333| St_return -> h_St_return
    334334
     
    466466    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    467467    internal_function -> 'a1 **)
    468 let rec internal_function_rect_Type4 h_mk_internal_function x_15460 =
     468let rec internal_function_rect_Type4 h_mk_internal_function x_15499 =
    469469  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    470470    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    471     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15460
     471    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15499
    472472  in
    473473  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    481481    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    482482    internal_function -> 'a1 **)
    483 let rec internal_function_rect_Type5 h_mk_internal_function x_15462 =
     483let rec internal_function_rect_Type5 h_mk_internal_function x_15501 =
    484484  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    485485    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    486     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15462
     486    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15501
    487487  in
    488488  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    496496    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    497497    internal_function -> 'a1 **)
    498 let rec internal_function_rect_Type3 h_mk_internal_function x_15464 =
     498let rec internal_function_rect_Type3 h_mk_internal_function x_15503 =
    499499  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    500500    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    501     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15464
     501    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15503
    502502  in
    503503  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    511511    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    512512    internal_function -> 'a1 **)
    513 let rec internal_function_rect_Type2 h_mk_internal_function x_15466 =
     513let rec internal_function_rect_Type2 h_mk_internal_function x_15505 =
    514514  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    515515    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    516     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15466
     516    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15505
    517517  in
    518518  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    526526    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    527527    internal_function -> 'a1 **)
    528 let rec internal_function_rect_Type1 h_mk_internal_function x_15468 =
     528let rec internal_function_rect_Type1 h_mk_internal_function x_15507 =
    529529  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    530530    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    531     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15468
     531    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15507
    532532  in
    533533  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    541541    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
    542542    internal_function -> 'a1 **)
    543 let rec internal_function_rect_Type0 h_mk_internal_function x_15470 =
     543let rec internal_function_rect_Type0 h_mk_internal_function x_15509 =
    544544  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    545545    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    546     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15470
     546    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15509
    547547  in
    548548  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
     
    649649    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
    650650
    651 type rTLabs_program = (internal_function AST.fundef, Nat.nat) AST.program
    652 
     651type rTLabs_program =
     652  (internal_function AST.fundef, AST.init_data List.list) AST.program
     653
Note: See TracChangeset for help on using the changeset viewer.