Changeset 2598


Ignore:
Timestamp:
Jan 31, 2013, 12:56:03 PM (6 years ago)
Author:
garnier
Message:

Tentative, partial draft for the definition of Clight-Cminor simulation for statements. Commented out for now.
Also, some stuff on memory injections, and some more aliases on abstract.ma.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/abstract.ma

    r2554 r2598  
    4646
    4747definition cl_eval_expr ≝ eval_expr.
     48
     49definition ClState ≝ State.
  • src/Clight/memoryInjections.ma

    r2594 r2598  
    579579qed.
    580580
     581(* A valid pointer stays valid after an alloc *)
     582(*
     583lemma alloc_valid_pointer_conservation :
     584  ∀m,m',z1,z2,r,new_block.
     585  alloc m z1 z2 r = 〈m', new_block〉 →
     586  ∀p. valid_pointer m p = true → valid_pointer m' p = true.
     587#m #m' #z1 #z2 #r * #new_block #Hregion_eq #Halloc
     588#p #Hvalid @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid)
     589-Hvalid lapply Halloc -Halloc cases m #cont #next #Hnext
     590whd in ⊢ ((??%%) → ?);
     591#Heq destruct (Heq) * * #Hblock_id
     592>unfold_low_bound >unfold_high_bound
     593>unfold_low_bound >unfold_high_bound
     594whd in match (update_block ?????);
     595whd in match (update_block ?????);
     596#HA #HB % [ % [ /2 by Zlt_to_Zle_to_Zlt/ ] ]
     597@(eq_block_elim … (pblock p) (mk_block r next))
     598[ 1,3: cases p in Hblock_id; #b #o #H #Heq destruct
     599       @False_ind
     600       @(absurd … H (irreflexive_Zlt ?))
     601| *: #Hneq normalize nodelta try assumption ]
     602qed.*)
     603
     604
     605lemma Zle_split :
     606  ∀a,b:Z. a ≤ b → a ≠ b → a <  b.
     607#a #b elim a elim b try /2/
     608#p1 #p2 #Hle #Hneq whd
     609@not_eq_to_le_to_lt
     610try // % #Heq destruct cases Hneq #H @H @refl
     611qed. 
     612
     613lemma alloc_valid_pointer_conservation :
     614  ∀m,m',z1,z2,r,new_block.
     615  alloc m z1 z2 r=〈m',new_block〉 →
     616  ∀p. (pblock p) ≠ (pi1 … new_block) →
     617      block_region (pblock p) = block_region (pi1 … new_block) →
     618      valid_pointer m' p = true →
     619      valid_pointer m p = true.
     620#m #m' #z1 #z2 #r * #new_block #Hregion
     621cases m #cont #next #Hnext
     622whd in ⊢ ((??%%) → ?);
     623#Heq destruct (Heq) * #b #o #Hneq #Hregion #Hvalid
     624@valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid)
     625-Hvalid
     626* * #Hblock_id
     627>unfold_low_bound >unfold_high_bound
     628>unfold_low_bound >unfold_high_bound
     629whd in match (update_block ?????);
     630whd in match (update_block ?????);
     631>(not_eq_block … Hneq) normalize nodelta
     632#HA #HB % [ % ] try assumption
     633cases b in Hneq Hregion Hblock_id; #r' #id * #Hnext_not_id #Hregion destruct
     634cut (next ≠ id)
     635[ % #H destruct @Hnext_not_id @refl ]
     636#Hneq #Hlt cut (id ≤ next)
     637[ /3 by monotonic_Zle_Zpred, Zlt_to_Zle/ ]
     638#Hle @Zle_split try @Hle @sym_neq @Hneq
     639qed.
     640
    581641(* Allocating a new zone produces a valid block. *)
    582642lemma alloc_valid_new_block :
     
    624684
    625685(* Memory allocation in m2 preserves [memory_inj].
    626  * This is lemma 43 from Leroy&Blazy. *)
     686 * This is lemma 66 from Leroy&Blazy. *)
    627687lemma alloc_memory_inj_m2 :
    628688  ∀E:embedding.
     
    693753 * of the allocation. *)
    694754
     755lemma block_neq_elim :
     756  ∀b1,b2. b1 ≠ b2 →
     757    (block_id b1 ≠ block_id b2 ∧ block_region b1 = block_region b2) ∨
     758    (block_id b1 = block_id b2 ∧ block_region b1 ≠ block_region b2) ∨
     759    (block_id b1 ≠ block_id b2 ∧ block_region b1 ≠ block_region b2).
     760* #r #id * #r' #id'
     761cases r cases r'
     762@(eqZb_elim …  id id')
     763#H1 #H2
     764[ 1,7: destruct @False_ind @(absurd … (refl ??) H2) ]
     765try /4 by or_introl, or_intror, conj/
     766destruct
     767[ %1 %2 @conj // % #H destruct
     768| %2 @conj try @H1 % #H destruct
     769| %1 %2 @conj // % #H destruct
     770| %2 @conj try @H1 % #H destruct ]
     771qed.
     772
    695773(* Allocating in m1 such that the resulting block has no image in m2 preserves
    696    the injection. This is lemma 44 for Leroy&Blazy. The proof should proceed as
     774   the injection. This is lemma 67 for Leroy&Blazy. The proof should proceed as
    697775   in Blazy & Leroy. Careful of using the mi_embedding hypothesis to rule out
    698776   absurd cases. *)
    699 axiom alloc_memory_inj_m1 :
     777lemma alloc_memory_inj_m1 :
    700778  ∀E:embedding.
    701779  ∀m1,m2,m1',z1,z2,r,new_block.
    702780  ∀H:memory_inj E m1 m2.
    703781  alloc m1 z1 z2 r = 〈m1', new_block〉 →
    704   E (pi1 … new_block) = None ? →
    705   memory_inj E m1' m2.
     782  memory_inj (λx. if eq_block x (pi1 … new_block) then None ? else E x) m1' m2 ∧
     783  embedding_compatible E (λx. if eq_block x (pi1 … new_block) then None ? else E x).
     784@cthulhu
     785qed. (* XXX finish this. *)
     786(* 
     787#E #m1 #m2 #m1' #z1 #z2 #r * #new_block #Hregion_eq #Hinj #Halloc
     788cut (E new_block = None ?)
     789[ @(mi_freeblock … Hinj) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj whd in ⊢ ((??%%) → ?);
     790  #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ]
     791#Hempty %
     792[ 2: whd #b @(eq_block_elim … b new_block) try // #Heq destruct (Heq) >Hempty %1 @refl ] 
     793%
     794[ whd #b1 #off1 #b2 #off2 #ty #v1
     795  @(eq_block_elim … b1 new_block)
     796  [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eq_block_b_b normalize nodelta
     797    #Habsurd destruct ]
     798  #Hneq #Hvalid
     799  whd in ⊢ ((??%?) → ?); >(not_eq_block … Hneq) normalize nodelta
     800  #Hembed cases (some_inversion ????? Hembed) * #b1' #off' * #Hembed
     801  normalize nodelta #Heq destruct (Heq)
     802  lapply (block_neq_elim … Hneq)
     803  *
     804  [ 2: * #Hid_neq #Hregion_neq
     805         lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) … Hneq)
     806*) 
     807     
    706808
    707809(* Embed a fresh block inside an unmapped portion of the target block.
    708  * This is the equivalent of lemma 45 for Leroy&Blazy. *)
     810 * This is the equivalent of lemma 68 for Leroy&Blazy. *)
    709811axiom alloc_memory_inj_m1_to_m2 :
    710812  ∀E:embedding.
     
    712814  ∀z1,z2:Z.
    713815  ∀b2,new_block.
    714   ∀delta:offset. 
    715   ∀H:memory_inj E m1 m2.
     816  ∀delta:offset.
     817  valid_block m2 b2 →
    716818  alloc m1 z1 z2 (block_region b2) = 〈m1', new_block〉 →
    717   E (pi1 … new_block) = Some ? 〈b2, delta〉 →
    718819  low_bound m2 b2 ≤ z1 + Zoo delta →
    719820  z2 + Zoo delta ≤ high_bound m2 b2 →
     
    722823                 high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨
    723824                 z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) →                 
    724   memory_inj E m1' m2.
     825  memory_inj E m1 m2 →
     826  memory_inj (λx. if eq_block x (pi1 … new_block) then Some ? 〈b2, delta〉 else E x) m1' m2.
    725827
    726828(* -------------------------------------- *)
  • src/Clight/toCminorCorrectness.ma

    r2597 r2598  
    235235
    236236
    237 (* This is the statement for expression simulation copied fro toCminorCorrectnessExpr.ma,
     237(* This is the statement for expression simulation copied from toCminorCorrectnessExpr.ma,
    238238   for easier reference.
    239239lemma eval_expr_sim :
     
    280280
    281281
    282 
     282(* TODO: relate Clight continuations and Cminor ones. *)
     283(*
     284axiom clight_cminor_cont_rel :
     285  clight_cminor_inv → cl_cont → cm_cont → block → stack → Prop.
     286
     287inductive clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop ≝
     288| CMR_normal :
     289  (* relates globals to globals and functions to functions *)
     290  ∀INV:  clight_cminor_inv.
     291
     292  (* ---- Clight variables ---- *)
     293  ∀cl_f: function.                               (* Clight enclosing function *) 
     294  ∀cl_s: statement.                                       (* Clight statement *) 
     295  ∀cl_k: cl_cont.                                      (* Clight continuation *)
     296  ∀cl_e: cl_env.                                        (* Clight environment *)
     297
     298  (* ---- Cminor variables ---- *) 
     299  ∀cl_m: mem.                                                (* Clight memory *)
     300  ∀cm_f: internal_function.                             (* enclosing function *)
     301  ∀cm_s: stmt.                                            (* Cminor statement *)
     302  ∀cm_k: cm_cont.                                       (* Cminor contiuation *)
     303  ∀cm_sp: block.                                      (* Cminor stack pointer *)
     304  ∀cm_st: stack.                                              (* Cminor stack *)
     305  ∀cm_e: cm_env.                                        (* Cminor environment *)
     306  ∀cm_m: mem.                                                (* Cminor memory *)
     307  ∀fInv: stmt_inv cm_f cm_e (f_body cm_f).               (* Cminor invariants *)
     308  ∀sInv: stmt_inv cm_f cm_e cm_s.
     309  ∀kInv: cont_inv cm_f cm_e cm_k.
     310
     311  (* ---- specify the mapping from variables to their alloc type (global, stack, register) ---- *)
     312  ∀alloctype:  var_types.                       (* map from var to alloc type *) 
     313  ∀stack_cons: ℕ.                              (* stack consumption of [cl_f] *)
     314  characterise_vars (globals INV) cl_f = 〈alloctype, stack_cons〉 →  (* spec of [alloctype] *)
     315
     316  (* ---- linking Clight and Cminor memories ---- *)
     317  ∀E: embedding.
     318  memory_inj E cl_m cm_m →
     319  memory_matching E cl_m cm_m cl_e cm_e INV cm_sp alloctype →
     320
     321  (* ---- specification of the contents of clight environment (needed for expr sim) ---- *)
     322  (* the two memories are those at function entry time. *)
     323  (∃m,m'. exec_alloc_variables empty_env m (fn_params cl_f @ fn_vars cl_f) = 〈cl_e,m'〉) → 
     324 
     325  (* ---- relate Clight and Cminor functions ---- *)
     326  ∀func_univ: universe SymbolTag.
     327  ∀Hfresh_globals: globals_fresh_for_univ ? (globals INV) func_univ.
     328  ∀Hfresh_function: fn_fresh_for_univ cl_f func_univ.
     329  translate_function func_univ (globals INV) cl_f Hfresh_globals Hfresh_function = OK ? cm_f →
     330
     331  (* ---- relate Clight and Cminor statements ---- *) 
     332  ∀stmt_univ: tmpgen alloctype.
     333  ∀lbl_univ:  labgen.
     334  ∀lbls:      lenv.
     335  ∀flag:      convert_flag.
     336  ∀outcome:   (Σsu:(tmpgen alloctype)×labgen×stmt.trans_inv alloctype lbls cl_s stmt_univ flag (opttyp_of_type (fn_return cl_f)) su).
     337  translate_statement alloctype stmt_univ lbl_univ lbls flag (opttyp_of_type (fn_return cl_f)) cl_s = OK ? outcome →
     338  (* TODO decompose outcome *)
     339
     340  (* ---- relate Clight continuation to Cminor continuation + stack pointer + stack ---- *)
     341  clight_cminor_cont_rel INV cl_k cm_k cm_sp cm_st →
     342   
     343  clight_cminor_rel INV
     344    (ClState cl_f cl_s cl_k cl_e cl_m)
     345    (CmState cm_f cm_s cm_e fInv sInv cm_m cm_sp cm_k kInv cm_st).
     346*)
    283347
    284348axiom clight_cminor_rel : clight_cminor_inv → Clight_state → Cminor_state → Prop.
  • src/Cminor/abstract.ma

    r2496 r2598  
    3636definition cm_eval_expr ≝ eval_expr.
    3737
     38definition CmState ≝ State.
     39
Note: See TracChangeset for help on using the changeset viewer.