 Timestamp:
 Apr 1, 2013, 7:04:56 PM (7 years ago)
 Location:
 src/Clight
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r2953 r3054 892 892 unnecessary temporary variable and assignment). 893 893 *) 894 inductive destination (vars:var_types) : Type[0] ≝895  IdDest : ∀id ,ty. local_id vars id (typ_of_type ty) → destination vars896  MemDest : (Σe:CMexpr ASTptr.expr_vars ? e (local_id vars)) → destination vars .894 inductive destination (vars:var_types) (t:typ) : Type[0] ≝ 895  IdDest : ∀id. local_id vars id t → destination vars t 896  MemDest : (Σe:CMexpr ASTptr.expr_vars ? e (local_id vars)) → destination vars t. 897 897 898 898 (* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a … … 911 911 the adres of e1 912 912 *) 913 definition translate_dest ≝913 definition translate_dest : ∀vars. ∀e:expr. res (destination vars (typ_of_type (typeof e))) ≝ 914 914 λvars,e1. 915 match e1 with915 match e1 return λe1. res (destination vars (typ_of_type (typeof e1))) with 916 916 [ Expr ed1 ty1 ⇒ 917 917 match ed1 with … … 919 919 do 〈c,t〉 as E ← lookup' vars id; 920 920 match c return λx.? → ? with 921 [ Local ⇒ λE. OK ? (IdDest vars id t ?) 922  Global r ⇒ λE. OK ? (MemDest ? (Cst ? (Oaddrsymbol id 0))) 923  Stack n ⇒ λE. OK ? (MemDest ? (Cst ? (Oaddrstack n))) 921 [ Local ⇒ λE. 922 (* Don't compare the Clight types, or we'll have to deal with 923 array/pointer punning. *) 924 match typ_eq (typ_of_type ty1) (typ_of_type t) with 925 [ inl _ ⇒ OK ? (IdDest vars (typ_of_type ty1) id ?) 926  inr _ ⇒ Error ? (msg TypeMismatch) 927 ] 928  Global r ⇒ λE. OK ? (MemDest … (Cst ? (Oaddrsymbol id 0))) 929  Stack n ⇒ λE. OK ? (MemDest … (Cst ? (Oaddrstack n))) 924 930 ] E 925 931  _ ⇒ 926 932 do e1' ← translate_addr vars e1; 927 OK ? (MemDest ?e1')933 OK ? (MemDest … e1') 928 934 ] 929 935 ]. 930 whd // >E @refl936 whd // >E // 931 937 qed. 932 938 … … 1179 1185 do dest ← translate_dest vars e1; (* e1 *) 1180 1186 match dest with 1181 [ IdDest id typ ⇒1187 [ IdDest id p ⇒ 1182 1188 (* Don't compare the Clight types, or we'll have to deal with 1183 1189 array/pointer punning. *) 1184 do e2' ← typ_should_eq (typ_of_type (typeof e2)) (typ_of_type ty) ? e2';1190 do e2' ← typ_should_eq (typ_of_type (typeof e2)) (typ_of_type (typeof e1)) ? e2'; 1185 1191 OK ? «〈uv, ul, St_assign ? id e2'〉, ?» 1186 1192  MemDest e1' ⇒ … … 1201 1207 do dest ← translate_dest vars e1; 1202 1208 match dest with 1203 [ IdDest id typ ⇒1209 [ IdDest id p ⇒ 1204 1210 (* No trace generated here, by inversion on translate_dest _ _ = IdDest _ _ _ *) 1205 OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»1211 OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type (typeof e1)〉) ef' args'〉, ?» 1206 1212  MemDest e1' ⇒ 1207 1213 let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in 
src/Clight/toCminorCorrectness.ma
r3036 r3054 1152 1152 (* We should be able to prove that ty = ty' with some more hypotheses, if needed. *) 1153 1153 lemma translate_dest_id_inversion : 1154 ∀var_types, e, var_id, ty,H.1155 translate_dest var_types e = return IdDest var_types var_id tyH →1154 ∀var_types, e, var_id, H. 1155 translate_dest var_types e = return IdDest var_types ? var_id H → 1156 1156 e = Expr (Evar var_id) (typeof e). 1157 1157 @cthulhu … … 1251 1251 ∀cl_block, cl_offset, trace. 1252 1252 ∀Hyp_present. 1253 translate_dest alloc_type cl_expr = OK ? (MemDest ?cm_expr) →1253 translate_dest alloc_type cl_expr = OK ? (MemDest … cm_expr) → 1254 1254 exec_lvalue cl_ge cl_env cl_m cl_expr = OK ? 〈〈cl_block, cl_offset〉, trace〉 → 1255 1255 ∃cm_val. eval_expr cm_ge ASTptr cm_expr cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧ … … 1273 1273 [ #r  #n  ] 1274 1274 * #cl_type * #Heq_lookup normalize nodelta 1275 [ 3: cases (type_eq_dec ??) normalize nodelta #H 1276 [ 2: whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ] 1277  *: ] 1278 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 1275 whd in ⊢ ((??%%) → ?); [3: cases (typ_eq ??) #Htyp whd in ⊢ (??%% → ?); ] #Heq destruct (Heq) 1279 1276 whd in ⊢ ((??%?) → ?); 1280 1277 @(match lookup SymbolTag block cl_env id … … 1497 1494 translate_dest vars (Expr ed ty) = 1498 1495 (do e1' ← translate_addr vars (Expr ed ty); 1499 OK ? (MemDest ?e1')).1496 OK ? (MemDest … e1')). 1500 1497 #vars * 1501 1498 [ #sz #i  #id  #e1  #e1  #op #e1 #op #e1 #e2  #cast_ty #e1 … … 1754 1751 memory_matching Em cl_ge cm_ge cl_m' cm_m cl_env 1755 1752 (update_present SymbolTag val cm_env var_id Hpresent cm_value) INV stackptr alloc_type. 1756 1757 lemma translate_dest_conservation :1758 ∀vars, e1.1759 ∀id, t, H.1760 translate_dest vars e1 = OK ? (IdDest vars id t H) →1761 typeof e1 = t.1762 #vars #e1 #id #t #H #Htranslate lapply (translate_dest_id_inversion … Htranslate)1763 #Heq >Heq in Htranslate;1764 whd in ⊢ ((??%?) → ?);1765 generalize in match (refl ??);1766 generalize in ⊢ ((???%) → (??(match % with [ _ ⇒ ?  _ ⇒ ? ] ?)?) → ?); *1767 normalize nodelta1768 [ 2: #er #_ #Habsurd destruct (Habsurd) ]1769 * * normalize nodelta1770 [ #a #b #c #Habsurd1771  #n #t #H #Habsurd1772  #ty #H ]1773 [ 1,2: destruct (Habsurd) ]1774 cases (type_eq_dec ??) normalize nodelta1775 #Hty #Heq destruct (Heq) >Hty @refl1776 qed.1777 1753 1778 1754 lemma alloc_tmp_monotonic : … … 2235 2211 #Hdest cases (bind_inversion ????? Hdest) Hdest #dest * 2236 2212 inversion dest normalize nodelta 2237 [ (* register dest *) #var_id # var_ty #His_local @(jmeq_absorb ?????) #Hdest2213 [ (* register dest *) #var_id #His_local @(jmeq_absorb ?????) #Hdest 2238 2214 #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq) 2239 2215 (* make explicit the nature of lhs, allowing to prove that no trace is emitted *) … … 2455 2431 #cl_called_f #Hfundef_fresh_for_tmp_u #Htranslate_fundef 2456 2432 whd nodelta in match (typeof ?); 2457 [ <(translate_dest_conservation … Htranslate_dest) 2458 @ClCm_cont_call_nostore normalize nodelta 2433 [ @ClCm_cont_call_nostore normalize nodelta 2459 2434 %{CL_lvalue_block} %{CL_lvalue_offset} %{(typeof lhs)} %{var_id} 2460 2435 @conj @refl … … 2797 2772  3: (* Local *) 2798 2773 #Hlookup_var_success 2799 cases (typ e_eq_dec ??) normalize nodelta #Htype_eq_dec2774 cases (typ_eq ??) normalize nodelta #Htyp_eq 2800 2775 whd in ⊢ ((???%) → ?); 2801 2776 #Heq destruct (Heq) normalize nodelta Htranslate_statement … … 2804 2779 * #cm_expr #Hexpr_vars * #Htyp_should_eq 2805 2780 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 2806 cases (typ_should_eq_inversion (typ_of_type (typeof rhs)) (typ_of_type type_of_var) … Htyp_should_eq)2781 cases (typ_should_eq_inversion (typ_of_type (typeof rhs)) (typ_of_type lhs_ty) … Htyp_should_eq) 2807 2782 Htyp_should_eq #Htyp_eq lapply Hexpr_vars_rhs lapply Hexpr_vars 2808 2783 Hlabel_wf Hreturn_ok Hlabels_translated Hstmt_inv_cm lapply sInv
Note: See TracChangeset
for help on using the changeset viewer.