Changeset 124 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
r13 r124 39 39  is_false_int: ∀sz,sg. 40 40 is_false (Vint zero) (Tint sz sg) 41  is_false_pointer: ∀ t.42 is_false (Vint zero) (Tpointer t)41  is_false_pointer: ∀s,t. 42 is_false (Vint zero) (Tpointer s t) 43 43  is_false_float: ∀sz. 44 44 is_false (Vfloat Fzero) (Tfloat sz). … … 48 48 n ≠ zero → 49 49 is_true (Vint n) (Tint sz sg) 50  is_true_pointer_int: ∀ b,ofs,sz,sg.51 is_true (Vptr b ofs) (Tint sz sg)52  is_true_int_pointer: ∀n, t.50  is_true_pointer_int: ∀pcl,b,ofs,sz,sg. 51 is_true (Vptr pcl b ofs) (Tint sz sg) 52  is_true_int_pointer: ∀n,s,t. 53 53 n ≠ zero → 54 is_true (Vint n) (Tpointer t)55  is_true_pointer_pointer: ∀ b,ofs,t.56 is_true (Vptr b ofs) (Tpointert)54 is_true (Vint n) (Tpointer s t) 55  is_true_pointer_pointer: ∀pcl,b,ofs,s,t. 56 is_true (Vptr pcl b ofs) (Tpointer s t) 57 57  is_true_float: ∀f,sz. 58 58 f ≠ Fzero → … … 101 101 match v with 102 102 [ Vint n ⇒ Some ? (of_bool (eq n zero)) 103  Vptr _ _ ⇒ Some ? Vfalse103  Vptr _ _ _ ⇒ Some ? Vfalse 104 104  _ ⇒ None ? 105 105 ] 106  Tpointer _ ⇒106  Tpointer _ _ ⇒ 107 107 match v with 108 108 [ Vint n ⇒ Some ? (of_bool (eq n zero)) 109  Vptr _ _ ⇒ Some ? Vfalse109  Vptr _ _ _ ⇒ Some ? Vfalse 110 110  _ ⇒ None ? 111 111 ] … … 134 134  add_case_pi ty ⇒ (**r pointer plus integer *) 135 135 match v1 with 136 [ Vptr b1 ofs1 ⇒ match v2 with137 [ Vint n2 ⇒ Some ? (Vptr b1 (add ofs1 (mul (repr (sizeof ty)) n2)))136 [ Vptr pcl1 b1 ofs1 ⇒ match v2 with 137 [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (add ofs1 (mul (repr (sizeof ty)) n2))) 138 138  _ ⇒ None ? ] 139 139  _ ⇒ None ? ] … … 141 141 match v1 with 142 142 [ Vint n1 ⇒ match v2 with 143 [ Vptr b2 ofs2 ⇒ Some ? (Vptrb2 (add ofs2 (mul (repr (sizeof ty)) n1)))143 [ Vptr pcl2 b2 ofs2 ⇒ Some ? (Vptr pcl2 b2 (add ofs2 (mul (repr (sizeof ty)) n1))) 144 144  _ ⇒ None ? ] 145 145  _ ⇒ None ? ] … … 163 163  sub_case_pi ty ⇒ (**r pointer minus integer *) 164 164 match v1 with 165 [ Vptr b1 ofs1 ⇒ match v2 with166 [ Vint n2 ⇒ Some ? (Vptr b1 (sub ofs1 (mul (repr (sizeof ty)) n2)))165 [ Vptr pcl1 b1 ofs1 ⇒ match v2 with 166 [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (sub ofs1 (mul (repr (sizeof ty)) n2))) 167 167  _ ⇒ None ? ] 168 168  _ ⇒ None ? ] 169 169  sub_case_pp ty ⇒ (**r pointer minus pointer *) 170 170 match v1 with 171 [ Vptr b1 ofs1 ⇒ match v2 with172 [ Vptr b2 ofs2 ⇒171 [ Vptr pcl1 b1 ofs1 ⇒ match v2 with 172 [ Vptr pcl2 b2 ofs2 ⇒ 173 173 if eqZb b1 b2 then 174 174 if eq (repr (sizeof ty)) zero then None ? … … 179 179  sub_default ⇒ None ? 180 180 ]. 181 181 182 182 nlet rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝ 183 183 match classify_mul t1 t2 with … … 313 313 [ Vint n1 ⇒ match v2 with 314 314 [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2)) 315  Vptr b ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ?315  Vptr pcl b ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ? 316 316  _ ⇒ None ? 317 317 ] 318  Vptr b1 ofs1 ⇒318  Vptr pcl1 b1 ofs1 ⇒ 319 319 match v2 with 320 [ Vptr b2 ofs2 ⇒321 if valid_pointer m b1 (signed ofs1)322 ∧ valid_pointer m b2 (signed ofs2) then320 [ Vptr pcl2 b2 ofs2 ⇒ 321 if valid_pointer m pcl1 b1 (signed ofs1) 322 ∧ valid_pointer m pcl2 b2 (signed ofs2) then 323 323 if eqZb b1 b2 324 324 then Some ? (of_bool (cmp c ofs1 ofs2)) … … 400 400 ]. 401 401 402 ninductive neutral_for_cast: type → Prop ≝ 403  nfc_int: ∀sg. 404 neutral_for_cast (Tint I32 sg) 405  nfc_ptr: ∀ty. 406 neutral_for_cast (Tpointer ty) 407  nfc_array: ∀ty,sz. 408 neutral_for_cast (Tarray ty sz) 409  nfc_fun: ∀targs,tres. 410 neutral_for_cast (Tfunction targs tres). 411 412 ninductive cast : val → type → type → val → Prop ≝ 413  cast_ii: ∀i,sz2,sz1,si1,si2. (**r int to int *) 414 cast (Vint i) (Tint sz1 si1) (Tint sz2 si2) 402 (* XXX should go somewhere else? *) 403 ndefinition ptr_cls_spc : ptr_class → mem_space ≝ 404 λp.match p with 405 [ Universal ⇒ Generic 406  Data ⇒ Data 407  IData ⇒ IData 408  XData ⇒ XData 409  Code ⇒ Code 410 ]. 411 ndefinition ptr_spc_cls : mem_space → ptr_class ≝ 412 λp.match p with 413 [ Generic ⇒ Universal 414  Data ⇒ Data 415  IData ⇒ IData 416  XData ⇒ XData 417  Code ⇒ Code 418 ]. 419 420 ndefinition blk_ptr_cls : block_class → ptr_class ≝ 421 λb.match b with 422 [ UnspecifiedB ⇒ Universal 423  DataB ⇒ Data 424  IDataB ⇒ IData 425  XDataB ⇒ XData 426  CodeB ⇒ Code 427 ]. 428 429 ninductive type_pointable : type → Prop ≝ 430  type_ptr_int : type_pointable (Tint I32 Unsigned) 431  type_ptr_pointer : ∀s,t. type_pointable (Tpointer s t) 432  type_ptr_array : ∀s,t,n. type_pointable (Tarray s t n) 433  type_ptr_function : ∀tys,ty. type_pointable (Tfunction tys ty). 434 435 ninductive type_space : type → mem_space → Prop ≝ 436  type_spc_int : type_space (Tint I32 Unsigned) Generic 437  type_spc_pointer : ∀s,t. type_space (Tpointer s t) s 438  type_spc_array : ∀s,t,n. type_space (Tarray s t n) s 439  type_spc_code : ∀tys,ty. type_space (Tfunction tys ty) Code. 440 441 ninductive cast : mem → val → type → type → val → Prop ≝ 442  cast_ii: ∀m,i,sz2,sz1,si1,si2. (**r int to int *) 443 cast m (Vint i) (Tint sz1 si1) (Tint sz2 si2) 415 444 (Vint (cast_int_int sz2 si2 i)) 416  cast_fi: ∀ f,sz1,sz2,si2. (**r float to int *)417 cast (Vfloat f) (Tfloat sz1) (Tint sz2 si2)445  cast_fi: ∀m,f,sz1,sz2,si2. (**r float to int *) 446 cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2) 418 447 (Vint (cast_int_int sz2 si2 (cast_float_int si2 f))) 419  cast_if: ∀ i,sz1,sz2,si1. (**r int to float *)420 cast (Vint i) (Tint sz1 si1) (Tfloat sz2)448  cast_if: ∀m,i,sz1,sz2,si1. (**r int to float *) 449 cast m (Vint i) (Tint sz1 si1) (Tfloat sz2) 421 450 (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) 422  cast_ff: ∀ f,sz1,sz2. (**r float to float *)423 cast (Vfloat f) (Tfloat sz1) (Tfloat sz2)451  cast_ff: ∀m,f,sz1,sz2. (**r float to float *) 452 cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2) 424 453 (Vfloat (cast_float_float sz2 f)) 425  cast_nn_p: ∀b,ofs,t1,t2. (**r no change in data representation *) 454  cast_pp: ∀m,pcl,psp,ty,ty',b,ofs. 455 type_pointable ty → 456 type_space ty' psp → 457 class_compat (blockclass m b) (ptr_spc_cls psp) → 458 cast m (Vptr pcl b ofs) ty ty' (Vptr (ptr_spc_cls psp) b ofs) 459  cast_pp_z: ∀m,ty,ty'. 460 type_pointable ty → (* Don't care which space it is for the source type *) 461 type_pointable ty' → 462 cast m (Vint zero) ty ty' (Vint zero). 463 (* XXX: other integers? 464  cast_nn_i: ∀m,n,t1,t2. (**r no change in data representation *) 426 465 neutral_for_cast t1 → neutral_for_cast t2 → 427 cast (Vptr b ofs) t1 t2 (Vptr b ofs) 428  cast_nn_i: ∀n,t1,t2. (**r no change in data representation *) 429 neutral_for_cast t1 → neutral_for_cast t2 → 430 cast (Vint n) t1 t2 (Vint n). 431 466 cast m (Vint n) t1 t2 (Vint n). 467 *) 432 468 (* * * Operational semantics *) 433 469 … … 442 478 block. *) 443 479 444 ndefinition env ≝ (tree_t ? PTree) block. (* map variable > location *)480 ndefinition env ≝ (tree_t ? PTree) (block_class × block). (* map variable > location *) 445 481 446 482 ndefinition empty_env: env ≝ (empty …). … … 452 488 reference, the pointer [Vptr b ofs] is returned. *) 453 489 454 nlet rec load_value_of_type (ty: type) (m: mem) ( b: block) (ofs: int) : option val ≝490 nlet rec load_value_of_type (ty: type) (m: mem) (pcl:ptr_class) (b: block) (ofs: int) : option val ≝ 455 491 match access_mode ty with 456 [ By_value chunk ⇒ loadv chunk m (Vptr b ofs)457  By_reference ⇒ Some ? (Vptr b ofs)492 [ By_value chunk ⇒ loadv chunk m (Vptr pcl b ofs) 493  By_reference ⇒ Some ? (Vptr pcl b ofs) 458 494  By_nothing ⇒ None ? 459 495 ]. … … 464 500 This is allowed only if [ty] indicates an access by value. *) 465 501 466 nlet rec store_value_of_type (ty_dest: type) (m: mem) ( loc: block) (ofs: int) (v: val) : option mem ≝502 nlet rec store_value_of_type (ty_dest: type) (m: mem) (pcl:ptr_class) (loc: block) (ofs: int) (v: val) : option mem ≝ 467 503 match access_mode ty_dest with 468 [ By_value chunk ⇒ storev chunk m (Vptr loc ofs) v504 [ By_value chunk ⇒ storev chunk m (Vptr pcl loc ofs) v 469 505  By_reference ⇒ None ? 470 506  By_nothing ⇒ None ? … … 486 522  alloc_variables_cons: 487 523 ∀e,m,id,ty,vars,m1,b1,m2,e2. 488 alloc m 0 (sizeof ty) = 〈m1, b1〉 →489 alloc_variables (set … id b1e) m1 vars e2 m2 →524 alloc m 0 (sizeof ty) UnspecifiedB = 〈m1, b1〉 → (* XXX *) 525 alloc_variables (set … id 〈UnspecifiedB, b1〉 e) m1 vars e2 m2 → 490 526 alloc_variables e m (〈id, ty〉 :: vars) e2 m2. 491 527 … … 502 538 bind_parameters e m (nil ?) (nil ?) m 503 539  bind_parameters_cons: 504 ∀e,m,id,ty,params,v1,vl,b ,m1,m2.505 get ??? id e = Some ? b→506 store_value_of_type ty m b zero v1 = Some ? m1 →540 ∀e,m,id,ty,params,v1,vl,bcls,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 → 507 543 bind_parameters e m1 params vl m2 → 508 544 bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2. … … 511 547 512 548 ndefinition blocks_of_env : env → list block ≝ λe. 513 map ?? ( snd ident block) (elements ??? e).549 map ?? (λx. snd ?? (snd ?? x)) (elements ??? e). 514 550 515 551 (* * Selection of the appropriate case of a [switch], given the value [n] … … 552 588  eval_Econst_float: ∀f,ty. 553 589 eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) 554  eval_Elvalue: ∀a,ty, loc,ofs,v.555 eval_lvalue ge e m (Expr a ty) loc ofs >556 load_value_of_type ty m loc ofs = Some ? v >590  eval_Elvalue: ∀a,ty,pcl,loc,ofs,v. 591 eval_lvalue ge e m (Expr a ty) pcl loc ofs > 592 load_value_of_type ty m pcl loc ofs = Some ? v > 557 593 eval_expr ge e m (Expr a ty) v 558  eval_Eaddrof: ∀a,ty, loc,ofs.559 eval_lvalue ge e m a loc ofs >560 eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr loc ofs)594  eval_Eaddrof: ∀a,ty,pcl,loc,ofs. 595 eval_lvalue ge e m a pcl loc ofs > 596 eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr pcl loc ofs) 561 597  eval_Esizeof: ∀ty',ty. 562 598 eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) … … 602 638  eval_Ecast: ∀a,ty,ty',v1,v. 603 639 eval_expr ge e m a v1 > 604 cast v1 (typeof a) ty v >640 cast m v1 (typeof a) ty v > 605 641 eval_expr ge e m (Expr (Ecast ty a) ty') v 606 642 … … 609 645 that contains the value of the expression [a]. *) 610 646 611 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr >block > int > Prop ≝612  eval_Evar_local: ∀id, l,ty.613 (* XXX notation? e!id*) get ??? id e = Some ? l>614 eval_lvalue ge e m (Expr (Evar id) ty) l zero647 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 zero 615 651  eval_Evar_global: ∀id,l,ty. 616 652 (* XXX e!id *) get ??? id e = None ? > 617 653 find_symbol ?? ge id = Some ? l > 618 eval_lvalue ge e m (Expr (Evar id) ty) l zero619  eval_Ederef: ∀a,ty, l,ofs.620 eval_expr ge e m a (Vptr l ofs) >621 eval_lvalue ge e m (Expr (Ederef a) ty) l ofs622  eval_Efield_struct: ∀a,i,ty, l,ofs,id,fList,delta.623 eval_lvalue ge e m a l ofs >654 eval_lvalue ge e m (Expr (Evar id) ty) Universal l zero (* XXX *) 655  eval_Ederef: ∀a,ty,pcl,l,ofs. 656 eval_expr ge e m a (Vptr pcl l ofs) > 657 eval_lvalue ge e m (Expr (Ederef a) ty) pcl l ofs 658  eval_Efield_struct: ∀a,i,ty,pcl,l,ofs,id,fList,delta. 659 eval_lvalue ge e m a pcl l ofs > 624 660 typeof a = Tstruct id fList > 625 661 field_offset i fList = OK ? delta > 626 eval_lvalue ge e m (Expr (Efield a i) ty) l (add ofs (repr delta))627  eval_Efield_union: ∀a,i,ty, l,ofs,id,fList.628 eval_lvalue ge e m a l ofs >662 eval_lvalue ge e m (Expr (Efield a i) ty) pcl l (add ofs (repr delta)) 663  eval_Efield_union: ∀a,i,ty,pcl,l,ofs,id,fList. 664 eval_lvalue ge e m a pcl l ofs > 629 665 typeof a = Tunion id fList > 630 eval_lvalue ge e m (Expr (Efield a i) ty) l ofs.666 eval_lvalue ge e m (Expr (Efield a i) ty) pcl l ofs. 631 667 632 668 (* … … 666 702  Kswitch: cont > cont 667 703 (**r catches [break] statements arising out of [switch] *) 668  Kcall: option ( block × int × type) > (**r where to store result *)704  Kcall: option (ptr_class × block × int × type) > (**r where to store result *) 669 705 function > (**r calling function *) 670 706 env > (**r local env of calling function *) … … 764 800 ninductive step (ge:genv) : state > trace > state > Prop := 765 801 766  step_assign: ∀f,a1,a2,k,e,m, loc,ofs,v2,m'.767 eval_lvalue ge e m a1 loc ofs >802  step_assign: ∀f,a1,a2,k,e,m,pcl,loc,ofs,v2,m'. 803 eval_lvalue ge e m a1 pcl loc ofs > 768 804 eval_expr ge e m a2 v2 > 769 store_value_of_type (typeof a1) m loc ofs v2 = Some ? m' >805 store_value_of_type (typeof a1) m pcl loc ofs v2 = Some ? m' > 770 806 step ge (State f (Sassign a1 a2) k e m) 771 807 E0 (State f Sskip k e m') … … 779 815 E0 (Callstate fd vargs (Kcall (None ?) f e k) m) 780 816 781  step_call_some: ∀f,lhs,a,al,k,e,m, loc,ofs,vf,vargs,fd.782 eval_lvalue ge e m lhs loc ofs >817  step_call_some: ∀f,lhs,a,al,k,e,m,pcl,loc,ofs,vf,vargs,fd. 818 eval_lvalue ge e m lhs pcl loc ofs > 783 819 eval_expr ge e m a vf > 784 820 eval_exprlist ge e m al vargs > … … 786 822 type_of_fundef fd = typeof a > 787 823 step ge (State f (Scall (Some ? lhs) a al) k e m) 788 E0 (Callstate fd vargs (Kcall (Some ? 〈〈 loc, ofs〉, typeof lhs〉) f e k) m)824 E0 (Callstate fd vargs (Kcall (Some ? 〈〈〈pcl, loc〉, ofs〉, typeof lhs〉) f e k) m) 789 825 790 826  step_seq: ∀f,s1,s2,k,e,m. … … 925 961 E0 (State f Sskip k e m) 926 962 927  step_returnstate_1: ∀v,f,e,k,m,m', loc,ofs,ty.928 store_value_of_type ty m loc ofs v = Some ? m' >929 step ge (Returnstate v (Kcall (Some ? 〈〈 loc, ofs〉, ty〉) f e k) m)963  step_returnstate_1: ∀v,f,e,k,m,m',pcl,loc,ofs,ty. 964 store_value_of_type ty m pcl loc ofs v = Some ? m' > 965 step ge (Returnstate v (Kcall (Some ? 〈〈〈pcl,loc〉, ofs〉, ty〉) f e k) m) 930 966 E0 (State f Sskip k e m'). 931 967 (*
Note: See TracChangeset
for help on using the changeset viewer.