Ignore:
Timestamp:
Mar 8, 2013, 9:07:28 PM (7 years ago)
Author:
sacerdot
Message:

Everything extracted again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/eRTLptrToLTL.ml

    r2797 r2827  
    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_21810 -> h_arg_decision_colour x_21810
    170 | Arg_decision_spill x_21811 -> h_arg_decision_spill x_21811
    171 | Arg_decision_imm x_21812 -> h_arg_decision_imm x_21812
     169| Arg_decision_colour x_21936 -> h_arg_decision_colour x_21936
     170| Arg_decision_spill x_21937 -> h_arg_decision_spill x_21937
     171| Arg_decision_imm x_21938 -> h_arg_decision_imm x_21938
    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_21817 -> h_arg_decision_colour x_21817
    178 | Arg_decision_spill x_21818 -> h_arg_decision_spill x_21818
    179 | Arg_decision_imm x_21819 -> h_arg_decision_imm x_21819
     177| Arg_decision_colour x_21943 -> h_arg_decision_colour x_21943
     178| Arg_decision_spill x_21944 -> h_arg_decision_spill x_21944
     179| Arg_decision_imm x_21945 -> h_arg_decision_imm x_21945
    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_21824 -> h_arg_decision_colour x_21824
    186 | Arg_decision_spill x_21825 -> h_arg_decision_spill x_21825
    187 | Arg_decision_imm x_21826 -> h_arg_decision_imm x_21826
     185| Arg_decision_colour x_21950 -> h_arg_decision_colour x_21950
     186| Arg_decision_spill x_21951 -> h_arg_decision_spill x_21951
     187| Arg_decision_imm x_21952 -> h_arg_decision_imm x_21952
    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_21831 -> h_arg_decision_colour x_21831
    194 | Arg_decision_spill x_21832 -> h_arg_decision_spill x_21832
    195 | Arg_decision_imm x_21833 -> h_arg_decision_imm x_21833
     193| Arg_decision_colour x_21957 -> h_arg_decision_colour x_21957
     194| Arg_decision_spill x_21958 -> h_arg_decision_spill x_21958
     195| Arg_decision_imm x_21959 -> h_arg_decision_imm x_21959
    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_21838 -> h_arg_decision_colour x_21838
    202 | Arg_decision_spill x_21839 -> h_arg_decision_spill x_21839
    203 | Arg_decision_imm x_21840 -> h_arg_decision_imm x_21840
     201| Arg_decision_colour x_21964 -> h_arg_decision_colour x_21964
     202| Arg_decision_spill x_21965 -> h_arg_decision_spill x_21965
     203| Arg_decision_imm x_21966 -> h_arg_decision_imm x_21966
    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_21845 -> h_arg_decision_colour x_21845
    210 | Arg_decision_spill x_21846 -> h_arg_decision_spill x_21846
    211 | Arg_decision_imm x_21847 -> h_arg_decision_imm x_21847
     209| Arg_decision_colour x_21971 -> h_arg_decision_colour x_21971
     210| Arg_decision_spill x_21972 -> h_arg_decision_spill x_21972
     211| Arg_decision_imm x_21973 -> h_arg_decision_imm x_21973
    212212
    213213(** val arg_decision_inv_rect_Type4 :
     
    340340
    341341(** val get_stack :
    342     AST.ident List.list -> I8051.register -> Nat.nat -> Joint.joint_seq
    343     List.list **)
    344 let get_stack globals r off =
    345   List.append (set_dp_by_offset globals off)
     342    AST.ident List.list -> Nat.nat -> I8051.register -> Nat.nat ->
     343    Joint.joint_seq List.list **)
     344let get_stack globals localss r off =
     345  let off0 = Nat.plus localss off in
     346  List.append (set_dp_by_offset globals off0)
    346347    (List.append (List.Cons ((Joint.LOAD ((Obj.magic a),
    347348      (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil))
     
    353354
    354355(** val set_stack_not_a :
    355     AST.ident List.list -> Nat.nat -> I8051.register -> Joint.joint_seq
    356     List.list **)
    357 let set_stack_not_a globals off r =
    358   List.append (set_dp_by_offset globals off) (List.Cons ((Joint.MOVE
     356    AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
     357    Joint.joint_seq List.list **)
     358let set_stack_not_a globals localss off r =
     359  let off0 = Nat.plus localss off in
     360  List.append (set_dp_by_offset globals off0) (List.Cons ((Joint.MOVE
    359361    (Obj.magic (Joint_LTL_LIN.To_acc (a, r)))), (List.Cons ((Joint.STORE
    360362    ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))),
     
    362364
    363365(** val set_stack_a :
    364     AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
    365 let set_stack_a globals off =
     366    AST.ident List.list -> Nat.nat -> Nat.nat -> Joint.joint_seq List.list **)
     367let set_stack_a globals localss off =
    366368  List.append (List.Cons ((Joint.MOVE
    367369    (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerST1, a)))), List.Nil))
    368     (set_stack_not_a globals off I8051.registerST1)
     370    (set_stack_not_a globals localss off I8051.registerST1)
    369371
    370372(** val set_stack :
    371     AST.ident List.list -> Nat.nat -> I8051.register -> Joint.joint_seq
    372     List.list **)
    373 let set_stack globals off r =
     373    AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
     374    Joint.joint_seq List.list **)
     375let set_stack globals localss off r =
    374376  match I8051.eq_Register r I8051.RegisterA with
    375   | Bool.True -> set_stack_a globals off
    376   | Bool.False -> set_stack_not_a globals off r
     377  | Bool.True -> set_stack_a globals localss off
     378  | Bool.False -> set_stack_not_a globals localss off r
    377379
    378380(** val set_stack_int :
    379     AST.ident List.list -> Nat.nat -> BitVector.byte -> Joint.joint_seq
    380     List.list **)
    381 let set_stack_int globals off int =
    382   List.append (set_dp_by_offset globals off) (List.Cons ((Joint.MOVE
     381    AST.ident List.list -> Nat.nat -> Nat.nat -> BitVector.byte ->
     382    Joint.joint_seq List.list **)
     383let set_stack_int globals localss off int =
     384  let off0 = Nat.plus localss off in
     385  List.append (set_dp_by_offset globals off0) (List.Cons ((Joint.MOVE
    383386    (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), (List.Cons
    384387    ((Joint.STORE ((Obj.magic Types.It), (Obj.magic Types.It),
     
    386389
    387390(** val move :
    388     AST.ident List.list -> Bool.bool -> Interference.decision -> arg_decision
    389     -> Joint.joint_seq List.list **)
    390 let move globals carry_lives_after dst src =
     391    AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
     392    arg_decision -> Joint.joint_seq List.list **)
     393let move globals localss carry_lives_after dst src =
    391394  match dst with
    392395  | Interference.Decision_spill dsto ->
     
    394397     | Arg_decision_colour srcr ->
    395398       preserve_carry_bit globals carry_lives_after
    396          (set_stack globals dsto srcr)
     399         (set_stack globals localss dsto srcr)
    397400     | Arg_decision_spill srco ->
    398401       (match Nat.eqb srco dsto with
     
    400403        | Bool.False ->
    401404          preserve_carry_bit globals carry_lives_after
    402             (List.append (get_stack globals I8051.RegisterA srco)
    403               (set_stack globals dsto I8051.RegisterA)))
     405            (List.append (get_stack globals localss I8051.RegisterA srco)
     406              (set_stack globals localss dsto I8051.RegisterA)))
    404407     | Arg_decision_imm int ->
    405408       preserve_carry_bit globals carry_lives_after
    406          (set_stack_int globals dsto int))
     409         (set_stack_int globals localss dsto int))
    407410  | Interference.Decision_colour dstr ->
    408411    (match src with
     
    428431     | Arg_decision_spill srco ->
    429432       preserve_carry_bit globals carry_lives_after
    430          (get_stack globals dstr srco)
     433         (get_stack globals localss dstr srco)
    431434     | Arg_decision_imm int ->
    432435       List.append (List.Cons ((Joint.MOVE
     
    509512
    510513(** val translate_op2 :
    511     AST.ident List.list -> Bool.bool -> BackEndOps.op2 ->
     514    AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
    512515    Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
    513516    List.list **)
    514 let translate_op2 globals carry_lives_after op dst arg1 arg2 =
     517let translate_op2 globals localss carry_lives_after op dst arg1 arg2 =
    515518  List.append
    516519    (preserve_carry_bit globals
     
    518521        (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2)))
    519522      (List.append
    520         (move globals Bool.False (Interference.Decision_colour
     523        (move globals localss Bool.False (Interference.Decision_colour
    521524          I8051.RegisterB) arg2)
    522         (move globals Bool.False (Interference.Decision_colour
     525        (move globals localss Bool.False (Interference.Decision_colour
    523526          I8051.RegisterA) arg1)))
    524527    (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a), (Obj.magic a),
    525528      (Obj.magic (Joint.hdw_argument_from_reg I8051.RegisterB)))), List.Nil))
    526       (move globals (Bool.andb (sets_carry op) carry_lives_after) dst
     529      (move globals localss (Bool.andb (sets_carry op) carry_lives_after) dst
    527530        (Arg_decision_colour I8051.RegisterA)))
    528531
    529532(** val translate_op2_smart :
    530     AST.ident List.list -> Bool.bool -> BackEndOps.op2 ->
     533    AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
    531534    Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
    532535    List.list **)
    533 let translate_op2_smart globals carry_lives_after op dst arg1 arg2 =
     536let translate_op2_smart globals localss carry_lives_after op dst arg1 arg2 =
    534537  preserve_carry_bit globals
    535538    (Bool.andb (Bool.andb (Bool.notb (sets_carry op)) carry_lives_after)
     
    539542     | Arg_decision_colour arg2r ->
    540543       List.append
    541          (move globals (uses_carry op) (Interference.Decision_colour
     544         (move globals localss (uses_carry op) (Interference.Decision_colour
    542545           I8051.RegisterA) arg1)
    543546         (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
    544547           (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_reg arg2r)))),
    545548           List.Nil))
    546            (move globals (Bool.andb (sets_carry op) carry_lives_after) dst
     549           (move globals localss
     550             (Bool.andb (sets_carry op) carry_lives_after) dst
    547551             (Arg_decision_colour I8051.RegisterA)))
    548552     | Arg_decision_spill x ->
     
    552556           | Arg_decision_colour arg1r ->
    553557             List.append
    554                (move globals (uses_carry op) (Interference.Decision_colour
    555                  I8051.RegisterA) arg2)
     558               (move globals localss (uses_carry op)
     559                 (Interference.Decision_colour I8051.RegisterA) arg2)
    556560               (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
    557561                 (Obj.magic a),
    558562                 (Obj.magic (Joint.hdw_argument_from_reg arg1r)))),
    559563                 List.Nil))
    560                  (move globals (Bool.andb (sets_carry op) carry_lives_after)
    561                    dst (Arg_decision_colour I8051.RegisterA)))
     564                 (move globals localss
     565                   (Bool.andb (sets_carry op) carry_lives_after) dst
     566                   (Arg_decision_colour I8051.RegisterA)))
    562567           | Arg_decision_spill x0 ->
    563              translate_op2 globals carry_lives_after op dst arg1 arg2
     568             translate_op2 globals localss carry_lives_after op dst arg1 arg2
    564569           | Arg_decision_imm arg1i ->
    565570             List.append
    566                (move globals (uses_carry op) (Interference.Decision_colour
    567                  I8051.RegisterA) arg2)
     571               (move globals localss (uses_carry op)
     572                 (Interference.Decision_colour I8051.RegisterA) arg2)
    568573               (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
    569574                 (Obj.magic a),
    570575                 (Obj.magic (Joint.hdw_argument_from_byte arg1i)))),
    571576                 List.Nil))
    572                  (move globals (Bool.andb (sets_carry op) carry_lives_after)
    573                    dst (Arg_decision_colour I8051.RegisterA))))
     577                 (move globals localss
     578                   (Bool.andb (sets_carry op) carry_lives_after) dst
     579                   (Arg_decision_colour I8051.RegisterA))))
    574580        | Bool.False ->
    575           translate_op2 globals carry_lives_after op dst arg1 arg2)
     581          translate_op2 globals localss carry_lives_after op dst arg1 arg2)
    576582     | Arg_decision_imm arg2i ->
    577583       List.append
    578          (move globals (uses_carry op) (Interference.Decision_colour
     584         (move globals localss (uses_carry op) (Interference.Decision_colour
    579585           I8051.RegisterA) arg1)
    580586         (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
    581587           (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_byte arg2i)))),
    582588           List.Nil))
    583            (move globals (Bool.andb (sets_carry op) carry_lives_after) dst
     589           (move globals localss
     590             (Bool.andb (sets_carry op) carry_lives_after) dst
    584591             (Arg_decision_colour I8051.RegisterA))))
    585592
     
    644651
    645652(** val translate_op1 :
    646     AST.ident List.list -> Bool.bool -> BackEndOps.op1 ->
     653    AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op1 ->
    647654    Interference.decision -> Interference.decision -> Joint.joint_seq
    648655    List.list **)
    649 let translate_op1 globals carry_lives_after op dst arg =
     656let translate_op1 globals localss carry_lives_after op dst arg =
    650657  let preserve_carry =
    651658    Bool.andb carry_lives_after (Bool.orb (is_spilled dst) (is_spilled arg))
     
    653660  preserve_carry_bit globals preserve_carry
    654661    (List.append
    655       (move globals Bool.False (Interference.Decision_colour I8051.RegisterA)
    656         (dec_to_arg_dec arg)) (List.Cons ((Joint.OP1 (op,
     662      (move globals localss Bool.False (Interference.Decision_colour
     663        I8051.RegisterA) (dec_to_arg_dec arg)) (List.Cons ((Joint.OP1 (op,
    657664      (Obj.magic Types.It), (Obj.magic Types.It))),
    658       (move globals Bool.False dst (Arg_decision_colour I8051.RegisterA)))))
     665      (move globals localss Bool.False dst (Arg_decision_colour
     666        I8051.RegisterA)))))
    659667
    660668(** val translate_opaccs :
    661     AST.ident List.list -> Bool.bool -> BackEndOps.opAccs ->
     669    AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.opAccs ->
    662670    Interference.decision -> Interference.decision -> arg_decision ->
    663671    arg_decision -> Joint.joint_seq List.list **)
    664 let translate_opaccs globals carry_lives_after op dst1 dst2 arg1 arg2 =
     672let translate_opaccs globals localss carry_lives_after op dst1 dst2 arg1 arg2 =
    665673  List.append
    666     (move globals Bool.False (Interference.Decision_colour I8051.RegisterB)
    667       arg2)
     674    (move globals localss Bool.False (Interference.Decision_colour
     675      I8051.RegisterB) arg2)
    668676    (List.append
    669       (move globals Bool.False (Interference.Decision_colour I8051.RegisterA)
    670         arg1) (List.Cons ((Joint.OPACCS (op, (Obj.magic Types.It),
    671       (Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic Types.It))),
     677      (move globals localss Bool.False (Interference.Decision_colour
     678        I8051.RegisterA) arg1) (List.Cons ((Joint.OPACCS (op,
     679      (Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic Types.It),
     680      (Obj.magic Types.It))),
    672681      (List.append
    673         (move globals Bool.False dst1 (Arg_decision_colour I8051.RegisterA))
     682        (move globals localss Bool.False dst1 (Arg_decision_colour
     683          I8051.RegisterA))
    674684        (List.append
    675           (move globals Bool.False dst2 (Arg_decision_colour
     685          (move globals localss Bool.False dst2 (Arg_decision_colour
    676686            I8051.RegisterB))
    677687          (match Bool.andb carry_lives_after
     
    681691
    682692(** val move_to_dp :
    683     AST.ident List.list -> arg_decision -> arg_decision -> Joint.joint_seq
    684     List.list **)
    685 let move_to_dp globals arg1 arg2 =
     693    AST.ident List.list -> Nat.nat -> arg_decision -> arg_decision ->
     694    Joint.joint_seq List.list **)
     695let move_to_dp globals localss arg1 arg2 =
    686696  match Bool.notb (arg_is_spilled arg1) with
    687697  | Bool.True ->
    688698    List.append
    689       (move globals Bool.False (Interference.Decision_colour
     699      (move globals localss Bool.False (Interference.Decision_colour
    690700        I8051.RegisterDPH) arg2)
    691       (move globals Bool.False (Interference.Decision_colour
     701      (move globals localss Bool.False (Interference.Decision_colour
    692702        I8051.RegisterDPL) arg1)
    693703  | Bool.False ->
     
    695705     | Bool.True ->
    696706       List.append
    697          (move globals Bool.False (Interference.Decision_colour
     707         (move globals localss Bool.False (Interference.Decision_colour
    698708           I8051.RegisterDPL) arg1)
    699          (move globals Bool.False (Interference.Decision_colour
     709         (move globals localss Bool.False (Interference.Decision_colour
    700710           I8051.RegisterDPH) arg2)
    701711     | Bool.False ->
    702712       List.append
    703          (move globals Bool.False (Interference.Decision_colour
     713         (move globals localss Bool.False (Interference.Decision_colour
    704714           I8051.RegisterB) arg1)
    705715         (List.append
    706            (move globals Bool.False (Interference.Decision_colour
     716           (move globals localss Bool.False (Interference.Decision_colour
    707717             I8051.RegisterDPH) arg2)
    708            (move globals Bool.False (Interference.Decision_colour
     718           (move globals localss Bool.False (Interference.Decision_colour
    709719             I8051.RegisterDPL) (Arg_decision_colour I8051.RegisterB))))
    710720
    711721(** val translate_store :
    712     AST.ident List.list -> Bool.bool -> arg_decision -> arg_decision ->
    713     arg_decision -> Joint.joint_seq List.list **)
    714 let translate_store globals carry_lives_after addr1 addr2 src =
     722    AST.ident List.list -> Nat.nat -> Bool.bool -> arg_decision ->
     723    arg_decision -> arg_decision -> Joint.joint_seq List.list **)
     724let translate_store globals localss carry_lives_after addr1 addr2 src =
    715725  preserve_carry_bit globals
    716726    (Bool.andb carry_lives_after
    717727      (Bool.orb (Bool.orb (arg_is_spilled addr1) (arg_is_spilled addr1))
    718728        (arg_is_spilled src)))
    719     (let move_to_dptr = move_to_dp globals addr1 addr2 in
     729    (let move_to_dptr = move_to_dp globals localss addr1 addr2 in
    720730    List.append
    721731      (match arg_is_spilled src with
    722732       | Bool.True ->
    723733         List.append
    724            (move globals Bool.False (Interference.Decision_colour
     734           (move globals localss Bool.False (Interference.Decision_colour
    725735             I8051.registerST0) src)
    726736           (List.append move_to_dptr (List.Cons ((Joint.MOVE
     
    732742
    733743(** val translate_load :
    734     AST.ident List.list -> Bool.bool -> Interference.decision -> arg_decision
    735     -> arg_decision -> Joint.joint_seq List.list **)
    736 let translate_load globals carry_lives_after dst addr1 addr2 =
     744    AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
     745    arg_decision -> arg_decision -> Joint.joint_seq List.list **)
     746let translate_load globals localss carry_lives_after dst addr1 addr2 =
    737747  preserve_carry_bit globals
    738748    (Bool.andb carry_lives_after
    739749      (Bool.orb (Bool.orb (is_spilled dst) (arg_is_spilled addr1))
    740750        (arg_is_spilled addr1)))
    741     (List.append (move_to_dp globals addr1 addr2)
     751    (List.append (move_to_dp globals localss addr1 addr2)
    742752      (List.append (List.Cons ((Joint.LOAD ((Obj.magic a),
    743753        (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil))
    744         (move globals Bool.False dst (Arg_decision_colour I8051.RegisterA))))
     754        (move globals localss Bool.False dst (Arg_decision_colour
     755          I8051.RegisterA))))
    745756
    746757(** val translate_address :
    747     __ List.list -> Bool.bool -> __ -> Interference.decision ->
     758    __ List.list -> Nat.nat -> Bool.bool -> __ -> Interference.decision ->
    748759    Interference.decision -> Joint.joint_seq List.list **)
    749 let translate_address globals carry_lives_after id addr1 addr2 =
     760let translate_address globals localss carry_lives_after id addr1 addr2 =
    750761  preserve_carry_bit (Obj.magic globals)
    751762    (Bool.andb carry_lives_after
     
    754765    (Obj.magic Types.It))),
    755766    (List.append
    756       (move (Obj.magic globals) Bool.False addr1 (Arg_decision_colour
     767      (move (Obj.magic globals) localss Bool.False addr1 (Arg_decision_colour
    757768        I8051.RegisterDPL))
    758       (move (Obj.magic globals) Bool.False addr2 (Arg_decision_colour
     769      (move (Obj.magic globals) localss Bool.False addr2 (Arg_decision_colour
    759770        I8051.RegisterDPH)))))
    760771
    761772(** val translate_low_address :
    762     AST.ident List.list -> Bool.bool -> Interference.decision -> Graphs.label
    763     -> Joint.joint_seq List.list **)
    764 let translate_low_address globals carry_lives_after dst lbl =
     773    AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
     774    Graphs.label -> Joint.joint_seq List.list **)
     775let translate_low_address globals localss carry_lives_after dst lbl =
    765776  match dst with
    766777  | Interference.Decision_spill x ->
    767778    List.Cons ((Joint.Extension_seq
    768779      (Obj.magic (Joint_LTL_LIN.LOW_ADDRESS (I8051.RegisterA, lbl)))),
    769       (move globals carry_lives_after dst (Arg_decision_colour
     780      (move globals localss carry_lives_after dst (Arg_decision_colour
    770781        I8051.RegisterA)))
    771782  | Interference.Decision_colour r ->
     
    774785
    775786(** val translate_high_address :
    776     AST.ident List.list -> Bool.bool -> Interference.decision -> Graphs.label
    777     -> Joint.joint_seq List.list **)
    778 let translate_high_address globals carry_lives_after dst lbl =
     787    AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
     788    Graphs.label -> Joint.joint_seq List.list **)
     789let translate_high_address globals localss carry_lives_after dst lbl =
    779790  match dst with
    780791  | Interference.Decision_spill x ->
    781792    List.Cons ((Joint.Extension_seq
    782793      (Obj.magic (Joint_LTL_LIN.HIGH_ADDRESS (I8051.RegisterA, lbl)))),
    783       (move globals carry_lives_after dst (Arg_decision_colour
     794      (move globals localss carry_lives_after dst (Arg_decision_colour
    784795        I8051.RegisterA)))
    785796  | Interference.Decision_colour r ->
     
    788799
    789800(** val translate_step :
    790     AST.ident List.list -> Fixpoints.valuation -> Interference.coloured_graph
    791     -> Nat.nat -> Graphs.label -> Joint.joint_step -> Blocks.bind_step_block **)
    792 let translate_step globals after grph stack_sz lbl s =
     801    AST.ident List.list -> Nat.nat -> Fixpoints.valuation ->
     802    Interference.coloured_graph -> Nat.nat -> Graphs.label ->
     803    Joint.joint_step -> Blocks.bind_step_block **)
     804let translate_step globals localss after grph stack_sz lbl s =
    793805  Bind_new.Bret
    794806    (let lookup = fun r -> grph.Interference.colouring (Types.Inl r) in
     
    800812    let carry_lives_after = Liveness.hlives I8051.RegisterCarry (after lbl)
    801813    in
    802     let move0 = move globals carry_lives_after in
     814    let move0 = move globals localss carry_lives_after in
    803815    (match s with
    804816     | Joint.COST_LABEL cost_lbl ->
     
    815827          { Types.fst = { Types.fst =
    816828          (Blocks.add_dummy_variance
    817             (move_to_dp globals (Obj.magic lookup_arg dpl)
     829            (move_to_dp globals localss (Obj.magic lookup_arg dpl)
    818830              (Obj.magic lookup_arg dph))); Types.snd = (fun x0 -> Joint.CALL
    819831          ((Types.Inr { Types.fst = (Obj.magic Types.It); Types.snd =
     
    860872          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    861873            globals
    862             (translate_address (Obj.magic globals) carry_lives_after
     874            (translate_address (Obj.magic globals) localss carry_lives_after
    863875              (Obj.magic lbl0) (Obj.magic lookup dpl) (Obj.magic lookup dph))
    864876        | Joint.OPACCS (op, dst1, dst2, arg1, arg2) ->
    865877          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    866878            globals
    867             (translate_opaccs globals carry_lives_after op
     879            (translate_opaccs globals localss carry_lives_after op
    868880              (Obj.magic lookup dst1) (Obj.magic lookup dst2)
    869881              (Obj.magic lookup_arg arg1) (Obj.magic lookup_arg arg2))
     
    871883          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    872884            globals
    873             (translate_op1 globals carry_lives_after op
     885            (translate_op1 globals localss carry_lives_after op
    874886              (Obj.magic lookup dst) (Obj.magic lookup arg))
    875887        | Joint.OP2 (op, dst, arg1, arg2) ->
    876888          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    877889            globals
    878             (translate_op2_smart globals carry_lives_after op
     890            (translate_op2_smart globals localss carry_lives_after op
    879891              (Obj.magic lookup dst) (Obj.magic lookup_arg arg1)
    880892              (Obj.magic lookup_arg arg2))
     
    888900          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    889901            globals
    890             (translate_load globals carry_lives_after (Obj.magic lookup dstr)
    891               (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2))
     902            (translate_load globals localss carry_lives_after
     903              (Obj.magic lookup dstr) (Obj.magic lookup_arg addr1)
     904              (Obj.magic lookup_arg addr2))
    892905        | Joint.STORE (addr1, addr2, srcr) ->
    893906          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
    894907            globals
    895             (translate_store globals carry_lives_after
     908            (translate_store globals localss carry_lives_after
    896909              (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2)
    897910              (Obj.magic lookup_arg srcr))
     
    908921                    (Joint.byte_of_nat stack_sz)))
    909922             | ERTLptr.LOW_ADDRESS (r1, l) ->
    910                translate_low_address globals carry_lives_after (lookup r1) l
     923               translate_low_address globals localss carry_lives_after
     924                 (lookup r1) l
    911925             | ERTLptr.HIGH_ADDRESS (r1, l) ->
    912                translate_high_address globals carry_lives_after (lookup r1) l))))
     926               translate_high_address globals localss carry_lives_after
     927                 (lookup r1) l))))
    913928
    914929(** val translate_fin_step :
     
    939954  TranslateUtils.init_params = (Obj.magic Types.It);
    940955  TranslateUtils.init_stack_size = stack_sz; TranslateUtils.added_prologue =
    941   List.Nil; TranslateUtils.f_step =
    942   (translate_step globals after coloured_graph stack_sz);
    943   TranslateUtils.f_fin = (translate_fin_step globals) }
    944 
    945 (** val first_free_stack_addr : LTL.ltl_program -> Nat.nat **)
    946 let first_free_stack_addr p =
    947   let globals_addr_internal = fun offset x_size ->
    948     let { Types.fst = eta4401; Types.snd = size } = x_size in
    949     let { Types.fst = x; Types.snd = region } = eta4401 in
    950     Nat.plus offset size
    951   in
    952   Util.foldl globals_addr_internal Nat.O p.AST.prog_vars
     956  List.Nil; TranslateUtils.new_regs = List.Nil; TranslateUtils.f_step =
     957  (translate_step globals (Types.pi1 int_fun).Joint.joint_if_local_stacksize
     958    after coloured_graph stack_sz); TranslateUtils.f_fin =
     959  (translate_fin_step globals) }
    953960
    954961(** val ertlptr_to_ltl :
     
    959966  let ltlprog =
    960967    TranslateUtils.b_graph_transform_program ERTLptr.eRTLptr LTL.lTL
    961       (translate_data the_fixpoint build) pr
     968      (fun globals h -> translate_data the_fixpoint build globals h) pr
    962969  in
    963970  { Types.fst = { Types.fst = ltlprog; Types.snd =
     
    967974    (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    968975      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    969       Nat.O))))))))))))))))) (first_free_stack_addr ltlprog)) }
    970 
     976      Nat.O)))))))))))))))))
     977    (Joint.globals_stacksize (Joint.graph_params_to_params LTL.lTL) ltlprog)) }
     978
Note: See TracChangeset for help on using the changeset viewer.