Ignore:
Timestamp:
Feb 6, 2013, 1:01:34 PM (7 years ago)
Author:
garnier
Message:

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminorCorrectnessExpr.ma

    r2601 r2608  
    3636      | Some cl_blo ⇒
    3737        (* global symbols are mapped to themselves. Perhaps too strong. *)
    38         E (block_id cl_blo) = Some ? 〈cl_blo, zero_offset〉
     38        E cl_blo = Some ? 〈cl_blo, zero_offset〉
    3939      ]
    4040    | Some cl_blo ⇒
     
    4444            match vtype with
    4545            [ Stack n ⇒
    46               E (block_id cl_blo) = Some ? 〈sp, mk_offset (repr I16 n)〉
     46              E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉
    4747            | Local ⇒
    4848              ∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
     
    9898| * #id' #ty' #tl #Hind #env #env' #var * #m * #m'
    9999  whd in ⊢ ((??%?) → ? → ?);
    100   cases (alloc m 0 (sizeof ty') XData) #m0 * #b #Hregion
     100  cases (alloc m 0 (sizeof ty') (*XData*)) #m0 #b (* #Hregion *)
    101101  normalize nodelta #Hexec #Hlookup
    102102  lapply (Hind …  (ex_intro … (ex_intro … Hexec)) Hlookup)
    103103  cases env #env cases id' #id' cases var #var normalize
    104104  @(eqb_elim … id' var)
    105   [ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
     105  [ 2: #Hneq * #Hlookup' #Hexists'
     106       lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
    106107       #Heq <Heq @conj try @Hlookup' % *
    107108       [ #Heq' destruct (Heq') cases Hneq #H @H @refl
     
    364365     destruct (Hexec_alloc) %1 @Hlookup
    365366| 2: * #id #ty #tail #Hind
    366      #init_env #env #var #clb #m #m' #Hlookup     
     367     #init_env #env #var #clb #m #m' #Hlookup
    367368     whd in ⊢ (??%? → ?);
    368      cases (alloc m 0 (sizeof ty) XData) #m0 * #blo #Hreg normalize nodelta
     369     cases (alloc m 0 (sizeof ty) (*XData*)) #m0 #blo normalize nodelta
    369370     #Hexec_alloc
    370371     @(match identifier_eq ? id var with [ inl Heq ⇒ ? | inr Hneq ⇒ ? ])
     
    22122213       @conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
    22132214       %4 whd in Hptr_translate:(??%?) ⊢ (??%?);
    2214        cases (E (block_id cl_blo)) in Hptr_translate; normalize nodelta
     2215       cases (E cl_blo) in Hptr_translate; normalize nodelta
    22152216       [ #H destruct (H) ]
    22162217       * #BL #OFF normalize nodelta #Heq destruct (Heq)
Note: See TracChangeset for help on using the changeset viewer.