Changeset 1713 for src/RTLabs/Traces.ma


Ignore:
Timestamp:
Feb 21, 2012, 11:58:12 AM (8 years ago)
Author:
campbell
Message:

Add a distinguished final state to the front-end languages to match up
with the structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1712 r1713  
    1818| Callstate _ _ _ _ _ ⇒ cl_call
    1919| Returnstate _ _ _ _ ⇒ cl_return
     20| Finalstate _ ⇒ cl_other
    2021].
    2122
     
    4344          λ_. match s' with
    4445          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
     46          | Finalstate r ⇒ True
    4547          | _ ⇒ False
    4648          ]
     
    5052      ]).
    5153[ normalize in H; destruct
     54| normalize in H; destruct
    5255| whd in H:(??%?);
    5356  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
     
    369372                          All ? (λf. well_cost_labelled_fn (func f)) fs
    370373| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
     374| Finalstate _ ⇒ True
    371375].
    372376
     
    385389| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
    386390| #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
     391| //
    387392] qed.
    388393
     
    404409| normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
    405410| normalize #H8 #H9 #H10 #H11 #H12 destruct
     411| #r #E normalize in E; destruct
    406412] qed.
    407413
     
    453459  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
    454460  | normalize #H411 #H412 #H413 #H414 #H415 destruct
     461  | normalize #H1 #H2 destruct
    455462  ] qed.
    456463
     
    497504    next f = next f' →
    498505    stack_of_state (f::fs) s1 →
    499     stack_preserved ends_with_ret s1 (State f' fs m).
     506    stack_preserved ends_with_ret s1 (State f' fs m)
     507| sp_stop : ∀e,s1,r.
     508    stack_preserved e s1 (Finalstate r)
     509.
    500510
    501511discriminator list.
     
    507517#fs0 #fs0' #s0 *
    508518[ #f #fs #m #H inversion H
    509   #a #b #c #d #e #g try #h try #i try #j destruct @refl
     519  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
    510520| #fd #args #dst #f #fs #m #H inversion H
    511   #a #b #c #d #e #g try #h try #i try #j destruct @refl
     521  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
    512522| #rtv #dst #fs #m #H inversion H
    513   #a #b #c #d #e #g try #h try #i try #j destruct @refl
     523  #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
     524] qed.
     525
     526lemma stack_preserved_final : ∀e,r,s.
     527  stack_preserved e (Finalstate r) s → ∃r'. s = Finalstate r'.
     528#e #r #s #H inversion H
     529[ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct
     530  inversion SOS #a #b #c #d #e #f try #g try #h destruct
     531| #H194 #H195 #H196 #H197 #H198 #H199 #SOS #H201 #H202 #H203 #H204 destruct
     532  inversion SOS #a #b #c #d #e #f try #g try #h destruct
     533| #e' #s' #r' #E1 #E2 #E3 #E4 destruct %{r'} @refl
    514534] qed.
    515535
     
    525545  | #s1'' #f #f' #fs' #m #N #S1' #E1 #E2 #E3 #E4 destruct
    526546    @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
     547  | #s1'' #r #E1 #E2 #E3 #E4 destruct //
    527548  ]
    528549| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
     550| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H
     551  cases (stack_preserved_final … H) #r #E destruct //
    529552] qed.
    530553
     
    539562| #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
    540563| #res #dst *
    541   [ #m #s2 #tr #_ #EV whd in EV:(??%?); destruct
     564  [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV; [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct // | *: normalize #a try #b destruct ] ]
    542565  | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV
    543566    whd in EV:(??%?); destruct @(sp_finished ? f) //
    544567  ]
     568| #r #s2 #tr #E normalize in E; destruct
    545569] qed.
    546570
     
    557581| #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL
    558582  #E normalize in E; destruct
     583| #ge #r #dst #m #E1 #E2 destruct @⊥ cases CL normalize #E destruct
    559584] qed.
    560585
     
    581606  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
    582607  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
    583   ]
     608  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
     609  ]
     610| #e #s1 #r #E1 #E2 #E3 #_ destruct //
    584611] qed.
    585612 
     
    605632  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
    606633  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
    607   ]
     634  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
     635  ]
     636| #e #s1 #r #E1 #E2 #E3 #E4 destruct //
    608637] qed.
    609638
     
    751780  match trace return λs,trace. well_cost_labelled_state s → ∀TM:will_return ??? trace. myge ? (times 3 (will_return_length ??? trace TM)) → sub_trace_result ge depth s trace (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
    752781  [ ft_stop st FINAL ⇒
    753       λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ?
     782      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
    754783
    755784  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
     
    836865| @le_S_S_to_le @TERMINATES_IN_TIME
    837866| @(wrl_nonzero … TERMINATES_IN_TIME)
    838 | (* Bad - we've reached the end of the trace; need to fix semantics so that
    839      this can't happen *)
     867| (* We can't reach the final state because the function terminates with a
     868     return *)
     869  inversion TERMINATES
     870  [ #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #_ -TERMINATES -TERMINATES destruct
     871  | #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 #H237 #H238 #H239 #H240 -TERMINATES -TERMINATES destruct
     872  | #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 -TERMINATES -TERMINATES destruct
     873  | #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 -TERMINATES -TERMINATES destruct
     874  ]
    840875| @(will_return_return … CL TERMINATES)
    841876| /2 by stack_preserved_return/
     
    902937  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 -TERMINATES -TERMINATES destruct
    903938  ]
    904 ] cases daemon qed.
     939] qed.
    905940
    906941(* We can initialise TIME with a suitably large value based on the length of the
     
    918953qed.
    919954 
    920 (* FIXME: there's trouble at the end of the program because we can't make a step
    921    away from the final return.
    922    
    923    We need to show that the "next pc" is preserved through a function call.
    924    
    925    Tail-calls are not handled properly (which means that if we try to show the
     955(* Tail-calls would not be handled properly (which means that if we try to show the
    926956   full version with non-termination we'll fail because calls and returns aren't
    927957   balanced.
     
    9901020| Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ]
    9911021| Returnstate _ _ _ _ ⇒ None ?
     1022| Finalstate _ ⇒ None ?
    9921023].
    9931024
     
    10981129  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
    10991130  steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =
    1100   match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 ].
     1131  match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ].
    11011132#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
    11021133whd in ⊢ (??%? → ?);
     
    11571188      normalize in S1; destruct
    11581189    | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
     1190    | #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 destruct
    11591191    ]
    11601192  ]
     
    11691201  | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct
    11701202    %1 whd in FS ⊢ %;
    1171     inversion (stack_preserved_return … EVAL) [ @refl | #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct ]
     1203    inversion (stack_preserved_return … EVAL) [ @refl | #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct | 4: #H276 #H277 #H278 #H279 #H280 #H281 #H282 destruct ]
    11721204    #s1 #f1 #f2 #fs #m #FE #SS1 #_ #E1 #E2 #_ destruct <FE
    11731205    inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct | #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct | #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ]
     
    11791211    | #lx #nx #H #E1x #E2x #_ destruct @H
    11801212    ]
     1213  | #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct
    11811214  ]
    11821215] qed.
Note: See TracChangeset for help on using the changeset viewer.