Changeset 1565
 Timestamp:
 Nov 25, 2011, 5:30:20 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1563 r1565 5 5 discriminator status_class. 6 6 7 (* NB: we do not consider jumps in the traces of RTLabs programs. *) 7 (* NB: For RTLabs we only classify branching behaviour as jumps. Other jumps 8 will be added later (LTL → LIN). *) 8 9 9 10 definition RTLabs_classify : state → status_class ≝ 10 11 λs. match s with 11 [ State _ _ _ ⇒ cl_other 12 [ State f _ _ ⇒ 13 match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with 14 [ St_cond _ _ _ ⇒ cl_jump 15  St_jumptable _ _ ⇒ cl_jump 16  _ ⇒ cl_other 17 ] 12 18  Callstate _ _ _ _ _ ⇒ cl_call 13 19  Returnstate _ _ _ _ ⇒ cl_return … … 42 48 ]). 43 49 [ normalize in H; destruct 44  normalize in H; destruct 50  whd in H:(??%?); 51 cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H; 52 normalize try #a try #b try #c try #d try #e try #g try #h destruct 45 53 ] qed. 46 54 … … 200 208 inductive nth_is_return (ge:genv) : nat → nat → ∀s. flat_trace io_out io_in ge s → Prop ≝ 201 209  nir_step : ∀n,s,tr,s',depth,EX,trace. 202 RTLabs_classify s = cl_other →210 RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → 203 211 nth_is_return ge n depth s' trace → 204 212 nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace) … … 259 267 #ge #n #s #tr #s' #EX #trace #CLASS #H 260 268 inversion H 261 [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥269 [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 * #H1 #H2 #_ #E1 #E2 #E3 @⊥ 262 270 H2 destruct >H1 in CLASS; #E destruct 263 271  #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct … … 268 276 ] qed. 269 277 270 (* Is the only welllabelledness fact I need here that the current state is 271 labelled? That doesn't seem like it should be enough? 272 273 Is this because the insertion of labels after jumps in LTL → LIN takes care 274 of the cost proof's needs? Is the important thing that every branch is 275 followed by a label? The LTL → LIN stage then only adds labels at merges. 276 *) 278 (* We require that labels appear after branch instructions and at the start of 279 functions. *) 280 281 definition is_cost_label : statement → Prop ≝ 282 λs. match s with [ St_cost _ _ ⇒ True  _ ⇒ False ]. 283 284 let rec All_All A (P:A → Prop) (Q:∀a. P a → Prop) l (H:All A P l) on l : Prop ≝ 285 match l return λl.All A P l → Prop with 286 [ nil ⇒ λ_. True 287  cons h t ⇒ λH. Q h (proj1 … H) ∧ All_All A P Q t (proj2 … H) 288 ] H. 289 290 definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝ 291 λf,s. match s return λs. labels_present ? s → Prop with 292 [ St_cond _ l1 l2 ⇒ λH. 293 is_cost_label (lookup_present … (f_graph f) l1 ?) ∧ 294 is_cost_label (lookup_present … (f_graph f) l2 ?) 295  St_jumptable _ ls ⇒ λH. 296 All_All … (λl,H. is_cost_label (lookup_present … (f_graph f) l H)) ls H 297  _ ⇒ λ_. True 298 ]. whd in H; 299 [ @(proj1 … H) 300  @(proj2 … H) 301 ] qed. 302 303 definition well_cost_labelled_fn : internal_function → Prop ≝ 304 λf. (∀l,s. ∀H:lookup … (f_graph f) l = Some ? s. 305 well_cost_labelled_statement f s (f_closed f …)) ∧ 306 is_cost_label (lookup_present … (f_graph f) (f_entry f) ?). 307 [ 2: @H  skip  cases (f_entry f) // ] qed. 308 309 (* We need to ensure that any code we come across is wellcostlabelled. We may 310 get function code from either the global environment or the state. *) 311 312 definition well_cost_labelled_ge : genv → Prop ≝ 313 λge. ∀v,f. find_funct ?? ge v = Some ? (Internal ? f) → well_cost_labelled_fn f. 314 315 definition well_cost_labelled_state : state → Prop ≝ 316 λs. match s with 317 [ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs 318  Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn  External _ ⇒ True ] ∧ 319 All ? (λf. well_cost_labelled_fn (func f)) fs 320  Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs 321 ]. 322 277 323 let rec make_label_return n ge s 278 (trace:flat_trace io_out io_in ge s) 279 (TERMINATES:nth_is_return ge n O s trace) 324 (trace: flat_trace io_out io_in ge s) 325 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 326 (STATE_COSTLABELLED: well_cost_labelled_state s) 327 (TERMINATES: nth_is_return ge n O s trace) 280 328 : Σs'.Σremainder:flat_trace io_out io_in ge s'. 281 329 trace_label_return (RTLabs_status ge) s s' ≝
Note: See TracChangeset
for help on using the changeset viewer.