Changeset 3049


Ignore:
Timestamp:
Apr 1, 2013, 12:06:08 AM (4 years ago)
Author:
campbell
Message:

Globalenvs and initial states for cast simplification.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r3048 r3049  
    18901890.
    18911891
    1892 record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
    1893   rg_find_symbol: ∀s.
    1894     find_symbol ? ge s = find_symbol ? ge' s;
    1895   rg_find_funct: ∀v,f,id.
    1896     find_funct_id ? ge v = Some ? 〈f,id〉 →
    1897     find_funct_id ? ge' v = Some ? 〈t f,id〉;
    1898   rg_find_funct_ptr: ∀b,f.
    1899     find_funct_ptr ? ge b = Some ? f →
    1900     find_funct_ptr ? ge' b = Some ? (t f)
    1901 }.
    1902 
    19031892(* The return type of any function is invariant under cast simplification *)
    19041893lemma fn_return_simplify : ∀f. fn_return (simplify_function f) = fn_return f.
     
    19141903] qed.
    19151904
    1916 lemma sim_related_globals : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' →
     1905lemma sim_related_globals : ∀ge,ge',en,m. related_globals simplify_fundef ge ge' →
    19171906  (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧
    19181907  (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)).
     
    19361925     cases (lookup SymbolTag block en v) normalize nodelta
    19371926     [ 2: #block @SimOk //
    1938      | 1: elim Hrelated #Hsymbol #_ #_ >(Hsymbol v) @SimOk //
     1927     | 1: >(rg_find_symbol … Hrelated … v) @SimOk //
    19391928     ]
    19401929| 4: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);
     
    20642053
    20652054lemma related_globals_expr_simulation : ∀ge,ge',en,m.
    2066   related_globals ? simplify_fundef ge ge' →
     2055  related_globals simplify_fundef ge ge' →
    20672056  ∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧
    20682057      typeof e = typeof (simplify_e e).
     
    20802069
    20812070lemma related_globals_lvalue_simulation : ∀ge,ge',en,m.
    2082   related_globals ? simplify_fundef ge ge' →
     2071  related_globals simplify_fundef ge ge' →
    20832072  ∀e. res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧
    20842073      typeof e = typeof (simplify_e e).
     
    20992088
    21002089lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
    2101 related_globals ? simplify_fundef ge ge' →
     2090related_globals simplify_fundef ge ge' →
    21022091∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)).
    21032092#ge #ge' #en #m #Hrelated #args
     
    24062395
    24072396theorem cast_correction : ∀ge, ge'.
    2408   related_globals ? simplify_fundef ge ge' →
     2397  related_globals simplify_fundef ge ge' →
    24092398  ∀s1, s1', tr, s2.
    24102399  state_cast s1 s1' →
     
    25552544                        | 1: #l -Hsim #Hsim lapply (Hsim l (refl ? (OK ? l))) #Heq >Heq
    25562545                             whd in match (bindIO ??????) in ⊢ (% → %);
    2557                              elim Hrelated #_ #Hfunct #_ lapply (Hfunct (\fst a))
     2546                             lapply (rg_find_funct_id … Hrelated … (\fst a))
    25582547                             cases (find_funct_id clight_fundef ge (\fst a));
    25592548                             [ 1: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
     
    28722861     #Habsurd destruct (Habsurd)
    28732862] qed.
     2863
     2864lemma initial_state_casts : ∀p,s.
     2865  make_initial_state p = OK ? s →
     2866  ∃s'.
     2867    make_initial_state (simplify_program p) = OK ? s' ∧
     2868    related_globals … simplify_fundef (make_global p) (make_global (simplify_program p)) ∧
     2869    state_cast s s'.
     2870* #vars #fns #main #s
     2871whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
     2872cases (bind_inversion ????? EX) -EX #m * #Em #EX
     2873cases (bind_inversion ????? EX) -EX #b * #Emain #EX
     2874cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
     2875whd in EX:(??%%); destruct
     2876whd in match (make_initial_state ?);
     2877letin ge' ≝ (make_global ?)
     2878cut (related_globals … simplify_fundef ge ge')
     2879[ // ] #RG
     2880lapply (rg_find_funct_ptr … RG … Emain') #FFP
     2881% [2: %
     2882[ %
     2883 [whd in ⊢ (??%?);
     2884  change with (transform_program ??? (mk_program …) (λ_.?)) in match (mk_program ??? (transf_program ????) ?);
     2885  >(init_mem_transf … (mk_program ?? vars fns main)) >Em in ⊢ (??%?);
     2886  whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
     2887  whd in ⊢ (??%?); >FFP in ⊢ (??%?);
     2888  whd in ⊢ (??%?); @refl
     2889| /3/
     2890] | /3/ ] | skip ]
     2891qed.
     2892
     2893
Note: See TracChangeset for help on using the changeset viewer.