Changeset 1583 for src/RTLabs
- Timestamp:
- Dec 2, 2011, 1:02:08 PM (9 years ago)
- Location:
- src/RTLabs
- Files:
-
- 2 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. *) -
src/RTLabs/semantics.ma
r1559 r1583 229 229 mk_fullexec … RTLabs_exec make_global make_initial_state. 230 230 231 232 (* Some lemmas about the semantics. *) 233 234 (* Note parts of frames and states that are preserved. *) 235 236 inductive frame_rel : frame → frame → Prop ≝ 237 | mk_frame_rel : 238 ∀func,locals,next,next_ok,sp,retdst,locals',next',next_ok'. frame_rel 239 (mk_frame func locals next next_ok sp retdst) 240 (mk_frame func locals' next' next_ok' sp retdst) 241 . 242 243 inductive state_rel : genv → state → state → Prop ≝ 244 | normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m') 245 | to_call : ∀ge,f,fs,m,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst (f'::fs) m) 246 | tail_call : ∀ge,f,fs,m,fd,args,dst,m'. ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst fs m') 247 | from_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m'. state_rel ge (Callstate (Internal ? fn) args dst fs m) (State (mk_frame fn locals next nok sp dst) fs m') 248 | to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m') 249 | from_ret : ∀ge,f,fs,rtv,dst,f',m. frame_rel f f' → state_rel ge (Returnstate rtv dst (f::fs) m) (State f' fs m) 250 . 251 252 lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop. 253 (∀a. e = Value ??? a → f a = Value ??? v → P v) → 254 (bindIO O I A B e f = Value ??? v → P v). 255 #O #I #A #B * 256 [ #o #k #f #v #P #H #E whd in E:(??%?); destruct 257 | #a #f #v #P #H #E @H [ @a | @refl | @E ] 258 | #m #f #v #P #H #E whd in E:(??%?); destruct 259 ] qed. 260 261 lemma eval_perserves : ∀ge,s,tr,s'. 262 eval_statement ge s = Value ??? 〈tr,s'〉 → 263 state_rel ge s s'. 264 #ge * 265 [ * #func #locals #next #next_ok #sp #retdst #fs #m 266 #tr #s' 267 whd in ⊢ (??%? → ?); 268 generalize in ⊢ (??(?%)? → ?); 269 cases (lookup_present LabelTag statement (f_graph func) next next_ok) 270 [ #l #LP whd in ⊢ (??%? → ?); #E destruct % % 271 | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % % 272 | #r #c #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #locals' #Eloc #E whd in E:(??%?); destruct % % 273 | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #v' #Ev' @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % % 274 | #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v1 #Ev1 @bindIO_value #v2 #Ev2 @bindIO_value #v' #Ev' @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % % 275 | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #v' #Ev' @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % % 276 | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #v' #Ev' @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % % 277 | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bindIO_value #b #Eb @bindIO_value #fd #Efd @bindIO_value #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ] 278 | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #fd #Efd @bindIO_value #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] 279 | #id #rs #LP whd in ⊢ (??%? → ?); @bindIO_value #b #Eb @bindIO_value #fd #Efd @bindIO_value #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] 280 | #r #rs #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #fd #Efd @bindIO_value #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] 281 | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #b #Eb #E whd in E:(??%?); destruct % % 282 | #r #ls #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ] 283 | #LP whd in ⊢ (??%? → ?); @bindIO_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bindIO_value #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5 284 ] 285 | * #fn #args #retdst #stk #m #tr #s' 286 whd in ⊢ (??%? → ?); 287 [ @bindIO_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?); 288 #E destruct %4 289 | @bindIO_value #evargs #Eargs @bindIO_value #evres #Eres whd in Eres:(??%?); 290 destruct 291 ] 292 | #v #r * [2: #f #fs ] #m #tr #s' 293 whd in ⊢ (??%? → ?); 294 [ @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct 295 %6 cases f #func #locals #next #next_ok #sp #retdst % 296 | #E destruct 297 ] 298 ] qed. 299
Note: See TracChangeset
for help on using the changeset viewer.