Changeset 1563 for src/RTLabs
- Timestamp:
- Nov 25, 2011, 1:49:27 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/Traces.ma
r1559 r1563 7 7 (* NB: we do not consider jumps in the traces of RTLabs programs. *) 8 8 9 inductive RTLabs_classify : state → status_class → Prop ≝ 10 | rtla_other : ∀f,fs,m. RTLabs_classify (State f fs m) cl_other 11 | rtla_call : ∀a,b,c,d,e. RTLabs_classify (Callstate a b c d e) cl_call 12 | rtla_ret : ∀a,b,c,d. RTLabs_classify (Returnstate a b c d) cl_return 13 . 9 definition RTLabs_classify : state → status_class ≝ 10 λs. match s with 11 [ State _ _ _ ⇒ cl_other 12 | Callstate _ _ _ _ _ ⇒ cl_call 13 | Returnstate _ _ _ _ ⇒ cl_return 14 ]. 14 15 15 16 inductive RTLabs_stmt_cost : statement → Prop ≝ … … 26 27 state 27 28 (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉) 28 RTLabs_classify29 (λs,c. RTLabs_classify s = c) 29 30 RTLabs_cost 30 31 (λs,s'. match s with 31 32 [ dp s p ⇒ 32 match s return λs. RTLabs_classify s cl_call → ? with33 match s return λs. RTLabs_classify s = cl_call → ? with 33 34 [ Callstate fd args dst stk m ⇒ 34 35 λ_. match s' with … … 40 41 ] p 41 42 ]). 42 inversion H try #a try #b try #c try #d try #e try #f destruct 43 qed. 43 [ normalize in H; destruct 44 | normalize in H; destruct 45 ] qed. 44 46 45 47 (* Before attempting to construct a structured trace, let's show that we can … … 164 166 ] qed. 165 167 168 (* Need a way to choose whether a called function terminates. Then, 169 if the initial function terminates we generate a purely inductive structured trace, 170 otherwise we start generating the coinductive one, and on every function call 171 use the choice method again to decide whether to step over or keep going. 172 173 Not quite what we need - have to decide on seeing each label whether we will see 174 another or hit a non-terminating call? 175 176 Also - need the notion of well-labelled in order to break loops. 177 178 179 180 outline: 181 182 does function terminate? 183 - yes, get (bound on the number of steps until return), generate finite 184 structure using bound as termination witness 185 - no, get (¬ bound on steps to return), start building infinite trace out of 186 finite steps. At calls, check for termination, generate appr. form. 187 188 generating the finite parts: 189 190 We start with the status after the call has been executed; well-labelling tells 191 us that this is a labelled state. Now we want to generate a trace_label_return 192 and also return the remainder of the flat trace. 193 194 *) 195 196 (* [nth_is_return ge n depth s trace] says that after [n] steps of [trace] from 197 [s] we reach the return state for the current function. [depth] performs 198 the call/return counting necessary for handling deeper function calls. 199 It should be zero at the top level. *) 200 inductive nth_is_return (ge:genv) : nat → nat → ∀s. flat_trace io_out io_in ge s → Prop ≝ 201 | nir_step : ∀n,s,tr,s',depth,EX,trace. 202 RTLabs_classify s = cl_other → 203 nth_is_return ge n depth s' trace → 204 nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace) 205 | nir_call : ∀n,s,tr,s',depth,EX,trace. 206 RTLabs_classify s = cl_call → 207 nth_is_return ge n (S depth) s' trace → 208 nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace) 209 | nir_ret : ∀n,s,tr,s',depth,EX,trace. 210 RTLabs_classify s = cl_return → 211 nth_is_return ge n depth s' trace → 212 nth_is_return ge (S n) (S depth) s (ft_step ?? ge s tr s' EX trace) 213 | nir_base : ∀s,trace. 214 RTLabs_classify s = cl_return → 215 nth_is_return ge O O s trace 216 . 217 218 discriminator nat. 219 220 (* Find time until a nested call completes. *) 221 lemma nth_is_return_down : ∀ge,n,depth,s,trace. 222 nth_is_return ge n (S depth) s trace → 223 ∃m. nth_is_return ge m depth s trace. 224 #ge #n elim n 225 (* It's impossible to run out of time... *) 226 [ #depth #s #trace #H inversion H 227 [ #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct 228 | #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct 229 | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct 230 | #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct 231 ] 232 | #n' #IH #depth #s #trace #H inversion H 233 [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct 234 cases (IH depth s1' trace1 ?) 235 [ #m' #H' %{(S m')} %1 // 236 | // 237 ] 238 | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct 239 cases (IH (S depth) s1' trace1 ?) 240 [ #m' #H' %{(S m')} %2 // 241 | // 242 ] 243 | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct 244 cases (depth1) in H2 ⊢ %; 245 [ #H2 %{O} %4 // 246 | #depth' #H2 cases (IH depth' s1' trace1 ?) 247 [ #m' #H' %{(S m')} %3 // 248 | // 249 ] 250 ] 251 | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct 252 ] 253 ] qed. 254 255 lemma nth_is_return_call : ∀ge,n,s,tr,s',EX,trace. 256 RTLabs_classify s = cl_call → 257 nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) → 258 ∃m. nth_is_return ge m O s' trace. 259 #ge #n #s #tr #s' #EX #trace #CLASS #H 260 inversion H 261 [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥ 262 -H2 destruct >H1 in CLASS; #E destruct 263 | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct 264 @nth_is_return_down // 265 | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥ 266 -H2 destruct 267 | #s1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct 268 ] qed. 269 270 (* Is the only well-labelledness 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 *) 277 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) 280 : Σs'.Σremainder:flat_trace io_out io_in ge s'. 281 trace_label_return (RTLabs_status ge) s s' ≝ 282 ?.
Note: See TracChangeset
for help on using the changeset viewer.