Changeset 1583 for src/RTLabs/Traces.ma
 Timestamp:
 Dec 2, 2011, 1:02:08 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1574 r1583 20 20 ]. 21 21 22 inductive RTLabs_stmt_cost : statement → Prop ≝ 23  stmt_cost : ∀c,l. RTLabs_stmt_cost (St_cost c l). 24 25 inductive RTLabs_cost : state → Prop ≝ 26  cost_instr : ∀f,fs,m. 27 RTLabs_stmt_cost (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) → 28 RTLabs_cost (State f fs m). 22 definition RTLabs_cost : state → bool ≝ 23 λs. match s with 24 [ State f fs m ⇒ 25 match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with 26 [ St_cost c l ⇒ true 27  _ ⇒ false 28 ] 29  _ ⇒ false 30 ]. 29 31 30 32 definition RTLabs_status : genv → abstract_status ≝ … … 34 36 (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉) 35 37 (λs,c. RTLabs_classify s = c) 36 RTLabs_cost38 (λs. RTLabs_cost s = true) 37 39 (λs,s'. match s with 38 40 [ dp s p ⇒ … … 219 221 nth_is_return ge n depth s' trace → 220 222 nth_is_return ge (S n) (S depth) s (ft_step ?? ge s tr s' EX trace) 221  nir_base : ∀s,trace. 223 (* Note that we require the ability to make a step after the return (this 224 corresponds to somewhere that will be guaranteed to be a label at the 225 end of the compilation chain). *) 226  nir_base : ∀s,tr,s',EX,trace. 222 227 RTLabs_classify s = cl_return → 223 nth_is_return ge O O s trace228 nth_is_return ge O O s (ft_step ?? ge s tr s' EX trace) 224 229 . 225 230 … … 273 278  #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥ 274 279 H2 destruct 275  #s1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct 280  #s1 #tr1 #s1' #EX1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct 281 ] qed. 282 283 lemma nth_is_return_notfn : ∀ge,n,s,tr,s',EX,trace. 284 RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → 285 nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) → 286 nth_is_return ge (pred n) O s' trace. 287 #ge #n #s #tr #s' #EX #trace * #CL #TERM inversion TERM 288 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // 289  #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct >H40 in CL; #E destruct 290  #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 destruct 291  #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct >H70 in CL; #E destruct 292  #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 destruct // 293  #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct >H100 in CL; #E destruct 294  #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 destruct 295  #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 destruct >H130 in CL; #E destruct 276 296 ] qed. 277 297 … … 313 333 314 334 definition well_cost_labelled_ge : genv → Prop ≝ 315 λge. ∀ v,f. find_funct ?? ge v= Some ? (Internal ? f) → well_cost_labelled_fn f.335 λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f. 316 336 317 337 definition well_cost_labelled_state : state → Prop ≝ … … 322 342  Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs 323 343 ]. 344 345 lemma well_cost_labelled_state_step : ∀ge,s,tr,s'. 346 eval_statement ge s = Value ??? 〈tr,s'〉 → 347 well_cost_labelled_ge ge → 348 well_cost_labelled_state s → 349 well_cost_labelled_state s'. 350 #ge #s #tr' #s' #EV cases (eval_perserves … EV) 351 [ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % // 352  #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/ 353  #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/ 354  #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/ 355  #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2 356  #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % // 357 ] qed. 324 358 325 359 (* Don't need to know that labels break loops because we have termination. *) … … 349 383 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 350 384 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 351 (STATEMENT_COSTLABEL: RTLabs_cost s )(* current statement is a cost label *)385 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 352 386 (TERMINATES: nth_is_return ge n O s trace) 353 387 : make_result ge (trace_label_return (RTLabs_status ge) s) ≝ … … 371 405 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 372 406 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 373 (STATEMENT_COSTLABEL: RTLabs_cost s )(* current statement is a cost label *)407 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 374 408 (TERMINATES: nth_is_return ge n O s trace) 375 409 : make_result ge (λs'. Σends. trace_label_label (RTLabs_status ge) ends s s') ≝ … … 387 421 (TERMINATES: nth_is_return ge n O s trace) 388 422 : make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') ≝ 389 match trace return λs,trace. nth_is_return ???? trace → make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') with 390 [ ft_stop st FINAL ⇒ λTERMINATES. ? 391  ft_step start tr next EV trace' ⇒ λTERMINATES. ? 392  ft_wrong start m EV ⇒ λTERMINATES. ⊥ 393 ] TERMINATES. 423 match trace return λs,trace. well_cost_labelled_state s → nth_is_return ???? trace → make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') with 424 [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ? 425  ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES. 426 match RTLabs_classify start return λx. RTLabs_classify start = x → ? with 427 [ cl_other ⇒ λCL. 428 match RTLabs_cost next return λx. RTLabs_cost next = x → ? with 429 [ true ⇒ λCS. 430 mk_make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends start s') next (pred n) trace' ?? (dp ?? doesnt_end_with_ret (tal_base_not_return (RTLabs_status ge) start next ???)) 431  false ⇒ λCS. 432 let r ≝ make_any_label (pred n) ge next trace' ENV_COSTLABELLED ?? in 433 match new_trace … r with 434 [ dp ends trc ⇒ 435 replace_new_trace ??? r 436 (dp ?? ends (tal_step_default (RTLabs_status ge) ends start next (new_state … r) ? trc ??)) 437 ] 438 ] (refl ??) 439  cl_jump ⇒ λCL. ? 440  cl_call ⇒ λCL. ? 441  cl_return ⇒ λCL. ? 442 ] (refl ? (RTLabs_classify start)) 443  ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥ 444 ] STATE_COSTLABELLED TERMINATES. 394 445 395 446 [ // … … 405 456  406 457  458  459  460  @(nth_is_return_notfn … TERMINATES) %1 @CL 461  @(well_cost_labelled_state_step … EV) // 462  %{tr} @EV 463  464  @CS 465  %{tr} @EV 466  @CL 467  % whd in ⊢ (% → ?); >CS #E destruct 468  @(well_cost_labelled_state_step … EV) // 469  @(nth_is_return_notfn … TERMINATES) %1 @CL 407 470  inversion TERMINATES 408 471 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 TERMINATES destruct 409 472  #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 TERMINATES destruct 410 473  #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 TERMINATES destruct 411  #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 TERMINATES destruct 474  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 TERMINATES destruct 475 ] 476  477 478 412 479 413 (* Now we're in trouble  if we're at the end of the function we don't have the 414 required guarantee that we can make another step. In particular, there isn't 415 one at the end of the program. *) 480 (* FIXME: there's trouble at the end of the program because we can't make a step 481 away from the final return. *)
Note: See TracChangeset
for help on using the changeset viewer.