Changeset 583
 Timestamp:
 Feb 22, 2011, 4:23:13 PM (9 years ago)
 Location:
 Deliverables/D3.1/Csemantics
 Files:

 5 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Cexec.ma
r500 r583 263 263 ] 264 264 ] 265 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × int × trace) ≝265 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × offset × trace) ≝ 266 266 match e' with 267 267 [ Evar id ⇒ 268 268 match (get … id en) with 269 [ None ⇒ do l ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈l,zero 〉,E0〉 (* global *)270  Some loc ⇒ OK ? 〈〈loc,zero 〉,E0〉 (* local *)269 [ None ⇒ do l ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *) 270  Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *) 271 271 ] 272 272  Ederef a ⇒ … … 281 281 do 〈lofs,tr〉 ← exec_lvalue ge en m a; 282 282 do delta ← field_offset i fList; 283 OK ? 〈〈\fst lofs, add(\snd lofs) (repr delta)〉,tr〉283 OK ? 〈〈\fst lofs,shift_offset (\snd lofs) (repr delta)〉,tr〉 284 284  Tunion id fList ⇒ 285 285 do 〈lofs,tr〉 ← exec_lvalue ge en m a; … … 289 289  _ ⇒ Error ? 290 290 ] 291 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × int × trace) ≝291 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝ 292 292 match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ]. 293 293 … … 332 332  cons v1 vl ⇒ 333 333 do b ← opt_to_res ? (get … id e); 334 do m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);334 do m1 ← opt_to_res ? (store_value_of_type ty m b zero_offset v1); 335 335 exec_bind_parameters e m1 params' vl 336 336 ] 
Deliverables/D3.1/Csemantics/Csem.ma
r582 r583 129 129 match v1 with 130 130 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 131 [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 ( addofs1 (mul (repr (sizeof ty)) n2)))131 [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (shift_offset ofs1 (mul (repr (sizeof ty)) n2))) 132 132  _ ⇒ None ? ] 133 133  Vnull r ⇒ match v2 with … … 138 138 match v1 with 139 139 [ Vint n1 ⇒ match v2 with 140 [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 ( addofs2 (mul (repr (sizeof ty)) n1)))140 [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset ofs2 (mul (repr (sizeof ty)) n1))) 141 141  _ ⇒ None ? ] 142 142  _ ⇒ None ? ] … … 161 161 match v1 with 162 162 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 163 [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 ( subofs1 (mul (repr (sizeof ty)) n2)))163 [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 (mul (repr (sizeof ty)) n2))) 164 164  _ ⇒ None ? ] 165 165  _ ⇒ None ? ] … … 170 170 if eq_block b1 b2 then 171 171 if eq (repr (sizeof ty)) zero then None ? 172 else Some ? (Vint (divu (sub ofs1 ofs2) (repr (sizeof ty))))172 else Some ? (Vint (divu (sub_offset ofs1 ofs2) (repr (sizeof ty)))) 173 173 else None ? 174 174  _ ⇒ None ? ] … … 323 323 match v2 with 324 324 [ Vptr r2 b2 p2 ofs2 ⇒ 325 if valid_pointer m r1 b1 (signed ofs1)326 ∧ valid_pointer m r2 b2 (signed ofs2)then325 if valid_pointer m r1 b1 ofs1 326 ∧ valid_pointer m r2 b2 ofs2 then 327 327 if eq_block b1 b2 328 then Some ? (of_bool (cmp c ofs1 ofs2))328 then Some ? (of_bool (cmp_offset c ofs1 ofs2)) 329 329 else sem_cmp_mismatch c 330 330 else None ? … … 463 463 reference, the pointer [Vptr b ofs] is returned. *) 464 464 465 let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: int) : option val ≝465 let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: offset) : option val ≝ 466 466 match access_mode ty with 467 467 [ By_value chunk ⇒ loadv chunk m (Vptr Any b ? ofs) … … 481 481 This is allowed only if [ty] indicates an access by value. *) 482 482 483 let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) (v: val) : option mem ≝483 let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: offset) (v: val) : option mem ≝ 484 484 match access_mode ty_dest with 485 485 [ By_value chunk ⇒ storev chunk m (Vptr Any loc ? ofs) v … … 523 523 ∀e,m,id,ty,params,v1,vl,b,m1,m2. 524 524 get ??? id e = Some ? b → 525 store_value_of_type ty m b zero v1 = Some ? m1 →525 store_value_of_type ty m b zero_offset v1 = Some ? m1 → 526 526 bind_parameters e m1 params vl m2 → 527 527 bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2. … … 633 633 be representable in a pointer of region r. *) 634 634 635 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → int → trace → Prop ≝635 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → offset → trace → Prop ≝ 636 636  eval_Evar_local: ∀id,l,ty. 637 637 (* XXX notation? e!id*) get ??? id e = Some ? l → 638 eval_lvalue ge e m (Expr (Evar id) ty) l zero E0638 eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0 639 639  eval_Evar_global: ∀id,l,ty. 640 640 (* XXX e!id *) get ??? id e = None ? → 641 641 find_symbol ?? ge id = Some ? l → 642 eval_lvalue ge e m (Expr (Evar id) ty) l zero E0642 eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0 643 643  eval_Ederef: ∀a,ty,r,l,p,ofs,tr. 644 644 eval_expr ge e m a (Vptr r l p ofs) tr → … … 651 651 typeof a = Tstruct id fList → 652 652 field_offset i fList = OK ? delta → 653 eval_lvalue ge e m (Expr (Efield a i) ty) l ( addofs (repr delta)) tr653 eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ofs (repr delta)) tr 654 654  eval_Efield_union: ∀a,i,ty,l,ofs,id,fList,tr. 655 655 eval_lvalue ge e m a l ofs tr → … … 702 702 (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)) 703 703 (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)) 704 (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 ≝704 (a:expr) (loc:block) (ofs:offset) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : P a loc ofs tr ev ≝ 705 705 match ev with 706 706 [ eval_Evar_local id l ty H ⇒ lvl id l ty H … … 721 721 ∀x4: expr. 722 722 ∀x6: block. 723 ∀x7: int.723 ∀x7: offset. 724 724 ∀x8: trace. 725 725 ∀P: 726 726 ∀_z1430: expr. 727 ∀_z1428: block. ∀_z1427: int. ∀_z1426: trace. Prop.727 ∀_z1428: block. ∀_z1427: offset. ∀_z1426: trace. Prop. 728 728 ∀_H1: ?. 729 729 ∀_H2: ?. … … 739 739 (λx4:expr. 740 740 (λx6:block. 741 (λx7: int.741 (λx7:offset. 742 742 (λx8:trace. 743 743 (λP:∀_z1430: expr. 744 744 ∀_z1428: block. 745 ∀_z1427: int. ∀_z1426: trace. Prop.745 ∀_z1427: offset. ∀_z1426: trace. Prop. 746 746 (λH1:?. 747 747 (λH2:?. … … 752 752 ((λHcut:∀z1435: eq expr x4 x4. 753 753 ∀z1433: eq block x6 x6. 754 ∀z1432: eq int x7 x7.754 ∀z1432: eq offset x7 x7. 755 755 ∀z1431: eq trace x8 x8. 756 756 P x4 x6 x7 x8. 757 757 (Hcut (refl expr x4) 758 758 (refl block x6) 759 (refl int x7) (refl trace x8)))759 (refl offset x7) (refl trace x8))) 760 760 ?))))))))))))))). 761 761 [ @(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) … … 829 829 (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)) 830 830 (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)) 831 (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 ≝831 (a:expr) (loc:block) (ofs:offset) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : Q a loc ofs tr ev ≝ 832 832 match ev with 833 833 [ eval_Evar_local id l ty H ⇒ lvl id l ty H … … 884 884  Kswitch: cont > cont 885 885 (**r catches [break] statements arising out of [switch] *) 886  Kcall: option (block × int × type) >(**r where to store result *)887 function > (**r calling function *)888 env > (**r local env of calling function *)886  Kcall: option (block × offset × type) > (**r where to store result *) 887 function > (**r calling function *) 888 env > (**r local env of calling function *) 889 889 cont > cont. 890 890 
Deliverables/D3.1/Csemantics/Globalenvs.ma
r500 r583 416 416  Some b' ⇒ 417 417 match pointer_compat_dec b' r' with 418 [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc ofs)418 [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset zero_offset ofs)) 419 419  inr _ ⇒ None ? 420 420 ] … … 523 523 init_mem_ 524 524 (λF,ge. functions ? ge) (* find_funct_ptr *) 525 (λF,ge,v. match v with [ Vptr _ b _ o ⇒ if eq o zerothen functions ? ge b else None ?  _ ⇒ None ? ]) (* find_funct *)525 (λF,ge,v. match v with [ Vptr _ b _ o ⇒ if eq_offset o zero_offset then functions ? ge b else None ?  _ ⇒ None ? ]) (* find_funct *) 526 526 (λF,ge. symbols ? ge) (* find_symbol *) 527 527 (* ? 
Deliverables/D3.1/Csemantics/Mem.ma
r500 r583 644 644 given offset falls within the bounds of the corresponding block. *) 645 645 646 definition valid_pointer : mem → region → block → Z→ bool ≝646 definition valid_pointer : mem → region → block → offset → bool ≝ 647 647 λm,r,b,ofs. Zltb (block_id b) (nextblock m) ∧ 648 Zleb (low_bound m b) ofs∧649 Zltb ofs(high_bound m b) ∧648 Zleb (low_bound m b) (offv ofs) ∧ 649 Zltb (offv ofs) (high_bound m b) ∧ 650 650 is_pointer_compat b r. 651 651 … … 680 680 let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝ 681 681 match addr with 682 [ Vptr r b p ofs ⇒ load chunk m r b ( signedofs)682 [ Vptr r b p ofs ⇒ load chunk m r b (offv ofs) 683 683  _ ⇒ None ? ]. 684 684 … … 727 727 λchunk,m,addr,v. 728 728 match addr with 729 [ Vptr r b p ofs ⇒ store chunk m r b ( signedofs) v729 [ Vptr r b p ofs ⇒ store chunk m r b (offv ofs) v 730 730  _ ⇒ None ? ]. 731 731 
Deliverables/D3.1/Csemantics/Values.ma
r500 r583 60 60 λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true  inr _ ⇒ false ]. 61 61 62 record offset : Type[0] ≝ { offv : Z }. 63 64 definition eq_offset ≝ λx,y. eqZb (offv x) (offv y). 65 definition shift_offset : offset → int → offset ≝ 66 λo,i. mk_offset (offv o + signed i). 67 definition neg_shift_offset : offset → int → offset ≝ 68 λo,i. mk_offset (offv o  signed i). 69 definition sub_offset : offset → offset → int ≝ 70 λx,y. repr (offv x  offv y). 71 definition zero_offset ≝ mk_offset OZ. 72 definition lt_offset : offset → offset → bool ≝ 73 λx,y. Zltb (offv x) (offv y). 74 62 75 (* * A value is either: 63 76  a machine integer; … … 76 89  Vfloat: float → val 77 90  Vnull: region → val 78  Vptr: ∀r:region. ∀b:block. pointer_compat b r → int → val.91  Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val. 79 92 80 93 definition Vzero: val ≝ Vint zero. … … 219 232 [ Vint n1 ⇒ match v2 with 220 233 [ Vint n2 ⇒ Vint (add n1 n2) 221  Vptr r b2 p ofs2 ⇒ Vptr r b2 p ( addofs2 n1)234  Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1) 222 235  _ ⇒ Vundef ] 223 236  Vptr r b1 p ofs1 ⇒ match v2 with 224 [ Vint n2 ⇒ Vptr r b1 p ( addofs1 n2)237 [ Vint n2 ⇒ Vptr r b1 p (shift_offset ofs1 n2) 225 238  _ ⇒ Vundef ] 226 239  _ ⇒ Vundef ]. … … 232 245  _ ⇒ Vundef ] 233 246  Vptr r1 b1 p1 ofs1 ⇒ match v2 with 234 [ Vint n2 ⇒ Vptr r1 b1 p1 ( subofs1 n2)247 [ Vint n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ofs1 n2) 235 248  Vptr r2 b2 p2 ofs2 ⇒ 236 if eq_block b1 b2 then Vint (sub ofs1 ofs2) else Vundef249 if eq_block b1 b2 then Vint (sub_offset ofs1 ofs2) else Vundef 237 250  _ ⇒ Vundef ] 238 251  Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero  _ ⇒ Vundef ] … … 397 410 ]. 398 411 399 (* TODO: consider whether to check pointer representations *) 412 definition cmp_offset ≝ 413 λc: comparison. λx,y:offset. 414 match c with 415 [ Ceq ⇒ eq_offset x y 416  Cne ⇒ ¬eq_offset x y 417  Clt ⇒ lt_offset x y 418  Cle ⇒ ¬lt_offset y x 419  Cgt ⇒ lt_offset y x 420  Cge ⇒ ¬lt_offset x y 421 ]. 422 400 423 definition cmp ≝ λc: comparison. λv1,v2: val. 401 424 match v1 with … … 406 429 [ Vptr r2 b2 p2 ofs2 ⇒ 407 430 if eq_block b1 b2 408 then of_bool (cmp c ofs1 ofs2)431 then of_bool (cmp_offset c ofs1 ofs2) 409 432 else cmp_mismatch c 410 433  Vnull r2 ⇒ cmp_mismatch c … … 425 448 [ Vptr r2 b2 p2 ofs2 ⇒ 426 449 if eq_block b1 b2 427 then of_bool (cmp uc ofs1 ofs2)450 then of_bool (cmp_offset c ofs1 ofs2) 428 451 else cmp_mismatch c 429 452  Vnull r2 ⇒ cmp_mismatch c
Note: See TracChangeset
for help on using the changeset viewer.