Changeset 2208 for src/RTLabs/RTLabsToRTL_paolo.ma
 Timestamp:
 Jul 18, 2012, 1:26:43 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL_paolo.ma
r2162 r2208 8 8 include alias "ASM/BitVector.ma". 9 9 include alias "arithmetics/nat.ma". 10 11 10 definition size_of_sig_type ≝ 12 11 λsig. … … 16 15 isize' ÷ (nat_of_bitvector ? int_size) 17 16  ASTfloat _ ⇒ ? (* dpm: not implemented *) 18  ASTptr rgn ⇒ nat_of_bitvector ? ptr_size19 ]. 20 cases not_implemented ;17  ASTptr ⇒ 2 (* rgn ⇒ nat_of_bitvector ? ptr_size *) 18 ]. 19 cases not_implemented 21 20 qed. 22 21 … … 46 45 qed. 47 46 48 definition find_local_env_arg ≝49 λr,lenv,prf. map … Reg(find_local_env r lenv prf).47 definition find_local_env_arg : register → local_env → ? → list psd_argument ≝ 48 λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf). 50 49 51 50 definition m_fresh : ∀tag.state_monad (universe tag) (identifier tag) ≝ … … 97 96 include alias "common/Identifiers.ma". 98 97 let rec rtl_args (args : list register) (env : local_env) on args : 99 All ? (λr.bool_to_Prop (r∈env)) args → list rtl_argument ≝98 All ? (λr.bool_to_Prop (r∈env)) args → list psd_argument ≝ 100 99 match args return λx.All ?? x → ? with 101 100 [ nil ⇒ λ_.[ ] … … 131 130 ∀globals. Op2 → 132 131 ∀dests : list register. 133 ∀srcrs1 : list rtl_argument.134 ∀srcrs2 : list rtl_argument.132 ∀srcrs1 : list psd_argument. 133 ∀srcrs2 : list psd_argument. 135 134 dests = srcrs1 → srcrs1 = srcrs2 → 136 135 list (joint_seq rtl_params globals) … … 149 148 ] @ map3 ???? (OP2 rtl_params globals op) destrs srcrs1 srcrs2 prf1 prf2. 150 149 151 let rec nat_to_args (size : nat) (k : nat) on size : Σl : list rtl_argument.l = size ≝150 let rec nat_to_args (size : nat) (k : nat) on size : Σl : list psd_argument.l = size ≝ 152 151 match size with 153 152 [ O ⇒ [ ] 154 153  S size' ⇒ 155 match nat_to_args size' (k ÷ 8) with 156 [ mk_Sig res prf ⇒ 157 imm_nat k :: res 158 ] 159 ]. normalize // qed. 154 (byte_of_nat k : psd_argument) :: nat_to_args size' (k ÷ 8) 155 ]. [ %  cases (nat_to_args ??) #res #EQ normalize >EQ % ] qed. 160 156 161 157 definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with … … 168 164 definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst. 169 165 match cst with 170 [ Oaddrsymbol r id offset⇒ member id (eq_identifier ?) globals166 [ Oaddrsymbol id _ ⇒ member id (eq_identifier ?) globals 171 167  _ ⇒ True 172 168 ]. … … 185 181 with 186 182 [ Ointconst size sign const ⇒ λcst_prf,prf. 187 map2 … (λr.λb : Byte.r ← (b : rtl_argument)) destrs183 map2 … (λr.λb : Byte.r ← b) destrs 188 184 (split_into_bytes size const) ? 189 185  Ofloatconst _ _ ⇒ ? 190  Oaddrsymbol rid offset ⇒ λcst_prf,prf.186  Oaddrsymbol id offset ⇒ λcst_prf,prf. 191 187 let 〈r1, r2〉 ≝ make_addr … destrs ? in 192 188 [ADDRESS rtl_params globals id ? r1 r2] … … 206 202 ∀globals. 207 203 ∀destrs: list register. 208 ∀srcrs: list rtl_argument.204 ∀srcrs: list psd_argument. 209 205 destrs = srcrs → list (joint_seq rtl_params globals) ≝ 210 206 λglobals,destrs,srcrs,length_eq. … … 229 225 *) 230 226 λglobals,destr,srcr. 231 [destr ← srcr .Or. 127 ; 227 let byte_127 : Byte ≝ false ::: maximum ? in 228 [destr ← srcr .Or. byte_127 ; 232 229 destr ← .Rl. destr ; 233 230 destr ← .Inc. destr ; … … 241 238 ν tmp in 242 239 (sign_mask ? tmp srcr @ 243 translate_move ? destrs (make_list ? (Reg tmp) (destrs)) (make_list_length …)).240 translate_move ? destrs (make_list ? (Reg ? tmp) (destrs)) (make_list_length …)). 244 241 245 242 definition translate_fill_with_zero : … … 282 279 let dst_rest ≝ \snd (\snd t) in 283 280 (* first, move the common part *) 284 translate_move ? src_common (map … Regdst_common) ? @@281 translate_move ? src_common (map … (Reg ?) dst_common) ? @@ 285 282 match src_rest return λ_.bind_new ?? with 286 283 [ nil ⇒ (* upcast *) … … 314 311 match nat_to_args (destrs) 1 with 315 312 [ mk_Sig res prf' ⇒ 316 translate_op ? Add destrs (map … Regdestrs) res ??317 ]. 318 // qed.313 translate_op ? Add destrs (map … (Reg ?) destrs) res ?? 314 ]. 315 >length_map // qed. 319 316 320 317 definition translate_notbool: … … 328 325 translate_fill_with_zero ? destrs' @@ 329 326 match srcrs return λ_.bind_new ?? with 330 [ nil ⇒ [destr ← 0]327 [ nil ⇒ [destr ← zero_byte] 331 328  cons srcr srcrs' ⇒ 332 329 (destr ← srcr) ::: … … 336 333 (* many uses of 0, better not use immediates *) 337 334 ν tmp in 338 [tmp ← 0;335 [tmp ← zero_byte ; 339 336 destr ← tmp .Sub. tmp ; 340 337 (* now carry bit is set iff destr was nonnull *) … … 363 360  Onotint sz sg ⇒ λeq1,eq2. 364 361 translate_notint globals destrs srcrs ? 365  Optrofint sz sg r⇒ λeq1,eq2.362  Optrofint sz sg ⇒ λeq1,eq2. 366 363 translate_cast globals Unsigned destrs srcrs 367  Ointofptr sz sg r⇒ λeq1,eq2.364  Ointofptr sz sg ⇒ λeq1,eq2. 368 365 translate_cast globals Unsigned destrs srcrs 369 366  Oid t ⇒ λeq1,eq2. 370 translate_move globals destrs (map … Regsrcrs) ?367 translate_move globals destrs (map … (Reg ?) srcrs) ? 371 368  _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *) 372 369 ] (refl …) (refl …). 373 [3,4,5,6,7,8,9: cases not_implemented374 *: destruct >prf1 >prf2 //370 [3,4,5,6,7,8,9: (* floats *) cases not_implemented 371 *: destruct >prf1 >prf2 [3: >length_map ] // 375 372 ] 376 373 qed. … … 401 398 (* the temporary destination, with a dummy register at the end *) 402 399 ∀tmp_destrs_dummy : list register. 403 ∀srcrs1,srcrs2 : list rtl_argument.400 ∀srcrs1,srcrs2 : list psd_argument. 404 401 tmp_destrs_dummy = S n → 405 402 n = srcrs1 → … … 431 428 for the bit to be carried. Redundant calculations will be eliminated 432 429 by constant propagation. *) 433 let args : list rtl_argument ≝434 [Reg a;Reg b] @ make_list ? (Imm (zero …)) (n  1  k) in430 let args : list psd_argument ≝ 431 [Reg ? a;Reg ? b] @ make_list ? (zero_byte : psd_argument) (n  1  k) in 435 432 let tmp_destrs_view : list register ≝ 436 433 ltl ? tmp_destrs_dummy k in 437 434 ❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k  i) srcrs2 ?) :: 438 translate_op … Add tmp_destrs_view (map … Regtmp_destrs_view) args ?? @435 translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @ 439 436 acc 440 437 ]. … … 452 449 [2: @le_plus_to_minus_r <plus_n_Sm <plus_n_O assumption] 453 450 cut (S n = 2 + (n  1)) 454 [2: #EQ >EQ //]451 [2: #EQ >EQ %] 455 452 >plus_minus_commutative 456 453 [2: @(transitive_le … k_prf) //] 457 454 @sym_eq 458 @plus_to_minus 459 <plus_n_Sm 460 // 455 @plus_to_minus % 461 456 ] qed. 462 457 … … 464 459 λglobals : list ident. 465 460 λdestrs : list register. 466 λsrcrs1 : list rtl_argument.467 λsrcrs2 : list rtl_argument.461 λsrcrs1 : list psd_argument. 462 λsrcrs2 : list psd_argument. 468 463 λsrcrs1_prf : destrs = srcrs1. 469 464 λsrcrs2_prf : srcrs1 = srcrs2. … … 494 489 foldr … translate_mul_k [ ] (range_strong (destrs)) @ 495 490 (* epilogue: saving the result *) 496 translate_move … destrs (map … Regtmp_destrs) ?.491 translate_move … destrs (map … (Reg ?) tmp_destrs) ?. 497 492 [ >length_map >tmp_destrs_prf // 498 493  >length_append <plus_n_Sm <plus_n_O // … … 505 500 λdiv_not_mod: bool. 506 501 λdestrs: list register. 507 λsrcrs1: list rtl_argument.508 λsrcrs2: list rtl_argument.502 λsrcrs1: list psd_argument. 503 λsrcrs2: list psd_argument. 509 504 λsrcrs1_prf : destrs = srcrs1. 510 505 λsrcrs2_prf : srcrs1 = srcrs2. … … 551 546 λglobals: list ident. 552 547 λdestrs: list register. 553 λsrcrs1: list rtl_argument.554 λsrcrs2: list rtl_argument.548 λsrcrs1: list psd_argument. 549 λsrcrs2: list psd_argument. 555 550 match destrs return λ_.srcrs1 = srcrs2 → bind_new ?? with 556 551 [ nil ⇒ λ_.[ ] … … 558 553 translate_fill_with_zero … destrs' @@ 559 554 match srcrs1 return λx.x = srcrs2 → bind_new ?? with 560 [ nil ⇒ λ_.[destr ← 0]555 [ nil ⇒ λ_.[destr ← zero_byte] 561 556  cons srcr1 srcrs1' ⇒ 562 557 match srcrs2 return λx.S (srcrs1') = x → bind_new ?? with … … 564 559  cons srcr2 srcrs2' ⇒ λEQ. 565 560 νtmpr in 566 let f : rtl_argument → rtl_argument → list (joint_seq rtl_params globals) → list (joint_seq rtl_params globals) ≝561 let f : psd_argument → psd_argument → list (joint_seq rtl_params globals) → list (joint_seq rtl_params globals) ≝ 567 562 λs1,s2,acc. 568 563 tmpr ← s1 .Xor. s2 :: … … 571 566 let epilogue : list (joint_seq rtl_params globals) ≝ 572 567 [ CLEAR_CARRY ?? ; 573 tmpr ← 0.Sub. destr ;568 tmpr ← zero_byte .Sub. destr ; 574 569 (* now carry bit is 1 iff destrs != 0 *) 575 destr ← 0 .Addc. 0] in570 destr ← zero_byte .Addc. zero_byte ] in 576 571 destr ← srcr1 .Xor. srcr2 :: 577 572 foldr2 ??? f epilogue srcrs1' srcrs2' ? … … 593 588 ∀globals. 594 589 ∀destrs: list register. 595 ∀srcrs1: list rtl_argument.596 ∀srcrs2: list rtl_argument.590 ∀srcrs1: list psd_argument. 591 ∀srcrs2: list psd_argument. 597 592 srcrs1 = srcrs2 → 598 593 bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝ … … 605 600 (* I perform a subtraction, but the only interest is in the carry bit *) 606 601 translate_op ? Sub (make_list … tmpr (srcrs1)) srcrs1 srcrs2 ? srcrs_prf @ 607 [ destr ← 0 .Addc. 0])602 [ destr ← zero_byte .Addc. zero_byte ]) 608 603 ]. 609 604 <make_list_length % qed. … … 613 608 let rec shift_signed globals 614 609 (tmp : register) 615 (srcrs : list rtl_argument) on srcrs : 616 Σt : (list rtl_argument) × (list (joint_seq rtl_params globals)).\fst t = srcrs ≝ 610 (srcrs : list psd_argument) on srcrs : 611 Σt : (list psd_argument) × (list (joint_seq rtl_params globals)).\fst t = srcrs ≝ 612 let byte_128 : Byte ≝ true ::: bv_zero ? in 617 613 match srcrs with 618 614 [ nil ⇒ 〈[ ],[ ]〉 619 615  cons srcr srcrs' ⇒ 620 616 match srcrs' with 621 [ nil ⇒ 〈[ Reg tmp ], [ tmp ← srcr .Add.128 ]〉617 [ nil ⇒ 〈[ Reg ? tmp ], [ tmp ← srcr .Add. byte_128 ]〉 622 618  _ ⇒ 623 619 let re ≝ shift_signed globals tmp srcrs' in … … 632 628 ∀globals. 633 629 ∀destrs: list register. 634 ∀srcrs1: list rtl_argument.635 ∀srcrs2: list rtl_argument.630 ∀srcrs1: list psd_argument. 631 ∀srcrs2: list psd_argument. 636 632 srcrs1 = srcrs2 → 637 633 bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝ … … 684 680 ∀globals.∀ty1,ty2,ty3.∀op : binary_operation ty1 ty2 ty3. 685 681 ∀destrs : list register. 686 ∀srcrs1,srcrs2 : list rtl_argument.682 ∀srcrs1,srcrs2 : list psd_argument. 687 683 destrs = size_of_sig_type ty3 → 688 684 srcrs1 = size_of_sig_type ty1 → … … 695 691 [ Oadd sz sg ⇒ λprf1,prf2,prf3. 696 692 translate_op globals Add destrs srcrs1 srcrs2 ?? 697  Oaddp sz r⇒ λprf1,prf2,prf3.693  Oaddp sz ⇒ λprf1,prf2,prf3. 698 694 let is_Oaddp ≝ 0 in 699 695 translate_op globals Add destrs srcrs1 srcrs2 ?? 700 696  Osub sz sg ⇒ λprf1,prf2,prf2. 701 697 translate_op globals Sub destrs srcrs1 srcrs2 ?? 702  Osubpi sz r⇒ λprf1,prf2,prf3.698  Osubpi sz ⇒ λprf1,prf2,prf3. 703 699 let is_Osubpi ≝ 0 in 704 700 translate_op globals Sub destrs srcrs1 srcrs2 ?? 705  Osubpp sz r1 r2⇒ λprf1,prf2,prf3.701  Osubpp sz ⇒ λprf1,prf2,prf3. 706 702 let is_Osubpp ≝ 0 in 707 703 translate_op globals Sub destrs srcrs1 srcrs2 ?? … … 722 718  Ocmpu sz sg c ⇒ λprf1,prf2,prf3. 723 719 translate_cmp true globals c destrs srcrs1 srcrs2 ? 724  Ocmpp rsg c ⇒ λprf1,prf2,prf3.720  Ocmpp sg c ⇒ λprf1,prf2,prf3. 725 721 let is_Ocmpp ≝ 0 in 726 722 translate_cmp true globals c destrs srcrs1 srcrs2 ? 727 723  _ ⇒ ⊥ (* assert false, implemented in run time or float op *) 728 ]. // try @not_implemented724 ]. try @not_implemented // 729 725 (* pointer arithmetics is broken at the moment *) 730 726 cases daemon … … 749 745 definition translate_load : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝ 750 746 λglobals: list ident. 751 λaddr : list rtl_argument.747 λaddr : list psd_argument. 752 748 λaddr_prf: 2 = addr. 753 749 λdestrs: list register. … … 755 751 ν tmp_addr_h in 756 752 let f ≝ λdestr : register.λacc : list (joint_seq rtl_params globals). 757 LOAD rtl_params globals destr (Reg tmp_addr_l) (Regtmp_addr_h) ::758 translate_op …Add753 LOAD rtl_params globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) :: 754 translate_op ? Add 759 755 [tmp_addr_l ; tmp_addr_h] 760 [ Reg tmp_addr_l ; Regtmp_addr_h]761 [ imm_nat 0 ; Imm int_size] ? ? @ acc in756 [tmp_addr_l ; tmp_addr_h] 757 [zero_byte ; (int_size : Byte)] ? ? @ acc in 762 758 translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@ 763 759 foldr … f [ ] destrs. 764 [1: <addr_prf] // qed. 760 [1: <addr_prf 761 ] // qed. 765 762 766 763 definition translate_store : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝ 767 764 λglobals: list ident. 768 λaddr : list rtl_argument.765 λaddr : list psd_argument. 769 766 λaddr_prf: 2 = addr. 770 λsrcrs: list rtl_argument.767 λsrcrs: list psd_argument. 771 768 ν tmp_addr_l in 772 769 ν tmp_addr_h in 773 let f ≝ λsrcr : rtl_argument.λacc : list (joint_seq rtl_params globals).774 STORE rtl_params globals (Reg tmp_addr_l) (Regtmp_addr_h) srcr ::770 let f ≝ λsrcr : psd_argument.λacc : list (joint_seq rtl_params globals). 771 STORE rtl_params globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr :: 775 772 translate_op … Add 776 773 [tmp_addr_l ; tmp_addr_h] 777 [ Reg tmp_addr_l ; Regtmp_addr_h]778 [ imm_nat 0 ; Imm int_size] ? ? @ acc in774 [tmp_addr_l ; tmp_addr_h] 775 [zero_byte ; (int_size : Byte)] ? ? @ acc in 779 776 translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@ 780 777 foldr … f [ ] srcrs.
Note: See TracChangeset
for help on using the changeset viewer.