 Timestamp:
 Nov 25, 2011, 1:49:27 PM (8 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 nonterminating call? 175 176 Also  need the notion of welllabelled 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; welllabelling 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 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 *) 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.