Changeset 1682
 Timestamp:
 Feb 9, 2012, 1:22:33 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1681 r1682 446 446 447 447 (* The preservation of (most of) the stack is useful to show as_after_return. 448 This is a partial closure of the state_rel relation in semantics.ma  we only 449 accumulate information up to the first return. *) 448 We do this by showing that during the execution of a function the lower stack 449 frames never change, and that after returning from the function we preserve 450 the identity of the next instruction to execute. 451 *) 452 453 inductive stack_of_state : list frame → state → Prop ≝ 454  sos_State : ∀f,fs,m. stack_of_state fs (State f fs m) 455  sos_Callstate : ∀fd,args,dst,f,fs,m. stack_of_state fs (Callstate fd args dst (f::fs) m) 456  sos_Returnstate : ∀rtv,dst,fs,m. stack_of_state fs (Returnstate rtv dst fs m) 457 . 458 450 459 inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝ 451  sp_normal : ∀f,f',fs,m,m'. frame_rel f f' → stack_preserved doesnt_end_with_ret (State f fs m) (State f' fs m') 452  sp_to_call : ∀f,f',fs,m,m',fd,args,dst. frame_rel f f' → stack_preserved doesnt_end_with_ret (State f fs m) (Callstate fd args dst (f'::fs) m') 453 (* Remember that this is one *after* the state just considered, so the trace 454 doesn't end with return, the return is the next state *) 455  sp_to_return : ∀f,fs,m,rtv,dst,m'. stack_preserved doesnt_end_with_ret (State f fs m) (Returnstate rtv dst fs m') 456  sp_from_return : ∀f,f',fs,m,rtv,dst,m'. (next f = next f') → frame_rel f f' → stack_preserved ends_with_ret (Returnstate rtv dst (f::fs) m) (State f' fs m') 457 (* A combination of the above *) 458  sp_over_return : ∀f1,f2,f3,fs,m,m'. (next f2 = next f3) → frame_rel f2 f3 → stack_preserved ends_with_ret (State f1 (f2::fs) m) (State f3 fs m'). 459 460 lemma frame_rel_trans : transitive ? frame_rel. 461 #x #y #z * 462 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 inversion H10 463 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 destruct // 464 qed. 460  sp_normal : ∀fs,s1,s2. 461 stack_of_state fs s1 → 462 stack_of_state fs s2 → 463 stack_preserved doesnt_end_with_ret s1 s2 464  sp_finished : ∀s1,f,f',fs,m. 465 next f = next f' → 466 stack_of_state (f::fs) s1 → 467 stack_preserved ends_with_ret s1 (State f' fs m). 468 469 discriminator list. 470 471 lemma stack_of_state_eq : ∀fs,fs',s. 472 stack_of_state fs s → 473 stack_of_state fs' s → 474 fs = fs'. 475 #fs0 #fs0' #s0 * 476 [ #f #fs #m #H inversion H 477 #a #b #c #d #e #g try #h try #i try #j destruct @refl 478  #fd #args #dst #f #fs #m #H inversion H 479 #a #b #c #d #e #g try #h try #i try #j destruct @refl 480  #rtv #dst #fs #m #H inversion H 481 #a #b #c #d #e #g try #h try #i try #j destruct @refl 482 ] qed. 465 483 466 484 lemma stack_preserved_join : ∀e,s1,s2,s3. … … 469 487 stack_preserved e s1 s3. 470 488 #e1 #s1 #s2 #s3 #H1 inversion H1 471 [ #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct #H2 inversion H2 472 [ #f2 #f2' #fs2 #m2 #m2' #F2 #E1 #E2 #E3 #E4 destruct % /2/ 473  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 destruct %2 /2/ 474  #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 destruct /2/ 475  #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H145 #H146 destruct 476  #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H148 #H149 #H150 destruct /2/ 477 ] 478  #f #f' #fs #m #m' #fd #args #dst #F #E1 #E2 #E3 #E4 destruct #H2 inversion H2 479 [ #f2 #f2' #fs2 #m2 #m2' #F2 #H2' #E1 #E2 #E3 destruct 480  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 destruct 481  #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 destruct 482  #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H145 #H146 destruct 483  #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H148 #H149 destruct 484 ] 485  #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct #H2 inversion H2 486 [ #f2 #f2' #fs2 #m2 #m2' #F2 #H2' #E1 #E2 #E3 destruct 487  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct 488  #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 destruct 489  #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H151 #H152 destruct /2/ 490  #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H154 #H155 destruct 491 ] 492  #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 destruct 493  #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 destruct 494 ] qed. 495 496 lemma stack_preserved_ret : ∀ge,s1,s2,tr. 489 [ #fs #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct 490 #H2 inversion H2 491 [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct 492 @(sp_normal fs) // <(stack_of_state_eq … S1' S2) // 493  #s1'' #f #f' #fs' #m #N #S1' #E1 #E2 #E3 #E4 destruct 494 @(sp_finished … N) >(stack_of_state_eq … S1' S2) // 495 ] 496  #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct 497 ] qed. 498 499 lemma stack_preserved_return : ∀ge,s1,s2,tr. 497 500 RTLabs_classify s1 = cl_return → 498 501 eval_statement ge s1 = Value ??? 〈tr,s2〉 → … … 506 509 [ #m #s2 #tr #_ #EV whd in EV:(??%?); destruct 507 510  #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV 508 whd in EV:(??%?); destruct @ sp_from_return cases f//511 whd in EV:(??%?); destruct @(sp_finished ? f) // 509 512 ] 510 513 ] qed. … … 532 535 cases (rtlabs_call_inv … CL) 533 536 #fd * #args * #dst * #stk * #m #E destruct 537 inversion SP 538 [ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct 539  #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct 540 inversion (eval_perserves … EV) 541 [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct 542  #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct 543  #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct 544 inversion S 545 [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/ 546  #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct 547  #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct 548 ] 549  #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct 550  #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct 551 ] 552 ] qed. 553 554 lemma RTLabs_after_call : ∀ge,s1,s2,s3,tr. 555 ∀CL : RTLabs_classify s1 = cl_call. 556 eval_statement ge s1 = Value ??? 〈tr,s2〉 → 557 stack_preserved ends_with_ret s2 s3 → 558 as_after_return (RTLabs_status ge) «s1,CL» s3. 559 #ge #s1 #s2 #s3 #tr #CL #EV #S23 560 cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct 561 inversion S23 562 [ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct 563  #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct 564 inversion (eval_perserves … EV) 565 [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct 566  #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct 567  #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct 568 inversion S 569 [ #fy #fsy #my #E1 #E2 #E3 destruct @N 570  #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct 571  #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct 572 ] 573  #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct 574  #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct 575 ] 576 ] qed. 534 577 535 578 (* Don't need to know that labels break loops because we have termination. *) … … 749 792 this can't happen *) 750 793  @(will_return_return … CL TERMINATES) 751  /2 /794  /2 by stack_preserved_return/ 752 795  %{tr} @EV 753 796  @(well_cost_labelled_state_step … EV) // … … 758 801  @(well_cost_labelled_jump … EV) // 759 802  @(well_cost_labelled_state_step … EV) // 760  @ sp_over_return803  @(stack_preserved_call … EV (stack_ok … r)) // 761 804  %{tr} @EV 762  (* TODO oh dear *)805  @RTLabs_after_call // 763 806  cases (will_return_call … TERMINATES) #H @le_S_to_le 764  cases r #H1 #H2 #H3 #H4 * #H5807  cases r #H1 #H2 #H3 #H4 #H5 * #H6 765 808 cases (will_return_call … CL TERMINATES) 766 809 #TM #X #Y @le_S_to_le @(transitive_lt … Y X) 767  (* TODO oh dear *)810  @RTLabs_after_call // 768 811  %{tr} @EV 812  @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) // 769 813  @(cost_labelled … r) 770  cases r #H72 #H73 #H74 #H75 * #H76 #H78814  cases r #H72 #H73 #H74 #H75 #HX * #H76 #H78 771 815 @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) 772 816 cases (will_return_call … TERMINATES) in H78; … … 785 829 @(monotonic_le_times_r 3 … GT) 786 830  whd @(will_return_notfn … TERMINATES) %1 @CL 831  @(stack_preserved_step … EV) /2/ 787 832  %{tr} @EV 788 833  %2 whd @CL … … 791 836  @CL 792 837  %{tr} @EV 838  @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/ 793 839  @(well_cost_labelled_state_step … EV) // 794 840  %1 @CL … … 813 859 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 814 860 (TERMINATES: will_return ge depth s trace) 815 : trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝861 : trace_result ge depth ends_with_ret s (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝ 816 862 make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES 817 863 (2 + 3 * will_return_length … TERMINATES) ?.
Note: See TracChangeset
for help on using the changeset viewer.