Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/eRTLptrToLTL.ml

    r2743 r2773  
    99open LabelledObjects
    1010
     11open BitVectorTrie
     12
    1113open Graphs
    1214
     
    1719open Registers
    1820
    19 open BitVectorTrie
    20 
    2121open CostLabel
    2222
     
    3737open Extralib
    3838
     39open Lists
     40
     41open Identifiers
     42
     43open Integers
     44
     45open AST
     46
     47open Division
     48
     49open Exp
     50
     51open Arithmetic
     52
    3953open Setoids
    4054
     
    4256
    4357open Option
    44 
    45 open Lists
    46 
    47 open Identifiers
    48 
    49 open Integers
    50 
    51 open AST
    52 
    53 open Division
    54 
    55 open Exp
    56 
    57 open Arithmetic
    5858
    5959open Extranat
     
    167167    arg_decision -> 'a1 **)
    168168let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    169 | Arg_decision_colour x_21681 -> h_arg_decision_colour x_21681
    170 | Arg_decision_spill x_21682 -> h_arg_decision_spill x_21682
    171 | Arg_decision_imm x_21683 -> h_arg_decision_imm x_21683
     169| Arg_decision_colour x_16991 -> h_arg_decision_colour x_16991
     170| Arg_decision_spill x_16992 -> h_arg_decision_spill x_16992
     171| Arg_decision_imm x_16993 -> h_arg_decision_imm x_16993
    172172
    173173(** val arg_decision_rect_Type5 :
     
    175175    arg_decision -> 'a1 **)
    176176let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    177 | Arg_decision_colour x_21688 -> h_arg_decision_colour x_21688
    178 | Arg_decision_spill x_21689 -> h_arg_decision_spill x_21689
    179 | Arg_decision_imm x_21690 -> h_arg_decision_imm x_21690
     177| Arg_decision_colour x_16998 -> h_arg_decision_colour x_16998
     178| Arg_decision_spill x_16999 -> h_arg_decision_spill x_16999
     179| Arg_decision_imm x_17000 -> h_arg_decision_imm x_17000
    180180
    181181(** val arg_decision_rect_Type3 :
     
    183183    arg_decision -> 'a1 **)
    184184let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    185 | Arg_decision_colour x_21695 -> h_arg_decision_colour x_21695
    186 | Arg_decision_spill x_21696 -> h_arg_decision_spill x_21696
    187 | Arg_decision_imm x_21697 -> h_arg_decision_imm x_21697
     185| Arg_decision_colour x_17005 -> h_arg_decision_colour x_17005
     186| Arg_decision_spill x_17006 -> h_arg_decision_spill x_17006
     187| Arg_decision_imm x_17007 -> h_arg_decision_imm x_17007
    188188
    189189(** val arg_decision_rect_Type2 :
     
    191191    arg_decision -> 'a1 **)
    192192let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    193 | Arg_decision_colour x_21702 -> h_arg_decision_colour x_21702
    194 | Arg_decision_spill x_21703 -> h_arg_decision_spill x_21703
    195 | Arg_decision_imm x_21704 -> h_arg_decision_imm x_21704
     193| Arg_decision_colour x_17012 -> h_arg_decision_colour x_17012
     194| Arg_decision_spill x_17013 -> h_arg_decision_spill x_17013
     195| Arg_decision_imm x_17014 -> h_arg_decision_imm x_17014
    196196
    197197(** val arg_decision_rect_Type1 :
     
    199199    arg_decision -> 'a1 **)
    200200let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    201 | Arg_decision_colour x_21709 -> h_arg_decision_colour x_21709
    202 | Arg_decision_spill x_21710 -> h_arg_decision_spill x_21710
    203 | Arg_decision_imm x_21711 -> h_arg_decision_imm x_21711
     201| Arg_decision_colour x_17019 -> h_arg_decision_colour x_17019
     202| Arg_decision_spill x_17020 -> h_arg_decision_spill x_17020
     203| Arg_decision_imm x_17021 -> h_arg_decision_imm x_17021
    204204
    205205(** val arg_decision_rect_Type0 :
     
    207207    arg_decision -> 'a1 **)
    208208let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
    209 | Arg_decision_colour x_21716 -> h_arg_decision_colour x_21716
    210 | Arg_decision_spill x_21717 -> h_arg_decision_spill x_21717
    211 | Arg_decision_imm x_21718 -> h_arg_decision_imm x_21718
     209| Arg_decision_colour x_17026 -> h_arg_decision_colour x_17026
     210| Arg_decision_spill x_17027 -> h_arg_decision_spill x_17027
     211| Arg_decision_imm x_17028 -> h_arg_decision_imm x_17028
    212212
    213213(** val arg_decision_inv_rect_Type4 :
     
    379379    AST.ident List.list -> Nat.nat -> BitVector.byte -> Joint.joint_seq
    380380    List.list **)
    381 let set_stack_int globals off int0 =
     381let set_stack_int globals off int =
    382382  List.append (set_dp_by_offset globals off) (List.Cons ((Joint.MOVE
    383     (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int0)))), (List.Cons
     383    (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), (List.Cons
    384384    ((Joint.STORE ((Obj.magic Types.It), (Obj.magic Types.It),
    385385    (Obj.magic a))), List.Nil))))
     
    402402            (List.append (get_stack globals I8051.RegisterA srco)
    403403              (set_stack globals dsto I8051.RegisterA)))
    404      | Arg_decision_imm int0 ->
     404     | Arg_decision_imm int ->
    405405       preserve_carry_bit globals carry_lives_after
    406          (set_stack_int globals dsto int0))
     406         (set_stack_int globals dsto int))
    407407  | Interference.Decision_colour dstr ->
    408408    (match src with
     
    429429       preserve_carry_bit globals carry_lives_after
    430430         (get_stack globals dstr srco)
    431      | Arg_decision_imm int0 ->
     431     | Arg_decision_imm int ->
    432432       List.append (List.Cons ((Joint.MOVE
    433          (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int0)))), List.Nil))
     433         (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), List.Nil))
    434434         (match I8051.eq_Register dstr I8051.RegisterA with
    435435          | Bool.True -> List.Nil
     
    512512    Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
    513513    List.list **)
    514 let translate_op2 globals carry_lives_after op4 dst arg1 arg2 =
     514let translate_op2 globals carry_lives_after op dst arg1 arg2 =
    515515  List.append
    516516    (preserve_carry_bit globals
    517       (Bool.andb (uses_carry op4)
     517      (Bool.andb (uses_carry op)
    518518        (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2)))
    519519      (List.append
     
    522522        (move globals Bool.False (Interference.Decision_colour
    523523          I8051.RegisterA) arg1)))
    524     (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a), (Obj.magic a),
     524    (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a), (Obj.magic a),
    525525      (Obj.magic (Joint.hdw_argument_from_reg I8051.RegisterB)))), List.Nil))
    526       (move globals (Bool.andb (sets_carry op4) carry_lives_after) dst
     526      (move globals (Bool.andb (sets_carry op) carry_lives_after) dst
    527527        (Arg_decision_colour I8051.RegisterA)))
    528528
     
    531531    Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
    532532    List.list **)
    533 let translate_op2_smart globals carry_lives_after op4 dst arg1 arg2 =
     533let translate_op2_smart globals carry_lives_after op dst arg1 arg2 =
    534534  preserve_carry_bit globals
    535     (Bool.andb (Bool.andb (Bool.notb (sets_carry op4)) carry_lives_after)
     535    (Bool.andb (Bool.andb (Bool.notb (sets_carry op)) carry_lives_after)
    536536      (Bool.orb (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2))
    537537        (is_spilled dst)))
     
    539539     | Arg_decision_colour arg2r ->
    540540       List.append
    541          (move globals (uses_carry op4) (Interference.Decision_colour
     541         (move globals (uses_carry op) (Interference.Decision_colour
    542542           I8051.RegisterA) arg1)
    543          (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a),
     543         (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
    544544           (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_reg arg2r)))),
    545545           List.Nil))
    546            (move globals (Bool.andb (sets_carry op4) carry_lives_after) dst
     546           (move globals (Bool.andb (sets_carry op) carry_lives_after) dst
    547547             (Arg_decision_colour I8051.RegisterA)))
    548548     | Arg_decision_spill x ->
    549        (match commutative op4 with
     549       (match commutative op with
    550550        | Bool.True ->
    551551          (match arg1 with
    552552           | Arg_decision_colour arg1r ->
    553553             List.append
    554                (move globals (uses_carry op4) (Interference.Decision_colour
     554               (move globals (uses_carry op) (Interference.Decision_colour
    555555                 I8051.RegisterA) arg2)
    556                (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a),
     556               (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
    557557                 (Obj.magic a),
    558558                 (Obj.magic (Joint.hdw_argument_from_reg arg1r)))),
    559559                 List.Nil))
    560                  (move globals (Bool.andb (sets_carry op4) carry_lives_after)
     560                 (move globals (Bool.andb (sets_carry op) carry_lives_after)
    561561                   dst (Arg_decision_colour I8051.RegisterA)))
    562562           | Arg_decision_spill x0 ->
    563              translate_op2 globals carry_lives_after op4 dst arg1 arg2
     563             translate_op2 globals carry_lives_after op dst arg1 arg2
    564564           | Arg_decision_imm arg1i ->
    565565             List.append
    566                (move globals (uses_carry op4) (Interference.Decision_colour
     566               (move globals (uses_carry op) (Interference.Decision_colour
    567567                 I8051.RegisterA) arg2)
    568                (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a),
     568               (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
    569569                 (Obj.magic a),
    570570                 (Obj.magic (Joint.hdw_argument_from_byte arg1i)))),
    571571                 List.Nil))
    572                  (move globals (Bool.andb (sets_carry op4) carry_lives_after)
     572                 (move globals (Bool.andb (sets_carry op) carry_lives_after)
    573573                   dst (Arg_decision_colour I8051.RegisterA))))
    574574        | Bool.False ->
    575           translate_op2 globals carry_lives_after op4 dst arg1 arg2)
     575          translate_op2 globals carry_lives_after op dst arg1 arg2)
    576576     | Arg_decision_imm arg2i ->
    577577       List.append
    578          (move globals (uses_carry op4) (Interference.Decision_colour
     578         (move globals (uses_carry op) (Interference.Decision_colour
    579579           I8051.RegisterA) arg1)
    580          (List.append (List.Cons ((Joint.OP2 (op4, (Obj.magic a),
     580         (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
    581581           (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_byte arg2i)))),
    582582           List.Nil))
    583            (move globals (Bool.andb (sets_carry op4) carry_lives_after) dst
     583           (move globals (Bool.andb (sets_carry op) carry_lives_after) dst
    584584             (Arg_decision_colour I8051.RegisterA))))
    585585
     
    647647    Interference.decision -> Interference.decision -> Joint.joint_seq
    648648    List.list **)
    649 let translate_op1 globals carry_lives_after op4 dst arg =
     649let translate_op1 globals carry_lives_after op dst arg =
    650650  let preserve_carry =
    651651    Bool.andb carry_lives_after (Bool.orb (is_spilled dst) (is_spilled arg))
     
    654654    (List.append
    655655      (move globals Bool.False (Interference.Decision_colour I8051.RegisterA)
    656         (dec_to_arg_dec arg)) (List.Cons ((Joint.OP1 (op4,
     656        (dec_to_arg_dec arg)) (List.Cons ((Joint.OP1 (op,
    657657      (Obj.magic Types.It), (Obj.magic Types.It))),
    658658      (move globals Bool.False dst (Arg_decision_colour I8051.RegisterA)))))
     
    662662    Interference.decision -> Interference.decision -> arg_decision ->
    663663    arg_decision -> Joint.joint_seq List.list **)
    664 let translate_opaccs globals carry_lives_after op4 dst1 dst2 arg1 arg2 =
     664let translate_opaccs globals carry_lives_after op dst1 dst2 arg1 arg2 =
    665665  List.append
    666666    (move globals Bool.False (Interference.Decision_colour I8051.RegisterB)
     
    668668    (List.append
    669669      (move globals Bool.False (Interference.Decision_colour I8051.RegisterA)
    670         arg1) (List.Cons ((Joint.OPACCS (op4, (Obj.magic Types.It),
     670        arg1) (List.Cons ((Joint.OPACCS (op, (Obj.magic Types.It),
    671671      (Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic Types.It))),
    672672      (List.append
     
    792792let translate_step globals after grph stack_sz lbl s =
    793793  Bind_new.Bret
    794     (let lookup1 = fun r -> grph.Interference.colouring (Types.Inl r) in
     794    (let lookup = fun r -> grph.Interference.colouring (Types.Inl r) in
    795795    let lookup_arg = fun a0 ->
    796796      match a0 with
    797       | Joint.Reg r -> dec_to_arg_dec (lookup1 r)
     797      | Joint.Reg r -> dec_to_arg_dec (lookup r)
    798798      | Joint.Imm b -> Arg_decision_imm b
    799799    in
     
    824824         (Blocks.add_dummy_variance
    825825           (move0 (Interference.Decision_colour I8051.RegisterA)
    826              (dec_to_arg_dec (Obj.magic lookup1 r)))); Types.snd = (fun x ->
     826             (dec_to_arg_dec (Obj.magic lookup r)))); Types.snd = (fun x ->
    827827         Joint.COND ((Obj.magic Types.It), ltrue)) }; Types.snd = List.Nil }
    828828     | Joint.Step_seq s' ->
     
    834834          let lookup_move_dst = fun x ->
    835835            match x with
    836             | ERTL.PSD r -> lookup1 r
     836            | ERTL.PSD r -> lookup r
    837837            | ERTL.HDW r -> Interference.Decision_colour r
    838838          in
     
    848848          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    849849            globals (List.Cons ((Joint.POP (Obj.magic a)),
    850             (move0 (Obj.magic lookup1 r) (Arg_decision_colour
     850            (move0 (Obj.magic lookup r) (Arg_decision_colour
    851851              I8051.RegisterA))))
    852852        | Joint.PUSH a0 ->
     
    861861            globals
    862862            (translate_address (Obj.magic globals) carry_lives_after
    863               (Obj.magic lbl0) (Obj.magic lookup1 dpl)
    864               (Obj.magic lookup1 dph))
    865         | Joint.OPACCS (op4, dst1, dst2, arg1, arg2) ->
     863              (Obj.magic lbl0) (Obj.magic lookup dpl) (Obj.magic lookup dph))
     864        | Joint.OPACCS (op, dst1, dst2, arg1, arg2) ->
    866865          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    867866            globals
    868             (translate_opaccs globals carry_lives_after op4
    869               (Obj.magic lookup1 dst1) (Obj.magic lookup1 dst2)
     867            (translate_opaccs globals carry_lives_after op
     868              (Obj.magic lookup dst1) (Obj.magic lookup dst2)
    870869              (Obj.magic lookup_arg arg1) (Obj.magic lookup_arg arg2))
    871         | Joint.OP1 (op4, dst, arg) ->
     870        | Joint.OP1 (op, dst, arg) ->
    872871          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    873872            globals
    874             (translate_op1 globals carry_lives_after op4
    875               (Obj.magic lookup1 dst) (Obj.magic lookup1 arg))
    876         | Joint.OP2 (op4, dst, arg1, arg2) ->
     873            (translate_op1 globals carry_lives_after op
     874              (Obj.magic lookup dst) (Obj.magic lookup arg))
     875        | Joint.OP2 (op, dst, arg1, arg2) ->
    877876          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    878877            globals
    879             (translate_op2_smart globals carry_lives_after op4
    880               (Obj.magic lookup1 dst) (Obj.magic lookup_arg arg1)
     878            (translate_op2_smart globals carry_lives_after op
     879              (Obj.magic lookup dst) (Obj.magic lookup_arg arg1)
    881880              (Obj.magic lookup_arg arg2))
    882881        | Joint.CLEAR_CARRY ->
     
    889888          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    890889            globals
    891             (translate_load globals carry_lives_after
    892               (Obj.magic lookup1 dstr) (Obj.magic lookup_arg addr1)
    893               (Obj.magic lookup_arg addr2))
     890            (translate_load globals carry_lives_after (Obj.magic lookup dstr)
     891              (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2))
    894892        | Joint.STORE (addr1, addr2, srcr) ->
    895893          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
     
    907905                | ERTL.Ertl_del_frame -> delframe globals stack_sz
    908906                | ERTL.Ertl_frame_size r ->
    909                   move0 (lookup1 r) (Arg_decision_imm
     907                  move0 (lookup r) (Arg_decision_imm
    910908                    (Joint.byte_of_nat stack_sz)))
    911              | ERTLptr.LOW_ADDRESS (r5, l) ->
    912                translate_low_address globals carry_lives_after (lookup1 r5) l
    913              | ERTLptr.HIGH_ADDRESS (r5, l) ->
    914                translate_high_address globals carry_lives_after (lookup1 r5)
    915                  l))))
     909             | ERTLptr.LOW_ADDRESS (r1, l) ->
     910               translate_low_address globals carry_lives_after (lookup r1) l
     911             | ERTLptr.HIGH_ADDRESS (r1, l) ->
     912               translate_high_address globals carry_lives_after (lookup r1) l))))
    916913
    917914(** val translate_fin_step :
     
    934931    Liveness.analyse_liveness the_fixpoint globals (Types.pi1 int_fun)
    935932  in
    936   let coloured_graph0 = build globals (Types.pi1 int_fun) after in
     933  let coloured_graph = build globals (Types.pi1 int_fun) after in
    937934  let stack_sz =
    938     Nat.plus coloured_graph0.Interference.spilled_no
     935    Nat.plus coloured_graph.Interference.spilled_no
    939936      (Types.pi1 int_fun).Joint.joint_if_stacksize
    940937  in
     
    943940  TranslateUtils.init_stack_size = stack_sz; TranslateUtils.added_prologue =
    944941  List.Nil; TranslateUtils.f_step =
    945   (translate_step globals after coloured_graph0 stack_sz);
     942  (translate_step globals after coloured_graph stack_sz);
    946943  TranslateUtils.f_fin = (translate_fin_step globals) }
    947944
Note: See TracChangeset for help on using the changeset viewer.