Changeset 2496 for src/Clight
 Timestamp:
 Nov 27, 2012, 5:50:51 PM (9 years ago)
 Location:
 src/Clight
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/abstract.ma
r2328 r2496 38 38 (* Help avoid ambiguous input fun *) 39 39 definition Clight_state ≝ state. 40 41 definition cl_genv ≝ genv. 42 43 definition cl_env ≝ env. 44 45 definition cl_cont ≝ cont. 46 47 definition cl_eval_expr ≝ eval_expr. 
src/Clight/frontend_misc.ma
r2468 r2496 85 85 ∃x. e = Some ? x ∧ f x = Some ? res. 86 86 #A #B #e #res #f cases e normalize nodelta 87 [ 1: #Habsurd destruct (Habsurd) 88  2: #a #Heq %{a} @conj >Heq @refl ] 89 qed. 90 91 lemma 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 87 102 [ 1: #Habsurd destruct (Habsurd) 88 103  2: #a #Heq %{a} @conj >Heq @refl ] 
src/Clight/toCminor.ma
r2469 r2496 621 621 ] *) 622 622  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. 626 627 (* We are accessing a global variable in an expression. Its Cminor counterpart also depends on 627 628 its access mode: … … 635 636  By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] 636 637 ] 637  Stack n ⇒ λ E.638  Stack n ⇒ λHeq_c. 638 639 (* We have decided that the variable should be allocated on the stack, 639 640 * because its adress was taken somewhere or becauste it's a structured data. *) … … 647 648 ] 648 649 (* 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 ] E650  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) 651 652  Ederef e1 ⇒ 652 653 do e1' ← translate_expr vars e1; … … 796 797 ]. 797 798 whd try @I 798 [ >E whd @refl799 [ >E whd >Heq_c @refl 799 800  2,3: @pi2 800 801  @(translate_binop_vars … E) @pi2 
src/Clight/toCminorCorrectness.ma
r2489 r2496 265 265 }. 266 266 267 include "Clight/CexecInd.ma". 268 include "Clight/frontend_misc.ma". 269 include "Clight/memoryInjections.ma". 270 271 lemma 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 281 qed. 282 283 definition 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 *) 307 lemma 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 proofequivalent 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 267 425 268 426 axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
Note: See TracChangeset
for help on using the changeset viewer.