Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (8 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/semanticsUtils.mli

    r2829 r2951  
    146146
    147147open ExtraMonads
     148
     149val reg_store :
     150  PreIdentifiers.identifier -> ByteValues.beval -> ByteValues.beval
     151  Identifiers.identifier_map -> ByteValues.beval Identifiers.identifier_map
     152
     153val reg_retrieve :
     154  ByteValues.beval Registers.register_env -> Registers.register ->
     155  ByteValues.beval Errors.res
    148156
    149157type hw_register_env = { reg_env : ByteValues.beval
     
    203211val hw_register_env_jmdiscr : hw_register_env -> hw_register_env -> __
    204212
    205 val empty_hw_register_env : hw_register_env
    206 
    207213val hwreg_retrieve : hw_register_env -> I8051.register -> ByteValues.beval
    208214
     
    217223  hw_register_env -> ByteValues.xpointer -> hw_register_env
    218224
    219 type reg_sp = { reg_sp_env : ByteValues.beval Identifiers.identifier_map;
    220                 stackp : ByteValues.xpointer }
    221 
    222 val reg_sp_rect_Type4 :
    223   (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
    224   -> reg_sp -> 'a1
    225 
    226 val reg_sp_rect_Type5 :
    227   (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
    228   -> reg_sp -> 'a1
    229 
    230 val reg_sp_rect_Type3 :
    231   (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
    232   -> reg_sp -> 'a1
    233 
    234 val reg_sp_rect_Type2 :
    235   (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
    236   -> reg_sp -> 'a1
    237 
    238 val reg_sp_rect_Type1 :
    239   (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
    240   -> reg_sp -> 'a1
    241 
    242 val reg_sp_rect_Type0 :
    243   (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
    244   -> reg_sp -> 'a1
    245 
    246 val reg_sp_env : reg_sp -> ByteValues.beval Identifiers.identifier_map
    247 
    248 val stackp : reg_sp -> ByteValues.xpointer
    249 
    250 val reg_sp_inv_rect_Type4 :
    251   reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
    252   ByteValues.xpointer -> __ -> 'a1) -> 'a1
    253 
    254 val reg_sp_inv_rect_Type3 :
    255   reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
    256   ByteValues.xpointer -> __ -> 'a1) -> 'a1
    257 
    258 val reg_sp_inv_rect_Type2 :
    259   reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
    260   ByteValues.xpointer -> __ -> 'a1) -> 'a1
    261 
    262 val reg_sp_inv_rect_Type1 :
    263   reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
    264   ByteValues.xpointer -> __ -> 'a1) -> 'a1
    265 
    266 val reg_sp_inv_rect_Type0 :
    267   reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
    268   ByteValues.xpointer -> __ -> 'a1) -> 'a1
    269 
    270 val reg_sp_discr : reg_sp -> reg_sp -> __
    271 
    272 val reg_sp_jmdiscr : reg_sp -> reg_sp -> __
    273 
    274 val dpi1__o__reg_sp_env__o__inject :
    275   (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
    276   Types.sig0
    277 
    278 val eject__o__reg_sp_env__o__inject :
    279   reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map Types.sig0
    280 
    281 val reg_sp_env__o__inject :
    282   reg_sp -> ByteValues.beval Identifiers.identifier_map Types.sig0
    283 
    284 val dpi1__o__reg_sp_env :
    285   (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
    286 
    287 val eject__o__reg_sp_env :
    288   reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map
    289 
    290 val reg_store :
    291   PreIdentifiers.identifier -> ByteValues.beval -> ByteValues.beval
    292   Identifiers.identifier_map -> ByteValues.beval Identifiers.identifier_map
    293 
    294 val reg_retrieve :
    295   ByteValues.beval Registers.register_env -> Registers.register ->
    296   ByteValues.beval Errors.res
    297 
    298 val reg_sp_store :
    299   PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
    300 
    301 val reg_sp_retrieve :
    302   reg_sp -> Registers.register -> ByteValues.beval Errors.res
    303 
    304 val reg_sp_init : ByteValues.xpointer -> reg_sp
    305 
    306225val init_hw_register_env : ByteValues.xpointer -> hw_register_env
    307226
    308227type sem_graph_params = { sgp_pars : Joint.uns_params;
    309228                          sgp_sup : (__ -> __
    310                                     Joint_semantics.sem_unserialized_params) }
     229                                    Joint_semantics.sem_unserialized_params);
     230                          graph_pre_main_generator : (Joint.joint_program ->
     231                                                     Joint.joint_closed_internal_function) }
    311232
    312233val sem_graph_params_rect_Type4 :
    313234  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
    314   'a1) -> sem_graph_params -> 'a1
     235  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
     236  sem_graph_params -> 'a1
    315237
    316238val sem_graph_params_rect_Type5 :
    317239  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
    318   'a1) -> sem_graph_params -> 'a1
     240  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
     241  sem_graph_params -> 'a1
    319242
    320243val sem_graph_params_rect_Type3 :
    321244  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
    322   'a1) -> sem_graph_params -> 'a1
     245  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
     246  sem_graph_params -> 'a1
    323247
    324248val sem_graph_params_rect_Type2 :
    325249  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
    326   'a1) -> sem_graph_params -> 'a1
     250  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
     251  sem_graph_params -> 'a1
    327252
    328253val sem_graph_params_rect_Type1 :
    329254  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
    330   'a1) -> sem_graph_params -> 'a1
     255  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
     256  sem_graph_params -> 'a1
    331257
    332258val sem_graph_params_rect_Type0 :
    333259  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
    334   'a1) -> sem_graph_params -> 'a1
     260  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
     261  sem_graph_params -> 'a1
    335262
    336263val sgp_pars : sem_graph_params -> Joint.uns_params
     
    339266  sem_graph_params -> 'a1 Joint_semantics.sem_unserialized_params
    340267
     268val graph_pre_main_generator :
     269  sem_graph_params -> Joint.joint_program ->
     270  Joint.joint_closed_internal_function
     271
    341272val sem_graph_params_inv_rect_Type4 :
    342273  sem_graph_params -> (Joint.uns_params -> (__ -> __
    343   Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
     274  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     275  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
    344276
    345277val sem_graph_params_inv_rect_Type3 :
    346278  sem_graph_params -> (Joint.uns_params -> (__ -> __
    347   Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
     279  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     280  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
    348281
    349282val sem_graph_params_inv_rect_Type2 :
    350283  sem_graph_params -> (Joint.uns_params -> (__ -> __
    351   Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
     284  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     285  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
    352286
    353287val sem_graph_params_inv_rect_Type1 :
    354288  sem_graph_params -> (Joint.uns_params -> (__ -> __
    355   Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
     289  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     290  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
    356291
    357292val sem_graph_params_inv_rect_Type0 :
    358293  sem_graph_params -> (Joint.uns_params -> (__ -> __
    359   Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
     294  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     295  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
    360296
    361297val sem_graph_params_jmdiscr : sem_graph_params -> sem_graph_params -> __
     
    366302  sem_graph_params -> Joint_semantics.sem_params
    367303
    368 val sem_params_from_sem_graph_params__o__msu_pars :
     304val sem_params_from_sem_graph_params__o__spp' :
     305  sem_graph_params -> Joint_semantics.serialized_params
     306
     307val sem_params_from_sem_graph_params__o__spp'__o__msu_pars :
    369308  sem_graph_params -> Joint.joint_closed_internal_function
    370309  Joint_semantics.sem_unserialized_params
    371310
    372 val sem_params_from_sem_graph_params__o__msu_pars__o__st_pars :
     311val sem_params_from_sem_graph_params__o__spp'__o__msu_pars__o__st_pars :
    373312  sem_graph_params -> Joint_semantics.sem_state_params
    374313
    375 val sem_params_from_sem_graph_params__o__spp :
     314val sem_params_from_sem_graph_params__o__spp'__o__spp :
    376315  sem_graph_params -> Joint.params
    377316
    378 val sem_params_from_sem_graph_params__o__spp__o__stmt_pars :
     317val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars :
    379318  sem_graph_params -> Joint.stmt_params
    380319
    381 val sem_params_from_sem_graph_params__o__spp__o__stmt_pars__o__uns_pars :
     320val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    382321  sem_graph_params -> Joint.uns_params
    383322
    384 val sem_params_from_sem_graph_params__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
     323val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    385324  sem_graph_params -> Joint.unserialized_params
    386325
    387326type sem_lin_params = { slp_pars : Joint.uns_params;
    388327                        slp_sup : (__ -> __
    389                                   Joint_semantics.sem_unserialized_params) }
     328                                  Joint_semantics.sem_unserialized_params);
     329                        lin_pre_main_generator : (Joint.joint_program ->
     330                                                 Joint.joint_closed_internal_function) }
    390331
    391332val sem_lin_params_rect_Type4 :
    392333  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
    393   'a1) -> sem_lin_params -> 'a1
     334  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
     335  sem_lin_params -> 'a1
    394336
    395337val sem_lin_params_rect_Type5 :
    396338  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
    397   'a1) -> sem_lin_params -> 'a1
     339  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
     340  sem_lin_params -> 'a1
    398341
    399342val sem_lin_params_rect_Type3 :
    400343  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
    401   'a1) -> sem_lin_params -> 'a1
     344  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
     345  sem_lin_params -> 'a1
    402346
    403347val sem_lin_params_rect_Type2 :
    404348  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
    405   'a1) -> sem_lin_params -> 'a1
     349  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
     350  sem_lin_params -> 'a1
    406351
    407352val sem_lin_params_rect_Type1 :
    408353  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
    409   'a1) -> sem_lin_params -> 'a1
     354  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
     355  sem_lin_params -> 'a1
    410356
    411357val sem_lin_params_rect_Type0 :
    412358  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
    413   'a1) -> sem_lin_params -> 'a1
     359  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
     360  sem_lin_params -> 'a1
    414361
    415362val slp_pars : sem_lin_params -> Joint.uns_params
    416363
    417364val slp_sup0 : sem_lin_params -> 'a1 Joint_semantics.sem_unserialized_params
     365
     366val lin_pre_main_generator :
     367  sem_lin_params -> Joint.joint_program ->
     368  Joint.joint_closed_internal_function
    418369
    419370val sem_lin_params_inv_rect_Type4 :
    420371  sem_lin_params -> (Joint.uns_params -> (__ -> __
    421   Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
     372  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     373  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
    422374
    423375val sem_lin_params_inv_rect_Type3 :
    424376  sem_lin_params -> (Joint.uns_params -> (__ -> __
    425   Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
     377  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     378  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
    426379
    427380val sem_lin_params_inv_rect_Type2 :
    428381  sem_lin_params -> (Joint.uns_params -> (__ -> __
    429   Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
     382  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     383  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
    430384
    431385val sem_lin_params_inv_rect_Type1 :
    432386  sem_lin_params -> (Joint.uns_params -> (__ -> __
    433   Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
     387  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     388  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
    434389
    435390val sem_lin_params_inv_rect_Type0 :
    436391  sem_lin_params -> (Joint.uns_params -> (__ -> __
    437   Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
     392  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
     393  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
    438394
    439395val sem_lin_params_jmdiscr : sem_lin_params -> sem_lin_params -> __
     
    444400  sem_lin_params -> Joint_semantics.sem_params
    445401
    446 val sem_params_from_sem_lin_params__o__msu_pars :
     402val sem_params_from_sem_lin_params__o__spp' :
     403  sem_lin_params -> Joint_semantics.serialized_params
     404
     405val sem_params_from_sem_lin_params__o__spp'__o__msu_pars :
    447406  sem_lin_params -> Joint.joint_closed_internal_function
    448407  Joint_semantics.sem_unserialized_params
    449408
    450 val sem_params_from_sem_lin_params__o__msu_pars__o__st_pars :
     409val sem_params_from_sem_lin_params__o__spp'__o__msu_pars__o__st_pars :
    451410  sem_lin_params -> Joint_semantics.sem_state_params
    452411
    453 val sem_params_from_sem_lin_params__o__spp : sem_lin_params -> Joint.params
    454 
    455 val sem_params_from_sem_lin_params__o__spp__o__stmt_pars :
     412val sem_params_from_sem_lin_params__o__spp'__o__spp :
     413  sem_lin_params -> Joint.params
     414
     415val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars :
    456416  sem_lin_params -> Joint.stmt_params
    457417
    458 val sem_params_from_sem_lin_params__o__spp__o__stmt_pars__o__uns_pars :
     418val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    459419  sem_lin_params -> Joint.uns_params
    460420
    461 val sem_params_from_sem_lin_params__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
     421val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    462422  sem_lin_params -> Joint.unserialized_params
    463423
     424val pre_main_id : AST.ident
     425
     426val joint_globalenv :
     427  Joint_semantics.sem_params -> Joint.joint_program ->
     428  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     429
    464430val match_genv_t_rect_Type4 :
    465431  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
Note: See TracChangeset for help on using the changeset viewer.