Changeset 2960 for extracted/traces.ml


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

    r2951 r2960  
    152152
    153153type evaluation_params = { globals : AST.ident List.list;
    154                            sparams : Joint_semantics.sem_params;
    155154                           ev_genv : Joint_semantics.genv }
    156155
    157156(** val evaluation_params_rect_Type4 :
    158     (AST.ident List.list -> Joint_semantics.sem_params ->
     157    Joint_semantics.sem_params -> (AST.ident List.list ->
    159158    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    160 let rec evaluation_params_rect_Type4 h_mk_evaluation_params x_5953 =
    161   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5953
    162   in
    163   h_mk_evaluation_params globals0 sparams0 ev_genv0
     159let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_55 =
     160  let { globals = globals0; ev_genv = ev_genv0 } = x_55 in
     161  h_mk_evaluation_params globals0 ev_genv0
    164162
    165163(** val evaluation_params_rect_Type5 :
    166     (AST.ident List.list -> Joint_semantics.sem_params ->
     164    Joint_semantics.sem_params -> (AST.ident List.list ->
    167165    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    168 let rec evaluation_params_rect_Type5 h_mk_evaluation_params x_5955 =
    169   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5955
    170   in
    171   h_mk_evaluation_params globals0 sparams0 ev_genv0
     166let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_57 =
     167  let { globals = globals0; ev_genv = ev_genv0 } = x_57 in
     168  h_mk_evaluation_params globals0 ev_genv0
    172169
    173170(** val evaluation_params_rect_Type3 :
    174     (AST.ident List.list -> Joint_semantics.sem_params ->
     171    Joint_semantics.sem_params -> (AST.ident List.list ->
    175172    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    176 let rec evaluation_params_rect_Type3 h_mk_evaluation_params x_5957 =
    177   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5957
    178   in
    179   h_mk_evaluation_params globals0 sparams0 ev_genv0
     173let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_59 =
     174  let { globals = globals0; ev_genv = ev_genv0 } = x_59 in
     175  h_mk_evaluation_params globals0 ev_genv0
    180176
    181177(** val evaluation_params_rect_Type2 :
    182     (AST.ident List.list -> Joint_semantics.sem_params ->
     178    Joint_semantics.sem_params -> (AST.ident List.list ->
    183179    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    184 let rec evaluation_params_rect_Type2 h_mk_evaluation_params x_5959 =
    185   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5959
    186   in
    187   h_mk_evaluation_params globals0 sparams0 ev_genv0
     180let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_61 =
     181  let { globals = globals0; ev_genv = ev_genv0 } = x_61 in
     182  h_mk_evaluation_params globals0 ev_genv0
    188183
    189184(** val evaluation_params_rect_Type1 :
    190     (AST.ident List.list -> Joint_semantics.sem_params ->
     185    Joint_semantics.sem_params -> (AST.ident List.list ->
    191186    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    192 let rec evaluation_params_rect_Type1 h_mk_evaluation_params x_5961 =
    193   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5961
    194   in
    195   h_mk_evaluation_params globals0 sparams0 ev_genv0
     187let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_63 =
     188  let { globals = globals0; ev_genv = ev_genv0 } = x_63 in
     189  h_mk_evaluation_params globals0 ev_genv0
    196190
    197191(** val evaluation_params_rect_Type0 :
    198     (AST.ident List.list -> Joint_semantics.sem_params ->
     192    Joint_semantics.sem_params -> (AST.ident List.list ->
    199193    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    200 let rec evaluation_params_rect_Type0 h_mk_evaluation_params x_5963 =
    201   let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } = x_5963
    202   in
    203   h_mk_evaluation_params globals0 sparams0 ev_genv0
    204 
    205 (** val globals : evaluation_params -> AST.ident List.list **)
    206 let rec globals xxx =
     194let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_65 =
     195  let { globals = globals0; ev_genv = ev_genv0 } = x_65 in
     196  h_mk_evaluation_params globals0 ev_genv0
     197
     198(** val globals :
     199    Joint_semantics.sem_params -> evaluation_params -> AST.ident List.list **)
     200let rec globals p xxx =
    207201  xxx.globals
    208202
    209 (** val sparams : evaluation_params -> Joint_semantics.sem_params **)
    210 let rec sparams xxx =
    211   xxx.sparams
    212 
    213 (** val ev_genv : evaluation_params -> Joint_semantics.genv **)
    214 let rec ev_genv xxx =
     203(** val ev_genv :
     204    Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv **)
     205let rec ev_genv p xxx =
    215206  xxx.ev_genv
    216207
    217208(** val evaluation_params_inv_rect_Type4 :
    218     evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params
     209    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
    219210    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    220 let evaluation_params_inv_rect_Type4 hterm h1 =
    221   let hcut = evaluation_params_rect_Type4 h1 hterm in hcut __
     211let evaluation_params_inv_rect_Type4 x1 hterm h1 =
     212  let hcut = evaluation_params_rect_Type4 x1 h1 hterm in hcut __
    222213
    223214(** val evaluation_params_inv_rect_Type3 :
    224     evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params
     215    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
    225216    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    226 let evaluation_params_inv_rect_Type3 hterm h1 =
    227   let hcut = evaluation_params_rect_Type3 h1 hterm in hcut __
     217let evaluation_params_inv_rect_Type3 x1 hterm h1 =
     218  let hcut = evaluation_params_rect_Type3 x1 h1 hterm in hcut __
    228219
    229220(** val evaluation_params_inv_rect_Type2 :
    230     evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params
     221    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
    231222    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    232 let evaluation_params_inv_rect_Type2 hterm h1 =
    233   let hcut = evaluation_params_rect_Type2 h1 hterm in hcut __
     223let evaluation_params_inv_rect_Type2 x1 hterm h1 =
     224  let hcut = evaluation_params_rect_Type2 x1 h1 hterm in hcut __
    234225
    235226(** val evaluation_params_inv_rect_Type1 :
    236     evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params
     227    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
    237228    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    238 let evaluation_params_inv_rect_Type1 hterm h1 =
    239   let hcut = evaluation_params_rect_Type1 h1 hterm in hcut __
     229let evaluation_params_inv_rect_Type1 x1 hterm h1 =
     230  let hcut = evaluation_params_rect_Type1 x1 h1 hterm in hcut __
    240231
    241232(** val evaluation_params_inv_rect_Type0 :
    242     evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params
     233    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
    243234    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    244 let evaluation_params_inv_rect_Type0 hterm h1 =
    245   let hcut = evaluation_params_rect_Type0 h1 hterm in hcut __
     235let evaluation_params_inv_rect_Type0 x1 hterm h1 =
     236  let hcut = evaluation_params_rect_Type0 x1 h1 hterm in hcut __
     237
     238(** val evaluation_params_discr :
     239    Joint_semantics.sem_params -> evaluation_params -> evaluation_params ->
     240    __ **)
     241let evaluation_params_discr a1 x y =
     242  Logic.eq_rect_Type2 x
     243    (let { globals = a0; ev_genv = a10 } = x in
     244    Obj.magic (fun _ dH -> dH __ __)) y
    246245
    247246(** val evaluation_params_jmdiscr :
    248     evaluation_params -> evaluation_params -> __ **)
    249 let evaluation_params_jmdiscr x y =
     247    Joint_semantics.sem_params -> evaluation_params -> evaluation_params ->
     248    __ **)
     249let evaluation_params_jmdiscr a1 x y =
    250250  Logic.eq_rect_Type2 x
    251     (let { globals = a0; sparams = a1; ev_genv = a2 } = x in
    252     Obj.magic (fun _ dH -> dH __ __ __)) y
    253 
    254 (** val sparams__o__spp' :
    255     evaluation_params -> Joint_semantics.serialized_params **)
    256 let sparams__o__spp' x0 =
    257   x0.sparams.Joint_semantics.spp'
    258 
    259 (** val sparams__o__spp'__o__msu_pars :
    260     evaluation_params -> Joint.joint_closed_internal_function
    261     Joint_semantics.sem_unserialized_params **)
    262 let sparams__o__spp'__o__msu_pars x0 =
    263   Joint_semantics.spp'__o__msu_pars x0.sparams
    264 
    265 (** val sparams__o__spp'__o__msu_pars__o__st_pars :
    266     evaluation_params -> Joint_semantics.sem_state_params **)
    267 let sparams__o__spp'__o__msu_pars__o__st_pars x0 =
    268   Joint_semantics.spp'__o__msu_pars__o__st_pars x0.sparams
    269 
    270 (** val sparams__o__spp'__o__spp : evaluation_params -> Joint.params **)
    271 let sparams__o__spp'__o__spp x0 =
    272   Joint_semantics.spp'__o__spp x0.sparams
    273 
    274 (** val sparams__o__spp'__o__spp__o__stmt_pars :
    275     evaluation_params -> Joint.stmt_params **)
    276 let sparams__o__spp'__o__spp__o__stmt_pars x0 =
    277   Joint_semantics.spp'__o__spp__o__stmt_pars x0.sparams
    278 
    279 (** val sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    280     evaluation_params -> Joint.uns_params **)
    281 let sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
    282   Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars x0.sparams
    283 
    284 (** val sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    285     evaluation_params -> Joint.unserialized_params **)
    286 let sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
    287   Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
    288     x0.sparams
     251    (let { globals = a0; ev_genv = a10 } = x in
     252    Obj.magic (fun _ dH -> dH __ __)) y
     253
     254(** val dpi1__o__ev_genv__o__inject :
     255    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
     256    Joint_semantics.genv Types.sig0 **)
     257let dpi1__o__ev_genv__o__inject x0 x2 =
     258  x2.Types.dpi1.ev_genv
     259
     260(** val dpi1__o__ev_genv__o__genv_to_genv_t__o__inject :
     261    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
     262    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     263    Types.sig0 **)
     264let dpi1__o__ev_genv__o__genv_to_genv_t__o__inject x0 x2 =
     265  Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
     266    x2.Types.dpi1.globals x2.Types.dpi1.ev_genv
     267
     268(** val dpi1__o__ev_genv__o__genv_to_genv_t :
     269    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
     270    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
     271let dpi1__o__ev_genv__o__genv_to_genv_t x0 x2 =
     272  let p = Joint_semantics.spp'__o__spp x0 in
     273  let globals0 = x2.Types.dpi1.globals in
     274  let g = x2.Types.dpi1.ev_genv in g.Joint_semantics.ge
     275
     276(** val eject__o__ev_genv__o__inject :
     277    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
     278    Joint_semantics.genv Types.sig0 **)
     279let eject__o__ev_genv__o__inject x0 x2 =
     280  (Types.pi1 x2).ev_genv
     281
     282(** val eject__o__ev_genv__o__genv_to_genv_t__o__inject :
     283    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
     284    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     285    Types.sig0 **)
     286let eject__o__ev_genv__o__genv_to_genv_t__o__inject x0 x2 =
     287  Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
     288    (Types.pi1 x2).globals (Types.pi1 x2).ev_genv
     289
     290(** val eject__o__ev_genv__o__genv_to_genv_t :
     291    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
     292    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
     293let eject__o__ev_genv__o__genv_to_genv_t x0 x2 =
     294  let p = Joint_semantics.spp'__o__spp x0 in
     295  let globals0 = (Types.pi1 x2).globals in
     296  let g = (Types.pi1 x2).ev_genv in g.Joint_semantics.ge
     297
     298(** val ev_genv__o__genv_to_genv_t :
     299    Joint_semantics.sem_params -> evaluation_params ->
     300    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
     301let ev_genv__o__genv_to_genv_t x0 x1 =
     302  let p = Joint_semantics.spp'__o__spp x0 in
     303  let globals0 = x1.globals in let g = x1.ev_genv in g.Joint_semantics.ge
     304
     305(** val ev_genv__o__genv_to_genv_t__o__inject :
     306    Joint_semantics.sem_params -> evaluation_params ->
     307    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     308    Types.sig0 **)
     309let ev_genv__o__genv_to_genv_t__o__inject x0 x1 =
     310  Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
     311    x1.globals x1.ev_genv
     312
     313(** val ev_genv__o__inject :
     314    Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
     315    Types.sig0 **)
     316let ev_genv__o__inject x0 x1 =
     317  x1.ev_genv
     318
     319(** val dpi1__o__ev_genv :
     320    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
     321    Joint_semantics.genv **)
     322let dpi1__o__ev_genv x0 x2 =
     323  x2.Types.dpi1.ev_genv
     324
     325(** val eject__o__ev_genv :
     326    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
     327    Joint_semantics.genv **)
     328let eject__o__ev_genv x0 x2 =
     329  (Types.pi1 x2).ev_genv
    289330
    290331type prog_params = { prog_spars : Joint_semantics.sem_params;
     
    295336    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    296337    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    297 let rec prog_params_rect_Type4 h_mk_prog_params x_5979 =
     338let rec prog_params_rect_Type4 h_mk_prog_params x_81 =
    298339  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    299     stack_sizes0 } = x_5979
     340    stack_sizes0 } = x_81
    300341  in
    301342  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    304345    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    305346    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    306 let rec prog_params_rect_Type5 h_mk_prog_params x_5981 =
     347let rec prog_params_rect_Type5 h_mk_prog_params x_83 =
    307348  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    308     stack_sizes0 } = x_5981
     349    stack_sizes0 } = x_83
    309350  in
    310351  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    313354    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    314355    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    315 let rec prog_params_rect_Type3 h_mk_prog_params x_5983 =
     356let rec prog_params_rect_Type3 h_mk_prog_params x_85 =
    316357  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    317     stack_sizes0 } = x_5983
     358    stack_sizes0 } = x_85
    318359  in
    319360  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    322363    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    323364    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    324 let rec prog_params_rect_Type2 h_mk_prog_params x_5985 =
     365let rec prog_params_rect_Type2 h_mk_prog_params x_87 =
    325366  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    326     stack_sizes0 } = x_5985
     367    stack_sizes0 } = x_87
    327368  in
    328369  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    331372    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    332373    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    333 let rec prog_params_rect_Type1 h_mk_prog_params x_5987 =
     374let rec prog_params_rect_Type1 h_mk_prog_params x_89 =
    334375  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    335     stack_sizes0 } = x_5987
     376    stack_sizes0 } = x_89
    336377  in
    337378  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    340381    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    341382    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    342 let rec prog_params_rect_Type0 h_mk_prog_params x_5989 =
     383let rec prog_params_rect_Type0 h_mk_prog_params x_91 =
    343384  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    344     stack_sizes0 } = x_5989
     385    stack_sizes0 } = x_91
    345386  in
    346387  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    394435    Obj.magic (fun _ dH -> dH __ __ __)) y
    395436
    396 (** val make_global : prog_params -> evaluation_params **)
    397 let make_global pars =
    398   let p = pars.prog in
    399   let spars = pars.prog_spars in
    400   let genv = SemanticsUtils.joint_globalenv spars p in
    401   let get_pc_lbl = fun id lbl ->
    402     Monad.m_bind0 (Monad.max_def Errors.res0)
    403       (Obj.magic
    404         (Joint_semantics.block_of_funct_id
    405           (Joint_semantics.spp'__o__msu_pars__o__st_pars spars) genv id))
    406       (fun bl ->
    407       Obj.magic
    408         (Joint_semantics.pc_of_label pars.prog_spars
    409           (AST.prog_var_names p.Joint.joint_prog) genv bl lbl))
    410   in
    411   { globals = (AST.prog_var_names p.Joint.joint_prog); sparams = spars;
    412   ev_genv = { Joint_semantics.ge = genv; Joint_semantics.stack_sizes =
    413   pars.stack_sizes; Joint_semantics.get_pc_from_label =
    414   (Obj.magic get_pc_lbl) } }
    415 
    416 (** val prog_params_to_ev_params__o__sparams :
    417     prog_params -> Joint_semantics.sem_params **)
    418 let prog_params_to_ev_params__o__sparams x0 =
    419   (make_global x0).sparams
    420 
    421 (** val prog_params_to_ev_params__o__sparams__o__spp' :
     437(** val prog_spars__o__spp' :
    422438    prog_params -> Joint_semantics.serialized_params **)
    423 let prog_params_to_ev_params__o__sparams__o__spp' x0 =
    424   sparams__o__spp' (make_global x0)
    425 
    426 (** val prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars :
     439let prog_spars__o__spp' x0 =
     440  x0.prog_spars.Joint_semantics.spp'
     441
     442(** val prog_spars__o__spp'__o__msu_pars :
    427443    prog_params -> Joint.joint_closed_internal_function
    428444    Joint_semantics.sem_unserialized_params **)
    429 let prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars x0 =
    430   sparams__o__spp'__o__msu_pars (make_global x0)
    431 
    432 (** val prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars :
     445let prog_spars__o__spp'__o__msu_pars x0 =
     446  Joint_semantics.spp'__o__msu_pars x0.prog_spars
     447
     448(** val prog_spars__o__spp'__o__msu_pars__o__st_pars :
    433449    prog_params -> Joint_semantics.sem_state_params **)
    434 let prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars x0 =
    435   sparams__o__spp'__o__msu_pars__o__st_pars (make_global x0)
    436 
    437 (** val prog_params_to_ev_params__o__sparams__o__spp'__o__spp :
    438     prog_params -> Joint.params **)
    439 let prog_params_to_ev_params__o__sparams__o__spp'__o__spp x0 =
    440   sparams__o__spp'__o__spp (make_global x0)
    441 
    442 (** val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars :
     450let prog_spars__o__spp'__o__msu_pars__o__st_pars x0 =
     451  Joint_semantics.spp'__o__msu_pars__o__st_pars x0.prog_spars
     452
     453(** val prog_spars__o__spp'__o__spp : prog_params -> Joint.params **)
     454let prog_spars__o__spp'__o__spp x0 =
     455  Joint_semantics.spp'__o__spp x0.prog_spars
     456
     457(** val prog_spars__o__spp'__o__spp__o__stmt_pars :
    443458    prog_params -> Joint.stmt_params **)
    444 let prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars x0 =
    445   sparams__o__spp'__o__spp__o__stmt_pars (make_global x0)
    446 
    447 (** val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
     459let prog_spars__o__spp'__o__spp__o__stmt_pars x0 =
     460  Joint_semantics.spp'__o__spp__o__stmt_pars x0.prog_spars
     461
     462(** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    448463    prog_params -> Joint.uns_params **)
    449 let prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
    450   sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars (make_global x0)
    451 
    452 (** val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
     464let prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
     465  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars x0.prog_spars
     466
     467(** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    453468    prog_params -> Joint.unserialized_params **)
    454 let prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
    455   sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
    456     (make_global x0)
     469let prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
     470  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
     471    x0.prog_spars
     472
     473(** val joint_make_global : prog_params -> evaluation_params **)
     474let joint_make_global p =
     475  { globals = (AST.prog_var_names p.prog.Joint.joint_prog); ev_genv =
     476    (SemanticsUtils.joint_globalenv p.prog_spars p.prog p.stack_sizes) }
     477
     478(** val joint_make_global__o__ev_genv :
     479    prog_params -> Joint_semantics.genv **)
     480let joint_make_global__o__ev_genv x0 =
     481  (joint_make_global x0).ev_genv
     482
     483(** val joint_make_global__o__ev_genv__o__genv_to_genv_t :
     484    prog_params -> Joint.joint_closed_internal_function AST.fundef
     485    Globalenvs.genv_t **)
     486let joint_make_global__o__ev_genv__o__genv_to_genv_t x0 =
     487  ev_genv__o__genv_to_genv_t x0.prog_spars (joint_make_global x0)
     488
     489(** val joint_make_global__o__ev_genv__o__genv_to_genv_t__o__inject :
     490    prog_params -> Joint.joint_closed_internal_function AST.fundef
     491    Globalenvs.genv_t Types.sig0 **)
     492let joint_make_global__o__ev_genv__o__genv_to_genv_t__o__inject x0 =
     493  ev_genv__o__genv_to_genv_t__o__inject x0.prog_spars (joint_make_global x0)
     494
     495(** val joint_make_global__o__ev_genv__o__inject :
     496    prog_params -> Joint_semantics.genv Types.sig0 **)
     497let joint_make_global__o__ev_genv__o__inject x0 =
     498  ev_genv__o__inject x0.prog_spars (joint_make_global x0)
     499
     500(** val joint_make_global__o__inject :
     501    prog_params -> evaluation_params Types.sig0 **)
     502let joint_make_global__o__inject x0 =
     503  joint_make_global x0
    457504
    458505(** val make_initial_state : prog_params -> Joint_semantics.state_pc **)
    459506let make_initial_state pars =
    460507  let p = pars.prog in
    461   let sem_globals = make_global pars in
    462   let ge = sem_globals.ev_genv in
     508  let ge = ev_genv pars.prog_spars in
    463509  let m0 =
    464510    (Globalenvs.globalenv_allocmem (fun x -> x) p.Joint.joint_prog).Types.snd
     
    478524  let main = p.Joint.joint_prog.AST.prog_main in
    479525  let st = { Joint_semantics.st_frms = (Types.Some
    480     (prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars
    481       pars).Joint_semantics.empty_framesT); Joint_semantics.istack =
    482     Joint_semantics.Empty_is; Joint_semantics.carry = (ByteValues.BBbit
    483     Bool.False); Joint_semantics.regs =
    484     ((prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars
    485        pars).Joint_semantics.empty_regsT spp); Joint_semantics.m = m;
    486     Joint_semantics.stack_usage = globals_size }
     526    (prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_framesT);
     527    Joint_semantics.istack = Joint_semantics.Empty_is;
     528    Joint_semantics.carry = (ByteValues.BBbit Bool.False);
     529    Joint_semantics.regs =
     530    ((prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_regsT
     531      spp); Joint_semantics.m = m; Joint_semantics.stack_usage =
     532    globals_size }
    487533  in
    488534  { Joint_semantics.st_no_pc =
    489   (Joint_semantics.set_sp
    490     (prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars
    491       pars) spp st); Joint_semantics.pc = Joint_semantics.init_pc;
     535  (Joint_semantics.set_sp (prog_spars__o__spp'__o__msu_pars__o__st_pars pars)
     536    spp st); Joint_semantics.pc = Joint_semantics.init_pc;
    492537  Joint_semantics.last_pop = (Joint_semantics.null_pc Positive.One) })) __
    493538
    494539(** val joint_classify_step :
    495     evaluation_params -> Joint.joint_step -> StructuredTraces.status_class **)
    496 let joint_classify_step p = function
     540    Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
     541    StructuredTraces.status_class **)
     542let joint_classify_step p g = function
    497543| Joint.COST_LABEL x -> StructuredTraces.Cl_other
    498544| Joint.CALL (f, args, dest) -> StructuredTraces.Cl_call
     
    501547
    502548(** val joint_classify_final :
    503     evaluation_params -> Joint.joint_fin_step ->
     549    Joint.unserialized_params -> Joint.joint_fin_step ->
    504550    StructuredTraces.status_class **)
    505551let joint_classify_final p = function
     
    509555
    510556(** val joint_classify :
    511     evaluation_params -> Joint_semantics.state_pc ->
    512     StructuredTraces.status_class **)
    513 let joint_classify p st =
    514   match Joint_semantics.fetch_statement p.sparams p.globals
    515           (let p0 = Joint_semantics.spp'__o__spp p.sparams in
    516           let globals0 = p.globals in
    517           let g = p.ev_genv in g.Joint_semantics.ge) st.Joint_semantics.pc with
     557    Joint_semantics.sem_params -> evaluation_params ->
     558    Joint_semantics.state_pc -> StructuredTraces.status_class **)
     559let joint_classify p pars st =
     560  match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
     561          st.Joint_semantics.pc with
    518562  | Errors.OK i_fn_s ->
    519563    (match i_fn_s.Types.snd with
    520      | Joint.Sequential (s, x) -> joint_classify_step p s
    521      | Joint.Final s -> joint_classify_final p s
     564     | Joint.Sequential (s, x) ->
     565       joint_classify_step
     566         (Joint.uns_pars__o__u_pars
     567           (Joint_semantics.spp'__o__spp__o__stmt_pars p)) pars.globals s
     568     | Joint.Final s ->
     569       joint_classify_final
     570         (Joint.uns_pars__o__u_pars
     571           (Joint_semantics.spp'__o__spp__o__stmt_pars p)) s
    522572     | Joint.FCOND (x0, x1, x2) -> StructuredTraces.Cl_jump)
    523573  | Errors.Error x -> StructuredTraces.Cl_other
    524574
    525575(** val joint_call_ident :
    526     evaluation_params -> Joint_semantics.state_pc -> AST.ident **)
    527 let joint_call_ident p st =
     576    Joint_semantics.sem_params -> evaluation_params ->
     577    Joint_semantics.state_pc -> AST.ident **)
     578let joint_call_ident p pars st =
    528579  let dummy = Positive.One in
    529   (match Joint_semantics.fetch_statement p.sparams p.globals
    530            (let p0 = Joint_semantics.spp'__o__spp p.sparams in
    531            let globals0 = p.globals in
    532            let g = p.ev_genv in g.Joint_semantics.ge) st.Joint_semantics.pc with
     580  (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
     581           st.Joint_semantics.pc with
    533582   | Errors.OK x ->
    534583     (match x.Types.snd with
     
    539588           (match Obj.magic
    540589                    (Monad.m_bind0 (Monad.max_def Errors.res0)
    541                       (Joint_semantics.block_of_call p.sparams p.globals
    542                         (let p0 = Joint_semantics.spp'__o__spp p.sparams in
    543                         let globals0 = p.globals in
    544                         let g = p.ev_genv in g.Joint_semantics.ge) f'
     590                      (Joint_semantics.block_of_call p pars.globals
     591                        (let p0 = Joint_semantics.spp'__o__spp p in
     592                        let globals0 = pars.globals in
     593                        let g = pars.ev_genv in g.Joint_semantics.ge) f'
    545594                        st.Joint_semantics.st_no_pc) (fun bl ->
    546595                      Obj.magic
    547                         (Joint_semantics.fetch_internal_function
    548                           (let p0 = Joint_semantics.spp'__o__spp p.sparams in
    549                           let globals0 = p.globals in
    550                           let g = p.ev_genv in g.Joint_semantics.ge) bl))) with
     596                        (Joint_semantics.fetch_internal_function pars.globals
     597                          pars.ev_genv bl))) with
    551598            | Errors.OK i_f -> i_f.Types.fst
    552599            | Errors.Error x0 -> dummy)
     
    558605
    559606(** val joint_tailcall_ident :
    560     evaluation_params -> Joint_semantics.state_pc -> AST.ident **)
    561 let joint_tailcall_ident p st =
     607    Joint_semantics.sem_params -> evaluation_params ->
     608    Joint_semantics.state_pc -> AST.ident **)
     609let joint_tailcall_ident p pars st =
    562610  let dummy = Positive.One in
    563   (match Joint_semantics.fetch_statement p.sparams p.globals
    564            (let p0 = Joint_semantics.spp'__o__spp p.sparams in
    565            let globals0 = p.globals in
    566            let g = p.ev_genv in g.Joint_semantics.ge) st.Joint_semantics.pc with
     611  (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
     612           st.Joint_semantics.pc with
    567613   | Errors.OK x ->
    568614     (match x.Types.snd with
     
    575621           (match Obj.magic
    576622                    (Monad.m_bind0 (Monad.max_def Errors.res0)
    577                       (Joint_semantics.block_of_call p.sparams p.globals
    578                         (let p0 = Joint_semantics.spp'__o__spp p.sparams in
    579                         let globals0 = p.globals in
    580                         let g = p.ev_genv in g.Joint_semantics.ge) f'
     623                      (Joint_semantics.block_of_call p pars.globals
     624                        (let p0 = Joint_semantics.spp'__o__spp p in
     625                        let globals0 = pars.globals in
     626                        let g = pars.ev_genv in g.Joint_semantics.ge) f'
    581627                        st.Joint_semantics.st_no_pc) (fun bl ->
    582628                      Obj.magic
    583                         (Joint_semantics.fetch_internal_function
    584                           (let p0 = Joint_semantics.spp'__o__spp p.sparams in
    585                           let globals0 = p.globals in
    586                           let g = p.ev_genv in g.Joint_semantics.ge) bl))) with
     629                        (Joint_semantics.fetch_internal_function pars.globals
     630                          pars.ev_genv bl))) with
    587631            | Errors.OK i_f -> i_f.Types.fst
    588632            | Errors.Error x0 -> dummy))
     
    595639
    596640(** val cost_label_of_stmt :
    597     evaluation_params -> Joint.joint_statement -> CostLabel.costlabel
    598     Types.option **)
    599 let cost_label_of_stmt p = function
     641    Joint_semantics.sem_params -> evaluation_params -> Joint.joint_statement
     642    -> CostLabel.costlabel Types.option **)
     643let cost_label_of_stmt p pars = function
    600644| Joint.Sequential (s0, x) ->
    601645  (match s0 with
     
    608652
    609653(** val joint_label_of_pc :
    610     evaluation_params -> ByteValues.program_counter -> CostLabel.costlabel
    611     Types.option **)
    612 let joint_label_of_pc p pc =
    613   match Joint_semantics.fetch_statement p.sparams p.globals
    614           (let p0 = Joint_semantics.spp'__o__spp p.sparams in
    615           let globals0 = p.globals in
    616           let g = p.ev_genv in g.Joint_semantics.ge) pc with
    617   | Errors.OK fn_stmt -> cost_label_of_stmt p fn_stmt.Types.snd
     654    Joint_semantics.sem_params -> evaluation_params ->
     655    ByteValues.program_counter -> CostLabel.costlabel Types.option **)
     656let joint_label_of_pc p pars pc =
     657  match Joint_semantics.fetch_statement p pars.globals pars.ev_genv pc with
     658  | Errors.OK fn_stmt -> cost_label_of_stmt p pars fn_stmt.Types.snd
    618659  | Errors.Error x -> Types.None
    619660
     
    624665
    625666(** val joint_final :
    626     Joint_semantics.sem_params -> AST.ident List.list -> Joint_semantics.genv
    627     -> Joint_semantics.state_pc -> Integers.int Types.option **)
    628 let joint_final p globals0 ge st =
    629   match ByteValues.eq_program_counter st.Joint_semantics.pc exit_pc' with
    630   | Bool.True ->
    631     let ret =
    632       (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main
    633     in
    634     Errors.res_to_opt
    635       (Obj.magic
    636         (Monad.m_bind0 (Monad.max_def Errors.res0)
    637           (Obj.magic
    638             (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result
    639               globals0
    640               (let p0 = Joint_semantics.spp'__o__spp p in
    641               let globals1 = globals0 in let g = ge in g.Joint_semantics.ge)
    642               ret st.Joint_semantics.st_no_pc)) (fun vals ->
    643           Obj.magic (ByteValues.word_of_list_beval vals))))
    644   | Bool.False -> Types.None
     667    Joint_semantics.sem_params -> evaluation_params ->
     668    Joint_semantics.state_pc -> Integers.int Types.option **)
     669let joint_final p pars st =
     670  let ge = pars.ev_genv in
     671  (match ByteValues.eq_program_counter st.Joint_semantics.pc exit_pc' with
     672   | Bool.True ->
     673     let ret =
     674       (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main
     675     in
     676     Errors.res_to_opt
     677       (Obj.magic
     678         (Monad.m_bind0 (Monad.max_def Errors.res0)
     679           (Obj.magic
     680             (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result
     681               pars.globals
     682               (let p0 = Joint_semantics.spp'__o__spp p in
     683               let globals0 = pars.globals in
     684               let g = ge in g.Joint_semantics.ge) ret
     685               st.Joint_semantics.st_no_pc)) (fun vals ->
     686           Obj.magic (ByteValues.word_of_list_beval vals))))
     687   | Bool.False -> Types.None)
    645688
    646689(** val joint_abstract_status :
     
    649692  { StructuredTraces.as_pc = pcDeq; StructuredTraces.as_pc_of =
    650693    (Obj.magic
    651       (Joint_semantics.pc
    652         (prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars
    653           p))); StructuredTraces.as_classify =
    654     (Obj.magic (joint_classify (make_global p)));
     694      (Joint_semantics.pc (prog_spars__o__spp'__o__msu_pars__o__st_pars p)));
     695    StructuredTraces.as_classify =
     696    (Obj.magic (joint_classify p.prog_spars (joint_make_global p)));
    655697    StructuredTraces.as_label_of_pc =
    656     (Obj.magic (joint_label_of_pc (make_global p)));
     698    (Obj.magic (joint_label_of_pc p.prog_spars (joint_make_global p)));
    657699    StructuredTraces.as_result =
    658     (Obj.magic
    659       (joint_final (prog_params_to_ev_params__o__sparams p)
    660         (make_global p).globals (make_global p).ev_genv));
     700    (Obj.magic (joint_final p.prog_spars (joint_make_global p)));
    661701    StructuredTraces.as_call_ident = (fun st ->
    662     joint_call_ident (make_global p) (Types.pi1 (Obj.magic st)));
    663     StructuredTraces.as_tailcall_ident = (fun st ->
    664     joint_tailcall_ident (make_global p) (Types.pi1 (Obj.magic st))) }
     702    joint_call_ident p.prog_spars (joint_make_global p)
     703      (Types.pi1 (Obj.magic st))); StructuredTraces.as_tailcall_ident =
     704    (fun st ->
     705    joint_tailcall_ident p.prog_spars (joint_make_global p)
     706      (Types.pi1 (Obj.magic st))) }
    665707
    666708(** val joint_status :
Note: See TracChangeset for help on using the changeset viewer.