Changeset 175 for Csemantics/Csem.ma
 Timestamp:
 Oct 13, 2010, 12:19:22 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Csem.ma
r155 r175 568 568 [e] is the current environment and [m] is the current memory state. *) 569 569 570 ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → Prop ≝570 ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝ 571 571  eval_Econst_int: ∀i,ty. 572 eval_expr ge e m (Expr (Econst_int i) ty) (Vint i) 572 eval_expr ge e m (Expr (Econst_int i) ty) (Vint i) E0 573 573  eval_Econst_float: ∀f,ty. 574 eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) 575  eval_Elvalue: ∀a,ty,psp,loc,ofs,v .576 eval_lvalue ge e m (Expr a ty) psp loc ofs >577 load_value_of_type ty m psp loc ofs = Some ? v >578 eval_expr ge e m (Expr a ty) v 579  eval_Eaddrof: ∀a,ty,psp,loc,ofs .580 eval_lvalue ge e m a psp loc ofs >581 eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr psp loc ofs) 574 eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0 575  eval_Elvalue: ∀a,ty,psp,loc,ofs,v,tr. 576 eval_lvalue ge e m (Expr a ty) psp loc ofs tr → 577 load_value_of_type ty m psp loc ofs = Some ? v → 578 eval_expr ge e m (Expr a ty) v tr 579  eval_Eaddrof: ∀a,ty,psp,loc,ofs,tr. 580 eval_lvalue ge e m a psp loc ofs tr → 581 eval_expr ge e m (Expr (Eaddrof a) ty) (Vptr psp loc ofs) tr 582 582  eval_Esizeof: ∀ty',ty. 583 eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) 584  eval_Eunop: ∀op,a,ty,v1,v. 585 eval_expr ge e m a v1 > 586 sem_unary_operation op v1 (typeof a) = Some ? v > 587 eval_expr ge e m (Expr (Eunop op a) ty) v 588  eval_Ebinop: ∀op,a1,a2,ty,v1,v2,v. 589 eval_expr ge e m a1 v1 > 590 eval_expr ge e m a2 v2 > 591 sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v > 592 eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v 593  eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2. 594 eval_expr ge e m a1 v1 > 595 is_true v1 (typeof a1) > 596 eval_expr ge e m a2 v2 > 597 eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v2 598  eval_Econdition_false: ∀a1,a2,a3,ty,v1,v3. 599 eval_expr ge e m a1 v1 > 600 is_false v1 (typeof a1) > 601 eval_expr ge e m a3 v3 > 602 eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3 603  eval_Eorbool_1: ∀a1,a2,ty,v1. 604 eval_expr ge e m a1 v1 > 605 is_true v1 (typeof a1) > 606 eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue 607  eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v. 608 eval_expr ge e m a1 v1 > 609 is_false v1 (typeof a1) > 610 eval_expr ge e m a2 v2 > 611 bool_of_val v2 (typeof a2) v > 612 eval_expr ge e m (Expr (Eorbool a1 a2) ty) v 613  eval_Eandbool_1: ∀a1,a2,ty,v1. 614 eval_expr ge e m a1 v1 > 615 is_false v1 (typeof a1) > 616 eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse 617  eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v. 618 eval_expr ge e m a1 v1 > 619 is_true v1 (typeof a1) > 620 eval_expr ge e m a2 v2 > 621 bool_of_val v2 (typeof a2) v > 622 eval_expr ge e m (Expr (Eandbool a1 a2) ty) v 623  eval_Ecast: ∀a,ty,ty',v1,v. 624 eval_expr ge e m a v1 > 625 cast m v1 (typeof a) ty v > 626 eval_expr ge e m (Expr (Ecast ty a) ty') v 583 eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0 584  eval_Eunop: ∀op,a,ty,v1,v,tr. 585 eval_expr ge e m a v1 tr → 586 sem_unary_operation op v1 (typeof a) = Some ? v → 587 eval_expr ge e m (Expr (Eunop op a) ty) v tr 588  eval_Ebinop: ∀op,a1,a2,ty,v1,v2,v,tr1,tr2. 589 eval_expr ge e m a1 v1 tr1 → 590 eval_expr ge e m a2 v2 tr2 → 591 sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v → 592 eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v (tr1⧺tr2) 593  eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2,tr1,tr2. 594 eval_expr ge e m a1 v1 tr1 → 595 is_true v1 (typeof a1) → 596 eval_expr ge e m a2 v2 tr2 → 597 eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v2 (tr1⧺tr2) 598  eval_Econdition_false: ∀a1,a2,a3,ty,v1,v3,tr1,tr2. 599 eval_expr ge e m a1 v1 tr1 → 600 is_false v1 (typeof a1) → 601 eval_expr ge e m a3 v3 tr2 → 602 eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3 (tr1⧺tr2) 603  eval_Eorbool_1: ∀a1,a2,ty,v1,tr. 604 eval_expr ge e m a1 v1 tr → 605 is_true v1 (typeof a1) → 606 eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue tr 607  eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2. 608 eval_expr ge e m a1 v1 tr1 → 609 is_false v1 (typeof a1) → 610 eval_expr ge e m a2 v2 tr2 → 611 bool_of_val v2 (typeof a2) v → 612 eval_expr ge e m (Expr (Eorbool a1 a2) ty) v (tr1⧺tr2) 613  eval_Eandbool_1: ∀a1,a2,ty,v1,tr. 614 eval_expr ge e m a1 v1 tr → 615 is_false v1 (typeof a1) → 616 eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse tr 617  eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2. 618 eval_expr ge e m a1 v1 tr1 → 619 is_true v1 (typeof a1) → 620 eval_expr ge e m a2 v2 tr2 → 621 bool_of_val v2 (typeof a2) v → 622 eval_expr ge e m (Expr (Eandbool a1 a2) ty) v (tr1⧺tr2) 623  eval_Ecast: ∀a,ty,ty',v1,v,tr. 624 eval_expr ge e m a v1 tr → 625 cast m v1 (typeof a) ty v → 626 eval_expr ge e m (Expr (Ecast ty a) ty') v tr 627  eval_Ecost: ∀a,ty,v,l,tr. 628 eval_expr ge e m a v tr → 629 eval_expr ge e m (Expr (Ecost l a) ty) v (tr⧺Echarge l) 627 630 628 631 (* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a] … … 630 633 that contains the value of the expression [a]. *) 631 634 632 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block > int >Prop ≝635 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block → int → trace → Prop ≝ 633 636  eval_Evar_local: ∀id,l,ty. 634 637 (* XXX notation? e!id*) get ??? id e = Some ? l → 635 eval_lvalue ge e m (Expr (Evar id) ty) Any l zero 638 eval_lvalue ge e m (Expr (Evar id) ty) Any l zero E0 636 639  eval_Evar_global: ∀id,sp,l,ty. 637 (* XXX e!id *) get ??? id e = None ? >638 find_symbol ?? ge id = Some ? 〈sp,l〉 >639 eval_lvalue ge e m (Expr (Evar id) ty) sp l zero 640  eval_Ederef: ∀a,ty,psp,l,ofs .641 eval_expr ge e m a (Vptr psp l ofs) >642 eval_lvalue ge e m (Expr (Ederef a) ty) psp l ofs 643  eval_Efield_struct: ∀a,i,ty,psp,l,ofs,id,fList,delta .644 eval_lvalue ge e m a psp l ofs >645 typeof a = Tstruct id fList >646 field_offset i fList = OK ? delta >647 eval_lvalue ge e m (Expr (Efield a i) ty) psp l (add ofs (repr delta)) 648  eval_Efield_union: ∀a,i,ty,psp,l,ofs,id,fList .649 eval_lvalue ge e m a psp l ofs >650 typeof a = Tunion id fList >651 eval_lvalue ge e m (Expr (Efield a i) ty) psp l ofs .640 (* XXX e!id *) get ??? id e = None ? → 641 find_symbol ?? ge id = Some ? 〈sp,l〉 → 642 eval_lvalue ge e m (Expr (Evar id) ty) sp l zero E0 643  eval_Ederef: ∀a,ty,psp,l,ofs,tr. 644 eval_expr ge e m a (Vptr psp l ofs) tr → 645 eval_lvalue ge e m (Expr (Ederef a) ty) psp l ofs tr 646  eval_Efield_struct: ∀a,i,ty,psp,l,ofs,id,fList,delta,tr. 647 eval_lvalue ge e m a psp l ofs tr → 648 typeof a = Tstruct id fList → 649 field_offset i fList = OK ? delta → 650 eval_lvalue ge e m (Expr (Efield a i) ty) psp l (add ofs (repr delta)) tr 651  eval_Efield_union: ∀a,i,ty,psp,l,ofs,id,fList,tr. 652 eval_lvalue ge e m a psp l ofs tr → 653 typeof a = Tunion id fList → 654 eval_lvalue ge e m (Expr (Efield a i) ty) psp l ofs tr. 652 655 653 656 (* … … 659 662 expressions [al] to their values [vl]. *) 660 663 661 ninductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr > list val > Prop :=664 ninductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝ 662 665  eval_Enil: 663 eval_exprlist ge e m (nil ?) (nil ?) 664  eval_Econs: ∀a,bl,v,vl .665 eval_expr ge e m a v >666 eval_exprlist ge e m bl vl >667 eval_exprlist ge e m (a :: bl) (v :: vl) .666 eval_exprlist ge e m (nil ?) (nil ?) E0 667  eval_Econs: ∀a,bl,v,vl,tr1,tr2. 668 eval_expr ge e m a v tr1 → 669 eval_exprlist ge e m bl vl tr2 → 670 eval_exprlist ge e m (a :: bl) (v :: vl) (tr1⧺tr2). 668 671 669 672 (*End EXPR.*) … … 783 786 (* * Transition relation *) 784 787 785 ninductive step (ge:genv) : state > trace > state > Prop := 786 787  step_assign: ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m'. 788 eval_lvalue ge e m a1 psp loc ofs > 789 eval_expr ge e m a2 v2 > 790 store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' > 788 (* XXX: note that cost labels in exprs expose a particular eval order. *) 789 790 ninductive step (ge:genv) : state → trace → state → Prop ≝ 791 792  step_assign: ∀f,a1,a2,k,e,m,psp,loc,ofs,v2,m',tr1,tr2. 793 eval_lvalue ge e m a1 psp loc ofs tr1 → 794 eval_expr ge e m a2 v2 tr2 → 795 store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' → 791 796 step ge (State f (Sassign a1 a2) k e m) 792 E0(State f Sskip k e m')793 794  step_call_none: ∀f,a,al,k,e,m,vf,vargs,fd .795 eval_expr ge e m a vf >796 eval_exprlist ge e m al vargs >797 find_funct ?? ge vf = Some ? fd >798 type_of_fundef fd = typeof a >797 (tr1⧺tr2) (State f Sskip k e m') 798 799  step_call_none: ∀f,a,al,k,e,m,vf,vargs,fd,tr1,tr2. 800 eval_expr ge e m a vf tr1 → 801 eval_exprlist ge e m al vargs tr2 → 802 find_funct ?? ge vf = Some ? fd → 803 type_of_fundef fd = typeof a → 799 804 step ge (State f (Scall (None ?) a al) k e m) 800 E0(Callstate fd vargs (Kcall (None ?) f e k) m)801 802  step_call_some: ∀f,lhs,a,al,k,e,m,psp,loc,ofs,vf,vargs,fd .803 eval_lvalue ge e m lhs psp loc ofs >804 eval_expr ge e m a vf >805 eval_exprlist ge e m al vargs >806 find_funct ?? ge vf = Some ? fd >807 type_of_fundef fd = typeof a >805 (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m) 806 807  step_call_some: ∀f,lhs,a,al,k,e,m,psp,loc,ofs,vf,vargs,fd,tr1,tr2,tr3. 808 eval_lvalue ge e m lhs psp loc ofs tr1 → 809 eval_expr ge e m a vf tr2 → 810 eval_exprlist ge e m al vargs tr3 → 811 find_funct ?? ge vf = Some ? fd → 812 type_of_fundef fd = typeof a → 808 813 step ge (State f (Scall (Some ? lhs) a al) k e m) 809 E0(Callstate fd vargs (Kcall (Some ? 〈〈〈psp, loc〉, ofs〉, typeof lhs〉) f e k) m)814 (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈〈psp, loc〉, ofs〉, typeof lhs〉) f e k) m) 810 815 811 816  step_seq: ∀f,s1,s2,k,e,m. … … 822 827 E0 (State f Sbreak k e m) 823 828 824  step_ifthenelse_true: ∀f,a,s1,s2,k,e,m,v1 .825 eval_expr ge e m a v1 >826 is_true v1 (typeof a) >829  step_ifthenelse_true: ∀f,a,s1,s2,k,e,m,v1,tr. 830 eval_expr ge e m a v1 tr → 831 is_true v1 (typeof a) → 827 832 step ge (State f (Sifthenelse a s1 s2) k e m) 828 E0(State f s1 k e m)829  step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1 .830 eval_expr ge e m a v1 >831 is_false v1 (typeof a) >833 tr (State f s1 k e m) 834  step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1,tr. 835 eval_expr ge e m a v1 tr → 836 is_false v1 (typeof a) → 832 837 step ge (State f (Sifthenelse a s1 s2) k e m) 833 E0(State f s2 k e m)834 835  step_while_false: ∀f,a,s,k,e,m,v .836 eval_expr ge e m a v >837 is_false v (typeof a) >838 tr (State f s2 k e m) 839 840  step_while_false: ∀f,a,s,k,e,m,v,tr. 841 eval_expr ge e m a v tr → 842 is_false v (typeof a) → 838 843 step ge (State f (Swhile a s) k e m) 839 E0(State f Sskip k e m)840  step_while_true: ∀f,a,s,k,e,m,v .841 eval_expr ge e m a v >842 is_true v (typeof a) >844 tr (State f Sskip k e m) 845  step_while_true: ∀f,a,s,k,e,m,v,tr. 846 eval_expr ge e m a v tr → 847 is_true v (typeof a) → 843 848 step ge (State f (Swhile a s) k e m) 844 E0(State f s (Kwhile a s k) e m)849 tr (State f s (Kwhile a s k) e m) 845 850  step_skip_or_continue_while: ∀f,x,a,s,k,e,m. 846 x = Sskip ∨ x = Scontinue >851 x = Sskip ∨ x = Scontinue → 847 852 step ge (State f x (Kwhile a s k) e m) 848 853 E0 (State f (Swhile a s) k e m) … … 854 859 step ge (State f (Sdowhile a s) k e m) 855 860 E0 (State f s (Kdowhile a s k) e m) 856  step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v .857 x = Sskip ∨ x = Scontinue >858 eval_expr ge e m a v >859 is_false v (typeof a) >861  step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v,tr. 862 x = Sskip ∨ x = Scontinue → 863 eval_expr ge e m a v tr → 864 is_false v (typeof a) → 860 865 step ge (State f x (Kdowhile a s k) e m) 861 E0(State f Sskip k e m)862  step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v .863 x = Sskip ∨ x = Scontinue >864 eval_expr ge e m a v >865 is_true v (typeof a) >866 tr (State f Sskip k e m) 867  step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v,tr. 868 x = Sskip ∨ x = Scontinue → 869 eval_expr ge e m a v tr → 870 is_true v (typeof a) → 866 871 step ge (State f x (Kdowhile a s k) e m) 867 E0(State f (Sdowhile a s) k e m)872 tr (State f (Sdowhile a s) k e m) 868 873  step_break_dowhile: ∀f,a,s,k,e,m. 869 874 step ge (State f Sbreak (Kdowhile a s k) e m) … … 871 876 872 877  step_for_start: ∀f,a1,a2,a3,s,k,e,m. 873 a1 ≠ Sskip >878 a1 ≠ Sskip → 874 879 step ge (State f (Sfor a1 a2 a3 s) k e m) 875 880 E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) 876  step_for_false: ∀f,a2,a3,s,k,e,m,v .877 eval_expr ge e m a2 v >878 is_false v (typeof a2) >881  step_for_false: ∀f,a2,a3,s,k,e,m,v,tr. 882 eval_expr ge e m a2 v tr → 883 is_false v (typeof a2) → 879 884 step ge (State f (Sfor Sskip a2 a3 s) k e m) 880 E0(State f Sskip k e m)881  step_for_true: ∀f,a2,a3,s,k,e,m,v .882 eval_expr ge e m a2 v >883 is_true v (typeof a2) >885 tr (State f Sskip k e m) 886  step_for_true: ∀f,a2,a3,s,k,e,m,v,tr. 887 eval_expr ge e m a2 v tr → 888 is_true v (typeof a2) → 884 889 step ge (State f (Sfor Sskip a2 a3 s) k e m) 885 E0(State f s (Kfor2 a2 a3 s k) e m)890 tr (State f s (Kfor2 a2 a3 s k) e m) 886 891  step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m. 887 x = Sskip ∨ x = Scontinue >892 x = Sskip ∨ x = Scontinue → 888 893 step ge (State f x (Kfor2 a2 a3 s k) e m) 889 894 E0 (State f a3 (Kfor3 a2 a3 s k) e m) … … 896 901 897 902  step_return_0: ∀f,k,e,m. 898 fn_return f = Tvoid >903 fn_return f = Tvoid → 899 904 step ge (State f (Sreturn (None ?)) k e m) 900 905 E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))) 901  step_return_1: ∀f,a,k,e,m,v .902 fn_return f ≠ Tvoid >903 eval_expr ge e m a v >906  step_return_1: ∀f,a,k,e,m,v,tr. 907 fn_return f ≠ Tvoid → 908 eval_expr ge e m a v tr → 904 909 step ge (State f (Sreturn (Some ? a)) k e m) 905 E0(Returnstate v (call_cont k) (free_list m (blocks_of_env e)))910 tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e))) 906 911  step_skip_call: ∀f,k,e,m. 907 is_call_cont k >908 fn_return f = Tvoid >912 is_call_cont k → 913 fn_return f = Tvoid → 909 914 step ge (State f Sskip k e m) 910 915 E0 (Returnstate Vundef k (free_list m (blocks_of_env e))) 911 916 912  step_switch: ∀f,a,sl,k,e,m,n .913 eval_expr ge e m a (Vint n) >917  step_switch: ∀f,a,sl,k,e,m,n,tr. 918 eval_expr ge e m a (Vint n) tr → 914 919 step ge (State f (Sswitch a sl) k e m) 915 E0(State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m)920 tr (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m) 916 921  step_skip_break_switch: ∀f,x,k,e,m. 917 x = Sskip ∨ x = Sbreak >922 x = Sskip ∨ x = Sbreak → 918 923 step ge (State f x (Kswitch k) e m) 919 924 E0 (State f Sskip k e m) … … 927 932 928 933  step_goto: ∀f,lbl,k,e,m,s',k'. 929 find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉 >934 find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉 → 930 935 step ge (State f (Sgoto lbl) k e m) 931 936 E0 (State f s' k' e m) 932 937 933 938  step_internal_function: ∀f,vargs,k,m,e,m1,m2. 934 alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 >935 bind_parameters e m1 (fn_params f) vargs m2 >939 alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 → 940 bind_parameters e m1 (fn_params f) vargs m2 → 936 941 step ge (Callstate (Internal f) vargs k m) 937 942 E0 (State f (fn_body f) k e m2) 938 943 939 944  step_external_function: ∀id,targs,tres,vargs,k,m,vres,t. 940 event_match (external_function id targs tres) vargs t vres >945 event_match (external_function id targs tres) vargs t vres → 941 946 step ge (Callstate (External id targs tres) vargs k m) 942 947 t (Returnstate vres k m) … … 947 952 948 953  step_returnstate_1: ∀v,f,e,k,m,m',psp,loc,ofs,ty. 949 store_value_of_type ty m psp loc ofs v = Some ? m' >954 store_value_of_type ty m psp loc ofs v = Some ? m' → 950 955 step ge (Returnstate v (Kcall (Some ? 〈〈〈psp,loc〉, ofs〉, ty〉) f e k) m) 951 E0 (State f Sskip k e m'). 956 E0 (State f Sskip k e m') 957 958  step_cost: ∀f,lbl,s,k,e,m. 959 step ge (State f (Scost lbl s) k e m) 960 (Echarge lbl) (State f s k e m). 952 961 (* 953 962 (** * Alternate bigstep semantics *)
Note: See TracChangeset
for help on using the changeset viewer.