Changeset 1081 for src


Ignore:
Timestamp:
Jul 20, 2011, 11:26:21 AM (9 years ago)
Author:
mulligan
Message:

completed rtl-ertl pass

Location:
src/RTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLTailcall.ma

    r1080 r1081  
    11include "RTL/RTL.ma".
    2 
    3 (* dpm: this should not be option, fix *)
    4 axiom map_fold:
    5   ∀A, B: Type[0].
    6   ∀f: label → A → B → option B.
    7   ∀m: rtl_statement_graph.
    8   ∀b: B.
    9     B.
    102
    113definition simplify_stmt ≝
     
    2113  | _ ⇒ graph
    2214  ].
    23  
    24 definition lift_option3: ∀A, B, C, D. ∀f: A → B → C → D. A → B → C → option D ≝
    25   λA, B, C, D: Type[0].
    26   λf: A → B → C → D.
    27   λa: A.
    28   λb: B.
    29   λc: C.
    30     Some ? (f a b c).
    31  
     15
    3216definition simplify_graph ≝
    33   λexit.
     17  λexit: label.
    3418  λgraph: rtl_statement_graph.
    35     map_fold ? ? (lift_option3 ? ? ? ? (simplify_stmt exit)) graph graph.
     19    foldi ? ? ? (simplify_stmt exit) graph graph.
     20
     21axiom simplify_graph_preserves_labels:
     22  ∀g: rtl_statement_graph.
     23  ∀l: label.
     24  ∀exit: label.
     25    lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph exit g) l ≠ None ?.
    3626   
    3727definition simplify_internal ≝
     
    5040        rtl_if_result' rtl_if_params' rtl_if_locals' rtl_if_stacksize'
    5141        rtl_if_graph' ? ?.
    52   [1: normalize nodelta;
     42  normalize nodelta
     43  [1: cases rtl_if_entry'
     44      #ENTRY #ENTRY_PRF
     45      %
     46      [1: @ENTRY
     47      |2: @simplify_graph_preserves_labels
     48          @ENTRY_PRF
     49      ]
     50  |2: cases rtl_if_exit'
     51      #EXIT #EXIT_PRF
     52      %
     53      [1: @EXIT
     54      |2: @simplify_graph_preserves_labels
     55          @EXIT_PRF
     56      ]
     57  ]
     58qed.
    5359
    5460definition simplify_funct ≝
     
    5763  let def' ≝
    5864    match def with
    59     [ rtl_f_internal def ⇒ rtl_f_internal (simplify_internal def)
    60     | rtl_f_external def ⇒ rtl_f_external def
    61     ] in
    62   〈id, def'〉.
     65    [ Internal def ⇒ Internal ? (simplify_internal def)
     66    | External def ⇒ External ? def
     67    ]
     68  in
     69    〈id, def'〉.
    6370 
    6471definition tailcall_simplify ≝
  • src/RTL/RTLtoERTL.ma

    r1079 r1081  
    669669  let vars ≝ map ? ? f (rtl_pr_functs p) in
    670670    mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p).
    671 
    672 let translate p =
    673   (* We simplify tail calls as regular calls for now. *)
    674   let p = RTLtailcall.simplify p in
    675   (* The tranformation on each RTL function: create an ERTL function and move
    676      its first cost label at the very beginning. *)
    677   let f funct = move_first_cost_label_up (translate_funct funct) in
    678   { ERTL.vars   = p.RTL.vars ;
    679     ERTL.functs = List.map f p.RTL.functs ;
    680     ERTL.main   = p.RTL.main }
    681 
    682 definition save_return_internal ≝
    683   λr.
    684   λstart_lbl.
    685   λdest_lbl.
    686   λdef.
    687   let 〈def, r_tmp〉 ≝ fresh_reg def in
    688   adds_graph [
    689     ertl_st_int r_tmp (bitvector_of_nat ? 0) start_lbl;
    690     ertl_st_set_hdw RegisterST0 r start_lbl;
    691     ertl_st_set_hdw RegisterST1 r_tmp start_lbl ] start_lbl dest_lbl def.
    692    
    693 definition save_return_internal' ≝
    694   λr1, r2.
    695   λstart_lbl.
    696   adds_graph [
    697     ertl_st_set_hdw RegisterST0 r1 start_lbl;
    698     ertl_st_set_hdw RegisterST1 r2 start_lbl
    699   ] start_lbl.
    700    
    701 definition save_return ≝
    702   λret_regs.
    703   match ret_regs with
    704   [ nil ⇒ [ get_params_hdw_internal ]
    705   | cons hd tl ⇒
    706     match tl with
    707     [ nil ⇒ [ save_return_internal hd ]
    708     | cons hd' tl' ⇒ [ save_return_internal' hd hd' ]
    709     ]
    710   ].
    711    
    712 definition add_epilogue ≝
    713   λret_regs.
    714   λsral.
    715   λsrah.
    716   λsregs.
    717   λdef.
    718   let start_lbl ≝ ertl_if_exit def in
    719   let tmp_lbl ≝ fresh_label def in
    720   match tmp_lbl with
    721   [ None ⇒ None ?
    722   | Some tmp_lbl ⇒
    723     let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
    724     match last_stmt with
    725     [ None ⇒ None ?
    726     | Some last_stmt ⇒
    727       let def ≝
    728         add_translates (
    729           save_return ret_regs @
    730           restore_hdws sregs @
    731           [adds_graph [
    732             ertl_st_push srah start_lbl;
    733             ertl_st_push sral start_lbl
    734           ]] @
    735           [adds_graph [
    736             ertl_st_del_frame start_lbl
    737           ]] @
    738           [adds_graph [
    739             ertl_st_hdw_to_hdw RegisterDPL RegisterST0 start_lbl;
    740             ertl_st_hdw_to_hdw RegisterDPH RegisterST1 start_lbl
    741           ]]) start_lbl tmp_lbl def in
    742       match def with
    743       [ None ⇒ None ?
    744       | Some def ⇒
    745         let def ≝ add_graph tmp_lbl last_stmt def in
    746           Some ? (change_exit_label tmp_lbl def)
    747       ]
    748     ]
    749   ].
    750  
    751 axiom add_pro_and_epilogue:
    752   ∀rs: register_set.
    753   ∀params: list register.
    754   ∀ret_args: list register.
    755   ∀def: ertl_internal_function.
    756     option ertl_internal_function.
    757    
    758 (*
    759   dpm: address callee_saved problem   
    760 definition add_pro_and_epilogue ≝
    761   λrs: register_set.
    762   λparams.
    763   λret_args.
    764   λdef.
    765   let 〈def, sra〉 ≝ fresh_regs def 2 in
    766   let sral ≝ safe_nth ? 0 sra ? in
    767   let srah ≝ safe_nth ? 1 sra ? in
    768   let 〈def, sregs〉 ≝ allocate_regs callee_saved def in
    769   let def ≝ add_prologue params sral srah sregs def in
    770   let def ≝ add_epilogue ret_args sral srah sregs def in
    771     def. 
    772 *)
    773 
    774 definition set_params_hdw ≝
    775   λparams.
    776   match length ? params with
    777   [ O ⇒ Some ? [ get_params_hdw_internal ]
    778   | _ ⇒
    779     match zip ? ? params parameters with
    780     [ None ⇒ None ?
    781     | Some zipped_params ⇒ Some ? (restore_hdws zipped_params)
    782     ]
    783   ].
    784  
    785 definition set_param_stack ≝
    786   λoff: nat.
    787   λsrcr.
    788   λstart_lbl, dest_lbl: label.
    789   λdef.
    790   let 〈def, addr1〉 ≝ fresh_reg def in
    791   let 〈def, addr2〉 ≝ fresh_reg def in
    792   let 〈def, tmpr〉 ≝ fresh_reg def in
    793   let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
    794     adds_graph [
    795       ertl_st_int addr2 int_offset start_lbl;
    796       ertl_st_get_hdw tmpr RegisterSPL start_lbl;
    797       ertl_st_clear_carry start_lbl;
    798       ertl_st_op2 Sub addr1 tmpr addr1 start_lbl;
    799       ertl_st_get_hdw tmpr RegisterSPH start_lbl;
    800       ertl_st_int addr2 (bitvector_of_nat ? 0) start_lbl;
    801       ertl_st_op2 Sub addr2 tmpr addr2 start_lbl;
    802       ertl_st_store addr1 addr2 srcr start_lbl
    803     ] start_lbl dest_lbl def.
    804 
    805 definition set_params_stack ≝
    806   λparams.
    807   match length ? params with
    808   [ O ⇒ [ get_params_hdw_internal ]
    809   | _ ⇒ mapi ? ? set_param_stack params
    810  
    811   ].
    812  
    813 definition set_params ≝
    814   λparams.
    815   let n ≝ min (length ? params) (length ? parameters) in
    816   let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
    817     match set_params_hdw hdw_params with
    818     [ None ⇒ None ?
    819     | Some hdw_params' ⇒ Some ? (hdw_params' @ (set_params_stack stack_params))
    820     ].
    821    
    822 definition fetch_result ≝
    823   λret_regs.
    824   λstart_lbl.
    825   match ret_regs with
    826   [ nil ⇒ adds_graph [ertl_st_skip start_lbl] start_lbl
    827   | cons hd tl ⇒
    828     match tl with
    829     [ nil ⇒
    830       adds_graph [
    831         ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
    832         ertl_st_get_hdw hd RegisterST0 start_lbl
    833       ] start_lbl
    834     | cons hd' tl' ⇒
    835       adds_graph [
    836         ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
    837         ertl_st_hdw_to_hdw RegisterST1 RegisterDPH start_lbl;
    838         ertl_st_get_hdw hd RegisterST0 start_lbl;
    839         ertl_st_get_hdw hd' RegisterST1 start_lbl
    840       ] start_lbl
    841     ]
    842   ].
    843  
    844 definition translate_call_id ≝
    845   λf.
    846   λargs.
    847   λret_regs.
    848   λstart_lbl, dest_lbl: label.
    849   λdef.
    850   let nb_args ≝ bitvector_of_nat ? (length ? args) in
    851   match set_params args with
    852   [ None ⇒ None ?
    853   | Some params_args ⇒
    854     add_translates (
    855       params_args @ [
    856         adds_graph [ ertl_st_call_id f nb_args start_lbl ] ;
    857         fetch_result ret_regs
    858       ]) start_lbl dest_lbl def
    859   ].
    860  
    861 definition translate_stmt ≝
    862   λlbl: label.
    863   λstmt: rtl_statement.
    864   λdef: ertl_internal_function.
    865   match stmt with
    866   [ rtl_st_skip lbl' ⇒
    867     Some ? (add_graph lbl (ertl_st_skip lbl') def)
    868   | rtl_st_cost cost_lbl lbl' ⇒
    869     Some ? (add_graph lbl (ertl_st_cost cost_lbl lbl') def)
    870   | rtl_st_addr r1 r2 x lbl' ⇒
    871     adds_graph [
    872       ertl_st_addr_l r1 x lbl;
    873       ertl_st_addr_h r2 x lbl
    874     ] lbl lbl' def
    875   | rtl_st_stack_addr r1 r2 lbl' ⇒
    876     adds_graph [
    877       ertl_st_get_hdw r1 RegisterSPL lbl;
    878       ertl_st_get_hdw r2 RegisterSPH lbl
    879     ] lbl lbl' def
    880   | rtl_st_int r i lbl' ⇒
    881     Some ? (add_graph lbl (ertl_st_int r i lbl') def)
    882   | rtl_st_move r1 r2 lbl' ⇒
    883     Some ? (add_graph lbl (ertl_st_move r1 r2 lbl') def)
    884   | rtl_st_opaccs opaccs d s1 s2 lbl' ⇒
    885     Some ? (add_graph lbl (ertl_st_opaccs opaccs d s1 s2 lbl') def)
    886   | rtl_st_op1 op1 d s lbl' ⇒
    887     Some ? (add_graph lbl (ertl_st_op1 op1 d s lbl') def)
    888   | rtl_st_op2 op2 d s1 s2 lbl' ⇒
    889     Some ? (add_graph lbl (ertl_st_op2 op2 d s1 s2 lbl') def)
    890   | rtl_st_clear_carry lbl' ⇒
    891     Some ? (add_graph lbl (ertl_st_clear_carry lbl') def)
    892   | rtl_st_load d a1 a2 lbl' ⇒
    893     Some ? (add_graph lbl (ertl_st_load d a1 a2 lbl') def)
    894   | rtl_st_store a1 a2 s lbl' ⇒
    895     Some ? (add_graph lbl (ertl_st_store a1 a2 s lbl') def)
    896   | rtl_st_call_id f args ret_regs lbl' ⇒
    897     translate_call_id f args ret_regs lbl lbl' def
    898   | rtl_st_call_ptr r1 r2 regs1 regs2 lbl ⇒ None ? (* dpm: todo *)
    899   | rtl_st_cond_acc src lbl_true lbl_false ⇒
    900     Some ? (add_graph lbl (ertl_st_cond_acc src lbl_true lbl_false) def)
    901   | rtl_st_return ret_regs ⇒
    902     Some ? (add_graph lbl (ertl_st_return ret_regs) def)
    903   | rtl_st_tailcall_id ident regs ⇒ None ? (* dpm: impossible *)
    904   | rtl_st_tailcall_ptr r1 r2 regs ⇒ None ? (* dpm: impossible *)
    905   ].
    906    
    907 definition translate_funct_internal ≝
    908   λdef.
    909   let nb_params ≝ length ? (rtl_if_params def) in
    910   let added_stacksize ≝ max 0 (nb_params - (length ? parameters)) in
    911   let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
    912   let def' ≝
    913     mk_ertl_internal_function
    914       (rtl_if_luniverse def) (rtl_if_runiverse def)
    915       nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
    916       (empty_map ? ?) (rtl_if_entry def) (rtl_if_exit def) in
    917   let def' ≝ map_fold ? ? translate_stmt (rtl_if_graph def) def' in
    918   let def' ≝ add_pro_and_epilogue register_list_set (rtl_if_params def) (rtl_if_result def) def' in
    919     def'.
    920    
    921 definition translate_funct ≝
    922   λid_def: ident × ?.
    923   let 〈id, def〉 ≝ id_def in
    924   let def' ≝
    925     match def with
    926     [ rtl_f_internal def ⇒
    927       match translate_funct_internal def with
    928       [ None ⇒ None ?
    929       | Some internal_def ⇒ Some ? (ertl_f_internal internal_def)
    930       ]
    931     | rtl_f_external def ⇒ Some ? (ertl_f_external def)
    932     ] in
    933   〈id, def'〉.
    934 
    935 definition generate ≝
    936   λstmt.
    937   λdef.
    938   let entry ≝ fresh_label def in
    939   match entry with
    940   [ None ⇒ None ?
    941   | Some entry ⇒
    942     let def ≝ add_graph entry stmt def in
    943       Some ? (change_entry_label entry def)
    944   ].
    945  
    946 let rec find_and_remove_first_cost_label_internal (def: ertl_internal_function)
    947                                                   (lbl: label) (n: nat) on n ≝
    948   match n with
    949   [ O ⇒ None ?
    950   | S n' ⇒
    951     let statement_at_label ≝ lookup ? ? (ertl_if_graph def) lbl in
    952     match statement_at_label with
    953     [ None ⇒ None ?
    954     | Some statement ⇒
    955       match statement with
    956       [ ertl_st_cost cost_lbl next_lbl ⇒
    957         let def' ≝ add_graph lbl (ertl_st_skip next_lbl) def in
    958           Some ? 〈Some ? cost_lbl, def'〉
    959       | ertl_st_cond_acc _ _ _ ⇒ Some ? 〈None ?, def〉
    960       | ertl_st_return _⇒ Some ? 〈None ?, def〉
    961       | ertl_st_skip lbl' ⇒ find_and_remove_first_cost_label_internal def lbl' n'
    962       | ertl_st_comment _ lbl' ⇒
    963         find_and_remove_first_cost_label_internal def lbl' n'
    964       | ertl_st_get_hdw _ _ lbl' ⇒
    965         find_and_remove_first_cost_label_internal def lbl' n'
    966       | ertl_st_set_hdw _ _ lbl' ⇒
    967         find_and_remove_first_cost_label_internal def lbl' n'
    968       | ertl_st_hdw_to_hdw _ _ lbl' ⇒
    969         find_and_remove_first_cost_label_internal def lbl' n'
    970       | ertl_st_pop _ lbl' ⇒
    971         find_and_remove_first_cost_label_internal def lbl' n'
    972       | ertl_st_push _ lbl' ⇒
    973         find_and_remove_first_cost_label_internal def lbl' n'
    974       | ertl_st_addr_h _ _ lbl' ⇒
    975         find_and_remove_first_cost_label_internal def lbl' n'
    976       | ertl_st_addr_l _ _ lbl' ⇒
    977         find_and_remove_first_cost_label_internal def lbl' n'
    978       | ertl_st_int _ _ lbl' ⇒
    979         find_and_remove_first_cost_label_internal def lbl' n'
    980       | ertl_st_move _ _ lbl' ⇒
    981         find_and_remove_first_cost_label_internal def lbl' n'
    982       | ertl_st_opaccs _ _ _ _ lbl' ⇒
    983         find_and_remove_first_cost_label_internal def lbl' n'
    984       | ertl_st_op2 _ _ _ _ lbl' ⇒
    985         find_and_remove_first_cost_label_internal def lbl' n'
    986       | ertl_st_op1 _ _ _ lbl' ⇒
    987         find_and_remove_first_cost_label_internal def lbl' n'
    988       | ertl_st_clear_carry lbl' ⇒
    989         find_and_remove_first_cost_label_internal def lbl' n'
    990       | ertl_st_load _ _ _ lbl' ⇒
    991         find_and_remove_first_cost_label_internal def lbl' n'
    992       | ertl_st_store _ _ _ lbl' ⇒
    993         find_and_remove_first_cost_label_internal def lbl' n'
    994       | ertl_st_call_id _ _ lbl' ⇒
    995         find_and_remove_first_cost_label_internal def lbl' n'
    996       | ertl_st_new_frame lbl' ⇒
    997         find_and_remove_first_cost_label_internal def lbl' n'
    998       | ertl_st_del_frame lbl' ⇒
    999         find_and_remove_first_cost_label_internal def lbl' n'
    1000       | ertl_st_frame_size _ lbl' ⇒
    1001         find_and_remove_first_cost_label_internal def lbl' n'
    1002       ]
    1003     ]
    1004   ].
    1005  
    1006 axiom num_entries:
    1007   ∀A: Type[0].
    1008   ∀g: graph A.
    1009     nat.
    1010  
    1011 definition find_and_remove_first_cost_label ≝
    1012   λdef.
    1013     find_and_remove_first_cost_label_internal def (ertl_if_entry def) (num_entries ? (ertl_if_graph def)).
    1014 
    1015 definition move_first_cost_label_up_internal ≝
    1016   λdef.
    1017   let cost_label_def ≝ find_and_remove_first_cost_label def in
    1018   match cost_label_def with
    1019   [ None ⇒ None ?
    1020   | Some cost_label_def ⇒
    1021     let 〈cost_label, def〉 ≝ cost_label_def in
    1022     match cost_label with
    1023     [ None ⇒ Some ? def
    1024     | Some cost_label ⇒ generate (ertl_st_cost cost_label (ertl_if_entry def)) def
    1025     ]
    1026   ].
    1027  
    1028 definition move_first_cost_label_up ≝
    1029   λid_def: ident × ?.
    1030   let 〈id, def〉 ≝ id_def in
    1031   let def' ≝
    1032     match def with 
    1033     [ ertl_f_internal int_fun ⇒
    1034       let cost_label_def ≝ move_first_cost_label_up_internal int_fun in
    1035       match cost_label_def with
    1036       [ None ⇒ None ?
    1037       | Some cost_label_def ⇒
    1038           Some ? (ertl_f_internal cost_label_def)
    1039       ]
    1040     | ertl_f_external _ ⇒ Some ? def
    1041     ] in
    1042   match def' with
    1043   [ None ⇒ None ?
    1044   | Some def' ⇒ Some ? 〈id, def'〉
    1045   ].
    1046  
    1047 definition translate_internal ≝
    1048   λfunct.
    1049     let 〈id, funct〉 ≝ translate_funct funct in
    1050     match funct with
    1051     [ None ⇒ None ?
    1052     | Some funct ⇒ move_first_cost_label_up 〈id, funct〉
    1053     ].
    1054 
    1055 let rec strip_none (A: Type[0]) (l: list (option A)) on l: list A ≝
    1056   match l with
    1057   [ nil ⇒ nil ?
    1058   | cons hd tl ⇒
    1059     match hd with
    1060     [ None ⇒ strip_none A tl
    1061     | Some hd ⇒ hd :: strip_none A tl
    1062     ]
    1063   ].
    1064  
    1065 definition translate: rtl_program → ertl_program ≝
    1066   λp.
    1067   let p ≝ tailcall_simplify p in
    1068   let rtl_pr_vars' ≝ rtl_pr_vars p in
    1069   let rtl_pr_functs' ≝ map … translate_internal (rtl_pr_functs p) in
    1070   let rtl_pr_functs_filtered ≝ strip_none ? rtl_pr_functs' in
    1071   let rtl_pr_main' ≝ rtl_pr_main p in
    1072     mk_ertl_program rtl_pr_vars' rtl_pr_functs_filtered rtl_pr_main'.
Note: See TracChangeset for help on using the changeset viewer.