Changeset 2960


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

New extraction, it diverges in RTL execution now.

Files:
2 deleted
30 edited

Legend:

Unmodified
Added
Removed
  • driver/cerco.ml

    r2934 r2960  
    5757  | Error m -> failwith (Error.errormsg m)
    5858in
     59prerr_endline "GOO1";
    5960let labelled = output.Extracted.Compiler.c_labelled_clight in
    6061let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
  • driver/error.ml

    r2826 r2960  
    7878| FramesEmptyOnPop -> "FramesEmptyOnPop"
    7979| RepeatedCostLabel0 -> "RepeatedCostLabel0"
     80| StackOverflow -> "StackOverflow"
    8081
    8182
  • extracted/compiler.ml

    r2951 r2960  
    496496(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
    497497let compute_fixpoint = Compute_fixpoints.compute_fixpoint
    498 
     498 
    499499(** val colour_graph : Interference.coloured_graph_computer **)
    500500let colour_graph = Compute_colouring.colour_graph
     
    531531  let i2 = Obj.magic observe Ertlptr_pass { Types.fst = p2; Types.snd = st1 }
    532532  in
    533   let { Types.fst = eta24710; Types.snd = max_stack } =
     533  let { Types.fst = eta665; Types.snd = max_stack } =
    534534    ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2
    535535  in
    536   let { Types.fst = p3; Types.snd = stack_cost } = eta24710 in
     536  let { Types.fst = p3; Types.snd = stack_cost } = eta665 in
    537537  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p3 in
    538538  let i3 = Obj.magic observe Ltl_pass { Types.fst = p3; Types.snd = st2 } in
     
    615615    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    616616    compiler_output -> 'a1 **)
    617 let rec compiler_output_rect_Type4 h_mk_compiler_output x_4341 =
     617let rec compiler_output_rect_Type4 h_mk_compiler_output x_589 =
    618618  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    619619    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    620     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4341
     620    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_589
    621621  in
    622622  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    627627    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    628628    compiler_output -> 'a1 **)
    629 let rec compiler_output_rect_Type5 h_mk_compiler_output x_4343 =
     629let rec compiler_output_rect_Type5 h_mk_compiler_output x_591 =
    630630  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    631631    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    632     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4343
     632    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_591
    633633  in
    634634  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    639639    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    640640    compiler_output -> 'a1 **)
    641 let rec compiler_output_rect_Type3 h_mk_compiler_output x_4345 =
     641let rec compiler_output_rect_Type3 h_mk_compiler_output x_593 =
    642642  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    643643    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    644     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4345
     644    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_593
    645645  in
    646646  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    651651    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    652652    compiler_output -> 'a1 **)
    653 let rec compiler_output_rect_Type2 h_mk_compiler_output x_4347 =
     653let rec compiler_output_rect_Type2 h_mk_compiler_output x_595 =
    654654  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    655655    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    656     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4347
     656    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_595
    657657  in
    658658  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    663663    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    664664    compiler_output -> 'a1 **)
    665 let rec compiler_output_rect_Type1 h_mk_compiler_output x_4349 =
     665let rec compiler_output_rect_Type1 h_mk_compiler_output x_597 =
    666666  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    667667    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    668     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4349
     668    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_597
    669669  in
    670670  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
     
    675675    Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    676676    compiler_output -> 'a1 **)
    677 let rec compiler_output_rect_Type0 h_mk_compiler_output x_4351 =
     677let rec compiler_output_rect_Type0 h_mk_compiler_output x_599 =
    678678  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    679679    c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    680     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_4351
     680    c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_599
    681681  in
    682682  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
  • extracted/eRTL.ml

    r2951 r2960  
    126126    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    127127let rec move_dst_rect_Type4 h_PSD h_HDW = function
    128 | PSD x_18520 -> h_PSD x_18520
    129 | HDW x_18521 -> h_HDW x_18521
     128| PSD x_7 -> h_PSD x_7
     129| HDW x_8 -> h_HDW x_8
    130130
    131131(** val move_dst_rect_Type5 :
    132132    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    133133let rec move_dst_rect_Type5 h_PSD h_HDW = function
    134 | PSD x_18525 -> h_PSD x_18525
    135 | HDW x_18526 -> h_HDW x_18526
     134| PSD x_12 -> h_PSD x_12
     135| HDW x_13 -> h_HDW x_13
    136136
    137137(** val move_dst_rect_Type3 :
    138138    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    139139let rec move_dst_rect_Type3 h_PSD h_HDW = function
    140 | PSD x_18530 -> h_PSD x_18530
    141 | HDW x_18531 -> h_HDW x_18531
     140| PSD x_17 -> h_PSD x_17
     141| HDW x_18 -> h_HDW x_18
    142142
    143143(** val move_dst_rect_Type2 :
    144144    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    145145let rec move_dst_rect_Type2 h_PSD h_HDW = function
    146 | PSD x_18535 -> h_PSD x_18535
    147 | HDW x_18536 -> h_HDW x_18536
     146| PSD x_22 -> h_PSD x_22
     147| HDW x_23 -> h_HDW x_23
    148148
    149149(** val move_dst_rect_Type1 :
    150150    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    151151let rec move_dst_rect_Type1 h_PSD h_HDW = function
    152 | PSD x_18540 -> h_PSD x_18540
    153 | HDW x_18541 -> h_HDW x_18541
     152| PSD x_27 -> h_PSD x_27
     153| HDW x_28 -> h_HDW x_28
    154154
    155155(** val move_dst_rect_Type0 :
    156156    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    157157let rec move_dst_rect_Type0 h_PSD h_HDW = function
    158 | PSD x_18545 -> h_PSD x_18545
    159 | HDW x_18546 -> h_HDW x_18546
     158| PSD x_32 -> h_PSD x_32
     159| HDW x_33 -> h_HDW x_33
    160160
    161161(** val move_dst_inv_rect_Type4 :
     
    352352| Ertl_new_frame -> h_ertl_new_frame
    353353| Ertl_del_frame -> h_ertl_del_frame
    354 | Ertl_frame_size x_18585 -> h_ertl_frame_size x_18585
     354| Ertl_frame_size x_72 -> h_ertl_frame_size x_72
    355355
    356356(** val ertl_seq_rect_Type5 :
     
    359359| Ertl_new_frame -> h_ertl_new_frame
    360360| Ertl_del_frame -> h_ertl_del_frame
    361 | Ertl_frame_size x_18590 -> h_ertl_frame_size x_18590
     361| Ertl_frame_size x_77 -> h_ertl_frame_size x_77
    362362
    363363(** val ertl_seq_rect_Type3 :
     
    366366| Ertl_new_frame -> h_ertl_new_frame
    367367| Ertl_del_frame -> h_ertl_del_frame
    368 | Ertl_frame_size x_18595 -> h_ertl_frame_size x_18595
     368| Ertl_frame_size x_82 -> h_ertl_frame_size x_82
    369369
    370370(** val ertl_seq_rect_Type2 :
     
    373373| Ertl_new_frame -> h_ertl_new_frame
    374374| Ertl_del_frame -> h_ertl_del_frame
    375 | Ertl_frame_size x_18600 -> h_ertl_frame_size x_18600
     375| Ertl_frame_size x_87 -> h_ertl_frame_size x_87
    376376
    377377(** val ertl_seq_rect_Type1 :
     
    380380| Ertl_new_frame -> h_ertl_new_frame
    381381| Ertl_del_frame -> h_ertl_del_frame
    382 | Ertl_frame_size x_18605 -> h_ertl_frame_size x_18605
     382| Ertl_frame_size x_92 -> h_ertl_frame_size x_92
    383383
    384384(** val ertl_seq_rect_Type0 :
     
    387387| Ertl_new_frame -> h_ertl_new_frame
    388388| Ertl_del_frame -> h_ertl_del_frame
    389 | Ertl_frame_size x_18610 -> h_ertl_frame_size x_18610
     389| Ertl_frame_size x_97 -> h_ertl_frame_size x_97
    390390
    391391(** val ertl_seq_inv_rect_Type4 :
     
    697697    Joint.add_graph eRTL (AST.prog_var_names p.Joint.joint_prog) l2
    698698      (Joint.Sequential ((Joint.CALL ((Types.Inl
    699       p.Joint.joint_prog.AST.prog_main),
    700       (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
     699      p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
    701700      (Obj.magic Types.It))), (Obj.magic l3))) res0
    702701  in
  • extracted/eRTLptr.ml

    r2951 r2960  
    130130    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    131131let rec ertlptr_seq_rect_Type4 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    132 | Ertlptr_ertl x_18654 -> h_ertlptr_ertl x_18654
    133 | LOW_ADDRESS (x_18656, x_18655) -> h_LOW_ADDRESS x_18656 x_18655
    134 | HIGH_ADDRESS (x_18658, x_18657) -> h_HIGH_ADDRESS x_18658 x_18657
     132| Ertlptr_ertl x_141 -> h_ertlptr_ertl x_141
     133| LOW_ADDRESS (x_143, x_142) -> h_LOW_ADDRESS x_143 x_142
     134| HIGH_ADDRESS (x_145, x_144) -> h_HIGH_ADDRESS x_145 x_144
    135135
    136136(** val ertlptr_seq_rect_Type5 :
     
    138138    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    139139let rec ertlptr_seq_rect_Type5 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    140 | Ertlptr_ertl x_18663 -> h_ertlptr_ertl x_18663
    141 | LOW_ADDRESS (x_18665, x_18664) -> h_LOW_ADDRESS x_18665 x_18664
    142 | HIGH_ADDRESS (x_18667, x_18666) -> h_HIGH_ADDRESS x_18667 x_18666
     140| Ertlptr_ertl x_150 -> h_ertlptr_ertl x_150
     141| LOW_ADDRESS (x_152, x_151) -> h_LOW_ADDRESS x_152 x_151
     142| HIGH_ADDRESS (x_154, x_153) -> h_HIGH_ADDRESS x_154 x_153
    143143
    144144(** val ertlptr_seq_rect_Type3 :
     
    146146    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    147147let rec ertlptr_seq_rect_Type3 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    148 | Ertlptr_ertl x_18672 -> h_ertlptr_ertl x_18672
    149 | LOW_ADDRESS (x_18674, x_18673) -> h_LOW_ADDRESS x_18674 x_18673
    150 | HIGH_ADDRESS (x_18676, x_18675) -> h_HIGH_ADDRESS x_18676 x_18675
     148| Ertlptr_ertl x_159 -> h_ertlptr_ertl x_159
     149| LOW_ADDRESS (x_161, x_160) -> h_LOW_ADDRESS x_161 x_160
     150| HIGH_ADDRESS (x_163, x_162) -> h_HIGH_ADDRESS x_163 x_162
    151151
    152152(** val ertlptr_seq_rect_Type2 :
     
    154154    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    155155let rec ertlptr_seq_rect_Type2 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    156 | Ertlptr_ertl x_18681 -> h_ertlptr_ertl x_18681
    157 | LOW_ADDRESS (x_18683, x_18682) -> h_LOW_ADDRESS x_18683 x_18682
    158 | HIGH_ADDRESS (x_18685, x_18684) -> h_HIGH_ADDRESS x_18685 x_18684
     156| Ertlptr_ertl x_168 -> h_ertlptr_ertl x_168
     157| LOW_ADDRESS (x_170, x_169) -> h_LOW_ADDRESS x_170 x_169
     158| HIGH_ADDRESS (x_172, x_171) -> h_HIGH_ADDRESS x_172 x_171
    159159
    160160(** val ertlptr_seq_rect_Type1 :
     
    162162    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    163163let rec ertlptr_seq_rect_Type1 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    164 | Ertlptr_ertl x_18690 -> h_ertlptr_ertl x_18690
    165 | LOW_ADDRESS (x_18692, x_18691) -> h_LOW_ADDRESS x_18692 x_18691
    166 | HIGH_ADDRESS (x_18694, x_18693) -> h_HIGH_ADDRESS x_18694 x_18693
     164| Ertlptr_ertl x_177 -> h_ertlptr_ertl x_177
     165| LOW_ADDRESS (x_179, x_178) -> h_LOW_ADDRESS x_179 x_178
     166| HIGH_ADDRESS (x_181, x_180) -> h_HIGH_ADDRESS x_181 x_180
    167167
    168168(** val ertlptr_seq_rect_Type0 :
     
    170170    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    171171let rec ertlptr_seq_rect_Type0 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    172 | Ertlptr_ertl x_18699 -> h_ertlptr_ertl x_18699
    173 | LOW_ADDRESS (x_18701, x_18700) -> h_LOW_ADDRESS x_18701 x_18700
    174 | HIGH_ADDRESS (x_18703, x_18702) -> h_HIGH_ADDRESS x_18703 x_18702
     172| Ertlptr_ertl x_186 -> h_ertlptr_ertl x_186
     173| LOW_ADDRESS (x_188, x_187) -> h_LOW_ADDRESS x_188 x_187
     174| HIGH_ADDRESS (x_190, x_189) -> h_HIGH_ADDRESS x_190 x_189
    175175
    176176(** val ertlptr_seq_inv_rect_Type4 :
     
    362362    Joint.add_graph eRTLptr (AST.prog_var_names p.Joint.joint_prog) l2
    363363      (Joint.Sequential ((Joint.CALL ((Types.Inl
    364       p.Joint.joint_prog.AST.prog_main),
    365       (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
     364      p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
    366365      (Obj.magic Types.It))), (Obj.magic l3))) res0
    367366  in
  • extracted/eRTLptrToLTL.ml

    r2951 r2960  
    181181    arg_decision -> 'a1 **)
    182182let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    183 | Arg_decision_colour x_19209 -> h_arg_decision_colour x_19209
    184 | Arg_decision_spill x_19210 -> h_arg_decision_spill x_19210
    185 | Arg_decision_imm x_19211 -> h_arg_decision_imm x_19211
     183| Arg_decision_colour x_380 -> h_arg_decision_colour x_380
     184| Arg_decision_spill x_381 -> h_arg_decision_spill x_381
     185| Arg_decision_imm x_382 -> h_arg_decision_imm x_382
    186186
    187187(** val arg_decision_rect_Type5 :
     
    189189    arg_decision -> 'a1 **)
    190190let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    191 | Arg_decision_colour x_19216 -> h_arg_decision_colour x_19216
    192 | Arg_decision_spill x_19217 -> h_arg_decision_spill x_19217
    193 | Arg_decision_imm x_19218 -> h_arg_decision_imm x_19218
     191| Arg_decision_colour x_387 -> h_arg_decision_colour x_387
     192| Arg_decision_spill x_388 -> h_arg_decision_spill x_388
     193| Arg_decision_imm x_389 -> h_arg_decision_imm x_389
    194194
    195195(** val arg_decision_rect_Type3 :
     
    197197    arg_decision -> 'a1 **)
    198198let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    199 | Arg_decision_colour x_19223 -> h_arg_decision_colour x_19223
    200 | Arg_decision_spill x_19224 -> h_arg_decision_spill x_19224
    201 | Arg_decision_imm x_19225 -> h_arg_decision_imm x_19225
     199| Arg_decision_colour x_394 -> h_arg_decision_colour x_394
     200| Arg_decision_spill x_395 -> h_arg_decision_spill x_395
     201| Arg_decision_imm x_396 -> h_arg_decision_imm x_396
    202202
    203203(** val arg_decision_rect_Type2 :
     
    205205    arg_decision -> 'a1 **)
    206206let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    207 | Arg_decision_colour x_19230 -> h_arg_decision_colour x_19230
    208 | Arg_decision_spill x_19231 -> h_arg_decision_spill x_19231
    209 | Arg_decision_imm x_19232 -> h_arg_decision_imm x_19232
     207| Arg_decision_colour x_401 -> h_arg_decision_colour x_401
     208| Arg_decision_spill x_402 -> h_arg_decision_spill x_402
     209| Arg_decision_imm x_403 -> h_arg_decision_imm x_403
    210210
    211211(** val arg_decision_rect_Type1 :
     
    213213    arg_decision -> 'a1 **)
    214214let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    215 | Arg_decision_colour x_19237 -> h_arg_decision_colour x_19237
    216 | Arg_decision_spill x_19238 -> h_arg_decision_spill x_19238
    217 | Arg_decision_imm x_19239 -> h_arg_decision_imm x_19239
     215| Arg_decision_colour x_408 -> h_arg_decision_colour x_408
     216| Arg_decision_spill x_409 -> h_arg_decision_spill x_409
     217| Arg_decision_imm x_410 -> h_arg_decision_imm x_410
    218218
    219219(** val arg_decision_rect_Type0 :
     
    221221    arg_decision -> 'a1 **)
    222222let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    223 | Arg_decision_colour x_19244 -> h_arg_decision_colour x_19244
    224 | Arg_decision_spill x_19245 -> h_arg_decision_spill x_19245
    225 | Arg_decision_imm x_19246 -> h_arg_decision_imm x_19246
     223| Arg_decision_colour x_415 -> h_arg_decision_colour x_415
     224| Arg_decision_spill x_416 -> h_arg_decision_spill x_416
     225| Arg_decision_imm x_417 -> h_arg_decision_imm x_417
    226226
    227227(** val arg_decision_inv_rect_Type4 :
  • extracted/eRTLptr_semantics.ml

    r2951 r2960  
    196196    Obj.magic
    197197      (Monad.m_bind0 (Monad.max_def Errors.res0)
    198         (Obj.magic (ge.Joint_semantics.get_pc_from_label id l))
     198        (Obj.magic (Joint_semantics.gen_pc_from_label globals ge id l))
    199199        (fun pc_lab ->
    200200        let { Types.fst = addrl; Types.snd = addrh } =
     
    205205    Obj.magic
    206206      (Monad.m_bind0 (Monad.max_def Errors.res0)
    207         (Obj.magic (ge.Joint_semantics.get_pc_from_label id l))
     207        (Obj.magic (Joint_semantics.gen_pc_from_label globals ge id l))
    208208        (fun pc_lab ->
    209209        let { Types.fst = addrl; Types.snd = addrh } =
  • extracted/errorMessages.ml

    r2827 r2960  
    8181| FrameErrorOnPop
    8282| FunctionNotFound
    83 
     83| StackOverflow
  • extracted/errorMessages.mli

    r2827 r2960  
    8181| FrameErrorOnPop
    8282| FunctionNotFound
     83| StackOverflow
    8384
  • extracted/interference.ml

    r2951 r2960  
    136136    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    137137let rec decision_rect_Type4 h_decision_spill h_decision_colour = function
    138 | Decision_spill x_19110 -> h_decision_spill x_19110
    139 | Decision_colour x_19111 -> h_decision_colour x_19111
     138| Decision_spill x_281 -> h_decision_spill x_281
     139| Decision_colour x_282 -> h_decision_colour x_282
    140140
    141141(** val decision_rect_Type5 :
    142142    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    143143let rec decision_rect_Type5 h_decision_spill h_decision_colour = function
    144 | Decision_spill x_19115 -> h_decision_spill x_19115
    145 | Decision_colour x_19116 -> h_decision_colour x_19116
     144| Decision_spill x_286 -> h_decision_spill x_286
     145| Decision_colour x_287 -> h_decision_colour x_287
    146146
    147147(** val decision_rect_Type3 :
    148148    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    149149let rec decision_rect_Type3 h_decision_spill h_decision_colour = function
    150 | Decision_spill x_19120 -> h_decision_spill x_19120
    151 | Decision_colour x_19121 -> h_decision_colour x_19121
     150| Decision_spill x_291 -> h_decision_spill x_291
     151| Decision_colour x_292 -> h_decision_colour x_292
    152152
    153153(** val decision_rect_Type2 :
    154154    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    155155let rec decision_rect_Type2 h_decision_spill h_decision_colour = function
    156 | Decision_spill x_19125 -> h_decision_spill x_19125
    157 | Decision_colour x_19126 -> h_decision_colour x_19126
     156| Decision_spill x_296 -> h_decision_spill x_296
     157| Decision_colour x_297 -> h_decision_colour x_297
    158158
    159159(** val decision_rect_Type1 :
    160160    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    161161let rec decision_rect_Type1 h_decision_spill h_decision_colour = function
    162 | Decision_spill x_19130 -> h_decision_spill x_19130
    163 | Decision_colour x_19131 -> h_decision_colour x_19131
     162| Decision_spill x_301 -> h_decision_spill x_301
     163| Decision_colour x_302 -> h_decision_colour x_302
    164164
    165165(** val decision_rect_Type0 :
    166166    (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
    167167let rec decision_rect_Type0 h_decision_spill h_decision_colour = function
    168 | Decision_spill x_19135 -> h_decision_spill x_19135
    169 | Decision_colour x_19136 -> h_decision_colour x_19136
     168| Decision_spill x_306 -> h_decision_spill x_306
     169| Decision_colour x_307 -> h_decision_colour x_307
    170170
    171171(** val decision_inv_rect_Type4 :
     
    219219    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    220220    __ -> 'a1) -> coloured_graph -> 'a1 **)
    221 let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_19171 =
    222   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19171 in
     221let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_342 =
     222  let { colouring = colouring0; spilled_no = spilled_no0 } = x_342 in
    223223  h_mk_coloured_graph colouring0 spilled_no0 __ __
    224224
     
    226226    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    227227    __ -> 'a1) -> coloured_graph -> 'a1 **)
    228 let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_19173 =
    229   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19173 in
     228let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_344 =
     229  let { colouring = colouring0; spilled_no = spilled_no0 } = x_344 in
    230230  h_mk_coloured_graph colouring0 spilled_no0 __ __
    231231
     
    233233    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    234234    __ -> 'a1) -> coloured_graph -> 'a1 **)
    235 let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_19175 =
    236   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19175 in
     235let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_346 =
     236  let { colouring = colouring0; spilled_no = spilled_no0 } = x_346 in
    237237  h_mk_coloured_graph colouring0 spilled_no0 __ __
    238238
     
    240240    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    241241    __ -> 'a1) -> coloured_graph -> 'a1 **)
    242 let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_19177 =
    243   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19177 in
     242let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_348 =
     243  let { colouring = colouring0; spilled_no = spilled_no0 } = x_348 in
    244244  h_mk_coloured_graph colouring0 spilled_no0 __ __
    245245
     
    247247    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    248248    __ -> 'a1) -> coloured_graph -> 'a1 **)
    249 let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_19179 =
    250   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19179 in
     249let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_350 =
     250  let { colouring = colouring0; spilled_no = spilled_no0 } = x_350 in
    251251  h_mk_coloured_graph colouring0 spilled_no0 __ __
    252252
     
    254254    Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
    255255    __ -> 'a1) -> coloured_graph -> 'a1 **)
    256 let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_19181 =
    257   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19181 in
     256let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_352 =
     257  let { colouring = colouring0; spilled_no = spilled_no0 } = x_352 in
    258258  h_mk_coloured_graph colouring0 spilled_no0 __ __
    259259
  • extracted/joint_LTL_LIN_semantics.ml

    r2951 r2960  
    244244    Obj.magic
    245245      (Monad.m_bind0 (Monad.max_def Errors.res0)
    246         (Obj.magic (ge.Joint_semantics.get_pc_from_label curr_id l))
     246        (Obj.magic (Joint_semantics.gen_pc_from_label globals ge curr_id l))
    247247        (fun pc_lab ->
    248248        let { Types.fst = addrl; Types.snd = addrh } =
     
    258258    Obj.magic
    259259      (Monad.m_bind0 (Monad.max_def Errors.res0)
    260         (Obj.magic (ge.Joint_semantics.get_pc_from_label curr_id l))
     260        (Obj.magic (Joint_semantics.gen_pc_from_label globals ge curr_id l))
    261261        (fun pc_lab ->
    262262        let { Types.fst = addrl; Types.snd = addrh } =
  • extracted/joint_fullexec.ml

    r2951 r2960  
    160160
    161161open Measurable
    162 
    163 type joint_global = { jglobals : AST.ident List.list;
    164                       jgenv : Joint_semantics.genv }
    165 
    166 (** val joint_global_rect_Type4 :
    167     Joint_semantics.sem_params -> (AST.ident List.list ->
    168     Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    169 let rec joint_global_rect_Type4 p h_mk_joint_global x_6006 =
    170   let { jglobals = jglobals0; jgenv = jgenv0 } = x_6006 in
    171   h_mk_joint_global jglobals0 jgenv0
    172 
    173 (** val joint_global_rect_Type5 :
    174     Joint_semantics.sem_params -> (AST.ident List.list ->
    175     Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    176 let rec joint_global_rect_Type5 p h_mk_joint_global x_6008 =
    177   let { jglobals = jglobals0; jgenv = jgenv0 } = x_6008 in
    178   h_mk_joint_global jglobals0 jgenv0
    179 
    180 (** val joint_global_rect_Type3 :
    181     Joint_semantics.sem_params -> (AST.ident List.list ->
    182     Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    183 let rec joint_global_rect_Type3 p h_mk_joint_global x_6010 =
    184   let { jglobals = jglobals0; jgenv = jgenv0 } = x_6010 in
    185   h_mk_joint_global jglobals0 jgenv0
    186 
    187 (** val joint_global_rect_Type2 :
    188     Joint_semantics.sem_params -> (AST.ident List.list ->
    189     Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    190 let rec joint_global_rect_Type2 p h_mk_joint_global x_6012 =
    191   let { jglobals = jglobals0; jgenv = jgenv0 } = x_6012 in
    192   h_mk_joint_global jglobals0 jgenv0
    193 
    194 (** val joint_global_rect_Type1 :
    195     Joint_semantics.sem_params -> (AST.ident List.list ->
    196     Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    197 let rec joint_global_rect_Type1 p h_mk_joint_global x_6014 =
    198   let { jglobals = jglobals0; jgenv = jgenv0 } = x_6014 in
    199   h_mk_joint_global jglobals0 jgenv0
    200 
    201 (** val joint_global_rect_Type0 :
    202     Joint_semantics.sem_params -> (AST.ident List.list ->
    203     Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    204 let rec joint_global_rect_Type0 p h_mk_joint_global x_6016 =
    205   let { jglobals = jglobals0; jgenv = jgenv0 } = x_6016 in
    206   h_mk_joint_global jglobals0 jgenv0
    207 
    208 (** val jglobals :
    209     Joint_semantics.sem_params -> joint_global -> AST.ident List.list **)
    210 let rec jglobals p xxx =
    211   xxx.jglobals
    212 
    213 (** val jgenv :
    214     Joint_semantics.sem_params -> joint_global -> Joint_semantics.genv **)
    215 let rec jgenv p xxx =
    216   xxx.jgenv
    217 
    218 (** val joint_global_inv_rect_Type4 :
    219     Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    220     Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    221 let joint_global_inv_rect_Type4 x1 hterm h1 =
    222   let hcut = joint_global_rect_Type4 x1 h1 hterm in hcut __
    223 
    224 (** val joint_global_inv_rect_Type3 :
    225     Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    226     Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    227 let joint_global_inv_rect_Type3 x1 hterm h1 =
    228   let hcut = joint_global_rect_Type3 x1 h1 hterm in hcut __
    229 
    230 (** val joint_global_inv_rect_Type2 :
    231     Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    232     Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    233 let joint_global_inv_rect_Type2 x1 hterm h1 =
    234   let hcut = joint_global_rect_Type2 x1 h1 hterm in hcut __
    235 
    236 (** val joint_global_inv_rect_Type1 :
    237     Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    238     Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    239 let joint_global_inv_rect_Type1 x1 hterm h1 =
    240   let hcut = joint_global_rect_Type1 x1 h1 hterm in hcut __
    241 
    242 (** val joint_global_inv_rect_Type0 :
    243     Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    244     Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
    245 let joint_global_inv_rect_Type0 x1 hterm h1 =
    246   let hcut = joint_global_rect_Type0 x1 h1 hterm in hcut __
    247 
    248 (** val joint_global_discr :
    249     Joint_semantics.sem_params -> joint_global -> joint_global -> __ **)
    250 let joint_global_discr a1 x y =
    251   Logic.eq_rect_Type2 x
    252     (let { jglobals = a0; jgenv = a10 } = x in
    253     Obj.magic (fun _ dH -> dH __ __)) y
    254 
    255 (** val joint_global_jmdiscr :
    256     Joint_semantics.sem_params -> joint_global -> joint_global -> __ **)
    257 let joint_global_jmdiscr a1 x y =
    258   Logic.eq_rect_Type2 x
    259     (let { jglobals = a0; jgenv = a10 } = x in
    260     Obj.magic (fun _ dH -> dH __ __)) y
    261 
    262 (** val dpi1__o__jgenv__o__inject :
    263     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    264     Joint_semantics.genv Types.sig0 **)
    265 let dpi1__o__jgenv__o__inject x0 x2 =
    266   x2.Types.dpi1.jgenv
    267 
    268 (** val dpi1__o__jgenv__o__genv_to_genv_t__o__inject :
    269     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    270     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    271     Types.sig0 **)
    272 let dpi1__o__jgenv__o__genv_to_genv_t__o__inject x0 x2 =
    273   Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
    274     x2.Types.dpi1.jglobals x2.Types.dpi1.jgenv
    275 
    276 (** val dpi1__o__jgenv__o__genv_to_genv_t :
    277     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    278     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
    279 let dpi1__o__jgenv__o__genv_to_genv_t x0 x2 =
    280   let p = Joint_semantics.spp'__o__spp x0 in
    281   let globals = x2.Types.dpi1.jglobals in
    282   let g = x2.Types.dpi1.jgenv in g.Joint_semantics.ge
    283 
    284 (** val eject__o__jgenv__o__inject :
    285     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    286     Joint_semantics.genv Types.sig0 **)
    287 let eject__o__jgenv__o__inject x0 x2 =
    288   (Types.pi1 x2).jgenv
    289 
    290 (** val eject__o__jgenv__o__genv_to_genv_t__o__inject :
    291     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    292     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    293     Types.sig0 **)
    294 let eject__o__jgenv__o__genv_to_genv_t__o__inject x0 x2 =
    295   Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
    296     (Types.pi1 x2).jglobals (Types.pi1 x2).jgenv
    297 
    298 (** val eject__o__jgenv__o__genv_to_genv_t :
    299     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    300     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
    301 let eject__o__jgenv__o__genv_to_genv_t x0 x2 =
    302   let p = Joint_semantics.spp'__o__spp x0 in
    303   let globals = (Types.pi1 x2).jglobals in
    304   let g = (Types.pi1 x2).jgenv in g.Joint_semantics.ge
    305 
    306 (** val jgenv__o__genv_to_genv_t :
    307     Joint_semantics.sem_params -> joint_global ->
    308     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
    309 let jgenv__o__genv_to_genv_t x0 x1 =
    310   let p = Joint_semantics.spp'__o__spp x0 in
    311   let globals = x1.jglobals in let g = x1.jgenv in g.Joint_semantics.ge
    312 
    313 (** val jgenv__o__genv_to_genv_t__o__inject :
    314     Joint_semantics.sem_params -> joint_global ->
    315     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    316     Types.sig0 **)
    317 let jgenv__o__genv_to_genv_t__o__inject x0 x1 =
    318   Joint_semantics.genv_to_genv_t__o__inject (Joint_semantics.spp'__o__spp x0)
    319     x1.jglobals x1.jgenv
    320 
    321 (** val jgenv__o__inject :
    322     Joint_semantics.sem_params -> joint_global -> Joint_semantics.genv
    323     Types.sig0 **)
    324 let jgenv__o__inject x0 x1 =
    325   x1.jgenv
    326 
    327 (** val dpi1__o__jgenv :
    328     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    329     Joint_semantics.genv **)
    330 let dpi1__o__jgenv x0 x2 =
    331   x2.Types.dpi1.jgenv
    332 
    333 (** val eject__o__jgenv :
    334     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    335     Joint_semantics.genv **)
    336 let eject__o__jgenv x0 x2 =
    337   (Types.pi1 x2).jgenv
    338 
    339 (** val eval_params_of_global :
    340     Joint_semantics.sem_params -> joint_global -> Traces.evaluation_params **)
    341 let eval_params_of_global p gl =
    342   { Traces.globals = gl.jglobals; Traces.sparams = p; Traces.ev_genv =
    343     gl.jgenv }
    344 
    345 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    346     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    347     Joint.unserialized_params **)
    348 let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 x2 =
    349   Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
    350     (eval_params_of_global x0 x2.Types.dpi1)
    351 
    352 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    353     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    354     Joint.uns_params **)
    355 let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 x2 =
    356   Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars
    357     (eval_params_of_global x0 x2.Types.dpi1)
    358 
    359 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
    360     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    361     Joint.stmt_params **)
    362 let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars x0 x2 =
    363   Traces.sparams__o__spp'__o__spp__o__stmt_pars
    364     (eval_params_of_global x0 x2.Types.dpi1)
    365 
    366 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp :
    367     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    368     Joint.params **)
    369 let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp x0 x2 =
    370   Traces.sparams__o__spp'__o__spp (eval_params_of_global x0 x2.Types.dpi1)
    371 
    372 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
    373     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    374     Joint_semantics.sem_state_params **)
    375 let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars x0 x2 =
    376   Traces.sparams__o__spp'__o__msu_pars__o__st_pars
    377     (eval_params_of_global x0 x2.Types.dpi1)
    378 
    379 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
    380     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    381     Joint.joint_closed_internal_function
    382     Joint_semantics.sem_unserialized_params **)
    383 let dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars x0 x2 =
    384   Traces.sparams__o__spp'__o__msu_pars
    385     (eval_params_of_global x0 x2.Types.dpi1)
    386 
    387 (** val dpi1__o__eval_params_of_global__o__sparams__o__spp' :
    388     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    389     Joint_semantics.serialized_params **)
    390 let dpi1__o__eval_params_of_global__o__sparams__o__spp' x0 x2 =
    391   Traces.sparams__o__spp' (eval_params_of_global x0 x2.Types.dpi1)
    392 
    393 (** val dpi1__o__eval_params_of_global__o__sparams :
    394     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    395     Joint_semantics.sem_params **)
    396 let dpi1__o__eval_params_of_global__o__sparams x0 x2 =
    397   (eval_params_of_global x0 x2.Types.dpi1).Traces.sparams
    398 
    399 (** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    400     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    401     Joint.unserialized_params **)
    402 let eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 x2 =
    403   Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
    404     (eval_params_of_global x0 (Types.pi1 x2))
    405 
    406 (** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    407     Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.uns_params **)
    408 let eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 x2 =
    409   Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars
    410     (eval_params_of_global x0 (Types.pi1 x2))
    411 
    412 (** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
    413     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    414     Joint.stmt_params **)
    415 let eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars x0 x2 =
    416   Traces.sparams__o__spp'__o__spp__o__stmt_pars
    417     (eval_params_of_global x0 (Types.pi1 x2))
    418 
    419 (** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp :
    420     Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.params **)
    421 let eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp x0 x2 =
    422   Traces.sparams__o__spp'__o__spp (eval_params_of_global x0 (Types.pi1 x2))
    423 
    424 (** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
    425     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    426     Joint_semantics.sem_state_params **)
    427 let eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars x0 x2 =
    428   Traces.sparams__o__spp'__o__msu_pars__o__st_pars
    429     (eval_params_of_global x0 (Types.pi1 x2))
    430 
    431 (** val eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
    432     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    433     Joint.joint_closed_internal_function
    434     Joint_semantics.sem_unserialized_params **)
    435 let eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars x0 x2 =
    436   Traces.sparams__o__spp'__o__msu_pars
    437     (eval_params_of_global x0 (Types.pi1 x2))
    438 
    439 (** val eject__o__eval_params_of_global__o__sparams__o__spp' :
    440     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    441     Joint_semantics.serialized_params **)
    442 let eject__o__eval_params_of_global__o__sparams__o__spp' x0 x2 =
    443   Traces.sparams__o__spp' (eval_params_of_global x0 (Types.pi1 x2))
    444 
    445 (** val eject__o__eval_params_of_global__o__sparams :
    446     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    447     Joint_semantics.sem_params **)
    448 let eject__o__eval_params_of_global__o__sparams x0 x2 =
    449   (eval_params_of_global x0 (Types.pi1 x2)).Traces.sparams
    450 
    451 (** val eval_params_of_global__o__sparams :
    452     Joint_semantics.sem_params -> joint_global -> Joint_semantics.sem_params **)
    453 let eval_params_of_global__o__sparams x0 x1 =
    454   (eval_params_of_global x0 x1).Traces.sparams
    455 
    456 (** val eval_params_of_global__o__sparams__o__spp' :
    457     Joint_semantics.sem_params -> joint_global ->
    458     Joint_semantics.serialized_params **)
    459 let eval_params_of_global__o__sparams__o__spp' x0 x1 =
    460   Traces.sparams__o__spp' (eval_params_of_global x0 x1)
    461 
    462 (** val eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
    463     Joint_semantics.sem_params -> joint_global ->
    464     Joint.joint_closed_internal_function
    465     Joint_semantics.sem_unserialized_params **)
    466 let eval_params_of_global__o__sparams__o__spp'__o__msu_pars x0 x1 =
    467   Traces.sparams__o__spp'__o__msu_pars (eval_params_of_global x0 x1)
    468 
    469 (** val eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
    470     Joint_semantics.sem_params -> joint_global ->
    471     Joint_semantics.sem_state_params **)
    472 let eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars x0 x1 =
    473   Traces.sparams__o__spp'__o__msu_pars__o__st_pars
    474     (eval_params_of_global x0 x1)
    475 
    476 (** val eval_params_of_global__o__sparams__o__spp'__o__spp :
    477     Joint_semantics.sem_params -> joint_global -> Joint.params **)
    478 let eval_params_of_global__o__sparams__o__spp'__o__spp x0 x1 =
    479   Traces.sparams__o__spp'__o__spp (eval_params_of_global x0 x1)
    480 
    481 (** val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
    482     Joint_semantics.sem_params -> joint_global -> Joint.stmt_params **)
    483 let eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars x0 x1 =
    484   Traces.sparams__o__spp'__o__spp__o__stmt_pars (eval_params_of_global x0 x1)
    485 
    486 (** val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    487     Joint_semantics.sem_params -> joint_global -> Joint.uns_params **)
    488 let eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 x1 =
    489   Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars
    490     (eval_params_of_global x0 x1)
    491 
    492 (** val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    493     Joint_semantics.sem_params -> joint_global -> Joint.unserialized_params **)
    494 let eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 x1 =
    495   Traces.sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
    496     (eval_params_of_global x0 x1)
    497 
    498 (** val dpi1__o__eval_params_of_global :
    499     Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    500     Traces.evaluation_params **)
    501 let dpi1__o__eval_params_of_global x0 x2 =
    502   eval_params_of_global x0 x2.Types.dpi1
    503 
    504 (** val eject__o__eval_params_of_global :
    505     Joint_semantics.sem_params -> joint_global Types.sig0 ->
    506     Traces.evaluation_params **)
    507 let eject__o__eval_params_of_global x0 x2 =
    508   eval_params_of_global x0 (Types.pi1 x2)
    509 
    510 (** val make_joint_global :
    511     Joint_semantics.sem_params -> (Joint.joint_program, AST.ident -> Nat.nat
    512     Types.option) Types.prod -> joint_global **)
    513 let make_joint_global pars p_stack =
    514   let p = p_stack.Types.fst in
    515   let stack_sizes = p_stack.Types.snd in
    516   let ev_pars =
    517     Traces.make_global { Traces.prog_spars = pars; Traces.prog = p;
    518       Traces.stack_sizes = stack_sizes }
    519   in
    520   { jglobals = ev_pars.Traces.globals; jgenv = ev_pars.Traces.ev_genv }
    521162
    522163(** val joint_exec :
     
    525166let joint_exec g =
    526167  { SmallstepExec.is_final = (fun env ->
    527     Obj.magic
    528       (Traces.joint_final g (Obj.magic env).jglobals (Obj.magic env).jgenv));
    529     SmallstepExec.step = (fun env st ->
     168    Obj.magic (Traces.joint_final g (Obj.magic env))); SmallstepExec.step =
     169    (fun env st ->
    530170    Obj.magic
    531171      (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    532172        (Obj.magic
    533           (Joint_semantics.eval_state g (Obj.magic env).jglobals
    534             (Obj.magic env).jgenv (Obj.magic st))) (fun st' ->
     173          (Joint_semantics.eval_state g (Obj.magic env).Traces.globals
     174            (Obj.magic env).Traces.ev_genv (Obj.magic st))) (fun st' ->
    535175        let charge =
    536           match Traces.joint_label_of_pc
    537                   (eval_params_of_global g (Obj.magic env))
     176          match Traces.joint_label_of_pc g (Obj.magic env)
    538177                  (Obj.magic st).Joint_semantics.pc with
    539178          | Types.None -> Events.e0
     
    548187let joint_fullexec g =
    549188  { SmallstepExec.es1 = (joint_exec g); SmallstepExec.make_global =
    550     (Obj.magic (make_joint_global g)); SmallstepExec.make_initial_state =
     189    (fun pr ->
     190    Obj.magic
     191      (Traces.joint_make_global { Traces.prog_spars = g; Traces.prog =
     192        (Obj.magic pr).Types.fst; Traces.stack_sizes =
     193        (Obj.magic pr).Types.snd })); SmallstepExec.make_initial_state =
    551194    (fun p_stacks ->
    552195    Obj.magic
     
    563206    Bool.notb
    564207      (PositiveMap.is_none
    565         (Traces.joint_label_of_pc (eval_params_of_global g (Obj.magic env))
     208        (Traces.joint_label_of_pc g (Obj.magic env)
    566209          (Obj.magic st).Joint_semantics.pc))); Measurable.pcs_classify =
    567     (fun env ->
    568     Obj.magic
    569       (Traces.joint_classify (eval_params_of_global g (Obj.magic env))));
     210    (fun env -> Obj.magic (Traces.joint_classify g (Obj.magic env)));
    570211    Measurable.pcs_callee = (fun env s _ ->
    571     Traces.joint_call_ident (eval_params_of_global g (Obj.magic env))
    572       (Obj.magic s)) }
    573 
     212    Traces.joint_call_ident g (Obj.magic env) (Obj.magic s)) }
     213
  • extracted/joint_fullexec.mli

    r2951 r2960  
    161161open Measurable
    162162
    163 type joint_global = { jglobals : AST.ident List.list;
    164                       jgenv : Joint_semantics.genv }
    165 
    166 val joint_global_rect_Type4 :
    167   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    168   -> 'a1) -> joint_global -> 'a1
    169 
    170 val joint_global_rect_Type5 :
    171   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    172   -> 'a1) -> joint_global -> 'a1
    173 
    174 val joint_global_rect_Type3 :
    175   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    176   -> 'a1) -> joint_global -> 'a1
    177 
    178 val joint_global_rect_Type2 :
    179   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    180   -> 'a1) -> joint_global -> 'a1
    181 
    182 val joint_global_rect_Type1 :
    183   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    184   -> 'a1) -> joint_global -> 'a1
    185 
    186 val joint_global_rect_Type0 :
    187   Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    188   -> 'a1) -> joint_global -> 'a1
    189 
    190 val jglobals :
    191   Joint_semantics.sem_params -> joint_global -> AST.ident List.list
    192 
    193 val jgenv :
    194   Joint_semantics.sem_params -> joint_global -> Joint_semantics.genv
    195 
    196 val joint_global_inv_rect_Type4 :
    197   Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    198   Joint_semantics.genv -> __ -> 'a1) -> 'a1
    199 
    200 val joint_global_inv_rect_Type3 :
    201   Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    202   Joint_semantics.genv -> __ -> 'a1) -> 'a1
    203 
    204 val joint_global_inv_rect_Type2 :
    205   Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    206   Joint_semantics.genv -> __ -> 'a1) -> 'a1
    207 
    208 val joint_global_inv_rect_Type1 :
    209   Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    210   Joint_semantics.genv -> __ -> 'a1) -> 'a1
    211 
    212 val joint_global_inv_rect_Type0 :
    213   Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
    214   Joint_semantics.genv -> __ -> 'a1) -> 'a1
    215 
    216 val joint_global_discr :
    217   Joint_semantics.sem_params -> joint_global -> joint_global -> __
    218 
    219 val joint_global_jmdiscr :
    220   Joint_semantics.sem_params -> joint_global -> joint_global -> __
    221 
    222 val dpi1__o__jgenv__o__inject :
    223   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    224   Joint_semantics.genv Types.sig0
    225 
    226 val dpi1__o__jgenv__o__genv_to_genv_t__o__inject :
    227   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    228   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    229   Types.sig0
    230 
    231 val dpi1__o__jgenv__o__genv_to_genv_t :
    232   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    233   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    234 
    235 val eject__o__jgenv__o__inject :
    236   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    237   Joint_semantics.genv Types.sig0
    238 
    239 val eject__o__jgenv__o__genv_to_genv_t__o__inject :
    240   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    241   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    242   Types.sig0
    243 
    244 val eject__o__jgenv__o__genv_to_genv_t :
    245   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    246   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    247 
    248 val jgenv__o__genv_to_genv_t :
    249   Joint_semantics.sem_params -> joint_global ->
    250   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    251 
    252 val jgenv__o__genv_to_genv_t__o__inject :
    253   Joint_semantics.sem_params -> joint_global ->
    254   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    255   Types.sig0
    256 
    257 val jgenv__o__inject :
    258   Joint_semantics.sem_params -> joint_global -> Joint_semantics.genv
    259   Types.sig0
    260 
    261 val dpi1__o__jgenv :
    262   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    263   Joint_semantics.genv
    264 
    265 val eject__o__jgenv :
    266   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    267   Joint_semantics.genv
    268 
    269 val eval_params_of_global :
    270   Joint_semantics.sem_params -> joint_global -> Traces.evaluation_params
    271 
    272 val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    273   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    274   Joint.unserialized_params
    275 
    276 val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    277   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    278   Joint.uns_params
    279 
    280 val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
    281   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    282   Joint.stmt_params
    283 
    284 val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__spp :
    285   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    286   Joint.params
    287 
    288 val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
    289   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    290   Joint_semantics.sem_state_params
    291 
    292 val dpi1__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
    293   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    294   Joint.joint_closed_internal_function
    295   Joint_semantics.sem_unserialized_params
    296 
    297 val dpi1__o__eval_params_of_global__o__sparams__o__spp' :
    298   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    299   Joint_semantics.serialized_params
    300 
    301 val dpi1__o__eval_params_of_global__o__sparams :
    302   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    303   Joint_semantics.sem_params
    304 
    305 val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    306   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    307   Joint.unserialized_params
    308 
    309 val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    310   Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.uns_params
    311 
    312 val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
    313   Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.stmt_params
    314 
    315 val eject__o__eval_params_of_global__o__sparams__o__spp'__o__spp :
    316   Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.params
    317 
    318 val eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
    319   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    320   Joint_semantics.sem_state_params
    321 
    322 val eject__o__eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
    323   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    324   Joint.joint_closed_internal_function
    325   Joint_semantics.sem_unserialized_params
    326 
    327 val eject__o__eval_params_of_global__o__sparams__o__spp' :
    328   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    329   Joint_semantics.serialized_params
    330 
    331 val eject__o__eval_params_of_global__o__sparams :
    332   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    333   Joint_semantics.sem_params
    334 
    335 val eval_params_of_global__o__sparams :
    336   Joint_semantics.sem_params -> joint_global -> Joint_semantics.sem_params
    337 
    338 val eval_params_of_global__o__sparams__o__spp' :
    339   Joint_semantics.sem_params -> joint_global ->
    340   Joint_semantics.serialized_params
    341 
    342 val eval_params_of_global__o__sparams__o__spp'__o__msu_pars :
    343   Joint_semantics.sem_params -> joint_global ->
    344   Joint.joint_closed_internal_function
    345   Joint_semantics.sem_unserialized_params
    346 
    347 val eval_params_of_global__o__sparams__o__spp'__o__msu_pars__o__st_pars :
    348   Joint_semantics.sem_params -> joint_global ->
    349   Joint_semantics.sem_state_params
    350 
    351 val eval_params_of_global__o__sparams__o__spp'__o__spp :
    352   Joint_semantics.sem_params -> joint_global -> Joint.params
    353 
    354 val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars :
    355   Joint_semantics.sem_params -> joint_global -> Joint.stmt_params
    356 
    357 val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    358   Joint_semantics.sem_params -> joint_global -> Joint.uns_params
    359 
    360 val eval_params_of_global__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    361   Joint_semantics.sem_params -> joint_global -> Joint.unserialized_params
    362 
    363 val dpi1__o__eval_params_of_global :
    364   Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
    365   Traces.evaluation_params
    366 
    367 val eject__o__eval_params_of_global :
    368   Joint_semantics.sem_params -> joint_global Types.sig0 ->
    369   Traces.evaluation_params
    370 
    371 val make_joint_global :
    372   Joint_semantics.sem_params -> (Joint.joint_program, AST.ident -> Nat.nat
    373   Types.option) Types.prod -> joint_global
    374 
    375163val joint_exec :
    376164  Joint_semantics.sem_params -> (IO.io_out, IO.io_in)
  • extracted/joint_semantics.ml

    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
    139140(** val 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 **)
    143 let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_5376 =
    144   let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    145     get_pc_from_label0 } = x_5376
    146   in
    147   h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     142    (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
     143    -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
     144    'a2) -> 'a1 genv_gen -> 'a2 **)
     145let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_55 =
     146  let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
     147    pc_from_label = pc_from_label0 } = x_55
     148  in
     149  h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
    148150
    149151(** val genv_gen_rect_Type5 :
    150152    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 **)
    153 let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_5378 =
    154   let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    155     get_pc_from_label0 } = x_5378
    156   in
    157   h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     153    (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
     154    -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
     155    'a2) -> 'a1 genv_gen -> 'a2 **)
     156let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_57 =
     157  let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
     158    pc_from_label = pc_from_label0 } = x_57
     159  in
     160  h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
    158161
    159162(** val genv_gen_rect_Type3 :
    160163    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 **)
    163 let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_5380 =
    164   let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    165     get_pc_from_label0 } = x_5380
    166   in
    167   h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     164    (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
     165    -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
     166    'a2) -> 'a1 genv_gen -> 'a2 **)
     167let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_59 =
     168  let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
     169    pc_from_label = pc_from_label0 } = x_59
     170  in
     171  h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
    168172
    169173(** val genv_gen_rect_Type2 :
    170174    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    171     (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    172     ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    173 let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_5382 =
    174   let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    175     get_pc_from_label0 } = x_5382
    176   in
    177   h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     175    (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
     176    -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
     177    'a2) -> 'a1 genv_gen -> 'a2 **)
     178let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_61 =
     179  let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
     180    pc_from_label = pc_from_label0 } = x_61
     181  in
     182  h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
    178183
    179184(** val genv_gen_rect_Type1 :
    180185    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    181     (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    182     ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    183 let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_5384 =
    184   let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    185     get_pc_from_label0 } = x_5384
    186   in
    187   h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     186    (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
     187    -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
     188    'a2) -> 'a1 genv_gen -> 'a2 **)
     189let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_63 =
     190  let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
     191    pc_from_label = pc_from_label0 } = x_63
     192  in
     193  h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
    188194
    189195(** val genv_gen_rect_Type0 :
    190196    AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ ->
    191     (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    192     ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    193 let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_5386 =
    194   let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    195     get_pc_from_label0 } = x_5386
    196   in
    197   h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     197    (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0
     198    -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) ->
     199    'a2) -> 'a1 genv_gen -> 'a2 **)
     200let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_65 =
     201  let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0;
     202    pc_from_label = pc_from_label0 } = x_65
     203  in
     204  h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0
    198205
    199206(** val ge :
     
    207214  xxx.stack_sizes
    208215
    209 (** val get_pc_from_label :
    210     AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
    211     ByteValues.program_counter Errors.res **)
    212 let rec get_pc_from_label globals xxx =
    213   xxx.get_pc_from_label
     216(** val premain : AST.ident List.list -> 'a1 genv_gen -> 'a1 **)
     217let rec premain globals xxx =
     218  xxx.premain
     219
     220(** val pc_from_label :
     221    AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 -> 'a1
     222    -> Graphs.label -> ByteValues.program_counter Types.option **)
     223let rec pc_from_label globals xxx =
     224  xxx.pc_from_label
    214225
    215226(** val genv_gen_inv_rect_Type4 :
    216227    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
    217     -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
    218     Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
    219     'a2 **)
     228    -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     229    Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     230    Types.option) -> __ -> 'a2) -> 'a2 **)
    220231let genv_gen_inv_rect_Type4 x2 hterm h1 =
    221232  let hcut = genv_gen_rect_Type4 x2 h1 hterm in hcut __
     
    223234(** val genv_gen_inv_rect_Type3 :
    224235    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
    225     -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
    226     Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
    227     'a2 **)
     236    -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     237    Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     238    Types.option) -> __ -> 'a2) -> 'a2 **)
    228239let genv_gen_inv_rect_Type3 x2 hterm h1 =
    229240  let hcut = genv_gen_rect_Type3 x2 h1 hterm in hcut __
     
    231242(** val genv_gen_inv_rect_Type2 :
    232243    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
    233     -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
    234     Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
    235     'a2 **)
     244    -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     245    Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     246    Types.option) -> __ -> 'a2) -> 'a2 **)
    236247let genv_gen_inv_rect_Type2 x2 hterm h1 =
    237248  let hcut = genv_gen_rect_Type2 x2 h1 hterm in hcut __
     
    239250(** val genv_gen_inv_rect_Type1 :
    240251    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
    241     -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
    242     Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
    243     'a2 **)
     252    -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     253    Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     254    Types.option) -> __ -> 'a2) -> 'a2 **)
    244255let genv_gen_inv_rect_Type1 x2 hterm h1 =
    245256  let hcut = genv_gen_rect_Type1 x2 h1 hterm in hcut __
     
    247258(** val genv_gen_inv_rect_Type0 :
    248259    AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t
    249     -> __ -> (AST.ident -> Nat.nat Types.option) -> (AST.ident ->
    250     Graphs.label -> ByteValues.program_counter Errors.res) -> __ -> 'a2) ->
    251     'a2 **)
     260    -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block
     261    Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter
     262    Types.option) -> __ -> 'a2) -> 'a2 **)
    252263let genv_gen_inv_rect_Type0 x2 hterm h1 =
    253264  let hcut = genv_gen_rect_Type0 x2 h1 hterm in hcut __
     
    257268let genv_gen_discr a2 x y =
    258269  Logic.eq_rect_Type2 x
    259     (let { ge = a0; stack_sizes = a20; get_pc_from_label = a3 } = x in
    260     Obj.magic (fun _ dH -> dH __ __ __ __)) y
     270    (let { ge = a0; stack_sizes = a20; premain = a3; pc_from_label = a4 } = x
     271     in
     272    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
    261273
    262274(** val genv_gen_jmdiscr :
     
    264276let genv_gen_jmdiscr a2 x y =
    265277  Logic.eq_rect_Type2 x
    266     (let { ge = a0; stack_sizes = a20; get_pc_from_label = a3 } = x in
    267     Obj.magic (fun _ dH -> dH __ __ __ __)) y
     278    (let { ge = a0; stack_sizes = a20; premain = a3; pc_from_label = a4 } = x
     279     in
     280    Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
    268281
    269282(** val dpi1__o__ge__o__inject :
     
    296309let eject__o__ge x1 x3 =
    297310  (Types.pi1 x3).ge
     311
     312(** val pre_main_id : AST.ident **)
     313let pre_main_id =
     314  Positive.One
     315
     316(** val fetch_function :
     317    AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
     318    (AST.ident, 'a1 AST.fundef) Types.prod Errors.res **)
     319let fetch_function g ge0 bl =
     320  match Z.eqZb (Pointers.block_id (Types.pi1 bl))
     321          (Z.zopp (Z.z_of_nat (Nat.S Nat.O))) with
     322  | Bool.True ->
     323    Obj.magic
     324      (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = pre_main_id;
     325        Types.snd = (AST.Internal ge0.premain) })
     326  | Bool.False ->
     327    Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
     328      List.Nil))
     329      (Obj.magic
     330        (Monad.m_bind0 (Monad.max_def Option.option)
     331          (Obj.magic (Globalenvs.symbol_for_block ge0.ge (Types.pi1 bl)))
     332          (fun id ->
     333          Monad.m_bind0 (Monad.max_def Option.option)
     334            (Obj.magic (Globalenvs.find_funct_ptr ge0.ge (Types.pi1 bl)))
     335            (fun fd ->
     336            Monad.m_return0 (Monad.max_def Option.option) { Types.fst = id;
     337              Types.snd = fd }))))
     338
     339(** val fetch_internal_function :
     340    AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 ->
     341    (AST.ident, 'a1) Types.prod Errors.res **)
     342let fetch_internal_function g ge0 bl =
     343  Obj.magic
     344    (Monad.m_bind2 (Monad.max_def Errors.res0)
     345      (Obj.magic (fetch_function g ge0 bl)) (fun id fd ->
     346      match fd with
     347      | AST.Internal ifd ->
     348        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = id;
     349          Types.snd = ifd }
     350      | AST.External x ->
     351        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
     352          ErrorMessages.BadFunction), List.Nil)))))
     353
     354(** val code_block_of_block :
     355    Pointers.block -> Pointers.block Types.sig0 Types.option **)
     356let code_block_of_block bl =
     357  (match Pointers.block_region bl with
     358   | AST.XData -> (fun _ -> Types.None)
     359   | AST.Code -> (fun _ -> Types.Some bl)) __
     360
     361(** val block_of_funct_id :
     362    'a1 Globalenvs.genv_t -> PreIdentifiers.identifier -> Pointers.block
     363    Types.sig0 Errors.res **)
     364let block_of_funct_id ge0 id =
     365  Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
     366    (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
     367    (Obj.magic
     368      (Monad.m_bind0 (Monad.max_def Option.option)
     369        (Obj.magic (Globalenvs.find_symbol ge0 id)) (fun bl ->
     370        Obj.magic (code_block_of_block bl))))
     371
     372(** val gen_pc_from_label :
     373    AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label ->
     374    ByteValues.program_counter Errors.res **)
     375let gen_pc_from_label g ge0 id lbl =
     376  Obj.magic
     377    (Monad.m_bind0 (Monad.max_def Errors.res0)
     378      (Obj.magic (block_of_funct_id ge0.ge id)) (fun bl ->
     379      Monad.m_bind2 (Monad.max_def Errors.res0)
     380        (Obj.magic (fetch_internal_function g ge0 bl)) (fun ignore f_def ->
     381        Obj.magic
     382          (Errors.opt_to_res (List.Cons ((Errors.MSG
     383            ErrorMessages.LabelNotFound), (List.Cons ((Errors.CTX
     384            (PreIdentifiers.LabelTag, lbl)), List.Nil))))
     385            (ge0.pc_from_label bl f_def lbl)))))
    298386
    299387type genv = Joint.joint_closed_internal_function genv_gen
     
    341429    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    342430    'a1) -> sem_state_params -> 'a1 **)
    343 let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_5406 =
     431let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_86 =
    344432  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    345     load_sp0; save_sp = save_sp0 } = x_5406
     433    load_sp0; save_sp = save_sp0 } = x_86
    346434  in
    347435  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    351439    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    352440    'a1) -> sem_state_params -> 'a1 **)
    353 let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_5408 =
     441let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_88 =
    354442  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    355     load_sp0; save_sp = save_sp0 } = x_5408
     443    load_sp0; save_sp = save_sp0 } = x_88
    356444  in
    357445  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    361449    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    362450    'a1) -> sem_state_params -> 'a1 **)
    363 let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_5410 =
     451let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_90 =
    364452  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    365     load_sp0; save_sp = save_sp0 } = x_5410
     453    load_sp0; save_sp = save_sp0 } = x_90
    366454  in
    367455  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    371459    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    372460    'a1) -> sem_state_params -> 'a1 **)
    373 let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_5412 =
     461let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_92 =
    374462  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    375     load_sp0; save_sp = save_sp0 } = x_5412
     463    load_sp0; save_sp = save_sp0 } = x_92
    376464  in
    377465  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    381469    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    382470    'a1) -> sem_state_params -> 'a1 **)
    383 let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_5414 =
     471let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_94 =
    384472  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    385     load_sp0; save_sp = save_sp0 } = x_5414
     473    load_sp0; save_sp = save_sp0 } = x_94
    386474  in
    387475  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    391479    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    392480    'a1) -> sem_state_params -> 'a1 **)
    393 let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_5416 =
     481let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_96 =
    394482  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    395     load_sp0; save_sp = save_sp0 } = x_5416
     483    load_sp0; save_sp = save_sp0 } = x_96
    396484  in
    397485  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    472560let rec internal_stack_rect_Type4 h_empty_is h_one_is h_both_is = function
    473561| Empty_is -> h_empty_is
    474 | One_is x_5442 -> h_one_is x_5442
    475 | Both_is (x_5444, x_5443) -> h_both_is x_5444 x_5443
     562| One_is x_122 -> h_one_is x_122
     563| Both_is (x_124, x_123) -> h_both_is x_124 x_123
    476564
    477565(** val internal_stack_rect_Type5 :
     
    480568let rec internal_stack_rect_Type5 h_empty_is h_one_is h_both_is = function
    481569| Empty_is -> h_empty_is
    482 | One_is x_5449 -> h_one_is x_5449
    483 | Both_is (x_5451, x_5450) -> h_both_is x_5451 x_5450
     570| One_is x_129 -> h_one_is x_129
     571| Both_is (x_131, x_130) -> h_both_is x_131 x_130
    484572
    485573(** val internal_stack_rect_Type3 :
     
    488576let rec internal_stack_rect_Type3 h_empty_is h_one_is h_both_is = function
    489577| Empty_is -> h_empty_is
    490 | One_is x_5456 -> h_one_is x_5456
    491 | Both_is (x_5458, x_5457) -> h_both_is x_5458 x_5457
     578| One_is x_136 -> h_one_is x_136
     579| Both_is (x_138, x_137) -> h_both_is x_138 x_137
    492580
    493581(** val internal_stack_rect_Type2 :
     
    496584let rec internal_stack_rect_Type2 h_empty_is h_one_is h_both_is = function
    497585| Empty_is -> h_empty_is
    498 | One_is x_5463 -> h_one_is x_5463
    499 | Both_is (x_5465, x_5464) -> h_both_is x_5465 x_5464
     586| One_is x_143 -> h_one_is x_143
     587| Both_is (x_145, x_144) -> h_both_is x_145 x_144
    500588
    501589(** val internal_stack_rect_Type1 :
     
    504592let rec internal_stack_rect_Type1 h_empty_is h_one_is h_both_is = function
    505593| Empty_is -> h_empty_is
    506 | One_is x_5470 -> h_one_is x_5470
    507 | Both_is (x_5472, x_5471) -> h_both_is x_5472 x_5471
     594| One_is x_150 -> h_one_is x_150
     595| Both_is (x_152, x_151) -> h_both_is x_152 x_151
    508596
    509597(** val internal_stack_rect_Type0 :
     
    512600let rec internal_stack_rect_Type0 h_empty_is h_one_is h_both_is = function
    513601| Empty_is -> h_empty_is
    514 | One_is x_5477 -> h_one_is x_5477
    515 | Both_is (x_5479, x_5478) -> h_both_is x_5479 x_5478
     602| One_is x_157 -> h_one_is x_157
     603| Both_is (x_159, x_158) -> h_both_is x_159 x_158
    516604
    517605(** val internal_stack_inv_rect_Type4 :
     
    597685    sem_state_params -> (__ Types.option -> internal_stack ->
    598686    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
    599 let rec state_rect_Type4 semp h_mk_state x_5527 =
     687let rec state_rect_Type4 semp h_mk_state x_207 =
    600688  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    601     m = m0; stack_usage = stack_usage0 } = x_5527
     689    m = m0; stack_usage = stack_usage0 } = x_207
    602690  in
    603691  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
     
    606694    sem_state_params -> (__ Types.option -> internal_stack ->
    607695    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
    608 let rec state_rect_Type5 semp h_mk_state x_5529 =
     696let rec state_rect_Type5 semp h_mk_state x_209 =
    609697  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    610     m = m0; stack_usage = stack_usage0 } = x_5529
     698    m = m0; stack_usage = stack_usage0 } = x_209
    611699  in
    612700  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
     
    615703    sem_state_params -> (__ Types.option -> internal_stack ->
    616704    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
    617 let rec state_rect_Type3 semp h_mk_state x_5531 =
     705let rec state_rect_Type3 semp h_mk_state x_211 =
    618706  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    619     m = m0; stack_usage = stack_usage0 } = x_5531
     707    m = m0; stack_usage = stack_usage0 } = x_211
    620708  in
    621709  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
     
    624712    sem_state_params -> (__ Types.option -> internal_stack ->
    625713    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
    626 let rec state_rect_Type2 semp h_mk_state x_5533 =
     714let rec state_rect_Type2 semp h_mk_state x_213 =
    627715  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    628     m = m0; stack_usage = stack_usage0 } = x_5533
     716    m = m0; stack_usage = stack_usage0 } = x_213
    629717  in
    630718  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
     
    633721    sem_state_params -> (__ Types.option -> internal_stack ->
    634722    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
    635 let rec state_rect_Type1 semp h_mk_state x_5535 =
     723let rec state_rect_Type1 semp h_mk_state x_215 =
    636724  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    637     m = m0; stack_usage = stack_usage0 } = x_5535
     725    m = m0; stack_usage = stack_usage0 } = x_215
    638726  in
    639727  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
     
    642730    sem_state_params -> (__ Types.option -> internal_stack ->
    643731    ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **)
    644 let rec state_rect_Type0 semp h_mk_state x_5537 =
     732let rec state_rect_Type0 semp h_mk_state x_217 =
    645733  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    646     m = m0; stack_usage = stack_usage0 } = x_5537
     734    m = m0; stack_usage = stack_usage0 } = x_217
    647735  in
    648736  h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0
     
    720808    sem_state_params -> (state -> ByteValues.program_counter ->
    721809    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    722 let rec state_pc_rect_Type4 semp h_mk_state_pc x_5553 =
    723   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5553 in
     810let rec state_pc_rect_Type4 semp h_mk_state_pc x_233 =
     811  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_233 in
    724812  h_mk_state_pc st_no_pc0 pc0 last_pop0
    725813
     
    727815    sem_state_params -> (state -> ByteValues.program_counter ->
    728816    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    729 let rec state_pc_rect_Type5 semp h_mk_state_pc x_5555 =
    730   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5555 in
     817let rec state_pc_rect_Type5 semp h_mk_state_pc x_235 =
     818  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_235 in
    731819  h_mk_state_pc st_no_pc0 pc0 last_pop0
    732820
     
    734822    sem_state_params -> (state -> ByteValues.program_counter ->
    735823    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    736 let rec state_pc_rect_Type3 semp h_mk_state_pc x_5557 =
    737   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5557 in
     824let rec state_pc_rect_Type3 semp h_mk_state_pc x_237 =
     825  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_237 in
    738826  h_mk_state_pc st_no_pc0 pc0 last_pop0
    739827
     
    741829    sem_state_params -> (state -> ByteValues.program_counter ->
    742830    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    743 let rec state_pc_rect_Type2 semp h_mk_state_pc x_5559 =
    744   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5559 in
     831let rec state_pc_rect_Type2 semp h_mk_state_pc x_239 =
     832  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_239 in
    745833  h_mk_state_pc st_no_pc0 pc0 last_pop0
    746834
     
    748836    sem_state_params -> (state -> ByteValues.program_counter ->
    749837    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    750 let rec state_pc_rect_Type1 semp h_mk_state_pc x_5561 =
    751   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5561 in
     838let rec state_pc_rect_Type1 semp h_mk_state_pc x_241 =
     839  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_241 in
    752840  h_mk_state_pc st_no_pc0 pc0 last_pop0
    753841
     
    755843    sem_state_params -> (state -> ByteValues.program_counter ->
    756844    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    757 let rec state_pc_rect_Type0 semp h_mk_state_pc x_5563 =
    758   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_5563 in
     845let rec state_pc_rect_Type0 semp h_mk_state_pc x_243 =
     846  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_243 in
    759847  h_mk_state_pc st_no_pc0 pc0 last_pop0
    760848
     
    895983  { st_frms = (Types.Some frms); istack = st.istack; carry = st.carry; regs =
    896984    st.regs; m = st.m; stack_usage = st.stack_usage }
    897 
    898 (** val fetch_function :
    899     'a1 Globalenvs.genv_t -> Pointers.block Types.sig0 -> (AST.ident, 'a1)
    900     Types.prod Errors.res **)
    901 let fetch_function ge0 bl =
    902   Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
    903     List.Nil))
    904     (Obj.magic
    905       (Monad.m_bind0 (Monad.max_def Option.option)
    906         (Obj.magic (Globalenvs.symbol_for_block ge0 (Types.pi1 bl)))
    907         (fun id ->
    908         Monad.m_bind0 (Monad.max_def Option.option)
    909           (Obj.magic (Globalenvs.find_funct_ptr ge0 (Types.pi1 bl)))
    910           (fun fd ->
    911           Monad.m_return0 (Monad.max_def Option.option) { Types.fst = id;
    912             Types.snd = fd }))))
    913 
    914 (** val fetch_internal_function :
    915     'a1 AST.fundef Globalenvs.genv_t -> Pointers.block Types.sig0 ->
    916     (AST.ident, 'a1) Types.prod Errors.res **)
    917 let fetch_internal_function ge0 bl =
    918   Obj.magic
    919     (Monad.m_bind2 (Monad.max_def Errors.res0)
    920       (Obj.magic (fetch_function ge0 bl)) (fun id fd ->
    921       match fd with
    922       | AST.Internal ifd ->
    923         Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = id;
    924           Types.snd = ifd }
    925       | AST.External x ->
    926         Obj.magic (Errors.Error (List.Cons ((Errors.MSG
    927           ErrorMessages.BadFunction), List.Nil)))))
    928985
    929986type call_kind =
     
    10941151    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    10951152    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1096 let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_5618 =
     1153let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_298 =
    10971154  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    10981155    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    11061163    set_result0; call_args_for_main = call_args_for_main0;
    11071164    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1108     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5618
     1165    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_298
    11091166  in
    11101167  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    11351192    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    11361193    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1137 let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_5620 =
     1194let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_300 =
    11381195  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    11391196    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    11471204    set_result0; call_args_for_main = call_args_for_main0;
    11481205    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1149     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5620
     1206    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_300
    11501207  in
    11511208  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    11761233    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    11771234    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1178 let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_5622 =
     1235let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_302 =
    11791236  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    11801237    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    11881245    set_result0; call_args_for_main = call_args_for_main0;
    11891246    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1190     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5622
     1247    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_302
    11911248  in
    11921249  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    12171274    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    12181275    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1219 let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_5624 =
     1276let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_304 =
    12201277  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    12211278    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    12291286    set_result0; call_args_for_main = call_args_for_main0;
    12301287    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1231     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5624
     1288    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_304
    12321289  in
    12331290  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    12581315    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    12591316    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1260 let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_5626 =
     1317let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_306 =
    12611318  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    12621319    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    12701327    set_result0; call_args_for_main = call_args_for_main0;
    12711328    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1272     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5626
     1329    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_306
    12731330  in
    12741331  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    12991356    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    13001357    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1301 let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_5628 =
     1358let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_308 =
    13021359  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    13031360    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    13111368    set_result0; call_args_for_main = call_args_for_main0;
    13121369    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1313     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_5628
     1370    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_308
    13141371  in
    13151372  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    17611818    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17621819    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
    1763 let rec serialized_params_rect_Type4 h_mk_serialized_params x_5698 =
     1820let rec serialized_params_rect_Type4 h_mk_serialized_params x_378 =
    17641821  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1765     point_of_offset = point_of_offset0 } = x_5698
     1822    point_of_offset = point_of_offset0 } = x_378
    17661823  in
    17671824  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     
    17721829    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17731830    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
    1774 let rec serialized_params_rect_Type5 h_mk_serialized_params x_5700 =
     1831let rec serialized_params_rect_Type5 h_mk_serialized_params x_380 =
    17751832  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1776     point_of_offset = point_of_offset0 } = x_5700
     1833    point_of_offset = point_of_offset0 } = x_380
    17771834  in
    17781835  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     
    17831840    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17841841    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
    1785 let rec serialized_params_rect_Type3 h_mk_serialized_params x_5702 =
     1842let rec serialized_params_rect_Type3 h_mk_serialized_params x_382 =
    17861843  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1787     point_of_offset = point_of_offset0 } = x_5702
     1844    point_of_offset = point_of_offset0 } = x_382
    17881845  in
    17891846  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     
    17941851    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17951852    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
    1796 let rec serialized_params_rect_Type2 h_mk_serialized_params x_5704 =
     1853let rec serialized_params_rect_Type2 h_mk_serialized_params x_384 =
    17971854  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1798     point_of_offset = point_of_offset0 } = x_5704
     1855    point_of_offset = point_of_offset0 } = x_384
    17991856  in
    18001857  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     
    18051862    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    18061863    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
    1807 let rec serialized_params_rect_Type1 h_mk_serialized_params x_5706 =
     1864let rec serialized_params_rect_Type1 h_mk_serialized_params x_386 =
    18081865  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1809     point_of_offset = point_of_offset0 } = x_5706
     1866    point_of_offset = point_of_offset0 } = x_386
    18101867  in
    18111868  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     
    18161873    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    18171874    -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **)
    1818 let rec serialized_params_rect_Type0 h_mk_serialized_params x_5708 =
     1875let rec serialized_params_rect_Type0 h_mk_serialized_params x_388 =
    18191876  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1820     point_of_offset = point_of_offset0 } = x_5708
     1877    point_of_offset = point_of_offset0 } = x_388
    18211878  in
    18221879  h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __
     
    19101967    (serialized_params -> (Joint.joint_program ->
    19111968    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
    1912 let rec sem_params_rect_Type4 h_mk_sem_params x_5726 =
    1913   let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5726 in
     1969let rec sem_params_rect_Type4 h_mk_sem_params x_406 =
     1970  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_406 in
    19141971  h_mk_sem_params spp'0 pre_main_generator0
    19151972
     
    19171974    (serialized_params -> (Joint.joint_program ->
    19181975    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
    1919 let rec sem_params_rect_Type5 h_mk_sem_params x_5728 =
    1920   let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5728 in
     1976let rec sem_params_rect_Type5 h_mk_sem_params x_408 =
     1977  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_408 in
    19211978  h_mk_sem_params spp'0 pre_main_generator0
    19221979
     
    19241981    (serialized_params -> (Joint.joint_program ->
    19251982    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
    1926 let rec sem_params_rect_Type3 h_mk_sem_params x_5730 =
    1927   let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5730 in
     1983let rec sem_params_rect_Type3 h_mk_sem_params x_410 =
     1984  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_410 in
    19281985  h_mk_sem_params spp'0 pre_main_generator0
    19291986
     
    19311988    (serialized_params -> (Joint.joint_program ->
    19321989    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
    1933 let rec sem_params_rect_Type2 h_mk_sem_params x_5732 =
    1934   let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5732 in
     1990let rec sem_params_rect_Type2 h_mk_sem_params x_412 =
     1991  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_412 in
    19351992  h_mk_sem_params spp'0 pre_main_generator0
    19361993
     
    19381995    (serialized_params -> (Joint.joint_program ->
    19391996    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
    1940 let rec sem_params_rect_Type1 h_mk_sem_params x_5734 =
    1941   let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5734 in
     1997let rec sem_params_rect_Type1 h_mk_sem_params x_414 =
     1998  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_414 in
    19421999  h_mk_sem_params spp'0 pre_main_generator0
    19432000
     
    19452002    (serialized_params -> (Joint.joint_program ->
    19462003    Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **)
    1947 let rec sem_params_rect_Type0 h_mk_sem_params x_5736 =
    1948   let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_5736 in
     2004let rec sem_params_rect_Type0 h_mk_sem_params x_416 =
     2005  let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_416 in
    19492006  h_mk_sem_params spp'0 pre_main_generator0
    19502007
     
    20342091
    20352092(** val fetch_statement :
    2036     sem_params -> AST.ident List.list -> Joint.joint_function
    2037     Globalenvs.genv_t -> ByteValues.program_counter -> ((AST.ident,
    2038     Joint.joint_closed_internal_function) Types.prod, Joint.joint_statement)
    2039     Types.prod Errors.res **)
     2093    sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter
     2094    -> ((AST.ident, Joint.joint_closed_internal_function) Types.prod,
     2095    Joint.joint_statement) Types.prod Errors.res **)
    20402096let fetch_statement p globals ge0 ptr =
    20412097  Obj.magic
    20422098    (Monad.m_bind2 (Monad.max_def Errors.res0)
    2043       (Obj.magic (fetch_internal_function ge0 ptr.ByteValues.pc_block))
     2099      (Obj.magic
     2100        (fetch_internal_function globals ge0 ptr.ByteValues.pc_block))
    20442101      (fun id fn ->
    20452102      let pt = point_of_pc p ptr in
     
    20542111
    20552112(** val pc_of_label :
    2056     sem_params -> AST.ident List.list -> Joint.joint_function
    2057     Globalenvs.genv_t -> Pointers.block Types.sig0 -> Graphs.label ->
    2058     ByteValues.program_counter Errors.res **)
     2113    sem_params -> AST.ident List.list -> genv -> Pointers.block Types.sig0 ->
     2114    Graphs.label -> ByteValues.program_counter Errors.res **)
    20592115let pc_of_label p globals ge0 bl lbl =
    20602116  Obj.magic
    20612117    (Monad.m_bind2 (Monad.max_def Errors.res0)
    2062       (Obj.magic (fetch_internal_function ge0 bl)) (fun i fn ->
     2118      (Obj.magic (fetch_internal_function globals ge0 bl)) (fun i fn ->
    20632119      Monad.m_bind0 (Monad.max_def Errors.res0)
    20642120        (Obj.magic
     
    20802136
    20812137(** val goto :
    2082     sem_params -> AST.ident List.list -> Joint.joint_function
    2083     Globalenvs.genv_t -> Graphs.label -> state_pc -> state_pc Errors.res **)
     2138    sem_params -> AST.ident List.list -> genv -> Graphs.label -> state_pc ->
     2139    state_pc Errors.res **)
    20842140let goto p globals ge0 l st =
    20852141  Obj.magic
     
    20962152
    20972153(** val next_of_call_pc :
    2098     sem_params -> AST.ident List.list -> Joint.joint_function
    2099     Globalenvs.genv_t -> ByteValues.program_counter -> __ Errors.res **)
     2154    sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter
     2155    -> __ Errors.res **)
    21002156let next_of_call_pc p globals ge0 pc0 =
    21012157  Obj.magic
     
    22892345    p.spp'.msu_pars.eval_ext_seq globals ge0 c curr_id st
    22902346
    2291 (** val code_block_of_block :
    2292     Pointers.block -> Pointers.block Types.sig0 Types.option **)
    2293 let code_block_of_block bl =
    2294   (match Pointers.block_region bl with
    2295    | AST.XData -> (fun _ -> Types.None)
    2296    | AST.Code -> (fun _ -> Types.Some bl)) __
    2297 
    2298 (** val block_of_funct_id :
    2299     sem_state_params -> 'a1 Globalenvs.genv_t -> PreIdentifiers.identifier ->
    2300     Pointers.block Types.sig0 Errors.res **)
    2301 let block_of_funct_id sp0 ge0 id =
    2302   Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction),
    2303     (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
    2304     (Obj.magic
    2305       (Monad.m_bind0 (Monad.max_def Option.option)
    2306         (Obj.magic (Globalenvs.find_symbol ge0 id)) (fun bl ->
    2307         Obj.magic (code_block_of_block bl))))
    2308 
    23092347(** val block_of_call :
    23102348    sem_params -> AST.ident List.list -> Joint.joint_function
     
    24232461    Obj.magic x) (fun bl ->
    24242462    Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    2425       (let x =
    2426          IOMonad.err_to_io
    2427            (fetch_function
    2428              (let p0 = spp'__o__spp p in
    2429              let globals0 = globals in let g = ge0 in g.ge) bl)
    2430        in
     2463      (let x = IOMonad.err_to_io (fetch_function globals ge0 bl) in
    24312464      Obj.magic x) (fun i fd ->
    24322465      match fd with
     
    24882521      (fun st' call_pc ->
    24892522      Monad.m_bind0 (Monad.max_def Errors.res0)
    2490         (Obj.magic
    2491           (next_of_call_pc p globals
    2492             (let p0 = spp'__o__spp p in
    2493             let globals0 = globals in let g = ge0 in g.ge) call_pc))
    2494         (fun nxt ->
     2523        (Obj.magic (next_of_call_pc p globals ge0 call_pc)) (fun nxt ->
    24952524        let st'' =
    24962525          set_last_pop p.spp'.msu_pars.st_pars
     
    25152544    Obj.magic x) (fun bl ->
    25162545    Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    2517       (let x =
    2518          IOMonad.err_to_io
    2519            (fetch_function
    2520              (let p0 = spp'__o__spp p in
    2521              let globals0 = globals in let g = ge0 in g.ge) bl)
    2522        in
     2546      (let x = IOMonad.err_to_io (fetch_function globals ge0 bl) in
    25232547      Obj.magic x) (fun i fd ->
    25242548      match fd with
     
    25772601               (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
    25782602               match b with
    2579                | Bool.True ->
    2580                  Obj.magic
    2581                    (goto p g
    2582                      (let p0 = spp'__o__spp p in
    2583                      let globals = g in let g0 = ge0 in g0.ge) l st)
     2603               | Bool.True -> Obj.magic (goto p g ge0 l st)
    25842604               | Bool.False ->
    25852605                 Monad.m_return0 (Monad.max_def Errors.res0) (next p nxt st)))))
     
    25902610    let curr_ret = (Types.pi1 curr_fn).Joint.joint_if_result in
    25912611    (match s0 with
    2592      | Joint.GOTO l ->
    2593        IOMonad.err_to_io
    2594          (goto p g
    2595            (let p0 = spp'__o__spp p in
    2596            let globals = g in let g0 = ge0 in g0.ge) l st)
     2612     | Joint.GOTO l -> IOMonad.err_to_io (goto p g ge0 l st)
    25972613     | Joint.RETURN ->
    25982614       IOMonad.err_to_io
     
    26112627            (Obj.magic (ByteValues.bool_of_beval v)) (fun b ->
    26122628            match b with
    2613             | Bool.True ->
    2614               Obj.magic
    2615                 (goto p g
    2616                   (let p0 = spp'__o__spp p in
    2617                   let globals = g in let g0 = ge0 in g0.ge) lbltrue st)
    2618             | Bool.False ->
    2619               Obj.magic
    2620                 (goto p g
    2621                   (let p0 = spp'__o__spp p in
    2622                   let globals = g in let g0 = ge0 in g0.ge) lblfalse st)))))
     2629            | Bool.True -> Obj.magic (goto p g ge0 lbltrue st)
     2630            | Bool.False -> Obj.magic (goto p g ge0 lblfalse st)))))
    26232631
    26242632(** val eval_state :
     
    26282636  Obj.magic
    26292637    (Monad.m_bind3 (Monad.max_def IOMonad.iOMonad)
    2630       (let x =
    2631          IOMonad.err_to_io
    2632            (fetch_statement p globals
    2633              (let p0 = spp'__o__spp p in
    2634              let globals0 = globals in let g = ge0 in g.ge) st.pc)
    2635        in
     2638      (let x = IOMonad.err_to_io (fetch_statement p globals ge0 st.pc) in
    26362639      Obj.magic x) (fun id fn s ->
    26372640      Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
  • 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 :
  • extracted/lIN.ml

    r2951 r2960  
    134134    (Obj.magic Types.It))) }, (List.Cons ({ Types.fst = Types.None;
    135135    Types.snd = (Joint.Sequential ((Joint.CALL ((Types.Inl
    136     p.Joint.joint_prog.AST.prog_main),
    137     (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
     136    p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
    138137    (Obj.magic Types.It))), (Obj.magic Types.It))) }, (List.Cons
    139138    ({ Types.fst = (Types.Some l3); Types.snd = (Joint.Final (Joint.GOTO
  • extracted/lINToASM.ml

    r2951 r2960  
    141141    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    142142    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    143 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_2395 =
     143let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_250 =
    144144  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    145     ident_map0; label_map = label_map0; address_map = address_map0 } = x_2395
     145    ident_map0; label_map = label_map0; address_map = address_map0 } = x_250
    146146  in
    147147  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    153153    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    154154    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    155 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_2397 =
     155let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_252 =
    156156  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    157     ident_map0; label_map = label_map0; address_map = address_map0 } = x_2397
     157    ident_map0; label_map = label_map0; address_map = address_map0 } = x_252
    158158  in
    159159  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    165165    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    166166    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    167 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_2399 =
     167let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_254 =
    168168  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    169     ident_map0; label_map = label_map0; address_map = address_map0 } = x_2399
     169    ident_map0; label_map = label_map0; address_map = address_map0 } = x_254
    170170  in
    171171  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    177177    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    178178    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    179 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_2401 =
     179let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_256 =
    180180  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    181     ident_map0; label_map = label_map0; address_map = address_map0 } = x_2401
     181    ident_map0; label_map = label_map0; address_map = address_map0 } = x_256
    182182  in
    183183  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    189189    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    190190    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    191 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_2403 =
     191let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_258 =
    192192  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    193     ident_map0; label_map = label_map0; address_map = address_map0 } = x_2403
     193    ident_map0; label_map = label_map0; address_map = address_map0 } = x_258
    194194  in
    195195  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    201201    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    202202    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    203 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_2405 =
     203let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_260 =
    204204  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    205     ident_map0; label_map = label_map0; address_map = address_map0 } = x_2405
     205    ident_map0; label_map = label_map0; address_map = address_map0 } = x_260
    206206  in
    207207  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    288288  let globals_addr_internal = fun res_offset x_size ->
    289289    let { Types.fst = res; Types.snd = offset } = res_offset in
    290     let { Types.fst = eta24644; Types.snd = data } = x_size in
    291     let { Types.fst = x; Types.snd = region } = eta24644 in
     290    let { Types.fst = eta17; Types.snd = data } = x_size in
     291    let { Types.fst = x; Types.snd = region } = eta17 in
    292292    { Types.fst =
    293293    (Identifiers.add PreIdentifiers.SymbolTag res x
     
    320320        (Identifiers.empty_map PreIdentifiers.LabelTag)
    321321    in
    322     let { Types.fst = eta24645; Types.snd = lmap0 } =
     322    let { Types.fst = eta18; Types.snd = lmap0 } =
    323323      match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
    324324      | Types.None ->
     
    332332          lmap }
    333333    in
    334     let { Types.fst = id; Types.snd = univ } = eta24645 in
     334    let { Types.fst = id; Types.snd = univ } = eta18 in
    335335    { Types.fst = { id_univ = univ; current_funct = current; ident_map =
    336336    u.ident_map; label_map =
     
    344344  Obj.magic (fun u ->
    345345    let imap = u.ident_map in
    346     let { Types.fst = eta24646; Types.snd = imap0 } =
     346    let { Types.fst = eta19; Types.snd = imap0 } =
    347347      match Identifiers.lookup PreIdentifiers.SymbolTag imap i with
    348348      | Types.None ->
     
    356356          imap }
    357357    in
    358     let { Types.fst = id; Types.snd = univ } = eta24646 in
     358    let { Types.fst = id; Types.snd = univ } = eta19 in
    359359    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
    360360    ident_map = imap0; label_map = u.label_map; address_map =
  • extracted/lTL.ml

    r2951 r2960  
    198198    Joint.add_graph lTL (AST.prog_var_names p.Joint.joint_prog) l2
    199199      (Joint.Sequential ((Joint.CALL ((Types.Inl
    200       p.Joint.joint_prog.AST.prog_main),
    201       (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
     200      p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
    202201      (Obj.magic Types.It))), (Obj.magic l3))) res0
    203202  in
  • extracted/policy.ml

    r2904 r2960  
    9494let rec jump_expansion_internal program n =
    9595  let labels = PolicyFront.create_label_map (Types.pi1 program) in
    96   let rec aux res =
    97 prerr_endline "JEI_start";
    98    let { Types.fst = no_ch; Types.snd = z } = res in
    99     match z with
    100      | Types.None ->
    101        { Types.fst = Bool.False; Types.snd = Types.None }
    102      | Types.Some op ->
    103          match no_ch with
    104          | Bool.True -> res
    105          | Bool.False ->
    106            aux
    107             (Types.pi1
    108              (PolicyStep.jump_expansion_step program (Types.pi1 labels)
    109                op))
    110   in
    111    aux
    112     { Types.fst = Bool.False; Types.snd =
    113        (Types.pi1
    114          (PolicyFront.jump_expansion_start program (Types.pi1 labels))) }
    115 (*
    11696  (match n with
    11797   | Nat.O ->
     
    134114              Types.pi1
    135115                (PolicyStep.jump_expansion_step program (Types.pi1 labels)
    136                   op))) __)) __)) __*)
     116                  op))) __)) __)) __
    137117
    138118(** val measure_int :
  • extracted/rTL.ml

    r2951 r2960  
    125125    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    126126let rec rtl_seq_rect_Type4 h_rtl_stack_address = function
    127 | Rtl_stack_address (x_18179, x_18178) -> h_rtl_stack_address x_18179 x_18178
     127| Rtl_stack_address (x_7, x_6) -> h_rtl_stack_address x_7 x_6
    128128
    129129(** val rtl_seq_rect_Type5 :
    130130    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    131131let rec rtl_seq_rect_Type5 h_rtl_stack_address = function
    132 | Rtl_stack_address (x_18183, x_18182) -> h_rtl_stack_address x_18183 x_18182
     132| Rtl_stack_address (x_11, x_10) -> h_rtl_stack_address x_11 x_10
    133133
    134134(** val rtl_seq_rect_Type3 :
    135135    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    136136let rec rtl_seq_rect_Type3 h_rtl_stack_address = function
    137 | Rtl_stack_address (x_18187, x_18186) -> h_rtl_stack_address x_18187 x_18186
     137| Rtl_stack_address (x_15, x_14) -> h_rtl_stack_address x_15 x_14
    138138
    139139(** val rtl_seq_rect_Type2 :
    140140    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    141141let rec rtl_seq_rect_Type2 h_rtl_stack_address = function
    142 | Rtl_stack_address (x_18191, x_18190) -> h_rtl_stack_address x_18191 x_18190
     142| Rtl_stack_address (x_19, x_18) -> h_rtl_stack_address x_19 x_18
    143143
    144144(** val rtl_seq_rect_Type1 :
    145145    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    146146let rec rtl_seq_rect_Type1 h_rtl_stack_address = function
    147 | Rtl_stack_address (x_18195, x_18194) -> h_rtl_stack_address x_18195 x_18194
     147| Rtl_stack_address (x_23, x_22) -> h_rtl_stack_address x_23 x_22
    148148
    149149(** val rtl_seq_rect_Type0 :
    150150    (Registers.register -> Registers.register -> 'a1) -> rtl_seq -> 'a1 **)
    151151let rec rtl_seq_rect_Type0 h_rtl_stack_address = function
    152 | Rtl_stack_address (x_18199, x_18198) -> h_rtl_stack_address x_18199 x_18198
     152| Rtl_stack_address (x_27, x_26) -> h_rtl_stack_address x_27 x_26
    153153
    154154(** val rtl_seq_inv_rect_Type4 :
     
    312312    Joint.add_graph rTL (AST.prog_var_names p.Joint.joint_prog) l2
    313313      (Joint.Sequential ((Joint.CALL ((Types.Inl
    314       p.Joint.joint_prog.AST.prog_main),
    315       (Obj.magic (List.map (fun x -> Joint.Reg x) rs)), (Obj.magic rs))),
    316       (Obj.magic l3))) res0
     314      p.Joint.joint_prog.AST.prog_main), (Obj.magic List.Nil),
     315      (Obj.magic List.Nil))), (Obj.magic l3))) res0
    317316  in
    318317  let res2 =
  • extracted/rTL_semantics.ml

    r2951 r2960  
    157157    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    158158    'a1) -> reg_sp -> 'a1 **)
    159 let rec reg_sp_rect_Type4 h_mk_reg_sp x_6032 =
    160   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6032 in
     159let rec reg_sp_rect_Type4 h_mk_reg_sp x_3 =
     160  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_3 in
    161161  h_mk_reg_sp reg_sp_env0 stackp0
    162162
     
    164164    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    165165    'a1) -> reg_sp -> 'a1 **)
    166 let rec reg_sp_rect_Type5 h_mk_reg_sp x_6034 =
    167   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6034 in
     166let rec reg_sp_rect_Type5 h_mk_reg_sp x_5 =
     167  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_5 in
    168168  h_mk_reg_sp reg_sp_env0 stackp0
    169169
     
    171171    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    172172    'a1) -> reg_sp -> 'a1 **)
    173 let rec reg_sp_rect_Type3 h_mk_reg_sp x_6036 =
    174   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6036 in
     173let rec reg_sp_rect_Type3 h_mk_reg_sp x_7 =
     174  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_7 in
    175175  h_mk_reg_sp reg_sp_env0 stackp0
    176176
     
    178178    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    179179    'a1) -> reg_sp -> 'a1 **)
    180 let rec reg_sp_rect_Type2 h_mk_reg_sp x_6038 =
    181   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6038 in
     180let rec reg_sp_rect_Type2 h_mk_reg_sp x_9 =
     181  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_9 in
    182182  h_mk_reg_sp reg_sp_env0 stackp0
    183183
     
    185185    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    186186    'a1) -> reg_sp -> 'a1 **)
    187 let rec reg_sp_rect_Type1 h_mk_reg_sp x_6040 =
    188   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6040 in
     187let rec reg_sp_rect_Type1 h_mk_reg_sp x_11 =
     188  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_11 in
    189189  h_mk_reg_sp reg_sp_env0 stackp0
    190190
     
    192192    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    193193    'a1) -> reg_sp -> 'a1 **)
    194 let rec reg_sp_rect_Type0 h_mk_reg_sp x_6042 =
    195   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_6042 in
     194let rec reg_sp_rect_Type0 h_mk_reg_sp x_13 =
     195  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_13 in
    196196  h_mk_reg_sp reg_sp_env0 stackp0
    197197
     
    297297    (Registers.register List.list -> ByteValues.program_counter ->
    298298    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
    299 let rec frame_rect_Type4 h_mk_frame x_6058 =
     299let rec frame_rect_Type4 h_mk_frame x_29 =
    300300  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    301     fr_regs = fr_regs0 } = x_6058
     301    fr_regs = fr_regs0 } = x_29
    302302  in
    303303  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    306306    (Registers.register List.list -> ByteValues.program_counter ->
    307307    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
    308 let rec frame_rect_Type5 h_mk_frame x_6060 =
     308let rec frame_rect_Type5 h_mk_frame x_31 =
    309309  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    310     fr_regs = fr_regs0 } = x_6060
     310    fr_regs = fr_regs0 } = x_31
    311311  in
    312312  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    315315    (Registers.register List.list -> ByteValues.program_counter ->
    316316    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
    317 let rec frame_rect_Type3 h_mk_frame x_6062 =
     317let rec frame_rect_Type3 h_mk_frame x_33 =
    318318  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    319     fr_regs = fr_regs0 } = x_6062
     319    fr_regs = fr_regs0 } = x_33
    320320  in
    321321  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    324324    (Registers.register List.list -> ByteValues.program_counter ->
    325325    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
    326 let rec frame_rect_Type2 h_mk_frame x_6064 =
     326let rec frame_rect_Type2 h_mk_frame x_35 =
    327327  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    328     fr_regs = fr_regs0 } = x_6064
     328    fr_regs = fr_regs0 } = x_35
    329329  in
    330330  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    333333    (Registers.register List.list -> ByteValues.program_counter ->
    334334    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
    335 let rec frame_rect_Type1 h_mk_frame x_6066 =
     335let rec frame_rect_Type1 h_mk_frame x_37 =
    336336  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    337     fr_regs = fr_regs0 } = x_6066
     337    fr_regs = fr_regs0 } = x_37
    338338  in
    339339  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    342342    (Registers.register List.list -> ByteValues.program_counter ->
    343343    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
    344 let rec frame_rect_Type0 h_mk_frame x_6068 =
     344let rec frame_rect_Type0 h_mk_frame x_39 =
    345345  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    346     fr_regs = fr_regs0 } = x_6068
     346    fr_regs = fr_regs0 } = x_39
    347347  in
    348348  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    471471          (Joint_semantics.set_m rTL_state_params mem st))))))) __
    472472
    473 (** val stackOverflow : ErrorMessages.errorMessage **)
    474 let stackOverflow = ErrorMessages.MISSING
    475 
    476473(** val rtl_setup_call_separate_overflow :
    477474    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
     
    485482    rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st
    486483  | Bool.False ->
    487     Errors.Error (List.Cons ((Errors.MSG stackOverflow), List.Nil))
     484    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.StackOverflow), List.Nil))
    488485
    489486(** val rtl_setup_call_unique :
     
    535532    AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
    536533    Values.val0 List.list Errors.res **)
    537 let rtl_fetch_external_args _ = assert false
     534let rtl_fetch_external_args _ =
     535  failwith "AXIOM TO BE REALIZED"
    538536
    539537(** val rtl_set_result :
    540538    Values.val0 List.list -> Registers.register List.list -> rTL_state ->
    541539    rTL_state Errors.res **)
    542 let rtl_set_result _ = assert false
     540let rtl_set_result _ =
     541  failwith "AXIOM TO BE REALIZED"
    543542
    544543(** val rtl_reg_store :
  • extracted/rTL_semantics.mli

    r2951 r2960  
    306306  rTL_state -> rTL_state Errors.res
    307307
    308 val stackOverflow : ErrorMessages.errorMessage
    309 
    310308val rtl_setup_call_separate_overflow :
    311309  Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
  • extracted/rTLabsToRTL.ml

    r2951 r2960  
    154154    -> 'a1) -> register_type -> 'a1 **)
    155155let rec register_type_rect_Type4 h_register_int h_register_ptr = function
    156 | Register_int x_18401 -> h_register_int x_18401
    157 | Register_ptr (x_18403, x_18402) -> h_register_ptr x_18403 x_18402
     156| Register_int x_60 -> h_register_int x_60
     157| Register_ptr (x_62, x_61) -> h_register_ptr x_62 x_61
    158158
    159159(** val register_type_rect_Type5 :
     
    161161    -> 'a1) -> register_type -> 'a1 **)
    162162let rec register_type_rect_Type5 h_register_int h_register_ptr = function
    163 | Register_int x_18407 -> h_register_int x_18407
    164 | Register_ptr (x_18409, x_18408) -> h_register_ptr x_18409 x_18408
     163| Register_int x_66 -> h_register_int x_66
     164| Register_ptr (x_68, x_67) -> h_register_ptr x_68 x_67
    165165
    166166(** val register_type_rect_Type3 :
     
    168168    -> 'a1) -> register_type -> 'a1 **)
    169169let rec register_type_rect_Type3 h_register_int h_register_ptr = function
    170 | Register_int x_18413 -> h_register_int x_18413
    171 | Register_ptr (x_18415, x_18414) -> h_register_ptr x_18415 x_18414
     170| Register_int x_72 -> h_register_int x_72
     171| Register_ptr (x_74, x_73) -> h_register_ptr x_74 x_73
    172172
    173173(** val register_type_rect_Type2 :
     
    175175    -> 'a1) -> register_type -> 'a1 **)
    176176let rec register_type_rect_Type2 h_register_int h_register_ptr = function
    177 | Register_int x_18419 -> h_register_int x_18419
    178 | Register_ptr (x_18421, x_18420) -> h_register_ptr x_18421 x_18420
     177| Register_int x_78 -> h_register_int x_78
     178| Register_ptr (x_80, x_79) -> h_register_ptr x_80 x_79
    179179
    180180(** val register_type_rect_Type1 :
     
    182182    -> 'a1) -> register_type -> 'a1 **)
    183183let rec register_type_rect_Type1 h_register_int h_register_ptr = function
    184 | Register_int x_18425 -> h_register_int x_18425
    185 | Register_ptr (x_18427, x_18426) -> h_register_ptr x_18427 x_18426
     184| Register_int x_84 -> h_register_int x_84
     185| Register_ptr (x_86, x_85) -> h_register_ptr x_86 x_85
    186186
    187187(** val register_type_rect_Type0 :
     
    189189    -> 'a1) -> register_type -> 'a1 **)
    190190let rec register_type_rect_Type0 h_register_int h_register_ptr = function
    191 | Register_int x_18431 -> h_register_int x_18431
    192 | Register_ptr (x_18433, x_18432) -> h_register_ptr x_18433 x_18432
     191| Register_int x_90 -> h_register_int x_90
     192| Register_ptr (x_92, x_91) -> h_register_ptr x_92 x_91
    193193
    194194(** val register_type_inv_rect_Type4 :
  • extracted/semantics.ml

    r2951 r2960  
    324324    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    325325    preclassified_system_pass -> 'a1 **)
    326 let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_6084 =
    327   let pcs_pcs = x_6084 in h_mk_preclassified_system_pass pcs_pcs __
     326let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_108 =
     327  let pcs_pcs = x_108 in h_mk_preclassified_system_pass pcs_pcs __
    328328
    329329(** val preclassified_system_pass_rect_Type5 :
    330330    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    331331    preclassified_system_pass -> 'a1 **)
    332 let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_6086 =
    333   let pcs_pcs = x_6086 in h_mk_preclassified_system_pass pcs_pcs __
     332let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_110 =
     333  let pcs_pcs = x_110 in h_mk_preclassified_system_pass pcs_pcs __
    334334
    335335(** val preclassified_system_pass_rect_Type3 :
    336336    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    337337    preclassified_system_pass -> 'a1 **)
    338 let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_6088 =
    339   let pcs_pcs = x_6088 in h_mk_preclassified_system_pass pcs_pcs __
     338let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_112 =
     339  let pcs_pcs = x_112 in h_mk_preclassified_system_pass pcs_pcs __
    340340
    341341(** val preclassified_system_pass_rect_Type2 :
    342342    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    343343    preclassified_system_pass -> 'a1 **)
    344 let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_6090 =
    345   let pcs_pcs = x_6090 in h_mk_preclassified_system_pass pcs_pcs __
     344let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_114 =
     345  let pcs_pcs = x_114 in h_mk_preclassified_system_pass pcs_pcs __
    346346
    347347(** val preclassified_system_pass_rect_Type1 :
    348348    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    349349    preclassified_system_pass -> 'a1 **)
    350 let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_6092 =
    351   let pcs_pcs = x_6092 in h_mk_preclassified_system_pass pcs_pcs __
     350let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_116 =
     351  let pcs_pcs = x_116 in h_mk_preclassified_system_pass pcs_pcs __
    352352
    353353(** val preclassified_system_pass_rect_Type0 :
    354354    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    355355    preclassified_system_pass -> 'a1 **)
    356 let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_6094 =
    357   let pcs_pcs = x_6094 in h_mk_preclassified_system_pass pcs_pcs __
     356let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_118 =
     357  let pcs_pcs = x_118 in h_mk_preclassified_system_pass pcs_pcs __
    358358
    359359(** val pcs_pcs :
     
    447447| Compiler.Assembly_pass ->
    448448  (fun prog ->
    449     let { Types.fst = eta27867; Types.snd = policy } = Obj.magic prog in
    450     let { Types.fst = code; Types.snd = sigma } = eta27867 in
     449    let { Types.fst = eta26; Types.snd = policy } = Obj.magic prog in
     450    let { Types.fst = code; Types.snd = sigma } = eta26 in
    451451    Interpret2.aSM_preclassified_system code sigma policy)
    452452| Compiler.Object_code_pass ->
  • extracted/semanticsUtils.ml

    r2951 r2960  
    168168    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    169169    -> hw_register_env -> 'a1 **)
    170 let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_5847 =
    171   let { reg_env = reg_env0; other_bit = other_bit0 } = x_5847 in
     170let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_432 =
     171  let { reg_env = reg_env0; other_bit = other_bit0 } = x_432 in
    172172  h_mk_hw_register_env reg_env0 other_bit0
    173173
     
    175175    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    176176    -> hw_register_env -> 'a1 **)
    177 let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_5849 =
    178   let { reg_env = reg_env0; other_bit = other_bit0 } = x_5849 in
     177let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_434 =
     178  let { reg_env = reg_env0; other_bit = other_bit0 } = x_434 in
    179179  h_mk_hw_register_env reg_env0 other_bit0
    180180
     
    182182    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    183183    -> hw_register_env -> 'a1 **)
    184 let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_5851 =
    185   let { reg_env = reg_env0; other_bit = other_bit0 } = x_5851 in
     184let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_436 =
     185  let { reg_env = reg_env0; other_bit = other_bit0 } = x_436 in
    186186  h_mk_hw_register_env reg_env0 other_bit0
    187187
     
    189189    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    190190    -> hw_register_env -> 'a1 **)
    191 let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_5853 =
    192   let { reg_env = reg_env0; other_bit = other_bit0 } = x_5853 in
     191let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_438 =
     192  let { reg_env = reg_env0; other_bit = other_bit0 } = x_438 in
    193193  h_mk_hw_register_env reg_env0 other_bit0
    194194
     
    196196    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    197197    -> hw_register_env -> 'a1 **)
    198 let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_5855 =
    199   let { reg_env = reg_env0; other_bit = other_bit0 } = x_5855 in
     198let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_440 =
     199  let { reg_env = reg_env0; other_bit = other_bit0 } = x_440 in
    200200  h_mk_hw_register_env reg_env0 other_bit0
    201201
     
    203203    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    204204    -> hw_register_env -> 'a1 **)
    205 let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_5857 =
    206   let { reg_env = reg_env0; other_bit = other_bit0 } = x_5857 in
     205let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_442 =
     206  let { reg_env = reg_env0; other_bit = other_bit0 } = x_442 in
    207207  h_mk_hw_register_env reg_env0 other_bit0
    208208
     
    319319    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    320320    -> sem_graph_params -> 'a1 **)
    321 let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_5873 =
     321let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_458 =
    322322  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    323     graph_pre_main_generator0 } = x_5873
     323    graph_pre_main_generator0 } = x_458
    324324  in
    325325  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    329329    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    330330    -> sem_graph_params -> 'a1 **)
    331 let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_5875 =
     331let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_460 =
    332332  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    333     graph_pre_main_generator0 } = x_5875
     333    graph_pre_main_generator0 } = x_460
    334334  in
    335335  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    339339    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    340340    -> sem_graph_params -> 'a1 **)
    341 let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_5877 =
     341let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_462 =
    342342  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    343     graph_pre_main_generator0 } = x_5877
     343    graph_pre_main_generator0 } = x_462
    344344  in
    345345  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    349349    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    350350    -> sem_graph_params -> 'a1 **)
    351 let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_5879 =
     351let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_464 =
    352352  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    353     graph_pre_main_generator0 } = x_5879
     353    graph_pre_main_generator0 } = x_464
    354354  in
    355355  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    359359    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    360360    -> sem_graph_params -> 'a1 **)
    361 let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_5881 =
     361let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_466 =
    362362  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    363     graph_pre_main_generator0 } = x_5881
     363    graph_pre_main_generator0 } = x_466
    364364  in
    365365  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    369369    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    370370    -> sem_graph_params -> 'a1 **)
    371 let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_5883 =
     371let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_468 =
    372372  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
    373     graph_pre_main_generator0 } = x_5883
     373    graph_pre_main_generator0 } = x_468
    374374  in
    375375  h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
     
    501501    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    502502    -> sem_lin_params -> 'a1 **)
    503 let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_5900 =
     503let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_485 =
    504504  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    505     lin_pre_main_generator0 } = x_5900
     505    lin_pre_main_generator0 } = x_485
    506506  in
    507507  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    511511    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    512512    -> sem_lin_params -> 'a1 **)
    513 let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_5902 =
     513let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_487 =
    514514  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    515     lin_pre_main_generator0 } = x_5902
     515    lin_pre_main_generator0 } = x_487
    516516  in
    517517  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    521521    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    522522    -> sem_lin_params -> 'a1 **)
    523 let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_5904 =
     523let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_489 =
    524524  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    525     lin_pre_main_generator0 } = x_5904
     525    lin_pre_main_generator0 } = x_489
    526526  in
    527527  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    531531    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    532532    -> sem_lin_params -> 'a1 **)
    533 let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_5906 =
     533let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_491 =
    534534  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    535     lin_pre_main_generator0 } = x_5906
     535    lin_pre_main_generator0 } = x_491
    536536  in
    537537  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    541541    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    542542    -> sem_lin_params -> 'a1 **)
    543 let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_5908 =
     543let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_493 =
    544544  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    545     lin_pre_main_generator0 } = x_5908
     545    lin_pre_main_generator0 } = x_493
    546546  in
    547547  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    551551    -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
    552552    -> sem_lin_params -> 'a1 **)
    553 let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_5910 =
     553let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_495 =
    554554  let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
    555     lin_pre_main_generator0 } = x_5910
     555    lin_pre_main_generator0 } = x_495
    556556  in
    557557  h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
     
    669669    (sem_lin_params_to_sem_params x0)
    670670
    671 (** val pre_main_id : AST.ident **)
    672 let pre_main_id =
    673   Positive.One
    674 
    675 (** val joint_globalenv :
    676     Joint_semantics.sem_params -> Joint.joint_program ->
    677     Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
    678 let joint_globalenv pars prog =
    679   let genv =
    680     Globalenvs.drop_fn pre_main_id
    681       (Globalenvs.globalenv (fun x -> x) prog.Joint.joint_prog)
    682   in
    683   { Globalenvs.functions =
    684   (PositiveMap.insert Positive.One (AST.Internal
    685     (pars.Joint_semantics.pre_main_generator prog))
    686     genv.Globalenvs.functions); Globalenvs.nextfunction =
    687   genv.Globalenvs.nextfunction; Globalenvs.symbols =
    688   (Identifiers.add PreIdentifiers.SymbolTag genv.Globalenvs.symbols
    689     pre_main_id (Z.zopp (Z.z_of_nat (Nat.S Nat.O)))) }
    690 
    691671(** val match_genv_t_rect_Type4 :
    692672    AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     
    767747  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
    768748
     749(** val joint_globalenv :
     750    Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
     751    Nat.nat Types.option) -> Joint_semantics.genv **)
     752let joint_globalenv p prog stacksizes =
     753  let genv = Globalenvs.globalenv (fun x -> x) prog.Joint.joint_prog in
     754  let pc_from_lbl = fun bl fn lbl ->
     755    Monad.m_bind0 (Monad.max_def Option.option)
     756      (Obj.magic
     757        ((Joint_semantics.spp'__o__spp p).Joint.point_of_label
     758          (AST.prog_var_names prog.Joint.joint_prog)
     759          (Types.pi1 fn).Joint.joint_if_code lbl)) (fun pt ->
     760      Monad.m_return0 (Monad.max_def Option.option) { ByteValues.pc_block =
     761        bl; ByteValues.pc_offset =
     762        (p.Joint_semantics.spp'.Joint_semantics.offset_of_point pt) })
     763  in
     764  { Joint_semantics.ge = genv; Joint_semantics.stack_sizes = stacksizes;
     765  Joint_semantics.premain = (p.Joint_semantics.pre_main_generator prog);
     766  Joint_semantics.pc_from_label = (Obj.magic pc_from_lbl) }
     767
  • extracted/semanticsUtils.mli

    r2951 r2960  
    422422  sem_lin_params -> Joint.unserialized_params
    423423
    424 val pre_main_id : AST.ident
     424val match_genv_t_rect_Type4 :
     425  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     426  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
     427
     428val match_genv_t_rect_Type5 :
     429  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     430  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
     431
     432val match_genv_t_rect_Type3 :
     433  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     434  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
     435
     436val match_genv_t_rect_Type2 :
     437  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     438  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
     439
     440val match_genv_t_rect_Type1 :
     441  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     442  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
     443
     444val match_genv_t_rect_Type0 :
     445  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     446  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
     447
     448val match_genv_t_inv_rect_Type4 :
     449  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     450  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
     451
     452val match_genv_t_inv_rect_Type3 :
     453  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     454  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
     455
     456val match_genv_t_inv_rect_Type2 :
     457  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     458  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
     459
     460val match_genv_t_inv_rect_Type1 :
     461  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     462  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
     463
     464val match_genv_t_inv_rect_Type0 :
     465  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     466  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
     467
     468val match_genv_t_discr :
     469  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     470  Globalenvs.genv_t -> __
     471
     472val match_genv_t_jmdiscr :
     473  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
     474  Globalenvs.genv_t -> __
    425475
    426476val joint_globalenv :
    427   Joint_semantics.sem_params -> Joint.joint_program ->
    428   Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    429 
    430 val match_genv_t_rect_Type4 :
    431   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    432   Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
    433 
    434 val match_genv_t_rect_Type5 :
    435   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    436   Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
    437 
    438 val match_genv_t_rect_Type3 :
    439   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    440   Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
    441 
    442 val match_genv_t_rect_Type2 :
    443   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    444   Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
    445 
    446 val match_genv_t_rect_Type1 :
    447   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    448   Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
    449 
    450 val match_genv_t_rect_Type0 :
    451   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    452   Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
    453 
    454 val match_genv_t_inv_rect_Type4 :
    455   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    456   Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
    457 
    458 val match_genv_t_inv_rect_Type3 :
    459   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    460   Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
    461 
    462 val match_genv_t_inv_rect_Type2 :
    463   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    464   Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
    465 
    466 val match_genv_t_inv_rect_Type1 :
    467   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    468   Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
    469 
    470 val match_genv_t_inv_rect_Type0 :
    471   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    472   Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
    473 
    474 val match_genv_t_discr :
    475   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    476   Globalenvs.genv_t -> __
    477 
    478 val match_genv_t_jmdiscr :
    479   AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
    480   Globalenvs.genv_t -> __
    481 
     477  Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
     478  Types.option) -> Joint_semantics.genv
     479
  • extracted/toCminor.ml

    r2951 r2960  
    198198    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    199199let rec var_type_rect_Type4 h_Global h_Stack h_Local = function
    200 | Global x_13081 -> h_Global x_13081
    201 | Stack x_13082 -> h_Stack x_13082
     200| Global x_138 -> h_Global x_138
     201| Stack x_139 -> h_Stack x_139
    202202| Local -> h_Local
    203203
     
    205205    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    206206let rec var_type_rect_Type5 h_Global h_Stack h_Local = function
    207 | Global x_13087 -> h_Global x_13087
    208 | Stack x_13088 -> h_Stack x_13088
     207| Global x_144 -> h_Global x_144
     208| Stack x_145 -> h_Stack x_145
    209209| Local -> h_Local
    210210
     
    212212    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    213213let rec var_type_rect_Type3 h_Global h_Stack h_Local = function
    214 | Global x_13093 -> h_Global x_13093
    215 | Stack x_13094 -> h_Stack x_13094
     214| Global x_150 -> h_Global x_150
     215| Stack x_151 -> h_Stack x_151
    216216| Local -> h_Local
    217217
     
    219219    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    220220let rec var_type_rect_Type2 h_Global h_Stack h_Local = function
    221 | Global x_13099 -> h_Global x_13099
    222 | Stack x_13100 -> h_Stack x_13100
     221| Global x_156 -> h_Global x_156
     222| Stack x_157 -> h_Stack x_157
    223223| Local -> h_Local
    224224
     
    226226    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    227227let rec var_type_rect_Type1 h_Global h_Stack h_Local = function
    228 | Global x_13105 -> h_Global x_13105
    229 | Stack x_13106 -> h_Stack x_13106
     228| Global x_162 -> h_Global x_162
     229| Stack x_163 -> h_Stack x_163
    230230| Local -> h_Local
    231231
     
    233233    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    234234let rec var_type_rect_Type0 h_Global h_Stack h_Local = function
    235 | Global x_13111 -> h_Global x_13111
    236 | Stack x_13112 -> h_Stack x_13112
     235| Global x_168 -> h_Global x_168
     236| Stack x_169 -> h_Stack x_169
    237237| Local -> h_Local
    238238
     
    12211221let rec destination_rect_Type4 vars h_IdDest h_MemDest = function
    12221222| IdDest (id, ty) -> h_IdDest id ty __
    1223 | MemDest x_14567 -> h_MemDest x_14567
     1223| MemDest x_216 -> h_MemDest x_216
    12241224
    12251225(** val destination_rect_Type5 :
     
    12281228let rec destination_rect_Type5 vars h_IdDest h_MemDest = function
    12291229| IdDest (id, ty) -> h_IdDest id ty __
    1230 | MemDest x_14572 -> h_MemDest x_14572
     1230| MemDest x_221 -> h_MemDest x_221
    12311231
    12321232(** val destination_rect_Type3 :
     
    12351235let rec destination_rect_Type3 vars h_IdDest h_MemDest = function
    12361236| IdDest (id, ty) -> h_IdDest id ty __
    1237 | MemDest x_14577 -> h_MemDest x_14577
     1237| MemDest x_226 -> h_MemDest x_226
    12381238
    12391239(** val destination_rect_Type2 :
     
    12421242let rec destination_rect_Type2 vars h_IdDest h_MemDest = function
    12431243| IdDest (id, ty) -> h_IdDest id ty __
    1244 | MemDest x_14582 -> h_MemDest x_14582
     1244| MemDest x_231 -> h_MemDest x_231
    12451245
    12461246(** val destination_rect_Type1 :
     
    12491249let rec destination_rect_Type1 vars h_IdDest h_MemDest = function
    12501250| IdDest (id, ty) -> h_IdDest id ty __
    1251 | MemDest x_14587 -> h_MemDest x_14587
     1251| MemDest x_236 -> h_MemDest x_236
    12521252
    12531253(** val destination_rect_Type0 :
     
    12561256let rec destination_rect_Type0 vars h_IdDest h_MemDest = function
    12571257| IdDest (id, ty) -> h_IdDest id ty __
    1258 | MemDest x_14592 -> h_MemDest x_14592
     1258| MemDest x_241 -> h_MemDest x_241
    12591259
    12601260(** val destination_inv_rect_Type4 :
     
    13821382    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13831383    'a1) -> labgen -> 'a1 **)
    1384 let rec labgen_rect_Type4 h_mk_labgen x_14627 =
    1385   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1386     x_14627
     1384let rec labgen_rect_Type4 h_mk_labgen x_276 =
     1385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_276
    13871386  in
    13881387  h_mk_labgen labuniverse0 label_genlist0 __
     
    13911390    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13921391    'a1) -> labgen -> 'a1 **)
    1393 let rec labgen_rect_Type5 h_mk_labgen x_14629 =
    1394   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1395     x_14629
     1392let rec labgen_rect_Type5 h_mk_labgen x_278 =
     1393  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_278
    13961394  in
    13971395  h_mk_labgen labuniverse0 label_genlist0 __
     
    14001398    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14011399    'a1) -> labgen -> 'a1 **)
    1402 let rec labgen_rect_Type3 h_mk_labgen x_14631 =
    1403   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1404     x_14631
     1400let rec labgen_rect_Type3 h_mk_labgen x_280 =
     1401  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_280
    14051402  in
    14061403  h_mk_labgen labuniverse0 label_genlist0 __
     
    14091406    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14101407    'a1) -> labgen -> 'a1 **)
    1411 let rec labgen_rect_Type2 h_mk_labgen x_14633 =
    1412   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1413     x_14633
     1408let rec labgen_rect_Type2 h_mk_labgen x_282 =
     1409  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_282
    14141410  in
    14151411  h_mk_labgen labuniverse0 label_genlist0 __
     
    14181414    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14191415    'a1) -> labgen -> 'a1 **)
    1420 let rec labgen_rect_Type1 h_mk_labgen x_14635 =
    1421   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1422     x_14635
     1416let rec labgen_rect_Type1 h_mk_labgen x_284 =
     1417  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_284
    14231418  in
    14241419  h_mk_labgen labuniverse0 label_genlist0 __
     
    14271422    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14281423    'a1) -> labgen -> 'a1 **)
    1429 let rec labgen_rect_Type0 h_mk_labgen x_14637 =
    1430   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1431     x_14637
     1424let rec labgen_rect_Type0 h_mk_labgen x_286 =
     1425  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_286
    14321426  in
    14331427  h_mk_labgen labuniverse0 label_genlist0 __
     
    15541548    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15551549    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14653 =
    1557   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14653 in
     1550let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_302 =
     1551  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_302 in
    15581552  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15591553
     
    15611555    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15621556    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14655 =
    1564   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14655 in
     1557let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_304 =
     1558  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_304 in
    15651559  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15661560
     
    15681562    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15691563    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14657 =
    1571   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14657 in
     1564let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_306 =
     1565  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_306 in
    15721566  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15731567
     
    15751569    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15761570    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14659 =
    1578   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14659 in
     1571let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_308 =
     1572  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_308 in
    15791573  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15801574
     
    15821576    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15831577    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14661 =
    1585   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14661 in
     1578let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_310 =
     1579  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_310 in
    15861580  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15871581
     
    15891583    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15901584    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14663 =
    1592   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14663 in
     1585let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_312 =
     1586  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_312 in
    15931587  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15941588
     
    16741668let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
    16751669| DoNotConvert -> h_DoNotConvert
    1676 | ConvertTo (x_14685, x_14684) -> h_ConvertTo x_14685 x_14684
     1670| ConvertTo (x_334, x_333) -> h_ConvertTo x_334 x_333
    16771671
    16781672(** val convert_flag_rect_Type5 :
     
    16811675let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
    16821676| DoNotConvert -> h_DoNotConvert
    1683 | ConvertTo (x_14690, x_14689) -> h_ConvertTo x_14690 x_14689
     1677| ConvertTo (x_339, x_338) -> h_ConvertTo x_339 x_338
    16841678
    16851679(** val convert_flag_rect_Type3 :
     
    16881682let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
    16891683| DoNotConvert -> h_DoNotConvert
    1690 | ConvertTo (x_14695, x_14694) -> h_ConvertTo x_14695 x_14694
     1684| ConvertTo (x_344, x_343) -> h_ConvertTo x_344 x_343
    16911685
    16921686(** val convert_flag_rect_Type2 :
     
    16951689let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
    16961690| DoNotConvert -> h_DoNotConvert
    1697 | ConvertTo (x_14700, x_14699) -> h_ConvertTo x_14700 x_14699
     1691| ConvertTo (x_349, x_348) -> h_ConvertTo x_349 x_348
    16981692
    16991693(** val convert_flag_rect_Type1 :
     
    17021696let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
    17031697| DoNotConvert -> h_DoNotConvert
    1704 | ConvertTo (x_14705, x_14704) -> h_ConvertTo x_14705 x_14704
     1698| ConvertTo (x_354, x_353) -> h_ConvertTo x_354 x_353
    17051699
    17061700(** val convert_flag_rect_Type0 :
     
    17091703let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
    17101704| DoNotConvert -> h_DoNotConvert
    1711 | ConvertTo (x_14710, x_14709) -> h_ConvertTo x_14710 x_14709
     1705| ConvertTo (x_359, x_358) -> h_ConvertTo x_359 x_358
    17121706
    17131707(** val convert_flag_inv_rect_Type4 :
     
    20322026        (Cminor_syntax.St_cost (l, s1')) })))
    20332027
    2034 (** val alloc_params :
     2028(** val alloc_params_main :
    20352029    var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag ->
    20362030    AST.typ Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list
     
    20382032    Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt)
    20392033    Types.prod Types.sig0 Errors.res **)
    2040 let alloc_params vars lbls statement uv ul rettyp params s =
     2034let alloc_params_main vars lbls statement uv ul rettyp params s =
    20412035  Util.foldl (fun su it ->
    20422036    let { Types.fst = id; Types.snd = ty } = it in
    20432037    Obj.magic
    20442038      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2045         (fun eta2436 ->
    2046         let result = eta2436 in
     2039        (fun eta650 ->
     2040        let result = eta650 in
    20472041        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20482042        (fun _ ->
     
    20622056             | Local -> (fun _ -> Errors.OK result)) __)))) __))) (Errors.OK
    20632057    s) params
     2058
     2059(** val alloc_params :
     2060    var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag ->
     2061    AST.typ Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list
     2062    -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod
     2063    Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt)
     2064    Types.prod Types.sig0 Errors.res **)
     2065let alloc_params vars lbls statement uv ul rettyp params su =
     2066  (let { Types.fst = tl; Types.snd = s0 } = Types.pi1 su in
     2067  (match s0 with
     2068   | Cminor_syntax.St_skip ->
     2069     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2070   | Cminor_syntax.St_assign (x, x0, x1) ->
     2071     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2072   | Cminor_syntax.St_store (x, x0, x1) ->
     2073     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2074   | Cminor_syntax.St_call (x, x0, x1) ->
     2075     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2076   | Cminor_syntax.St_seq (x, x0) ->
     2077     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2078   | Cminor_syntax.St_ifthenelse (x, x0, x1, x2, x3) ->
     2079     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2080   | Cminor_syntax.St_return x ->
     2081     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2082   | Cminor_syntax.St_label (x, x0) ->
     2083     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2084   | Cminor_syntax.St_goto x ->
     2085     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2086   | Cminor_syntax.St_cost (cl, s') ->
     2087     (fun _ ->
     2088       Obj.magic
     2089         (Monad.m_bind0 (Monad.max_def Errors.res0)
     2090           (Obj.magic
     2091             (alloc_params_main vars lbls statement uv ul rettyp params
     2092               { Types.fst = tl; Types.snd = s' })) (fun tls ->
     2093           Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     2094             (Types.pi1 tls).Types.fst; Types.snd = (Cminor_syntax.St_cost
     2095             (cl, (Types.pi1 tls).Types.snd)) }))))) __
    20642096
    20652097(** val populate_lenv :
  • extracted/toCminor.mli

    r2773 r2960  
    495495  Types.option -> Csyntax.statement -> ((tmpgen, labgen) Types.prod,
    496496  Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res
     497
     498val alloc_params_main :
     499  var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag -> AST.typ
     500  Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list ->
     501  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 ->
     502  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0
     503  Errors.res
    497504
    498505val alloc_params :
  • 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 :
  • extracted/traces.mli

    r2951 r2960  
    152152
    153153type evaluation_params = { globals : AST.ident List.list;
    154                            sparams : Joint_semantics.sem_params;
    155154                           ev_genv : Joint_semantics.genv }
    156155
    157156val evaluation_params_rect_Type4 :
    158   (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
     157  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    159158  -> 'a1) -> evaluation_params -> 'a1
    160159
    161160val evaluation_params_rect_Type5 :
    162   (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
     161  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    163162  -> 'a1) -> evaluation_params -> 'a1
    164163
    165164val evaluation_params_rect_Type3 :
    166   (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
     165  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    167166  -> 'a1) -> evaluation_params -> 'a1
    168167
    169168val evaluation_params_rect_Type2 :
    170   (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
     169  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    171170  -> 'a1) -> evaluation_params -> 'a1
    172171
    173172val evaluation_params_rect_Type1 :
    174   (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
     173  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
    175174  -> 'a1) -> evaluation_params -> 'a1
    176175
    177176val evaluation_params_rect_Type0 :
    178   (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
    179   -> 'a1) -> evaluation_params -> 'a1
    180 
    181 val globals : evaluation_params -> AST.ident List.list
    182 
    183 val sparams : evaluation_params -> Joint_semantics.sem_params
    184 
    185 val ev_genv : evaluation_params -> Joint_semantics.genv
     177  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
     178  -> 'a1) -> evaluation_params -> 'a1
     179
     180val globals :
     181  Joint_semantics.sem_params -> evaluation_params -> AST.ident List.list
     182
     183val ev_genv :
     184  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
    186185
    187186val evaluation_params_inv_rect_Type4 :
    188   evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
     187  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
    189188  Joint_semantics.genv -> __ -> 'a1) -> 'a1
    190189
    191190val evaluation_params_inv_rect_Type3 :
    192   evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
     191  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
    193192  Joint_semantics.genv -> __ -> 'a1) -> 'a1
    194193
    195194val evaluation_params_inv_rect_Type2 :
    196   evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
     195  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
    197196  Joint_semantics.genv -> __ -> 'a1) -> 'a1
    198197
    199198val evaluation_params_inv_rect_Type1 :
    200   evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
     199  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
    201200  Joint_semantics.genv -> __ -> 'a1) -> 'a1
    202201
    203202val evaluation_params_inv_rect_Type0 :
    204   evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
    205   Joint_semantics.genv -> __ -> 'a1) -> 'a1
    206 
    207 val evaluation_params_jmdiscr : evaluation_params -> evaluation_params -> __
    208 
    209 val sparams__o__spp' : evaluation_params -> Joint_semantics.serialized_params
    210 
    211 val sparams__o__spp'__o__msu_pars :
    212   evaluation_params -> Joint.joint_closed_internal_function
    213   Joint_semantics.sem_unserialized_params
    214 
    215 val sparams__o__spp'__o__msu_pars__o__st_pars :
    216   evaluation_params -> Joint_semantics.sem_state_params
    217 
    218 val sparams__o__spp'__o__spp : evaluation_params -> Joint.params
    219 
    220 val sparams__o__spp'__o__spp__o__stmt_pars :
    221   evaluation_params -> Joint.stmt_params
    222 
    223 val sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    224   evaluation_params -> Joint.uns_params
    225 
    226 val sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    227   evaluation_params -> Joint.unserialized_params
     203  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
     204  Joint_semantics.genv -> __ -> 'a1) -> 'a1
     205
     206val evaluation_params_discr :
     207  Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> __
     208
     209val evaluation_params_jmdiscr :
     210  Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> __
     211
     212val dpi1__o__ev_genv__o__inject :
     213  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
     214  Joint_semantics.genv Types.sig0
     215
     216val dpi1__o__ev_genv__o__genv_to_genv_t__o__inject :
     217  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
     218  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     219  Types.sig0
     220
     221val dpi1__o__ev_genv__o__genv_to_genv_t :
     222  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
     223  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     224
     225val eject__o__ev_genv__o__inject :
     226  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
     227  Joint_semantics.genv Types.sig0
     228
     229val eject__o__ev_genv__o__genv_to_genv_t__o__inject :
     230  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
     231  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     232  Types.sig0
     233
     234val eject__o__ev_genv__o__genv_to_genv_t :
     235  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
     236  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     237
     238val ev_genv__o__genv_to_genv_t :
     239  Joint_semantics.sem_params -> evaluation_params ->
     240  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     241
     242val ev_genv__o__genv_to_genv_t__o__inject :
     243  Joint_semantics.sem_params -> evaluation_params ->
     244  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
     245  Types.sig0
     246
     247val ev_genv__o__inject :
     248  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
     249  Types.sig0
     250
     251val dpi1__o__ev_genv :
     252  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
     253  Joint_semantics.genv
     254
     255val eject__o__ev_genv :
     256  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
     257  Joint_semantics.genv
    228258
    229259type prog_params = { prog_spars : Joint_semantics.sem_params;
     
    283313val prog_params_jmdiscr : prog_params -> prog_params -> __
    284314
    285 val make_global : prog_params -> evaluation_params
    286 
    287 val prog_params_to_ev_params__o__sparams :
    288   prog_params -> Joint_semantics.sem_params
    289 
    290 val prog_params_to_ev_params__o__sparams__o__spp' :
    291   prog_params -> Joint_semantics.serialized_params
    292 
    293 val prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars :
     315val prog_spars__o__spp' : prog_params -> Joint_semantics.serialized_params
     316
     317val prog_spars__o__spp'__o__msu_pars :
    294318  prog_params -> Joint.joint_closed_internal_function
    295319  Joint_semantics.sem_unserialized_params
    296320
    297 val prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars :
     321val prog_spars__o__spp'__o__msu_pars__o__st_pars :
    298322  prog_params -> Joint_semantics.sem_state_params
    299323
    300 val prog_params_to_ev_params__o__sparams__o__spp'__o__spp :
    301   prog_params -> Joint.params
    302 
    303 val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars :
     324val prog_spars__o__spp'__o__spp : prog_params -> Joint.params
     325
     326val prog_spars__o__spp'__o__spp__o__stmt_pars :
    304327  prog_params -> Joint.stmt_params
    305328
    306 val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
     329val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    307330  prog_params -> Joint.uns_params
    308331
    309 val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
     332val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    310333  prog_params -> Joint.unserialized_params
    311334
     335val joint_make_global : prog_params -> evaluation_params
     336
     337val joint_make_global__o__ev_genv : prog_params -> Joint_semantics.genv
     338
     339val joint_make_global__o__ev_genv__o__genv_to_genv_t :
     340  prog_params -> Joint.joint_closed_internal_function AST.fundef
     341  Globalenvs.genv_t
     342
     343val joint_make_global__o__ev_genv__o__genv_to_genv_t__o__inject :
     344  prog_params -> Joint.joint_closed_internal_function AST.fundef
     345  Globalenvs.genv_t Types.sig0
     346
     347val joint_make_global__o__ev_genv__o__inject :
     348  prog_params -> Joint_semantics.genv Types.sig0
     349
     350val joint_make_global__o__inject :
     351  prog_params -> evaluation_params Types.sig0
     352
    312353val make_initial_state : prog_params -> Joint_semantics.state_pc
    313354
    314355val joint_classify_step :
    315   evaluation_params -> Joint.joint_step -> StructuredTraces.status_class
     356  Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
     357  StructuredTraces.status_class
    316358
    317359val joint_classify_final :
    318   evaluation_params -> Joint.joint_fin_step -> StructuredTraces.status_class
     360  Joint.unserialized_params -> Joint.joint_fin_step ->
     361  StructuredTraces.status_class
    319362
    320363val joint_classify :
    321   evaluation_params -> Joint_semantics.state_pc ->
    322   StructuredTraces.status_class
     364  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
     365  -> StructuredTraces.status_class
    323366
    324367val joint_call_ident :
    325   evaluation_params -> Joint_semantics.state_pc -> AST.ident
     368  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
     369  -> AST.ident
    326370
    327371val joint_tailcall_ident :
    328   evaluation_params -> Joint_semantics.state_pc -> AST.ident
     372  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
     373  -> AST.ident
    329374
    330375val pcDeq : Deqsets.deqSet
    331376
    332377val cost_label_of_stmt :
    333   evaluation_params -> Joint.joint_statement -> CostLabel.costlabel
    334   Types.option
     378  Joint_semantics.sem_params -> evaluation_params -> Joint.joint_statement ->
     379  CostLabel.costlabel Types.option
    335380
    336381val joint_label_of_pc :
    337   evaluation_params -> ByteValues.program_counter -> CostLabel.costlabel
    338   Types.option
     382  Joint_semantics.sem_params -> evaluation_params ->
     383  ByteValues.program_counter -> CostLabel.costlabel Types.option
    339384
    340385val exit_pc' : ByteValues.program_counter
    341386
    342387val joint_final :
    343   Joint_semantics.sem_params -> AST.ident List.list -> Joint_semantics.genv
    344   -> Joint_semantics.state_pc -> Integers.int Types.option
     388  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
     389  -> Integers.int Types.option
    345390
    346391val joint_abstract_status : prog_params -> StructuredTraces.abstract_status
Note: See TracChangeset for help on using the changeset viewer.