Changeset 1705
 Timestamp:
 Feb 16, 2012, 6:05:45 PM (7 years ago)
 Location:
 src/RTLabs
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1682 r1705 19 19  Returnstate _ _ _ _ ⇒ cl_return 20 20 ]. 21 22 definition is_cost_label : statement → bool ≝ 23 λs. match s with [ St_cost _ _ ⇒ true  _ ⇒ false ]. 21 24 22 25 definition RTLabs_cost : state → bool ≝ … … 910 913 qed. 911 914 915 (* Define a notion of sound labellings of RTLabs programs. *) 916 917 let rec successors (s : statement) : list label ≝ 918 match s with 919 [ St_skip l ⇒ [l] 920  St_cost _ l ⇒ [l] 921  St_const _ _ l ⇒ [l] 922  St_op1 _ _ _ _ _ l ⇒ [l] 923  St_op2 _ _ _ _ l ⇒ [l] 924  St_load _ _ _ l ⇒ [l] 925  St_store _ _ _ l ⇒ [l] 926  St_call_id _ _ _ l ⇒ [l] 927  St_call_ptr _ _ _ l ⇒ [l] 928 (* 929  St_tailcall_id _ _ ⇒ [ ] 930  St_tailcall_ptr _ _ ⇒ [ ] 931 *) 932  St_cond _ l1 l2 ⇒ [l1; l2] 933  St_jumptable _ ls ⇒ ls 934  St_return ⇒ [ ] 935 ]. 936 937 definition actual_successor : state → option label ≝ 938 λs. match s with 939 [ State f fs m ⇒ Some ? (next f) 940  Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f)  _ ⇒ None ? ] 941  Returnstate _ _ _ _ ⇒ None ? 942 ]. 943 944 lemma nth_opt_Exists : ∀A,n,l,a. 945 nth_opt A n l = Some A a → 946 Exists A (λa'. a' = a) l. 947 #A #n elim n 948 [ * [ #a #E normalize in E; destruct  #a #l #a' #E normalize in E; destruct % // ] 949  #m #IH * 950 [ #a #E normalize in E; destruct 951  #a #l #a' #E %2 @IH @E 952 ] 953 ] qed. 954 955 lemma eval_successor : ∀ge,f,fs,m,tr,s'. 956 eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 → 957 RTLabs_classify s' = cl_return ∨ 958 ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))). 959 #ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s' 960 whd in ⊢ (??%? → ?); 961 generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok) 962 [ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 963  #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 964  #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 965  #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 966  #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 967  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 968  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 969  #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 970  #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 971  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1}  %{l2} ] % // [ %  %2 %] // 972  #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev 973 cases v [ #E normalize in E; destruct  #sz #i  #f #E normalize in E; destruct  #r #E normalize in E; destruct  #p #E normalize in E; destruct ] 974 whd in ⊢ (??%? → ?); 975 generalize in ⊢ (??(?%)? → ?); 976 cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ?  _ ⇒ ? ] ?)? → ?); 977 [ #e #E normalize in E; destruct 978  #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El) 979 ] 980  #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl 981 ] qed. 982 983 definition steps_for_statement : statement → nat ≝ 984 λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1  St_call_ptr _ _ _ _ ⇒ 1  St_return ⇒ 1  _ ⇒ 0 ]). 985 986 inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝ 987  stlb_refl : ∀l,n,H. is_cost_label (lookup_present … g l H) → steps_to_label_bound g l (S n) 988  stlb_step : ∀l,n,H. 989 let stmt ≝ lookup_present … g l H in 990 (∀l'. Exists label (λl0. l0 = l') (successors stmt) → steps_to_label_bound g l' n) → 991 steps_to_label_bound g l (steps_for_statement stmt + n). 992 993 discriminator nat. 994 995 lemma steps_to_label_bound_inv_step : ∀g,l,n. 996 steps_to_label_bound g l n → 997 ∀H. 998 let stmt ≝ lookup_present … g l H in 999 ¬ (bool_to_Prop (is_cost_label stmt)) → 1000 (∀l'. Exists label (λl0. l0 = l') (successors stmt) → 1001 ∃n'. n = n' + steps_for_statement stmt ∧ 1002 steps_to_label_bound g l' n'). 1003 #g #l0 #n0 #H1 inversion H1 1004 [ #l #n #H2 #C #E1 #E2 #_ destruct #H3 #H4 @⊥ @(absurd ? C H4) 1005  #l #n #H2 #IH #_ #E1 #E2 #_ destruct #H3 #NC #l' #EX 1006 % [2: % [ @commutative_plus  @IH // ] ] 1007 ] qed. 1008 1009 definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n. 1010 1011 let rec soundly_labelled_fn (fn : internal_function) : Prop ≝ 1012 soundly_labelled_pc (f_graph fn) (f_entry fn). 912 1013 913 1014 … … 921 1022  Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False  cons f _ ⇒ soundly_labelled_frame f ] 922 1023 ]. 1024 923 1025 definition frame_steps_to_label_bound : frame → nat → Prop ≝ 924 1026 λf. steps_to_label_bound (f_graph (func f)) (next f). 925 1027 926 1028 inductive state_steps_to_label_bound : state → nat → Prop ≝ 927  sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) (n*2)928  sstlb_call : ∀fd,args,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Callstate fd args dst (f::fs) m) (S (n*2))929  sstlb_ret : ∀rtv,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Returnstate rtv dst (f::fs) m) (S (n*2))1029  sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) n 1030  sstlb_call : ∀fd,args,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Callstate fd args dst (f::fs) m) (S n) 1031  sstlb_ret : ∀rtv,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Returnstate rtv dst (f::fs) m) (S n) 930 1032 . 1033 1034 lemma state_steps_to_label_bound_zero : ∀s. 1035 ¬ state_steps_to_label_bound s O. 1036 #s % #H inversion H 1037 [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct 1038 inversion H52 1039 [ #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct 1040  #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 normalize in H74; destruct 1041 ] 1042  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct 1043  #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct 1044 ] qed. 1045 1046 lemma eval_steps : ∀ge,f,fs,m,tr,s'. 1047 eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 → 1048 steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) = 1049 match s' with [ State _ _ _ ⇒ 1  Callstate _ _ _ _ _ ⇒ 2  Returnstate _ _ _ _ ⇒ 2 ]. 1050 #ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s' 1051 whd in ⊢ (??%? → ?); 1052 generalize in ⊢ (??(?%)? → ?); cases (lookup_present ??? next next_ok) 1053 [ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl 1054  #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl 1055  #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1056  #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1057  #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1058  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl 1059  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl 1060  #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl 1061  #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl 1062  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl 1063  #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev 1064 cases v [ #E normalize in E; destruct  #sz #i  #f #E normalize in E; destruct  #r #E normalize in E; destruct  #p #E normalize in E; destruct ] 1065 whd in ⊢ (??%? → ?); 1066 generalize in ⊢ (??(?%)? → ?); 1067 cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [ _ ⇒ ?  _ ⇒ ? ] ?)? → ?); 1068 [ #e #E normalize in E; destruct 1069  #l #El whd in ⊢ (??%? → ?); #E destruct @refl 1070 ] 1071  #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl 1072 ] qed. 1073 1074 lemma state_steps_to_label_bound_step : ∀ge,s,tr,s',n. 1075 state_steps_to_label_bound s (S n) → 1076 eval_statement ge s = Value ??? 〈tr, s'〉 → 1077 RTLabs_cost s = false → 1078 (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨ 1079 state_steps_to_label_bound s' n. 1080 #ge #s #tr #s' #n #STEPS inversion STEPS 1081 [ #f #fs #m #m #FS #E1 #E2 #_ destruct 1082 #EVAL cases (eval_successor … EVAL) 1083 [ /3/ 1084  * #l * #S1 #S2 #NC %2 1085 cases (steps_to_label_bound_inv_step … FS … l S2) 1086 [ 2: change with (RTLabs_cost (State f fs m)) in ⊢ (?(?%)); >NC % // ] 1087 #n' 1088 inversion (eval_perserves … EVAL) 1089 [ #ge0 #f0 #f' #fs' #m0 #m' #F #E1 #E2 #E3 #_ destruct 1090 >(eval_steps … EVAL) * >commutative_plus #En normalize in En; 1091 whd in S1:(??%?); 1092 #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct 1093 %1 @H 1094  #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct 1095 >(eval_steps … EVAL) * >commutative_plus #En normalize in En; 1096 whd in S1:(??%?); 1097 #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct 1098 %2 // 1099  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 1100 destruct 1101  #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 destruct 1102 normalize in S1; destruct 1103  #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 destruct 1104 ] 1105 ] 1106  #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct 1107 /3/ 1108  #rtv #dst #f #fs #m #n' #FS #E1 #E2 #_ destruct 1109 #EVAL #NC %2 inversion (eval_perserves … EVAL) 1110 [ #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct 1111  #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 destruct 1112  #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct 1113  #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct 1114  #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct 1115 %1 whd in FS ⊢ %; 1116 inversion (stack_preserved_return … EVAL) [ @refl  #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct ] 1117 #s1 #f1 #f2 #fs #m #FE #SS1 #_ #E1 #E2 #_ destruct <FE 1118 inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct  #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct  #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ] 1119 inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct 1120 @FS 1121 ] 1122 ] qed. 1123 931 1124 932 1125 (* … … 1017 1210 (LABEL_LIMIT: state_steps_to_label_bound s n) 1018 1211 on n : finite_prefix ge s ≝ 1019 match n return λn. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S n) = Some ? s' ∧ RTLabs_cost s' = true)→ finite_prefix ge s with1020 [ O ⇒ λ STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ?1021  S n' ⇒ 1022 match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S (S n')) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with1212 match n return λn. state_steps_to_label_bound s n → finite_prefix ge s with 1213 [ O ⇒ λLABEL_LIMIT. ⊥ 1214  S n' ⇒ 1215 match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → state_steps_to_label_bound s (S n') → finite_prefix ge s with 1023 1216 [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥ 1024 1217  ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. … … 1029 1222 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' 1030 1223  false ⇒ λCS. 1031 let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ?? LABEL_LIMITin1224 let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ??? in 1032 1225 fp_add_default ge ?? CL fs ? CS 1033 1226 ] (refl ??) 1034 1227  cl_jump ⇒ λCL. 1035 1228 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' 1036  cl_call ⇒ λCL. 1229  cl_call ⇒ λCL.?(* 1037 1230 match ORACLE ge O next trace' return λ_. finite_prefix ge start with 1038 1231 [ or_introl TERMINATES ⇒ … … 1048 1241  or_intror NO_TERMINATION ⇒ 1049 1242 fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace') 1050 ] 1243 ]*) 1051 1244  cl_return ⇒ λCL. ⊥ 1052 1245 ] (refl ??) 1053 1246  ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥ 1054 ] 1055 ] STATE_COSTLABELLED NO_TERMINATIONLABEL_LIMIT.1056 [ 1057  2,17: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct1247 ] STATE_COSTLABELLED NO_TERMINATION 1248 ] LABEL_LIMIT. 1249 [ cases (state_steps_to_label_bound_zero s) /2/ 1250  (* TODO: how do we know that we're not at the final state? *) 1058 1251  @(absurd ?? NO_TERMINATION) 1059 1252 %{0} % @wr_base // 1060 1253  @(well_cost_labelled_jump … EV) // 1254  5,6,8,9,10: /2/ 1255  1256  @(well_cost_labelled_state_step … EV) // 1257  @(not_to_not … NO_TERMINATION) 1258 * #depth * #TERM %{depth} % @wr_step /2/ 1259  cases (state_steps_to_label_bound_step … LABEL_LIMIT EV ?) 1260 1261 @(well_cost_labelled_call … EV) // 1262  1263 2,14: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct 1061 1264  5,6,8: /2/ 1062 1265  1063  1064  @(well_cost_labelled_state_step … EV) // 1065  @(well_cost_labelled_call … EV) // 1266 *) 1066 1267  12,13,14: /2/ 1067 1268  @(well_cost_labelled_state_step … EV) // 
src/RTLabs/syntax.ma
r1680 r1705 96 96 97 97 98 (* Define a notion of sound labellings of RTLabs programs. *)99 100 let rec successors (s : statement) : list label ≝101 match s with102 [ St_skip l ⇒ [l]103  St_cost _ l ⇒ [l]104  St_const _ _ l ⇒ [l]105  St_op1 _ _ _ _ _ l ⇒ [l]106  St_op2 _ _ _ _ l ⇒ [l]107  St_load _ _ _ l ⇒ [l]108  St_store _ _ _ l ⇒ [l]109  St_call_id _ _ _ l ⇒ [l]110  St_call_ptr _ _ _ l ⇒ [l]111 (*112  St_tailcall_id _ _ ⇒ [ ]113  St_tailcall_ptr _ _ ⇒ [ ]114 *)115  St_cond _ l1 l2 ⇒ [l1; l2]116  St_jumptable _ ls ⇒ ls117  St_return ⇒ [ ]118 ].119 120 definition is_cost_label : statement → bool ≝121 λs. match s with [ St_cost _ _ ⇒ true  _ ⇒ false ].122 123 inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝124  stlb_refl : ∀l,n,H. is_cost_label (lookup_present … g l H) → steps_to_label_bound g l n125  stlb_step : ∀l,n,H.126 (∀l'. Exists label (λl0. l0 = l') (successors (lookup_present … g l H)) → steps_to_label_bound g l' n) →127 steps_to_label_bound g l (S n).128 129 discriminator nat.130 131 lemma steps_to_label_bound_inv_step : ∀g,l,n.132 steps_to_label_bound g l n →133 ∀H. ¬ (bool_to_Prop (is_cost_label (lookup_present … g l H))) →134 (∀l'. Exists label (λl0. l0 = l') (successors (lookup_present … g l H)) → steps_to_label_bound g l' (pred n)).135 #g #l0 #n0 #H1 inversion H1136 [ #l #n #H2 #C #E1 #E2 #_ destruct #H3 #H4 @⊥ @(absurd ? C H4)137  #l #n #H2 #IH #_ #E1 #E2 #_ destruct #H3 #NC @IH138 ] qed.139 140 definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.141 142 let rec soundly_labelled_fn (fn : internal_function) : Prop ≝143 soundly_labelled_pc (f_graph fn) (f_entry fn).144
Note: See TracChangeset
for help on using the changeset viewer.