Changeset 125 for Csemantics/Csem.ma
 Timestamp:
 Sep 24, 2010, 10:31:32 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Csem.ma
r124 r125 48 48 n ≠ zero → 49 49 is_true (Vint n) (Tint sz sg) 50  is_true_pointer_int: ∀p cl,b,ofs,sz,sg.51 is_true (Vptr p clb ofs) (Tint sz sg)50  is_true_pointer_int: ∀psp,b,ofs,sz,sg. 51 is_true (Vptr psp b ofs) (Tint sz sg) 52 52  is_true_int_pointer: ∀n,s,t. 53 53 n ≠ zero → 54 54 is_true (Vint n) (Tpointer s t) 55  is_true_pointer_pointer: ∀p cl,b,ofs,s,t.56 is_true (Vptr p clb ofs) (Tpointer s t)55  is_true_pointer_pointer: ∀psp,b,ofs,s,t. 56 is_true (Vptr psp b ofs) (Tpointer s t) 57 57  is_true_float: ∀f,sz. 58 58 f ≠ Fzero → … … 313 313 [ Vint n1 ⇒ match v2 with 314 314 [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2)) 315  Vptr p clb ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ?315  Vptr psp b ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ? 316 316  _ ⇒ None ? 317 317 ] … … 400 400 ]. 401 401 402 (* XXX should go somewhere else? *)403 ndefinition ptr_cls_spc : ptr_class → mem_space ≝404 λp.match p with405 [ Universal ⇒ Generic406  Data ⇒ Data407  IData ⇒ IData408  XData ⇒ XData409  Code ⇒ Code410 ].411 ndefinition ptr_spc_cls : mem_space → ptr_class ≝412 λp.match p with413 [ Generic ⇒ Universal414  Data ⇒ Data415  IData ⇒ IData416  XData ⇒ XData417  Code ⇒ Code418 ].419 420 ndefinition blk_ptr_cls : block_class → ptr_class ≝421 λb.match b with422 [ UnspecifiedB ⇒ Universal423  DataB ⇒ Data424  IDataB ⇒ IData425  XDataB ⇒ XData426  CodeB ⇒ Code427 ].428 429 402 ninductive type_pointable : type → Prop ≝ 430 403  type_ptr_int : type_pointable (Tint I32 Unsigned) … … 433 406  type_ptr_function : ∀tys,ty. type_pointable (Tfunction tys ty). 434 407 435 ninductive type_space : type → mem _space → Prop ≝436  type_spc_int : type_space (Tint I32 Unsigned) Generic408 ninductive type_space : type → memory_space → Prop ≝ 409  type_spc_int : type_space (Tint I32 Unsigned) Any 437 410  type_spc_pointer : ∀s,t. type_space (Tpointer s t) s 438 411  type_spc_array : ∀s,t,n. type_space (Tarray s t n) s … … 452 425 cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2) 453 426 (Vfloat (cast_float_float sz2 f)) 454  cast_pp: ∀m,p cl,psp,ty,ty',b,ofs.427  cast_pp: ∀m,psp,psp',ty,ty',b,ofs. 455 428 type_pointable ty → 456 type_space ty' psp →457 class_compat (blockclass m b) (ptr_spc_cls psp)→458 cast m (Vptr p cl b ofs) ty ty' (Vptr (ptr_spc_cls psp)b ofs)429 type_space ty' psp' → 430 pointer_compat (block_space m b) psp' → 431 cast m (Vptr psp b ofs) ty ty' (Vptr psp' b ofs) 459 432  cast_pp_z: ∀m,ty,ty'. 460 433 type_pointable ty → (* Don't care which space it is for the source type *) … … 478 451 block. *) 479 452 480 ndefinition env ≝ (tree_t ? PTree) (block_class × block). (* map variable > location *)453 ndefinition env ≝ (tree_t ? PTree) block. (* map variable > location *) 481 454 482 455 ndefinition empty_env: env ≝ (empty …). … … 488 461 reference, the pointer [Vptr b ofs] is returned. *) 489 462 490 nlet rec load_value_of_type (ty: type) (m: mem) (p cl:ptr_class) (b: block) (ofs: int) : option val ≝463 nlet rec load_value_of_type (ty: type) (m: mem) (psp:memory_space) (b: block) (ofs: int) : option val ≝ 491 464 match access_mode ty with 492 [ By_value chunk ⇒ loadv chunk m (Vptr p clb ofs)493  By_reference ⇒ Some ? (Vptr p clb ofs)465 [ By_value chunk ⇒ loadv chunk m (Vptr psp b ofs) 466  By_reference ⇒ Some ? (Vptr psp b ofs) 494 467  By_nothing ⇒ None ? 495 468 ]. … … 500 473 This is allowed only if [ty] indicates an access by value. *) 501 474 502 nlet rec store_value_of_type (ty_dest: type) (m: mem) (p cl:ptr_class) (loc: block) (ofs: int) (v: val) : option mem ≝475 nlet rec store_value_of_type (ty_dest: type) (m: mem) (psp:memory_space) (loc: block) (ofs: int) (v: val) : option mem ≝ 503 476 match access_mode ty_dest with 504 [ By_value chunk ⇒ storev chunk m (Vptr p clloc ofs) v477 [ By_value chunk ⇒ storev chunk m (Vptr psp loc ofs) v 505 478  By_reference ⇒ None ? 506 479  By_nothing ⇒ None ? … … 522 495  alloc_variables_cons: 523 496 ∀e,m,id,ty,vars,m1,b1,m2,e2. 524 alloc m 0 (sizeof ty) UnspecifiedB = 〈m1, b1〉 → (* XXX *)525 alloc_variables (set … id 〈UnspecifiedB, b1〉e) m1 vars e2 m2 →497 alloc m 0 (sizeof ty) Any = 〈m1, b1〉 → 498 alloc_variables (set … id b1 e) m1 vars e2 m2 → 526 499 alloc_variables e m (〈id, ty〉 :: vars) e2 m2. 527 500 … … 538 511 bind_parameters e m (nil ?) (nil ?) m 539 512  bind_parameters_cons: 540 ∀e,m,id,ty,params,v1,vl,b cls,b,m1,m2.541 get ??? id e = Some ? 〈bcls,b〉→542 store_value_of_type ty m (blk_ptr_cls bcls)b zero v1 = Some ? m1 →513 ∀e,m,id,ty,params,v1,vl,b,m1,m2. 514 get ??? id e = Some ? b → 515 store_value_of_type ty m Any b zero v1 = Some ? m1 → 543 516 bind_parameters e m1 params vl m2 → 544 517 bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2. 545 518 519 (* XXX: this doesn't look right  we're assigning arbitrary memory spaces to 520 parameters? *) 521 546 522 (* * Return the list of blocks in the codomain of [e]. *) 547 523 548 524 ndefinition blocks_of_env : env → list block ≝ λe. 549 map ?? (λx. snd ?? (snd ?? x)) (elements ??? e).525 map ?? (λx. snd ?? x) (elements ??? e). 550 526 551 527 (* * Selection of the appropriate case of a [switch], given the value [n] … … 588 564  eval_Econst_float: ∀f,ty. 589 565 eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) 590  eval_Elvalue: ∀a,ty,p cl,loc,ofs,v.591 eval_lvalue ge e m (Expr a ty) p clloc ofs >592 load_value_of_type ty m p clloc ofs = Some ? v >566  eval_Elvalue: ∀a,ty,psp,loc,ofs,v. 567 eval_lvalue ge e m (Expr a ty) psp loc ofs > 568 load_value_of_type ty m psp loc ofs = Some ? v > 593 569 eval_expr ge e m (Expr a ty) v 594  eval_Eaddrof: ∀a,ty,p cl,loc,ofs.595 eval_lvalue ge e m a p clloc ofs >596 eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr p clloc ofs)570  eval_Eaddrof: ∀a,ty,psp,loc,ofs. 571 eval_lvalue ge e m a psp loc ofs > 572 eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr psp loc ofs) 597 573  eval_Esizeof: ∀ty',ty. 598 574 eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) … … 645 621 that contains the value of the expression [a]. *) 646 622 647 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → ptr_class→ block > int > Prop ≝648  eval_Evar_local: ∀id, bcl,l,ty.649 (* XXX notation? e!id*) get ??? id e = Some ? 〈bcl,l〉 >650 eval_lvalue ge e m (Expr (Evar id) ty) (blk_ptr_cls bcl)l zero651  eval_Evar_global: ∀id, l,ty.623 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block > int > Prop ≝ 624  eval_Evar_local: ∀id,l,ty. 625 (* XXX notation? e!id*) get ??? id e = Some ? l → 626 eval_lvalue ge e m (Expr (Evar id) ty) Any l zero 627  eval_Evar_global: ∀id,sp,l,ty. 652 628 (* XXX e!id *) get ??? id e = None ? > 653 find_symbol ?? ge id = Some ? l>654 eval_lvalue ge e m (Expr (Evar id) ty) Universal l zero (* XXX *)655  eval_Ederef: ∀a,ty,p cl,l,ofs.656 eval_expr ge e m a (Vptr p cll ofs) >657 eval_lvalue ge e m (Expr (Ederef a) ty) p cll ofs658  eval_Efield_struct: ∀a,i,ty,p cl,l,ofs,id,fList,delta.659 eval_lvalue ge e m a p cll ofs >629 find_symbol ?? ge id = Some ? 〈sp,l〉 > 630 eval_lvalue ge e m (Expr (Evar id) ty) sp l zero 631  eval_Ederef: ∀a,ty,psp,l,ofs. 632 eval_expr ge e m a (Vptr psp l ofs) > 633 eval_lvalue ge e m (Expr (Ederef a) ty) psp l ofs 634  eval_Efield_struct: ∀a,i,ty,psp,l,ofs,id,fList,delta. 635 eval_lvalue ge e m a psp l ofs > 660 636 typeof a = Tstruct id fList > 661 637 field_offset i fList = OK ? delta > 662 eval_lvalue ge e m (Expr (Efield a i) ty) p cll (add ofs (repr delta))663  eval_Efield_union: ∀a,i,ty,p cl,l,ofs,id,fList.664 eval_lvalue ge e m a p cll ofs >638 eval_lvalue ge e m (Expr (Efield a i) ty) psp l (add ofs (repr delta)) 639  eval_Efield_union: ∀a,i,ty,psp,l,ofs,id,fList. 640 eval_lvalue ge e m a psp l ofs > 665 641 typeof a = Tunion id fList > 666 eval_lvalue ge e m (Expr (Efield a i) ty) p cll ofs.642 eval_lvalue ge e m (Expr (Efield a i) ty) psp l ofs. 667 643 668 644 (* … … 702 678  Kswitch: cont > cont 703 679 (**r catches [break] statements arising out of [switch] *) 704  Kcall: option ( ptr_class× block × int × type) > (**r where to store result *)680  Kcall: option (memory_space × block × int × type) > (**r where to store result *) 705 681 function > (**r calling function *) 706 682 env > (**r local env of calling function *) … … 800 776 ninductive step (ge:genv) : state > trace > state > Prop := 801 777 802  step_assign: ∀f,a1,a2,k,e,m,p cl,loc,ofs,v2,m'.803 eval_lvalue ge e m a1 p clloc ofs >778  step_assign: ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m'. 779 eval_lvalue ge e m a1 psp loc ofs > 804 780 eval_expr ge e m a2 v2 > 805 store_value_of_type (typeof a1) m p clloc ofs v2 = Some ? m' >781 store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' > 806 782 step ge (State f (Sassign a1 a2) k e m) 807 783 E0 (State f Sskip k e m') … … 815 791 E0 (Callstate fd vargs (Kcall (None ?) f e k) m) 816 792 817  step_call_some: ∀f,lhs,a,al,k,e,m,p cl,loc,ofs,vf,vargs,fd.818 eval_lvalue ge e m lhs p clloc ofs >793  step_call_some: ∀f,lhs,a,al,k,e,m,psp,loc,ofs,vf,vargs,fd. 794 eval_lvalue ge e m lhs psp loc ofs > 819 795 eval_expr ge e m a vf > 820 796 eval_exprlist ge e m al vargs > … … 822 798 type_of_fundef fd = typeof a > 823 799 step ge (State f (Scall (Some ? lhs) a al) k e m) 824 E0 (Callstate fd vargs (Kcall (Some ? 〈〈〈p cl, loc〉, ofs〉, typeof lhs〉) f e k) m)800 E0 (Callstate fd vargs (Kcall (Some ? 〈〈〈psp, loc〉, ofs〉, typeof lhs〉) f e k) m) 825 801 826 802  step_seq: ∀f,s1,s2,k,e,m. … … 961 937 E0 (State f Sskip k e m) 962 938 963  step_returnstate_1: ∀v,f,e,k,m,m',p cl,loc,ofs,ty.964 store_value_of_type ty m p clloc ofs v = Some ? m' >965 step ge (Returnstate v (Kcall (Some ? 〈〈〈p cl,loc〉, ofs〉, ty〉) f e k) m)939  step_returnstate_1: ∀v,f,e,k,m,m',psp,loc,ofs,ty. 940 store_value_of_type ty m psp loc ofs v = Some ? m' > 941 step ge (Returnstate v (Kcall (Some ? 〈〈〈psp,loc〉, ofs〉, ty〉) f e k) m) 966 942 E0 (State f Sskip k e m'). 967 943 (* … … 1281 1257 let ge := globalenv Genv ?? p in 1282 1258 let m0 := init_mem Genv ?? p in 1283 find_symbol ?? ge (prog_main ?? p) = Some ? b>1259 find_symbol ?? ge (prog_main ?? p) = Some ? 〈Code,b〉 > 1284 1260 find_funct_ptr ?? ge b = Some ? f > 1285 1261 initial_state p (Callstate f (nil ?) Kstop m0).
Note: See TracChangeset
for help on using the changeset viewer.