# Changeset 2496 for src/Clight

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

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

Location:
src/Clight
Files:
4 edited

Unmodified
Removed
• ## src/Clight/abstract.ma

 r2328 (* Help avoid ambiguous input fun *) definition Clight_state ≝ state. definition cl_genv ≝ genv. definition cl_env ≝ env. definition cl_cont ≝ cont. definition cl_eval_expr ≝ eval_expr.
• ## src/Clight/frontend_misc.ma

 r2468 ∃x. e = Some ? x ∧ f x = Some ? res. #A #B #e #res #f cases e normalize nodelta [ 1: #Habsurd destruct (Habsurd) | 2: #a #Heq %{a} @conj >Heq @refl ] qed. lemma res_inversion : ∀A,B:Type[0]. ∀e:option A. ∀errmsg. ∀result:B. ∀f:A → res B. match e with [ None ⇒ Error ? errmsg | Some x ⇒ f x ] = OK ? result → ∃x. e = Some ? x ∧ f x = OK ? result. #A #B #e #errmsg #result #f cases e normalize nodelta [ 1: #Habsurd destruct (Habsurd) | 2: #a #Heq %{a} @conj >Heq @refl ]
• ## src/Clight/toCminor.ma

 r2469 ] *) | Evar id ⇒ do 〈c,t〉 as E ← lookup' vars id; (* E is an equality proof of the shape "lookup' vars id = Ok " *) match c return λx.? = ? → res (Σe':CMexpr ?. ?) with [ Global r ⇒ λ_. (* E is an equality proof of the shape "lookup' vars id = Ok " *) do 〈c,t〉 as E ← lookup' vars id; match c return λx. (c = x) → res (Σe':CMexpr ?. ?) with [ Global r ⇒ λHeq_c. (* We are accessing a global variable in an expression. Its Cminor counterpart also depends on its access mode: | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] ] | Stack n ⇒ λE. | Stack n ⇒ λHeq_c. (* We have decided that the variable should be allocated on the stack, * because its adress was taken somewhere or becauste it's a structured data. *) ] (* 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. *) | 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, ?») ] E | 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, ?») ] (refl ? c) | Ederef e1 ⇒ do e1' ← translate_expr vars e1; ]. whd try @I [ >E whd @refl [ >E whd >Heq_c @refl | 2,3: @pi2 | @(translate_binop_vars … E) @pi2
• ## src/Clight/toCminorCorrectness.ma

 r2489 }. include "Clight/CexecInd.ma". include "Clight/frontend_misc.ma". include "Clight/memoryInjections.ma". lemma intsize_eq_inversion : ∀sz,sz'. ∀A:Type[0]. ∀ok,not_ok. intsize_eq_elim' sz sz' (λsz,sz'. res A) (OK ? ok) (Error ? not_ok) = (OK ? ok) → sz = sz'. * * try // normalize #A #ok #not_ok #Habsurd destruct qed. definition local_matching ≝ λE:embedding. λm,m':mem. λen:cl_env. λvenv:cm_env. λsp:block. λvars:var_types. ∀id,cl_blo. lookup SymbolTag ? en id = Some ? cl_blo → match lookup ?? vars id with [ Some kind ⇒ let 〈vtype, type〉 ≝ kind in match vtype with [ Stack n ⇒ E cl_blo = Some ? 〈sp, offset_of_Z (Z_of_nat n)〉 | Local ⇒ ∀v,v'. load_value_of_type type m cl_blo zero_offset = Some ? v → lookup ?? venv id = Some ? v' → value_eq E v v' | _ ⇒ False ] | None ⇒ False ]. (* TODO : memory injections + link clight env+mem with local env+stack+mem *) lemma eval_expr_sim : ∀(inv:clight_cminor_inv). ∀(cl_env:cl_env). ∀(cl_m:mem). ∀(cm_env:cm_env). ∀(sp:block). ∀(cm_m:mem). ∀(vars:var_types). ∀E:embedding. ∀minj:memory_inj E cl_m cm_m. local_matching E cl_m cm_m cl_env cm_env sp vars → (∀(e:expr). ∀(e':CMexpr (typ_of_type (typeof e))). (*vars = pi1 … (characterise_vars … [globals] [f]) →*) (*local_matching en m venv sp m' →  *) ∀Hexpr_vars. translate_expr vars e = OK ? («e', Hexpr_vars») → ∀val,trace,Hyp_present. exec_expr (ge_cl … inv) cl_env cl_m e = OK ? 〈val, trace〉 → eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, val〉) ∧ (∀ed,ty. ∀(e':CMexpr (typ_of_type ty)). (*vars = pi1 … (characterise_vars … [globals] [f]) →*) (*local_matching en m venv sp m' →  *) ∀Hexpr_vars. translate_expr vars (Expr ed ty) = OK ? («e', Hexpr_vars») → ∀resblo,resoff,trace,Hyp_present. exec_lvalue' (ge_cl … inv) cl_env cl_m ed ty = OK ? 〈resblo, resoff, trace〉 → eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, Vptr (mk_pointer resblo resoff)〉). #inv #cl_env #cl_m #cm_env #sp #cm_m #vars #E #Hinj #Hlocal_matching @expr_lvalue_ind_combined [ 1: (* Integer constant *) #csz #ty cases ty [ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ] #i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate #val #trace #Hpresent #Hexec_cl whd in Htranslate:(??%?); [ 1,3,4,5,6,7,8: destruct ] (* This intsize_eq_elim' is the proof-equivalent of eating a sandwich with sand inside. *) @cthulhu | 2: * [ #sz #i | #var_id | #e1 | #e1 | #op #e1 | #op #e1 #e2 | #cast_ty #e1 | #cond #iftrue #iffalse | #e1 #e2 | #e1 #e2 | #sizeofty | #e1 #field | #cost #e1 ] #ty whd in ⊢ (% → ?); #Hind try @I whd in match (Plvalue ???); whd in match (typeof ?); #cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec whd in Hexec:(??%?); whd in match (exec_lvalue' ?????) in Hexec:(??%?); cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success whd in Hcl_success:(???%); [ 1: (* var case *) lapply Hcl_success -Hcl_success (* Peform case analysis on presence of variable in local Clight env. * if success, exec_expr/exec_lvalue tells us that it shoud be local. *) @(match lookup SymbolTag block cl_env var_id return λx.(lookup SymbolTag block cl_env var_id = x) → ? with [ None ⇒ λHcl_lookup. ? | Some loc ⇒ λHcl_lookup. ? ] (refl ? (lookup SymbolTag block cl_env var_id))) normalize nodelta [ 1: (* global case *) @cthulhu (* TODO: case analysis on lookup in global, if so use Brian's invariant *) | 2: (* local case *) #Heq destruct (Heq) lapply (bind2_eq_inversion ?????? Htranslate_expr) * #var_alloc_type * #var_type * generalize in match var_alloc_type; * normalize nodelta [ 1: (* Global case. This should be contradictory, right ? * If lookup succeeded, then our local shadows any global with the same * name, and [characterise_vars] should say so. TODO, this lemma. *) @cthulhu | 2: (* Stack local *) #stack_depth #Hlookup_vartype_success * #_ lapply (Hlocal_matching … Hcl_lookup) whd in Hlookup_vartype_success:(??%?); lapply (res_inversion ?????? Hlookup_vartype_success) * * #var_alloc_type' #var_type' * #Hlookup' #Heq destruct (Heq) >Hlookup' normalize nodelta #Hembedding_eq (* TODO modify local_invariant to match the needs here *) @cthulhu | 3: (* Register local *) #Hlookup_eq * #_ (* TODO : elim type_should_eq, extract type equality, use local_matching *) @cthulhu ] ] | 2: (* Deref case. Reduce the deref, exhibit the underlying load. *) cases (bind_inversion ????? Hcl_success) -Hcl_success * #cl_subexpr_val #cl_subexpr_trace * whd in ⊢ (? → (???%) → ?); @(match cl_subexpr_val return λx. cl_subexpr_val = x → ? with [ Vundef ⇒ λHval_eq. ? | Vint sz' i ⇒ λHval_eq. ? | Vnull ⇒ λHval_eq. ? | Vptr p ⇒ λHptr_eq. ? ] (refl ? cl_subexpr_val)) normalize nodelta [ 1,2,3: #_ #Habsurd destruct ] #Hcl_exec_to_pointer #Heq destruct (Heq) (* Now that we have executed the Clight part, reduce the Cminor one *) whd in Htranslate_expr:(??%?); cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr * #cm_expr #Hexpr_vars * #Htranslate_expr whd (* ... *)   @cthulhu | 3: @cthulhu ] | *: @cthulhu ] qed. axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
Note: See TracChangeset for help on using the changeset viewer.