 Timestamp:
 Dec 7, 2011, 4:24:42 PM (10 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.