Changeset 1626 for src/Clight/toCminor.ma
 Timestamp:
 Dec 19, 2011, 2:48:33 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r1612 r1626 82 82 . 83 83 84 definition var_types ≝ identifier_map SymbolTag var_type.84 definition var_types ≝ identifier_map SymbolTag (var_type × type). 85 85 86 86 axiom UndeclaredIdentifier : String. … … 89 89 λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id). 90 90 91 definition local_id : var_types → ident → Prop ≝ 92 λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False  _ ⇒ True ]  _ ⇒ False ]. 91 (* Assert that an identifier is a local variable with the given typ. *) 92 definition local_id : var_types → ident → typ → Prop ≝ 93 λvars,id,t. match lookup' vars id with [ OK vt ⇒ match (\fst vt) with [ Global _ ⇒ False  _ ⇒ t = typ_of_type (\snd vt) ]  _ ⇒ False ]. 93 94 94 95 (* Note that the semantics allows locals to shadow globals. … … 105 106 ]. 106 107 107 definition characterise_vars : list (ident×region ) → function → var_types × nat ≝108 definition characterise_vars : list (ident×region×type) → function → var_types × nat ≝ 108 109 λglobals, f. 109 let m ≝ foldr ?? (λidr ,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in110 let m ≝ foldr ?? (λidrt,m. add ?? m (\fst (\fst idrt)) 〈Global (\snd (\fst idrt)), \snd idrt〉) (empty_map ??) globals in 110 111 let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in 111 112 let 〈m,stacksize〉 ≝ foldr ?? (λv,ms. … … 115 116 then 〈Stack stack_high,stack_high + sizeof ty〉 116 117 else 〈Local, stack_high〉 in 117 〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in118 〈add ?? m id 〈c, ty〉, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in 118 119 〈m,stacksize〉. 119 120 120 lemma local_id_add_global : ∀vars,id,r, id'.121 local_id (add ?? vars id (Global r)) id' → local_id vars id'.122 #var #id #r # id'121 lemma local_id_add_global : ∀vars,id,r,t,id',t'. 122 local_id (add ?? vars id 〈Global r, t〉) id' t' → local_id vars id' t'. 123 #var #id #r #t #id' #t' 123 124 whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?] → ?); 124 125 cases (identifier_eq ? id id') … … 127 128 ] qed. 128 129 129 lemma local_id_add_miss : ∀vars,id, t,id'.130 id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.131 #vars #id # t #id' #NE130 lemma local_id_add_miss : ∀vars,id,vt,id',t'. 131 id ≠ id' → local_id (add ?? vars id vt) id' t' → local_id vars id' t'. 132 #vars #id #vt #id' #t' #NE 132 133 whd in ⊢ (% → %); 133 134 whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ] → match % with [ _ ⇒ ?  _ ⇒ ? ]); … … 138 139 lemma characterise_vars_all : ∀l,f,vars,n. 139 140 characterise_vars l f = 〈vars,n〉 → 140 ∀i . local_id vars i→141 Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).141 ∀i,t. local_id vars i t → 142 Exists ? (λx.\fst x = i ∧ typ_of_type (\snd x) = t) (fn_params f @ fn_vars f). 142 143 #globals #f 143 144 whd in ⊢ (∀_.∀_.??%? → ?); 144 145 elim (fn_params f @ fn_vars f) 145 [ #vars #n whd in ⊢ (??%? → ?); #E destruct #i # H @False_ind146 [ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #t #H @False_ind 146 147 elim globals in H; 147 148 [ normalize // 148  * #id #rg #t #IH whd in ⊢ (?%? → ?); #H @IH @(local_id_add_global ????H)149  * * #id #rg #t #tl #IH whd in ⊢ (?%?? → ?); #H @IH @(local_id_add_global … H) 149 150 ] 150  * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i 151  * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i #t 152 153 #H >(contract_pair var_types nat ?) in E; 154 whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); 155 cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); 156 #H' lapply (extract_pair ???????? H') H' * #m0 * #n0 * #EQ #EQ2 157 151 158 cases (identifier_eq ? id i) 152 [ #E' <E' #H % @refl 153  #NE #H whd %2 >(contract_pair var_types nat ?) in E; 154 whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); 155 cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); 156 #H' lapply (extract_pair ???????? H') H' * #m0 * #n0 * #EQ #EQ2 157 @(IH m0 n0) 159 [ 1,3: #E' >E' in EQ2:%; #EQ2 % % 160 [ 1,3: @refl 161  *: destruct (EQ2) change with (add ?????) in H:(?%??); 162 whd in H; whd in H:(match % with [_ ⇒ ?_ ⇒ ?]); >lookup_add_hit in H; 163 whd in ⊢ (% → ?); #E'' >E'' @refl 164 ] 165  *: #NE %2 @(IH m0 n0) 158 166 [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ 159 167  2,4: destruct (EQ2) @(local_id_add_miss … H) @NE … … 446 454  Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?» 447 455  Evar id ⇒ 448 do cas E ← lookup' vars id;456 do 〈c,t〉 as E ← lookup' vars id; 449 457 match c return λx.? = ? → res (Σe':CMexpr ?. ?) with 450 458 [ Global r ⇒ λ_. … … 460 468  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 461 469 ] 462  Local ⇒ λE. OK ? «Id ? id, ?»470  Local ⇒ λE. type_should_eq t ty (λt.Σe':CMexpr (typ_of_type t).expr_vars (typ_of_type t) e' (local_id vars)) («Id (typ_of_type t) id, ?») 463 471 ] E 464 472  Ederef e1 ⇒ … … 572 580 match ed with 573 581 [ Evar id ⇒ 574 do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);582 do 〈c,t〉 ← lookup' vars id; 575 583 match c return λ_. res (𝚺r.Σz:CMexpr (ASTptr r).?) with 576 584 [ Global r ⇒ OK ? ❬r, «Cst ? (Oaddrsymbol id 0), ?»❭ … … 599 607 ]. 600 608 whd try @I 601 [ >E @I609 [ >E whd @refl 602 610  >(E ? (refl ??)) @refl 603 611  3,4: @pi2 … … 615 623 616 624 inductive destination (vars:var_types) : Type[0] ≝ 617  IdDest : ∀id :ident. local_id vars id→ destination vars625  IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars 618 626  MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars. 619 627 … … 629 637 match ed1 with 630 638 [ Evar id ⇒ 631 do cas E ← lookup' vars id;639 do 〈c,t〉 as E ← lookup' vars id; 632 640 match c return λx.? → ? with 633 [ Local ⇒ λE. OK ? (IdDest vars id ?)641 [ Local ⇒ λE. OK ? (IdDest vars id t ?) 634 642  Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0))) 635 643  Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n))) … … 640 648 ] 641 649 ]. 642 whd // >E @ I650 whd // >E @refl 643 651 qed. 644 652 … … 686 694 do dest ← translate_dest vars e1 (typeof e2); 687 695 match dest with 688 [ IdDest id p ⇒ OK ? «St_assign ? id e2', ?» 696 [ IdDest id ty p ⇒ 697 do e2' ← type_should_eq (typeof e2) ty ? e2'; 698 OK ? «St_assign ? id e2', ?» 689 699  MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?» 690 700 ]. … … 712 722 record tmpgen : Type[0] ≝ { 713 723 tmp_universe : universe SymbolTag; 714 tmp_env : list (ident × typ )724 tmp_env : list (ident × type) 715 725 }. 716 726 717 definition alloc_tmp : memory_chunk→ tmpgen → ident × tmpgen ≝718 λ c,g.727 definition alloc_tmp : type → tmpgen → ident × tmpgen ≝ 728 λty,g. 719 729 let 〈tmp,u〉 ≝ fresh ? (tmp_universe g) in 720 〈tmp, mk_tmpgen u (〈tmp, ty p_of_memory_chunk c〉::(tmp_env g))〉.730 〈tmp, mk_tmpgen u (〈tmp, ty〉::(tmp_env g))〉. 721 731 722 732 lemma lookup_label_hit : ∀lbls,l,l'. … … 728 738 definition add_tmps : var_types → tmpgen → var_types ≝ 729 739 λvs,g. 730 foldr ?? (λidty,vs. add ?? vs (\fst idty) Local) vs (tmp_env g).740 foldr ?? (λidty,vs. add ?? vs (\fst idty) 〈Local, \snd idty〉) vs (tmp_env g). 731 741 732 742 definition tmps_preserved : var_types → tmpgen → tmpgen → Prop ≝ 733 743 λvars,u1,u2. 734 ∀id . local_id (add_tmps vars u1) id → local_id (add_tmps vars u2) id.744 ∀id,ty. local_id (add_tmps vars u1) id ty → local_id (add_tmps vars u2) id ty. 735 745 736 746 lemma alloc_tmp_preserves : ∀tmp,u,u',vars,q. 737 747 〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'. 748 cases daemon (* XXX freshness 738 749 #tmp #g #g' #vars #q 739 750 whd in ⊢ (???% → ?); #E … … 744 755 [ >E >lookup_add_hit @I 745 756  cases E #NE >lookup_add_miss [ @H  /2/ 746 ] qed.757 ] *) qed. 747 758 748 759 definition trans_inv : var_types → lenv → statement → tmpgen → (stmt×tmpgen) → Prop ≝ … … 763 774 qed. 764 775 765 lemma local_id_add_local_oblivious : ∀vars,id,id'. 766 local_id vars id → local_id (add ?? vars id' Local) id. 767 #vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 776 (* XXX Not true without fresh id' XXX 777 lemma local_id_add_local_oblivious : ∀vars,id,ty,id',ty'. 778 local_id vars id ty → local_id (add ?? vars id' 〈Local, ty'〉) id ty. 779 #vars #id #ty #id' #ty' #H whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]) 768 780 cases (identifier_eq ? id id') 769 781 [ #E >E >lookup_add_hit @I 770 782  #NE >lookup_add_miss [ @H  /2/ 771 783 ] qed. 772 773 lemma local_id_add_tmps_oblivious : ∀vars,id,u. 774 local_id vars id → local_id (add_tmps vars u) id. 784 *) 785 786 (* XXX freshness XXX *) 787 axiom local_id_add_tmps_oblivious : ∀vars,id,ty,u. 788 local_id vars id ty → local_id (add_tmps vars u) id ty. 789 (* 775 790 #vars #id * #u #l #H elim l 776 791 [ // 777 792  * #id' #ty #tl @local_id_add_local_oblivious 778 793 ] qed. 794 *) 779 795 780 796 lemma add_tmps_oblivious : ∀vars,lbls,s,u. … … 784 800 #s' * #H1 #H2 % 785 801 [ @(stmt_vars_mp … H1) 786 #id @local_id_add_tmps_oblivious802 #id #t @local_id_add_tmps_oblivious 787 803  @H2 788 804 ] qed. 789 805 790 lemma local_id_fresh_tmp : ∀tmp,u, q,u0,vars.791 〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.792 #tmp #u # q#u0 #vars806 lemma local_id_fresh_tmp : ∀tmp,u,ty,u0,vars. 807 〈tmp,u〉 = alloc_tmp ty u0 → local_id (add_tmps vars u) tmp (typ_of_type ty). 808 #tmp #u #ty #u0 #vars 793 809 whd in ⊢ (???% → ?); #E 794 810 destruct 795 whd in ⊢ (?%? ); whd whd in ⊢ match % with [ _ ⇒ ?  _ ⇒ ? ]; >lookup_add_hit796 @ I811 whd in ⊢ (?%??); whd whd in ⊢ match % with [ _ ⇒ ?  _ ⇒ ? ]; >lookup_add_hit 812 @refl 797 813 qed. 798 814 … … 812 828 do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *) 813 829 match dest with 814 [ IdDest id p ⇒ OK ? «〈St_call (Some ? id) ef' args', u〉, ?»830 [ IdDest id ty p ⇒ OK ? «〈St_call (Some ? 〈id,typ_of_type ty〉) ef' args', u〉, ?» 815 831  MemDest r q e1' ⇒ 816 let 〈tmp, u〉 as Etmp ≝ alloc_tmp qu in817 OK ? «〈St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), u〉, ?»832 let 〈tmp, u〉 as Etmp ≝ alloc_tmp (typeof e1) u in 833 OK ? «〈St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r q e1' (Id ? tmp)), u〉, ?» 818 834 ] 819 835 ] … … 891 907 try @I 892 908 try (#l #H @(match H in False with [ ])) 893 try (#id # H @H)909 try (#id #ty #H @H) 894 910 [ @add_tmps_oblivious @(pi2 ?? s') 895 911  @local_id_add_tmps_oblivious @p 896 912 ] 897 try (@sub_pi2 #x @expr_vars_mp #i @local_id_add_tmps_oblivious)898 [ 1,3,6: @sub_pi2 #x @All_mp * #ty #e @expr_vars_mp #i @local_id_add_tmps_oblivious913 try (@sub_pi2 #x @expr_vars_mp #i #ty @local_id_add_tmps_oblivious) 914 [ 1,3,6: @sub_pi2 #x @All_mp * #ty #e @expr_vars_mp #i #ty' @local_id_add_tmps_oblivious 899 915  2,4: @(local_id_fresh_tmp … Etmp) 900 916  @(alloc_tmp_preserves … Etmp) … … 907 923 %{l'} % [ 1,3: @E2  *: @Exists_append_r @D2 ] 908 924 ] 909  10,14: cases H2 #_ #TP2 #id # L @TP2 cases H1 #_ #TP1 @TP1 @L925  10,14: cases H2 #_ #TP2 #id #ty #L @TP2 cases H1 #_ #TP1 @TP1 @L 910 926  15,18: @(π1 (π1 H1)) 911 927  16,19: cases H1 * #_ #L1 #_ #l #H cases (L1 l H) #l' * #E1 #D1 … … 913 929  17,20: @(π2 H1) 914 930 (* Sfor *) 915  @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id # H @(π2 H3) @(π2 H2) @H  @H5 ]931  @(stmt_P_mp … (π1 (π1 H1))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #ty #H @(π2 H3) @(π2 H2) @H  @H5 ] 916 932  @(π1 (π1 H3)) 917  @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id # H @(π2 H3) @H  @H5 ]933  @(stmt_P_mp … (π1 (π1 H2))) #s * #H4 #H5 % [ @(stmt_vars_mp … H4) #id #ty #H @(π2 H3) @H  @H5 ] 918 934  #l #H cases (Exists_append … H) 919 935 [ #EX1 cases H1 * #S1 #L1 #_ cases (L1 l EX1) #l' * #E1 #D1 … … 926 942 ] 927 943 ] 928  #id # H @(π2 H3) @(π2 H2) @(π2 H1) @H944  #id #ty #H @(π2 H3) @(π2 H2) @(π2 H1) @H 929 945 (* Slabel *) 930 946  %{l} @E … … 948 964 let 〈id,ty〉 ≝ it in 949 965 do «s,u, Is» ← su; 950 do tas E ← lookup' vars id;966 do 〈t,ty'〉 as E ← lookup' vars id; 951 967 match t return λx.? → ? with 952 968 [ Local ⇒ λE. OK (Σs:stmt×tmpgen.?) «〈s,u〉,Is» … … 957 973  By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 958 974 ]; 959 OK ? «〈St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty ) id)) s, u〉, ?»975 OK ? «〈St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s, u〉, ?» 960 976  Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id] 961 977 ] E) (OK ? s) params. 962 978 try @conj try @conj try @conj try @conj try @conj try @conj 963 979 try @I 964 [ @(expr_vars_mp … (λid . local_id_add_tmps_oblivious vars id u)) whd >E @I980 [ @(expr_vars_mp … (λid,ty. local_id_add_tmps_oblivious vars id ty u)) whd >E @refl 965 981  @(π1 (π1 Is)) 966 982  @(π2 (π1 Is)) … … 1030 1046 qed. 1031 1047 1032 lemma local_id_split : ∀vars,tmpgen,i .1033 local_id (add_tmps vars tmpgen) i →1034 local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen).1035 #vars #tmpgen #i 1036 whd in ⊢ (?%? → ?);1048 lemma local_id_split : ∀vars,tmpgen,i,t. 1049 local_id (add_tmps vars tmpgen) i t → 1050 local_id vars i t ∨ Exists ? (λx. \fst x = i ∧ typ_of_type (\snd x) = t) (tmp_env tmpgen). 1051 #vars #tmpgen #i #t 1052 whd in ⊢ (?%?? → ?); 1037 1053 elim (tmp_env tmpgen) 1038 1054 [ #H %1 @H 1039 1055  * #id #ty #tl #IH 1040 1056 cases (identifier_eq ? i id) 1041 [ #E >E #H %2 whd %1 @refl1057 [ #E >E #H %2 whd %1 % [ @refl  whd in H; whd in H:(match % with [_⇒?_⇒?]); >lookup_add_hit in H; #E1 >E1 @refl ] 1042 1058  #NE #H cases (IH ?) 1043 1059 [ #H' %1 @H' … … 1057 1073 ] qed. 1058 1074 1059 definition translate_function : universe SymbolTag → list (ident×region ) → function → res internal_function ≝1075 definition translate_function : universe SymbolTag → list (ident×region×type) → function → res internal_function ≝ 1060 1076 λtmpuniverse, globals, f. 1061 1077 do «lbls, Ilbls» ← build_label_env (fn_body f); … … 1067 1083 (opttyp_of_type (fn_return f)) 1068 1084 (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f)) 1069 (( tmp_env tmp)@(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))1085 ((map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env tmp @ fn_vars f))) 1070 1086 stacksize 1071 1087 s ?). … … 1074 1090 #s1 * #H1 #H2 % 1075 1091 [ @(stmt_vars_mp … H1) 1076 #i # H1092 #i #t #H 1077 1093 cases (local_id_split … H) 1078 [ #H' @Exists_squeeze>map_append1079 @Exists_map [ 2: @ (characterise_vars_all … (sym_eq ??? E) i) @H'1094 [ #H' >map_append 1095 @Exists_map [ 2: @Exists_squeeze @(characterise_vars_all … (sym_eq ??? E) i t) @H' 1080 1096  skip 1081  * #id #ty #E1 <E1@refl1097  * #id #ty * #E1 #E2 <E1 <E2 @refl 1082 1098 ] 1083  #EX @Exists_append_r @Exists_append_l @EX1099  #EX @Exists_append_r <map_append @Exists_append_l @Exists_map [2: @EX  skip  * #id #ty * #E1 #E2 <E1 <E2 % @refl ] 1084 1100 ] 1085 1101  @(stmt_labels_mp … H2) … … 1090 1106 ] qed. 1091 1107 1092 definition translate_fundef : universe SymbolTag → list (ident×region ) → clight_fundef → res (fundef internal_function) ≝1108 definition translate_fundef : universe SymbolTag → list (ident×region×type) → clight_fundef → res (fundef internal_function) ≝ 1093 1109 λtmpuniverse,globals,f. 1094 1110 match f with … … 1105 1121 λp. 1106 1122 let tmpuniverse ≝ universe_for_program p in 1107 let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names?? p) in1108 let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fstv)〉) (prog_vars ?? p) in1123 let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in 1124 let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in 1109 1125 let globals ≝ fun_globals @ var_globals in 1110 1126 transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)).
Note: See TracChangeset
for help on using the changeset viewer.