Changeset 2496


Ignore:
Timestamp:
Nov 27, 2012, 5:50:51 PM (7 years ago)
Author:
garnier
Message:

Some tentative work on the simulation proof for expressions, in order to adjust the invariant
on memories.

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/abstract.ma

    r2328 r2496  
    3838(* Help avoid ambiguous input fun *)
    3939definition Clight_state ≝ state.
     40
     41definition cl_genv ≝ genv.
     42
     43definition cl_env ≝ env.
     44
     45definition cl_cont ≝ cont.
     46
     47definition cl_eval_expr ≝ eval_expr.
  • src/Clight/frontend_misc.ma

    r2468 r2496  
    8585 ∃x. e = Some ? x ∧ f x = Some ? res.
    8686 #A #B #e #res #f cases e normalize nodelta
     87[ 1: #Habsurd destruct (Habsurd)
     88| 2: #a #Heq %{a} @conj >Heq @refl ]
     89qed.
     90
     91lemma res_inversion :
     92  ∀A,B:Type[0].
     93  ∀e:option A.
     94  ∀errmsg.
     95  ∀result:B.
     96  ∀f:A → res B.
     97 match e with
     98 [ None ⇒ Error ? errmsg
     99 | Some x ⇒ f x ] = OK ? result →
     100 ∃x. e = Some ? x ∧ f x = OK ? result.
     101 #A #B #e #errmsg #result #f cases e normalize nodelta
    87102[ 1: #Habsurd destruct (Habsurd)
    88103| 2: #a #Heq %{a} @conj >Heq @refl ]
  • src/Clight/toCminor.ma

    r2469 r2496  
    621621      ] *)
    622622  | Evar id ⇒
    623       do 〈c,t〉 as E ← lookup' vars id; (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *)
    624       match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
    625       [ Global r ⇒ λ_.
     623      (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *) 
     624      do 〈c,t〉 as E ← lookup' vars id;
     625      match c return λx. (c = x) → res (Σe':CMexpr ?. ?) with
     626      [ Global r ⇒ λHeq_c.
    626627          (* We are accessing a global variable in an expression. Its Cminor counterpart also depends on
    627628             its access mode:
     
    635636          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    636637          ]
    637       | Stack n ⇒ λE.
     638      | Stack n ⇒ λHeq_c.
    638639          (* We have decided that the variable should be allocated on the stack,
    639640           * because its adress was taken somewhere or becauste it's a structured data. *)
     
    647648          ]
    648649          (* This is a local variable. Keep it as an identifier in the Cminor code, ensuring that the type of the original expr and of ty match. *)
    649       | 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, ?»)
    650       ] E
     650      | Local ⇒ λHeq_c. 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, ?»)
     651      ] (refl ? c)
    651652  | Ederef e1 ⇒
    652653      do e1' ← translate_expr vars e1;
     
    796797].
    797798whd try @I
    798 [ >E whd @refl
     799[ >E whd >Heq_c @refl
    799800| 2,3: @pi2
    800801| @(translate_binop_vars … E) @pi2
  • src/Clight/toCminorCorrectness.ma

    r2489 r2496  
    265265}.
    266266
     267include "Clight/CexecInd.ma".
     268include "Clight/frontend_misc.ma".
     269include "Clight/memoryInjections.ma".
     270
     271lemma intsize_eq_inversion :
     272  ∀sz,sz'.
     273  ∀A:Type[0].
     274  ∀ok,not_ok.
     275  intsize_eq_elim' sz sz' (λsz,sz'. res A)
     276                          (OK ? ok)
     277                          (Error ? not_ok) = (OK ? ok) →
     278  sz = sz'.
     279* * try // normalize
     280#A #ok #not_ok #Habsurd destruct
     281qed.
     282
     283definition local_matching ≝
     284  λE:embedding.
     285  λm,m':mem.
     286  λen:cl_env.
     287  λvenv:cm_env.
     288  λsp:block.
     289  λvars:var_types.
     290
     291  ∀id,cl_blo. lookup SymbolTag ? en id = Some ? cl_blo →
     292              match lookup ?? vars id with
     293              [ Some kind ⇒
     294                let 〈vtype, type〉 ≝ kind in
     295                match vtype with
     296                [ Stack n ⇒
     297                  E cl_blo = Some ? 〈sp, offset_of_Z (Z_of_nat n)〉
     298                | Local ⇒
     299                  ∀v,v'. load_value_of_type type m cl_blo zero_offset = Some ? v →
     300                         lookup ?? venv id = Some ? v' →
     301                         value_eq E v v'
     302                | _ ⇒ False ]
     303              | None ⇒ False ].
     304
     305
     306(* TODO : memory injections + link clight env+mem with local env+stack+mem *)
     307lemma eval_expr_sim :
     308  ∀(inv:clight_cminor_inv).
     309
     310  ∀(cl_env:cl_env).
     311  ∀(cl_m:mem).
     312
     313  ∀(cm_env:cm_env).
     314  ∀(sp:block).
     315  ∀(cm_m:mem).
     316  ∀(vars:var_types).
     317
     318  ∀E:embedding.
     319  ∀minj:memory_inj E cl_m cm_m.
     320  local_matching E cl_m cm_m cl_env cm_env sp vars →
     321
     322  (∀(e:expr).
     323   ∀(e':CMexpr (typ_of_type (typeof e))).
     324   (*vars = pi1 … (characterise_vars … [globals] [f]) →*)
     325   (*local_matching en m venv sp m' →  *)
     326   ∀Hexpr_vars.
     327   translate_expr vars e = OK ? («e', Hexpr_vars») →
     328   ∀val,trace,Hyp_present.
     329   exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈val, trace〉 →
     330   eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, val〉) ∧
     331
     332  (∀ed,ty.
     333   ∀(e':CMexpr (typ_of_type ty)).
     334   (*vars = pi1 … (characterise_vars … [globals] [f]) →*)
     335   (*local_matching en m venv sp m' →  *)
     336   ∀Hexpr_vars.
     337   translate_expr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
     338   ∀resblo,resoff,trace,Hyp_present.
     339   exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈resblo, resoff, trace〉 →
     340   eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, Vptr (mk_pointer resblo resoff)〉). 
     341#inv #cl_env #cl_m #cm_env #sp #cm_m #vars #E #Hinj #Hlocal_matching
     342@expr_lvalue_ind_combined
     343[ 1: (* Integer constant *)
     344  #csz #ty cases ty
     345  [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     346  | #structname #fieldspec | #unionname #fieldspec | #id ] 
     347  #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
     348  #val #trace #Hpresent #Hexec_cl
     349  whd in Htranslate:(??%?);
     350  [ 1,3,4,5,6,7,8: destruct ]
     351  (* This intsize_eq_elim' is the proof-equivalent of eating a sandwich with
     352     sand inside. *)
     353  @cthulhu
     354| 2: *
     355  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
     356  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
     357  #ty whd in ⊢ (% → ?); #Hind try @I
     358  whd in match (Plvalue ???);
     359  whd in match (typeof ?);
     360  #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
     361  whd in Hexec:(??%?);
     362  whd in match (exec_lvalue' ?????) in Hexec:(??%?);
     363  cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
     364  whd in Hcl_success:(???%);
     365  [ 1: (* var case *)
     366       lapply Hcl_success -Hcl_success
     367       (* Peform case analysis on presence of variable in local Clight env.
     368        * if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
     369       @(match lookup SymbolTag block cl_env var_id
     370         return λx.(lookup SymbolTag block cl_env var_id = x) → ?
     371         with
     372         [ None ⇒ λHcl_lookup. ?
     373         | Some loc ⇒ λHcl_lookup. ?
     374         ] (refl ? (lookup SymbolTag block cl_env var_id)))
     375       normalize nodelta
     376       [ 1: (* global case *)
     377            @cthulhu (* TODO: case analysis on lookup in global, if so use Brian's invariant *)
     378       | 2: (* local case *)
     379            #Heq destruct (Heq)
     380            lapply (bind2_eq_inversion ?????? Htranslate_expr)
     381            * #var_alloc_type * #var_type *
     382            generalize in match var_alloc_type; * normalize nodelta
     383            [ 1: (* Global case. This should be contradictory, right ?
     384                  * If lookup succeeded, then our local shadows any global with the same
     385                  * name, and [characterise_vars] should say so. TODO, this lemma. *)
     386                 @cthulhu
     387            | 2: (* Stack local *)
     388                 #stack_depth #Hlookup_vartype_success * #_
     389                 lapply (Hlocal_matching … Hcl_lookup)
     390                 whd in Hlookup_vartype_success:(??%?);
     391                 lapply (res_inversion ?????? Hlookup_vartype_success)
     392                 * * #var_alloc_type' #var_type' * #Hlookup' #Heq destruct (Heq)
     393                 >Hlookup' normalize nodelta #Hembedding_eq
     394                 (* TODO modify local_invariant to match the needs here *)
     395                 @cthulhu
     396            | 3: (* Register local *)
     397                  #Hlookup_eq * #_
     398                 (* TODO : elim type_should_eq, extract type equality, use local_matching *)
     399                 @cthulhu
     400            ]
     401       ]
     402  | 2: (* Deref case. Reduce the deref, exhibit the underlying load. *)
     403       cases (bind_inversion ????? Hcl_success) -Hcl_success
     404       * #cl_subexpr_val #cl_subexpr_trace *
     405       whd in ⊢ (? → (???%) → ?);
     406       @(match cl_subexpr_val
     407         return λx. cl_subexpr_val = x → ?
     408         with
     409         [ Vundef ⇒ λHval_eq. ?
     410         | Vint sz' i ⇒ λHval_eq. ?
     411         | Vnull ⇒ λHval_eq. ?
     412         | Vptr p ⇒ λHptr_eq. ? ] (refl ? cl_subexpr_val)) normalize nodelta
     413       [ 1,2,3: #_ #Habsurd destruct ]
     414       #Hcl_exec_to_pointer #Heq destruct (Heq)
     415       (* Now that we have executed the Clight part, reduce the Cminor one *)
     416       whd in Htranslate_expr:(??%?);
     417       cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
     418       * #cm_expr #Hexpr_vars * #Htranslate_expr
     419       whd (* ... *)   @cthulhu
     420  | 3: @cthulhu ]
     421| *: @cthulhu
     422] qed. 
     423
     424
    267425
    268426axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
  • src/Cminor/abstract.ma

    r2489 r2496  
    2727| Finalstate _ ⇒ cl_other
    2828].
     29
     30definition cm_genv ≝ genv.
     31
     32definition cm_env ≝ env.
     33
     34definition cm_cont ≝ cont.
     35
     36definition cm_eval_expr ≝ eval_expr.
     37
  • src/common/Errors.ma

    r2453 r2496  
    270270notation > "vbox('do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 48 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.
    271271
     272lemma bind2_eq_inversion:
     273  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C. ∀z.
     274  bind2_eq ??? f g = return z →
     275  ∃x. ∃y. ∃Eq. f = return 〈x, y〉 ∧ g x y Eq = return z.
     276#A #B #C #f cases f
     277[ * #a #b #g normalize #z #Heq %{a} %{b} %{(refl ??)} @conj try @refl @Heq
     278| #errmsg #g #z normalize #Habsurd destruct (Habsurd) ]
     279qed.
     280
    272281definition res_to_opt : ∀A:Type[0]. res A → option A ≝
    273282 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
Note: See TracChangeset for help on using the changeset viewer.