Changeset 498


Ignore:
Timestamp:
Feb 11, 2011, 4:45:36 PM (6 years ago)
Author:
campbell
Message:

Make block type a little more abstract; remove knowledge about the old
representation for a pointer from the evaluation of lvalues.

Location:
Deliverables/D3.1/C-semantics
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Cexec.ma

    r496 r498  
    184184
    185185definition load_value_of_type' ≝
    186 λty,m,l. match l with [ pair pl ofs ⇒ match pl with [ pair r loc ⇒
    187   load_value_of_type ty m r loc ofs ] ].
     186λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ].
    188187
    189188(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
     
    210209      OK ? 〈v,tr〉
    211210  | Eaddrof a ⇒
    212       do 〈plo,tr〉 ← exec_lvalue ge en m a;
    213       OK ? 〈match plo with [ pair pl ofs ⇒ match pl with [ pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉
     211      do 〈lo,tr〉 ← exec_lvalue ge en m a;
     212      match ty with
     213      [ Tpointer r _ ⇒ OK ? 〈match lo with [ pair loc ofs ⇒  Vptr r loc ofs ], tr〉
     214      | _ ⇒ Error ?
     215      ]
    214216  | Esizeof ty' ⇒ OK ? 〈Vint (repr (sizeof ty')), E0〉
    215217  | Eunop op a ⇒
     
    254256  ]
    255257]
    256 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (region × block × int × trace) ≝
     258and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × int × trace) ≝
    257259  match e' with
    258260  [ Evar id ⇒
    259261      match (get … id en) with
    260       [ None ⇒ do 〈r,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈r,〈r,l〉〉,zero〉,E0〉 (* global *)
    261       | Some loc ⇒ OK ? 〈〈〈Any,loc〉,zero〉,E0〉 (* local *)
     262      [ None ⇒ do l ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈l,zero〉,E0〉 (* global *)
     263      | Some loc ⇒ OK ? 〈〈loc,zero〉,E0〉 (* local *)
    262264      ]
    263265  | Ederef a ⇒
    264266      do 〈v,tr〉 ← exec_expr ge en m a;
    265267      match v with
    266       [ Vptr sp l ofs ⇒ OK ? 〈〈〈sp,l〉,ofs〉,tr〉
     268      [ Vptr _ l ofs ⇒ OK ? 〈〈l,ofs〉,tr〉
    267269      | _ ⇒ Error ?
    268270      ]
     
    270272      match (typeof a) with
    271273      [ Tstruct id fList ⇒
    272           do 〈plofs,tr〉 ← exec_lvalue ge en m a;
     274          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
    273275          do delta ← field_offset i fList;
    274           OK ? 〈〈\fst plofs,add (\snd plofs) (repr delta)〉,tr〉
     276          OK ? 〈〈\fst lofs,add (\snd lofs) (repr delta)〉,tr〉
    275277      | Tunion id fList ⇒
    276           do 〈plofs,tr〉 ← exec_lvalue ge en m a;
    277           OK ? 〈plofs,tr〉
     278          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
     279          OK ? 〈lofs,tr〉
    278280      | _ ⇒ Error ?
    279281      ]
    280282  | _ ⇒ Error ?
    281283  ]
    282 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (region × block × int × trace) ≝
     284and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × int × trace) ≝
    283285match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
    284286
     
    323325      | cons v1 vl ⇒
    324326          do b ← opt_to_res ? (get … id e);
    325           do m1 ← opt_to_res ? (store_value_of_type ty m Any b zero v1);
     327          do m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);
    326328          exec_bind_parameters e m1 params' vl
    327329      ]
     
    495497definition store_value_of_type' ≝
    496498λty,m,l,v.
    497 match l with [ pair pl ofs ⇒
    498   match pl with [ pair pcl loc ⇒
    499     store_value_of_type ty m pcl loc ofs v ] ].
     499match l with [ pair loc ofs ⇒
     500  store_value_of_type ty m loc ofs v ].
    500501
    501502let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
     
    518519         | Some lhs' ⇒
    519520           ! locofs ← exec_lvalue ge e m lhs';
    520            ret ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k)
     521           ret ? (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k)
    521522         ];
    522523    ret ? 〈E0, Callstate fd vargs k' m〉)
  • Deliverables/D3.1/C-semantics/CexecComplete.ma

    r496 r498  
    118118
    119119(* Use to narrow down the choice of expression to just the lvalues. *)
    120 lemma lvalue_expr: ∀ge,env,m,e,ty,sp,l,ofs,tr. ∀P:expr_descr → Prop.
    121   eval_lvalue ge env m (Expr e ty) sp l ofs tr →
     120lemma lvalue_expr: ∀ge,env,m,e,ty,l,ofs,tr. ∀P:expr_descr → Prop.
     121  eval_lvalue ge env m (Expr e ty) l ofs tr →
    122122  (∀id. P (Evar id)) → (∀e'. P (Ederef e')) → (∀e',id. P (Efield e' id)) →
    123123  P e.
    124 #ge #env #m #e #ty #sp #l #ofs #tr #P #H @(eval_lvalue_inv_ind … H)
     124#ge #env #m #e #ty #l #ofs #tr #P #H @(eval_lvalue_inv_ind … H)
    125125[ #id #l #ty #e1 #e2 #e3 #e4 #e5 #e6 destruct; //
    126126| #id #sp #l #ty #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
    127127| #e #ty #sp #l #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; //
    128 | #e #id #ty #sp #l #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
    129 | #e #id #ty #sp #l #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
     128| #e #id #ty #l #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
     129| #e #id #ty #l #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
    130130] qed.
    131131
     
    159159lemma expr_lvalue_complete: ∀ge,env,m.
    160160(∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉)) ∧
    161 (∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yields ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)).
     161(∀e,l,off,tr. eval_lvalue ge env m e l off tr → yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)).
    162162#ge #env #m
    163163@(combined_expr_lvalue_ind ge env m
    164164  (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
    165   (λe,sp,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)));
     165  (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)));
    166166[ #i #ty @refl
    167167| #f #ty @refl
    168 | #e #ty #sp #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
     168| #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
    169169    [ #id | #e' | #e' #id ] #H3
    170170    whd in ⊢ (??%?);
     
    224224  (* lvalues *)
    225225| #id #l #ty #e1 whd in ⊢ (??%?); >e1 @refl
    226 | #id #sp #l #ty #e1 #e2 whd in ⊢ (??%?); >e1
     226| #id #l #ty #e1 #e2 whd in ⊢ (??%?); >e1
    227227    >e2 @refl
    228 | #e #ty #sp #l #ofs #tr #H1 #H2 whd in ⊢ (??%?);
     228| #e #ty #r #l #ofs #tr #H1 #H2 whd in ⊢ (??%?);
    229229    >(yields_eq ??? H2)
    230230    @refl
    231 | #e #i #ty #sp #l #ofs #id #fList #delta #tr #H1 #H2 #H3 #H4 cases e in H2 H4 ⊢ %;
     231| #e #i #ty #l #ofs #id #fList #delta #tr #H1 #H2 #H3 #H4 cases e in H2 H4 ⊢ %;
    232232    #e' #ty' #H2 whd in H2:(??%?); >H2 #H4 whd in ⊢ (??%?);
    233233    >(yields_eq ??? H4) whd in ⊢ (??%?);
    234234    >H3 @refl
    235 | #e #i #ty #sp #l #ofs #id #fList #tr cases e; #e' #ty' #H1 #H2
     235| #e #i #ty #l #ofs #id #fList #tr cases e; #e' #ty' #H1 #H2
    236236    whd in H2:(??%?); >H2 #H3 whd in ⊢ (??%?);
    237237    >(yields_eq ??? H3) @refl
     
    253253
    254254theorem lvalue_complete: ∀ge,env,m.
    255  ∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yields ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉).
     255 ∀e,l,off,tr. eval_lvalue ge env m e l off tr → yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉).
    256256#ge #env #m elim (expr_lvalue_complete ge env m); /2/; qed.
    257257
     
    363363  step ge s tr s' → yieldsIO ? (exec_step ge s) 〈tr,s'〉.
    364364#ge #s #tr #s' #H elim H;
    365 [ #f #e #e1 #k #e2 #m #sp #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?);
     365[ #f #e #e1 #k #e2 #m #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?);
    366366    >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?);
    367367    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
     
    373373    >H4 elim (assert_type_eq_true (fun_typeof e)); #pty #ety >ety
    374374    @refl
    375 | #f #el #ef #eargs #k #env #m #sp #loc #ofs #vf #vargs #f' #tr1 #tr2 #tr3 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
     375| #f #el #ef #eargs #k #env #m #loc #ofs #vf #vargs #f' #tr1 #tr2 #tr3 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
    376376    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
    377377    >(yields_eq ??? (exprlist_complete … H3)) whd in ⊢ (??%?);
     
    455455    @refl
    456456| #v #f #env #k #m @refl
    457 | #v #f #env #k #m1 #m2 #sp #loc #ofs #ty #H whd in ⊢ (??%?);
     457| #v #f #env #k #m1 #m2 #loc #ofs #ty #H whd in ⊢ (??%?);
    458458    >H @refl
    459459| #f #l #s #k #env #m @refl
  • Deliverables/D3.1/C-semantics/CexecSound.ma

    r496 r498  
    177177theorem exec_expr_sound: ∀ge:genv. ∀en:env. ∀m:mem. ∀e:expr.
    178178(P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
    179 #ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
     179#ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
    180180(* XXX // fails [ 1,2: #ty #c whd //  *)
    181181[ #ty #c whd %
     
    194194    | #loc #eget @(eval_Evar_local … eget)
    195195    ]
    196 | #ty #e #He whd in ⊢ (???%);
    197     @bind2_OK #v cases v; //; #sp #l #ofs #tr #Hv whd;
    198     @eval_Ederef >Hv in He #He @He
     196| #ty #e #He whd in ⊢ (???%)
     197    @bind2_OK #v cases v // #r #l #ofs #tr #Hv whd
     198    @eval_Ederef [ 2: >Hv in He #He @He | skip ]
    199199| #ty #e'' #ty'' #He'' @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
    200     whd; @eval_Eaddrof >H in He'' #He'' @He''
     200  cases ty // #r #pty
     201    whd @eval_Eaddrof >H in He'' #He'' @He''
    201202| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
    202203    @opt_bind_OK #v #ev
     
    259260] qed.
    260261
    261 lemma addrof_eval_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
    262 eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr sp loc off) tr →
    263 eval_lvalue ge en m e sp loc off tr.
    264 #ge #en #m #e #sp #loc #off #tr #ty #H inversion H;
     262lemma addrof_eval_lvalue: ∀ge,en,m,e,r,loc,off,tr,ty.
     263eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr r loc off) tr →
     264eval_lvalue ge en m e loc off tr.
     265#ge #en #m #e #r #loc #off #tr #ty #H inversion H;
    265266[ 1,2,5: #a #b #H @False_ind destruct (H);
    266 | #a #b #c #d #e #f #g #H1 #i #H2 <H2 in H1 #H1 @False_ind
     267| #a #b #c #d #e #f #H1 #g #H2 <H2 in H1 #H1 @False_ind
    267268    @(eval_lvalue_inv_ind … H1)
    268269    [ #a #b #c #d #bad destruct (bad);
    269     | #a #b #c #d #e #f #bad destruct (bad);
     270    | #a #b #c #d #e #bad destruct (bad);
    270271    | #a #b #c #d #e #f #g #bad destruct (bad);
    271     | #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad @False_ind destruct (bad);
    272     | #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad);
    273     ]
    274 | #e' #ty' #sp' #loc' #ofs' #tr' #H #e1 #e2 #e3 destruct (e1 e2 e3); @H
     272    | #a #b #c #d #e #f #g #h #i #j #k #l #m #bad @False_ind destruct (bad);
     273    | #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
     274    ]
     275| #e' #ty' #loc' #ofs' #v #tr' #H #e1 #e2 #e3 destruct (e1 e2 e3); @H
    275276| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
    276277| #a #b #c #d #e #f #g #h #i #j #k #l #k #l #bad destruct (bad);
     
    285286] qed.
    286287
    287 lemma addrof_exec_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
    288 exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉 →
    289 exec_expr ge en m (Expr (Eaddrof e) ty) = OK ? 〈Vptr sp loc off, tr〉.
    290 #ge #en #m #e #sp #loc #off #tr #ty #H whd in ⊢ (??%?);
    291 >H //;
     288lemma addrof_exec_lvalue: ∀ge,en,m,e,r,loc,off,tr,ty.
     289exec_lvalue ge en m e = OK ? 〈〈loc,off〉,tr〉 →
     290exec_expr ge en m (Expr (Eaddrof e) (Tpointer r ty)) = OK ? 〈Vptr r loc off, tr〉.
     291#ge #en #m #e #r #loc #off #tr #ty #H whd in ⊢ (??%?)
     292>H //
    292293qed.
    293294
    294295theorem exec_lvalue_sound: ∀ge,en,m,e.
    295 P_res ? (λr.eval_lvalue ge en m e (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) (exec_lvalue ge en m e).
     296P_res ? (λr.eval_lvalue ge en m e (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue ge en m e).
    296297#ge #en #m #e lapply (refl ? (exec_lvalue ge en m e));
    297298cases (exec_lvalue ge en m e) in ⊢ (???% → %);
    298 [ #x cases x; #y cases y; #z cases z; #sp #loc #off #tr #H whd;
    299     @(addrof_eval_lvalue … Tvoid)
    300     lapply (addrof_exec_lvalue … Tvoid H); #H'
    301     lapply (exec_expr_sound ge en m (Expr (Eaddrof e) Tvoid));
     299[ #x cases x #y cases y #loc #off #tr #H whd
     300    @(addrof_eval_lvalue … Any … (Tpointer Any Tvoid))
     301    lapply (addrof_exec_lvalue … Any … (Tpointer Any Tvoid) H) #H'
     302    lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer Any Tvoid)))
    302303    >H' #H'' @H''
    303 | #_ whd; @I
     304| #_ whd @I
    304305] qed.
    305306
     
    310311  P_res_to_P ???? (exec_expr_sound ge en m e) H.
    311312
    312 definition exec_lvalue_sound' ≝ λge,en,m,e,sp,loc,off,tr.
    313   λH:exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉.
     313definition exec_lvalue_sound' ≝ λge,en,m,e,loc,off,tr.
     314  λH:exec_lvalue ge en m e = OK ? 〈〈loc,off〉,tr〉.
    314315  P_res_to_P ???? (exec_lvalue_sound ge en m e) H.
    315316
  • Deliverables/D3.1/C-semantics/Csem.ma

    r496 r498  
    464464  reference, the pointer [Vptr b ofs] is returned. *)
    465465
    466 let rec load_value_of_type (ty: type) (m: mem) (psp:region) (b: block) (ofs: int) : option val ≝
     466let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: int) : option val ≝
    467467  match access_mode ty with
    468   [ By_value chunk ⇒ loadv chunk m (Vptr psp b ofs)
    469   | By_reference ⇒ Some ? (Vptr psp b ofs)
     468  [ By_value chunk ⇒ loadv chunk m (Vptr Any b ofs)
     469  | By_reference r ⇒ Some ? (Vptr r b ofs)
    470470  | By_nothing ⇒ None ?
    471471  ].
     
    476476  This is allowed only if [ty] indicates an access by value. *)
    477477
    478 let rec store_value_of_type (ty_dest: type) (m: mem) (psp:region) (loc: block) (ofs: int) (v: val) : option mem ≝
     478let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) (v: val) : option mem ≝
    479479  match access_mode ty_dest with
    480   [ By_value chunk ⇒ storev chunk m (Vptr psp loc ofs) v
    481   | By_reference ⇒ None ?
     480  [ By_value chunk ⇒ storev chunk m (Vptr Any loc ofs) v
     481  | By_reference _ ⇒ None ?
    482482  | By_nothing ⇒ None ?
    483483  ].
     
    516516      ∀e,m,id,ty,params,v1,vl,b,m1,m2.
    517517      get ??? id e = Some ? b →
    518       store_value_of_type ty m Any b zero v1 = Some ? m1 →
     518      store_value_of_type ty m b zero v1 = Some ? m1 →
    519519      bind_parameters e m1 params vl m2 →
    520520      bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2.
    521 
    522 (* XXX: this doesn't look right - we're assigning arbitrary memory spaces to
    523    parameters? *)
    524521
    525522(* * Return the list of blocks in the codomain of [e]. *)
     
    567564  | eval_Econst_float:   ∀f,ty.
    568565      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0
    569   | eval_Elvalue: ∀a,ty,r,loc,ofs,v,tr.
    570       eval_lvalue ge e m (Expr a ty) r loc ofs tr →
    571       load_value_of_type ty m r loc ofs = Some ? v →
     566  | eval_Elvalue: ∀a,ty,loc,ofs,v,tr.
     567      eval_lvalue ge e m (Expr a ty) loc ofs tr →
     568      load_value_of_type ty m loc ofs = Some ? v →
    572569      eval_expr ge e m (Expr a ty) v tr
    573570  | eval_Eaddrof: ∀a,ty,r,loc,ofs,tr.
    574       eval_lvalue ge e m a r loc ofs tr →
    575       eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr r loc ofs) tr
     571      eval_lvalue ge e m a loc ofs tr →
     572      eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc ofs) tr
    576573  | eval_Esizeof: ∀ty',ty.
    577574      eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0
     
    628625  be representable in a pointer of region r. *)
    629626
    630 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → region → block → int → trace → Prop ≝
     627with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → int → trace → Prop ≝
    631628  | eval_Evar_local:   ∀id,l,ty.
    632629      (* XXX notation? e!id*) get ??? id e = Some ? l →
    633       eval_lvalue ge e m (Expr (Evar id) ty) Any l zero E0
    634   | eval_Evar_global: ∀id,r,l,ty.
     630      eval_lvalue ge e m (Expr (Evar id) ty) l zero E0
     631  | eval_Evar_global: ∀id,l,ty.
    635632      (* XXX e!id *) get ??? id e = None ? →
    636       find_symbol ?? ge id = Some ? 〈r,l〉
    637       eval_lvalue ge e m (Expr (Evar id) ty) r 〈r,l〉 zero E0
     633      find_symbol ?? ge id = Some ? l
     634      eval_lvalue ge e m (Expr (Evar id) ty) l zero E0
    638635  | eval_Ederef: ∀a,ty,r,l,ofs,tr.
    639636      eval_expr ge e m a (Vptr r l ofs) tr →
    640       eval_lvalue ge e m (Expr (Ederef a) ty) r l ofs tr
    641  | eval_Efield_struct:   ∀a,i,ty,r,l,ofs,id,fList,delta,tr.
    642       eval_lvalue ge e m a r l ofs tr →
     637      eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr
     638    (* Aside: note that each block of memory is entirely contained within one
     639       memory region; hence adding a field offset will not produce a location
     640       outside of the original location's region. *)
     641 | eval_Efield_struct:   ∀a,i,ty,l,ofs,id,fList,delta,tr.
     642      eval_lvalue ge e m a l ofs tr →
    643643      typeof a = Tstruct id fList →
    644644      field_offset i fList = OK ? delta →
    645       eval_lvalue ge e m (Expr (Efield a i) ty) r l (add ofs (repr delta)) tr
    646  | eval_Efield_union:   ∀a,i,ty,r,l,ofs,id,fList,tr.
    647       eval_lvalue ge e m a r l ofs tr →
     645      eval_lvalue ge e m (Expr (Efield a i) ty) l (add ofs (repr delta)) tr
     646 | eval_Efield_union:   ∀a,i,ty,l,ofs,id,fList,tr.
     647      eval_lvalue ge e m a l ofs tr →
    648648      typeof a = Tunion id fList →
    649       eval_lvalue ge e m (Expr (Efield a i) ty) r l ofs tr.
     649      eval_lvalue ge e m (Expr (Efield a i) ty) l ofs tr.
    650650
    651651let rec eval_expr_ind (ge:genv) (e:env) (m:mem)
     
    653653  (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
    654654  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    655   (elv:∀a,ty,psp,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty psp loc ofs v tr H1 H2))
     655  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
    656656  (ead:∀a,ty,psp,loc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
    657657  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
     
    670670  [ eval_Econst_int i ty ⇒ eci i ty
    671671  | eval_Econst_float f ty ⇒ ecF f ty
    672   | eval_Elvalue a ty psp loc ofs v tr H1 H2 ⇒ elv a ty psp loc ofs v tr H1 H2
     672  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2
    673673  | eval_Eaddrof a ty psp loc ofs tr H ⇒ ead a ty psp loc ofs tr H
    674674  | eval_Esizeof ty' ty ⇒ esz ty' ty
     
    688688
    689689let rec eval_lvalue_ind (ge:genv) (e:env) (m:mem)
    690   (P:∀a,psp,loc,ofs,tr. eval_lvalue ge e m a psp loc ofs tr → Prop)
    691   (lvl:∀id,l,ty,H. P ????? (eval_Evar_local ge e m id l ty H))
    692   (lvg:∀id,sp,l,ty,H1,H2. P ????? (eval_Evar_global ge e m id sp l ty H1 H2))
    693   (lde:∀a,ty,psp,l,ofs,tr,H. P ????? (eval_Ederef ge e m a ty psp l ofs tr H))
    694   (lfs:∀a,i,ty,psp,l,ofs,id,fList,delta,tr,H1,H2,H3. P a psp l ofs tr H1 → P ????? (eval_Efield_struct ge e m a i ty psp l ofs id fList delta tr H1 H2 H3))
    695   (lfu:∀a,i,ty,psp,l,ofs,id,fList,tr,H1,H2. P a psp l ofs tr H1 → P ????? (eval_Efield_union ge e m a i ty psp l ofs id fList tr H1 H2))
    696   (a:expr) (psp:region) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a psp loc ofs tr) on ev : P a psp loc ofs tr ev ≝
     690  (P:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
     691  (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H))
     692  (lvg:∀id,l,ty,H1,H2. P ???? (eval_Evar_global ge e m id l ty H1 H2))
     693  (lde:∀a,ty,psp,l,ofs,tr,H. P ???? (eval_Ederef ge e m a ty psp l ofs tr H))
     694  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. P a l ofs tr H1 → P ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
     695  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. P a l ofs tr H1 → P ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
     696  (a:expr) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : P a loc ofs tr ev ≝
    697697  match ev with
    698698  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    699   | eval_Evar_global id sp l ty H1 H2 ⇒ lvg id sp l ty H1 H2
     699  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    700700  | eval_Ederef a ty psp l ofs tr H ⇒ lde a ty psp l ofs tr H
    701   | eval_Efield_struct a i ty psp l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty psp l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a psp l ofs tr H1)
    702   | eval_Efield_union a i ty psp l ofs id fList tr H1 H2 ⇒ lfu a i ty psp l ofs id fList tr H1 H2 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a psp l ofs tr H1)
     701  | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1)
     702  | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1)
    703703  ].
    704704
     
    712712    ∀x3: mem.
    713713     ∀x4: expr.
    714       ∀x5: region.
    715714       ∀x6: block.
    716715        ∀x7: int.
     
    718717          ∀P:
    719718            ∀_z1430: expr.
    720              ∀_z1429: region.
    721719              ∀_z1428: block. ∀_z1427: int. ∀_z1426: trace. Prop.
    722720           ∀_H1: ?.
     
    725723              ∀_H4: ?.
    726724               ∀_H5: ?.
    727                 ∀_Hterm: eval_lvalue x1 x2 x3 x4 x5 x6 x7 x8.
    728                  P x4 x5 x6 x7 x8
     725                ∀_Hterm: eval_lvalue x1 x2 x3 x4 x6 x7 x8.
     726                 P x4 x6 x7 x8
    729727:=
    730728  (λx1:genv.
     
    732730      (λx3:mem.
    733731        (λx4:expr.
    734           (λx5:region.
    735732            (λx6:block.
    736733              (λx7:int.
    737734                (λx8:trace.
    738735                  (λP:∀_z1430: expr.
    739                         ∀_z1429: region.
    740736                         ∀_z1428: block.
    741737                          ∀_z1427: int. ∀_z1426: trace. Prop.
     
    745741                          (λH4:?.
    746742                            (λH5:?.
    747                               (λHterm:eval_lvalue x1 x2 x3 x4 x5 x6 x7 x8.
     743                              (λHterm:eval_lvalue x1 x2 x3 x4 x6 x7 x8.
    748744                                ((λHcut:∀z1435: eq expr x4 x4.
    749                                           ∀z1434: eq region x5 x5.
    750745                                           ∀z1433: eq block x6 x6.
    751746                                            ∀z1432: eq int x7 x7.
    752747                                             ∀z1431: eq trace x8 x8.
    753                                               P x4 x5 x6 x7 x8.
     748                                              P x4 x6 x7 x8.
    754749                                   (Hcut (refl expr x4)
    755                                      (refl region x5) (refl block x6)
     750                                     (refl block x6)
    756751                                     (refl int x7) (refl trace x8)))
    757                                   ?)))))))))))))))).
    758 [ @(eval_lvalue_ind x1 x2 x3 (λa,psp,loc,ofs,tr,e. ∀e1:eq ? x4 a. ∀e2:eq ? x5 psp. ∀e3:eq ? x6 loc. ∀e4:eq ? x7 ofs. ∀e5:eq ? x8 tr. P a psp loc ofs tr) … Hterm)
     752                                  ?))))))))))))))).
     753[ @(eval_lvalue_ind x1 x2 x3 (λa,loc,ofs,tr,e. ∀e1:eq ? x4 a. ∀e3:eq ? x6 loc. ∀e4:eq ? x7 ofs. ∀e5:eq ? x8 tr. P a loc ofs tr) … Hterm)
    759754  [ @H1 | @H2 | @H3 | @H4 | @H5 ]
    760755| *: skip
     
    763758let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem)
    764759  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
    765   (Q:∀a,psp,loc,ofs,tr. eval_lvalue ge e m a psp loc ofs tr → Prop)
     760  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
    766761  (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
    767762  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    768   (elv:∀a,ty,psp,loc,ofs,v,tr,H1,H2. Q (Expr a ty) psp loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty psp loc ofs v tr H1 H2))
    769   (ead:∀a,ty,psp,loc,ofs,tr,H. Q a psp loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
     763  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
     764  (ead:∀a,ty,psp,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
    770765  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
    771766  (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
     
    779774  (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2))
    780775  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
    781   (lvl:∀id,l,ty,H. Q ????? (eval_Evar_local ge e m id l ty H))
    782   (lvg:∀id,sp,l,ty,H1,H2. Q ????? (eval_Evar_global ge e m id sp l ty H1 H2))
    783   (lde:∀a,ty,psp,l,ofs,tr,H. P a (Vptr psp l ofs) tr H → Q ????? (eval_Ederef ge e m a ty psp l ofs tr H))
    784   (lfs:∀a,i,ty,psp,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a psp l ofs tr H1 → Q ????? (eval_Efield_struct ge e m a i ty psp l ofs id fList delta tr H1 H2 H3))
    785   (lfu:∀a,i,ty,psp,l,ofs,id,fList,tr,H1,H2. Q a psp l ofs tr H1 → Q ????? (eval_Efield_union ge e m a i ty psp l ofs id fList tr H1 H2))
     776  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
     777  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
     778  (lde:∀a,ty,psp,l,ofs,tr,H. P a (Vptr psp l ofs) tr H → Q ???? (eval_Ederef ge e m a ty psp l ofs tr H))
     779  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
     780  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
    786781 
    787782  (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝
     
    789784  [ eval_Econst_int i ty ⇒ eci i ty
    790785  | eval_Econst_float f ty ⇒ ecF f ty
    791   | eval_Elvalue a ty psp loc ofs v tr H1 H2 ⇒ elv a ty psp loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) psp loc ofs tr H1)
    792   | eval_Eaddrof a ty psp loc ofs tr H ⇒ ead a ty psp loc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a psp loc ofs tr H)
     786  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) loc ofs tr H1)
     787  | eval_Eaddrof a ty psp loc ofs tr H ⇒ ead a ty psp loc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H)
    793788  | eval_Esizeof ty' ty ⇒ esz ty' ty
    794789  | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
     
    805800and eval_lvalue_ind2 (ge:genv) (e:env) (m:mem)
    806801  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
    807   (Q:∀a,psp,loc,ofs,tr. eval_lvalue ge e m a psp loc ofs tr → Prop)
     802  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
    808803  (eci:∀i,ty. P ??? (eval_Econst_int ge e m i ty))
    809804  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
    810   (elv:∀a,ty,psp,loc,ofs,v,tr,H1,H2. Q (Expr a ty) psp loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty psp loc ofs v tr H1 H2))
    811   (ead:∀a,ty,psp,loc,ofs,tr,H. Q a psp loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
     805  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
     806  (ead:∀a,ty,psp,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))
    812807  (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty))
    813808  (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
     
    821816  (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2))
    822817  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
    823   (lvl:∀id,l,ty,H. Q ????? (eval_Evar_local ge e m id l ty H))
    824   (lvg:∀id,sp,l,ty,H1,H2. Q ????? (eval_Evar_global ge e m id sp l ty H1 H2))
    825   (lde:∀a,ty,psp,l,ofs,tr,H. P a (Vptr psp l ofs) tr H → Q ????? (eval_Ederef ge e m a ty psp l ofs tr H))
    826   (lfs:∀a,i,ty,psp,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a psp l ofs tr H1 → Q ????? (eval_Efield_struct ge e m a i ty psp l ofs id fList delta tr H1 H2 H3))
    827   (lfu:∀a,i,ty,psp,l,ofs,id,fList,tr,H1,H2. Q a psp l ofs tr H1 → Q ????? (eval_Efield_union ge e m a i ty psp l ofs id fList tr H1 H2))
    828   (a:expr) (psp:region) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a psp loc ofs tr) on ev : Q a psp loc ofs tr ev ≝
     818  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
     819  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
     820  (lde:∀a,ty,psp,l,ofs,tr,H. P a (Vptr psp l ofs) tr H → Q ???? (eval_Ederef ge e m a ty psp l ofs tr H))
     821  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
     822  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
     823  (a:expr) (loc:block) (ofs:int) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : Q a loc ofs tr ev ≝
    829824  match ev with
    830825  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
    831   | eval_Evar_global id sp l ty H1 H2 ⇒ lvg id sp l ty H1 H2
     826  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
    832827  | eval_Ederef a ty psp l ofs tr H ⇒ lde a ty psp l ofs tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr psp l ofs) tr H)
    833   | eval_Efield_struct a i ty psp l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty psp l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a psp l ofs tr H1)
    834   | eval_Efield_union a i ty psp l ofs id fList tr H1 H2 ⇒ lfu a i ty psp l ofs id fList tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a psp l ofs tr H1)
     828  | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
     829  | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
    835830  ].
    836831
     
    881876  | Kswitch: cont -> cont
    882877       (**r catches [break] statements arising out of [switch] *)
    883   | Kcall: option (region × block × int × type) ->   (**r where to store result *)
     878  | Kcall: option (block × int × type) ->   (**r where to store result *)
    884879           function ->                      (**r calling function *)
    885880           env ->                           (**r local env of calling function *)
     
    995990inductive step (ge:genv) : state → trace → state → Prop ≝
    996991
    997   | step_assign:   ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m',tr1,tr2.
    998       eval_lvalue ge e m a1 psp loc ofs tr1 →
     992  | step_assign:   ∀f,a1,a2,k,e,m,loc,ofs,v2,m',tr1,tr2.
     993      eval_lvalue ge e m a1 loc ofs tr1 →
    999994      eval_expr ge e m a2 v2 tr2 →
    1000       store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' →
     995      store_value_of_type (typeof a1) m loc ofs v2 = Some ? m' →
    1001996      step ge (State f (Sassign a1 a2) k e m)
    1002997           (tr1⧺tr2) (State f Sskip k e m')
     
    10101005           (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m)
    10111006
    1012   | step_call_some:   ∀f,lhs,a,al,k,e,m,psp,loc,ofs,vf,vargs,fd,tr1,tr2,tr3.
    1013       eval_lvalue ge e m lhs psp loc ofs tr1 →
     1007  | step_call_some:   ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,tr1,tr2,tr3.
     1008      eval_lvalue ge e m lhs loc ofs tr1 →
    10141009      eval_expr ge e m a vf tr2 →
    10151010      eval_exprlist ge e m al vargs tr3 →
     
    10171012      type_of_fundef fd = fun_typeof a →
    10181013      step ge (State f (Scall (Some ? lhs) a al) k e m)
    1019            (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈〈psp, loc〉, ofs〉, typeof lhs〉) f e k) m)
     1014           (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)
    10201015
    10211016  | step_seq:  ∀f,s1,s2,k,e,m.
     
    11561151           E0 (State f Sskip k e m)
    11571152
    1158   | step_returnstate_1: ∀v,f,e,k,m,m',psp,loc,ofs,ty.
    1159       store_value_of_type ty m psp loc ofs v = Some ? m' →
    1160       step ge (Returnstate v (Kcall (Some ? 〈〈〈psp,loc〉, ofs〉, ty〉) f e k) m)
     1153  | step_returnstate_1: ∀v,f,e,k,m,m',loc,ofs,ty.
     1154      store_value_of_type ty m loc ofs v = Some ? m' →
     1155      step ge (Returnstate v (Kcall (Some ? 〈〈loc, ofs〉, ty〉) f e k) m)
    11611156           E0 (State f Sskip k e m')
    11621157           
  • Deliverables/D3.1/C-semantics/Csyntax.ma

    r487 r498  
    628628inductive mode: Type[0] ≝
    629629  | By_value: memory_chunk → mode
    630   | By_reference: mode
     630  | By_reference: region → mode
    631631  | By_nothing: mode.
    632632
     
    645645  | Tvoid ⇒ By_nothing
    646646  | Tpointer r _ ⇒ By_value (Mpointer r)
    647   | Tarray _ _ _ ⇒ By_reference
    648   | Tfunction _ _ ⇒ By_reference
     647  | Tarray r _ _ ⇒ By_reference r
     648  | Tfunction _ _ ⇒ By_reference Code
    649649  | Tstruct _ fList ⇒ By_nothing
    650650  | Tunion _ fList ⇒ By_nothing
  • Deliverables/D3.1/C-semantics/Globalenvs.ma

    r496 r498  
    341341definition add_funct : ∀F:Type[0]. (ident × F) → genv F → genv F ≝
    342342λF,name_fun,g.
    343   let b ≝ nextfunction ? g in
    344   mk_genv F ((*ZMap.set*) λb'. if eq_block 〈Code,b〉 b' then (Some ? (\snd name_fun)) else (functions ? g b'))
    345             (Zpred b)
    346             ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? 〈Code,b〉 | inr _ ⇒ (symbols ? g i) ]).
     343  let blk_id ≝ nextfunction ? g in
     344  let b ≝ mk_block Code blk_id in
     345  mk_genv F ((*ZMap.set*) λb'. if eq_block b b' then (Some ? (\snd name_fun)) else (functions ? g b'))
     346            (Zpred blk_id)
     347            ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? b | inr _ ⇒ (symbols ? g i) ]).
    347348
    348349definition add_symbol : ∀F:Type[0]. ident → block → genv F → genv F ≝
     
    403404     addresses of the memory region in question - here there are no real
    404405     pointers, so use the real region. *)
    405   let r ≝ \fst b in
     406  let r ≝ block_region m b in
    406407  match id with
    407408  [ Init_int8 n ⇒ store Mint8unsigned m r b p (Vint n)
     
    468469definition alloc_init_data : mem → list init_data → region → mem × block ≝
    469470  λm,i_data,r.
    470   〈mk_mem (update_block ? 〈r, nextblock m〉
     471  let b ≝ mk_block r (nextblock m) in
     472  〈mk_mem (update_block ? b
    471473                 (mk_block_contents OZ (size_init_data_list i_data) (λ_.Undef))
    472474                 (blocks m))
    473475         (Zsucc (nextblock m))
    474476         (succ_nextblock_pos m),
    475    〈r, nextblock m〉〉.
     477   b〉.
    476478
    477479(* init *)
  • Deliverables/D3.1/C-semantics/Mem.ma

    r497 r498  
    222222  mk_mem (λx.empty_block OZ OZ) (pos one) one_pos.
    223223
    224 definition nullptr: block ≝ 〈Any,OZ〉.
     224definition nullptr: block ≝ mk_block Any OZ.
    225225
    226226(* Allocation of a fresh block with the given bounds.  Return an updated
     
    237237
    238238definition alloc : mem → Z → Z → region → mem × block ≝
    239   λm,lo,hi,r.〈mk_mem
    240               (update_block … 〈r,nextblock m〉
    241                  (empty_block lo hi)
    242                  (blocks m))
    243               (Zsucc (nextblock m))
    244               (succ_nextblock_pos m),
    245             〈r,nextblock m〉〉.
     239  λm,lo,hi,r.
     240  let b ≝ mk_block r (nextblock m) in
     241  〈mk_mem
     242    (update_block … b
     243      (empty_block lo hi)
     244      (blocks m))
     245    (Zsucc (nextblock m))
     246    (succ_nextblock_pos m),
     247    b〉.
    246248
    247249(* Freeing a block.  Return the updated memory state where the given
     
    274276  λm,b.high (blocks m b).
    275277definition block_region: mem → block → region ≝
    276   λm,b.\fst b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *)
     278  λm,b.block_region b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *)
    277279
    278280(* A block address is valid if it was previously allocated. It remains valid
     
    281283(* TODO: should this check for region? *)
    282284definition valid_block : mem → block → Prop ≝
    283   λm,b.\snd b < nextblock m.
     285  λm,b.block_id b < nextblock m.
    284286
    285287(* FIXME: hacks to get around lack of nunfold *)
     
    288290lemma unfold_high_bound : ∀m,b. high_bound m b = high (blocks m b).
    289291//; qed.
    290 lemma unfold_valid_block : ∀m,b. (valid_block m b) = (\snd b < nextblock m).
     292lemma unfold_valid_block : ∀m,b. (valid_block m b) = (block_id b < nextblock m).
    291293//; qed.
    292294
     
    629631cases b #br #bi
    630632@(Zltb_elim_Type0 bi (nextblock m)) #Hnext
    631 [ @(Zleb_elim_Type0 (low_bound m 〈br,bi〉) ofs) #Hlo
    632     [ @(Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m 〈br,bi〉)) #Hhi
     633[ @(Zleb_elim_Type0 (low_bound m (mk_block br bi)) ofs) #Hlo
     634    [ @(Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m (mk_block br bi))) #Hhi
    633635        [ elim (dec_dividesZ (align_chunk chunk) ofs); #Hal
    634           [ cases (pointer_compat_dec (block_region m 〈br,bi〉) r); #Hcl
     636          [ cases (pointer_compat_dec (block_region m (mk_block br bi)) r); #Hcl
    635637            [ %1 % // @Hnext ]
    636638          ]
     
    657659
    658660definition valid_pointer : mem → region → block → Z → bool ≝
    659 λm,r,b,ofs. Zltb (\snd b) (nextblock m) ∧
     661λm,r,b,ofs. Zltb (block_id b) (nextblock m) ∧
    660662  Zleb (low_bound m b) ofs ∧
    661663  Zltb ofs (high_bound m b) ∧
  • Deliverables/D3.1/C-semantics/Values.ma

    r496 r498  
    2424include "basics/logic.ma".
    2525
    26 definition block ≝ region × Z.
     26record block : Type[0] ≝
     27{ block_region : region
     28; block_id : Z
     29}.
    2730
    2831definition eq_block ≝
    2932λb1,b2.
    30 match b1 with [ pair r1 i1 ⇒
    31 match b2 with [ pair r2 i2 ⇒
    32   eq_region r1 r2 ∧ eqZb i1 i2
    33 ] ].
     33  eq_region (block_region b1) (block_region b2) ∧
     34  eqZb (block_id b1) (block_id b2)
     35.
    3436
    3537lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2.
Note: See TracChangeset for help on using the changeset viewer.