Changeset 2527


Ignore:
Timestamp:
Dec 3, 2012, 6:22:46 PM (7 years ago)
Author:
garnier
Message:

Progress on CL to CM.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectness.ma

    r2510 r2527  
    395395qed.
    396396
    397 lemma exec_alloc_hit_monotonic : ∀variables,env,env',var_id.
    398   (∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) →
    399   ∀bl. lookup ?? env var_id = Some ? bl →
    400   ∃bl'.lookup ?? env' var_id = Some ? bl'.
    401 #variables elim variables
    402 [ #env #env' #var_id * #m * #m' normalize #Heq destruct
    403   #bl #H %{bl} @H
    404 | * #id #ty #tl #Hind #env #env' #var_id
    405   * #m * #m'
    406   whd in match (exec_alloc_variables ???);
    407   cases (alloc ????) #m * #b' #Hregion normalize nodelta
    408   @(match identifier_eq ? id var_id with [ inl Heq ⇒ ? | inr Hneq ⇒ ? ])
    409   [ 2: #Hexec' #bl #Hlookup
    410         lapply (Hind ?? var_id (ex_intro … (ex_intro … Hexec')) bl ?)
    411         [ <Hlookup @lookup_add_miss @sym_neq @Hneq ] // ]
    412   destruct (Heq) #Hexec' #bl' #Hlookup
    413   @(Hind ?? var_id (ex_intro … (ex_intro … Hexec')) b' ?)
    414   @lookup_add_hit
    415 ] qed.
    416397
    417398lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id.
     
    478459#H cases Hnot_exists #H' @H' @H
    479460qed.
    480  
    481 
    482 (* TODO : memory injections + link clight env+mem with local env+stack+mem *)
     461
     462lemma intsize_eq_elim_dec :
     463  ∀sz1,sz2.
     464  ∀P: ∀sz1,sz2. Type[0].
     465  ((∀ifok,iferr. intsize_eq_elim' sz1 sz1 P ifok iferr = ifok) ∧ sz1 = sz2) ∨
     466  ((∀ifok,iferr. intsize_eq_elim' sz1 sz2 P ifok iferr = iferr) ∧ sz1 ≠ sz2).
     467* * #P normalize
     468try /3 by or_introl, conj, refl/
     469%2 @conj try //
     470% #H destruct
     471qed.
     472
     473
    483474lemma eval_expr_sim :
    484475  ∀(inv:clight_cminor_inv).
     
    508499   ∀Hexpr_vars.
    509500   translate_expr vars (Expr ed ty) = OK ? («e', Hexpr_vars») →
    510    ∀resblo,resoff,trace,Hyp_present.
    511    exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈resblo, resoff, trace〉 →
    512    (* TODO: shift 〈resblo, resoff〉 through E *)
    513    eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, Vptr (mk_pointer resblo resoff)〉).
     501   ∀cl_blo,cl_off,trace,Hyp_present.
     502   exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
     503   match E cl_blo with
     504   [ Some loc ⇒
     505     let 〈cm_blo, delta〉 ≝ loc in
     506     match access_mode ty with
     507     [ By_value t ⇒
     508        (∃cm_val. loadv t cm_m (Vptr (mk_pointer cm_blo (offset_plus cl_off delta))) = Some ? cm_val ∧
     509                  eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉)
     510     | By_reference ⇒
     511        eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m
     512          = OK ? 〈trace, Vptr (mk_pointer cm_blo (offset_plus cl_off delta))〉             
     513     | By_nothing _ ⇒ True ]
     514   | None ⇒ False ]).
    514515#inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env
    515516#sp #cm_m #E #Hinj #Hlocal_matching
     
    523524  whd in Htranslate:(??%?);
    524525  [ 1,3,4,5,6,7,8: destruct ]
    525   (* This intsize_eq_elim' is the proof-equivalent of eating a sandwich with
    526      sand inside. *)
    527   @cthulhu
     526  cases (intsize_eq_elim_dec csz sz (λsz0.λsz0'.res (Σe0':expr (typ_of_type (Tint sz0' sg)).expr_vars (typ_of_type (Tint sz0' sg)) e0' (local_id vars))))
     527  [ 2: * #H_err #H_neq_sz
     528       lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
     529       >Htranslate #Habsurd destruct (Habsurd) ]
     530  * #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
     531  destruct (Heq_sz)
     532  >Htranslate -Htranslate -H_ok #Heq destruct (Heq)
     533  whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta
     534  #Heq destruct (Heq) %{(Vint sz i)} @conj try @refl //
    528535| 2: *
    529   [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
     536  [ #sz #i | #var_id | * #ed1 #ty1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1
    530537  | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ]
    531538  try /2 by I/
     
    693700            ]
    694701       ]       
    695   | 2: (* Deref case. Reduce the deref, exhibit the underlying load. *)
    696        cases (bind_inversion ????? Hcl_success) -Hcl_success
    697        * #cl_subexpr_val #cl_subexpr_trace *
    698        whd in ⊢ (? → (???%) → ?);
     702  | 2: whd in match (typeof ?) in Hind;
     703       lapply (Hind cm_expr Hexpr_vars Htranslate_expr cl_b cl_o cl_t Hyp_present) -Hind
     704       cases (bind_inversion ????? Hcl_success) -Hcl_success * #cl_subexpr_val #cl_trace *
     705       #Hexec_expr
    699706       @(match cl_subexpr_val
    700707         return λx. cl_subexpr_val = x → ?
     
    704711         | Vnull ⇒ λHval_eq. ?
    705712         | Vptr p ⇒ λHptr_eq. ? ] (refl ? cl_subexpr_val)) normalize nodelta
    706        [ 1,2,3: #_ #Habsurd destruct ]
    707        #Hcl_exec_to_pointer #Heq destruct (Heq)
    708        (* Now that we have executed the Clight part, reduce the Cminor one *)
    709        whd in Htranslate_expr:(??%?);
    710        cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
    711        * #cm_expr #Hexpr_vars * #Htranslate_expr
    712        whd (* ... *)   @cthulhu
    713   | 3: @cthulhu ]
     713       whd in ⊢ ((???%) → ?);
     714       [ 1,2,3: #Habsurd destruct ] #Heq destruct (Heq) destruct (Hptr_eq)
     715       whd in match (exec_lvalue' ?????) in Hind; #Hind
     716       cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val
     717       * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     718       lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hload_success
     719       whd in Hexec_expr:(???%); whd in match (exec_lvalue' ?????) in Hind;
     720       lapply Hind -Hind >Hexec_expr normalize nodelta
     721       #Hind lapply (Hind (refl ??)) -Hind
     722       @(match E (pblock p)
     723         return λx. (E (pblock p) = x) → ?
     724         with
     725         [ None ⇒ λHembed. ?
     726         | Some loc ⇒ λHembed. ? ] (refl ? (E (pblock p))))
     727       normalize nodelta
     728       [ 1: @False_ind ]
     729       cases loc in Hembed; normalize nodelta
     730       lapply Hload_success -Hload_success
     731       lapply Hexec_expr -Hexec_expr
     732       lapply Hyp_present -Hyp_present
     733       lapply Htranslate_expr -Htranslate_expr
     734       lapply Hexpr_vars -Hexpr_vars
     735       lapply cm_expr -cm_expr
     736       cases ty
     737       [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     738       | #structname #fieldspec | #unionname #fieldspec | #id ]
     739       normalize nodelta
     740       #cm_expr #Hexpr_vars #Htranslate_expr #Hyp_present #Hexec_expr
     741       #Hload_success #BL #OFF #Hembed
     742       [ 1,6,7: normalize in Hload_success; #_ destruct
     743       | 4,5: whd in match (typ_of_type ?); #Heval >Heval
     744              %{(Vptr (mk_pointer BL (offset_plus (poff p) OFF)))}
     745              @conj try @refl
     746              lapply (load_value_of_type_by_ref … Hload_success ??) try //
     747              #Heq >Heq %4 whd in ⊢ (??%%); >Hembed @refl
     748       | *: * #cm_val * #Hloadv #Heval_expr >Heval_expr
     749              lapply (mi_inj … Hinj … (pblock p) (poff p) BL (offset_plus (poff p) OFF) … Hload_success)
     750              [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl
     751              | 2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ]
     752              * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq'
     753              %{cm_val'} @conj try assumption
     754              whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success';
     755              #Heq destruct @refl ]
     756  | 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
     757       lapply (refl ? (typeof e1))
     758       cases (typeof e1) in ⊢ ((???%) → %);
     759       [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     760       | #structname #fieldspec | #unionname #fieldspec | #id ]
     761       #Heq_typeof normalize nodelta
     762       [ 1,2,3,4,5,8: #Habsurd destruct ]
     763       #Hexec_compound_clight
     764       lapply (Hind … Htranslate_expr) -Hind -Htranslate_expr
     765       cases (bind_inversion ????? Hexec_compound_clight) -Hexec_compound_clight
     766       * * #CLB #CLO #CLTR
     767       * #Hexec_lvalue #Hfield_offset whd in match (exec_lvalue' ?????);
     768       >Hexec_lvalue normalize nodelta >Heq_typeof normalize nodelta
     769       whd in match (m_bind ?????);
     770       [ 2: normalize in Hfield_offset; destruct (Hfield_offset)
     771            #Hind lapply (Hind ??? Hyp_present (refl ??)) -Hind
     772            @(match E cl_b
     773            return λx. (E cl_b = x) → ?
     774            with
     775            [ None ⇒ λHembed. ?
     776            | Some loc ⇒ λHembed. ? ] (refl ? (E cl_b))) normalize nodelta
     777            [ 1: @False_ind ] cases loc in Hembed; #BLO #OFF #Hembed normalize nodelta
     778            lapply Hyp_present -Hyp_present
     779            lapply Hexpr_vars -Hexpr_vars
     780            lapply cm_expr -cm_expr
     781            cases ty normalize nodelta
     782            [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
     783            | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]
     784            #cm_expr #Hexpr_vars #Hyp_present
     785            [ 1,6,7: #_ #Hload_void cases (bind_inversion ????? Hload_void)
     786                   #val * #Hopt_to_res #Hok lapply (opt_to_res_inversion ???? Hopt_to_res)
     787                   normalize in ⊢ (% → ?); #Habsurd destruct                   
     788            | 4,5: whd in match (typ_of_type ?); #Heval >Heval
     789                   #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp)
     790                   #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?);                   
     791                   lapply (opt_to_res_inversion ???? Hopt_to_res)
     792                   #Hload_success #Heq destruct (Heq)
     793                   lapply (load_value_of_type_by_ref … Hload_success ??) try //
     794                   #Hval_eq >Hval_eq                   
     795                   %{(Vptr (mk_pointer BLO (offset_plus cl_o OFF)))}
     796                   @conj try @refl
     797                   %4 whd in ⊢ (??%%); >Hembed @refl
     798            | 2,3,8: * #cm_val * #Hloadv #Heval_expr >Heval_expr
     799                   #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp)
     800                   #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     801                   lapply (opt_to_res_inversion ???? Hopt_to_res)
     802                   #Hload_success
     803                   lapply (mi_inj … Hinj … cl_b cl_o BLO (offset_plus cl_o OFF) … Hload_success)
     804                   [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl
     805                   | 2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ]
     806                   * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq'
     807                   %{cm_val'} @conj try assumption
     808                   whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success';
     809                   #Heq destruct (Heq) @refl ]
     810       | 1: cases (bind_inversion ????? Hfield_offset) -Hfield_offset #field_offset * #Hfield_offset_eq
     811            #Heq whd in Heq:(???%); destruct (Heq) >Hfield_offset_eq normalize nodelta
     812            #Hind lapply (Hind ??? Hyp_present (refl ??)) -Hind
     813            @(match E cl_b
     814            return λx. (E cl_b = x) → ?
     815            with
     816            [ None ⇒ λHembed. ?
     817            | Some loc ⇒ λHembed. ? ] (refl ? (E cl_b)))
     818            normalize nodelta
     819            [ 1: @False_ind ] cases loc in Hembed; #BLO #OFF #Hembed normalize nodelta
     820            lapply Hyp_present -Hyp_present
     821            lapply Hexpr_vars -Hexpr_vars
     822            lapply cm_expr -cm_expr
     823            cases ty normalize nodelta
     824            [ | #sz' #sg' | #ptr_ty' | #array_ty' #array_sz' | #domain' #codomain'
     825            | #structname' #fieldspec' | #unionname' #fieldspec' | #id' ]           
     826            #cm_expr #Hexpr_vars #Hyp_present
     827            [ 1,6,7: #_ #Hload_void cases (bind_inversion ????? Hload_void)
     828                   #val * #Hopt_to_res #Hok lapply (opt_to_res_inversion ???? Hopt_to_res)
     829                   normalize in ⊢ (% → ?); #Habsurd destruct
     830            | 4,5: whd in match (typ_of_type ?); #Heval >Heval
     831                   #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp) -Hload_success_hyp
     832                   #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?);                   
     833                   lapply (opt_to_res_inversion ???? Hopt_to_res)
     834                   #Hload_success #Heq destruct (Heq)
     835                   lapply (load_value_of_type_by_ref … Hload_success ??) try //
     836                   #Hval_eq >Hval_eq                   
     837                   %{(Vptr (mk_pointer BLO (offset_plus (shift_offset (bitsize_of_intsize I32) CLO (repr I32 field_offset)) OFF)))}
     838                   @conj try @refl
     839                   %4 whd in ⊢ (??%%); >Hembed @refl
     840            | 2,3,8: * #cm_val * #Hloadv #Heval_expr >Heval_expr
     841                   #Hload_success_hyp cases (bind_inversion ????? Hload_success_hyp)
     842                   #cl_val * #Hopt_to_res whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     843                   lapply (opt_to_res_inversion ???? Hopt_to_res)
     844                   #Hload_success
     845                   lapply (mi_inj ??? Hinj
     846                            cl_b
     847                            (mk_offset
     848                              (addition_n offset_size (offv CLO)
     849                              (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 field_offset))))
     850                            BLO (offset_plus (mk_offset
     851                              (addition_n offset_size (offv CLO)
     852                              (sign_ext (bitsize_of_intsize I32) offset_size (repr I32 field_offset)))) OFF) ? val ?? Hload_success)
     853                   [ 1,4,7: whd in ⊢ (??%?); >Hembed @refl
     854                   | 2,5,8: @(load_by_value_success_valid_pointer … Hload_success) // ]
     855                   * #cm_val' * >Hload_success #Hload_success' #Hvalue_eq'
     856                   %{cm_val'} @conj try assumption
     857                   whd in Hloadv:(??%?) Hload_success':(??%?); >Hloadv in Hload_success';
     858                   #Heq destruct (Heq) @refl ]
     859  ] ]
     860| 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
     861     whd in Hexec_lvalue_var:(??%?);
     862     (* check whether var is local or global *)
     863     lapply (Hlocal_matching var) cases (lookup ?? cl_env var) in Hexec_lvalue_var;
     864     normalize nodelta
     865     [ 1: (* global *)
     866          #Hexec_opt
     867          cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
     868          whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq)
     869          >(opt_to_res_inversion ???? Hopt_to_res) normalize nodelta
     870          #Hembed >Hembed normalize nodelta
     871          (* Standard stuff. *)
     872          @cthulhu
     873     | 2: (* local *)
     874          @cthulhu
     875     ]
    714876| *: @cthulhu
    715 ] qed. 
     877] qed.
    716878
    717879
Note: See TracChangeset for help on using the changeset viewer.