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/rTL_semantics.mli

    r2829 r2951  
    150150
    151151open RTL
     152
     153type reg_sp = { reg_sp_env : ByteValues.beval Identifiers.identifier_map;
     154                stackp : ByteValues.xpointer }
     155
     156val reg_sp_rect_Type4 :
     157  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
     158  -> reg_sp -> 'a1
     159
     160val reg_sp_rect_Type5 :
     161  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
     162  -> reg_sp -> 'a1
     163
     164val reg_sp_rect_Type3 :
     165  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
     166  -> reg_sp -> 'a1
     167
     168val reg_sp_rect_Type2 :
     169  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
     170  -> reg_sp -> 'a1
     171
     172val reg_sp_rect_Type1 :
     173  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
     174  -> reg_sp -> 'a1
     175
     176val reg_sp_rect_Type0 :
     177  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
     178  -> reg_sp -> 'a1
     179
     180val reg_sp_env : reg_sp -> ByteValues.beval Identifiers.identifier_map
     181
     182val stackp : reg_sp -> ByteValues.xpointer
     183
     184val reg_sp_inv_rect_Type4 :
     185  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
     186  ByteValues.xpointer -> __ -> 'a1) -> 'a1
     187
     188val reg_sp_inv_rect_Type3 :
     189  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
     190  ByteValues.xpointer -> __ -> 'a1) -> 'a1
     191
     192val reg_sp_inv_rect_Type2 :
     193  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
     194  ByteValues.xpointer -> __ -> 'a1) -> 'a1
     195
     196val reg_sp_inv_rect_Type1 :
     197  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
     198  ByteValues.xpointer -> __ -> 'a1) -> 'a1
     199
     200val reg_sp_inv_rect_Type0 :
     201  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
     202  ByteValues.xpointer -> __ -> 'a1) -> 'a1
     203
     204val reg_sp_discr : reg_sp -> reg_sp -> __
     205
     206val reg_sp_jmdiscr : reg_sp -> reg_sp -> __
     207
     208val dpi1__o__reg_sp_env__o__inject :
     209  (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
     210  Types.sig0
     211
     212val eject__o__reg_sp_env__o__inject :
     213  reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map Types.sig0
     214
     215val reg_sp_env__o__inject :
     216  reg_sp -> ByteValues.beval Identifiers.identifier_map Types.sig0
     217
     218val dpi1__o__reg_sp_env :
     219  (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
     220
     221val eject__o__reg_sp_env :
     222  reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map
     223
     224val reg_sp_store :
     225  PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
     226
     227val reg_sp_retrieve :
     228  reg_sp -> Registers.register -> ByteValues.beval Errors.res
     229
     230val reg_sp_empty : ByteValues.xpointer -> reg_sp
    152231
    153232type frame = { fr_ret_regs : Registers.register List.list;
    154233               fr_pc : ByteValues.program_counter;
    155                fr_carry : ByteValues.bebit; fr_regs : SemanticsUtils.reg_sp }
     234               fr_carry : ByteValues.bebit; fr_regs : reg_sp }
    156235
    157236val frame_rect_Type4 :
    158237  (Registers.register List.list -> ByteValues.program_counter ->
    159   ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1
     238  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
    160239
    161240val frame_rect_Type5 :
    162241  (Registers.register List.list -> ByteValues.program_counter ->
    163   ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1
     242  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
    164243
    165244val frame_rect_Type3 :
    166245  (Registers.register List.list -> ByteValues.program_counter ->
    167   ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1
     246  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
    168247
    169248val frame_rect_Type2 :
    170249  (Registers.register List.list -> ByteValues.program_counter ->
    171   ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1
     250  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
    172251
    173252val frame_rect_Type1 :
    174253  (Registers.register List.list -> ByteValues.program_counter ->
    175   ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1
     254  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
    176255
    177256val frame_rect_Type0 :
    178257  (Registers.register List.list -> ByteValues.program_counter ->
    179   ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1
     258  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
    180259
    181260val fr_ret_regs : frame -> Registers.register List.list
     
    185264val fr_carry : frame -> ByteValues.bebit
    186265
    187 val fr_regs : frame -> SemanticsUtils.reg_sp
     266val fr_regs : frame -> reg_sp
    188267
    189268val frame_inv_rect_Type4 :
    190269  frame -> (Registers.register List.list -> ByteValues.program_counter ->
    191   ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1
     270  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
    192271
    193272val frame_inv_rect_Type3 :
    194273  frame -> (Registers.register List.list -> ByteValues.program_counter ->
    195   ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1
     274  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
    196275
    197276val frame_inv_rect_Type2 :
    198277  frame -> (Registers.register List.list -> ByteValues.program_counter ->
    199   ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1
     278  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
    200279
    201280val frame_inv_rect_Type1 :
    202281  frame -> (Registers.register List.list -> ByteValues.program_counter ->
    203   ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1
     282  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
    204283
    205284val frame_inv_rect_Type0 :
    206285  frame -> (Registers.register List.list -> ByteValues.program_counter ->
    207   ByteValues.bebit -> SemanticsUtils.reg_sp -> __ -> 'a1) -> 'a1
     286  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
    208287
    209288val frame_discr : frame -> frame -> __
     
    216295
    217296val rtl_arg_retrieve :
    218   SemanticsUtils.reg_sp -> Joint.psd_argument -> ByteValues.beval Errors.res
     297  reg_sp -> Joint.psd_argument -> ByteValues.beval Errors.res
    219298
    220299val rtl_fetch_ra :
    221300  rTL_state -> (rTL_state, ByteValues.program_counter) Types.prod Errors.res
    222301
    223 val rtl_init_local :
    224   Registers.register -> SemanticsUtils.reg_sp -> SemanticsUtils.reg_sp
     302val rtl_init_local : Registers.register -> reg_sp -> reg_sp
    225303
    226304val rtl_setup_call_separate :
     
    228306  rTL_state -> rTL_state Errors.res
    229307
     308val stackOverflow : ErrorMessages.errorMessage
     309
     310val rtl_setup_call_separate_overflow :
     311  Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
     312  rTL_state -> rTL_state Errors.res
     313
    230314val rtl_setup_call_unique :
    231315  Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
     
    271355
    272356val reg_res_store :
    273   PreIdentifiers.identifier -> ByteValues.beval -> SemanticsUtils.reg_sp ->
    274   SemanticsUtils.reg_sp Errors.res
     357  PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
     358  Errors.res
    275359
    276360val rTL_semantics_separate : SemanticsUtils.sem_graph_params
    277361
     362val rTL_semantics_separate_overflow : SemanticsUtils.sem_graph_params
     363
    278364val rTL_semantics_unique : SemanticsUtils.sem_graph_params
    279365
Note: See TracChangeset for help on using the changeset viewer.