Changeset 2214 for src/RTLabs
 Timestamp:
 Jul 19, 2012, 2:42:02 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL_paolo.ma
r2208 r2214 133 133 ∀srcrs2 : list psd_argument. 134 134 dests = srcrs1 → srcrs1 = srcrs2 → 135 list (joint_seq rtl_paramsglobals)135 list (joint_seq RTL globals) 136 136 ≝ 137 137 λglobals: list ident. … … 146 146  Sub ⇒ [CLEAR_CARRY ??] 147 147  _ ⇒ [ ] 148 ] @ map3 ???? (OP2 rtl_paramsglobals op) destrs srcrs1 srcrs2 prf1 prf2.148 ] @ map3 ???? (OP2 RTL globals op) destrs srcrs1 srcrs2 prf1 prf2. 149 149 150 150 let rec nat_to_args (size : nat) (k : nat) on size : Σl : list psd_argument.l = size ≝ … … 174 174 ∀destrs: list register. 175 175 destrs = size_of_cst ? cst_sig → 176 list (joint_seq rtl_paramsglobals)176 list (joint_seq RTL globals) 177 177 ≝ 178 178 λty,globals,cst_sig,destrs. … … 186 186  Oaddrsymbol id offset ⇒ λcst_prf,prf. 187 187 let 〈r1, r2〉 ≝ make_addr … destrs ? in 188 [ADDRESS rtl_paramsglobals id ? r1 r2]188 [ADDRESS RTL globals id ? r1 r2] 189 189  Oaddrstack offset ⇒ λcst_prf,prf. 190 190 let 〈r1, r2〉 ≝ make_addr … destrs ? in 191 [(rtl_stack_address r1 r2 : joint_seq rtl_paramsglobals)]191 [(rtl_stack_address r1 r2 : joint_seq RTL globals)] 192 192 ] (pi2 … cst_sig). 193 193 [2: cases not_implemented … … 203 203 ∀destrs: list register. 204 204 ∀srcrs: list psd_argument. 205 destrs = srcrs → list (joint_seq rtl_paramsglobals) ≝205 destrs = srcrs → list (joint_seq RTL globals) ≝ 206 206 λglobals,destrs,srcrs,length_eq. 207 207 map2 … (λdst,src.dst ← src) destrs srcrs length_eq. … … 216 216 217 217 definition sign_mask : ∀globals.register → register → 218 list (joint_seq rtl_paramsglobals) ≝218 list (joint_seq RTL globals) ≝ 219 219 (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that: 220 220 byte in destr if srcr is: neg  pos … … 234 234 ∀globals : list ident. 235 235 list register → register → 236 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝236 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 237 237 λglobals,destrs,srcr. 238 238 ν tmp in … … 242 242 definition translate_fill_with_zero : 243 243 ∀globals : list ident. 244 list register → list (joint_seq rtl_paramsglobals) ≝244 list register → list (joint_seq RTL globals) ≝ 245 245 λglobals,destrs. 246 246 match nat_to_args (destrs) 0 with … … 270 270 ∀globals: list ident. 271 271 signedness → list register → list register → 272 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝272 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 273 273 λglobals,src_sign,destrs,srcrs. 274 274 match reduce_strong ?? destrs srcrs with … … 299 299 ∀destrs : list register. 300 300 ∀srcrs_arg : list register. 301 destrs = srcrs_arg → list (joint_seq rtl_paramsglobals) ≝301 destrs = srcrs_arg → list (joint_seq RTL globals) ≝ 302 302 λglobals, destrs, srcrs, prf. 303 map2 ??? (OP1 rtl_paramsglobals Cmpl) destrs srcrs prf.304 305 definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝303 map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf. 304 305 definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 306 306 λglobals: list ident. 307 307 λdestrs: list register. … … 318 318 ∀globals : list ident. 319 319 list register → list register → 320 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝320 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 321 321 λglobals,destrs,srcrs. 322 322 match destrs with … … 328 328  cons srcr srcrs' ⇒ 329 329 (destr ← srcr) ::: 330 map register (joint_seq rtl_paramsglobals) (λr. destr ← destr .Or. r) srcrs' @@330 map register (joint_seq RTL globals) (λr. destr ← destr .Or. r) srcrs' @@ 331 331 (* now destr is nonnull iff srcrs was nonnull *) 332 332 CLEAR_CARRY ?? ::: … … 341 341 342 342 definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? → 343 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝343 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 344 344 λglobals. 345 345 λty, ty'. … … 351 351 match op1 352 352 return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' → 353 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) with353 bind_new (localsT RTL) (list (joint_seq RTL globals)) with 354 354 [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2. 355 355 translate_cast globals src_sign destrs srcrs … … 410 410 (Σi.i<S k) → 411 411 (* the accumulator *) 412 list (joint_seq rtl_paramsglobals) →413 list (joint_seq rtl_paramsglobals) ≝412 list (joint_seq RTL globals) → 413 list (joint_seq RTL globals) ≝ 414 414 λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2, 415 415 tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc. … … 456 456 ] qed. 457 457 458 definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝458 definition translate_mul : ∀globals.?→?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 459 459 λglobals : list ident. 460 460 λdestrs : list register. … … 472 472 (* the step calculating all products with least significant byte going in the 473 473 kth position of the result *) 474 let translate_mul_k : (Σk.k<destrs) → list (joint_seq rtl_paramsglobals) →475 list (joint_seq rtl_paramsglobals) ≝474 let translate_mul_k : (Σk.k<destrs) → list (joint_seq RTL globals) → 475 list (joint_seq RTL globals) ≝ 476 476 λk_sig,acc.match k_sig with 477 477 [ mk_Sig k k_prf ⇒ … … 496 496 497 497 definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→ 498 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝498 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 499 499 λglobals: list ident. 500 500 λdiv_not_mod: bool. … … 543 543 544 544 definition translate_ne: ∀globals: list ident.?→?→?→?→ 545 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝545 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 546 546 λglobals: list ident. 547 547 λdestrs: list register. … … 559 559  cons srcr2 srcrs2' ⇒ λEQ. 560 560 νtmpr in 561 let f : psd_argument → psd_argument → list (joint_seq rtl_params globals) → list (joint_seq rtl_paramsglobals) ≝561 let f : psd_argument → psd_argument → list (joint_seq RTL globals) → list (joint_seq RTL globals) ≝ 562 562 λs1,s2,acc. 563 563 tmpr ← s1 .Xor. s2 :: 564 564 destr ← destr .Or. tmpr :: 565 565 acc in 566 let epilogue : list (joint_seq rtl_paramsglobals) ≝566 let epilogue : list (joint_seq RTL globals) ≝ 567 567 [ CLEAR_CARRY ?? ; 568 568 tmpr ← zero_byte .Sub. destr ; … … 577 577 (* if destrs is 0 or 1, it inverses it. To be used after operations that 578 578 ensure this. *) 579 definition translate_toggle_bool : ∀globals.?→list (joint_seq rtl_paramsglobals) ≝579 definition translate_toggle_bool : ∀globals.?→list (joint_seq RTL globals) ≝ 580 580 λglobals: list ident. 581 581 λdestrs: list register. … … 591 591 ∀srcrs2: list psd_argument. 592 592 srcrs1 = srcrs2 → 593 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝593 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 594 594 λglobals,destrs,srcrs1,srcrs2,srcrs_prf. 595 595 match destrs with … … 609 609 (tmp : register) 610 610 (srcrs : list psd_argument) on srcrs : 611 Σt : (list psd_argument) × (list (joint_seq rtl_paramsglobals)).\fst t = srcrs ≝611 Σt : (list psd_argument) × (list (joint_seq RTL globals)).\fst t = srcrs ≝ 612 612 let byte_128 : Byte ≝ true ::: bv_zero ? in 613 613 match srcrs with … … 631 631 ∀srcrs2: list psd_argument. 632 632 srcrs1 = srcrs2 → 633 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝633 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 634 634 λglobals,destrs,srcrs1,srcrs2,srcrs_prf. 635 635 νtmp_last_s1 in … … 649 649 qed. 650 650 651 definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝651 definition translate_lt : bool→∀globals.?→?→?→?→bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 652 652 λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs_prf. 653 653 if is_unsigned then … … 684 684 srcrs1 = size_of_sig_type ty1 → 685 685 srcrs2 = size_of_sig_type ty2 → 686 bind_new (localsT rtl_params) (list (joint_seq rtl_paramsglobals)) ≝686 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 687 687 λglobals,ty1,ty2,ty3,op2,destrs,srcrs1,srcrs2. 688 688 match op2 return λty1,ty2,ty3.λx : binary_operation ty1 ty2 ty3. … … 728 728 729 729 definition translate_cond: ∀globals: list ident. list register → label → 730 bind_seq_block rtl_params globals (joint_step rtl_paramsglobals) ≝730 bind_seq_block RTL globals (joint_step RTL globals) ≝ 731 731 λglobals: list ident. 732 732 λsrcrs: list register. 733 733 λlbl_true: label. 734 match srcrs return λ_.bind_seq_block rtl_params? (joint_step ??) with734 match srcrs return λ_.bind_seq_block RTL ? (joint_step ??) with 735 735 [ nil ⇒ bret … 〈[ ], NOOP ??〉 736 736  cons srcr srcrs' ⇒ 737 737 ν tmpr in 738 let f : register → joint_seq rtl_paramsglobals ≝738 let f : register → joint_seq RTL globals ≝ 739 739 λr. tmpr ← tmpr .Or. r in 740 bret … 〈MOVE rtl_paramsglobals 〈tmpr,srcr〉 ::740 bret … 〈MOVE RTL globals 〈tmpr,srcr〉 :: 741 741 map ?? f srcrs', (COND … tmpr lbl_true : joint_step ??) 〉 742 742 ]. 743 743 744 744 (* Paolo: to be controlled (original seemed overly complex) *) 745 definition translate_load : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝745 definition translate_load : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝ 746 746 λglobals: list ident. 747 747 λaddr : list psd_argument. … … 750 750 ν tmp_addr_l in 751 751 ν tmp_addr_h in 752 let f ≝ λdestr : register.λacc : list (joint_seq rtl_paramsglobals).753 LOAD rtl_paramsglobals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) ::752 let f ≝ λdestr : register.λacc : list (joint_seq RTL globals). 753 LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) :: 754 754 translate_op ? Add 755 755 [tmp_addr_l ; tmp_addr_h] … … 761 761 ] // qed. 762 762 763 definition translate_store : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝763 definition translate_store : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝ 764 764 λglobals: list ident. 765 765 λaddr : list psd_argument. … … 768 768 ν tmp_addr_l in 769 769 ν tmp_addr_h in 770 let f ≝ λsrcr : psd_argument.λacc : list (joint_seq rtl_paramsglobals).771 STORE rtl_paramsglobals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr ::770 let f ≝ λsrcr : psd_argument.λacc : list (joint_seq RTL globals). 771 STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr :: 772 772 translate_op … Add 773 773 [tmp_addr_l ; tmp_addr_h] … … 780 780 definition translate_statement : ∀globals.local_env → statement → 781 781 𝚺b : 782 bind_seq_block rtl_params globals (joint_step rtl_paramsglobals) +783 bind_seq_block rtl_params globals (joint_fin_step rtl_params).782 bind_seq_block RTL globals (joint_step RTL globals) + 783 bind_seq_block RTL globals (joint_fin_step RTL). 784 784 if is_inl … b then label else unit ≝ 785 785 λglobals,lenv,stmt. … … 812 812 ❬(match retr with 813 813 [ Some retr ⇒ 814 CALL_ID rtl_params? f (rtl_args args lenv ?) (find_local_env retr lenv ?)814 CALL_ID RTL ? f (rtl_args args lenv ?) (find_local_env retr lenv ?) 815 815  None ⇒ 816 CALL_ID rtl_params? f (rtl_args args lenv ?) [ ]816 CALL_ID RTL ? f (rtl_args args lenv ?) [ ] 817 817 ] : bind_seq_block ???), lbl'❭ 818 818  St_call_ptr f args retr lbl' ⇒ … … 882 882 let entry' ≝ f_entry def in 883 883 let exit' ≝ f_exit def in 884 let graph' ≝ empty_map LabelTag (joint_statement rtl_paramsglobals) in884 let graph' ≝ empty_map LabelTag (joint_statement RTL globals) in 885 885 let graph' ≝ add LabelTag ? graph' entry' 886 886 (GOTO … exit') in … … 891 891 b_adds_graph … (rtl_ertl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in 892 892 let res ≝ 893 mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'893 mk_joint_internal_function RTL globals luniverse' runiverse' result' params' 894 894 locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in 895 895 foldi … f_trans (f_graph def) res.
Note: See TracChangeset
for help on using the changeset viewer.