Changeset 2640
 Timestamp:
 Feb 7, 2013, 3:13:41 PM (6 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTL.ma
r2490 r2640 18 18 (* call_dest ≝ *) (list register) 19 19 (* ext_seq ≝ *) rtl_seq 20 (* ext_seq_labels ≝ *) (λ_.[]) 20 21 (* has_tailcalls ≝ *) has_tailcalls 21 (* paramsT ≝ *) (list register) 22 (* localsT ≝ *) register. 22 (* paramsT ≝ *) (list register). 23 23 24 24 definition RTL ≝ mk_graph_params (RTL_uns true). 
src/RTLabs/RTLabsToRTL.ma
r2601 r2640 5 5 include "common/Graphs.ma". 6 6 include "joint/TranslateUtils.ma". 7 include "utilities/bindLists.ma".8 7 include alias "ASM/BitVector.ma". 9 8 include alias "arithmetics/nat.ma". 10 11 definition rtl_fresh_reg:12 ∀globals.freshT RTL globals register ≝13 λglobals,def.14 let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in15 〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.16 17 definition rtl_fresh_reg_no_local :18 ∀globals.freshT RTL globals register ≝19 λglobals,def.20 let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in21 〈set_runiverse ?? def runiverse, r〉.22 9 23 10 definition size_of_sig_type ≝ … … 57 44 λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf). 58 45 59 definition initialize_local_env_internal : 60 ∀globals. 61 ((joint_internal_function RTL globals) × local_env) → (register×typ) → 62 ((joint_internal_function RTL globals) × local_env) ≝ 63 λglobals,def_env,r_sig. 64 let 〈def,lenv〉 ≝ def_env in 65 let 〈r, sig〉 ≝ r_sig in 66 let size ≝ size_of_sig_type sig in 67 let 〈def,rs〉 ≝ repeat_fresh … (rtl_fresh_reg_no_local globals) size def in 68 〈def,add … lenv r rs〉. 46 (* move *) 47 let rec m_iter (M : Monad) X (f : X → M X) (n : ℕ) (m : M X) on n : M X ≝ 48 match n with 49 [ O ⇒ m 50  S k ⇒ 51 ! v ← m ; 52 m_iter … f k (f v) 53 ]. 54 55 definition fresh_registers : ∀p,g.ℕ → state_monad (joint_internal_function p g) (list register) ≝ 56 λp,g,n. 57 let f ≝ λacc.! m ← fresh_register … ; return (m :: acc) in 58 m_iter … f n (return [ ]). 69 59 70 60 include alias "common/Identifiers.ma". … … 80 70 ∀globals. 81 71 list (register×typ) → 82 freshT RTL globals local_env ≝ 83 λglobals,registers,def. 84 foldl ?? (initialize_local_env_internal globals) 〈def,empty_map …〉 registers. 72 state_monad (joint_internal_function RTL globals) local_env ≝ 73 λglobals,registers. 74 let f ≝ 75 λr_sig,lenv. 76 let 〈r, sig〉 ≝ r_sig in 77 let size ≝ size_of_sig_type sig in 78 ! regs ← fresh_registers … size ; 79 return add … lenv r regs in 80 m_fold … f registers (empty_map …). 85 81 86 82 lemma initialize_local_env_in : ∀globals,l,def,r. 87 83 Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env globals l def). 88 #globals #l #U #r @(list_elim_left … l) 89 [ * 90  * #tl #sig #hd #IH #G elim (Exists_append … G) G 91 whd in match initialize_local_env; normalize nodelta 92 >foldl_step change with (initialize_local_env ???) in match (foldl ?????); 93 [ #H lapply (IH H) 94  * [2: *] #EQ destruct(EQ) 95 ] 96 cases (initialize_local_env ???) 97 #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta 98 elim (repeat_fresh ??????) #U'' #rs 99 [ >mem_set_add @orb_Prop_r assumption 100  @mem_set_add_id 101 ] 84 whd in match initialize_local_env; normalize nodelta #globals 85 cut (∀l,init,def,r.(Exists ? (λx.\fst x = r) l ∨ bool_to_Prop (r ∈ init)) → 86 r ∈ \snd (m_fold (state_monad ?) ??? l init def)) 87 [7: #aux #l #def #r #H @aux %1{H} *:] 88 #l elim l l 89 [ #init #def #r * [*] #H @H ] 90 * #hd #sig #tl #IH #init #def #r #H 91 whd in ⊢ (?(???(???%)?)); normalize nodelta 92 whd in ⊢ (?(???(???(match % with [ _ ⇒ ?]))?)); 93 inversion (fresh_registers ????) #def' #regs #EQfresh normalize nodelta 94 @IH cases H H [*] #H 95 [ destruct %2 @mem_set_add_id 96  %1{H} 97  %2 >mem_set_add @orb_Prop_r @H 98 ] 102 99 qed. 103 100 … … 112 109 (* params *) list (register×typ) → 113 110 (* return *) option (register×typ) → 114 freshT RTL globalslocal_env ≝111 state_monad (joint_internal_function RTL globals) local_env ≝ 115 112 λglobals,locals,params,ret,def. 116 113 let 〈def',lenv〉 as EQ ≝ … … 120 117  None ⇒ [ ] 121 118 ]) @ locals @ params) def in 122 let locals' ≝ map_list_local_env lenv locals ? in123 119 let params' ≝ map_list_local_env lenv params ? in 124 120 let ret' ≝ match ret return λx.ret = x → ? with … … 129 125 mk_joint_internal_function RTL globals 130 126 (joint_if_luniverse … def') (joint_if_runiverse … def') ret' 131 params' locals'(joint_if_stacksize … def')132 (joint_if_code … def') (joint_if_entry … def') (joint_if_exit … def')in127 params' (joint_if_stacksize … def') 128 (joint_if_code … def') (joint_if_entry … def') in 133 129 〈def'', lenv〉. @hide_prf 134 130 [ >(proj2_rewrite ????? EQ) … … 136 132 *: >(proj2_rewrite ????? EQ) 137 133 @(All_mp ??? (λpr.initialize_local_env_in ??? (\fst pr))) 138 [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) params)) 139 [ #a #H @Exists_append_r @Exists_append_r @H 140  generalize in match params; 141 ] 142  @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) locals)) 143 [ #a #H @Exists_append_r @Exists_append_l @H 144  generalize in match locals; 145 ] 134 @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) params)) 135 [ #a #H @Exists_append_r @Exists_append_r @H 136  elim params [%] #hd #tl #IH % [ %1 % ] @(All_mp … IH) #x #G %2{G} 146 137 ] 147 #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G}148 138 ] 149 139 qed. … … 152 142 λA. 153 143 λlst: list A. 154 λprf: 2 = length A lst.〈nth_safe … 0 lst ?, nth_safe … 1 lst ?〉. <prf //144 λprf: 2 = length A lst.〈nth_safe … 0 lst ?, nth_safe … 1 lst ?〉. <prf [%2] %1 155 145 qed. 156 146 … … 187 177 188 178 let rec list_inject_All_aux A P (l : list A) on l : All A P l → list (Σx.P x) ≝ 189 match l return λx.All A P x → ?with179 match l return λx.All A P x → list (Σx.P x) with 190 180 [ nil ⇒ λ_.[ ] 191  cons hd tl ⇒ λprf.«hd, ?» :: list_inject_All_aux A P tl ? 192 ]. cases prf #H1 #H2 [@H1  @H2] 193 qed. 194 195 include alias "basics/lists/list.ma". 181  cons hd tl ⇒ λprf.«hd, proj1 … prf» :: list_inject_All_aux A P tl (proj2 … prf) 182 ]. 183 196 184 definition translate_op: 197 185 ∀globals. Op2 → … … 200 188 ∀srcrs2 : list psd_argument. 201 189 dests = srcrs1 → srcrs1 = srcrs2 → 202 list (joint_seq RTL globals)190 bind_new register (list (joint_seq RTL globals)) 203 191 ≝ 204 192 λglobals: list ident. … … 251 239 definition translate_op_asym_unsigned : 252 240 ∀globals.Op2 → list register → list psd_argument → list psd_argument → 253 list (joint_seq RTL globals) ≝241 bind_new register (list (joint_seq RTL globals)) ≝ 254 242 λglobals,op,destrs,srcrs1,srcrs2. 255 243 let l ≝ destrs in … … 257 245 let srcrs2' ≝ cast_list ? (zero_byte : psd_argument) l srcrs2 in 258 246 translate_op globals op destrs srcrs1' srcrs2' ??. 247 @hide_prf 259 248 normalize nodelta 260 249 >length_cast_list [2: >length_cast_list ] % … … 266 255  S size' ⇒ 267 256 (byte_of_nat k : psd_argument) :: nat_to_args size' (k ÷ 8) 268 ]. [ %  cases (nat_to_args ??) #res #EQ normalize >EQ % ] qed.257 ]. @hide_prf [ %  cases (nat_to_args ??) #res #EQ normalize >EQ % ] qed. 269 258 270 259 definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with … … 273 262 ]. 274 263 275 (* JHM/BJC 2012.11.26: TODO fix this use of bool_to_Prop/remove other defn of member *)276 264 definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst. 277 265 match cst with 278 [ Oaddrsymbol id _ ⇒ bool_to_Prop ( member ? (eq_identifier ?) idglobals)266 [ Oaddrsymbol id _ ⇒ bool_to_Prop (id ∈ globals) 279 267  _ ⇒ True 280 268 ]. 281 269 282 270 definition translate_cst : 283 271 ∀ty. … … 286 274 ∀destrs: list register. 287 275 destrs = size_of_cst ? cst_sig → 288 list (joint_seq RTL globals)276 bind_new register (list (joint_seq RTL globals)) 289 277 ≝ 290 278 λty,globals,cst_sig,destrs. … … 302 290 [(rtl_stack_address r1 r2 : joint_seq RTL globals)] 303 291 ] (pi2 … cst_sig). 292 @hide_prf 304 293 [ cases (split_into_bytes ??) #lst 305 #EQ >EQ >prf whd in ⊢ (??%?); cases size % .306  @cst_prf (* previously failed to typecheck here, until change 2012.11.26 above *)294 #EQ >EQ >prf whd in ⊢ (??%?); cases size % 295  @cst_prf 307 296 *: >prf % 308 297 ] … … 344 333 ∀globals : list ident. 345 334 list register → psd_argument → 346 bind_new (localsT RTL)(list (joint_seq RTL globals)) ≝335 bind_new register (list (joint_seq RTL globals)) ≝ 347 336 λglobals,destrs,srca. 348 337 ν tmp in … … 369 358 ]. 370 359 371 lemma last_not_empty : ∀A,l. 372 match l with [ nil ⇒ False  _ ⇒ True ] → 360 lemma last_def : ∀A,hd,tl.last A (hd @ [tl]) = Some ? tl. 361 #A #hd elim hd hd [ #tl % ] #hd * [ #_ #last % ] #hd' #tl #IH #last 362 @IH qed. 363 364 lemma last_last_ne : ∀A,l.last A (pi1 … l) = Some ? (last_ne … l). 365 #A * @list_elim_left [*] #hd #tl #_ #prf 366 whd in match last_ne; normalize nodelta 367 >split_on_last_ne_def @last_def qed. 368 369 lemma last_not_empty : ∀A,l.not_empty A l → 373 370 match last A l with 374 371 [ None ⇒ False 375 372  _ ⇒ True ]. 376 #A #l elim l [ * ] 377 #hd * [ #_ * % ] 378 #hd' #tl #IH * @(IH I) 379 qed. 373 #A #l #prf >(last_last_ne … «l, prf») % qed. 380 374 381 375 definition translate_op_asym_signed : 382 376 ∀globals.Op2 → list register → list psd_argument → list psd_argument → 383 bind_new (localsT RTL)(list (joint_seq RTL globals)) ≝377 bind_new register (list (joint_seq RTL globals)) ≝ 384 378 λglobals,op,destrs,srcrs1,srcrs2. 385 379 νtmp1,tmp2 in 386 380 let l ≝ destrs in 387 let f≝ λsrcrs,tmp.381 let cast_srcrs ≝ λsrcrs,tmp. 388 382 let srcrs_l ≝ srcrs in 389 383 if leb srcrs_l l then 390 match last …srcrs with384 match last ? srcrs with 391 385 [ Some last ⇒ 392 386 〈srcrs @ make_list … (Reg ? tmp) (l  srcrs_l), … … 397 391 else 398 392 〈lhd … srcrs l, [ ]〉 in 399 let prf : ∀srcrs,tmp.destrs = \fst ( fsrcrs tmp) ≝ ? in400 let srcrs1init ≝ fsrcrs1 tmp1 in401 let srcrs2init ≝ fsrcrs2 tmp2 in402 \snd srcrs1init @ \snd srcrs2init@393 let prf : ∀srcrs,tmp.destrs = \fst (cast_srcrs srcrs tmp) ≝ ? in 394 let srcrs1init ≝ cast_srcrs srcrs1 tmp1 in 395 let srcrs2init ≝ cast_srcrs srcrs2 tmp2 in 396 \snd srcrs1init @@ \snd srcrs2init @@ 403 397 translate_op globals op destrs (\fst srcrs1init) (\fst srcrs2init) ??. 398 @hide_prf 404 399 [ @prf  <prf @prf ] 405 400 #srcrs #tmp normalize nodelta 406 401 @leb_elim #H normalize nodelta 407 [ lapply (last_not_empty … srcrs) 408 cases (last ??) 409 [ cases srcrs 410 [ #_ normalize >length_make_list % 411  #hd #tl #abs elim(abs I) 412 ] 413  #last #_ normalize nodelta 414 >length_append >length_make_list 402 [ cases (last ??) normalize nodelta 403 [ >length_make_list % 404  #_ >length_append >length_make_list 415 405 @minus_to_plus // 416 406 ] 417  >length_lhd normalize @leb_elim 418 [ #G elim (absurd … G H) 419  #_ % 420 ] 407  >length_lhd normalize >(not_le_to_leb_false … H) % 421 408 ] 422 409 qed. … … 426 413 ∀globals: list ident. 427 414 signedness → list register → list register → 428 bind_new (localsT RTL)(list (joint_seq RTL globals)) ≝415 bind_new register (list (joint_seq RTL globals)) ≝ 429 416 λglobals,src_sign,destrs,srcrs. 430 417 match reduce_strong ?? destrs srcrs with … … 459 446 map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf. 460 447 461 definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT RTL)(list (joint_seq RTL globals)) ≝448 definition translate_negint : ∀globals.? → ? → ? → bind_new register (list (joint_seq RTL globals)) ≝ 462 449 λglobals: list ident. 463 450 λdestrs: list register. 464 451 λsrcrs: list register. 465 452 λprf: destrs = srcrs. (* assert in caml code *) 466 translate_notint … destrs srcrs prf @ 467 match nat_to_args (destrs) 1 with 468 [ mk_Sig res prf' ⇒ 469 translate_op ? Add destrs (map … (Reg ?) destrs) res ?? 470 ]. 471 >length_map // qed. 453 translate_notint … destrs srcrs prf @@ 454 translate_op ? Add destrs (map … (Reg ?) destrs) (nat_to_args (destrs) 1) ??. 455 @hide_prf >length_map [ cases (nat_to_args ??) ] // qed. 472 456 473 457 definition translate_notbool: 474 458 ∀globals : list ident. 475 459 list register → list register → 476 bind_new (localsT RTL)(list (joint_seq RTL globals)) ≝460 bind_new register (list (joint_seq RTL globals)) ≝ 477 461 λglobals,destrs,srcrs. 478 462 match destrs with … … 497 481 498 482 definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? → 499 bind_new (localsT RTL)(list (joint_seq RTL globals)) ≝483 bind_new register (list (joint_seq RTL globals)) ≝ 500 484 λglobals. 501 485 λty, ty'. … … 507 491 match op1 508 492 return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' → 509 bind_new (localsT RTL)(list (joint_seq RTL globals)) with493 bind_new register (list (joint_seq RTL globals)) with 510 494 [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2. 511 495 translate_cast globals src_sign destrs srcrs … … 524 508  _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *) 525 509 ] (refl …) (refl …). 510 @hide_prf 526 511 destruct >prf1 >prf2 [3: >length_map ] // 527 512 qed. … … 548 533 (Σi.i<S k) → 549 534 (* the accumulator *) 550 list (joint_seq RTL globals) →551 list (joint_seq RTL globals) ≝535 bind_new register (list (joint_seq RTL globals)) → 536 bind_new register (list (joint_seq RTL globals)) ≝ 552 537 λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2, 553 538 tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc. … … 570 555 let tmp_destrs_view : list register ≝ 571 556 ltl ? tmp_destrs_dummy k in 572 ❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k  i) srcrs2 ?) ::573 translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @ 557 [❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k  i) srcrs2 ?)] @@ 558 translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @@ 574 559 acc 575 560 ]. 576 [ @lt_plus_to_minus [ @le_S_S_to_le assumption  <srcrs2_prf <srcrs1_prf 561 @hide_prf 562 [ <srcrs1_prf 563 @(transitive_le … i_prf k_prf) 564  @lt_plus_to_minus [ @le_S_S_to_le assumption  <srcrs2_prf <srcrs1_prf 577 565 whd >(plus_n_O (S k)) @le_plus // ] 578  <srcrs1_prf 579 @(transitive_le … i_prf k_prf) 580  >length_map // 566  >length_map % 581 567  >length_map 582 568 >length_ltl … … 584 570 >length_make_list 585 571 normalize in ⊢ (???(?%?)); 586 >plus_minus_commutative 587 [2: @le_plus_to_minus_r <plus_n_Sm <plus_n_O assumption] 588 cut (S n = 2 + (n  1)) 589 [2: #EQ >EQ %] 590 >plus_minus_commutative 591 [2: @(transitive_le … k_prf) //] 592 @sym_eq 593 @plus_to_minus % 572 cases n in k_prf; [ #ABS cases (absurd ? ABS ?) /2 by le_to_not_lt/ ] 573 #n' #k_prf >minus_S_S <minus_n_O 574 >plus_minus_commutative [%] @le_S_S_to_le assumption 594 575 ] qed. 595 576 596 definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT RTL)(list (joint_seq RTL globals)) ≝577 definition translate_mul : ∀globals.?→?→?→?→?→bind_new register (list (joint_seq RTL globals)) ≝ 597 578 λglobals : list ident. 598 579 λdestrs : list register. … … 610 591 (* the step calculating all products with least significant byte going in the 611 592 kth position of the result *) 612 let translate_mul_k : (Σk.k<destrs) → list (joint_seq RTL globals) →613 list (joint_seq RTL globals) ≝593 let translate_mul_k : (Σk.k<destrs) → bind_new register (list (joint_seq RTL globals)) → 594 bind_new register (list (joint_seq RTL globals)) ≝ 614 595 λk_sig,acc.match k_sig with 615 596 [ mk_Sig k k_prf ⇒ … … 620 601 (* initializing tmp_destrs to zero 621 602 dummy is intentionally uninitialized *) 622 translate_fill_with_zero … tmp_destrs @ 603 translate_fill_with_zero … tmp_destrs @@ 623 604 (* the main body, roughly: 624 605 for k in 0 ... n1 do 625 606 for i in 0 ... k do 626 607 translate_mul_i … k … i *) 627 foldr … translate_mul_k [ ] (range_strong (destrs)) @ 608 foldr … translate_mul_k [ ] (range_strong (destrs)) @@ 628 609 (* epilogue: saving the result *) 629 610 translate_move … destrs (map … (Reg ?) tmp_destrs) ?. 611 @hide_prf 630 612 [ >length_map >tmp_destrs_prf // 631 613  >length_append <plus_n_Sm <plus_n_O // … … 634 616 635 617 definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→ 636 bind_new (localsT RTL)(list (joint_seq RTL globals)) ≝618 bind_new register (list (joint_seq RTL globals)) ≝ 637 619 λglobals: list ident. 638 620 λdiv_not_mod: bool. … … 663 645 ] (refl …). 664 646 [3: elim not_implemented] 665 destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct qed. 647 @hide_prf 648 destruct normalize in srcrs1_prf srcrs2_prf; destruct qed. 666 649 667 650 (* Paolo: to be moved elsewhere *) … … 677 660 ] (refl …) 678 661 ] (refl …). 662 @hide_prf 679 663 destruct normalize in prf; [destruct//] 680 664 qed. 681 665 682 666 definition translate_ne: ∀globals: list ident.?→?→?→?→ 683 bind_new (localsT RTL)(list (joint_seq RTL globals)) ≝667 bind_new register (list (joint_seq RTL globals)) ≝ 684 668 λglobals: list ident. 685 669 λdestrs: list register. … … 711 695 ] 712 696 ] EQ 713 ]. normalize in EQ; destruct(EQ) assumption qed. 697 ]. 698 @hide_prf normalize in EQ; destruct(EQ) assumption qed. 714 699 715 700 (* if destrs is 0 or 1, it inverses it. To be used after operations that 716 701 ensure this. *) 717 definition translate_toggle_bool : ∀globals.?→ list (joint_seq RTL globals) ≝702 definition translate_toggle_bool : ∀globals.?→bind_new register (list (joint_seq RTL globals)) ≝ 718 703 λglobals: list ident. 719 704 λdestrs: list register. … … 729 714 ∀srcrs2: list psd_argument. 730 715 srcrs1 = srcrs2 → 731 bind_new (localsT RTL)(list (joint_seq RTL globals)) ≝716 bind_new register (list (joint_seq RTL globals)) ≝ 732 717 λglobals,destrs,srcrs1,srcrs2,srcrs_prf. 733 718 match destrs with … … 735 720  cons destr destrs' ⇒ 736 721 ν tmpr in 737 (translate_fill_with_zero … destrs' @ 722 (translate_fill_with_zero … destrs' @@ 738 723 (* I perform a subtraction, but the only interest is in the carry bit *) 739 translate_op ? Sub (make_list … tmpr (srcrs1)) srcrs1 srcrs2 ? srcrs_prf @ 724 translate_op ? Sub (make_list … tmpr (srcrs1)) srcrs1 srcrs2 ? srcrs_prf @@ 740 725 [ destr ← zero_byte .Addc. zero_byte ]) 741 726 ]. 727 @hide_prf 742 728 >length_make_list % qed. 743 729 … … 759 745 ] 760 746 ]. 747 @hide_prf 761 748 [1,2: % 762 749 *: cases re * #a #b >p1 normalize #EQ >EQ % … … 769 756 ∀srcrs2: list psd_argument. 770 757 srcrs1 = srcrs2 → 771 bind_new (localsT RTL)(list (joint_seq RTL globals)) ≝758 bind_new register (list (joint_seq RTL globals)) ≝ 772 759 λglobals,destrs,srcrs1,srcrs2,srcrs_prf. 773 760 νtmp_last_s1 in … … 781 768 shift_srcrs1 @@ shift_srcrs2 @@ 782 769 translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2 ?. 770 @hide_prf 783 771 whd in match new_srcrs1; whd in match new_srcrs2; 784 772 cases p1 … … 787 775 qed. 788 776 789 definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT RTL)(list (joint_seq RTL globals)) ≝777 definition translate_lt : bool→∀globals.?→?→?→?→bind_new register (list (joint_seq RTL globals)) ≝ 790 778 λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs_prf. 791 779 if is_unsigned then … … 812 800 translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf @@ 813 801 translate_toggle_bool globals destrs 814 ]. 815 // qed. 802 ]. @sym_eq assumption qed. 816 803 817 804 definition translate_op2 : … … 822 809 srcrs1 = size_of_sig_type ty1 → 823 810 srcrs2 = size_of_sig_type ty2 → 824 bind_new (localsT RTL)(list (joint_seq RTL globals)) ≝811 bind_new register (list (joint_seq RTL globals)) ≝ 825 812 λglobals,ty1,ty2,ty3,op2,destrs,srcrs1,srcrs2. 826 813 match op2 return λty1,ty2,ty3.λx : binary_operation ty1 ty2 ty3. … … 829 816 [ Oadd sz sg ⇒ λprf1,prf2,prf3. 830 817 translate_op globals Add destrs srcrs1 srcrs2 ?? 831  Oaddp sz ⇒ λprf1,prf2,prf3.818  Oaddpi sz ⇒ λprf1,prf2,prf3. 832 819 translate_op_asym_signed globals Add destrs srcrs1 srcrs2 820  Oaddip sz ⇒ λprf1,prf2,prf3. 821 translate_op_asym_signed globals Add destrs srcrs2 srcrs1 833 822  Osub sz sg ⇒ λprf1,prf2,prf2. 834 823 translate_op globals Sub destrs srcrs1 srcrs2 ?? … … 857 846 translate_cmp true globals c destrs srcrs1 srcrs2 ? 858 847  _ ⇒ ⊥ (* assert false, implemented in run time or float op *) 859 ]. try @not_implemented //848 ]. try @not_implemented @hide_prf // 860 849 qed. 861 850 862 851 definition translate_cond: ∀globals: list ident. list register → label → 863 bind_s eq_block RTL globals (joint_step RTL globals)≝852 bind_step_block RTL globals ≝ 864 853 λglobals: list ident. 865 854 λsrcrs: list register. 866 855 λlbl_true: label. 867 match srcrs return λ_.bind_s eq_block RTL ? (joint_step ??)with868 [ nil ⇒ bret … 〈[ ], NOOP ??〉856 match srcrs return λ_.bind_step_block RTL ? with 857 [ nil ⇒ bret … [ ] 869 858  cons srcr srcrs' ⇒ 870 859 ν tmpr in 871 860 let f : register → joint_seq RTL globals ≝ 872 861 λr. tmpr ← tmpr .Or. r in 873 bret … 〈MOVE RTL globals 〈tmpr,srcr〉 ::874 map ?? f srcrs' , (COND … tmpr lbl_true : joint_step ??) 〉862 bret … ((MOVE RTL globals 〈tmpr,srcr〉 :: 863 map ?? f srcrs' : list (joint_step ??)) @ [COND … tmpr lbl_true]) 875 864 ]. 876 865 877 866 (* Paolo: to be controlled (original seemed overly complex) *) 878 definition translate_load : ∀globals.?→?→?→bind_new (localsT RTL)? ≝867 definition translate_load : ∀globals.?→?→?→bind_new register ? ≝ 879 868 λglobals: list ident. 880 869 λaddr : list psd_argument. … … 883 872 ν tmp_addr_l in 884 873 ν tmp_addr_h in 885 let f ≝ λdestr : register.λacc : list (joint_seq RTL globals). 886 LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) :: 874 (translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@ 875 let f ≝ λdestr : register.λacc : bind_new register (list (joint_seq RTL globals)). 876 [LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h)] @@ 887 877 translate_op ? Add 888 878 [tmp_addr_l ; tmp_addr_h] 889 879 [tmp_addr_l ; tmp_addr_h] 890 [zero_byte ; (int_size : Byte)] ? ? @ acc in 891 translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@ 892 foldr … f [ ] destrs. 893 [1: <addr_prf 894 ] // qed. 880 [zero_byte ; (int_size : Byte)] ? ? @@ acc in 881 foldr … f [ ] destrs). 882 @hide_prf 883 [ <addr_prf ] % qed. 895 884 896 definition translate_store : ∀globals.?→?→?→bind_new (localsT RTL)? ≝885 definition translate_store : ∀globals.?→?→?→bind_new register ? ≝ 897 886 λglobals: list ident. 898 887 λaddr : list psd_argument. … … 901 890 ν tmp_addr_l in 902 891 ν tmp_addr_h in 903 let f ≝ λsrcr : psd_argument.λacc : list (joint_seq RTL globals). 904 STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr :: 892 (translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@ 893 let f ≝ λsrcr : psd_argument.λacc : bind_new register (list (joint_seq RTL globals)). 894 [STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr] @@ 905 895 translate_op … Add 906 896 [tmp_addr_l ; tmp_addr_h] 907 897 [tmp_addr_l ; tmp_addr_h] 908 [zero_byte ; (int_size : Byte)] ? ? @ acc in 909 translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@ 910 foldr … f [ ] srcrs. 911 [1: <addr_prf] // qed. 898 [zero_byte ; (int_size : Byte)] ? ? @@ acc in 899 foldr … f [ ] srcrs). 900 @hide_prf [ <addr_prf ] % qed. 912 901 913 902 lemma lenv_typed_reg_typed_ok1 : … … 951 940 qed. 952 941 942 definition ensure_bind_step_block : ∀p : params.∀g. 943 bind_new register (list (joint_step p g)) → bind_step_block p g ≝ 944 λp,g,b.! l ← b; bret ? (step_block p g) l. 945 946 definition ensure_bind_step_block_from_seq : ∀p : params.∀g. 947 bind_new register (list (joint_seq p g)) → bind_step_block p g ≝ 948 λp,g,b.! l ← b; bret ? (step_block p g) l. 949 950 coercion bind_step_block_from_bind_list nocomposites : 951 ∀p : params.∀g. 952 ∀b : bind_new register (list (joint_step p g)).bind_step_block p g ≝ 953 ensure_bind_step_block on _b : bind_new register (list (joint_step ??)) to 954 bind_step_block ??. 955 956 coercion bind_step_block_from_bind_seq_list nocomposites : 957 ∀p : params.∀g. 958 ∀b : bind_new register (list (joint_seq p g)).bind_step_block p g ≝ 959 ensure_bind_step_block_from_seq on _b : bind_new register (list (joint_seq ??)) to 960 bind_step_block ??. 961 953 962 definition translate_statement : ∀globals, locals.∀env. 954 963 local_env_typed locals env → 955 964 ∀stmt : statement.statement_typed locals stmt → 956 965 𝚺b : 957 bind_s eq_block RTL globals (joint_step RTL globals)+958 bind_ seq_block RTL globals (joint_fin_step RTL).959 if is_inl … b then label else unit≝966 bind_step_block RTL globals + 967 bind_fin_block RTL globals. 968 match b with [ inl _ ⇒ label  _ ⇒ unit] ≝ 960 969 λglobals,locals,lenv,lenv_typed,stmt. 961 match stmt return λstmt.statement_typed locals stmt → 𝚺b: bind_seq_block ???+bind_seq_block ???.if is_inl … b then label else unitwith970 match stmt return λstmt.statement_typed locals stmt → 𝚺b: bind_step_block RTL globals ⊎ bind_fin_block RTL globals.match b with [ inl _ ⇒ label  _ ⇒ unit ] with 962 971 [ St_skip lbl' ⇒ λstmt_typed. 963 ❬ NOOP ??, lbl'❭972 ❬inl … (bret … [ ]), lbl'❭ 964 973  St_cost cost_lbl lbl' ⇒ λstmt_typed. 965 ❬ COST_LABEL … cost_lbl, lbl'❭974 ❬inl … (bret … [COST_LABEL … cost_lbl]), lbl'❭ 966 975  St_const ty destr cst lbl' ⇒ λstmt_typed. 967 ❬ translate_cst ty globals cst (find_local_env destr lenv ?) ?, lbl'❭976 ❬inl … (translate_cst ty globals cst (find_local_env destr lenv ?) ?), lbl'❭ 968 977  St_op1 ty ty' op1 destr srcr lbl' ⇒ λstmt_typed. 969 ❬ translate_op1 globals ty' ty op1978 ❬inl … (translate_op1 globals ty' ty op1 970 979 (find_local_env destr lenv ?) 971 (find_local_env srcr lenv ?) ?? , lbl'❭980 (find_local_env srcr lenv ?) ??), lbl'❭ 972 981  St_op2 ty1 ty2 ty3 op2 destr srcr1 srcr2 lbl' ⇒ λstmt_typed. 973 ❬ translate_op2 globals … op2982 ❬inl … (translate_op2 globals … op2 974 983 (find_local_env destr lenv ?) 975 984 (find_local_env_arg srcr1 lenv ?) 976 (find_local_env_arg srcr2 lenv ?) ??? , lbl'❭985 (find_local_env_arg srcr2 lenv ?) ???), lbl'❭ 977 986 (* XXX: should we be ignoring this? *) 978 987  St_load ignore addr destr lbl' ⇒ λstmt_typed. 979 ❬ translate_load globals980 (find_local_env_arg addr lenv ?) ? (find_local_env destr lenv ?) , lbl'❭988 ❬inl … (translate_load globals 989 (find_local_env_arg addr lenv ?) ? (find_local_env destr lenv ?)), lbl'❭ 981 990 (* XXX: should we be ignoring this? *) 982 991  St_store ignore addr srcr lbl' ⇒ λstmt_typed. 983 ❬ translate_store globals (find_local_env_arg addr lenv ?) ?984 (find_local_env_arg srcr lenv ?) , lbl'❭992 ❬inl … (translate_store globals (find_local_env_arg addr lenv ?) ? 993 (find_local_env_arg srcr lenv ?)), lbl'❭ 985 994  St_call_id f args retr lbl' ⇒ λstmt_typed. 986 ❬ (CALL RTL ? (inl … f) (rtl_args args lenv ?)995 ❬inl ?? (bret ?? [CALL RTL ? (inl … f) (rtl_args args lenv ?) 987 996 (match retr with 988 997 [ Some retr ⇒ find_local_env retr lenv ? 989 998  None ⇒ [ ] 990 ]) : bind_seq_block ???), lbl'❭999 ])]), lbl'❭ 991 1000  St_call_ptr f args retr lbl' ⇒ λstmt_typed. 992 1001 let fs ≝ find_and_addr_arg f lenv ?? in 993 ❬ (CALL RTL ? (inr ?? fs) (rtl_args args lenv ?)1002 ❬inl … (bret … [CALL RTL ? (inr ?? fs) (rtl_args args lenv ?) 994 1003 (match retr with 995 1004 [ Some retr ⇒ 996 1005 find_local_env retr lenv ? 997 1006  None ⇒ [ ] 998 ]) : joint_step ??), lbl'❭1007 ])]), lbl'❭ 999 1008  St_cond r lbl_true lbl_false ⇒ λstmt_typed. 1000 ❬translate_cond globals (find_local_env r lenv ?) lbl_true, lbl_false❭ 1001  St_return ⇒ λ_. ❬inr … (RETURN ?),it❭ 1002 ]. 1003 [ >(lenv_typed_reg_typed_ok1 … lenv_typed stmt_typed) 1009 ❬inl … (translate_cond globals (find_local_env r lenv ?) lbl_true), lbl_false❭ 1010  St_return ⇒ λ_. ❬inr … (bret … 〈[ ], RETURN ?〉),it❭ 1011 ]. 1012 @hide_prf 1013 [ cases daemon (* needs more hypotheses *) 1014  @(lenv_typed_reg_typed_ok2 … lenv_typed stmt_typed) 1015  >(lenv_typed_reg_typed_ok1 … lenv_typed stmt_typed) 1004 1016 @cst_size_ok 1005  @(lenv_typed_reg_typed_ok2 … lenv_typed stmt_typed)1006  cases daemon (* needs more hypotheses *)1007 1017 4,5,6,7: cases stmt_typed #dstr_typed #srcr_typed 1008 [ 1,2: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption1009  @(lenv_typed_reg_typed_ok2 … lenv_typed srcr_typed)1010  @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_typed)1018 [3,4: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption 1019 2: @(lenv_typed_reg_typed_ok2 … lenv_typed srcr_typed) 1020 1: @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_typed) 1011 1021 ] 1012 1022 8,9,10,11,12,13: 1013 1023 cases stmt_typed * #srcrs1_prf #srcrs2_prf #dstr_prf 1014 [ 1,2: @(lenv_typed_arg_typed_ok1 … lenv_typed) assumption1015  @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption1016  @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs2_prf)1017  @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs1_prf)1018  @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_prf)1024 [5,6: @(lenv_typed_arg_typed_ok1 … lenv_typed) assumption 1025 4: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption 1026 3: @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs2_prf) 1027 2: @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs1_prf) 1028 1: @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_prf) 1019 1029 ] 1020 1030 *: cases daemon (* TODO *) … … 1022 1032 qed. 1023 1033 1024 (* XXX: we use a "hack" here to circumvent the proof obligations required to1025 create res, an empty internal_function record. we insert into our graph1026 the start and end nodes to ensure that they are in, and place dummy1027 skip instructions at these nodes. *)1028 1034 definition translate_internal : 1029 1035 ∀globals.internal_function → (* insert here more properties *) … … 1035 1041 let stack_size' ≝ f_stacksize def in 1036 1042 let entry' ≝ f_entry def in 1037 let exit' ≝ f_exit def in 1038 let init ≝ init_graph_if RTL globals luniverse' runiverse' [ ] [ ] 1039 [ ] stack_size' (pi1 … entry') (pi1 … exit') in 1043 let init ≝ init_graph_if RTL globals luniverse' runiverse' [ ] 1044 [ ] stack_size' (pi1 … entry') in 1040 1045 let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals 1041 1046 (f_locals def) (f_params def) (f_result def) init in … … 1044 1049 let f_trans ≝ λlbl,stmt,def. 1045 1050 let pr ≝ translate_statement … vars lenv ? stmt ? in 1046 b_adds_graph … (rtl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in 1051 match dpi1 … pr return λx.match x with [ inl _ ⇒ label  _ ⇒ unit ] → ? with 1052 [ inl instrs ⇒ λlbl'.b_adds_graph … instrs lbl lbl' def 1053  inr instrs ⇒ λ_.b_fin_adds_graph … instrs lbl def 1054 ] (dpi2 … pr) in 1047 1055 foldi … f_trans (f_graph def) init'. (* TODO *) cases daemon 1048 1056 qed.
Note: See TracChangeset
for help on using the changeset viewer.