 Timestamp:
 Apr 27, 2011, 5:25:26 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r763 r777 1 1 include "RTL/RTL.ma". 2 2 include "ERTL/ERTL.ma". 3 include "ASM/RegisterSet.ma". 3 4 4 5 definition change_exit_label ≝ … … 47 48 definition fresh_label ≝ 48 49 λdef. 49 fresh LabelTag (ertl_if_luniverse def). 50 match fresh LabelTag (ertl_if_luniverse def) with 51 [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ) 52  Error ⇒ None ? 53 ]. 50 54 51 55 definition change_label ≝ … … 88 92 let tmp_lbl ≝ fresh_label def in 89 93 match tmp_lbl with 90 [ OK o ⇒ 91 let 〈lbl, univ〉 ≝ o in 92 let stmt ≝ change_label lbl hd in 94 [ Some tmp_lbl ⇒ 95 let stmt ≝ change_label tmp_lbl hd in 93 96 let def ≝ add_graph start_lbl hd def in 94 adds_graph tl lbl dest_lbl def95  Error⇒ None ?97 adds_graph tl tmp_lbl dest_lbl def 98  None ⇒ None ? 96 99 ] 97 100 ] 98 101 ]. 99 102 100 let rec add_translates (translate_list: list (label → label → ertl_internal_function → ertl_internal_function))103 let rec add_translates (translate_list: list (label → label → ertl_internal_function → option ertl_internal_function)) 101 104 (start_lbl: label) (dest_lbl: label) 102 105 (def: ertl_internal_function): option ertl_internal_function ≝ … … 105 108  cons hd tl ⇒ 106 109 match tl with 107 [ nil ⇒ Some ? (hd start_lbl dest_lbl def)110 [ nil ⇒ hd start_lbl dest_lbl def 108 111  _ ⇒ 109 112 let tmp_lbl ≝ fresh_label def in 110 113 match tmp_lbl with 111 [ OK o ⇒ 112 let 〈lbl, univ〉 ≝ o in 113 let def ≝ hd start_lbl lbl def in 114 add_translates tl lbl dest_lbl def 115  Error ⇒ None ? 114 [ Some tmp_lbl ⇒ 115 match hd start_lbl tmp_lbl def with 116 [ Some def ⇒ add_translates tl tmp_lbl dest_lbl def 117  None ⇒ None ? 118 ] 119  None ⇒ None ? 116 120 ] 117 121 ] … … 129 133 ]. 130 134 135 definition save_hdws_internal ≝ 136 λdestr_srcr: register × hardware_register. 137 λstart_lbl: label. 138 let 〈destr, srcr〉 ≝ destr_srcr in 139 adds_graph [ ertl_st_get_hdw destr srcr start_lbl ] start_lbl. 140 131 141 definition save_hdws ≝ 132 λ 142 λl. 143 map ? ? save_hdws_internal l. 144 145 definition restore_hdws_internal ≝ 146 λdestr_srcr: hardware_register × register. 147 λstart_lbl: label. 148 let 〈destr, srcr〉 ≝ destr_srcr in 149 adds_graph [ ertl_st_set_hdw destr srcr start_lbl ] start_lbl. 150 151 definition swap_components ≝ 152 λA, B: Type[0]. 153 λp: A × B. 154 let 〈l, r〉 ≝ p in 155 〈r, l〉. 156 157 definition restore_hdws ≝ 158 λl. 159 map ? ? restore_hdws_internal (map ? ? (swap_components ? ?) l). 160 161 definition get_params_hdw_internal ≝ 162 λstart_lbl: label. 163 adds_graph [ ertl_st_skip start_lbl ] start_lbl. 164 165 definition get_params_hdw ≝ 166 λparams: list register. 167 match length ? params with 168 [ O ⇒ Some ? [ get_params_hdw_internal ] 169  _ ⇒ 170 match zip ? ? params parameters with 171 [ None ⇒ None ? 172  Some l ⇒ Some ? (save_hdws l) 173 ] 174 ]. 175 176 definition get_param_stack ≝ 177 λoff: nat. 178 λdestr. 179 λstart_lbl, dest_lbl: label. 180 λdef. 181 let 〈def, addr1〉 ≝ fresh_reg def in 182 let 〈def, addr2〉 ≝ fresh_reg def in 183 let 〈def, tmpr〉 ≝ fresh_reg def in 184 let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in 185 adds_graph [ 186 ertl_st_frame_size addr1 start_lbl; 187 ertl_st_int tmpr int_offset start_lbl; 188 ertl_st_op2 Sub addr1 addr1 tmpr start_lbl; 189 ertl_st_get_hdw tmpr RegisterSPL start_lbl; 190 ertl_st_op2 Add addr1 addr1 tmpr start_lbl; 191 ertl_st_int addr2 (bitvector_of_nat 8 0) start_lbl; 192 ertl_st_get_hdw tmpr RegisterSPH start_lbl; 193 ertl_st_op2 Addc addr2 addr2 tmpr start_lbl; 194 ertl_st_load destr addr1 addr2 start_lbl 195 ] start_lbl dest_lbl def. 196 197 definition get_params_stack_internal ≝ 198 λi. 199 λr. 200 get_param_stack i r. 201 202 definition get_params_stack ≝ 203 λparams. 204 match length ? params with 205 [ O ⇒ [ get_params_hdw_internal ] 206  _ ⇒ mapi ? ? get_params_stack_internal params 207 ]. 208 209 definition get_params ≝ 210 λparams. 211 let n ≝ min (length ? params) (length ? parameters) in 212 let 〈hdw_params, stack_params〉 ≝ list_split ? n params in 213 match get_params_hdw hdw_params with 214 [ None ⇒ None ? 215  Some hdw_params ⇒ Some ? (hdw_params @ (get_params_stack stack_params)) 216 ]. 217 218 definition add_prologue ≝ 219 λparams. 220 λsral. 221 λsrah. 222 λsregs. 223 λdef. 224 let start_lbl ≝ ertl_if_entry def in 225 let tmp_lbl ≝ fresh_label def in 226 match tmp_lbl with 227 [ None ⇒ None ? 228  Some tmp_lbl ⇒ 229 let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in 230 let params ≝ 231 match get_params params with 232 [ Some params ⇒ params 233  None ⇒ [ ] (* dpm: is this ok? *) 234 ] in 235 let def ≝ 236 add_translates ( 237 adds_graph [ ertl_st_new_frame start_lbl ] :: 238 adds_graph [ ertl_st_pop sral start_lbl; ertl_st_pop srah start_lbl ] :: 239 save_hdws sregs @ 240 params) start_lbl tmp_lbl def in 241 match def with 242 [ Some def ⇒ 243 match last_stmt with 244 [ Some last_stmt ⇒ Some ? (add_graph tmp_lbl last_stmt def) 245  None ⇒ None ? 246 ] 247  None ⇒ None ? 248 ] 249 ]. 250 251 definition allocate_regs_internal ≝ 252 λr: register. 253 λdef_sregs. 254 let 〈def, sregs〉 ≝ def_sregs in 255 let 〈def, r'〉 ≝ fresh_reg def in 256 〈def, 〈r', r〉 :: sregs〉. 257 258 definition allocate_regs ≝ 259 λrs: register_set. 260 λsaved: rs_set rs. 261 λdef. 262 rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉. 263 264 definition save_return_internal ≝ 265 λr. 266 λstart_lbl. 267 λdest_lbl. 268 λdef. 269 let 〈def, r_tmp〉 ≝ fresh_reg def in 270 adds_graph [ 271 ertl_st_int r_tmp (bitvector_of_nat ? 0) start_lbl; 272 ertl_st_set_hdw RegisterST0 r start_lbl; 273 ertl_st_set_hdw RegisterST1 r_tmp start_lbl ] start_lbl dest_lbl def. 274 275 definition save_return_internal' ≝ 276 λr1, r2. 277 λstart_lbl. 278 adds_graph [ 279 ertl_st_set_hdw RegisterST0 r1 start_lbl; 280 ertl_st_set_hdw RegisterST1 r2 start_lbl 281 ] start_lbl. 282 283 definition save_return ≝ 284 λret_regs. 285 match ret_regs with 286 [ nil ⇒ [ get_params_hdw_internal ] 287  cons hd tl ⇒ 288 match tl with 289 [ nil ⇒ [ save_return_internal hd ] 290  cons hd' tl' ⇒ [ save_return_internal' hd hd' ] 291 ] 292 ]. 293 294 definition add_epilogue ≝ 295 λret_regs. 296 λsral. 297 λsrah. 298 λsregs. 299 λdef. 300 let start_lbl ≝ ertl_if_exit def in 301 let tmp_lbl ≝ fresh_label def in 302 match tmp_lbl with 303 [ None ⇒ None ? 304  Some tmp_lbl ⇒ 305 let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in 306 match last_stmt with 307 [ None ⇒ None ? 308  Some last_stmt ⇒ 309 let def ≝ 310 add_translates ( 311 save_return ret_regs @ 312 restore_hdws sregs @ 313 [adds_graph [ 314 ertl_st_push srah start_lbl; 315 ertl_st_push sral start_lbl 316 ]] @ 317 [adds_graph [ 318 ertl_st_del_frame start_lbl 319 ]] @ 320 [adds_graph [ 321 ertl_st_hdw_to_hdw RegisterDPL RegisterST0 start_lbl; 322 ertl_st_hdw_to_hdw RegisterDPH RegisterST1 start_lbl 323 ]]) start_lbl tmp_lbl def in 324 match def with 325 [ None ⇒ None ? 326  Some def ⇒ 327 let def ≝ add_graph tmp_lbl last_stmt def in 328 Some ? (change_exit_label tmp_lbl def) 329 ] 330 ] 331 ]. 332 333 definition add_pro_and_epilogue ≝ 334 λrs: register_set. 335 λparams. 336 λret_args. 337 λdef. 338 let 〈def, sra〉 ≝ fresh_regs def 2 in 339 let sral ≝ nth ? 0 sra in 340 let srah ≝ nth sra 1 in 341 let 〈def, sregs〉 ≝ allocate_regs callee_saved def in 342 let def ≝ add_prologue params sral srah sregs def in 343 let def ≝ add_epilogue ret_args sral srah sregs def in 344 def.
Note: See TracChangeset
for help on using the changeset viewer.