Changeset 1675


Ignore:
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:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1671 r1675  
    1919| Returnstate _ _ _ _ ⇒ cl_return
    2020].
    21 
    22 definition is_cost_label : statement → bool ≝
    23 λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
    2421
    2522definition RTLabs_cost : state → bool ≝
     
    769766qed.
    770767
     768
     769
     770definition soundly_labelled_frame : frame → Prop ≝
     771λf. soundly_labelled_pc (f_graph (func f)) (next f).
     772
     773definition 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].
     779definition frame_steps_to_label_bound : frame → nat → Prop ≝
     780λf. steps_to_label_bound (f_graph (func f)) (next f).
     781
     782inductive 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(*
     789lemma 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*)
    771817(* When constructing an infinite trace, we need to be able to grab the finite
    772818   portion of the trace for the next [trace_label_diverges] constructor.  We
     
    825871  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
    826872  (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)
    828874  on n : finite_prefix ge s ≝
    829875match 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  
    8888
    8989definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
     90
     91
     92
     93
     94(* Define a notion of sound labellings of RTLabs programs. *)
     95
     96let rec successors (s : statement) : list label ≝
     97match 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
     114definition is_cost_label : statement → bool ≝
     115λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
     116
     117inductive 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   
     123discriminator nat.
     124
     125lemma 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
     134definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
     135
     136let 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.