Changeset 2232 for src/Cminor
 Timestamp:
 Jul 23, 2012, 2:05:10 PM (9 years ago)
 Location:
 src/Cminor
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/initialisation.ma
r2176 r2232 68 68  #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?); 69 69 >(IH1 H1) >(IH2 H2) @refl 70  #s #IH * * #_ #_ #H @(IH H)71  #s #IH * * #_ #_ #H @(IH H)72 70  #l #s #IH * * #_ * 73 71  #l #s #IH * * #_ #_ #H @(IH H) 
src/Cminor/semantics.ma
r2176 r2232 159 159  Some sk ⇒ Some ? sk 160 160 ] 161  St_loop s' ⇒ λInv. find_label l s' (Kseq (St_loop s') k) f en ??162  St_block s' ⇒ λInv. find_label l s' (Kblock k) f en ??163 161  St_label l' s' ⇒ λInv. 164 162 match identifier_eq ? l l' with … … 173 171 try @(π2 (π1 Inv)) 174 172 [ % [ @(π2 Inv)  @kInv ] 175  % [ @Inv  @kInv ]176 173  % [ @(π2 Inv)  @kInv ] 177 174 ] qed. … … 208 205  #sk #_ #E whd in E:(??%?); destruct 209 206 ] 210  #s1 #IH #k #f #en #Inv #kInv @IH211  #s1 #IH #k #f #en #Inv #kInv @IH212 207  #E whd in i:(??%?); cases (identifier_eq Label l a) in i; 213 208 whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct  *; #H cases (H (sym_eq … E)) ] … … 286 281 axiom FailedStore : String. 287 282 axiom BadFunctionValue : String. 288 axiom BadSwitchValue : String.289 axiom UnknownLabel : String.290 283 axiom ReturnMismatch : String. 291 284 … … 329 322 ! b ← eval_bool_of_val v; 330 323 return 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉 331  St_loop s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st〉332  St_block s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kblock k) ? st〉333  St_exit n ⇒ λInv.334 ! k' ← k_exit n k ?? kInv;335 return 〈E0, State f St_skip en fInv ? m sp k' ? st〉336  St_switch sz _ e cs default ⇒ λInv.337 ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;338 match v with339 [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.340 ! k' ← k_exit (find_case ?? i cs default) k ?? kInv;341 return 〈tr, State f St_skip en fInv ? m sp k' ? st〉)342 (Error ? (msg BadSwitchValue))343  _ ⇒ Error ? (msg BadSwitchValue)344 ]345 324  St_return eo ⇒ 346 325 match eo return λeo. stmt_inv f en (St_return eo) → ? with … … 411 390  @(π2 Inv') 412 391  @(π1 Inv') 413  @(pi2 … k')414  @(pi2 … k')415  % [ @Inv  @kInv ]416 392  cases b [ @(π2 (π1 Inv))  @(π2 Inv) ] 417 393  % [ @(π2 Inv)  @kInv ] 418 394  @stmt_inv_update @fInv 419  10,11:395  7,8: 420 396 @(stmt_P_mp … (f_inv f)) 421 397 #s * #V #L % 
src/Cminor/syntax.ma
r2176 r2232 46 46  St_seq : stmt → stmt → stmt 47 47  St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt 48  St_loop : stmt → stmt49  St_block : stmt → stmt50  St_exit : nat → stmt51 (* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)52  St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt53 48  St_return : option (𝚺t. expr t) → stmt 54 49  St_label : identifier Label → stmt → stmt … … 60 55 [ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2 61 56  St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2 62  St_loop s' ⇒ P s ∧ stmt_P P s'63  St_block s' ⇒ P s ∧ stmt_P P s'64 57  St_label _ s' ⇒ P s ∧ stmt_P P s' 65 58  St_cost _ s' ⇒ P s ∧ stmt_P P s' … … 71 64 [ #s1 #s2 * * /2/ 72 65  #sz #sg #e #s1 #s2 * * /2/ 73  3,4: #s * /2/ 74  5,6: #i #s normalize * /2/ 66  *: #i #s normalize * /2/ 75 67 ] qed. 76 68 … … 86 78 *) 87 79  St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P 88  St_switch _ _ e _ _ ⇒ expr_vars ? e P89 80  St_return oe ⇒ match oe with [ None ⇒ True  Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ] 90 81  _ ⇒ True … … 103 94 [ #s1 #s2 #H1 #H2 normalize * * /4/ 104 95  #sz #sg #e #s1 #s2 #H1 #H2 * * /5/ 105  #s #H * /5/106  #s #H * /5/107 96  #l #s #H * /5/ 108 97  #l #s #H * /5/ … … 120 109  #s1 #s2 #H1 #H2 * /3/ 121 110  #sz #sg #e #s1 #s2 #H1 #H2 /5/ 122  7,8: #s #H1 #H2 /2/123  //124  /5/125 111  * normalize [ //  *; normalize /3/ ] 126 112  /2/ … … 137 123 [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) 138 124  St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) 139  St_loop s ⇒ labels_of s140  St_block s ⇒ labels_of s141 125  St_label l s ⇒ l::(labels_of s) 142 126  St_cost _ s ⇒ labels_of s 
src/Cminor/toRTLabs.ma
r2178 r2232 610 610 alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,12,0)". 611 611 612 definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝613 λA,P,m,l,n.614 match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with615 [ None ⇒ λ_. Error ? m616  Some a ⇒ λH'. OK ? «a, ?»617 ] (All_nth A P n l (pi2 … l)).618 @H' @refl qed.619 620 612 lemma lookup_label_rev : ∀lenv,l,l',p. 621 613 lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'. … … 677 669 qed. 678 670 679 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) (exits:Σls:list label. All ? (present ?? (pf_graph … f)) ls)on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝671 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝ 680 672 match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with 681 673 [ St_skip ⇒ λ_. OK ? «f, ?» … … 719 711 *) 720 712  St_seq s1 s2 ⇒ λEnv. 721 do f2 ← add_stmt env label_env s2 ? f «exits, ?»;722 do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»;713 do f2 ← add_stmt env label_env s2 ? f; 714 do f1 ← add_stmt env label_env s1 ? f2; 723 715 OK ? «pi1 … f1, ?» 724 716  St_ifthenelse _ _ e s1 s2 ⇒ λEnv. 725 717 let l_next ≝ pf_entry … f in 726 do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;718 do f2 ← add_stmt env label_env s2 (π2 Env) f; 727 719 let l2 ≝ pf_entry … f2 in 728 720 let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in 729 do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;721 do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f; 730 722 let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in 731 723 let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in 732 724 OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?» 733  St_loop s ⇒ λEnv.734 let f ≝ add_fresh_to_graph … R_skip f ?? in (* dummy statement, fill in afterwards *)735 let l_loop ≝ pf_entry … f in736 do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;737 OK ? «pi1 … (fill_in_statement … l_loop (R_skip (pf_entry … f)) f ??), ?»738  St_block s ⇒ λEnv.739 do f ← add_stmt env label_env s (π2 Env) f («pf_entry … f::exits, ?»);740 OK ? «pi1 … f, ?»741  St_exit n ⇒ λEnv.742 do l ← nth_sig ?? (msg BadCminorProgram) exits n;743 OK ? «pi1 … (add_fresh_to_graph … (λ_. R_skip l) f ??), ?»744  St_switch sz sg e tab n ⇒ λEnv.745 let ❬f,r❭ ≝ choose_reg … e f ? in746 do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;747 let f ≝ add_fresh_to_graph … (λ_. R_skip l_default) f ?? in748 do f ← foldr ? (res (Σf':partial_fn ??. ?)) (λcs,f.749 do f ← f;750 let 〈i,n〉 ≝ cs in751 let ❬f,cr❭ ≝ fresh_reg … f (ASTint sz sg) in752 let ❬f,br❭ ≝ fresh_reg … f (ASTint I8 Unsigned) in753 do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;754 let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in755 let f ≝ add_fresh_to_graph … (St_op2 … (Ocmp sz sg Unsigned Ceq) br r cr) f ?? in756 let f ≝ add_fresh_to_graph … (St_const ? cr (Ointconst sz sg i)) f ?? in757 OK ? «pi1 … f, ?») (OK ? f) tab;758 OK ? «pi1 … (add_expr ? env ? e (π1 Env) f «r, ?»), ?»759 725  St_return opt_e ⇒ let f0 ≝ f in 760 726 let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in … … 776 742 ] 777 743  St_label l s' ⇒ λEnv. 778 do f ← add_stmt env label_env s' (π2 Env) f exits;744 do f ← add_stmt env label_env s' (π2 Env) f; 779 745 let l' ≝ lookup_label label_env l ? in 780 746 OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?» … … 783 749 OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?» 784 750  St_cost l s' ⇒ λEnv. 785 do f ← add_stmt env label_env s' (π2 Env) f exits;751 do f ← add_stmt env label_env s' (π2 Env) f; 786 752 OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?» 787 753 ] Env. … … 799 765  @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I 800 766  @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I 801  (*4,8:*)@(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I802  (*5,9:*)@sym_eq @(All2_length … (pi2 ?? args_regs))803  (*6,10:*)@(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I767  @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I 768  @sym_eq @(All2_length … (pi2 ?? args_regs)) 769  @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I 804 770  @(π1 (π1 (π1 Env))) 805  8,10,11,16,17: (*11,13,14,19,20:*) (@(All_mp … (pi2 ?? exits))) #i #H @(fn_con_graph … H) repeat @fn_contains_step @I806 771  #l #H cases (Exists_append … H) 807 772 [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1) … … 815 780  @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I 816 781  #l #H % [ @H  @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ] 817  @(pi2 … (pf_entry …))818  @Cminor_labels_sig @(equal_Cminor_labels_added ??? s) [ @refl  @(stmt_labels_added ????? (pi2 ?? f)) ]819  % [ @pi2  @(pi2 ?? exits) ]820  @(equal_Cminor_labels_added ??? s) [ @refl  @(stmt_labels_added ????? (pi2 ?? f)) ]821  #l' #H @(pi2 … l)822  #l #H @(fn_con_graph … (pi2 ?? l_default)) repeat @fn_contains_step @I823  @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I824  #l #H % [ @(fn_con_graph … (pi2 ?? l_case)) repeat @fn_contains_step @I  @H ]825  #l % [ % [ @(fn_con_env … (pi2 ?? r))  @(fn_con_env … (pi2 ?? cr)) ]  @(fn_con_env … (pi2 ?? br)) ] repeat @fn_contains_step @I826  #l @(fn_con_env … (pi2 ?? cr)) repeat @fn_contains_step @I827 782  #_ (* see above *) <E @(pi2 ?? r) 828 783  @(pi2 … (pf_entry …)) … … 867 822 l 868 823 l in 869 do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];824 do f ← add_stmt env label_env (f_body f) ? emptyfn; 870 825 OK ? (mk_internal_function 871 826 (pf_labgen … f) … … 881 836 (pf_exit … f) 882 837 ). 883 [ @I 884  emptyfn @(stmt_P_mp … (f_inv f)) 838 [ emptyfn @(stmt_P_mp … (f_inv f)) 885 839 #s * #V #L % 886 840 [ @(stmt_vars_mp … V) … … 925 879  whd in ⊢ (??%? → ?); #E' destruct (E') 926 880 ] 927  7,8: whd >lookup_add_hit % #E destruct881  6,7: whd >lookup_add_hit % #E destruct 928 882  % @refl 929 883 ]
Note: See TracChangeset
for help on using the changeset viewer.