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/rTLToERTL.ml

    r2773 r2827  
    165165
    166166(** val get_params_stack :
    167     AST.ident List.list -> Registers.register List.list ->
    168     (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
    169 let get_params_stack globals params =
    170   Bind_new.Bnew (fun tmpr -> Bind_new.Bnew (fun addr1 -> Bind_new.Bnew
    171     (fun addr2 ->
    172     let params_length_byte =
    173       Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    174         (Nat.S (Nat.S Nat.O)))))))) (List.length params)
    175     in
    176     let l =
    177       List.append (List.Cons
    178         ((let x =
    179             ERTL.ertl_seq_joint globals
    180               (Obj.magic (ERTL.Ertl_frame_size tmpr))
    181           in
    182          x), (List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.OP2
    183         (BackEndOps.Sub, (Obj.magic tmpr),
    184         (Obj.magic (Joint.psd_argument_from_reg tmpr)),
    185         (Obj.magic (Joint.psd_argument_from_byte params_length_byte)))),
    186         (List.Cons ((Joint.MOVE
    187         (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
    188           (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
    189         (List.Cons ((Joint.MOVE
    190         (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
    191           (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
    192         (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic addr1),
    193         (Obj.magic (Joint.psd_argument_from_reg addr1)),
    194         (Obj.magic (Joint.psd_argument_from_reg tmpr)))), (List.Cons
    195         ((Joint.OP2 (BackEndOps.Addc, (Obj.magic addr2),
    196         (Obj.magic (Joint.psd_argument_from_reg addr2)),
    197         (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
    198         List.Nil))))))))))))))
    199         (List.flatten
    200           (List.map (get_param_stack globals addr1 addr2) params))
    201     in
    202     Bind_new.Bret l)))
     167    AST.ident List.list -> Registers.register -> Registers.register ->
     168    Registers.register -> Registers.register List.list -> Joint.joint_seq
     169    List.list **)
     170let get_params_stack globals tmpr addr1 addr2 params =
     171  let params_length_byte =
     172    Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     173      (Nat.S (Nat.S Nat.O)))))))) (List.length params)
     174  in
     175  List.append (List.Cons
     176    ((let x =
     177        ERTL.ertl_seq_joint globals (Obj.magic (ERTL.Ertl_frame_size tmpr))
     178      in
     179     x), (List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.OP2
     180    (BackEndOps.Sub, (Obj.magic tmpr),
     181    (Obj.magic (Joint.psd_argument_from_reg tmpr)),
     182    (Obj.magic (Joint.psd_argument_from_byte params_length_byte)))),
     183    (List.Cons ((Joint.MOVE
     184    (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
     185      (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })), (List.Cons
     186    ((Joint.MOVE
     187    (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
     188      (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })), (List.Cons
     189    ((Joint.OP2 (BackEndOps.Add, (Obj.magic addr1),
     190    (Obj.magic (Joint.psd_argument_from_reg addr1)),
     191    (Obj.magic (Joint.psd_argument_from_reg tmpr)))), (List.Cons ((Joint.OP2
     192    (BackEndOps.Addc, (Obj.magic addr2),
     193    (Obj.magic (Joint.psd_argument_from_reg addr2)),
     194    (Obj.magic (Joint.psd_argument_from_byte Joint.zero_byte)))),
     195    List.Nil))))))))))))))
     196    (List.flatten (List.map (get_param_stack globals addr1 addr2) params))
    203197
    204198(** val get_params :
    205     AST.ident List.list -> Registers.register List.list ->
    206     (Registers.register, Joint.joint_seq) BindLists.bind_list **)
    207 let get_params globals params =
     199    AST.ident List.list -> Registers.register -> Registers.register ->
     200    Registers.register -> Registers.register List.list -> Joint.joint_seq
     201    List.list **)
     202let get_params globals tmpr addr1 addr2 params =
    208203  let n = Nat.min (List.length params) (List.length I8051.registerParams) in
    209204  let { Types.fst = hdw_params; Types.snd = stack_params } =
    210205    Util.list_split n params
    211206  in
    212   BindLists.bappend
    213     (let l = get_params_hdw globals hdw_params in Bind_new.Bret l)
    214     (get_params_stack globals stack_params)
     207  List.append (get_params_hdw globals hdw_params)
     208    (get_params_stack globals tmpr addr1 addr2 stack_params)
    215209
    216210(** val save_return :
     
    260254(** val prologue :
    261255    AST.ident List.list -> Registers.register List.list -> Registers.register
    262     -> Registers.register -> (Registers.register, I8051.register) Types.prod
     256    -> Registers.register -> Registers.register -> Registers.register ->
     257    Registers.register -> (Registers.register, I8051.register) Types.prod
    263258    List.list -> (Registers.register, Joint.joint_seq List.list)
    264259    Bind_new.bind_new **)
    265 let prologue globals params sral srah sregs =
    266   BindLists.bappend
    267     (let l = List.Cons
    268        ((let x = ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_new_frame)
    269          in
    270         x), (List.Cons ((Joint.POP (Obj.magic sral)), (List.Cons ((Joint.POP
    271        (Obj.magic srah)), List.Nil)))))
    272      in
    273     Bind_new.Bret l)
    274     (BindLists.bappend (let l = save_hdws globals sregs in Bind_new.Bret l)
    275       (get_params globals params))
     260let prologue globals params sral srah tmpr addr1 addr2 sregs =
     261  let l =
     262    List.append (List.Cons
     263      ((let x = ERTL.ertl_seq_joint globals (Obj.magic ERTL.Ertl_new_frame)
     264        in
     265       x), (List.Cons ((Joint.POP (Obj.magic sral)), (List.Cons ((Joint.POP
     266      (Obj.magic srah)), List.Nil))))))
     267      (List.append (save_hdws globals sregs)
     268        (get_params globals tmpr addr1 addr2 params))
     269  in
     270  Bind_new.Bret l
    276271
    277272(** val set_params_hdw :
     
    377372    Joint.COND (r, ltrue)) }; Types.snd = List.Nil }
    378373| Joint.Step_seq s0 ->
    379   (match s0 with
    380    | Joint.COMMENT msg ->
    381      Bind_new.Bret
    382        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    383          globals (List.Cons ((Joint.COMMENT msg), List.Nil)))
    384    | Joint.MOVE rs ->
    385      Bind_new.Bret
    386        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     374  Bind_new.Bret
     375    (match s0 with
     376     | Joint.COMMENT msg ->
     377       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     378         globals (List.Cons ((Joint.COMMENT msg), List.Nil))
     379     | Joint.MOVE rs ->
     380       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    387381         globals (List.Cons ((Joint.MOVE
    388382         (Obj.magic { Types.fst = (ERTL.PSD (Obj.magic rs).Types.fst);
    389383           Types.snd =
    390384           (ERTL.psd_argument_move_src (Obj.magic rs).Types.snd) })),
    391          List.Nil)))
    392    | Joint.POP x0 ->
    393      Bind_new.Bret
    394        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    395          globals List.Nil)
    396    | Joint.PUSH x0 ->
    397      Bind_new.Bret
    398        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    399          globals List.Nil)
    400    | Joint.ADDRESS (x0, r1, r2) ->
    401      Bind_new.Bret
    402        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    403          globals (List.Cons ((Joint.ADDRESS (x0, r1, r2)), List.Nil)))
    404    | Joint.OPACCS (op, destr1, destr2, srcr1, srcr2) ->
    405      Bind_new.Bret
    406        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     385         List.Nil))
     386     | Joint.POP x0 ->
     387       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     388         globals List.Nil
     389     | Joint.PUSH x0 ->
     390       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     391         globals List.Nil
     392     | Joint.ADDRESS (x0, r1, r2) ->
     393       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     394         globals (List.Cons ((Joint.ADDRESS (x0, r1, r2)), List.Nil))
     395     | Joint.OPACCS (op, destr1, destr2, srcr1, srcr2) ->
     396       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    407397         globals (List.Cons ((Joint.OPACCS (op, destr1, destr2, srcr1,
    408          srcr2)), List.Nil)))
    409    | Joint.OP1 (op1, destr, srcr) ->
    410      Bind_new.Bret
    411        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    412          globals (List.Cons ((Joint.OP1 (op1, destr, srcr)), List.Nil)))
    413    | Joint.OP2 (op2, destr, srcr1, srcr2) ->
    414      Bind_new.Bret
    415        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     398         srcr2)), List.Nil))
     399     | Joint.OP1 (op1, destr, srcr) ->
     400       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     401         globals (List.Cons ((Joint.OP1 (op1, destr, srcr)), List.Nil))
     402     | Joint.OP2 (op2, destr, srcr1, srcr2) ->
     403       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    416404         globals (List.Cons ((Joint.OP2 (op2, destr, srcr1, srcr2)),
    417          List.Nil)))
    418    | Joint.CLEAR_CARRY ->
    419      Bind_new.Bret
    420        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    421          globals (List.Cons (Joint.CLEAR_CARRY, List.Nil)))
    422    | Joint.SET_CARRY ->
    423      Bind_new.Bret
    424        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    425          globals (List.Cons (Joint.SET_CARRY, List.Nil)))
    426    | Joint.LOAD (destr, addr1, addr2) ->
    427      Bind_new.Bret
    428        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    429          globals (List.Cons ((Joint.LOAD (destr, addr1, addr2)), List.Nil)))
    430    | Joint.STORE (addr1, addr2, srcr) ->
    431      Bind_new.Bret
    432        (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    433          globals (List.Cons ((Joint.STORE (addr1, addr2, srcr)), List.Nil)))
    434    | Joint.Extension_seq ext ->
    435      let RTL.Rtl_stack_address (addr1, addr2) = Obj.magic ext in
    436      Bind_new.Bret
    437      (Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
    438        globals (List.Cons ((Joint.MOVE
    439        (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
    440          (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
    441        (List.Cons ((Joint.MOVE
    442        (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
    443          (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
    444        List.Nil))))))
     405         List.Nil))
     406     | Joint.CLEAR_CARRY ->
     407       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     408         globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
     409     | Joint.SET_CARRY ->
     410       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     411         globals (List.Cons (Joint.SET_CARRY, List.Nil))
     412     | Joint.LOAD (destr, addr1, addr2) ->
     413       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     414         globals (List.Cons ((Joint.LOAD (destr, addr1, addr2)), List.Nil))
     415     | Joint.STORE (addr1, addr2, srcr) ->
     416       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     417         globals (List.Cons ((Joint.STORE (addr1, addr2, srcr)), List.Nil))
     418     | Joint.Extension_seq ext ->
     419       let RTL.Rtl_stack_address (addr1, addr2) = Obj.magic ext in
     420       Blocks.ensure_step_block (Joint.graph_params_to_params ERTL.eRTL)
     421         globals (List.Cons ((Joint.MOVE
     422         (Obj.magic { Types.fst = (ERTL.PSD addr1); Types.snd =
     423           (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPL)) })),
     424         (List.Cons ((Joint.MOVE
     425         (Obj.magic { Types.fst = (ERTL.PSD addr2); Types.snd =
     426           (ERTL.move_src_from_dst (ERTL.HDW I8051.registerSPH)) })),
     427         List.Nil)))))
    445428
    446429(** val translate_fin_step :
     
    459442
    460443(** val allocate_regs :
    461     (Registers.register -> Registers.register -> (Registers.register,
    462     I8051.register) Types.prod List.list -> (Registers.register, 'a1)
    463     Bind_new.bind_new) -> (Registers.register, 'a1) Bind_new.bind_new **)
     444    ((Registers.register, I8051.register) Types.prod List.list ->
     445    (Registers.register, 'a1) Bind_new.bind_new) -> (Registers.register, 'a1)
     446    Bind_new.bind_new **)
    464447let allocate_regs f =
    465   Bind_new.Bnew (fun ral -> Bind_new.Bnew (fun rah ->
    466     let allocate_regs_internal = fun acc r ->
    467       Monad.m_bind0 (Monad.max_def Bind_new.bindNew) acc (fun tl ->
    468         Obj.magic (Bind_new.Bnew (fun r' ->
    469           Obj.magic
    470             (Monad.m_return0 (Monad.max_def Bind_new.bindNew) (List.Cons
    471               ({ Types.fst = r'; Types.snd = r }, tl))))))
    472     in
    473     Obj.magic
    474       (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
    475         (Util.foldl allocate_regs_internal
    476           (Monad.m_return0 (Monad.max_def Bind_new.bindNew) List.Nil)
    477           I8051.registerCalleeSaved) (fun to_save ->
    478         Obj.magic f ral rah to_save))))
     448  let allocate_regs_internal = fun acc r ->
     449    Monad.m_bind0 (Monad.max_def Bind_new.bindNew) acc (fun tl ->
     450      Obj.magic (Bind_new.Bnew (fun r' ->
     451        Obj.magic
     452          (Monad.m_return0 (Monad.max_def Bind_new.bindNew) (List.Cons
     453            ({ Types.fst = r'; Types.snd = r }, tl))))))
     454  in
     455  Obj.magic
     456    (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
     457      (Util.foldl allocate_regs_internal
     458        (Monad.m_return0 (Monad.max_def Bind_new.bindNew) List.Nil)
     459        I8051.registerCalleeSaved) (fun to_save -> Obj.magic f to_save))
    479460
    480461(** val translate_data :
    481462    AST.ident List.list -> Joint.joint_closed_internal_function ->
    482     (Registers.register, TranslateUtils.b_graph_translate_data)
    483     Bind_new.bind_new **)
     463    TranslateUtils.bound_b_graph_translate_data **)
    484464let translate_data globals def =
    485465  let params = (Types.pi1 def).Joint.joint_if_params in
     
    489469        (List.length I8051.registerParams))
    490470  in
    491   allocate_regs (fun ral rah to_save ->
     471  allocate_regs (fun to_save -> Bind_new.Bnew (fun ral -> Bind_new.Bnew
     472    (fun rah -> Bind_new.Bnew (fun tmpr -> Bind_new.Bnew (fun addr1 ->
     473    Bind_new.Bnew (fun addr2 ->
    492474    Obj.magic
    493475      (Monad.m_bind0 (Monad.max_def Bind_new.bindNew)
    494         (Obj.magic (prologue globals (Obj.magic params) ral rah to_save))
    495         (fun prologue0 ->
     476        (Obj.magic
     477          (prologue globals (Obj.magic params) ral rah tmpr addr1 addr2
     478            to_save)) (fun prologue0 ->
    496479        Monad.m_return0 (Monad.max_def Bind_new.bindNew)
    497480          { TranslateUtils.init_ret = (Obj.magic Types.It);
     
    499482          (Obj.magic (List.length (Obj.magic params)));
    500483          TranslateUtils.init_stack_size = new_stacksize;
    501           TranslateUtils.added_prologue = prologue0; TranslateUtils.f_step =
    502           (translate_step globals); TranslateUtils.f_fin =
     484          TranslateUtils.added_prologue = prologue0;
     485          TranslateUtils.new_regs = (List.Cons (addr2, (List.Cons (addr1,
     486          (List.Cons (tmpr, (List.Cons (rah, (List.Cons (ral,
     487          (List.map (fun x -> x.Types.fst) to_save)))))))))));
     488          TranslateUtils.f_step = (translate_step globals);
     489          TranslateUtils.f_fin =
    503490          (translate_fin_step globals
    504491            (Obj.magic (Types.pi1 def).Joint.joint_if_result) ral rah
    505             to_save) })))
     492            to_save) }))))))))
    506493
    507494(** val rtl_to_ertl : RTL.rtl_program -> ERTL.ertl_program **)
Note: See TracChangeset for help on using the changeset viewer.