Changeset 1257 for src/RTL/RTLtoERTL.ma
 Timestamp:
 Sep 22, 2011, 6:04:27 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1254 r1257 36 36 adds_graph globals stmt_list tmp_lbl dest_lbl def]]. 37 37 38 (* 38 (*CSC: bad programming habit: the code below puts everywhere a fake 39 label and then adds_graph fixes them *) 40 (*CSC: the code is artificially fixed to work on ertl_statements, but 41 it works on every graph_params *) 39 42 let rec add_translates 40 ( translate_list: list ?) (start_lbl: label) (dest_lbl: label)41 (def: ertl_internal_function )43 (globals: list ident) (translate_list: list ?) (start_lbl: label) (dest_lbl: label) 44 (def: ertl_internal_function globals) 42 45 on translate_list ≝ 43 46 match translate_list with 44 [ nil ⇒ add_graph start_lbl (ertl_st_skipdest_lbl) def47 [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def 45 48  cons trans translate_list ⇒ 46 49 match translate_list with 47 50 [ nil ⇒ trans start_lbl dest_lbl def 48 51  _ ⇒ 49 let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in52 let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in 50 53 let def ≝ trans start_lbl tmp_lbl def in 51 add_translates translate_list tmp_lbl dest_lbl def 52 ] 53 ]. 54 *) 54 add_translates globals translate_list tmp_lbl dest_lbl def]]. 55 55 56 56 definition fresh_reg: … … 129 129 joint_st_sequential … (joint_instr_extension … (ertl_st_ext_frame_size addr1)) start_lbl; 130 130 joint_st_sequential … (joint_instr_int … tmpr int_offset) start_lbl; 131 joint_st_sequential … (joint_instr_op2 … Sub addr1 addr1 tmpr) start_lbl (*;132 joint_st_sequential … (joint_instr_ get_hdw … tmpr RegisterSPL) start_lbl;131 joint_st_sequential … (joint_instr_op2 … Sub addr1 addr1 tmpr) start_lbl; 132 joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl; 133 133 joint_st_sequential … (joint_instr_op2 … Add addr1 addr1 tmpr) start_lbl; 134 134 joint_st_sequential … (joint_instr_int … addr2 (bitvector_of_nat 8 0)) start_lbl; 135 joint_st_sequential … (joint_instr_ get_hdw … tmpr RegisterSPH) start_lbl;135 joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl; 136 136 joint_st_sequential … (joint_instr_op2 … Addc addr2 addr2 tmpr) start_lbl; 137 joint_st_sequential … (joint_instr_load … destr addr1 addr2) start_lbl *)137 joint_st_sequential … (joint_instr_load … destr addr1 addr2) start_lbl 138 138 ] start_lbl dest_lbl def. 139 139 140 140 definition get_params_stack ≝ 141 λ params.141 λglobals,params. 142 142 match params with 143 [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl ] 144  _ ⇒ 145 let f ≝ λi. λr. get_param_stack i r in 146 mapi ? ? f params 147 ]. 143 [ nil ⇒ [ λstart_lbl. adds_graph … [joint_st_goto … start_lbl] start_lbl ] 144  _ ⇒ mapi ? ? (get_param_stack globals) params ]. 148 145 149 146 definition get_params ≝ 150 λ params.151 let n ≝ min (length ? params) (length ?RegisterParams) in152 let 〈hdw_params, stack_params〉 ≝ list_split ?n params in153 let hdw_params ≝ get_params_hdw hdw_params in154 hdw_params @ (get_params_stack stack_params).147 λglobals,params. 148 let n ≝ min (length … params) (length … RegisterParams) in 149 let 〈hdw_params, stack_params〉 ≝ list_split … n params in 150 let hdw_params ≝ get_params_hdw globals hdw_params in 151 hdw_params @ (get_params_stack … stack_params). 155 152 156 153 definition add_prologue ≝ 154 λglobals. 157 155 λparams: list register. 158 156 λsral. … … 160 158 λsregs. 161 159 λdef. 162 let start_lbl ≝ ertl_if_entrydef in163 let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in164 match lookup ? ? ( ertl_if_graphdef) start_lbl165 return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ertl_internal_functionwith166 [ None ⇒ λnone_absrd. ?160 let start_lbl ≝ joint_if_entry globals (ertl_params globals) def in 161 let 〈tmp_lbl, nuniv〉 ≝ fresh_label ? def in 162 match lookup ? ? (joint_if_code ? (ertl_params globals) def) start_lbl 163 return λx. x ≠ None ? → ertl_internal_function globals with 164 [ None ⇒ λnone_absrd. ⊥ 167 165  Some last_stmt ⇒ λsome_prf. 168 166 let def ≝ 169 add_translates 170 ((adds_graph [171 ertl_st_new_framestart_lbl167 add_translates … 168 ((adds_graph … [ 169 joint_st_sequential … (joint_instr_extension ertl_params_ globals ertl_st_ext_new_frame) start_lbl 172 170 ]) :: 173 (adds_graph [174 ertl_st_pop sralstart_lbl;175 ertl_st_pop srahstart_lbl171 (adds_graph … [ 172 joint_st_sequential … (joint_instr_pop … sral) start_lbl; 173 joint_st_sequential … (joint_instr_pop … srah) start_lbl 176 174 ]) :: 177 (save_hdws sregs) @178 (get_params params))175 (save_hdws … sregs) @ 176 (get_params … params)) 179 177 start_lbl tmp_lbl def 180 178 in 181 add_graph tmp_lbl last_stmt def179 add_graph … tmp_lbl last_stmt def 182 180 ] ?. 183 cases not_implemented (* dep. types here *) 181 [ cases start_lbl #x #H @H 182  cases (none_absrd) /2/ ] 184 183 qed. 185 184
Note: See TracChangeset
for help on using the changeset viewer.