Ignore:
Timestamp:
Mar 31, 2013, 10:01:42 PM (6 years ago)
Author:
campbell
Message:

Switch removal and labelling combined.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r3046 r3047  
    429429
    430430let rec program_switch_removal (p : clight_program) : clight_program ≝
    431  let prog_funcs ≝ prog_funct ?? p in
    432  let sf_funcs   ≝ map ?? (λcl_fundef.
    433     let 〈fun_id, fun_def〉 ≝ cl_fundef in
    434     〈fun_id, fundef_switch_removal fun_def〉
    435   ) prog_funcs in
    436  mk_program ??
    437   (prog_vars … p)
    438   sf_funcs
    439   (prog_main … p).
     431  transform_program ??? p (λ_. fundef_switch_removal).
    440432
    441433(* -----------------------------------------------------------------------------
     
    19201912      (Kcall r (\fst (function_switch_removal f)) en' k').
    19211913
    1922 record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
    1923   rg_find_symbol: ∀s.
    1924     find_symbol ? ge s = find_symbol ? ge' s;
    1925   rg_find_funct_id: ∀v,f,id.
    1926     find_funct_id ? ge v = Some ? 〈f,id〉 →
    1927     find_funct_id ? ge' v = Some ? 〈t f,id〉;
    1928   rg_find_funct_ptr: ∀b,f.
    1929     find_funct_ptr ? ge b = Some ? f →
    1930     find_funct_ptr ? ge' b = Some ? (t f)
    1931 }.
    1932 
    19331914inductive switch_state_sim (ge : genv) : state → state → Prop ≝
    19341915| sws_state :
     
    22142195lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,writeable,ext.
    22152196  ∀Hext:sr_memext m1 m2 writeable.
    2216   switch_removal_globals ? fundef_switch_removal ge ge' →
     2197  related_globals … fundef_switch_removal ge ge' →
    22172198  disjoint_extension en1 en2 ext →
    22182199(*  disjoint_extension en1 en2 ext Hext → *)
     
    27502731theorem switch_removal_correction :
    27512732  ∀ge,ge'.
    2752   switch_removal_globals ? fundef_switch_removal ge ge' →
     2733  related_globals … fundef_switch_removal ge ge' →
    27532734  ∀s1,s1',tr,s2.
    27542735  switch_state_sim ge s1 s1' →
     
    32593240   | *: @cthulhu ]
    32603241 | *: @cthulhu ] qed.
     3242
     3243
     3244lemma initial_state_in_switch_simulation : ∀p,s.
     3245  make_initial_state p = OK ? s →
     3246  ∃s'.
     3247    make_initial_state (program_switch_removal p) = OK ? s' ∧
     3248    related_globals … fundef_switch_removal (make_global p) (make_global (program_switch_removal p)) ∧
     3249    switch_state_sim (make_global p) s s'.
     3250* #vars #fns #main #s
     3251whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
     3252cases (bind_inversion ????? EX) -EX #m * #Em #EX
     3253cases (bind_inversion ????? EX) -EX #b * #Emain #EX
     3254cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
     3255whd in EX:(??%%); destruct
     3256whd in match (make_initial_state ?);
     3257letin ge' ≝ (make_global ?)
     3258cut (related_globals … fundef_switch_removal ge ge')
     3259[ // ] #RG
     3260lapply (rg_find_funct_ptr … RG … Emain') #FFP
     3261% [2: %
     3262[ %
     3263 [whd in ⊢ (??%?);
     3264  change with (transform_program ??? (mk_program …) (λ_.?)) in match (mk_program ??? (transf_program ????) ?);
     3265  >(init_mem_transf … (mk_program ?? vars fns main)) >Em in ⊢ (??%?);
     3266  whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
     3267  whd in ⊢ (??%?); >FFP in ⊢ (??%?);
     3268  whd in ⊢ (??%?); @refl
     3269| /3/
     3270] | /3/ ] | skip ]
     3271qed.
     3272
     3273lemma switch_final_related : ∀ge1,s1,s2.
     3274  switch_state_sim ge1 s1 s2 →
     3275  is_final s1 = is_final s2.
     3276#Xge #Xs1 #Xs2 * //
     3277qed.
     3278
Note: See TracChangeset for help on using the changeset viewer.