Changeset 2568


Ignore:
Timestamp:
Jan 4, 2013, 2:59:36 PM (7 years ago)
Author:
campbell
Message:

Relax some Clight type checks to Cminor type checks to avoid array/pointer
confusion. Drop a dead function.

Location:
src/Clight
Files:
6 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2565 r2568  
    718718      do e1' ← translate_expr vars e1;
    719719      do e2' ← translate_expr vars e2;
    720       do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
     720      do e2' ← typ_should_eq (typ_of_type (typeof e2)) (typ_of_type ty) ? e2';
    721721      do e3' ← translate_expr vars e3;
    722       do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3';
     722      do e3' ← typ_should_eq (typ_of_type (typeof e3)) (typ_of_type ty) ? e3';
    723723      match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → res ? with
    724724      [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?»
     
    996996definition stmt_inv ≝  λvars. stmt_P (stmt_vars (local_id vars)).
    997997
    998 (* I (Ilias) decided to inline the following definition, to make explicit the data constructed.
    999  * This was needed to prove some stuff in translate_statement at some point, but it might be
    1000  * useless now. If needed, I can revert this change.  *)
    1001 definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt. stmt_inv vars s) ≝
    1002 λvars,e1,e2.
    1003 do e2' ← translate_expr vars e2;
    1004 do dest ← translate_dest vars e1;
    1005 match dest with
    1006 [ IdDest id ty p ⇒
    1007     do e2' ← type_should_eq (typeof e2) ty ? e2';
    1008     OK ? «St_assign ? id e2', ?»
    1009 | MemDest e1' ⇒ OK ? «St_store ? e1' e2', ?»
    1010 ].
    1011 % try (//) elim e2' /2/ elim e1' /2/
    1012 qed.
    1013 
    1014998definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
    1015999λA,B,f,oa.
     
    11771161    match dest with
    11781162    [ IdDest id ty p ⇒
    1179        do e2' ← type_should_eq (typeof e2) ty ? e2';
     1163       (* Don't compare the Clight types, or we'll have to deal with
     1164          array/pointer punning. *)
     1165       do e2' ← typ_should_eq (typ_of_type (typeof e2)) (typ_of_type ty) ? e2';
    11801166       OK ? «〈uv, ul, St_assign ? id e2'〉, ?»
    11811167    | MemDest e1' ⇒
  • src/Clight/toCminorCorrectness.ma

    r2565 r2568  
    17661766  cases (bind_inversion ????? Htranslate) -Htranslate
    17671767  * #cm_expr_e2_welltyped #Hexpr2_vars_wt * #Htypecheck
    1768   lapply (type_should_eq_inversion (typeof e2) ty … Htypecheck) -Htypecheck
     1768  lapply (typ_should_eq_inversion (typ_of_type (typeof e2)) (typ_of_type ty) … Htypecheck) -Htypecheck
    17691769  *  #Htypeof_e2_eq_ty
    17701770  lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
     
    17771777  cases (bind_inversion ????? Htranslate) -Htranslate 
    17781778  * #cm_expr_e3_welltyped #Hexpr3_vars_wt * #Htypecheck
    1779   lapply (type_should_eq_inversion (typeof e3) ty … Htypecheck) -Htypecheck
     1779  lapply (typ_should_eq_inversion (typ_of_type (typeof e3)) (typ_of_type ty) … Htypecheck) -Htypecheck
    17801780  * #Htypeof_e3_eq_ty
    17811781  lapply (Hind3 cm_expr_e3 Hexpr_vars_e3 Htranslate_e3) -Hind3
Note: See TracChangeset for help on using the changeset viewer.