Changeset 1640 for src/RTLabs/RTLabsToRTL_paolo.ma
 Timestamp:
 Jan 11, 2012, 5:41:45 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL_paolo.ma
r1636 r1640 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 for15 @{'op2 $op $r $a1 $a2}.16 notation "r ← . op . a" with precedence 50 for17 @{'op1 $op $r $a}.18 notation "r ← a" with precedence 50 for19 @{'mov $r $a}.20 notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for21 @{'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 … … 141 124 eqb m n = true → m = n. 142 125 #m#n@eqb_elim // #_ #F destruct(F) qed. 143 126 144 127 definition translate_op: 145 128 ∀globals. Op2 → … … 161 144 (* first, clear carry if op relies on it *) 162 145 match op with 163 [ Addc ⇒ [ clear_carry?]164  Sub ⇒ [ clear_carry?]146 [ Addc ⇒ [CLEAR_CARRY ??] 147  Sub ⇒ [CLEAR_CARRY ??] 165 148  _ ⇒ [ ] 166 149 ] @ … … 228 211 match split_into_bytes size const with 229 212 [ mk_Sig bytes bytes_length_proof ⇒ 230 map2 … ( reg_from_byte globals)destrs bytes ?213 map2 … (λr.λb : Byte.r ← (b : rtl_argument)) destrs bytes ? 231 214 ] 232 215  Ofloatconst float ⇒ λ_.⊥ … … 374 357  cons srcr srcrs' ⇒ 375 358 let f : register → rtl_instruction globals ≝ 376 λr. OP2 ?? Or destr (Reg destr) (Reg r)in377 reg_from_reg … srcr destr::359 λr. destr ← destr .Or. r in 360 MOVE rtl_params globals 〈destr,srcr〉 :: 378 361 map … f srcrs' @ 379 362 (* now destr is nonnull iff srcrs was nonnull *) 380 clear_carry …::363 CLEAR_CARRY ? ? :: 381 364 (* many uses of 0, better not use immediates *) 382 365 ν tmp in … … 420 403 ] 421 404 qed. 405 406 include alias "arithmetics/nat.ma". 422 407 423 408 let rec range_strong_internal (start : ℕ) (count : ℕ) … … 615 600 acc in 616 601 let epilogue : list (rtl_instruction globals) ≝ 617 [ clear_carry… ;602 [ CLEAR_CARRY … ; 618 603 tmpr ← 0 .Sub. destr ; 619 604 (* now carry bit is 1 iff destrs != 0 *) … … 782 767  cons srcr srcrs' ⇒ 783 768 ν tmpr in 784 let f ≝ λr. OP2 rtl_params globals Or tmpr (Reg tmpr) (Reg r) in 785 reg_from_reg globals tmpr srcr :: 769 let f : register → rtl_instruction globals ≝ 770 λr. tmpr ← tmpr .Or. r in 771 MOVE rtl_params globals 〈tmpr,srcr〉 :: 786 772 map … f srcrs' @ 787 [ COND …tmpr lbl_true ]773 [ COND ?? tmpr lbl_true ] 788 774 ]. 789 775 … … 926 912 let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse 927 913 (f_params def @ f_locals def) (f_result def) in 928 let param s ≝ map_list_local_env lenv (map … \fst (f_params def)) in914 let parameters ≝ map_list_local_env lenv (map … \fst (f_params def)) in 929 915 let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in 930 916 let result ≝ … … 939 925 let runiverse' ≝ runiverse in 940 926 let result' ≝ result in 941 let params' ≝ param s in927 let params' ≝ parameters in 942 928 let locals' ≝ locals in 943 929 let stack_size' ≝ f_stacksize def in 944 930 let entry' ≝ f_entry def in 945 931 let exit' ≝ f_exit def in 946 let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params globals entry') in 947 let graph' ≝ add LabelTag ? graph' exit' (RETURN rtl_params globals) in 932 let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' 933 (GOTO (rtl_params : params) globals entry') in 934 let graph' ≝ add LabelTag ? graph' exit' 935 (RETURN (rtl_params : params) globals) in 948 936 let res ≝ 949 937 mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'
Note: See TracChangeset
for help on using the changeset viewer.