 Timestamp:
 Apr 28, 2011, 5:36:33 PM (9 years ago)
 Location:
 src/RTL
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTL.ma
r756 r782 10 10 inductive rtl_statement: Type[0] ≝ 11 11  rtl_st_skip: label → rtl_statement 12  rtl_st_cost: costlabel → rtl_statement12  rtl_st_cost: costlabel → label → rtl_statement 13 13  rtl_st_addr: register → register → ident → label → rtl_statement 14  rtl_st_stack_ Addr: register → register → label → rtl_statement14  rtl_st_stack_addr: register → register → label → rtl_statement 15 15  rtl_st_int: register → Byte → label → rtl_statement 16 16  rtl_st_move: register → register → label → rtl_statement … … 25 25  rtl_st_tailcall_id: ident → registers → rtl_statement 26 26  rtl_st_tailcall_ptr: register → register → registers → rtl_statement 27  rtl_st_cond acc: register → label → label → rtl_statement27  rtl_st_cond_acc: register → label → label → rtl_statement 28 28  rtl_st_return: registers → rtl_statement. 29 29 
src/RTL/RTLtoERTL.ma
r777 r782 1 1 include "RTL/RTL.ma". 2 2 include "ERTL/ERTL.ma". 3 include " ASM/RegisterSet.ma".3 include "utilities/RegisterSet.ma". 4 4 5 5 definition change_exit_label ≝ … … 10 10 let ertl_if_params' ≝ ertl_if_params p in 11 11 let ertl_if_locals' ≝ ertl_if_locals p in 12 let ertl_if_stacksize' ≝ ertl_if_stacksize p in 12 13 let ertl_if_graph' ≝ ertl_if_graph p in 13 14 let ertl_if_entry' ≝ ertl_if_entry p in 14 15 let ertl_if_exit' ≝ l in 15 16 mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse' 16 ertl_if_params' ertl_if_locals' 17 ertl_if_params' ertl_if_locals' ertl_if_stacksize' 17 18 ertl_if_graph' ertl_if_entry' ertl_if_exit'. 18 19 … … 24 25 let ertl_if_params' ≝ ertl_if_params p in 25 26 let ertl_if_locals' ≝ ertl_if_locals p in 27 let ertl_if_stacksize' ≝ ertl_if_stacksize p in 26 28 let ertl_if_graph' ≝ ertl_if_graph p in 27 29 let ertl_if_entry' ≝ l in 28 30 let ertl_if_exit' ≝ ertl_if_exit p in 29 31 mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse' 30 ertl_if_params' ertl_if_locals' 32 ertl_if_params' ertl_if_locals' ertl_if_stacksize' 31 33 ertl_if_graph' ertl_if_entry' ertl_if_exit'. 32 34 … … 39 41 let ertl_if_params' ≝ ertl_if_params p in 40 42 let ertl_if_locals' ≝ ertl_if_locals p in 43 let ertl_if_stacksize' ≝ ertl_if_stacksize p in 41 44 let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in 42 45 let ertl_if_entry' ≝ ertl_if_entry p in 43 46 let ertl_if_exit' ≝ ertl_if_exit p in 44 47 mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse' 45 ertl_if_params' ertl_if_locals' 48 ertl_if_params' ertl_if_locals' ertl_if_stacksize' 46 49 ertl_if_graph' ertl_if_entry' ertl_if_exit'. 47 50 … … 330 333 ] 331 334 ]. 332 335 336 axiom add_pro_and_epilogue: 337 ∀rs: register_set. 338 ∀params: list register. 339 ∀ret_args: list register. 340 ∀def: ertl_internal_function. 341 option ertl_internal_function. 342 343 (* 344 dpm: address callee_saved problem 333 345 definition add_pro_and_epilogue ≝ 334 346 λrs: register_set. … … 337 349 λdef. 338 350 let 〈def, sra〉 ≝ fresh_regs def 2 in 339 let sral ≝ nth ? 0 srain340 let srah ≝ nth sra 1in351 let sral ≝ safe_nth ? 0 sra ? in 352 let srah ≝ safe_nth ? 1 sra ? in 341 353 let 〈def, sregs〉 ≝ allocate_regs callee_saved def in 342 354 let def ≝ add_prologue params sral srah sregs def in 343 355 let def ≝ add_epilogue ret_args sral srah sregs def in 344 def. 356 def. 357 *) 358 359 definition set_params_hdw ≝ 360 λparams. 361 match length ? params with 362 [ O ⇒ Some ? [ get_params_hdw_internal ] 363  _ ⇒ 364 match zip ? ? params parameters with 365 [ None ⇒ None ? 366  Some zipped_params ⇒ Some ? (restore_hdws zipped_params) 367 ] 368 ]. 369 370 definition set_param_stack ≝ 371 λoff: nat. 372 λsrcr. 373 λstart_lbl, dest_lbl: label. 374 λdef. 375 let 〈def, addr1〉 ≝ fresh_reg def in 376 let 〈def, addr2〉 ≝ fresh_reg def in 377 let 〈def, tmpr〉 ≝ fresh_reg def in 378 let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in 379 adds_graph [ 380 ertl_st_int addr2 int_offset start_lbl; 381 ertl_st_get_hdw tmpr RegisterSPL start_lbl; 382 ertl_st_clear_carry start_lbl; 383 ertl_st_op2 Sub addr1 tmpr addr1 start_lbl; 384 ertl_st_get_hdw tmpr RegisterSPH start_lbl; 385 ertl_st_int addr2 (bitvector_of_nat ? 0) start_lbl; 386 ertl_st_op2 Sub addr2 tmpr addr2 start_lbl; 387 ertl_st_store addr1 addr2 srcr start_lbl 388 ] start_lbl dest_lbl def. 389 390 definition set_params_stack ≝ 391 λparams. 392 match length ? params with 393 [ O ⇒ [ get_params_hdw_internal ] 394  _ ⇒ mapi ? ? set_param_stack params 395 396 ]. 397 398 definition set_params ≝ 399 λparams. 400 let n ≝ min (length ? params) (length ? parameters) in 401 let 〈hdw_params, stack_params〉 ≝ list_split ? n params in 402 match set_params_hdw hdw_params with 403 [ None ⇒ None ? 404  Some hdw_params' ⇒ Some ? (hdw_params' @ (set_params_stack stack_params)) 405 ]. 406 407 definition fetch_result ≝ 408 λret_regs. 409 λstart_lbl. 410 match ret_regs with 411 [ nil ⇒ adds_graph [ertl_st_skip start_lbl] start_lbl 412  cons hd tl ⇒ 413 match tl with 414 [ nil ⇒ 415 adds_graph [ 416 ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl; 417 ertl_st_get_hdw hd RegisterST0 start_lbl 418 ] start_lbl 419  cons hd' tl' ⇒ 420 adds_graph [ 421 ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl; 422 ertl_st_hdw_to_hdw RegisterST1 RegisterDPH start_lbl; 423 ertl_st_get_hdw hd RegisterST0 start_lbl; 424 ertl_st_get_hdw hd' RegisterST1 start_lbl 425 ] start_lbl 426 ] 427 ]. 428 429 definition translate_call_id ≝ 430 λf. 431 λargs. 432 λret_regs. 433 λstart_lbl, dest_lbl: label. 434 λdef. 435 let nb_args ≝ bitvector_of_nat ? (length ? args) in 436 match set_params args with 437 [ None ⇒ None ? 438  Some params_args ⇒ 439 add_translates ( 440 params_args @ [ 441 adds_graph [ ertl_st_call_id f nb_args start_lbl ] ; 442 fetch_result ret_regs 443 ]) start_lbl dest_lbl def 444 ]. 445 446 definition translate_stmt ≝ 447 λlbl: label. 448 λstmt: rtl_statement. 449 λdef: ertl_internal_function. 450 match stmt with 451 [ rtl_st_skip lbl' ⇒ 452 Some ? (add_graph lbl (ertl_st_skip lbl') def) 453  rtl_st_cost cost_lbl lbl' ⇒ 454 Some ? (add_graph lbl (ertl_st_cost cost_lbl lbl') def) 455  rtl_st_addr r1 r2 x lbl' ⇒ 456 adds_graph [ 457 ertl_st_addr_l r1 x lbl; 458 ertl_st_addr_h r2 x lbl 459 ] lbl lbl' def 460  rtl_st_stack_addr r1 r2 lbl' ⇒ 461 adds_graph [ 462 ertl_st_get_hdw r1 RegisterSPL lbl; 463 ertl_st_get_hdw r2 RegisterSPH lbl 464 ] lbl lbl' def 465  rtl_st_int r i lbl' ⇒ 466 Some ? (add_graph lbl (ertl_st_int r i lbl') def) 467  rtl_st_move r1 r2 lbl' ⇒ 468 Some ? (add_graph lbl (ertl_st_move r1 r2 lbl') def) 469  rtl_st_opaccs opaccs d s1 s2 lbl' ⇒ 470 Some ? (add_graph lbl (ertl_st_opaccs opaccs d s1 s2 lbl') def) 471  rtl_st_op1 op1 d s lbl' ⇒ 472 Some ? (add_graph lbl (ertl_st_op1 op1 d s lbl') def) 473  rtl_st_op2 op2 d s1 s2 lbl' ⇒ 474 Some ? (add_graph lbl (ertl_st_op2 op2 d s1 s2 lbl') def) 475  rtl_st_clear_carry lbl' ⇒ 476 Some ? (add_graph lbl (ertl_st_clear_carry lbl') def) 477  rtl_st_load d a1 a2 lbl' ⇒ 478 Some ? (add_graph lbl (ertl_st_load d a1 a2 lbl') def) 479  rtl_st_store a1 a2 s lbl' ⇒ 480 Some ? (add_graph lbl (ertl_st_store a1 a2 s lbl') def) 481  rtl_st_call_id f args ret_regs lbl' ⇒ 482 translate_call_id f args ret_regs lbl lbl' def 483  rtl_st_call_ptr r1 r2 regs1 regs2 lbl ⇒ None ? (* dpm: todo *) 484  rtl_st_cond_acc src lbl_true lbl_false ⇒ 485 Some ? (add_graph lbl (ertl_st_cond_acc src lbl_true lbl_false) def) 486  rtl_st_return ret_regs ⇒ 487 Some ? (add_graph lbl (ertl_st_return ret_regs) def) 488  rtl_st_tailcall_id ident regs ⇒ None ? (* dpm: impossible *) 489  rtl_st_tailcall_ptr r1 r2 regs ⇒ None ? (* dpm: impossible *) 490 ]. 491 492 (* dpm: this should not be option, fix *) 493 axiom map_fold: 494 ∀A, B: Type[0]. 495 ∀f: label → A → B → option B. 496 ∀m: rtl_statement_graph. 497 ∀b: B. 498 B. 499 500 definition translate_internal ≝ 501 λdef. 502 let nb_params ≝ length ? (rtl_if_params def) in 503 let added_stacksize ≝ max 0 (nb_params  (length ? parameters)) in 504 let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in 505 let def' ≝ 506 mk_ertl_internal_function 507 (rtl_if_luniverse def) (rtl_if_runiverse def) 508 nb_params new_locals ((rtl_if_stacksize def) + added_stacksize) 509 (empty_map ? ?) (rtl_if_entry def) (rtl_if_exit def) in 510 let def' ≝ map_fold ? ? translate_stmt (rtl_if_graph def) def' in 511 let def' ≝ add_pro_and_epilogue register_list_set (rtl_if_params def) (rtl_if_result def) def' in 512 def'. 513 514 definition translate_funct ≝ 515 λid_def: ident × ?. 516 let 〈id, def〉 ≝ id_def in 517 let def' ≝ 518 match def with 519 [ rtl_f_internal def ⇒ 520 match translate_internal def with 521 [ None ⇒ None ? 522  Some internal_def ⇒ Some ? (ertl_f_internal internal_def) 523 ] 524  rtl_f_external def ⇒ Some ? (ertl_f_external def) 525 ] in 526 〈id, def'〉. 527 528 definition generate ≝ 529 λstmt. 530 λdef. 531 let entry ≝ fresh_label def in 532 match entry with 533 [ None ⇒ None ? 534  Some entry ⇒ 535 let def ≝ add_graph entry stmt def in 536 Some ? (change_entry_label entry def) 537 ]. 538
Note: See TracChangeset
for help on using the changeset viewer.