Changeset 2890


Ignore:
Timestamp:
Mar 15, 2013, 11:11:45 PM (4 years ago)
Author:
sacerdot
Message:

Exported again, now the execution is correct up to LIN for a simple program.

Location:
extracted
Files:
18 edited

Legend:

Unmodified
Added
Removed
  • extracted/aSMCosts.ml

    r2873 r2890  
    209209   | Nat.S program_size' ->
    210210     (fun _ ->
    211        (let { Types.fst = eta31796; Types.snd = ticks } =
     211       (let { Types.fst = eta31808; Types.snd = ticks } =
    212212          Fetch.fetch code_memory' program_counter'
    213213        in
    214214       let { Types.fst = instruction; Types.snd = program_counter'' } =
    215          eta31796
     215         eta31808
    216216       in
    217217       (fun _ ->
  • extracted/cminor_semantics.ml

    r2873 r2890  
    123123let rec cont_rect_Type4 h_Kend h_Kseq h_Kblock = function
    124124| Kend -> h_Kend
    125 | Kseq (x_25457, x_25456) ->
    126   h_Kseq x_25457 x_25456 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_25456)
    127 | Kblock x_25458 ->
    128   h_Kblock x_25458 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_25458)
     125| Kseq (x_25483, x_25482) ->
     126  h_Kseq x_25483 x_25482 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_25482)
     127| Kblock x_25484 ->
     128  h_Kblock x_25484 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_25484)
    129129
    130130(** val cont_rect_Type3 :
     
    133133let rec cont_rect_Type3 h_Kend h_Kseq h_Kblock = function
    134134| Kend -> h_Kend
    135 | Kseq (x_25471, x_25470) ->
    136   h_Kseq x_25471 x_25470 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_25470)
    137 | Kblock x_25472 ->
    138   h_Kblock x_25472 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_25472)
     135| Kseq (x_25497, x_25496) ->
     136  h_Kseq x_25497 x_25496 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_25496)
     137| Kblock x_25498 ->
     138  h_Kblock x_25498 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_25498)
    139139
    140140(** val cont_rect_Type2 :
     
    143143let rec cont_rect_Type2 h_Kend h_Kseq h_Kblock = function
    144144| Kend -> h_Kend
    145 | Kseq (x_25478, x_25477) ->
    146   h_Kseq x_25478 x_25477 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_25477)
    147 | Kblock x_25479 ->
    148   h_Kblock x_25479 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_25479)
     145| Kseq (x_25504, x_25503) ->
     146  h_Kseq x_25504 x_25503 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_25503)
     147| Kblock x_25505 ->
     148  h_Kblock x_25505 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_25505)
    149149
    150150(** val cont_rect_Type1 :
     
    153153let rec cont_rect_Type1 h_Kend h_Kseq h_Kblock = function
    154154| Kend -> h_Kend
    155 | Kseq (x_25485, x_25484) ->
    156   h_Kseq x_25485 x_25484 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_25484)
    157 | Kblock x_25486 ->
    158   h_Kblock x_25486 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_25486)
     155| Kseq (x_25511, x_25510) ->
     156  h_Kseq x_25511 x_25510 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_25510)
     157| Kblock x_25512 ->
     158  h_Kblock x_25512 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_25512)
    159159
    160160(** val cont_rect_Type0 :
     
    163163let rec cont_rect_Type0 h_Kend h_Kseq h_Kblock = function
    164164| Kend -> h_Kend
    165 | Kseq (x_25492, x_25491) ->
    166   h_Kseq x_25492 x_25491 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_25491)
    167 | Kblock x_25493 ->
    168   h_Kblock x_25493 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_25493)
     165| Kseq (x_25518, x_25517) ->
     166  h_Kseq x_25518 x_25517 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_25517)
     167| Kblock x_25519 ->
     168  h_Kblock x_25519 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_25519)
    169169
    170170(** val cont_inv_rect_Type4 :
     
    226226let rec stack_rect_Type4 h_SStop h_Scall = function
    227227| SStop -> h_SStop
    228 | Scall (dest, f, x_25552, en, k, x_25548) ->
    229   h_Scall dest f x_25552 en __ __ k __ x_25548
    230     (stack_rect_Type4 h_SStop h_Scall x_25548)
     228| Scall (dest, f, x_25578, en, k, x_25574) ->
     229  h_Scall dest f x_25578 en __ __ k __ x_25574
     230    (stack_rect_Type4 h_SStop h_Scall x_25574)
    231231
    232232(** val stack_rect_Type3 :
     
    236236let rec stack_rect_Type3 h_SStop h_Scall = function
    237237| SStop -> h_SStop
    238 | Scall (dest, f, x_25568, en, k, x_25564) ->
    239   h_Scall dest f x_25568 en __ __ k __ x_25564
    240     (stack_rect_Type3 h_SStop h_Scall x_25564)
     238| Scall (dest, f, x_25594, en, k, x_25590) ->
     239  h_Scall dest f x_25594 en __ __ k __ x_25590
     240    (stack_rect_Type3 h_SStop h_Scall x_25590)
    241241
    242242(** val stack_rect_Type2 :
     
    246246let rec stack_rect_Type2 h_SStop h_Scall = function
    247247| SStop -> h_SStop
    248 | Scall (dest, f, x_25576, en, k, x_25572) ->
    249   h_Scall dest f x_25576 en __ __ k __ x_25572
    250     (stack_rect_Type2 h_SStop h_Scall x_25572)
     248| Scall (dest, f, x_25602, en, k, x_25598) ->
     249  h_Scall dest f x_25602 en __ __ k __ x_25598
     250    (stack_rect_Type2 h_SStop h_Scall x_25598)
    251251
    252252(** val stack_rect_Type1 :
     
    256256let rec stack_rect_Type1 h_SStop h_Scall = function
    257257| SStop -> h_SStop
    258 | Scall (dest, f, x_25584, en, k, x_25580) ->
    259   h_Scall dest f x_25584 en __ __ k __ x_25580
    260     (stack_rect_Type1 h_SStop h_Scall x_25580)
     258| Scall (dest, f, x_25610, en, k, x_25606) ->
     259  h_Scall dest f x_25610 en __ __ k __ x_25606
     260    (stack_rect_Type1 h_SStop h_Scall x_25606)
    261261
    262262(** val stack_rect_Type0 :
     
    266266let rec stack_rect_Type0 h_SStop h_Scall = function
    267267| SStop -> h_SStop
    268 | Scall (dest, f, x_25592, en, k, x_25588) ->
    269   h_Scall dest f x_25592 en __ __ k __ x_25588
    270     (stack_rect_Type0 h_SStop h_Scall x_25588)
     268| Scall (dest, f, x_25618, en, k, x_25614) ->
     269  h_Scall dest f x_25618 en __ __ k __ x_25614
     270    (stack_rect_Type0 h_SStop h_Scall x_25614)
    271271
    272272(** val stack_inv_rect_Type4 :
  • extracted/eRTLptrToLTL.ml

    r2873 r2890  
    813813    in
    814814    let move0 = move globals localss carry_lives_after in
    815     (match s with
    816      | Joint.COST_LABEL cost_lbl ->
    817        { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
    818          Joint.COST_LABEL cost_lbl) }; Types.snd = List.Nil }
    819      | Joint.CALL (f, n_args, x) ->
    820        (match f with
    821         | Types.Inl f0 ->
    822           { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
    823             Joint.CALL ((Types.Inl f0), n_args, (Obj.magic Types.It))) };
     815    (match Liveness.eliminable_step globals (after lbl) s with
     816     | Bool.True ->
     817       let x =
     818         Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     819           globals List.Nil
     820       in
     821       x
     822     | Bool.False ->
     823       (match s with
     824        | Joint.COST_LABEL cost_lbl ->
     825          { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
     826            Joint.COST_LABEL cost_lbl) }; Types.snd = List.Nil }
     827        | Joint.CALL (f, n_args, x) ->
     828          (match f with
     829           | Types.Inl f0 ->
     830             { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
     831               Joint.CALL ((Types.Inl f0), n_args, (Obj.magic Types.It))) };
     832               Types.snd = List.Nil }
     833           | Types.Inr dp ->
     834             let { Types.fst = dpl; Types.snd = dph } = dp in
     835             { Types.fst = { Types.fst =
     836             (Blocks.add_dummy_variance
     837               (move_to_dp globals localss (Obj.magic lookup_arg dpl)
     838                 (Obj.magic lookup_arg dph))); Types.snd = (fun x0 ->
     839             Joint.CALL ((Types.Inr { Types.fst = (Obj.magic Types.It);
     840             Types.snd = (Obj.magic Types.It) }), n_args,
     841             (Obj.magic Types.It))) }; Types.snd = List.Nil })
     842        | Joint.COND (r, ltrue) ->
     843          { Types.fst = { Types.fst =
     844            (Blocks.add_dummy_variance
     845              (move0 (Interference.Decision_colour I8051.RegisterA)
     846                (dec_to_arg_dec (Obj.magic lookup r)))); Types.snd =
     847            (fun x -> Joint.COND ((Obj.magic Types.It), ltrue)) };
    824848            Types.snd = List.Nil }
    825         | Types.Inr dp ->
    826           let { Types.fst = dpl; Types.snd = dph } = dp in
    827           { Types.fst = { Types.fst =
    828           (Blocks.add_dummy_variance
    829             (move_to_dp globals localss (Obj.magic lookup_arg dpl)
    830               (Obj.magic lookup_arg dph))); Types.snd = (fun x0 -> Joint.CALL
    831           ((Types.Inr { Types.fst = (Obj.magic Types.It); Types.snd =
    832           (Obj.magic Types.It) }), n_args, (Obj.magic Types.It))) };
    833           Types.snd = List.Nil })
    834      | Joint.COND (r, ltrue) ->
    835        { Types.fst = { Types.fst =
    836          (Blocks.add_dummy_variance
    837            (move0 (Interference.Decision_colour I8051.RegisterA)
    838              (dec_to_arg_dec (Obj.magic lookup r)))); Types.snd = (fun x ->
    839          Joint.COND ((Obj.magic Types.It), ltrue)) }; Types.snd = List.Nil }
    840      | Joint.Step_seq s' ->
    841        (match s' with
    842         | Joint.COMMENT c ->
    843           Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    844             globals (List.Cons ((Joint.COMMENT c), List.Nil))
    845         | Joint.MOVE pair_regs ->
    846           let lookup_move_dst = fun x ->
    847             match x with
    848             | ERTL.PSD r -> lookup r
    849             | ERTL.HDW r -> Interference.Decision_colour r
    850           in
    851           let dst = lookup_move_dst (Obj.magic pair_regs).Types.fst in
    852           let src =
    853             match (Obj.magic pair_regs).Types.snd with
    854             | Joint.Reg r -> dec_to_arg_dec (lookup_move_dst r)
    855             | Joint.Imm b -> Arg_decision_imm b
    856           in
    857           Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    858             globals (move0 dst src)
    859         | Joint.POP r ->
    860           Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    861             globals (List.Cons ((Joint.POP (Obj.magic a)),
    862             (move0 (Obj.magic lookup r) (Arg_decision_colour
    863               I8051.RegisterA))))
    864         | Joint.PUSH a0 ->
    865           Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    866             globals
    867             (List.append
    868               (move0 (Interference.Decision_colour I8051.RegisterA)
    869                 (Obj.magic lookup_arg a0)) (List.Cons ((Joint.PUSH
    870               (Obj.magic a)), List.Nil)))
    871         | Joint.ADDRESS (lbl0, dpl, dph) ->
    872           Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    873             globals
    874             (translate_address (Obj.magic globals) localss carry_lives_after
    875               (Obj.magic lbl0) (Obj.magic lookup dpl) (Obj.magic lookup dph))
    876         | Joint.OPACCS (op, dst1, dst2, arg1, arg2) ->
    877           Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    878             globals
    879             (translate_opaccs globals localss carry_lives_after op
    880               (Obj.magic lookup dst1) (Obj.magic lookup dst2)
    881               (Obj.magic lookup_arg arg1) (Obj.magic lookup_arg arg2))
    882         | Joint.OP1 (op, dst, arg) ->
    883           Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    884             globals
    885             (translate_op1 globals localss carry_lives_after op
    886               (Obj.magic lookup dst) (Obj.magic lookup arg))
    887         | Joint.OP2 (op, dst, arg1, arg2) ->
    888           Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    889             globals
    890             (translate_op2_smart globals localss carry_lives_after op
    891               (Obj.magic lookup dst) (Obj.magic lookup_arg arg1)
    892               (Obj.magic lookup_arg arg2))
    893         | Joint.CLEAR_CARRY ->
    894           Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    895             globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
    896         | Joint.SET_CARRY ->
    897           Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    898             globals (List.Cons (Joint.SET_CARRY, List.Nil))
    899         | Joint.LOAD (dstr, addr1, addr2) ->
    900           Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    901             globals
    902             (translate_load globals localss carry_lives_after
    903               (Obj.magic lookup dstr) (Obj.magic lookup_arg addr1)
    904               (Obj.magic lookup_arg addr2))
    905         | Joint.STORE (addr1, addr2, srcr) ->
    906           Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    907             globals
    908             (translate_store globals localss carry_lives_after
    909               (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2)
    910               (Obj.magic lookup_arg srcr))
    911         | Joint.Extension_seq ext ->
    912           Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    913             globals
    914             (match Obj.magic ext with
    915              | ERTLptr.Ertlptr_ertl ext' ->
    916                (match ext' with
    917                 | ERTL.Ertl_new_frame -> newframe globals stack_sz
    918                 | ERTL.Ertl_del_frame -> delframe globals stack_sz
    919                 | ERTL.Ertl_frame_size r ->
    920                   move0 (lookup r) (Arg_decision_imm
    921                     (Joint.byte_of_nat stack_sz)))
    922              | ERTLptr.LOW_ADDRESS (r1, l) ->
    923                translate_low_address globals localss carry_lives_after
    924                  (lookup r1) l
    925              | ERTLptr.HIGH_ADDRESS (r1, l) ->
    926                translate_high_address globals localss carry_lives_after
    927                  (lookup r1) l))))
     849        | Joint.Step_seq s' ->
     850          (match s' with
     851           | Joint.COMMENT c ->
     852             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     853               globals (List.Cons ((Joint.COMMENT c), List.Nil))
     854           | Joint.MOVE pair_regs ->
     855             let lookup_move_dst = fun x ->
     856               match x with
     857               | ERTL.PSD r -> lookup r
     858               | ERTL.HDW r -> Interference.Decision_colour r
     859             in
     860             let dst = lookup_move_dst (Obj.magic pair_regs).Types.fst in
     861             let src =
     862               match (Obj.magic pair_regs).Types.snd with
     863               | Joint.Reg r -> dec_to_arg_dec (lookup_move_dst r)
     864               | Joint.Imm b -> Arg_decision_imm b
     865             in
     866             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     867               globals (move0 dst src)
     868           | Joint.POP r ->
     869             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     870               globals (List.Cons ((Joint.POP (Obj.magic a)),
     871               (move0 (Obj.magic lookup r) (Arg_decision_colour
     872                 I8051.RegisterA))))
     873           | Joint.PUSH a0 ->
     874             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     875               globals
     876               (List.append
     877                 (move0 (Interference.Decision_colour I8051.RegisterA)
     878                   (Obj.magic lookup_arg a0)) (List.Cons ((Joint.PUSH
     879                 (Obj.magic a)), List.Nil)))
     880           | Joint.ADDRESS (lbl0, dpl, dph) ->
     881             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     882               globals
     883               (translate_address (Obj.magic globals) localss
     884                 carry_lives_after (Obj.magic lbl0) (Obj.magic lookup dpl)
     885                 (Obj.magic lookup dph))
     886           | Joint.OPACCS (op, dst1, dst2, arg1, arg2) ->
     887             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     888               globals
     889               (translate_opaccs globals localss carry_lives_after op
     890                 (Obj.magic lookup dst1) (Obj.magic lookup dst2)
     891                 (Obj.magic lookup_arg arg1) (Obj.magic lookup_arg arg2))
     892           | Joint.OP1 (op, dst, arg) ->
     893             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     894               globals
     895               (translate_op1 globals localss carry_lives_after op
     896                 (Obj.magic lookup dst) (Obj.magic lookup arg))
     897           | Joint.OP2 (op, dst, arg1, arg2) ->
     898             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     899               globals
     900               (translate_op2_smart globals localss carry_lives_after op
     901                 (Obj.magic lookup dst) (Obj.magic lookup_arg arg1)
     902                 (Obj.magic lookup_arg arg2))
     903           | Joint.CLEAR_CARRY ->
     904             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     905               globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
     906           | Joint.SET_CARRY ->
     907             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     908               globals (List.Cons (Joint.SET_CARRY, List.Nil))
     909           | Joint.LOAD (dstr, addr1, addr2) ->
     910             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     911               globals
     912               (translate_load globals localss carry_lives_after
     913                 (Obj.magic lookup dstr) (Obj.magic lookup_arg addr1)
     914                 (Obj.magic lookup_arg addr2))
     915           | Joint.STORE (addr1, addr2, srcr) ->
     916             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     917               globals
     918               (translate_store globals localss carry_lives_after
     919                 (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2)
     920                 (Obj.magic lookup_arg srcr))
     921           | Joint.Extension_seq ext ->
     922             Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     923               globals
     924               (match Obj.magic ext with
     925                | ERTLptr.Ertlptr_ertl ext' ->
     926                  (match ext' with
     927                   | ERTL.Ertl_new_frame -> newframe globals stack_sz
     928                   | ERTL.Ertl_del_frame -> delframe globals stack_sz
     929                   | ERTL.Ertl_frame_size r ->
     930                     move0 (lookup r) (Arg_decision_imm
     931                       (Joint.byte_of_nat stack_sz)))
     932                | ERTLptr.LOW_ADDRESS (r1, l) ->
     933                  translate_low_address globals localss carry_lives_after
     934                    (lookup r1) l
     935                | ERTLptr.HIGH_ADDRESS (r1, l) ->
     936                  translate_high_address globals localss carry_lives_after
     937                    (lookup r1) l)))))
    928938
    929939(** val translate_fin_step :
  • extracted/fetch.ml

    r2873 r2890  
    9898  (Types.pi1
    9999    (FoldStuff.foldl_strong program (fun prefix x tl _ labels_costs_ppc ->
    100       (let { Types.fst = eta29124; Types.snd = ppc } =
     100      (let { Types.fst = eta29136; Types.snd = ppc } =
    101101         Types.pi1 labels_costs_ppc
    102102       in
    103103      (fun _ ->
    104       (let { Types.fst = labels; Types.snd = costs } = eta29124 in
     104      (let { Types.fst = labels; Types.snd = costs } = eta29136 in
    105105      (fun _ ->
    106106      (let { Types.fst = label; Types.snd = instr } = x in
  • extracted/joint_fullexec.ml

    r2873 r2890  
    149149    Joint_semantics.sem_params -> (AST.ident List.list ->
    150150    Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    151 let rec joint_global_rect_Type4 p h_mk_joint_global x_26113 =
    152   let { jglobals = jglobals0; jgenv = jgenv0 } = x_26113 in
     151let rec joint_global_rect_Type4 p h_mk_joint_global x_26139 =
     152  let { jglobals = jglobals0; jgenv = jgenv0 } = x_26139 in
    153153  h_mk_joint_global jglobals0 jgenv0
    154154
     
    156156    Joint_semantics.sem_params -> (AST.ident List.list ->
    157157    Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    158 let rec joint_global_rect_Type5 p h_mk_joint_global x_26115 =
    159   let { jglobals = jglobals0; jgenv = jgenv0 } = x_26115 in
     158let rec joint_global_rect_Type5 p h_mk_joint_global x_26141 =
     159  let { jglobals = jglobals0; jgenv = jgenv0 } = x_26141 in
    160160  h_mk_joint_global jglobals0 jgenv0
    161161
     
    163163    Joint_semantics.sem_params -> (AST.ident List.list ->
    164164    Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    165 let rec joint_global_rect_Type3 p h_mk_joint_global x_26117 =
    166   let { jglobals = jglobals0; jgenv = jgenv0 } = x_26117 in
     165let rec joint_global_rect_Type3 p h_mk_joint_global x_26143 =
     166  let { jglobals = jglobals0; jgenv = jgenv0 } = x_26143 in
    167167  h_mk_joint_global jglobals0 jgenv0
    168168
     
    170170    Joint_semantics.sem_params -> (AST.ident List.list ->
    171171    Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    172 let rec joint_global_rect_Type2 p h_mk_joint_global x_26119 =
    173   let { jglobals = jglobals0; jgenv = jgenv0 } = x_26119 in
     172let rec joint_global_rect_Type2 p h_mk_joint_global x_26145 =
     173  let { jglobals = jglobals0; jgenv = jgenv0 } = x_26145 in
    174174  h_mk_joint_global jglobals0 jgenv0
    175175
     
    177177    Joint_semantics.sem_params -> (AST.ident List.list ->
    178178    Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    179 let rec joint_global_rect_Type1 p h_mk_joint_global x_26121 =
    180   let { jglobals = jglobals0; jgenv = jgenv0 } = x_26121 in
     179let rec joint_global_rect_Type1 p h_mk_joint_global x_26147 =
     180  let { jglobals = jglobals0; jgenv = jgenv0 } = x_26147 in
    181181  h_mk_joint_global jglobals0 jgenv0
    182182
     
    184184    Joint_semantics.sem_params -> (AST.ident List.list ->
    185185    Joint_semantics.genv -> 'a1) -> joint_global -> 'a1 **)
    186 let rec joint_global_rect_Type0 p h_mk_joint_global x_26123 =
    187   let { jglobals = jglobals0; jgenv = jgenv0 } = x_26123 in
     186let rec joint_global_rect_Type0 p h_mk_joint_global x_26149 =
     187  let { jglobals = jglobals0; jgenv = jgenv0 } = x_26149 in
    188188  h_mk_joint_global jglobals0 jgenv0
    189189
  • extracted/joint_semantics.ml

    r2882 r2890  
    141141    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    142142    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    143 let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_3 =
     143let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_25736 =
    144144  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    145     get_pc_from_label0 } = x_3
     145    get_pc_from_label0 } = x_25736
    146146  in
    147147  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     
    151151    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    152152    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    153 let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_5 =
     153let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_25738 =
    154154  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    155     get_pc_from_label0 } = x_5
     155    get_pc_from_label0 } = x_25738
    156156  in
    157157  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     
    161161    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    162162    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    163 let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_7 =
     163let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_25740 =
    164164  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    165     get_pc_from_label0 } = x_7
     165    get_pc_from_label0 } = x_25740
    166166  in
    167167  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     
    171171    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    172172    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    173 let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_9 =
     173let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_25742 =
    174174  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    175     get_pc_from_label0 } = x_9
     175    get_pc_from_label0 } = x_25742
    176176  in
    177177  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     
    181181    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    182182    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    183 let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_11 =
     183let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_25744 =
    184184  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    185     get_pc_from_label0 } = x_11
     185    get_pc_from_label0 } = x_25744
    186186  in
    187187  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     
    191191    (AST.ident -> Nat.nat Types.option) -> (AST.ident -> Graphs.label ->
    192192    ByteValues.program_counter Errors.res) -> 'a2) -> 'a1 genv_gen -> 'a2 **)
    193 let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_13 =
     193let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_25746 =
    194194  let { ge = ge0; stack_sizes = stack_sizes0; get_pc_from_label =
    195     get_pc_from_label0 } = x_13
     195    get_pc_from_label0 } = x_25746
    196196  in
    197197  h_mk_genv_gen ge0 __ stack_sizes0 get_pc_from_label0
     
    341341    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    342342    'a1) -> sem_state_params -> 'a1 **)
    343 let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_33 =
     343let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_25766 =
    344344  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    345     load_sp0; save_sp = save_sp0 } = x_33
     345    load_sp0; save_sp = save_sp0 } = x_25766
    346346  in
    347347  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    351351    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    352352    'a1) -> sem_state_params -> 'a1 **)
    353 let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_35 =
     353let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_25768 =
    354354  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    355     load_sp0; save_sp = save_sp0 } = x_35
     355    load_sp0; save_sp = save_sp0 } = x_25768
    356356  in
    357357  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    361361    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    362362    'a1) -> sem_state_params -> 'a1 **)
    363 let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_37 =
     363let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_25770 =
    364364  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    365     load_sp0; save_sp = save_sp0 } = x_37
     365    load_sp0; save_sp = save_sp0 } = x_25770
    366366  in
    367367  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    371371    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    372372    'a1) -> sem_state_params -> 'a1 **)
    373 let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_39 =
     373let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_25772 =
    374374  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    375     load_sp0; save_sp = save_sp0 } = x_39
     375    load_sp0; save_sp = save_sp0 } = x_25772
    376376  in
    377377  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    381381    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    382382    'a1) -> sem_state_params -> 'a1 **)
    383 let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_41 =
     383let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_25774 =
    384384  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    385     load_sp0; save_sp = save_sp0 } = x_41
     385    load_sp0; save_sp = save_sp0 } = x_25774
    386386  in
    387387  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    391391    ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) ->
    392392    'a1) -> sem_state_params -> 'a1 **)
    393 let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_43 =
     393let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_25776 =
    394394  let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp =
    395     load_sp0; save_sp = save_sp0 } = x_43
     395    load_sp0; save_sp = save_sp0 } = x_25776
    396396  in
    397397  h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0
     
    472472let rec internal_stack_rect_Type4 h_empty_is h_one_is h_both_is = function
    473473| Empty_is -> h_empty_is
    474 | One_is x_69 -> h_one_is x_69
    475 | Both_is (x_71, x_70) -> h_both_is x_71 x_70
     474| One_is x_25802 -> h_one_is x_25802
     475| Both_is (x_25804, x_25803) -> h_both_is x_25804 x_25803
    476476
    477477(** val internal_stack_rect_Type5 :
     
    480480let rec internal_stack_rect_Type5 h_empty_is h_one_is h_both_is = function
    481481| Empty_is -> h_empty_is
    482 | One_is x_76 -> h_one_is x_76
    483 | Both_is (x_78, x_77) -> h_both_is x_78 x_77
     482| One_is x_25809 -> h_one_is x_25809
     483| Both_is (x_25811, x_25810) -> h_both_is x_25811 x_25810
    484484
    485485(** val internal_stack_rect_Type3 :
     
    488488let rec internal_stack_rect_Type3 h_empty_is h_one_is h_both_is = function
    489489| Empty_is -> h_empty_is
    490 | One_is x_83 -> h_one_is x_83
    491 | Both_is (x_85, x_84) -> h_both_is x_85 x_84
     490| One_is x_25816 -> h_one_is x_25816
     491| Both_is (x_25818, x_25817) -> h_both_is x_25818 x_25817
    492492
    493493(** val internal_stack_rect_Type2 :
     
    496496let rec internal_stack_rect_Type2 h_empty_is h_one_is h_both_is = function
    497497| Empty_is -> h_empty_is
    498 | One_is x_90 -> h_one_is x_90
    499 | Both_is (x_92, x_91) -> h_both_is x_92 x_91
     498| One_is x_25823 -> h_one_is x_25823
     499| Both_is (x_25825, x_25824) -> h_both_is x_25825 x_25824
    500500
    501501(** val internal_stack_rect_Type1 :
     
    504504let rec internal_stack_rect_Type1 h_empty_is h_one_is h_both_is = function
    505505| Empty_is -> h_empty_is
    506 | One_is x_97 -> h_one_is x_97
    507 | Both_is (x_99, x_98) -> h_both_is x_99 x_98
     506| One_is x_25830 -> h_one_is x_25830
     507| Both_is (x_25832, x_25831) -> h_both_is x_25832 x_25831
    508508
    509509(** val internal_stack_rect_Type0 :
     
    512512let rec internal_stack_rect_Type0 h_empty_is h_one_is h_both_is = function
    513513| Empty_is -> h_empty_is
    514 | One_is x_104 -> h_one_is x_104
    515 | Both_is (x_106, x_105) -> h_both_is x_106 x_105
     514| One_is x_25837 -> h_one_is x_25837
     515| Both_is (x_25839, x_25838) -> h_both_is x_25839 x_25838
    516516
    517517(** val internal_stack_inv_rect_Type4 :
     
    596596    sem_state_params -> (__ Types.option -> internal_stack ->
    597597    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    598 let rec state_rect_Type4 semp h_mk_state x_154 =
     598let rec state_rect_Type4 semp h_mk_state x_25887 =
    599599  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    600     m = m0 } = x_154
     600    m = m0 } = x_25887
    601601  in
    602602  h_mk_state st_frms0 istack0 carry0 regs0 m0
     
    605605    sem_state_params -> (__ Types.option -> internal_stack ->
    606606    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    607 let rec state_rect_Type5 semp h_mk_state x_156 =
     607let rec state_rect_Type5 semp h_mk_state x_25889 =
    608608  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    609     m = m0 } = x_156
     609    m = m0 } = x_25889
    610610  in
    611611  h_mk_state st_frms0 istack0 carry0 regs0 m0
     
    614614    sem_state_params -> (__ Types.option -> internal_stack ->
    615615    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    616 let rec state_rect_Type3 semp h_mk_state x_158 =
     616let rec state_rect_Type3 semp h_mk_state x_25891 =
    617617  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    618     m = m0 } = x_158
     618    m = m0 } = x_25891
    619619  in
    620620  h_mk_state st_frms0 istack0 carry0 regs0 m0
     
    623623    sem_state_params -> (__ Types.option -> internal_stack ->
    624624    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    625 let rec state_rect_Type2 semp h_mk_state x_160 =
     625let rec state_rect_Type2 semp h_mk_state x_25893 =
    626626  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    627     m = m0 } = x_160
     627    m = m0 } = x_25893
    628628  in
    629629  h_mk_state st_frms0 istack0 carry0 regs0 m0
     
    632632    sem_state_params -> (__ Types.option -> internal_stack ->
    633633    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    634 let rec state_rect_Type1 semp h_mk_state x_162 =
     634let rec state_rect_Type1 semp h_mk_state x_25895 =
    635635  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    636     m = m0 } = x_162
     636    m = m0 } = x_25895
    637637  in
    638638  h_mk_state st_frms0 istack0 carry0 regs0 m0
     
    641641    sem_state_params -> (__ Types.option -> internal_stack ->
    642642    ByteValues.bebit -> __ -> BEMem.bemem -> 'a1) -> state -> 'a1 **)
    643 let rec state_rect_Type0 semp h_mk_state x_164 =
     643let rec state_rect_Type0 semp h_mk_state x_25897 =
    644644  let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0;
    645     m = m0 } = x_164
     645    m = m0 } = x_25897
    646646  in
    647647  h_mk_state st_frms0 istack0 carry0 regs0 m0
     
    719719    sem_state_params -> (state -> ByteValues.program_counter ->
    720720    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    721 let rec state_pc_rect_Type4 semp h_mk_state_pc x_180 =
    722   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_180 in
     721let rec state_pc_rect_Type4 semp h_mk_state_pc x_25913 =
     722  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25913 in
    723723  h_mk_state_pc st_no_pc0 pc0 last_pop0
    724724
     
    726726    sem_state_params -> (state -> ByteValues.program_counter ->
    727727    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    728 let rec state_pc_rect_Type5 semp h_mk_state_pc x_182 =
    729   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_182 in
     728let rec state_pc_rect_Type5 semp h_mk_state_pc x_25915 =
     729  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25915 in
    730730  h_mk_state_pc st_no_pc0 pc0 last_pop0
    731731
     
    733733    sem_state_params -> (state -> ByteValues.program_counter ->
    734734    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    735 let rec state_pc_rect_Type3 semp h_mk_state_pc x_184 =
    736   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_184 in
     735let rec state_pc_rect_Type3 semp h_mk_state_pc x_25917 =
     736  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25917 in
    737737  h_mk_state_pc st_no_pc0 pc0 last_pop0
    738738
     
    740740    sem_state_params -> (state -> ByteValues.program_counter ->
    741741    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    742 let rec state_pc_rect_Type2 semp h_mk_state_pc x_186 =
    743   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_186 in
     742let rec state_pc_rect_Type2 semp h_mk_state_pc x_25919 =
     743  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25919 in
    744744  h_mk_state_pc st_no_pc0 pc0 last_pop0
    745745
     
    747747    sem_state_params -> (state -> ByteValues.program_counter ->
    748748    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    749 let rec state_pc_rect_Type1 semp h_mk_state_pc x_188 =
    750   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_188 in
     749let rec state_pc_rect_Type1 semp h_mk_state_pc x_25921 =
     750  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25921 in
    751751  h_mk_state_pc st_no_pc0 pc0 last_pop0
    752752
     
    754754    sem_state_params -> (state -> ByteValues.program_counter ->
    755755    ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **)
    756 let rec state_pc_rect_Type0 semp h_mk_state_pc x_190 =
    757   let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_190 in
     756let rec state_pc_rect_Type0 semp h_mk_state_pc x_25923 =
     757  let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_25923 in
    758758  h_mk_state_pc st_no_pc0 pc0 last_pop0
    759759
     
    10941094    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    10951095    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1096 let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_245 =
     1096let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_25978 =
    10971097  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    10981098    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    11061106    set_result0; call_args_for_main = call_args_for_main0;
    11071107    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1108     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_245
     1108    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25978
    11091109  in
    11101110  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    11351135    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    11361136    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1137 let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_247 =
     1137let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_25980 =
    11381138  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    11391139    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    11471147    set_result0; call_args_for_main = call_args_for_main0;
    11481148    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1149     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_247
     1149    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25980
    11501150  in
    11511151  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    11761176    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    11771177    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1178 let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_249 =
     1178let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_25982 =
    11791179  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    11801180    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    11881188    set_result0; call_args_for_main = call_args_for_main0;
    11891189    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1190     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_249
     1190    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25982
    11911191  in
    11921192  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    12171217    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    12181218    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1219 let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_251 =
     1219let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_25984 =
    12201220  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    12211221    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    12291229    set_result0; call_args_for_main = call_args_for_main0;
    12301230    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1231     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_251
     1231    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25984
    12321232  in
    12331233  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    12581258    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    12591259    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1260 let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_253 =
     1260let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_25986 =
    12611261  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    12621262    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    12701270    set_result0; call_args_for_main = call_args_for_main0;
    12711271    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1272     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_253
     1272    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25986
    12731273  in
    12741274  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    12991299    state -> (state, ByteValues.program_counter) Types.prod Errors.res) ->
    13001300    'a2) -> 'a1 sem_unserialized_params -> 'a2 **)
    1301 let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_255 =
     1301let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_25988 =
    13021302  let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ =
    13031303    acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ =
     
    13111311    set_result0; call_args_for_main = call_args_for_main0;
    13121312    call_dest_for_main = call_dest_for_main0; read_result = read_result0;
    1313     eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_255
     1313    eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_25988
    13141314  in
    13151315  h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0
     
    17611761    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17621762    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1763 let rec sem_params_rect_Type4 h_mk_sem_params x_325 =
     1763let rec sem_params_rect_Type4 h_mk_sem_params x_26058 =
    17641764  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1765     point_of_offset = point_of_offset0 } = x_325
     1765    point_of_offset = point_of_offset0 } = x_26058
    17661766  in
    17671767  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
     
    17711771    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17721772    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1773 let rec sem_params_rect_Type5 h_mk_sem_params x_327 =
     1773let rec sem_params_rect_Type5 h_mk_sem_params x_26060 =
    17741774  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1775     point_of_offset = point_of_offset0 } = x_327
     1775    point_of_offset = point_of_offset0 } = x_26060
    17761776  in
    17771777  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
     
    17811781    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17821782    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1783 let rec sem_params_rect_Type3 h_mk_sem_params x_329 =
     1783let rec sem_params_rect_Type3 h_mk_sem_params x_26062 =
    17841784  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1785     point_of_offset = point_of_offset0 } = x_329
     1785    point_of_offset = point_of_offset0 } = x_26062
    17861786  in
    17871787  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
     
    17911791    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    17921792    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1793 let rec sem_params_rect_Type2 h_mk_sem_params x_331 =
     1793let rec sem_params_rect_Type2 h_mk_sem_params x_26064 =
    17941794  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1795     point_of_offset = point_of_offset0 } = x_331
     1795    point_of_offset = point_of_offset0 } = x_26064
    17961796  in
    17971797  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
     
    18011801    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    18021802    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1803 let rec sem_params_rect_Type1 h_mk_sem_params x_333 =
     1803let rec sem_params_rect_Type1 h_mk_sem_params x_26066 =
    18041804  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1805     point_of_offset = point_of_offset0 } = x_333
     1805    point_of_offset = point_of_offset0 } = x_26066
    18061806  in
    18071807  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
     
    18111811    sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __)
    18121812    -> __ -> __ -> 'a1) -> sem_params -> 'a1 **)
    1813 let rec sem_params_rect_Type0 h_mk_sem_params x_335 =
     1813let rec sem_params_rect_Type0 h_mk_sem_params x_26068 =
    18141814  let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0;
    1815     point_of_offset = point_of_offset0 } = x_335
     1815    point_of_offset = point_of_offset0 } = x_26068
    18161816  in
    18171817  h_mk_sem_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __
  • extracted/lINToASM.ml

    r2873 r2890  
    280280  let globals_addr_internal = fun res_offset x_size ->
    281281    let { Types.fst = res; Types.snd = offset } = res_offset in
    282     let { Types.fst = eta29074; Types.snd = size } = x_size in
    283     let { Types.fst = x; Types.snd = region } = eta29074 in
     282    let { Types.fst = eta29086; Types.snd = size } = x_size in
     283    let { Types.fst = x; Types.snd = region } = eta29086 in
    284284    { Types.fst =
    285285    (Identifiers.add PreIdentifiers.SymbolTag res x
     
    309309        (Identifiers.empty_map PreIdentifiers.LabelTag)
    310310    in
    311     let { Types.fst = eta29075; Types.snd = lmap0 } =
     311    let { Types.fst = eta29087; Types.snd = lmap0 } =
    312312      match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
    313313      | Types.None ->
     
    321321          lmap }
    322322    in
    323     let { Types.fst = id; Types.snd = univ } = eta29075 in
     323    let { Types.fst = id; Types.snd = univ } = eta29087 in
    324324    { Types.fst = { id_univ = univ; current_funct = current; ident_map =
    325325    u.ident_map; label_map =
     
    333333  Obj.magic (fun u ->
    334334    let imap = u.ident_map in
    335     let { Types.fst = eta29076; Types.snd = imap0 } =
     335    let { Types.fst = eta29088; Types.snd = imap0 } =
    336336      match Identifiers.lookup PreIdentifiers.SymbolTag imap i with
    337337      | Types.None ->
     
    345345          imap }
    346346    in
    347     let { Types.fst = id; Types.snd = univ } = eta29076 in
     347    let { Types.fst = id; Types.snd = univ } = eta29088 in
    348348    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
    349349    ident_map = imap0; label_map = u.label_map; address_map =
  • extracted/liveness.ml

    r2773 r2890  
    147147    (Set_adt.set_singleton r) }
    148148
     149(** val pairwise :
     150    ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a2 -> 'a2) -> ('a1, 'a2) Types.prod ->
     151    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod **)
     152let pairwise f g c1 c2 =
     153  { Types.fst = (f c1.Types.fst c2.Types.fst); Types.snd =
     154    (g c1.Types.snd c2.Types.snd) }
     155
    149156(** val rl_join : __ -> __ -> __ **)
    150 let rl_join left right =
    151   let { Types.fst = lp; Types.snd = lh } = Obj.magic left in
    152   let { Types.fst = rp; Types.snd = rh } = Obj.magic right in
    153   Obj.magic { Types.fst = (Set_adt.set_union lp rp); Types.snd =
    154     (Set_adt.set_union lh rh) }
     157let rl_join =
     158  Obj.magic (pairwise Set_adt.set_union Set_adt.set_union)
    155159
    156160(** val rl_diff : __ -> __ -> __ **)
    157 let rl_diff left right =
    158   let { Types.fst = lp; Types.snd = lh } = Obj.magic left in
    159   let { Types.fst = rp; Types.snd = rh } = Obj.magic right in
    160   Obj.magic { Types.fst = (Set_adt.set_diff lp rp); Types.snd =
    161     (Set_adt.set_diff lh rh) }
     161let rl_diff =
     162  Obj.magic (pairwise Set_adt.set_diff Set_adt.set_diff)
    162163
    163164(** val defined : AST.ident List.list -> Joint.joint_statement -> __ **)
     
    303304| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
    304305
     306(** val eliminable_step :
     307    AST.ident List.list -> __ -> Joint.joint_step -> Bool.bool **)
     308let eliminable_step globals l s =
     309  let pliveafter = (Obj.magic l).Types.fst in
     310  let hliveafter = (Obj.magic l).Types.snd in
     311  (match s with
     312   | Joint.COST_LABEL x -> Bool.False
     313   | Joint.CALL (x, x0, x1) -> Bool.False
     314   | Joint.COND (x, x0) -> Bool.False
     315   | Joint.Step_seq s0 ->
     316     (match s0 with
     317      | Joint.COMMENT x -> Bool.False
     318      | Joint.MOVE pair_reg ->
     319        Bool.notb
     320          (match (Obj.magic pair_reg).Types.fst with
     321           | ERTL.PSD p1 ->
     322             Set_adt.set_member
     323               (Identifiers.eq_identifier PreIdentifiers.RegisterTag) p1
     324               pliveafter
     325           | ERTL.HDW h1 ->
     326             Set_adt.set_member I8051.eq_Register h1 hliveafter)
     327      | Joint.POP x -> Bool.False
     328      | Joint.PUSH x -> Bool.False
     329      | Joint.ADDRESS (x, r1, r2) ->
     330        Bool.notb
     331          (Bool.orb
     332            (Set_adt.set_member
     333              (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
     334              (Obj.magic r1) pliveafter)
     335            (Set_adt.set_member
     336              (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
     337              (Obj.magic r2) pliveafter))
     338      | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
     339        Bool.notb
     340          (Bool.orb
     341            (Bool.orb
     342              (Set_adt.set_member
     343                (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
     344                (Obj.magic dr1) pliveafter)
     345              (Set_adt.set_member
     346                (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
     347                (Obj.magic dr2) pliveafter))
     348            (Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
     349              hliveafter))
     350      | Joint.OP1 (op1, r1, r2) ->
     351        Bool.notb
     352          (Set_adt.set_member
     353            (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
     354            (Obj.magic r1) pliveafter)
     355      | Joint.OP2 (op2, r1, r2, r3) ->
     356        Bool.notb
     357          (Bool.orb
     358            (match op2 with
     359             | BackEndOps.Add ->
     360               Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
     361                 hliveafter
     362             | BackEndOps.Addc ->
     363               Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
     364                 hliveafter
     365             | BackEndOps.Sub ->
     366               Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
     367                 hliveafter
     368             | BackEndOps.And -> Bool.False
     369             | BackEndOps.Or -> Bool.False
     370             | BackEndOps.Xor -> Bool.False)
     371            (Set_adt.set_member
     372              (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
     373              (Obj.magic r1) pliveafter))
     374      | Joint.CLEAR_CARRY -> Bool.False
     375      | Joint.SET_CARRY -> Bool.False
     376      | Joint.LOAD (acc_a, dpl, dph) ->
     377        Bool.notb
     378          (Set_adt.set_member
     379            (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
     380            (Obj.magic acc_a) pliveafter)
     381      | Joint.STORE (x, x0, x1) -> Bool.False
     382      | Joint.Extension_seq ext ->
     383        (match Obj.magic ext with
     384         | ERTLptr.Ertlptr_ertl ext' ->
     385           (match ext' with
     386            | ERTL.Ertl_new_frame -> Bool.False
     387            | ERTL.Ertl_del_frame -> Bool.False
     388            | ERTL.Ertl_frame_size r ->
     389              Bool.notb
     390                (Set_adt.set_member
     391                  (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r
     392                  pliveafter))
     393         | ERTLptr.LOW_ADDRESS (r1, l') ->
     394           Bool.notb
     395             (Set_adt.set_member
     396               (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r1
     397               pliveafter)
     398         | ERTLptr.HIGH_ADDRESS (r1, l') ->
     399           Bool.notb
     400             (Set_adt.set_member
     401               (Identifiers.eq_identifier PreIdentifiers.RegisterTag) r1
     402               pliveafter))))
     403
    305404(** val eliminable :
    306     AST.ident List.list -> __ -> Joint.joint_statement -> __ Types.option **)
     405    AST.ident List.list -> __ -> Joint.joint_statement -> Bool.bool **)
    307406let eliminable globals l s =
    308407  let pliveafter = (Obj.magic l).Types.fst in
    309408  let hliveafter = (Obj.magic l).Types.snd in
    310409  (match s with
    311    | Joint.Sequential (seq, l0) ->
    312      (match seq with
    313       | Joint.COST_LABEL x -> Types.None
    314       | Joint.CALL (x, x0, x1) -> Types.None
    315       | Joint.COND (x, x0) -> Types.None
    316       | Joint.Step_seq s0 ->
    317         (match s0 with
    318          | Joint.COMMENT x -> Types.None
    319          | Joint.MOVE pair_reg ->
    320            (match match (Obj.magic pair_reg).Types.fst with
    321                   | ERTL.PSD p1 ->
    322                     Set_adt.set_member
    323                       (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
    324                       p1 pliveafter
    325                   | ERTL.HDW h1 ->
    326                     Set_adt.set_member I8051.eq_Register h1 hliveafter with
    327             | Bool.True -> Types.None
    328             | Bool.False -> Types.Some l0)
    329          | Joint.POP x -> Types.None
    330          | Joint.PUSH x -> Types.None
    331          | Joint.ADDRESS (x, r1, r2) ->
    332            (match Bool.orb
    333                     (Set_adt.set_member
    334                       (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
    335                       (Obj.magic r1) pliveafter)
    336                     (Set_adt.set_member
    337                       (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
    338                       (Obj.magic r2) pliveafter) with
    339             | Bool.True -> Types.None
    340             | Bool.False -> Types.Some l0)
    341          | Joint.OPACCS (opaccs, dr1, dr2, sr1, sr2) ->
    342            (match Bool.orb
    343                     (Bool.orb
    344                       (Set_adt.set_member
    345                         (Identifiers.eq_identifier
    346                           PreIdentifiers.RegisterTag) (Obj.magic dr1)
    347                         pliveafter)
    348                       (Set_adt.set_member
    349                         (Identifiers.eq_identifier
    350                           PreIdentifiers.RegisterTag) (Obj.magic dr2)
    351                         pliveafter))
    352                     (Set_adt.set_member I8051.eq_Register I8051.RegisterCarry
    353                       hliveafter) with
    354             | Bool.True -> Types.None
    355             | Bool.False -> Types.Some l0)
    356          | Joint.OP1 (op1, r1, r2) ->
    357            (match Set_adt.set_member
    358                     (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
    359                     (Obj.magic r1) pliveafter with
    360             | Bool.True -> Types.None
    361             | Bool.False -> Types.Some l0)
    362          | Joint.OP2 (op2, r1, r2, r3) ->
    363            (match Bool.orb
    364                     (match op2 with
    365                      | BackEndOps.Add ->
    366                        Set_adt.set_member I8051.eq_Register
    367                          I8051.RegisterCarry hliveafter
    368                      | BackEndOps.Addc ->
    369                        Set_adt.set_member I8051.eq_Register
    370                          I8051.RegisterCarry hliveafter
    371                      | BackEndOps.Sub ->
    372                        Set_adt.set_member I8051.eq_Register
    373                          I8051.RegisterCarry hliveafter
    374                      | BackEndOps.And -> Bool.False
    375                      | BackEndOps.Or -> Bool.False
    376                      | BackEndOps.Xor -> Bool.False)
    377                     (Set_adt.set_member
    378                       (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
    379                       (Obj.magic r1) pliveafter) with
    380             | Bool.True -> Types.None
    381             | Bool.False -> Types.Some l0)
    382          | Joint.CLEAR_CARRY -> Types.None
    383          | Joint.SET_CARRY -> Types.None
    384          | Joint.LOAD (acc_a, dpl, dph) ->
    385            (match Set_adt.set_member
    386                     (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
    387                     (Obj.magic acc_a) pliveafter with
    388             | Bool.True -> Types.None
    389             | Bool.False -> Types.Some l0)
    390          | Joint.STORE (x, x0, x1) -> Types.None
    391          | Joint.Extension_seq ext ->
    392            (match Obj.magic ext with
    393             | ERTLptr.Ertlptr_ertl ext' ->
    394               (match ext' with
    395                | ERTL.Ertl_new_frame -> Types.None
    396                | ERTL.Ertl_del_frame -> Types.None
    397                | ERTL.Ertl_frame_size r ->
    398                  (match Set_adt.set_member
    399                           (Identifiers.eq_identifier
    400                             PreIdentifiers.RegisterTag) r pliveafter with
    401                   | Bool.True -> Types.None
    402                   | Bool.False -> Types.Some l0))
    403             | ERTLptr.LOW_ADDRESS (r1, l') ->
    404               (match Set_adt.set_member
    405                        (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
    406                        r1 pliveafter with
    407                | Bool.True -> Types.None
    408                | Bool.False -> Types.Some l0)
    409             | ERTLptr.HIGH_ADDRESS (r1, l') ->
    410               (match Set_adt.set_member
    411                        (Identifiers.eq_identifier PreIdentifiers.RegisterTag)
    412                        r1 pliveafter with
    413                | Bool.True -> Types.None
    414                | Bool.False -> Types.Some l0))))
    415    | Joint.Final x -> Types.None
    416    | Joint.FCOND (x0, x1, x2) -> Types.None)
     410   | Joint.Sequential (seq, x) -> eliminable_step globals l seq
     411   | Joint.Final x -> Bool.False
     412   | Joint.FCOND (x0, x1, x2) -> Bool.False)
    417413
    418414(** val statement_semantics :
     
    420416let statement_semantics globals stmt liveafter =
    421417  match eliminable globals liveafter stmt with
    422   | Types.None ->
     418  | Bool.True -> liveafter
     419  | Bool.False ->
    423420    rl_join (rl_diff liveafter (defined globals stmt))
    424421      (Obj.magic (used globals stmt))
    425   | Types.Some l -> liveafter
    426422
    427423(** val livebefore :
  • extracted/liveness.mli

    r2773 r2890  
    121121val rl_hsingleton : I8051.register -> __
    122122
     123val pairwise :
     124  ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a2 -> 'a2) -> ('a1, 'a2) Types.prod ->
     125  ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod
     126
    123127val rl_join : __ -> __ -> __
    124128
     
    135139  Set_adt.set, I8051.register Set_adt.set) Types.prod
    136140
     141val eliminable_step :
     142  AST.ident List.list -> __ -> Joint.joint_step -> Bool.bool
     143
    137144val eliminable :
    138   AST.ident List.list -> __ -> Joint.joint_statement -> __ Types.option
     145  AST.ident List.list -> __ -> Joint.joint_statement -> Bool.bool
    139146
    140147val statement_semantics :
  • extracted/measurable.ml

    r2873 r2890  
    112112    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
    113113    'a1) -> classified_system -> 'a1 **)
    114 let rec classified_system_rect_Type4 h_mk_classified_system x_25390 =
     114let rec classified_system_rect_Type4 h_mk_classified_system x_25416 =
    115115  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
    116116    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
    117     x_25390
     117    x_25416
    118118  in
    119119  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
     
    124124    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
    125125    'a1) -> classified_system -> 'a1 **)
    126 let rec classified_system_rect_Type5 h_mk_classified_system x_25392 =
     126let rec classified_system_rect_Type5 h_mk_classified_system x_25418 =
    127127  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
    128128    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
    129     x_25392
     129    x_25418
    130130  in
    131131  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
     
    136136    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
    137137    'a1) -> classified_system -> 'a1 **)
    138 let rec classified_system_rect_Type3 h_mk_classified_system x_25394 =
     138let rec classified_system_rect_Type3 h_mk_classified_system x_25420 =
    139139  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
    140140    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
    141     x_25394
     141    x_25420
    142142  in
    143143  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
     
    148148    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
    149149    'a1) -> classified_system -> 'a1 **)
    150 let rec classified_system_rect_Type2 h_mk_classified_system x_25396 =
     150let rec classified_system_rect_Type2 h_mk_classified_system x_25422 =
    151151  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
    152152    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
    153     x_25396
     153    x_25422
    154154  in
    155155  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
     
    160160    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
    161161    'a1) -> classified_system -> 'a1 **)
    162 let rec classified_system_rect_Type1 h_mk_classified_system x_25398 =
     162let rec classified_system_rect_Type1 h_mk_classified_system x_25424 =
    163163  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
    164164    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
    165     x_25398
     165    x_25424
    166166  in
    167167  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
     
    172172    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
    173173    'a1) -> classified_system -> 'a1 **)
    174 let rec classified_system_rect_Type0 h_mk_classified_system x_25400 =
     174let rec classified_system_rect_Type0 h_mk_classified_system x_25426 =
    175175  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
    176176    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
    177     x_25400
     177    x_25426
    178178  in
    179179  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
     
    361361    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
    362362    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
    363 let rec preclassified_system_rect_Type4 h_mk_preclassified_system x_25420 =
     363let rec preclassified_system_rect_Type4 h_mk_preclassified_system x_25446 =
    364364  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
    365     pcs_classify0; pcs_callee = pcs_callee0 } = x_25420
     365    pcs_classify0; pcs_callee = pcs_callee0 } = x_25446
    366366  in
    367367  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
     
    371371    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
    372372    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
    373 let rec preclassified_system_rect_Type5 h_mk_preclassified_system x_25422 =
     373let rec preclassified_system_rect_Type5 h_mk_preclassified_system x_25448 =
    374374  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
    375     pcs_classify0; pcs_callee = pcs_callee0 } = x_25422
     375    pcs_classify0; pcs_callee = pcs_callee0 } = x_25448
    376376  in
    377377  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
     
    381381    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
    382382    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
    383 let rec preclassified_system_rect_Type3 h_mk_preclassified_system x_25424 =
     383let rec preclassified_system_rect_Type3 h_mk_preclassified_system x_25450 =
    384384  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
    385     pcs_classify0; pcs_callee = pcs_callee0 } = x_25424
     385    pcs_classify0; pcs_callee = pcs_callee0 } = x_25450
    386386  in
    387387  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
     
    391391    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
    392392    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
    393 let rec preclassified_system_rect_Type2 h_mk_preclassified_system x_25426 =
     393let rec preclassified_system_rect_Type2 h_mk_preclassified_system x_25452 =
    394394  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
    395     pcs_classify0; pcs_callee = pcs_callee0 } = x_25426
     395    pcs_classify0; pcs_callee = pcs_callee0 } = x_25452
    396396  in
    397397  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
     
    401401    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
    402402    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
    403 let rec preclassified_system_rect_Type1 h_mk_preclassified_system x_25428 =
     403let rec preclassified_system_rect_Type1 h_mk_preclassified_system x_25454 =
    404404  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
    405     pcs_classify0; pcs_callee = pcs_callee0 } = x_25428
     405    pcs_classify0; pcs_callee = pcs_callee0 } = x_25454
    406406  in
    407407  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
     
    411411    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
    412412    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
    413 let rec preclassified_system_rect_Type0 h_mk_preclassified_system x_25430 =
     413let rec preclassified_system_rect_Type0 h_mk_preclassified_system x_25456 =
    414414  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
    415     pcs_classify0; pcs_callee = pcs_callee0 } = x_25430
     415    pcs_classify0; pcs_callee = pcs_callee0 } = x_25456
    416416  in
    417417  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
  • extracted/rTL_semantics.ml

    r2873 r2890  
    158158    (Registers.register List.list -> ByteValues.program_counter ->
    159159    ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
    160 let rec frame_rect_Type4 h_mk_frame x_26366 =
     160let rec frame_rect_Type4 h_mk_frame x_26392 =
    161161  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    162     fr_regs = fr_regs0 } = x_26366
     162    fr_regs = fr_regs0 } = x_26392
    163163  in
    164164  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    167167    (Registers.register List.list -> ByteValues.program_counter ->
    168168    ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
    169 let rec frame_rect_Type5 h_mk_frame x_26368 =
     169let rec frame_rect_Type5 h_mk_frame x_26394 =
    170170  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    171     fr_regs = fr_regs0 } = x_26368
     171    fr_regs = fr_regs0 } = x_26394
    172172  in
    173173  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    176176    (Registers.register List.list -> ByteValues.program_counter ->
    177177    ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
    178 let rec frame_rect_Type3 h_mk_frame x_26370 =
     178let rec frame_rect_Type3 h_mk_frame x_26396 =
    179179  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    180     fr_regs = fr_regs0 } = x_26370
     180    fr_regs = fr_regs0 } = x_26396
    181181  in
    182182  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    185185    (Registers.register List.list -> ByteValues.program_counter ->
    186186    ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
    187 let rec frame_rect_Type2 h_mk_frame x_26372 =
     187let rec frame_rect_Type2 h_mk_frame x_26398 =
    188188  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    189     fr_regs = fr_regs0 } = x_26372
     189    fr_regs = fr_regs0 } = x_26398
    190190  in
    191191  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    194194    (Registers.register List.list -> ByteValues.program_counter ->
    195195    ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
    196 let rec frame_rect_Type1 h_mk_frame x_26374 =
     196let rec frame_rect_Type1 h_mk_frame x_26400 =
    197197  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    198     fr_regs = fr_regs0 } = x_26374
     198    fr_regs = fr_regs0 } = x_26400
    199199  in
    200200  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
     
    203203    (Registers.register List.list -> ByteValues.program_counter ->
    204204    ByteValues.bebit -> SemanticsUtils.reg_sp -> 'a1) -> frame -> 'a1 **)
    205 let rec frame_rect_Type0 h_mk_frame x_26376 =
     205let rec frame_rect_Type0 h_mk_frame x_26402 =
    206206  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    207     fr_regs = fr_regs0 } = x_26376
     207    fr_regs = fr_regs0 } = x_26402
    208208  in
    209209  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
  • extracted/semantics.ml

    r2875 r2890  
    326326    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    327327    preclassified_system_pass -> 'a1 **)
    328 let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_3 =
    329   let pcs_pcs = x_3 in h_mk_preclassified_system_pass pcs_pcs __
     328let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_26418 =
     329  let pcs_pcs = x_26418 in h_mk_preclassified_system_pass pcs_pcs __
    330330
    331331(** val preclassified_system_pass_rect_Type5 :
    332332    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    333333    preclassified_system_pass -> 'a1 **)
    334 let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_5 =
    335   let pcs_pcs = x_5 in h_mk_preclassified_system_pass pcs_pcs __
     334let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_26420 =
     335  let pcs_pcs = x_26420 in h_mk_preclassified_system_pass pcs_pcs __
    336336
    337337(** val preclassified_system_pass_rect_Type3 :
    338338    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    339339    preclassified_system_pass -> 'a1 **)
    340 let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_7 =
    341   let pcs_pcs = x_7 in h_mk_preclassified_system_pass pcs_pcs __
     340let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_26422 =
     341  let pcs_pcs = x_26422 in h_mk_preclassified_system_pass pcs_pcs __
    342342
    343343(** val preclassified_system_pass_rect_Type2 :
    344344    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    345345    preclassified_system_pass -> 'a1 **)
    346 let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_9 =
    347   let pcs_pcs = x_9 in h_mk_preclassified_system_pass pcs_pcs __
     346let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_26424 =
     347  let pcs_pcs = x_26424 in h_mk_preclassified_system_pass pcs_pcs __
    348348
    349349(** val preclassified_system_pass_rect_Type1 :
    350350    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    351351    preclassified_system_pass -> 'a1 **)
    352 let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_11 =
    353   let pcs_pcs = x_11 in h_mk_preclassified_system_pass pcs_pcs __
     352let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_26426 =
     353  let pcs_pcs = x_26426 in h_mk_preclassified_system_pass pcs_pcs __
    354354
    355355(** val preclassified_system_pass_rect_Type0 :
    356356    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    357357    preclassified_system_pass -> 'a1 **)
    358 let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_13 =
    359   let pcs_pcs = x_13 in h_mk_preclassified_system_pass pcs_pcs __
     358let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_26428 =
     359  let pcs_pcs = x_26428 in h_mk_preclassified_system_pass pcs_pcs __
    360360
    361361(** val pcs_pcs :
     
    406406let pcs_pcs__o__pcs_exec__o__es1 x0 x1 =
    407407  Measurable.pcs_exec__o__es1 (pcs_pcs x0 x1)
    408 
    409 exception NotImplementedYet
    410408
    411409(** val preclassified_system_of_pass :
     
    449447  (fun x ->
    450448    Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics)
    451 | Compiler.Assembly_pass -> (fun prog -> raise NotImplementedYet)
     449| Compiler.Assembly_pass -> assert false (* absurd case *)
    452450| Compiler.Object_code_pass ->
    453451  (fun prog -> Interpret2.oC_preclassified_system (Obj.magic prog))
     
    459457    Types.unit0 **)
    460458let run_and_print pass prog n print_pass print_event print_error print_exit =
    461  try
    462459  let pcs = preclassified_system_of_pass pass prog in
    463460  let prog0 = prog in
     
    477474      | Errors.Error msg -> print_error msg)
    478475   | Errors.Error msg -> print_error msg)
    479  with
    480   NotImplementedYet -> Types.It
    481 
     476
  • extracted/semanticsUtils.ml

    r2873 r2890  
    154154    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    155155    -> hw_register_env -> 'a1 **)
    156 let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_26234 =
    157   let { reg_env = reg_env0; other_bit = other_bit0 } = x_26234 in
     156let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_26260 =
     157  let { reg_env = reg_env0; other_bit = other_bit0 } = x_26260 in
    158158  h_mk_hw_register_env reg_env0 other_bit0
    159159
     
    161161    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    162162    -> hw_register_env -> 'a1 **)
    163 let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_26236 =
    164   let { reg_env = reg_env0; other_bit = other_bit0 } = x_26236 in
     163let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_26262 =
     164  let { reg_env = reg_env0; other_bit = other_bit0 } = x_26262 in
    165165  h_mk_hw_register_env reg_env0 other_bit0
    166166
     
    168168    (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
    169169    -> hw_register_env -> 'a1 **)
    170 let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_26238 =
    171   let { reg_env = reg_env0; other_bit = other_bit0 } = x_26238 in
     170let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_26264 =
     171  let { reg_env = reg_env0; other_bit = other_bit0 } = x_26264 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_Type2 h_mk_hw_register_env x_26240 =
    178   let { reg_env = reg_env0; other_bit = other_bit0 } = x_26240 in
     177let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_26266 =
     178  let { reg_env = reg_env0; other_bit = other_bit0 } = x_26266 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_Type1 h_mk_hw_register_env x_26242 =
    185   let { reg_env = reg_env0; other_bit = other_bit0 } = x_26242 in
     184let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_26268 =
     185  let { reg_env = reg_env0; other_bit = other_bit0 } = x_26268 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_Type0 h_mk_hw_register_env x_26244 =
    192   let { reg_env = reg_env0; other_bit = other_bit0 } = x_26244 in
     191let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_26270 =
     192  let { reg_env = reg_env0; other_bit = other_bit0 } = x_26270 in
    193193  h_mk_hw_register_env reg_env0 other_bit0
    194194
     
    301301    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    302302    'a1) -> reg_sp -> 'a1 **)
    303 let rec reg_sp_rect_Type4 h_mk_reg_sp x_26260 =
    304   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26260 in
     303let rec reg_sp_rect_Type4 h_mk_reg_sp x_26286 =
     304  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26286 in
    305305  h_mk_reg_sp reg_sp_env0 stackp0
    306306
     
    308308    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    309309    'a1) -> reg_sp -> 'a1 **)
    310 let rec reg_sp_rect_Type5 h_mk_reg_sp x_26262 =
    311   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26262 in
     310let rec reg_sp_rect_Type5 h_mk_reg_sp x_26288 =
     311  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26288 in
    312312  h_mk_reg_sp reg_sp_env0 stackp0
    313313
     
    315315    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    316316    'a1) -> reg_sp -> 'a1 **)
    317 let rec reg_sp_rect_Type3 h_mk_reg_sp x_26264 =
    318   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26264 in
     317let rec reg_sp_rect_Type3 h_mk_reg_sp x_26290 =
     318  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26290 in
    319319  h_mk_reg_sp reg_sp_env0 stackp0
    320320
     
    322322    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    323323    'a1) -> reg_sp -> 'a1 **)
    324 let rec reg_sp_rect_Type2 h_mk_reg_sp x_26266 =
    325   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26266 in
     324let rec reg_sp_rect_Type2 h_mk_reg_sp x_26292 =
     325  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26292 in
    326326  h_mk_reg_sp reg_sp_env0 stackp0
    327327
     
    329329    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    330330    'a1) -> reg_sp -> 'a1 **)
    331 let rec reg_sp_rect_Type1 h_mk_reg_sp x_26268 =
    332   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26268 in
     331let rec reg_sp_rect_Type1 h_mk_reg_sp x_26294 =
     332  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26294 in
    333333  h_mk_reg_sp reg_sp_env0 stackp0
    334334
     
    336336    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    337337    'a1) -> reg_sp -> 'a1 **)
    338 let rec reg_sp_rect_Type0 h_mk_reg_sp x_26270 =
    339   let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26270 in
     338let rec reg_sp_rect_Type0 h_mk_reg_sp x_26296 =
     339  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_26296 in
    340340  h_mk_reg_sp reg_sp_env0 stackp0
    341341
     
    459459    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    460460    -> 'a1) -> sem_graph_params -> 'a1 **)
    461 let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_26286 =
    462   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26286 in
     461let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_26312 =
     462  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26312 in
    463463  h_mk_sem_graph_params sgp_pars0 sgp_sup0
    464464
     
    466466    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    467467    -> 'a1) -> sem_graph_params -> 'a1 **)
    468 let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_26288 =
    469   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26288 in
     468let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_26314 =
     469  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26314 in
    470470  h_mk_sem_graph_params sgp_pars0 sgp_sup0
    471471
     
    473473    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    474474    -> 'a1) -> sem_graph_params -> 'a1 **)
    475 let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_26290 =
    476   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26290 in
     475let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_26316 =
     476  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26316 in
    477477  h_mk_sem_graph_params sgp_pars0 sgp_sup0
    478478
     
    480480    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    481481    -> 'a1) -> sem_graph_params -> 'a1 **)
    482 let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_26292 =
    483   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26292 in
     482let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_26318 =
     483  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26318 in
    484484  h_mk_sem_graph_params sgp_pars0 sgp_sup0
    485485
     
    487487    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    488488    -> 'a1) -> sem_graph_params -> 'a1 **)
    489 let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_26294 =
    490   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26294 in
     489let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_26320 =
     490  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26320 in
    491491  h_mk_sem_graph_params sgp_pars0 sgp_sup0
    492492
     
    494494    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    495495    -> 'a1) -> sem_graph_params -> 'a1 **)
    496 let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_26296 =
    497   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26296 in
     496let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_26322 =
     497  let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0 } = x_26322 in
    498498  h_mk_sem_graph_params sgp_pars0 sgp_sup0
    499499
     
    599599    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    600600    -> 'a1) -> sem_lin_params -> 'a1 **)
    601 let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_26313 =
    602   let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26313 in
     601let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_26339 =
     602  let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26339 in
    603603  h_mk_sem_lin_params slp_pars0 slp_sup0
    604604
     
    606606    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    607607    -> 'a1) -> sem_lin_params -> 'a1 **)
    608 let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_26315 =
    609   let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26315 in
     608let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_26341 =
     609  let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26341 in
    610610  h_mk_sem_lin_params slp_pars0 slp_sup0
    611611
     
    613613    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    614614    -> 'a1) -> sem_lin_params -> 'a1 **)
    615 let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_26317 =
    616   let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26317 in
     615let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_26343 =
     616  let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26343 in
    617617  h_mk_sem_lin_params slp_pars0 slp_sup0
    618618
     
    620620    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    621621    -> 'a1) -> sem_lin_params -> 'a1 **)
    622 let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_26319 =
    623   let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26319 in
     622let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_26345 =
     623  let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26345 in
    624624  h_mk_sem_lin_params slp_pars0 slp_sup0
    625625
     
    627627    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    628628    -> 'a1) -> sem_lin_params -> 'a1 **)
    629 let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_26321 =
    630   let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26321 in
     629let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_26347 =
     630  let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26347 in
    631631  h_mk_sem_lin_params slp_pars0 slp_sup0
    632632
     
    634634    (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
    635635    -> 'a1) -> sem_lin_params -> 'a1 **)
    636 let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_26323 =
    637   let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26323 in
     636let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_26349 =
     637  let { slp_pars = slp_pars0; slp_sup = slp_sup0 } = x_26349 in
    638638  h_mk_sem_lin_params slp_pars0 slp_sup0
    639639
  • extracted/status.ml

    r2873 r2890  
    8989    serialBufferType -> 'a1 **)
    9090let rec serialBufferType_rect_Type4 h_Eight h_Nine = function
    91 | Eight x_24784 -> h_Eight x_24784
    92 | Nine (x_24786, x_24785) -> h_Nine x_24786 x_24785
     91| Eight x_24810 -> h_Eight x_24810
     92| Nine (x_24812, x_24811) -> h_Nine x_24812 x_24811
    9393
    9494(** val serialBufferType_rect_Type5 :
     
    9696    serialBufferType -> 'a1 **)
    9797let rec serialBufferType_rect_Type5 h_Eight h_Nine = function
    98 | Eight x_24790 -> h_Eight x_24790
    99 | Nine (x_24792, x_24791) -> h_Nine x_24792 x_24791
     98| Eight x_24816 -> h_Eight x_24816
     99| Nine (x_24818, x_24817) -> h_Nine x_24818 x_24817
    100100
    101101(** val serialBufferType_rect_Type3 :
     
    103103    serialBufferType -> 'a1 **)
    104104let rec serialBufferType_rect_Type3 h_Eight h_Nine = function
    105 | Eight x_24796 -> h_Eight x_24796
    106 | Nine (x_24798, x_24797) -> h_Nine x_24798 x_24797
     105| Eight x_24822 -> h_Eight x_24822
     106| Nine (x_24824, x_24823) -> h_Nine x_24824 x_24823
    107107
    108108(** val serialBufferType_rect_Type2 :
     
    110110    serialBufferType -> 'a1 **)
    111111let rec serialBufferType_rect_Type2 h_Eight h_Nine = function
    112 | Eight x_24802 -> h_Eight x_24802
    113 | Nine (x_24804, x_24803) -> h_Nine x_24804 x_24803
     112| Eight x_24828 -> h_Eight x_24828
     113| Nine (x_24830, x_24829) -> h_Nine x_24830 x_24829
    114114
    115115(** val serialBufferType_rect_Type1 :
     
    117117    serialBufferType -> 'a1 **)
    118118let rec serialBufferType_rect_Type1 h_Eight h_Nine = function
    119 | Eight x_24808 -> h_Eight x_24808
    120 | Nine (x_24810, x_24809) -> h_Nine x_24810 x_24809
     119| Eight x_24834 -> h_Eight x_24834
     120| Nine (x_24836, x_24835) -> h_Nine x_24836 x_24835
    121121
    122122(** val serialBufferType_rect_Type0 :
     
    124124    serialBufferType -> 'a1 **)
    125125let rec serialBufferType_rect_Type0 h_Eight h_Nine = function
    126 | Eight x_24814 -> h_Eight x_24814
    127 | Nine (x_24816, x_24815) -> h_Nine x_24816 x_24815
     126| Eight x_24840 -> h_Eight x_24840
     127| Nine (x_24842, x_24841) -> h_Nine x_24842 x_24841
    128128
    129129(** val serialBufferType_inv_rect_Type4 :
     
    182182    -> 'a1) -> lineType -> 'a1 **)
    183183let rec lineType_rect_Type4 h_P1 h_P3 h_SerialBuffer = function
    184 | P1 x_24863 -> h_P1 x_24863
    185 | P3 x_24864 -> h_P3 x_24864
    186 | SerialBuffer x_24865 -> h_SerialBuffer x_24865
     184| P1 x_24889 -> h_P1 x_24889
     185| P3 x_24890 -> h_P3 x_24890
     186| SerialBuffer x_24891 -> h_SerialBuffer x_24891
    187187
    188188(** val lineType_rect_Type5 :
     
    190190    -> 'a1) -> lineType -> 'a1 **)
    191191let rec lineType_rect_Type5 h_P1 h_P3 h_SerialBuffer = function
    192 | P1 x_24870 -> h_P1 x_24870
    193 | P3 x_24871 -> h_P3 x_24871
    194 | SerialBuffer x_24872 -> h_SerialBuffer x_24872
     192| P1 x_24896 -> h_P1 x_24896
     193| P3 x_24897 -> h_P3 x_24897
     194| SerialBuffer x_24898 -> h_SerialBuffer x_24898
    195195
    196196(** val lineType_rect_Type3 :
     
    198198    -> 'a1) -> lineType -> 'a1 **)
    199199let rec lineType_rect_Type3 h_P1 h_P3 h_SerialBuffer = function
    200 | P1 x_24877 -> h_P1 x_24877
    201 | P3 x_24878 -> h_P3 x_24878
    202 | SerialBuffer x_24879 -> h_SerialBuffer x_24879
     200| P1 x_24903 -> h_P1 x_24903
     201| P3 x_24904 -> h_P3 x_24904
     202| SerialBuffer x_24905 -> h_SerialBuffer x_24905
    203203
    204204(** val lineType_rect_Type2 :
     
    206206    -> 'a1) -> lineType -> 'a1 **)
    207207let rec lineType_rect_Type2 h_P1 h_P3 h_SerialBuffer = function
    208 | P1 x_24884 -> h_P1 x_24884
    209 | P3 x_24885 -> h_P3 x_24885
    210 | SerialBuffer x_24886 -> h_SerialBuffer x_24886
     208| P1 x_24910 -> h_P1 x_24910
     209| P3 x_24911 -> h_P3 x_24911
     210| SerialBuffer x_24912 -> h_SerialBuffer x_24912
    211211
    212212(** val lineType_rect_Type1 :
     
    214214    -> 'a1) -> lineType -> 'a1 **)
    215215let rec lineType_rect_Type1 h_P1 h_P3 h_SerialBuffer = function
    216 | P1 x_24891 -> h_P1 x_24891
    217 | P3 x_24892 -> h_P3 x_24892
    218 | SerialBuffer x_24893 -> h_SerialBuffer x_24893
     216| P1 x_24917 -> h_P1 x_24917
     217| P3 x_24918 -> h_P3 x_24918
     218| SerialBuffer x_24919 -> h_SerialBuffer x_24919
    219219
    220220(** val lineType_rect_Type0 :
     
    222222    -> 'a1) -> lineType -> 'a1 **)
    223223let rec lineType_rect_Type0 h_P1 h_P3 h_SerialBuffer = function
    224 | P1 x_24898 -> h_P1 x_24898
    225 | P3 x_24899 -> h_P3 x_24899
    226 | SerialBuffer x_24900 -> h_SerialBuffer x_24900
     224| P1 x_24924 -> h_P1 x_24924
     225| P3 x_24925 -> h_P3 x_24925
     226| SerialBuffer x_24926 -> h_SerialBuffer x_24926
    227227
    228228(** val lineType_inv_rect_Type4 :
     
    731731    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    732732    preStatus -> 'a2 **)
    733 let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_25286 =
     733let rec preStatus_rect_Type4 code_memory h_mk_PreStatus x_25312 =
    734734  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    735735    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    737737    special_function_registers_8053; special_function_registers_8052 =
    738738    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    739     p3_latch0; clock = clock0 } = x_25286
     739    p3_latch0; clock = clock0 } = x_25312
    740740  in
    741741  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    749749    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    750750    preStatus -> 'a2 **)
    751 let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_25288 =
     751let rec preStatus_rect_Type5 code_memory h_mk_PreStatus x_25314 =
    752752  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    753753    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    755755    special_function_registers_8053; special_function_registers_8052 =
    756756    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    757     p3_latch0; clock = clock0 } = x_25288
     757    p3_latch0; clock = clock0 } = x_25314
    758758  in
    759759  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    767767    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    768768    preStatus -> 'a2 **)
    769 let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_25290 =
     769let rec preStatus_rect_Type3 code_memory h_mk_PreStatus x_25316 =
    770770  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    771771    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    773773    special_function_registers_8053; special_function_registers_8052 =
    774774    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    775     p3_latch0; clock = clock0 } = x_25290
     775    p3_latch0; clock = clock0 } = x_25316
    776776  in
    777777  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    785785    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    786786    preStatus -> 'a2 **)
    787 let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_25292 =
     787let rec preStatus_rect_Type2 code_memory h_mk_PreStatus x_25318 =
    788788  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    789789    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    791791    special_function_registers_8053; special_function_registers_8052 =
    792792    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    793     p3_latch0; clock = clock0 } = x_25292
     793    p3_latch0; clock = clock0 } = x_25318
    794794  in
    795795  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    803803    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    804804    preStatus -> 'a2 **)
    805 let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_25294 =
     805let rec preStatus_rect_Type1 code_memory h_mk_PreStatus x_25320 =
    806806  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    807807    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    809809    special_function_registers_8053; special_function_registers_8052 =
    810810    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    811     p3_latch0; clock = clock0 } = x_25294
     811    p3_latch0; clock = clock0 } = x_25320
    812812  in
    813813  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
     
    821821    Vector.vector -> BitVector.byte -> BitVector.byte -> time -> 'a2) -> 'a1
    822822    preStatus -> 'a2 **)
    823 let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_25296 =
     823let rec preStatus_rect_Type0 code_memory h_mk_PreStatus x_25322 =
    824824  let { low_internal_ram = low_internal_ram0; high_internal_ram =
    825825    high_internal_ram0; external_ram = external_ram0; program_counter =
     
    827827    special_function_registers_8053; special_function_registers_8052 =
    828828    special_function_registers_8054; p1_latch = p1_latch0; p3_latch =
    829     p3_latch0; clock = clock0 } = x_25296
     829    p3_latch0; clock = clock0 } = x_25322
    830830  in
    831831  h_mk_PreStatus low_internal_ram0 high_internal_ram0 external_ram0
  • extracted/toCminor.ml

    r2882 r2890  
    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_634 -> h_Global x_634
    201 | Stack x_635 -> h_Stack x_635
     200| Global x_13042 -> h_Global x_13042
     201| Stack x_13043 -> h_Stack x_13043
    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_640 -> h_Global x_640
    208 | Stack x_641 -> h_Stack x_641
     207| Global x_13048 -> h_Global x_13048
     208| Stack x_13049 -> h_Stack x_13049
    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_646 -> h_Global x_646
    215 | Stack x_647 -> h_Stack x_647
     214| Global x_13054 -> h_Global x_13054
     215| Stack x_13055 -> h_Stack x_13055
    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_652 -> h_Global x_652
    222 | Stack x_653 -> h_Stack x_653
     221| Global x_13060 -> h_Global x_13060
     222| Stack x_13061 -> h_Stack x_13061
    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_658 -> h_Global x_658
    229 | Stack x_659 -> h_Stack x_659
     228| Global x_13066 -> h_Global x_13066
     229| Stack x_13067 -> h_Stack x_13067
    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_664 -> h_Global x_664
    236 | Stack x_665 -> h_Stack x_665
     235| Global x_13072 -> h_Global x_13072
     236| Stack x_13073 -> h_Stack x_13073
    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_712 -> h_MemDest x_712
     1223| MemDest x_14528 -> h_MemDest x_14528
    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_717 -> h_MemDest x_717
     1230| MemDest x_14533 -> h_MemDest x_14533
    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_722 -> h_MemDest x_722
     1237| MemDest x_14538 -> h_MemDest x_14538
    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_727 -> h_MemDest x_727
     1244| MemDest x_14543 -> h_MemDest x_14543
    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_732 -> h_MemDest x_732
     1251| MemDest x_14548 -> h_MemDest x_14548
    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_737 -> h_MemDest x_737
     1258| MemDest x_14553 -> h_MemDest x_14553
    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_772 =
    1385   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_772
     1384let rec labgen_rect_Type4 h_mk_labgen x_14588 =
     1385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1386    x_14588
    13861387  in
    13871388  h_mk_labgen labuniverse0 label_genlist0 __
     
    13901391    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13911392    'a1) -> labgen -> 'a1 **)
    1392 let rec labgen_rect_Type5 h_mk_labgen x_774 =
    1393   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_774
     1393let rec labgen_rect_Type5 h_mk_labgen x_14590 =
     1394  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1395    x_14590
    13941396  in
    13951397  h_mk_labgen labuniverse0 label_genlist0 __
     
    13981400    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13991401    'a1) -> labgen -> 'a1 **)
    1400 let rec labgen_rect_Type3 h_mk_labgen x_776 =
    1401   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_776
     1402let rec labgen_rect_Type3 h_mk_labgen x_14592 =
     1403  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1404    x_14592
    14021405  in
    14031406  h_mk_labgen labuniverse0 label_genlist0 __
     
    14061409    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14071410    'a1) -> labgen -> 'a1 **)
    1408 let rec labgen_rect_Type2 h_mk_labgen x_778 =
    1409   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_778
     1411let rec labgen_rect_Type2 h_mk_labgen x_14594 =
     1412  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1413    x_14594
    14101414  in
    14111415  h_mk_labgen labuniverse0 label_genlist0 __
     
    14141418    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14151419    'a1) -> labgen -> 'a1 **)
    1416 let rec labgen_rect_Type1 h_mk_labgen x_780 =
    1417   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_780
     1420let rec labgen_rect_Type1 h_mk_labgen x_14596 =
     1421  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1422    x_14596
    14181423  in
    14191424  h_mk_labgen labuniverse0 label_genlist0 __
     
    14221427    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14231428    'a1) -> labgen -> 'a1 **)
    1424 let rec labgen_rect_Type0 h_mk_labgen x_782 =
    1425   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_782
     1429let rec labgen_rect_Type0 h_mk_labgen x_14598 =
     1430  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1431    x_14598
    14261432  in
    14271433  h_mk_labgen labuniverse0 label_genlist0 __
     
    15481554    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15491555    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1550 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_798 =
    1551   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_798 in
     1556let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14614 =
     1557  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14614 in
    15521558  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15531559
     
    15551561    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15561562    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1557 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_800 =
    1558   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_800 in
     1563let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14616 =
     1564  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14616 in
    15591565  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15601566
     
    15621568    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15631569    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1564 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_802 =
    1565   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_802 in
     1570let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14618 =
     1571  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14618 in
    15661572  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15671573
     
    15691575    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15701576    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1571 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_804 =
    1572   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_804 in
     1577let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14620 =
     1578  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14620 in
    15731579  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15741580
     
    15761582    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15771583    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1578 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_806 =
    1579   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_806 in
     1584let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14622 =
     1585  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14622 in
    15801586  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15811587
     
    15831589    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15841590    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1585 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_808 =
    1586   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_808 in
     1591let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14624 =
     1592  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14624 in
    15871593  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15881594
     
    16681674let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
    16691675| DoNotConvert -> h_DoNotConvert
    1670 | ConvertTo (x_830, x_829) -> h_ConvertTo x_830 x_829
     1676| ConvertTo (x_14646, x_14645) -> h_ConvertTo x_14646 x_14645
    16711677
    16721678(** val convert_flag_rect_Type5 :
     
    16751681let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
    16761682| DoNotConvert -> h_DoNotConvert
    1677 | ConvertTo (x_835, x_834) -> h_ConvertTo x_835 x_834
     1683| ConvertTo (x_14651, x_14650) -> h_ConvertTo x_14651 x_14650
    16781684
    16791685(** val convert_flag_rect_Type3 :
     
    16821688let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
    16831689| DoNotConvert -> h_DoNotConvert
    1684 | ConvertTo (x_840, x_839) -> h_ConvertTo x_840 x_839
     1690| ConvertTo (x_14656, x_14655) -> h_ConvertTo x_14656 x_14655
    16851691
    16861692(** val convert_flag_rect_Type2 :
     
    16891695let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
    16901696| DoNotConvert -> h_DoNotConvert
    1691 | ConvertTo (x_845, x_844) -> h_ConvertTo x_845 x_844
     1697| ConvertTo (x_14661, x_14660) -> h_ConvertTo x_14661 x_14660
    16921698
    16931699(** val convert_flag_rect_Type1 :
     
    16961702let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
    16971703| DoNotConvert -> h_DoNotConvert
    1698 | ConvertTo (x_850, x_849) -> h_ConvertTo x_850 x_849
     1704| ConvertTo (x_14666, x_14665) -> h_ConvertTo x_14666 x_14665
    16991705
    17001706(** val convert_flag_rect_Type0 :
     
    17031709let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
    17041710| DoNotConvert -> h_DoNotConvert
    1705 | ConvertTo (x_855, x_854) -> h_ConvertTo x_855 x_854
     1711| ConvertTo (x_14671, x_14670) -> h_ConvertTo x_14671 x_14670
    17061712
    17071713(** val convert_flag_inv_rect_Type4 :
     
    20372043    Obj.magic
    20382044      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2039         (fun eta244 ->
    2040         let result = eta244 in
     2045        (fun eta2436 ->
     2046        let result = eta2436 in
    20412047        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20422048        (fun _ ->
  • extracted/traces.ml

    r2873 r2890  
    142142    (AST.ident List.list -> Joint_semantics.sem_params ->
    143143    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    144 let rec evaluation_params_rect_Type4 h_mk_evaluation_params x_26060 =
     144let rec evaluation_params_rect_Type4 h_mk_evaluation_params x_26086 =
    145145  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    146     x_26060
     146    x_26086
    147147  in
    148148  h_mk_evaluation_params globals0 sparams0 ev_genv0
     
    151151    (AST.ident List.list -> Joint_semantics.sem_params ->
    152152    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    153 let rec evaluation_params_rect_Type5 h_mk_evaluation_params x_26062 =
     153let rec evaluation_params_rect_Type5 h_mk_evaluation_params x_26088 =
    154154  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    155     x_26062
     155    x_26088
    156156  in
    157157  h_mk_evaluation_params globals0 sparams0 ev_genv0
     
    160160    (AST.ident List.list -> Joint_semantics.sem_params ->
    161161    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    162 let rec evaluation_params_rect_Type3 h_mk_evaluation_params x_26064 =
     162let rec evaluation_params_rect_Type3 h_mk_evaluation_params x_26090 =
    163163  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    164     x_26064
     164    x_26090
    165165  in
    166166  h_mk_evaluation_params globals0 sparams0 ev_genv0
     
    169169    (AST.ident List.list -> Joint_semantics.sem_params ->
    170170    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    171 let rec evaluation_params_rect_Type2 h_mk_evaluation_params x_26066 =
     171let rec evaluation_params_rect_Type2 h_mk_evaluation_params x_26092 =
    172172  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    173     x_26066
     173    x_26092
    174174  in
    175175  h_mk_evaluation_params globals0 sparams0 ev_genv0
     
    178178    (AST.ident List.list -> Joint_semantics.sem_params ->
    179179    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    180 let rec evaluation_params_rect_Type1 h_mk_evaluation_params x_26068 =
     180let rec evaluation_params_rect_Type1 h_mk_evaluation_params x_26094 =
    181181  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    182     x_26068
     182    x_26094
    183183  in
    184184  h_mk_evaluation_params globals0 sparams0 ev_genv0
     
    187187    (AST.ident List.list -> Joint_semantics.sem_params ->
    188188    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
    189 let rec evaluation_params_rect_Type0 h_mk_evaluation_params x_26070 =
     189let rec evaluation_params_rect_Type0 h_mk_evaluation_params x_26096 =
    190190  let { globals = globals0; sparams = sparams0; ev_genv = ev_genv0 } =
    191     x_26070
     191    x_26096
    192192  in
    193193  h_mk_evaluation_params globals0 sparams0 ev_genv0
     
    279279    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    280280    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    281 let rec prog_params_rect_Type4 h_mk_prog_params x_26086 =
     281let rec prog_params_rect_Type4 h_mk_prog_params x_26112 =
    282282  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    283     stack_sizes0 } = x_26086
     283    stack_sizes0 } = x_26112
    284284  in
    285285  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    288288    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    289289    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    290 let rec prog_params_rect_Type5 h_mk_prog_params x_26088 =
     290let rec prog_params_rect_Type5 h_mk_prog_params x_26114 =
    291291  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    292     stack_sizes0 } = x_26088
     292    stack_sizes0 } = x_26114
    293293  in
    294294  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    297297    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    298298    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    299 let rec prog_params_rect_Type3 h_mk_prog_params x_26090 =
     299let rec prog_params_rect_Type3 h_mk_prog_params x_26116 =
    300300  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    301     stack_sizes0 } = x_26090
     301    stack_sizes0 } = x_26116
    302302  in
    303303  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    306306    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    307307    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    308 let rec prog_params_rect_Type2 h_mk_prog_params x_26092 =
     308let rec prog_params_rect_Type2 h_mk_prog_params x_26118 =
    309309  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    310     stack_sizes0 } = x_26092
     310    stack_sizes0 } = x_26118
    311311  in
    312312  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    315315    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    316316    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    317 let rec prog_params_rect_Type1 h_mk_prog_params x_26094 =
     317let rec prog_params_rect_Type1 h_mk_prog_params x_26120 =
    318318  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    319     stack_sizes0 } = x_26094
     319    stack_sizes0 } = x_26120
    320320  in
    321321  h_mk_prog_params prog_spars0 prog0 stack_sizes0
     
    324324    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    325325    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
    326 let rec prog_params_rect_Type0 h_mk_prog_params x_26096 =
     326let rec prog_params_rect_Type0 h_mk_prog_params x_26122 =
    327327  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    328     stack_sizes0 } = x_26096
     328    stack_sizes0 } = x_26122
    329329  in
    330330  h_mk_prog_params prog_spars0 prog0 stack_sizes0
  • extracted/untrusted/build.ml

    r2773 r2890  
    2727    Identifiers.foldi PreIdentifiers.LabelTag (fun label stmt graph ->
    2828      let live = liveafter label in
    29       match Glue.option_of_matitaoption (Liveness.eliminable globals live stmt) with
    30 
    31       | Some _ ->
     29      if Liveness.eliminable globals live stmt = Bool.True then
    3230
    3331          (* This statement is eliminable and should be ignored. Eliminable
     
    3937          graph
    4038
    41       | None ->
     39      else
    4240
    4341          (* Create interference edges. The general rule is, every
  • extracted/untrusted/compute_colouring.ml

    r2884 r2890  
    44  (* Build an interference graph for this function, and color
    55     it. Define a function that allows consulting the coloring. *)
    6 
    7 let liveafter n =
    8 let {Types.fst = setreg;
    9      Types.snd = setReg} = Obj.magic (liveafter n) in
    10 let res =
    11  Pset.fold (fun reg acc -> "r_" ^ string_of_int (Glue.int_of_matitapos reg) ^ "," ^ acc)
    12   setreg "" in
    13 prerr_endline ("LINE " ^ string_of_int (Glue.int_of_matitapos n) ^ ": " ^ res);
    14 liveafter n in
    156
    167  let uses = Uses.examine_internal globals int_fun in
     
    5950  (* Define a new function that consults both colorings at once. *)
    6051
    61 let print_Register =
    62  function
    63   | I8051.Register00     -> "Register00"
    64   | I8051.Register01     -> "Register01"
    65   | I8051.Register02     -> "Register02"
    66   | I8051.Register03     -> "Register03"
    67   | I8051.Register04     -> "Register04"
    68   | I8051.Register05     -> "Register05"
    69   | I8051.Register06     -> "Register06"
    70   | I8051.Register07     -> "Register07"
    71   | I8051.Register10     -> "Register10"
    72   | I8051.Register11     -> "Register11"
    73   | I8051.Register12     -> "Register12"
    74   | I8051.Register13     -> "Register13"
    75   | I8051.Register14     -> "Register14"
    76   | I8051.Register15     -> "Register15"
    77   | I8051.Register16     -> "Register16"
    78   | I8051.Register17     -> "Register17"
    79   | I8051.Register20     -> "Register20"
    80   | I8051.Register21     -> "Register21"
    81   | I8051.Register22     -> "Register22"
    82   | I8051.Register23     -> "Register23"
    83   | I8051.Register24     -> "Register24"
    84   | I8051.Register25     -> "Register25"
    85   | I8051.Register26     -> "Register26"
    86   | I8051.Register27     -> "Register27"
    87   | I8051.Register30     -> "Register30"
    88   | I8051.Register31     -> "Register31"
    89   | I8051.Register32     -> "Register32"
    90   | I8051.Register33     -> "Register33"
    91   | I8051.Register34     -> "Register34"
    92   | I8051.Register35     -> "Register35"
    93   | I8051.Register36     -> "Register36"
    94   | I8051.Register37     -> "Register37"
    95   | I8051.RegisterA      -> "RegisterA"
    96   | I8051.RegisterB      -> "RegisterB"
    97   | I8051.RegisterDPL    -> "RegisterDPL"
    98   | I8051.RegisterDPH    -> "RegisterDPH"
    99   | I8051.RegisterCarry  -> "RegisterCarry"
    100 in
    101 
    102 
    10352  let lookup r =
    10453   match r with
     
    10857           Interference.Decision_spill (Glue.matitanat_of_int (Untrusted_interference.Vertex.Map.find (Untrusted_interference.lookup H.graph r) S.coloring))
    10958       | Coloring.Color color ->
    110 prerr_endline ("SPILLED r_" ^ string_of_int (Glue.int_of_matitapos r) ^ " = " ^ print_Register color);
    11159           Interference.Decision_colour color)
    11260    | Types.Inr r -> Interference.Decision_colour r
Note: See TracChangeset for help on using the changeset viewer.