Changeset 1636 for src/RTLabs/RTLabsToRTL_paolo.ma
- Timestamp:
- Jan 9, 2012, 12:38:32 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabsToRTL_paolo.ma
r1635 r1636 8 8 include alias "ASM/BitVector.ma". 9 9 include alias "arithmetics/nat.ma". 10 11 12 (* Paolo: to be moved elsewhere *) 13 14 notation "r ← a1 .op. a2" with precedence 50 for 15 @{'op2 $op $r $a1 $a2}. 16 notation "r ← . op . a" with precedence 50 for 17 @{'op1 $op $r $a}. 18 notation "r ← a" with precedence 50 for 19 @{'mov $r $a}. 20 notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for 21 @{'opaccs $op $r $s $a1 $a2}. 22 23 interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2). 24 interpretation "op1" 'op1 op r a = (OP1 ? ? op r a). 25 interpretation "move" 'mov r a = (MOVE ? ? (REG r a)). 26 interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2). 27 10 28 11 29 definition size_of_sig_type ≝ … … 138 156 λsrcrs2. 139 157 λprf1,prf2. 140 let f_add ≝ λop,destr,srcr1,srcr2. 141 OP2 rtl_params globals op destr srcr1 srcr2 in 158 let f_add ≝ OP2 rtl_params globals in 142 159 let res : list (rtl_instruction globals) ≝ 143 160 map3 ???? (f_add op) destrs srcrs1 srcrs2 ?? in … … 166 183 ] (refl …) 167 184 | _ ⇒ res 168 ]. 185 ]. 169 186 [5,6: assumption 170 187 |1: >prf1 in eq_destrs; >eq_srcrs1 normalize // … … 238 255 |destrs| = |srcrs| → list (rtl_instruction globals) ≝ 239 256 λglobals,destrs,srcrs,length_eq. 240 map2 … (λdst,src. MOVE rtl_params … (REG dst src)) destrs srcrs length_eq.257 map2 … (λdst,src.dst ← src) destrs srcrs length_eq. 241 258 242 259 let rec make … … 269 286 *) 270 287 λglobals,destr,srcr. 271 [ OP2 … Or destr (Reg srcr) (imm_nat 127);272 OP1 … Rl destrdestr ;273 OP1 … Inc destrdestr ;274 OP1 … Cmpl destrdestr ].288 [destr ← srcr .Or. 127 ; 289 destr ← .Rl. destr ; 290 destr ← .Inc. destr ; 291 destr ← .Cmpl. destr ]. 275 292 276 293 definition translate_cast_signed : … … 354 371 translate_cast_unsigned ? destrs' @ (* fill destrs' with 0 *) 355 372 match srcrs with 356 [ nil ⇒ [ reg_from_nat … destr0]373 [ nil ⇒ [destr ← 0] 357 374 | cons srcr srcrs' ⇒ 358 375 let f : register → rtl_instruction globals ≝ … … 364 381 (* many uses of 0, better not use immediates *) 365 382 ν tmp in 366 [ reg_from_nat … tmp0 ;367 OP2 … Sub destr (Reg tmp) (Reg tmp);383 [tmp ← 0 ; 384 destr ← tmp .Sub. tmp ; 368 385 (* now carry bit is set iff destr was non-null *) 369 OP2 … Addc destr (Reg tmp) (Reg tmp)]386 destr ← tmp .Addc. tmp] 370 387 ] 371 388 ]. … … 461 478 let tmp_destrs_view : list register ≝ 462 479 ltl ? tmp_destrs_dummy k in 463 OPACCS rtl_params globals Mul a b 464 (nth_safe ? i srcrs1 ?) 465 (nth_safe ? (k - i) srcrs2 ?) :: 480 ❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?) :: 466 481 translate_op … Add tmp_destrs_view (map … Reg tmp_destrs_view) args ?? @ 467 482 acc … … 501 516 (* temporary registers for the result are created, so to avoid overwriting 502 517 sources *) 503 νν tmp_destrs:|destrs| with tmp_destrs_prf in518 νν tmp_destrs × |destrs| with tmp_destrs_prf in 504 519 νdummy in 505 520 (* the step calculating all products with least significant byte going in the … … 520 535 for i in 0 ... k do 521 536 translate_mul_i … k … i *) 522 foldr … translate_mul_k [ ] (range_strong (|destrs|)) @ 537 foldr … translate_mul_k [ ] (range_strong (|destrs|)) @ 523 538 (* epilogue: saving the result *) 524 539 translate_move … destrs (map … Reg tmp_destrs) ?. … … 552 567 let 〈destr1, destr2〉 ≝ 553 568 if div_not_mod then 〈destr, dummy〉 else 〈dummy, destr〉 in 554 [ OPACCS rtl_params globals DivuModu destr1 destr2 srcr1srcr2]569 [❮destr1, destr2❯ ← srcr1 .DivuModu. srcr2] 555 570 ] (refl …) 556 571 ] (refl …) … … 561 576 destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct qed. 562 577 578 (* Paolo: to be moved elsewhere *) 563 579 let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (f : A→B→C→C) (init : C) (l1 : list A) (l2 : list B) 564 580 (prf : |l1| = |l2|) on l1 : C ≝ … … 572 588 ] (refl …) 573 589 ] (refl …). 574 [destruct normalize in prf; destruct 575 |destruct normalize in prf; // 576 ] qed. 577 578 let rec foldr3 (A : Type[0]) (B : Type[0]) (C : Type[0]) (D : Type[0]) 579 (f : A→B→C→D→D) (init : D) (l1 : list A) (l2 : list B) (l3 : list C) 580 (prf1 : |l1| = |l2|) (prf2 : |l2| = |l3|) on l1 : D ≝ 581 match l1 return λx.x = l1 → D with 582 [ nil ⇒ λ_.init 583 | cons a l1' ⇒ λeq_l1. 584 match l2 return λy.y = l2 → D with 585 [ nil ⇒ λeq_l2.⊥ 586 | cons b l2' ⇒ λeq_l2. 587 match l3 return λz.z = l3 → D with 588 [ nil ⇒ λeq_l3.⊥ 589 | cons c l3' ⇒ λeq_l3. 590 f a b c (foldr3 A B C D f init l1' l2' l3' ? ?) 591 ] (refl …) 592 ] (refl …) 593 ] (refl …). 594 destruct normalize in prf1; normalize in prf2; destruct // qed. 590 destruct normalize in prf; [destruct|//] 591 qed. 595 592 596 593 definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_instruction globals) ≝ … … 614 611 let f : rtl_argument → rtl_argument → list (rtl_instruction globals) → list (rtl_instruction globals) ≝ 615 612 λs1,s2,acc. 616 OP2 … Xor tmpr s1s2 ::617 OP2 … Or destr (Reg destr) (Reg tmpr)::613 tmpr ← s1 .Xor. s2 :: 614 destr ← destr .Or. tmpr :: 618 615 acc in 619 616 let epilogue : list (rtl_instruction globals) ≝ 620 617 [ clear_carry … ; 621 OP2 … Sub tmpr (Imm (zero …)) (Reg destr);618 tmpr ← 0 .Sub. destr ; 622 619 (* now carry bit is 1 iff destrs != 0 *) 623 OP2 … Addc destr (Imm (zero …)) (Imm (zero …))] in620 destr ← 0 .Addc. 0 ] in 624 621 translate_cast_unsigned … destrs' @ 625 OP2 rtl_params globals Xor destr srcr1srcr2 ::622 destr ← srcr1 .Xor. srcr2 :: 626 623 foldr2 ??? f epilogue srcrs1' srcrs2' ? 627 624 ] (refl …) … … 637 634 match destrs with 638 635 [ nil ⇒ [ ] 639 | cons destr _ ⇒ [ OP1 rtl_params globals Cmpl destrdestr]636 | cons destr _ ⇒ [destr ← .Cmpl. destr] 640 637 ]. 641 638 … … 655 652 (* I perform a subtraction, but the only interest is in the carry bit *) 656 653 translate_op ? Sub (make … destr (|destrs|)) srcrs1 srcrs2 ?? @ 657 [ OP2 … Addc destr (imm_nat 0) (imm_nat 0)]654 [ destr ← 0 .Addc. 0 ] 658 655 ]. 659 656 [ <make_length ] assumption qed. … … 669 666 | cons srcr srcrs' ⇒ 670 667 match srcrs' with 671 [ nil ⇒ 〈[ Reg tmp ], [ OP2 … Add tmp srcr (imm_nat 128)]〉668 [ nil ⇒ 〈[ Reg tmp ], [ tmp ← srcr .Add. 128 ]〉 672 669 | _ ⇒ 673 670 let 〈new_srcrs', op〉 ≝ shift_signed globals tmp srcrs' in
Note: See TracChangeset
for help on using the changeset viewer.