 Timestamp:
 Jul 18, 2011, 5:21:14 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTLtoERTL.ma
r1071 r1075 1 1 include "RTL/RTL.ma". 2 (* include "RTL/RTLTailcall.ma". *) 2 include "utilities/RegisterSet.ma". 3 3 include "ERTL/ERTL.ma". 4 4 … … 148 148 ]. 149 149 150 axiom fresh_regs_length: 151 ∀def: ertl_internal_function. 152 ∀n: nat. 153 (\snd (fresh_regs def n)) = n. 154 155 definition fresh_regs_strong: ? → ∀n: nat. Σregs: ertl_internal_function × (list register). \snd regs = n ≝ 156 λdef: ertl_internal_function. 157 λn: nat. 158 fresh_regs def n. 159 @fresh_regs_length 160 qed. 161 150 162 definition save_hdws_internal ≝ 151 163 λdestr_srcr: register × hardware_register. … … 232 244 let start_lbl ≝ ertl_if_entry def in 233 245 let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in 234 match lookup ? ? (ertl_if_graph def) start_lbl with 235 [ None ⇒ ? 236  Some last_stmt ⇒ 246 match lookup ? ? (ertl_if_graph def) start_lbl 247 return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ertl_internal_function with 248 [ None ⇒ λnone_absrd. ? 249  Some last_stmt ⇒ λsome_prf. 237 250 let def ≝ 238 251 add_translates … … 249 262 in 250 263 add_graph tmp_lbl last_stmt def 251 ] .252 cases not_implemented (* until Brian gives goahead for dep. types*)264 ] ?. 265 cases not_implemented (* dep. types here *) 253 266 qed. 254 267 … … 259 272 λdef: ertl_internal_function. 260 273 let 〈def, tmpr〉 ≝ fresh_reg def in 261 match reduce_strong ? RegisterSTS ret_regs with274 match reduce_strong ? ? RegisterSTS ret_regs with 262 275 [ dp crl crl_proof ⇒ 263 276 let commonl ≝ \fst (\fst crl) in … … 267 280 let init_tmpr ≝ ertl_st_int tmpr (zero ?) start_lbl in 268 281 let f_save ≝ λst. λr. ertl_st_set_hdw st r start_lbl in 269 let saves ≝ map2 ? ? ? f_save commonl commonr ?in282 let saves ≝ map2 ? ? ? f_save commonl commonr crl_proof in 270 283 let f_default ≝ λst. ertl_st_set_hdw st tmpr start_lbl in 271 284 let defaults ≝ map ? ? f_default restl in … … 273 286 ]. 274 287 275 let save_return ret_regs start_lbl dest_lbl def = 276 let (def, tmpr) = fresh_reg def in 277 let ((common1, rest1), (common2, _)) = 278 MiscPottier.reduce I8051.sts ret_regs in 279 let init_tmpr = ERTL.St_int (tmpr, 0, start_lbl) in 280 let f_save st r = ERTL.St_set_hdw (st, r, start_lbl) in 281 let saves = List.map2 f_save common1 common2 in 282 let f_default st = ERTL.St_set_hdw (st, tmpr, start_lbl) in 283 let defaults = List.map f_default rest1 in 284 adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def 288 definition assign_result ≝ 289 λstart_lbl: label. 290 match reduce_strong ? ? RegisterRets RegisterSTS with 291 [ dp crl crl_proof ⇒ 292 let commonl ≝ \fst (\fst crl) in 293 let commonr ≝ \fst (\snd crl) in 294 let f ≝ λret. λst. ertl_st_hdw_to_hdw ret st start_lbl in 295 let insts ≝ map2 ? ? ? f commonl commonr crl_proof in 296 adds_graph insts start_lbl 297 ]. 298 299 definition add_epilogue ≝ 300 λret_regs. 301 λsral. 302 λsrah. 303 λsregs. 304 λdef. 305 let start_lbl ≝ ertl_if_exit def in 306 let 〈tmp_lbl, nuniv〉 ≝ fresh_label def in 307 match lookup ? ? (ertl_if_graph def) start_lbl 308 return λx. lookup ? ? (ertl_if_graph def) start_lbl ≠ None ? → ? with 309 [ None ⇒ λnone_absd. ? 310  Some last_stmt ⇒ λsome_prf. 311 let def ≝ 312 add_translates ( 313 [save_return ret_regs] @ 314 restore_hdws sregs @ 315 [adds_graph [ 316 ertl_st_push srah start_lbl; 317 ertl_st_push sral start_lbl 318 ]] @ 319 [adds_graph [ 320 ertl_st_del_frame start_lbl 321 ]] @ 322 [assign_result] 323 ) start_lbl tmp_lbl def 324 in 325 let def ≝ add_graph tmp_lbl last_stmt def in 326 change_exit_label tmp_lbl def 327 ] ?. 328 cases not_implemented (* dep types here *) 329 qed. 285 330 286 331 definition allocate_regs_internal ≝ 287 λr: register.332 λr: Register. 288 333 λdef_sregs. 289 334 let 〈def, sregs〉 ≝ def_sregs in … … 292 337 293 338 definition allocate_regs ≝ 294 λrs : register_set.339 λrs. 295 340 λsaved: rs_set rs. 296 341 λdef. 297 342 rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉. 343 344 definition add_pro_and_epilogue ≝ 345 λparams. 346 λret_regs. 347 λdef. 348 match fresh_regs_strong def 2 with 349 [ dp def_sra def_sra_proof ⇒ 350 let def ≝ \fst def_sra in 351 let sra ≝ \snd def_sra in 352 let sral ≝ nth_safe ? 0 sra ? in 353 let srah ≝ nth_safe ? 1 sra ? in 354 let 〈def, sregs〉 ≝ allocate_regs register_list_set RegisterCalleeSaved def in 355 let def ≝ add_prologue params sral srah sregs def in 356 let def ≝ add_epilogue ret_regs sral srah sregs def in 357 def 358 ]. 359 [1: >def_sra_proof // 360 2: >def_sra_proof // 361 ] 362 qed. 363 364 definition set_params_hdw ≝ 365 λparams. 366 match params with 367 [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl] 368  _ ⇒ 369 let l ≝ zip_pottier ? ? params parameters in 370 restore_hdws l 371 ]. 372 373 definition set_param_stack ≝ 374 λoff. 375 λsrcr. 376 λstart_lbl: label. 377 λdest_lbl: label. 378 λdef: ertl_internal_function. 379 let 〈def, addr1〉 ≝ fresh_reg def in 380 let 〈def, addr2〉 ≝ fresh_reg def in 381 let 〈def, tmpr〉 ≝ fresh_reg def in 382 let 〈ignore, int_off〉 ≝ half_add ? off int_size in 383 adds_graph [ 384 ertl_st_int addr1 int_off start_lbl; 385 ertl_st_get_hdw tmpr RegisterSPL start_lbl; 386 ertl_st_clear_carry start_lbl; 387 ertl_st_op2 Sub addr1 tmpr addr1 start_lbl; 388 ertl_st_get_hdw tmpr RegisterSPH start_lbl; 389 ertl_st_int addr2 (zero ?) start_lbl; 390 ertl_st_op2 Sub addr2 tmpr addr2 start_lbl; 391 ertl_st_store addr1 addr2 srcr start_lbl 392 ] start_lbl dest_lbl def. 393 394 definition set_params_stack ≝ 395 λparams. 396 match params with 397 [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl] 398  _ ⇒ 399 let f ≝ λi. λr. set_param_stack (bitvector_of_nat ? i) r in 400 mapi ? ? f params 401 ]. 402 403 axiom min_fst: 404 ∀m, n: nat. 405 min m n ≤ m. 406 407 definition set_params ≝ 408 λparams. 409 let n ≝ min (params) (parameters) in 410 let hdw_stack_params ≝ split ? params n ? in 411 let hdw_params ≝ \fst hdw_stack_params in 412 let stack_params ≝ \snd hdw_stack_params in 413 set_params_hdw hdw_params @ set_params_stack stack_params. 414 @min_fst 415 qed. 416 417 definition fetch_result ≝ 418 λret_regs. 419 λstart_lbl: label. 420 match reduce_strong ? ? RegisterSTS RegisterRets with 421 [ dp crl first_crl_proof ⇒ 422 let commonl ≝ \fst (\fst crl) in 423 let commonr ≝ \fst (\snd crl) in 424 let f_save ≝ λst. λret. ertl_st_hdw_to_hdw st ret start_lbl in 425 let saves ≝ map2 ? ? ? f_save commonl commonr ? in 426 match reduce_strong ? ? ret_regs RegisterSTS with 427 [ dp crl second_crl_proof ⇒ 428 let commonl ≝ \fst (\fst crl) in 429 let commonr ≝ \fst (\snd crl) in 430 let f_restore ≝ λr. λst. ertl_st_get_hdw r st start_lbl in 431 let restores ≝ map2 ? ? ? f_restore commonl commonr ? in 432 adds_graph (saves @ restores) start_lbl 433 ] 434 ]. 435 [ normalize nodelta; @second_crl_proof 436  @first_crl_proof 437 ] 438 qed. 439 440 definition translate_call_id ≝ 441 λf. 442 λargs. 443 λret_regs. 444 λstart_lbl. 445 λdest_lbl. 446 λdef. 447 let nb_args ≝ args in 448 add_translates ( 449 set_params args @ [ 450 adds_graph [ ertl_st_call_id f (bitvector_of_nat ? nb_args) start_lbl ]; 451 fetch_result ret_regs 452 ] 453 ) start_lbl dest_lbl def. 454 455 definition translate_stmt ≝ 456 λlbl. 457 λstmt. 458 λdef. 459 match stmt with 460 [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def 461  rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def 462  rtl_st_addr r1 r2 x lbl' ⇒ 463 adds_graph [ 464 ertl_st_addr_l r1 x lbl; 465 ertl_st_addr_h r2 x lbl 466 ] lbl lbl' def 467  rtl_st_stack_addr r1 r2 lbl' ⇒ 468 adds_graph [ 469 ertl_st_get_hdw r1 RegisterSPL lbl; 470 ertl_st_get_hdw r2 RegisterSPH lbl 471 ] lbl lbl' def 472  rtl_st_int r i lbl' ⇒ add_graph lbl (ertl_st_int r i lbl') def 473  rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def 474  rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒ 475 adds_graph [ 476 ertl_st_opaccs_a op destr1 srcr1 srcr2 lbl; 477 ertl_st_opaccs_b op destr2 srcr1 srcr2 lbl 478 ] lbl lbl' def 479  rtl_st_op1 op1 destr srcr lbl' ⇒ 480 add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def 481  rtl_st_op2 op2 destr srcr1 srcr2 lbl' ⇒ 482 add_graph lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def 483  rtl_st_clear_carry lbl' ⇒ 484 add_graph lbl (ertl_st_clear_carry lbl') def 485  rtl_st_set_carry lbl' ⇒ 486 add_graph lbl (ertl_st_set_carry lbl') def 487  rtl_st_load destr addr1 addr2 lbl' ⇒ 488 add_graph lbl (ertl_st_load destr addr1 addr2 lbl') def 489  rtl_st_store addr1 addr2 srcr lbl' ⇒ 490 add_graph lbl (ertl_st_store addr1 addr2 srcr lbl') def 491  rtl_st_call_id f args ret_regs lbl' ⇒ 492 translate_call_id f args ret_regs lbl lbl' def 493  rtl_st_cond srcr lbl_true lbl_false ⇒ 494 add_graph lbl (ertl_st_cond srcr lbl_true lbl_false) def 495  rtl_st_return ⇒ 496 add_graph lbl ertl_st_return def 497  _ ⇒ ? (* assert false: not implemented or should not happen *) 498 ]. 499 cases not_implemented 500 qed. 501 502 298 503 299 504 definition save_return_internal ≝
Note: See TracChangeset
for help on using the changeset viewer.