Changeset 2500


Ignore:
Timestamp:
Nov 28, 2012, 5:57:38 PM (7 years ago)
Author:
garnier
Message:

Continuing work on simulation in Clight/Cminor?

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2496 r2500  
    130130#A #x #y * normalize
    131131#H destruct @conj @refl
     132qed.
     133
     134lemma opt_to_res_inversion :
     135  ∀A:Type[0]. ∀errmsg. ∀opt. ∀val. opt_to_res A errmsg opt = OK ? val →
     136  opt = Some ? val.
     137#A #errmsg *
     138[ 1: #val normalize #Habsurd destruct
     139| 2: #res #val normalize #Heq destruct @refl ]
    132140qed.
    133141
  • src/Clight/memoryInjections.ma

    r2483 r2500  
    265265  λo1,o2. mk_offset (addition_n ? (offv o1) (offv o2)).
    266266
    267 lemma offset_plus_0 : ∀o. offset_plus o (mk_offset (zero ?)) = o.
     267lemma offset_plus_0 : ∀o. offset_plus (mk_offset (zero ?)) o = o.
    268268* #o
    269269whd in match (offset_plus ??);
     270>commutative_addition_n
    270271>addition_n_0 @refl
    271272qed.
  • src/Clight/toCminorCorrectness.ma

    r2496 r2500  
    297297                  E cl_blo = Some ? 〈sp, offset_of_Z (Z_of_nat n)〉
    298298                | 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'
     299                  ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
     300                      ∃v'. lookup ?? venv id = Some ? v' ∧
     301                           value_eq E v v'
    302302                | _ ⇒ False ]
    303303              | None ⇒ False ].
     304             
     305lemma type_should_eq_inversion :
     306  ∀ty1,ty2,P,f,res.
     307    type_should_eq ty1 ty2 P f = OK ? res →
     308    ty1 = ty2 ∧ f ≃ res.
     309#ty1 #ty2 #P #f #res normalize
     310cases (type_eq_dec ty1 ty2) normalize nodelta
     311[ 2: #Hneq #Habsurd destruct ]
     312#Heq #Heq2 @conj try assumption
     313destruct (Heq2) cases Heq normalize nodelta
     314@eq_to_jmeq @refl
     315qed.
     316
     317lemma load_value_of_type_by_ref :
     318  ∀ty,m,b,off,val.
     319    load_value_of_type ty m b off = Some ? val →
     320    typ_of_type ty ≃ ASTptr →
     321    access_mode ty ≃ By_reference →
     322    val = Vptr (mk_pointer b off).
     323*
     324[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     325| #structname #fieldspec | #unionname #fieldspec | #id ]
     326#m #b #off #val
     327[ 1,6,7: normalize #Habsurd destruct (Habsurd)
     328| 4,5: normalize #Heq #_ #_ destruct @refl
     329| 2: #_ normalize #Heq destruct
     330| *: #Hload normalize #_ #H
     331      lapply (jmeq_to_eq ??? H) #Heq destruct
     332] qed.       
     333
    304334
    305335
     
    320350  local_matching E cl_m cm_m cl_env cm_env sp vars →
    321351
     352   (*vars = pi1 … (characterise_vars … [globals] [f]) →*)
     353   (*local_matching en m venv sp m' →  *)
     354
    322355  (∀(e:expr).
    323356   ∀(e':CMexpr (typ_of_type (typeof e))).
    324    (*vars = pi1 … (characterise_vars … [globals] [f]) →*)
    325    (*local_matching en m venv sp m' →  *)
    326357   ∀Hexpr_vars.
    327358   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〉) ∧
     359   ∀cl_val,trace,Hyp_present.
     360   exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
     361   ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
     362            value_eq E cl_val cm_val) ∧
    331363
    332364  (∀ed,ty.
    333365   ∀(e':CMexpr (typ_of_type ty)).
    334    (*vars = pi1 … (characterise_vars … [globals] [f]) →*)
    335    (*local_matching en m venv sp m' →  *)
    336366   ∀Hexpr_vars.
    337367   translate_expr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
    338368   ∀resblo,resoff,trace,Hyp_present.
    339369   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)〉). 
     370   (* TODO: shift 〈resblo, resoff〉 through E *)
     371   eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, Vptr (mk_pointer resblo resoff)〉).
    341372#inv #cl_env #cl_m #cm_env #sp #cm_m #vars #E #Hinj #Hlocal_matching
    342373@expr_lvalue_ind_combined
     
    355386  [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
    356387  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
    357   #ty whd in ⊢ (% → ?); #Hind try @I
     388  try /2 by I/
     389  #ty whd in ⊢ (% → ?); #Hind
    358390  whd in match (Plvalue ???);
    359391  whd in match (typeof ?);
     
    364396  whd in Hcl_success:(???%);
    365397  [ 1: (* var case *)
     398
    366399       lapply Hcl_success -Hcl_success
    367400       (* Peform case analysis on presence of variable in local Clight env.
     
    378411       | 2: (* local case *)
    379412            #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
     413            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
     414            * #var_id_alloc_type * #var_id_type *
     415            generalize in match var_id_alloc_type; * normalize nodelta
    383416            [ 1: (* Global case. This should be contradictory, right ?
    384417                  * If lookup succeeded, then our local shadows any global with the same
     
    386419                 @cthulhu
    387420            | 2: (* Stack local *)
    388                  #stack_depth #Hlookup_vartype_success * #_
    389                  lapply (Hlocal_matching … Hcl_lookup)
     421                 lapply Hcl_load_success -Hcl_load_success
     422                 lapply Hyp_present -Hyp_present
     423                 lapply Hexpr_vars -Hexpr_vars
     424                 lapply cm_expr -cm_expr inversion (access_mode ty)
     425                 [ #typ_of_ty | | #typ_of_ty ]
     426                 #Heq_typ_of_type #Heq_access_mode
     427                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success
     428                 #stack_depth #Hlookup_vartype_success normalize nodelta
     429                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     430                 lapply (Hlocal_matching … Hcl_lookup)
    390431                 whd in Hlookup_vartype_success:(??%?);
    391                  lapply (res_inversion ?????? Hlookup_vartype_success)
    392                  * * #var_alloc_type' #var_type' * #Hlookup' #Heq destruct (Heq)
     432                 cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
     433                 * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
    393434                 >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
     435                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
     436                 #loaded_val * #Hload_val
     437                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     438                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
     439                 #Hload_success
     440                 whd in match (eval_expr ???????);
     441                 cut (pointer_translation (mk_pointer cl_b zero_offset) E =
     442                      Some ? (mk_pointer sp (offset_of_Z stack_depth)))
     443                 [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
     444                        >offset_plus_0 @refl ]
     445                 #Hpointer_translation       
     446                 [ 2: (* By-ref *)
     447                      whd in Hload_success:(??%?);
     448                      lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode)
     449                      #Heq_val
     450                      >Heq_val
     451                      %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
     452                      @conj try @refl
     453                      %4 (* boring and trivial *)
     454                      @cthulhu                     
     455                 | 1: (* By value *)
     456                      lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
     457                      [ @(load_by_value_success_valid_pointer … Hload_success)
     458                        lapply (jmeq_to_eq ??? Heq_typ_of_type)
     459                        #Heq_typ_of_type'
     460                        (* boring and trivial *)
     461                        @cthulhu ]
     462                      * #cm_val * #Hload_in_cm #Hvalue_eq
     463                      %{cm_val} @conj try assumption
     464                      (* unpack Hload_in_cm using Heq_access_mode as an hypothesis. profit *)
     465                      @cthulhu ]
     466            | 3: (* Register local variable *)
     467                 #Hlookup_eq
     468                 lapply (res_inversion ?????? Hlookup_eq)
     469                 * * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
     470                 #Htype_eq
     471                 cases (type_should_eq_inversion
     472                            var_id_type
     473                            ty
     474                            (λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars))
     475                            … Htype_eq) -Htype_eq
     476                 (* Reverting all premises in order to perform type rewrite *)
     477                 #Htype_eq
     478                 lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq
     479                 lapply Hcl_load_success -Hcl_load_success
     480                 lapply Hcl_lookup -Hcl_lookup
     481                 lapply Hyp_present -Hyp_present
     482                 lapply Hexpr_vars -Hexpr_vars
     483                 lapply cm_expr
     484                 destruct (Htype_eq)
     485                 #cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup'
     486                 #Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq
     487                 destruct (Hexpr_eq)
     488                 whd in match (eval_expr ???????);
     489                 whd in match (lookup_present ?????);
     490                 lapply (Hlocal_matching … Hcl_lookup) >Hlookup' normalize nodelta
     491                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
     492                 #loaded_val * #Hload_val
     493                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     494                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
     495                 #Hload_success #Hlookup_in_cm_env
     496                 cases (Hlookup_in_cm_env ? Hload_success) #val'
     497                 * #Hlookup_in_cm #Hvalue_eq %{val'}
     498                 cases Hyp_present
     499                 >Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption
     500                 (* seems ok *)
    400501            ]
    401502       ]
  • src/common/Errors.ma

    r2496 r2500  
    273273  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C. ∀z.
    274274  bind2_eq ??? f g = return z →
    275   ∃x. ∃y. ∃Eq. f = return 〈x, y〉 ∧ g x y Eq = return z.
     275  ∃x. ∃y. ∃Eq. g x y Eq = return z.
    276276#A #B #C #f cases f
    277 [ * #a #b #g normalize #z #Heq %{a} %{b} %{(refl ??)} @conj try @refl @Heq
     277[ * #a #b #g normalize #z #Heq %{a} %{b} %{(refl ? (OK ? 〈a,b〉))} @Heq
    278278| #errmsg #g #z normalize #Habsurd destruct (Habsurd) ]
    279 qed. 
     279qed.
    280280
    281281definition res_to_opt : ∀A:Type[0]. res A → option A ≝
Note: See TracChangeset for help on using the changeset viewer.