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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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 :
Note: See TracChangeset for help on using the changeset viewer.