Changeset 1583


Ignore:
Timestamp:
Dec 2, 2011, 1:02:08 PM (8 years ago)
Author:
campbell
Message:

More on RTLabs structured traces.
Fixed mistake in structure trace definition that made it unhabitable.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1574 r1583  
    2020].
    2121
    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).
     22definition 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].
    2931
    3032definition RTLabs_status : genv → abstract_status ≝
     
    3436    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
    3537    (λs,c. RTLabs_classify s = c)
    36     RTLabs_cost
     38    (λs. RTLabs_cost s = true)
    3739    (λs,s'. match s with
    3840      [ dp s p ⇒
     
    219221    nth_is_return ge n depth s' trace →
    220222    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.
    222227    RTLabs_classify s = cl_return →
    223     nth_is_return ge O O s trace
     228    nth_is_return ge O O s (ft_step ?? ge s tr s' EX trace)
    224229.
    225230
     
    273278| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥
    274279  -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
     283lemma 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
    276296] qed.
    277297
     
    313333
    314334definition 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.
    316336
    317337definition well_cost_labelled_state : state → Prop ≝
     
    322342| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
    323343].
     344
     345lemma 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.
    324358
    325359(* Don't need to know that labels break loops because we have termination. *)
     
    349383  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    350384  (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 *)
    352386  (TERMINATES: nth_is_return ge n O s trace)
    353387  : make_result ge (trace_label_return (RTLabs_status ge) s) ≝
     
    371405  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    372406  (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 *)
    374408  (TERMINATES: nth_is_return ge n O s trace)
    375409  : make_result ge (λs'. Σends. trace_label_label (RTLabs_status ge) ends s s') ≝
     
    387421  (TERMINATES: nth_is_return ge n O s trace)
    388422  : 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.
     423match 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.
    394445
    395446[ //
     
    405456|
    406457|
     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
    407470| inversion TERMINATES
    408471  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 -TERMINATES destruct
    409472  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 -TERMINATES destruct
    410473  | #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
    412479 
    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  
    229229  mk_fullexec … RTLabs_exec make_global make_initial_state.
    230230
     231
     232(* Some lemmas about the semantics. *)
     233
     234(* Note parts of frames and states that are preserved. *)
     235
     236inductive 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
     243inductive 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
     252lemma 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
     261lemma 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
  • src/common/Globalenvs.ma

    r1545 r1583  
    549549  ?*)
    550550.
     551
     552lemma find_funct_find_funct_ptr : ∀F,ge,v,f.
     553  find_funct Genv F ge v = Some F f →
     554  ∃pty,b,c. v = Vptr (mk_pointer pty b c zero_offset)  ∧ find_funct_ptr Genv F ge b = Some F f.
     555#F #ge *
     556[ #f #E normalize in E; destruct
     557| #sz #i #f #E normalize in E; destruct
     558| #f #fn #E normalize in E; destruct
     559| #r #f #E normalize in E; destruct
     560| * #pty #b #c * #off #f #E normalize in E;
     561  cases off in E ⊢ %; [ 2,3: #x ]
     562  #E normalize in E; destruct
     563  %{pty} %{b} %{c} % // @E
     564] qed.
     565
    551566(*
    552567##[ #A B C transf p b f; elim p; #fns main vars;
  • src/common/StructuredTraces.ma

    r1574 r1583  
    7676        trace_any_label S end_flag status_init status_end →
    7777        as_classifier S status_pre cl_other →
    78         ¬ (as_costed S status_pre) →
     78        ¬ (as_costed S status_init) →
    7979          trace_any_label S end_flag status_pre status_end.
    8080
Note: See TracChangeset for help on using the changeset viewer.