Changeset 1675

Timestamp:

Feb 6, 2012, 3:33:52 PM (6 years ago)

Author:

campbell

Message:

Some work on sound labelled for RTLabs.

Location:

src/RTLabs

Files:

• Traces.ma (modified) (3 diffs)
• syntax.ma (modified) (1 diff)

src/RTLabs/Traces.ma

@@ -19 +19 @@
 | Returnstate _ _ _ _ ⇒ cl_return
 ].
-
-definition is_cost_label : statement → bool ≝
-λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
 
 definition RTLabs_cost : state → bool ≝
@@ -769 +766 @@
 qed.
 
+
+
+definition soundly_labelled_frame : frame → Prop ≝
+λf. soundly_labelled_pc (f_graph (func f)) (next f).
+
+definition soundly_labelled_state : state → Prop ≝
+λs. match s with
+[ State f _ _ ⇒ soundly_labelled_frame f
+| Callstate _ _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
+| Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ]
+].
+definition frame_steps_to_label_bound : frame → nat → Prop ≝
+λf. steps_to_label_bound (f_graph (func f)) (next f).
+
+inductive state_steps_to_label_bound : state → nat → Prop ≝
+| sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) (n*2)
+| 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))
+| 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))
+.
+
+(*
+lemma state_steps_to_label_step : ∀ge,f,fs,m,n,tr,s'.
+  state_steps_to_label_bound (State f fs m) (S (S n)) →
+  ¬ (bool_to_Prop (RTLabs_cost (State f fs m))) →
+  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
+  state_steps_to_label_bound s' (match s' with [ State _ _ _ ⇒ n | _ ⇒ S n ]).
+#ge #f0 #fs0 #m0 #n0 #tr #s' #H inversion H
+[ * #func #locals #next #next_ok #sp #dst #fs #m #n #H1 #E1 #E2 #_ destruct
+  cases n in H1 E2; [ #H1 #E2 normalize in E2; destruct | #n' #H1 #E2 normalize in E2; destruct ]
+  #NC whd in ⊢ (??%? → ?);
+  generalize in ⊢ (??(?%)? → ?);
+  lapply (steps_to_label_bound_inv_step … H1 next_ok NC)
+  cases (lookup_present ??? next next_ok)
+  [ #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl
+  | #cl #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl
+  | #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
+  | #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
+  | #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
+  | #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
+  | #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
+  | #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
+  | #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
+  | #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
+  | #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 ]
+  | #r #l1 #l2 #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
+  | #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 ]
+  | #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
+  ]
+*)
 (* When constructing an infinite trace, we need to be able to grab the finite
    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 *)
   (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))
-  (LABEL_LIMIT: ∃s'. And (nth_state ge s trace (S n) = Some ? s') (RTLabs_cost s' = true))
+  (LABEL_LIMIT: state_steps_to_label_bound s n)
   on n : finite_prefix ge s ≝
 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

@@ -88 +88 @@
 
 definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
+
+
+
+
+(* Define a notion of sound labellings of RTLabs programs. *)
+
+let rec successors (s : statement) : list label ≝
+match s with
+[ St_skip l ⇒ [l]
+| St_cost _ l ⇒ [l]
+| St_const _ _ l ⇒ [l]
+| St_op1 _ _ _ _ _ l ⇒ [l]
+| St_op2 _ _ _ _ l ⇒ [l]
+| St_load _ _ _ l ⇒ [l]
+| St_store _ _ _ l ⇒ [l]
+| St_call_id _ _ _ l ⇒ [l]
+| St_call_ptr _ _ _ l ⇒ [l]
+| St_tailcall_id _ _ ⇒ [ ]
+| St_tailcall_ptr _ _ ⇒ [ ]
+| St_cond _ l1 l2 ⇒ [l1; l2]
+| St_jumptable _ ls ⇒ ls
+| St_return ⇒ [ ]
+].
+
+definition is_cost_label : statement → bool ≝
+λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
+
+inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝
+| stlb_refl : ∀l,n,H. is_cost_label (lookup_present … g l H) → steps_to_label_bound g l n
+| stlb_step : ∀l,n,H.
+    (∀l'. Exists label (λl0. l0 = l') (successors (lookup_present … g l H)) → steps_to_label_bound g l' n) →
+    steps_to_label_bound g l (S n).
+    
+discriminator nat.
+
+lemma steps_to_label_bound_inv_step : ∀g,l,n.
+  steps_to_label_bound g l n →
+  ∀H. ¬ (bool_to_Prop (is_cost_label (lookup_present … g l H))) → 
+    (∀l'. Exists label (λl0. l0 = l') (successors (lookup_present … g l H)) → steps_to_label_bound g l' (pred n)).
+#g #l0 #n0 #H1 inversion H1
+[ #l #n #H2 #C #E1 #E2 #_ destruct #H3 #H4 @⊥ @(absurd ? C H4)
+| #l #n #H2 #IH #_ #E1 #E2 #_ destruct #H3 #NC @IH
+] qed.
+
+definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
+
+let rec soundly_labelled_fn (fn : internal_function) : Prop ≝
+  soundly_labelled_pc (f_graph fn) (f_entry fn).
+