Changeset 1595 for src/RTLabs
- Timestamp:
- Dec 7, 2011, 4:24:42 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/Traces.ma
r1594 r1595 204 204 *) 205 205 206 (* [ nth_is_return ge n depth s trace] says that after [n] steps of [trace] from207 [ s] we reach the return state for the current function. [depth] performs208 the call/return counting necessary for handling deeper function calls.209 It should be zero at the top level. *)210 inductive nth_is_return (ge:genv) : nat →nat → ∀s. flat_trace io_out io_in ge s → Prop ≝211 | nir_step : ∀n,s,tr,s',depth,EX,trace.206 (* [will_return ge depth s trace] says that after a finite number of steps of 207 [trace] from [s] we reach the return state for the current function. [depth] 208 performs the call/return counting necessary for handling deeper function 209 calls. It should be zero at the top level. *) 210 inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Prop ≝ 211 | wr_step : ∀s,tr,s',depth,EX,trace. 212 212 RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → 213 nth_is_return ge ndepth s' trace →214 nth_is_return ge (S n)depth s (ft_step ?? ge s tr s' EX trace)215 | nir_call : ∀n,s,tr,s',depth,EX,trace.213 will_return ge depth s' trace → 214 will_return ge depth s (ft_step ?? ge s tr s' EX trace) 215 | wr_call : ∀s,tr,s',depth,EX,trace. 216 216 RTLabs_classify s = cl_call → 217 nth_is_return ge n(S depth) s' trace →218 nth_is_return ge (S n)depth s (ft_step ?? ge s tr s' EX trace)219 | nir_ret : ∀n,s,tr,s',depth,EX,trace.217 will_return ge (S depth) s' trace → 218 will_return ge depth s (ft_step ?? ge s tr s' EX trace) 219 | wr_ret : ∀s,tr,s',depth,EX,trace. 220 220 RTLabs_classify s = cl_return → 221 nth_is_return ge ndepth s' trace →222 nth_is_return ge (S n)(S depth) s (ft_step ?? ge s tr s' EX trace)221 will_return ge depth s' trace → 222 will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace) 223 223 (* Note that we require the ability to make a step after the return (this 224 224 corresponds to somewhere that will be guaranteed to be a label at the 225 225 end of the compilation chain). *) 226 | nir_base : ∀s,tr,s',EX,trace.226 | wr_base : ∀s,tr,s',EX,trace. 227 227 RTLabs_classify s = cl_return → 228 nth_is_return ge OO s (ft_step ?? ge s tr s' EX trace)228 will_return ge O s (ft_step ?? ge s tr s' EX trace) 229 229 . 230 230 231 231 discriminator nat. 232 233 lemma will_return_call : ∀ge,depth,s,trace. 234 will_return ge depth s trace → 235 will_return ge (pred depth) s trace. 236 #ge #depth #s #trace #H elim H 237 [ #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %1 // 238 | #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %2 // 239 cases d in H1 H2 ⊢ %; // 240 | #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 241 cases d in H1 H2 ⊢ %; [ #H1 #H2 %4 // | /2/ ] 242 | #s1 #tr #s2 #EX #trc #CL %4 // 243 ] qed. 244 245 (* 246 (* If we'll return then we must return from calls. *) 247 lemma will_return_call : ∀ge,depth,s,trace. 248 will_return ge (S depth) s trace → 249 will_return ge depth s trace. 250 #ge #depth #s #trace #H elim H in ⊢ ?; 251 [ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/ 252 | #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/ 253 | #H204 #H205 #H206 #H207 #H208 #H209 #H210 #H211 #H212 #H213 /2/ 254 | #H215 #H216 #H217 #H218 #H219 #H220 #H221 255 inversion H221 256 [ #H223 #H224 #H225 #H226 #H227 #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 destruct >H220 in H229; * #E destruct 257 | #H237 #H238 #H239 #H240 #H241 #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 destruct >H220 in H243; #E destruct 258 | #H265 #H266 #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 destruct 259 | #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 destruct 260 ] qed. check will_return_call. 261 | #H130 #H131 #H132 #H133 #H134 #H135 262 inversion H 263 [ #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 #H199 #H200 #H201 #H202 destruct 264 cases H196 #E destruct 265 266 267 let rec will_return_call ge depth s trace (H:will_return ge (S depth) s trace) 268 on H : will_return ge depth s trace ≝ 269 match H return λSdepth,s,trace. λ_. S depth = Sdepth → will_return ge depth s trace with 270 [ wr_step s tr s' d EX trace CL H' ⇒ λE. wr_step ge s tr s' ? EX trace CL ? 271 | wr_call s tr s' d EX trace CL H' ⇒ λE. ? 272 | wr_ret s tr s' d EX trace CL H' ⇒ λE. ? 273 | wr_base s tr s' EX trace CL ⇒ λE. ? 274 ] (refl ? (S depth)). 275 [ @(match E return λx,E. will_return ? x ?? → will_return ge ??? with [ refl ⇒ λH''.? ] H') 276 @(will_return_call … H'') 277 | *: cases daemon ] qed. 278 | %2 /2/ 279 | destruct cases d in H' ⊢ %; 280 [ #H' @wr_base // 281 | #d' #H' %3 /2/ 282 ] 283 | destruct 284 ] qed. 285 286 (* If we'll return then we must return from calls. *) 287 lemma will_return_call : ∀ge,depth,s,trace. 288 will_return ge (S depth) s trace → 289 will_return ge depth s trace. 290 #ge #depth #s #trace #H lapply (refl ? (S depth)) 291 generalize in ⊢ (???(?%) → ??%??); elim H in ⊢ (∀_.???% → %); 292 [ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %1 /2/ 293 | #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %2 /2/ @H3 294 295 discriminator nat. 296 297 232 298 233 299 (* Find time until a nested call completes. *) … … 294 360 | #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 destruct 295 361 | #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 destruct >H130 in CL; #E destruct 362 ] qed. 363 *) 364 365 lemma will_return_notfn : ∀ge,s,tr,s',EX,trace. 366 RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → 367 will_return ge O s (ft_step ?? ge s tr s' EX trace) → 368 will_return ge O s' trace. 369 #ge #s #tr #s' #EX #trace * #CL #TERM inversion TERM 370 [ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct // 371 | #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 destruct >CL in H310; #E destruct 372 | #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 destruct 373 | #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 destruct >CL in H337; #E destruct 374 | #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct // 375 | #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 destruct >CL in H363; #E destruct 376 | #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 destruct 377 | #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 destruct >CL in H390; #E destruct 296 378 ] qed. 297 379 … … 407 489 ] qed. 408 490 491 lemma rtlabs_call_inv : ∀s. 492 RTLabs_classify s = cl_call → 493 ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m. 494 * [ #f #fs #m whd in ⊢ (??%? → ?); 495 cases (lookup_present … (next f) (next_ok f)) normalize 496 try #A try #B try #C try #D try #E try #F try #G destruct 497 | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl 498 | normalize #H411 #H412 #H413 #H414 #H415 destruct 499 ] qed. 500 501 lemma well_cost_labelled_call : ∀ge,s,tr,s'. 502 eval_statement ge s = Value ??? 〈tr,s'〉 → 503 well_cost_labelled_state s → 504 RTLabs_classify s = cl_call → 505 RTLabs_cost s' = true. 506 #ge #s #tr #s' #EV #WCL #CL 507 cases (rtlabs_call_inv s CL) 508 #fd * #args * #dst * #stk * #m #E >E in EV WCL; 509 whd in ⊢ (??%? → % → ?); 510 cases fd 511 [ #fn whd in ⊢ (??%? → % → ?); 512 @bindIO_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any) 513 #m' #b whd in ⊢ (??%? → ?); #E' destruct 514 * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3 515 @WCL2 516 | #fn whd in ⊢ (??%? → % → ?); 517 @bindIO_value #evargs #Eargs 518 @bindIO_value #evres #Eres 519 normalize in Eres; destruct 520 ] qed. 409 521 410 522 (* Don't need to know that labels break loops because we have termination. *) … … 412 524 record trace_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ { 413 525 new_state : state; 414 termination_count : nat;415 526 remainder : flat_trace io_out io_in ge new_state; 416 527 cost_labelled : well_cost_labelled_state new_state; … … 424 535 (* We handle returns specially *) 425 536 match ends with 426 [ doesnt_end_with_ret ⇒ nth_is_return ge (termination_count ?? trace_res)O (new_state ?? trace_res) (remainder ?? trace_res)537 [ doesnt_end_with_ret ⇒ will_return ge O (new_state ?? trace_res) (remainder ?? trace_res) 427 538 | ends_with_ret ⇒ True 428 539 ] … … 436 547 (mk_trace_result ge (T2 (ends … r)) 437 548 (new_state … r) 438 (termination_count … r)439 549 (remainder … r) 440 550 (cost_labelled … r) … … 449 559 mk_trace_result ge T2 450 560 (new_state … r) 451 (termination_count … r)452 561 (remainder … r) 453 562 (cost_labelled … r) … … 455 564 . 456 565 457 let rec make_label_return nge s566 let rec make_label_return ge s 458 567 (trace: flat_trace io_out io_in ge s) 459 568 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 460 569 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 461 570 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 462 (TERMINATES: nth_is_return ge nO s trace)571 (TERMINATES: will_return ge O s trace) 463 572 : trace_result ge (trace_label_return (RTLabs_status ge) s) ≝ 464 573 465 let r ≝ make_label_label n ge s trace ????in574 let r ≝ make_label_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES in 466 575 match ends … r return λx. trace_label_label ? x ?? → match x with [doesnt_end_with_ret⇒ ?|_⇒ ?] → ? with 467 576 [ ends_with_ret ⇒ λtll,term. 468 577 replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll) 469 578 | doesnt_end_with_ret ⇒ λtll,term. 470 let r' ≝ make_label_return (termination_count … r)ge (new_state … r)471 (remainder … r) ??? term in579 let r' ≝ make_label_return ge (new_state … r) 580 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? term in 472 581 replace_trace … r' 473 582 (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r')) 474 583 ] (new_trace … r) (terminates … r) 475 584 476 and make_label_label nge s585 and make_label_label ge s 477 586 (trace: flat_trace io_out io_in ge s) 478 587 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 479 588 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 480 589 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 481 (TERMINATES: nth_is_return ge nO s trace)590 (TERMINATES: will_return ge O s trace) 482 591 : sub_trace_result ge (λends. trace_label_label (RTLabs_status ge) ends s) ≝ 483 let r ≝ make_any_label n ge s trace ???in592 let r ≝ make_any_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES in 484 593 replace_sub_trace ??? r 485 594 (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) 486 595 487 and make_any_label nge s596 and make_any_label ge s 488 597 (trace: flat_trace io_out io_in ge s) 489 598 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 490 599 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 491 (TERMINATES: nth_is_return ge nO s trace)600 (TERMINATES: will_return ge O s trace) 492 601 : sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) ≝ 493 match trace return λs,trace. well_cost_labelled_state s → nth_is_return ???? trace → sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) with602 match trace return λs,trace. well_cost_labelled_state s → will_return ??? trace → sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) with 494 603 [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ? 495 604 | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES. … … 498 607 match RTLabs_cost next return λx. RTLabs_cost next = x → ? with 499 608 [ true ⇒ λCS. 500 mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next (pred n)trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ?609 mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ? 501 610 | false ⇒ λCS. 502 let r ≝ make_any_label (pred n)ge next trace' ENV_COSTLABELLED ?? in611 let r ≝ make_any_label ge next trace' ENV_COSTLABELLED ?? in 503 612 replace_sub_trace ??? r 504 613 (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??) 505 614 ] (refl ??) 506 615 | cl_jump ⇒ λCL. 507 mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next (pred n) trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ? 508 | cl_call ⇒ λCL. ? 616 mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ? 617 | cl_call ⇒ λCL. 618 let r ≝ make_label_return ge next trace' ENV_COSTLABELLED ??? in 619 let r' ≝ make_any_label ge (new_state … r) (remainder … r) ENV_COSTLABELLED ?? in 620 replace_sub_trace ??? r' 621 (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r')) 509 622 | cl_return ⇒ λCL. 510 mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) ends_with_ret (mk_trace_result ge ? next (pred n)trace' ? (tal_base_return (RTLabs_status ge) start next ? CL)) ?623 mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) ends_with_ret (mk_trace_result ge ? next trace' ? (tal_base_return (RTLabs_status ge) start next ? CL)) ? 511 624 ] (refl ? (RTLabs_classify start)) 512 625 | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥ 513 626 ] STATE_COSTLABELLED TERMINATES. 514 627 515 [ // 516 | // 517 | @(trace_label_label_label … tll) 518 | // 519 | // 520 | // 521 | // 522 | // 523 | // 524 | // 628 [ @(trace_label_label_label … tll) 525 629 | 526 630 | %{tr} @EV … … 531 635 | @(well_cost_labelled_jump … EV) // 532 636 | @(well_cost_labelled_state_step … EV) // 533 | @(nth_is_return_notfn … TERMINATES) %2 @CL 637 | @(will_return_notfn … TERMINATES) %2 @CL 638 | (* oh dear *) 639 | %{tr} @EV 640 | @(cost_labelled … r) 534 641 | 535 | %{tr} @EV 642 | 643 | 644 645 @(well_cost_labelled_state_step … EV) // 536 646 | % whd in ⊢ (% → ?); >CL #E destruct 537 647 | @CS 538 | @(well_cost_labelled_state_step … EV) //539 648 | @(nth_is_return_notfn … TERMINATES) %1 @CL 540 649 | % whd in ⊢ (% → ?); >CS #E destruct
Note: See TracChangeset
for help on using the changeset viewer.