Changeset 3054


Ignore:
Timestamp:
Apr 1, 2013, 7:04:56 PM (4 years ago)
Author:
campbell
Message:

Put missing typ check in; adjust proof because I did it a little
differently to Ilias.

Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2953 r3054  
    892892   unnecessary temporary variable and assignment).
    893893   *)
    894 inductive destination (vars:var_types) : Type[0] ≝
    895 | IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars
    896 | MemDest : (Σe:CMexpr ASTptr.expr_vars ? e (local_id vars)) → destination vars.
     894inductive 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.
    897897
    898898(* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a
     
    911911    the adres of e1
    912912*)
    913 definition translate_dest
     913definition translate_dest : ∀vars. ∀e:expr. res (destination vars (typ_of_type (typeof e)))
    914914λvars,e1.
    915   match e1 with
     915  match e1 return λe1. res (destination vars (typ_of_type (typeof e1))) with
    916916  [ Expr ed1 ty1 ⇒
    917917      match ed1 with
     
    919919          do 〈c,t〉 as E ← lookup' vars id;
    920920          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)))
    924930          ] E
    925931      | _ ⇒
    926932          do e1' ← translate_addr vars e1;
    927           OK ? (MemDest ? e1')
     933          OK ? (MemDest e1')
    928934      ]
    929935  ].
    930 whd // >E @refl
     936whd // >E //
    931937qed.
    932938
     
    11791185    do dest ← translate_dest vars e1; (* e1 *)
    11801186    match dest with
    1181     [ IdDest id ty p ⇒
     1187    [ IdDest id p ⇒
    11821188       (* Don't compare the Clight types, or we'll have to deal with
    11831189          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';
    11851191       OK ? «〈uv, ul, St_assign ? id e2'〉, ?»
    11861192    | MemDest e1' ⇒
     
    12011207        do dest ← translate_dest vars e1;
    12021208        match dest with
    1203         [ IdDest id ty p ⇒
     1209        [ IdDest id p ⇒
    12041210            (* 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'〉, ?»
    12061212        | MemDest e1' ⇒
    12071213            let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in
  • src/Clight/toCminorCorrectness.ma

    r3036 r3054  
    11521152(* We should be able to prove that ty = ty' with some more hypotheses, if needed. *)
    11531153lemma translate_dest_id_inversion :
    1154   ∀var_types, e, var_id, ty,H.
    1155    translate_dest var_types e = return IdDest var_types var_id ty H →
     1154  ∀var_types, e, var_id, H.
     1155   translate_dest var_types e = return IdDest var_types ? var_id H →
    11561156   e = Expr (Evar var_id) (typeof e).
    11571157@cthulhu
     
    12511251  ∀cl_block, cl_offset, trace.
    12521252  ∀Hyp_present. 
    1253      translate_dest alloc_type cl_expr = OK ? (MemDest ? cm_expr) →
     1253     translate_dest alloc_type cl_expr = OK ? (MemDest cm_expr) →
    12541254     exec_lvalue cl_ge cl_env cl_m cl_expr = OK ? 〈〈cl_block, cl_offset〉, trace〉 →
    12551255     ∃cm_val. eval_expr cm_ge ASTptr cm_expr cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
     
    12731273[ #r | #n | ]
    12741274* #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)
     1275whd in ⊢ ((??%%) → ?); [3: cases (typ_eq ??) #Htyp whd in ⊢ (??%% → ?); ] #Heq destruct (Heq)
    12791276whd in ⊢ ((??%?) → ?);
    12801277@(match lookup SymbolTag block cl_env id
     
    14971494    translate_dest vars (Expr ed ty) =
    14981495    (do e1' ← translate_addr vars (Expr ed ty);
    1499      OK ? (MemDest ? e1')).
     1496     OK ? (MemDest e1')).
    15001497#vars *
    15011498[ #sz #i | #id | #e1 | #e1 | #op #e1 |#op #e1 #e2 | #cast_ty #e1
     
    17541751   memory_matching Em cl_ge cm_ge cl_m' cm_m cl_env
    17551752    (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 nodelta
    1768 [ 2: #er #_ #Habsurd destruct (Habsurd) ]
    1769 * * normalize nodelta
    1770 [ #a #b #c #Habsurd
    1771 | #n #t #H #Habsurd
    1772 | #ty #H ]
    1773 [ 1,2: destruct (Habsurd) ]
    1774 cases (type_eq_dec ??) normalize nodelta
    1775 #Hty #Heq destruct (Heq) >Hty @refl
    1776 qed.
    17771753
    17781754lemma alloc_tmp_monotonic :
     
    22352211       #Hdest cases (bind_inversion ????? Hdest) -Hdest #dest *
    22362212       inversion dest normalize nodelta
    2237        [ (* register dest *) #var_id #var_ty #His_local @(jmeq_absorb ?????) #Hdest
     2213       [ (* register dest *) #var_id #His_local @(jmeq_absorb ?????) #Hdest
    22382214         #Htranslate_dest whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    22392215         (* make explicit the nature of lhs, allowing to prove that no trace is emitted *)
     
    24552431             #cl_called_f #Hfundef_fresh_for_tmp_u #Htranslate_fundef
    24562432             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
    24592434               %{CL_lvalue_block} %{CL_lvalue_offset} %{(typeof lhs)} %{var_id}
    24602435               @conj @refl
     
    27972772          | 3: (* Local *)
    27982773               #Hlookup_var_success
    2799                cases (type_eq_dec ??) normalize nodelta #Htype_eq_dec
     2774               cases (typ_eq ??) normalize nodelta #Htyp_eq
    28002775               whd in ⊢ ((???%) → ?);
    28012776               #Heq destruct (Heq) normalize nodelta -Htranslate_statement
     
    28042779               * #cm_expr #Hexpr_vars * #Htyp_should_eq
    28052780               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)
    28072782               -Htyp_should_eq #Htyp_eq lapply Hexpr_vars_rhs lapply Hexpr_vars
    28082783               -Hlabel_wf -Hreturn_ok -Hlabels_translated -Hstmt_inv_cm lapply sInv               
Note: See TracChangeset for help on using the changeset viewer.