Changeset 2510


Ignore:
Timestamp:
Nov 30, 2012, 4:40:37 PM (7 years ago)
Author:
garnier
Message:

Some progress on the Cl -> Cm front

Location:
src/Clight
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2500 r2510  
    285285(* General results on lists. *)
    286286(* --------------------------------------------------------------------------- *)
     287
     288let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝
     289match l with
     290[ nil ⇒ false
     291| cons hd tl ⇒
     292  let 〈id, ty〉 ≝ hd in
     293  match identifier_eq SymbolTag i id with
     294  [ inl Hid_eq ⇒ true
     295  | inr Hid_neq ⇒ mem_assoc_env i tl 
     296  ]
     297].
    287298
    288299(* If mem succeeds in finding an element, then the list can be partitioned around this element. *)
  • src/Clight/switchRemoval.ma

    r2488 r2510  
    757757     <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl
    758758] qed.
    759 
    760 (* Lookup functions in list environments (used to type local variables in functions) *)     
    761 let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝
    762 match l with
    763 [ nil ⇒ false
    764 | cons hd tl ⇒
    765   let 〈id, ty〉 ≝ hd in
    766   match identifier_eq SymbolTag i id with
    767   [ inl Hid_eq ⇒ true
    768   | inr Hid_neq ⇒ mem_assoc_env i tl 
    769   ]
    770 ].
    771759
    772760(* --------------------------------------------------------------------------- *)
  • src/Clight/toCminor.ma

    r2496 r2510  
    114114  (* globals are added into a map, with var_type Global, region π_2(idrt) and type π_3(idrt) *)
    115115  let m ≝ foldr ?? (λidrt,m. add ?? m (\fst (\fst idrt)) 〈Global (\snd (\fst idrt)), \snd idrt〉) (empty_map ??) globals in
    116   (* variables in the body of the function are gathered in [mem_vars] *)
     116  (* variables whose addr is taken in the body of the function are gathered in [mem_vars] *)
    117117  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
    118118  (* iterate on the parameters and local variables of the function, with a tuple (map, stack_high) as an accumulator *)
  • src/Clight/toCminorCorrectness.ma

    r2500 r2510  
    281281qed.
    282282
    283 definition local_matching ≝
     283(* Perhaps we will have to be more precise on what is allocated, etc.
     284   cf [exec_alloc_variables]. For now this is conveniently hidden in
     285   the [value_eq E v v'] *)
     286definition memory_matching ≝
    284287  λE:embedding.
    285288  λm,m':mem.
    286289  λen:cl_env.
    287290  λvenv:cm_env.
     291  λcminv:clight_cminor_inv.
    288292  λsp:block.
    289293  λ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. 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'
    302                 | _ ⇒ False ]
    303               | None ⇒ False ].
     294  ∀id.
     295    match lookup SymbolTag ? en id with
     296    [ None ⇒
     297      match find_symbol ? (ge_cl cminv) id with
     298      [ None ⇒ True
     299      | Some cl_blo ⇒ E cl_blo = Some ? 〈cl_blo, zero_offset〉
     300      ]
     301    | Some cl_blo ⇒
     302         match lookup ?? vars id with
     303         [ Some kind ⇒
     304            let 〈vtype, type〉 ≝ kind in
     305            match vtype with
     306            [ Stack n ⇒
     307              E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉
     308            | Local ⇒
     309              ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
     310                   ∃v'. lookup ?? venv id = Some ? v' ∧
     311                        value_eq E v v'
     312            | _ ⇒ False ]
     313        | None ⇒ False ]
     314    ].
    304315             
    305316lemma type_should_eq_inversion :
     
    330341| *: #Hload normalize #_ #H
    331342      lapply (jmeq_to_eq ??? H) #Heq destruct
    332 ] qed.       
    333 
    334 
     343] qed.
     344
     345lemma load_value_of_type_by_value :
     346  ∀ty,m,b,off,val.
     347  access_mode ty = By_value (typ_of_type ty) →
     348  load_value_of_type ty m b off = Some ? val →
     349  loadv (typ_of_type ty) m (Vptr (mk_pointer b off)) = Some ? val.
     350
     351[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain
     352| #structname #fieldspec | #unionname #fieldspec | #id ]
     353#m #b #off #val
     354normalize in match (access_mode ?);
     355[ 1,4,5,6,7: #Habsurd destruct ]
     356#_
     357#H @H
     358qed.
     359
     360include "Clight/CexecSound.ma".
     361
     362lemma lookup_exec_alloc :
     363  ∀source_variables, initial_env, env, var_id, clb, m, m'.
     364  lookup ?? env var_id = Some ? clb →
     365  exec_alloc_variables initial_env m source_variables = 〈env,m'〉 →
     366  lookup ?? initial_env var_id = Some ? clb ∨
     367  Exists ? (λx. \fst x = var_id) source_variables.
     368#source_variables
     369elim source_variables
     370[ 1: #init_env #env #var #clb #m #m' #Hlookup #Hexec_alloc normalize in Hexec_alloc;
     371     destruct (Hexec_alloc) %1 @Hlookup
     372| 2: * #id #ty #tail #Hind
     373     #init_env #env #var #clb #m #m' #Hlookup     
     374     whd in ⊢ (??%? → ?);
     375     cases (alloc m 0 (sizeof ty) XData) #m0 * #blo #Hreg normalize nodelta
     376     #Hexec_alloc
     377     @(match identifier_eq ? id var with [ inl Heq ⇒ ? | inr Hneq ⇒ ? ])
     378     [ 1: destruct (Heq) %2 %1 @refl ]
     379     cases (Hind … Hlookup Hexec_alloc)
     380     [ @cthulhu (* standard reasoning on positive_maps. check lib. *)
     381     | #Hexists %2 %2 @Hexists ]
     382] qed.
     383
     384lemma characterise_vars_lookup_local :
     385  ∀globals,f,vartypes,stacksize,id,clb,env.
     386   characterise_vars globals f = 〈vartypes, stacksize〉 →
     387   lookup ?? env id = Some ? clb →
     388   (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈env,m'〉) →
     389   ∃t. local_id vartypes id t.
     390#globals #f #vartypes #stacksize #id #clb #env
     391#Hchar #Hlookup * #m * #m' #Hexec
     392cases (lookup_exec_alloc … Hlookup Hexec)
     393[ normalize in ⊢ (% → ?); #Heq destruct
     394| @(characterise_vars_localid … Hchar) ]
     395qed.
     396
     397lemma 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.
     416
     417lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id.
     418  (∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) →
     419  lookup ?? env' var_id = None ? →
     420  lookup ?? env var_id = None ? ∧
     421  ¬(Exists (ident×type) (λx:ident×type.\fst  x=var_id) variables). 
     422#vars elim vars
     423[ #env #env' #var_id normalize * #m * #m' #Heq destruct (Heq)
     424  #H @conj try @H % //
     425| * #id' #ty' #tl #Hind #env #env' #var * #m * #m'
     426  whd in ⊢ ((??%?) → ? → ?);
     427  cases (alloc m 0 (sizeof ty') XData) #m0 * #b #Hregion
     428  normalize nodelta #Hexec #Hlookup
     429  lapply (Hind …  (ex_intro … (ex_intro … Hexec)) Hlookup)
     430  cases env #env cases id' #id' cases var #var normalize
     431  @(eqb_elim … id' var)
     432  [ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
     433       #Heq <Heq @conj try @Hlookup' % *
     434       [ #Heq' destruct (Heq') cases Hneq #H @H @refl
     435       | cases Hexists' #H @H ]
     436  | 1: #Heq destruct (Heq) * #Hlookup' #Hexists'   
     437       lapply (lookup_opt_pm_set_hit … (Some ? b) var … env) #H1
     438       >H1 in Hlookup'; #Heq destruct
     439  ]
     440] qed.
     441
     442lemma variable_not_in_env_but_in_vartypes_is_global :
     443  ∀env,env',f,vars,stacksize,globals,var_id,allocty,ty.
     444  (∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) →
     445  characterise_vars globals f =〈vars,stacksize〉 →
     446  lookup ?? env' var_id = None ? →       
     447  lookup' vars var_id = OK ? 〈allocty, ty〉 →
     448  ∃r.allocty = Global r.
     449#env #env' #f #vars #stacksize #globals #var_id #allocty #ty #Hexec_alloc
     450#Hcharacterise #Hlookup_fail #Hlookup_type_ok
     451lapply (characterise_vars_src … Hcharacterise var_id ?)
     452[ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t *
     453 #Hlookup >Hlookup #_ #Habsurd destruct ]
     454*
     455[ 1: * #r * #ty' * #Hlookup' #Hex %{r}
     456     >Hlookup' in Hlookup_type_ok; #Heq destruct @refl ]
     457* #t whd in ⊢ (% → ?); >Hlookup_type_ok whd normalize nodelta
     458@(match allocty
     459  return λx. allocty = x → ?
     460  with
     461  [ Global r ⇒ λ_. ?
     462  | Stack st' ⇒ λHalloc. ?
     463  | Local ⇒ λHalloc. ?
     464  ] (refl ? allocty))
     465[ @False_ind ] normalize nodelta
     466#Heq_typ
     467(* Halloc is in contradiction with Hlookup_fail *)
     468lapply (exec_alloc_fail_antimonotonic … Hexec_alloc … Hlookup_fail)
     469* #Hlookup' #Hnot_exists
     470lapply (characterise_vars_all … Hcharacterise var_id t ?)
     471[ 1,3: whd destruct (Halloc) >Hlookup_type_ok // ]
     472#Hexists @False_ind
     473cut (Exists (ident×type) (λx:ident×type.\fst  x=var_id) (fn_params f@fn_vars f))
     474[ 1,3: elim (fn_params f @ fn_vars f) in Hexists; //
     475       * #id' #ty' #tl #Hind *
     476       [ 1,3: * #Heq #_ %1 @Heq
     477       | *: #H %2 @Hind @H ] ]
     478#H cases Hnot_exists #H' @H' @H
     479qed.
     480 
    335481
    336482(* TODO : memory injections + link clight env+mem with local env+stack+mem *)
    337483lemma eval_expr_sim :
    338484  ∀(inv:clight_cminor_inv).
    339 
     485  ∀(f:function).
     486  ∀(vars:var_types).
     487  ∀stacksize.
     488  characterise_vars (globals inv) f = 〈vars, stacksize〉 →
    340489  ∀(cl_env:cl_env).
     490  (∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉) →
    341491  ∀(cl_m:mem).
    342 
    343492  ∀(cm_env:cm_env).
    344493  ∀(sp:block).
    345494  ∀(cm_m:mem).
    346   ∀(vars:var_types).
    347 
    348495  ∀E:embedding.
    349496  ∀minj:memory_inj E cl_m cm_m.
    350   local_matching E cl_m cm_m cl_env cm_env sp vars →
    351 
    352    (*vars = pi1 … (characterise_vars … [globals] [f]) →*)
    353    (*local_matching en m venv sp m' →  *)
    354 
     497  memory_matching E cl_m cm_m cl_env cm_env inv sp vars →
    355498  (∀(e:expr).
    356499   ∀(e':CMexpr (typ_of_type (typeof e))).
     
    361504   ∃cm_val. eval_expr (ge_cm inv) (typ_of_type (typeof e)) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, cm_val〉 ∧
    362505            value_eq E cl_val cm_val) ∧
    363 
    364506  (∀ed,ty.
    365507   ∀(e':CMexpr (typ_of_type ty)).
     
    370512   (* TODO: shift 〈resblo, resoff〉 through E *)
    371513   eval_expr (ge_cm inv) (typ_of_type ty) e' cm_env Hyp_present sp cm_m = OK ? 〈trace, Vptr (mk_pointer resblo resoff)〉).
    372 #inv #cl_env #cl_m #cm_env #sp #cm_m #vars #E #Hinj #Hlocal_matching
     514#inv #f #vars #stacksize #Hcharacterise #cl_env #Hexec_alloc #cl_m #cm_env
     515#sp #cm_m #E #Hinj #Hlocal_matching
    373516@expr_lvalue_ind_combined
    374517[ 1: (* Integer constant *)
     
    396539  whd in Hcl_success:(???%);
    397540  [ 1: (* var case *)
    398 
    399        lapply Hcl_success -Hcl_success
     541       lapply Hcl_success -Hcl_success -Hind
    400542       (* Peform case analysis on presence of variable in local Clight env.
    401543        * if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
     
    408550       normalize nodelta
    409551       [ 1: (* global case *)
    410             @cthulhu (* TODO: case analysis on lookup in global, if so use Brian's invariant *)
     552            #Hlookup_global
     553            cases (bind_inversion ????? Hlookup_global) -Hlookup_global #global_block
     554            * #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol
     555            #Heq whd in Heq:(???%); destruct (Heq)
     556            lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
     557            * #var_id_alloctype * #var_id_type * #Heq
     558            cases (variable_not_in_env_but_in_vartypes_is_global …
     559                        Hexec_alloc Hcharacterise Hcl_lookup Heq)
     560            #r #Heq' destruct (Heq') normalize nodelta
     561            lapply Hcl_load_success -Hcl_load_success
     562            lapply Hyp_present -Hyp_present
     563            lapply Hexpr_vars -Hexpr_vars
     564            lapply cm_expr -cm_expr inversion (access_mode ty)
     565            [ #typ_of_ty | | #typ_of_ty ]
     566            #Heq_typ_of_type #Heq_access_mode
     567            #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
     568            whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
     569            whd in match (eval_expr ???????);
     570            whd in match (eval_expr ???????);
     571            whd in match (eval_constant ????);
     572            <(eq_sym … inv) >Hfind_symbol normalize nodelta
     573            cases (bind_inversion ????? Hcl_load_success) #x *
     574            #Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val)
     575            lapply (opt_to_res_inversion ???? Hopt_to_res)
     576            #Hcl_load_success
     577            [ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
     578                 @conj try @refl
     579                 whd in Hcm_load_success:(??%?);
     580                 lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty
     581                 >(load_value_of_type_by_ref … Hcl_load_success)
     582                 try assumption %4
     583                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
     584                 >Hfind_symbol normalize nodelta #Heq_embedding
     585                 whd in match (shift_offset ???);
     586                 >addition_n_0 whd in match (pointer_translation ??); >Heq_embedding
     587                 normalize nodelta @refl
     588            | 1: cut (access_mode ty=By_value (typ_of_type ty))
     589                 [ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt
     590                   lapply Heq_access_mode <Heqt // ] #Haccess
     591                 lapply (load_by_value_success_valid_pointer … Haccess … Hcl_load_success)
     592                 #Hvalid_ptr
     593                 lapply (mi_inj … Hinj ?? cl_b zero_offset … Hvalid_ptr … Hcl_load_success)
     594                 [ whd in ⊢ (??%?);
     595                   lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
     596                   >Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ]
     597                 * #val' * #Hcm_load_success #Hvalue_eq
     598                 lapply (load_value_of_type_by_value … Haccess … Hcm_load_success)
     599                 #Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq <Htypeq >Hloadv
     600                 normalize %{val'} @conj try @refl assumption ]
    411601       | 2: (* local case *)
    412602            #Heq destruct (Heq)
     
    414604            * #var_id_alloc_type * #var_id_type *
    415605            generalize in match var_id_alloc_type; * normalize nodelta
    416             [ 1: (* Global case. This should be contradictory, right ?
    417                   * If lookup succeeded, then our local shadows any global with the same
    418                   * name, and [characterise_vars] should say so. TODO, this lemma. *)
    419                  @cthulhu
     606            [ 1: #r #Hlookup_vartype
     607                 lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc)
     608                 * #typ whd in match (local_id ???);
     609                 >Hlookup_vartype normalize nodelta @False_ind
    420610            | 2: (* Stack local *)
    421611                 lapply Hcl_load_success -Hcl_load_success
     
    428618                 #stack_depth #Hlookup_vartype_success normalize nodelta
    429619                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    430                  lapply (Hlocal_matching … Hcl_lookup)
    431                  whd in Hlookup_vartype_success:(??%?);
     620                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
    432621                 cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
    433622                 * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
     
    437626                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    438627                 lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
    439                  #Hload_success
    440                  whd in match (eval_expr ???????);
     628                 #Hload_success whd in match (eval_expr ???????);
    441629                 cut (pointer_translation (mk_pointer cl_b zero_offset) E =
    442                       Some ? (mk_pointer sp (offset_of_Z stack_depth)))
     630                      Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth))))
    443631                 [ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
    444632                        >offset_plus_0 @refl ]
    445                  #Hpointer_translation       
     633                 #Hpointer_translation
    446634                 [ 2: (* By-ref *)
    447635                      whd in Hload_success:(??%?);
     
    451639                      %{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
    452640                      @conj try @refl
    453                       %4 (* boring and trivial *)
    454                       @cthulhu                     
     641                      %4 whd in match (shift_offset ???);
     642                      whd in match zero_offset;
     643                      >commutative_addition_n >addition_n_0 @Hpointer_translation
    455644                 | 1: (* By value *)
     645                      lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0                       
    456646                      lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
    457647                      [ @(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 ]
     648                        lapply Heq_access_mode <Heq0 /2 by jmeq_to_eq/ ]
    462649                      * #cm_val * #Hload_in_cm #Hvalue_eq
    463650                      %{cm_val} @conj try assumption
    464                       (* unpack Hload_in_cm using Heq_access_mode as an hypothesis. profit *)
    465                       @cthulhu ]
     651                      lapply (load_value_of_type_by_value … Hload_in_cm)
     652                      [ lapply Heq_access_mode <Heq0 #Heq1
     653                        @(jmeq_to_eq ??? Heq1) ]
     654                      #Hloadv <Heq0
     655                      whd in match (shift_offset ???); >commutative_addition_n >addition_n_0
     656                      >Hloadv @refl ]
    466657            | 3: (* Register local variable *)
    467658                 #Hlookup_eq
     
    488679                 whd in match (eval_expr ???????);
    489680                 whd in match (lookup_present ?????);
    490                  lapply (Hlocal_matching … Hcl_lookup) >Hlookup' normalize nodelta
     681                 lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
     682                 >Hlookup' normalize nodelta #Hmatching
    491683                 cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
    492                  #loaded_val * #Hload_val 
     684                 #loaded_val * #Hload_val
    493685                 whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
    494686                 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'
     687                 #Hload_success
     688                 cases (Hmatching … Hload_success) #val'
    497689                 * #Hlookup_in_cm #Hvalue_eq %{val'}
    498690                 cases Hyp_present
     
    500692                 (* seems ok *)
    501693            ]
    502        ]
     694       ]       
    503695  | 2: (* Deref case. Reduce the deref, exhibit the underlying load. *)
    504696       cases (bind_inversion ????? Hcl_success) -Hcl_success
Note: See TracChangeset for help on using the changeset viewer.