Changeset 583 for Deliverables/D3.1/Csemantics/Csem.ma
 Timestamp:
 Feb 22, 2011, 4:23:13 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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
Note: See TracChangeset
for help on using the changeset viewer.