Changeset 496 for Deliverables/D3.1/Csemantics/Csem.ma
 Timestamp:
 Feb 11, 2011, 4:45:28 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Csem.ma
r487 r496 169 169 [ Vptr pcl1 b1 ofs1 ⇒ match v2 with 170 170 [ Vptr pcl2 b2 ofs2 ⇒ 171 if eq Zbb1 b2 then171 if eq_block b1 b2 then 172 172 if eq (repr (sizeof ty)) zero then None ? 173 173 else Some ? (Vint (divu (sub ofs1 ofs2) (repr (sizeof ty)))) … … 326 326 if valid_pointer m r1 b1 (signed ofs1) 327 327 ∧ valid_pointer m r2 b2 (signed ofs2) then 328 if eq Zbb1 b2328 if eq_block b1 b2 329 329 then Some ? (of_bool (cmp c ofs1 ofs2)) 330 330 else sem_cmp_mismatch c … … 432 432 type_region ty r → 433 433 type_region ty' r' → 434 pointer_compat (block_ spacem b) r' →434 pointer_compat (block_region m b) r' → 435 435 cast m (Vptr r b ofs) ty ty' (Vptr r' b ofs) 436 436  cast_ip_z: ∀m,sz,sg,ty',r. … … 567 567  eval_Econst_float: ∀f,ty. 568 568 eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0 569  eval_Elvalue: ∀a,ty, psp,loc,ofs,v,tr.570 eval_lvalue ge e m (Expr a ty) psploc ofs tr →571 load_value_of_type ty m psploc ofs = Some ? v →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 → 572 572 eval_expr ge e m (Expr a ty) v tr 573  eval_Eaddrof: ∀a,ty, psp,loc,ofs,tr.574 eval_lvalue ge e m a psploc ofs tr →575 eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr psploc ofs) tr573  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 576 576  eval_Esizeof: ∀ty',ty. 577 577 eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0 … … 623 623 eval_expr ge e m (Expr (Ecost l a) ty) v (tr⧺Echarge l) 624 624 625 (* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]625 (* * [eval_lvalue ge e m a r b ofs] defines the evaluation of expression [a] 626 626 in lvalue position. The result is the memory location [b, ofs] 627 that contains the value of the expression [a]. *) 627 that contains the value of the expression [a]. The memory location should 628 be representable in a pointer of region r. *) 628 629 629 630 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → region → block → int → trace → Prop ≝ … … 631 632 (* XXX notation? e!id*) get ??? id e = Some ? l → 632 633 eval_lvalue ge e m (Expr (Evar id) ty) Any l zero E0 633  eval_Evar_global: ∀id, sp,l,ty.634  eval_Evar_global: ∀id,r,l,ty. 634 635 (* XXX e!id *) get ??? id e = None ? → 635 find_symbol ?? ge id = Some ? 〈 sp,l〉 →636 eval_lvalue ge e m (Expr (Evar id) ty) sp lzero E0637  eval_Ederef: ∀a,ty, psp,l,ofs,tr.638 eval_expr ge e m a (Vptr pspl ofs) tr →639 eval_lvalue ge e m (Expr (Ederef a) ty) pspl ofs tr640  eval_Efield_struct: ∀a,i,ty, psp,l,ofs,id,fList,delta,tr.641 eval_lvalue ge e m a pspl ofs tr →636 find_symbol ?? ge id = Some ? 〈r,l〉 → 637 eval_lvalue ge e m (Expr (Evar id) ty) r 〈r,l〉 zero E0 638  eval_Ederef: ∀a,ty,r,l,ofs,tr. 639 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 → 642 643 typeof a = Tstruct id fList → 643 644 field_offset i fList = OK ? delta → 644 eval_lvalue ge e m (Expr (Efield a i) ty) pspl (add ofs (repr delta)) tr645  eval_Efield_union: ∀a,i,ty, psp,l,ofs,id,fList,tr.646 eval_lvalue ge e m a pspl ofs tr →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 → 647 648 typeof a = Tunion id fList → 648 eval_lvalue ge e m (Expr (Efield a i) ty) pspl ofs tr.649 eval_lvalue ge e m (Expr (Efield a i) ty) r l ofs tr. 649 650 650 651 let rec eval_expr_ind (ge:genv) (e:env) (m:mem) … … 1479 1480 globalenv Genv ?? p = OK ? ge → 1480 1481 init_mem Genv ?? p = OK ? m0 → 1481 find_symbol ?? ge (prog_main ?? p) = Some ? 〈Code,b〉→1482 find_symbol ?? ge (prog_main ?? p) = Some ? b → 1482 1483 find_funct_ptr ?? ge b = Some ? f → 1483 1484 initial_state p (Callstate f (nil ?) Kstop m0).
Note: See TracChangeset
for help on using the changeset viewer.