Ignore:
Timestamp:
Mar 26, 2013, 4:51:40 PM (7 years ago)
Author:
sacerdot
Message:

New extraction, it diverges in RTL execution now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint_semantics.mli

    r2951 r2960  
    133133type 'f genv_gen = { ge : 'f AST.fundef Globalenvs.genv_t;
    134134                     stack_sizes : (AST.ident -> Nat.nat Types.option);
    135                      get_pc_from_label : (AST.ident -> Graphs.label ->
    136                                          ByteValues.program_counter
    137                                          Errors.res) }
     135                     premain : 'f;
     136                     pc_from_label : (Pointers.block Types.sig0 -> 'f ->
     137                                     Graphs.label ->
     138                                     ByteValues.program_counter Types.option) }
    138139
    139140val genv_gen_rect_Type4 :
    140141  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    141   (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    142   ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2
     142  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
     143  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
     144  'a1 genv_gen -> 'a2
    143145
    144146val genv_gen_rect_Type5 :
    145147  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    146   (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    147   ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2
     148  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
     149  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
     150  'a1 genv_gen -> 'a2
    148151
    149152val genv_gen_rect_Type3 :
    150153  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    151   (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    152   ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2
     154  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
     155  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
     156  'a1 genv_gen -> 'a2
    153157
    154158val genv_gen_rect_Type2 :
    155159  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    156   (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    157   ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2
     160  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
     161  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
     162  'a1 genv_gen -> 'a2
    158163
    159164val genv_gen_rect_Type1 :
    160165  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    161   (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    162   ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2
     166  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
     167  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
     168  'a1 genv_gen -> 'a2
    163169
    164170val genv_gen_rect_Type0 :
    165171  AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    166   (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    167   ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2
     172  (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 ->
     173  'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) ->
     174  'a1 genv_gen -> 'a2
    168175
    169176val ge :
     
    173180  AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Nat.nat Types.option
    174181
    175 val get_pc_from_label :
    176   AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
    177   ByteValues.program_counter Errors.res
     182val premain : AST.ident List.list -> 'a1 genv_gen -> 'a1
     183
     184val pc_from_label :
     185  AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 -> 'a1 ->
     186  Graphs.label -> ByteValues.program_counter Types.option
    178187
    179188val genv_gen_inv_rect_Type4 :
    180189  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
    181   __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    182   ByteValues.program_counter Errors.res) -> __ -> 'a2) -> 'a2
     190  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     191  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     192  Types.option) -> __ -> 'a2) -> 'a2
    183193
    184194val genv_gen_inv_rect_Type3 :
    185195  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
    186   __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    187   ByteValues.program_counter Errors.res) -> __ -> 'a2) -> 'a2
     196  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     197  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     198  Types.option) -> __ -> 'a2) -> 'a2
    188199
    189200val genv_gen_inv_rect_Type2 :
    190201  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
    191   __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    192   ByteValues.program_counter Errors.res) -> __ -> 'a2) -> 'a2
     202  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     203  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     204  Types.option) -> __ -> 'a2) -> 'a2
    193205
    194206val genv_gen_inv_rect_Type1 :
    195207  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
    196   __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    197   ByteValues.program_counter Errors.res) -> __ -> 'a2) -> 'a2
     208  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     209  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     210  Types.option) -> __ -> 'a2) -> 'a2
    198211
    199212val genv_gen_inv_rect_Type0 :
    200213  AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t ->
    201   __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    202   ByteValues.program_counter Errors.res) -> __ -> 'a2) -> 'a2
     214  __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     215  Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     216  Types.option) -> __ -> 'a2) -> 'a2
    203217
    204218val genv_gen_discr :
     
    227241  AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef
    228242  Globalenvs.genv_t
     243
     244val pre_main_id : AST.ident
     245
     246val fetch_function :
     247  AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
     248  (AST.ident, 'a1 AST.fundef) Types.prod Errors.res
     249
     250val fetch_internal_function :
     251  AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
     252  (AST.ident, 'a1) Types.prod Errors.res
     253
     254val code_block_of_block :
     255  Pointers.block -> Pointers.block Types.sig0 Types.option
     256
     257val block_of_funct_id :
     258  'a1 Globalenvs.genv_t -> PreIdentifiers.identifier -> Pointers.block
     259  Types.sig0 Errors.res
     260
     261val gen_pc_from_label :
     262  AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
     263  ByteValues.program_counter Errors.res
    229264
    230265type genv = Joint.joint_closed_internal_function genv_gen
     
    542577
    543578val set_frms : sem_state_params -> __ -> state -> state
    544 
    545 val fetch_function :
    546   'a1 Globalenvs.genv_t -> Pointers.block Types.sig0 -> (AST.ident, 'a1)
    547   Types.prod Errors.res
    548 
    549 val fetch_internal_function :
    550   'a1 AST.fundef Globalenvs.genv_t -> Pointers.block Types.sig0 ->
    551   (AST.ident, 'a1) Types.prod Errors.res
    552579
    553580type call_kind =
     
    12201247
    12211248val fetch_statement :
    1222   sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
    1223   -> ByteValues.program_counter -> ((AST.ident,
    1224   Joint.joint_closed_internal_function) Types.prod, Joint.joint_statement)
    1225   Types.prod Errors.res
     1249  sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter ->
     1250  ((AST.ident, Joint.joint_closed_internal_function) Types.prod,
     1251  Joint.joint_statement) Types.prod Errors.res
    12261252
    12271253val pc_of_label :
    1228   sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
    1229   -> Pointers.block Types.sig0 -> Graphs.label -> ByteValues.program_counter
    1230   Errors.res
     1254  sem_params -> AST.ident List.list -> genv -> Pointers.block Types.sig0 ->
     1255  Graphs.label -> ByteValues.program_counter Errors.res
    12311256
    12321257val succ_pc :
     
    12351260
    12361261val goto :
    1237   sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
    1238   -> Graphs.label -> state_pc -> state_pc Errors.res
     1262  sem_params -> AST.ident List.list -> genv -> Graphs.label -> state_pc ->
     1263  state_pc Errors.res
    12391264
    12401265val next : sem_params -> __ -> state_pc -> state_pc
    12411266
    12421267val next_of_call_pc :
    1243   sem_params -> AST.ident List.list -> Joint.joint_function Globalenvs.genv_t
    1244   -> ByteValues.program_counter -> __ Errors.res
     1268  sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter ->
     1269  __ Errors.res
    12451270
    12461271val eval_seq_no_pc :
    12471272  sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_seq
    12481273  -> state -> state Errors.res
    1249 
    1250 val code_block_of_block :
    1251   Pointers.block -> Pointers.block Types.sig0 Types.option
    1252 
    1253 val block_of_funct_id :
    1254   sem_state_params -> 'a1 Globalenvs.genv_t -> PreIdentifiers.identifier ->
    1255   Pointers.block Types.sig0 Errors.res
    12561274
    12571275val block_of_call :
Note: See TracChangeset for help on using the changeset viewer.