Changeset 1675
- Timestamp:
- Feb 6, 2012, 3:33:52 PM (6 years ago)
- Location:
- src/RTLabs
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/Traces.ma
r1671 r1675 19 19 | Returnstate _ _ _ _ ⇒ cl_return 20 20 ]. 21 22 definition is_cost_label : statement → bool ≝23 λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].24 21 25 22 definition RTLabs_cost : state → bool ≝ … … 769 766 qed. 770 767 768 769 770 definition soundly_labelled_frame : frame → Prop ≝ 771 λf. soundly_labelled_pc (f_graph (func f)) (next f). 772 773 definition soundly_labelled_state : state → Prop ≝ 774 λs. match s with 775 [ State f _ _ ⇒ soundly_labelled_frame f 776 | Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ] 777 | Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ] 778 ]. 779 definition frame_steps_to_label_bound : frame → nat → Prop ≝ 780 λf. steps_to_label_bound (f_graph (func f)) (next f). 781 782 inductive state_steps_to_label_bound : state → nat → Prop ≝ 783 | sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) (n*2) 784 | 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)) 785 | 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)) 786 . 787 788 (* 789 lemma state_steps_to_label_step : ∀ge,f,fs,m,n,tr,s'. 790 state_steps_to_label_bound (State f fs m) (S (S n)) → 791 ¬ (bool_to_Prop (RTLabs_cost (State f fs m))) → 792 eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 → 793 state_steps_to_label_bound s' (match s' with [ State _ _ _ ⇒ n | _ ⇒ S n ]). 794 #ge #f0 #fs0 #m0 #n0 #tr #s' #H inversion H 795 [ * #func #locals #next #next_ok #sp #dst #fs #m #n #H1 #E1 #E2 #_ destruct 796 cases n in H1 E2; [ #H1 #E2 normalize in E2; destruct | #n' #H1 #E2 normalize in E2; destruct ] 797 #NC whd in ⊢ (??%? → ?); 798 generalize in ⊢ (??(?%)? → ?); 799 lapply (steps_to_label_bound_inv_step … H1 next_ok NC) 800 cases (lookup_present ??? next next_ok) 801 [ #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl 802 | #cl #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl 803 | #r #cs #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #E3 @bind_ok #locals' #E4 whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl 804 | #t1 #t2 #op #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl 805 | #op #r1 #r2 #r3 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl 806 | #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl 807 | #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct normalize %1 whd @H2 %1 @refl 808 | #id #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl 809 | #r #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl 810 | #id #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl 811 | #r #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] 812 | #r #l1 #l2 #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % % 813 | #r #ls #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ] 814 | #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5 815 ] 816 *) 771 817 (* When constructing an infinite trace, we need to be able to grab the finite 772 818 portion of the trace for the next [trace_label_diverges] constructor. We … … 825 871 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 826 872 (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace))) 827 (LABEL_LIMIT: ∃s'. And (nth_state ge s trace (S n) = Some ? s') (RTLabs_cost s' = true))873 (LABEL_LIMIT: state_steps_to_label_bound s n) 828 874 on n : finite_prefix ge s ≝ 829 875 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 with -
src/RTLabs/syntax.ma
r1626 r1675 88 88 89 89 definition RTLabs_program ≝ program (λ_.fundef internal_function) nat. 90 91 92 93 94 (* Define a notion of sound labellings of RTLabs programs. *) 95 96 let rec successors (s : statement) : list label ≝ 97 match s with 98 [ St_skip l ⇒ [l] 99 | St_cost _ l ⇒ [l] 100 | St_const _ _ l ⇒ [l] 101 | St_op1 _ _ _ _ _ l ⇒ [l] 102 | St_op2 _ _ _ _ l ⇒ [l] 103 | St_load _ _ _ l ⇒ [l] 104 | St_store _ _ _ l ⇒ [l] 105 | St_call_id _ _ _ l ⇒ [l] 106 | St_call_ptr _ _ _ l ⇒ [l] 107 | St_tailcall_id _ _ ⇒ [ ] 108 | St_tailcall_ptr _ _ ⇒ [ ] 109 | St_cond _ l1 l2 ⇒ [l1; l2] 110 | St_jumptable _ ls ⇒ ls 111 | St_return ⇒ [ ] 112 ]. 113 114 definition is_cost_label : statement → bool ≝ 115 λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ]. 116 117 inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝ 118 | stlb_refl : ∀l,n,H. is_cost_label (lookup_present … g l H) → steps_to_label_bound g l n 119 | stlb_step : ∀l,n,H. 120 (∀l'. Exists label (λl0. l0 = l') (successors (lookup_present … g l H)) → steps_to_label_bound g l' n) → 121 steps_to_label_bound g l (S n). 122 123 discriminator nat. 124 125 lemma steps_to_label_bound_inv_step : ∀g,l,n. 126 steps_to_label_bound g l n → 127 ∀H. ¬ (bool_to_Prop (is_cost_label (lookup_present … g l H))) → 128 (∀l'. Exists label (λl0. l0 = l') (successors (lookup_present … g l H)) → steps_to_label_bound g l' (pred n)). 129 #g #l0 #n0 #H1 inversion H1 130 [ #l #n #H2 #C #E1 #E2 #_ destruct #H3 #H4 @⊥ @(absurd ? C H4) 131 | #l #n #H2 #IH #_ #E1 #E2 #_ destruct #H3 #NC @IH 132 ] qed. 133 134 definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n. 135 136 let rec soundly_labelled_fn (fn : internal_function) : Prop ≝ 137 soundly_labelled_pc (f_graph fn) (f_entry fn). 138
Note: See TracChangeset
for help on using the changeset viewer.