Changeset 1563 for src/RTLabs


Ignore:
Timestamp:
Nov 25, 2011, 1:49:27 PM (8 years ago)
Author:
campbell
Message:

A little progress on constructing RTLabs structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1559 r1563  
    77(* NB: we do not consider jumps in the traces of RTLabs programs. *)
    88
    9 inductive RTLabs_classify : state → status_class → Prop ≝
    10 | rtla_other : ∀f,fs,m.    RTLabs_classify (State f fs m)        cl_other
    11 | rtla_call  : ∀a,b,c,d,e. RTLabs_classify (Callstate a b c d e) cl_call
    12 | rtla_ret   : ∀a,b,c,d.   RTLabs_classify (Returnstate a b c d) cl_return
    13 .
     9definition RTLabs_classify : state → status_class ≝
     10λs. match s with
     11[ State _ _ _ ⇒ cl_other
     12| Callstate _ _ _ _ _ ⇒ cl_call
     13| Returnstate _ _ _ _ ⇒ cl_return
     14].
    1415
    1516inductive RTLabs_stmt_cost : statement → Prop ≝
     
    2627    state
    2728    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
    28     RTLabs_classify
     29    (λs,c. RTLabs_classify s = c)
    2930    RTLabs_cost
    3031    (λs,s'. match s with
    3132      [ dp s p ⇒
    32         match s return λs. RTLabs_classify s cl_call → ? with
     33        match s return λs. RTLabs_classify s = cl_call → ? with
    3334        [ Callstate fd args dst stk m ⇒
    3435          λ_. match s' with
     
    4041        ] p
    4142      ]).
    42 inversion H try #a try #b try #c try #d try #e try #f destruct
    43 qed.
     43[ normalize in H; destruct
     44| normalize in H; destruct
     45] qed.
    4446
    4547(* Before attempting to construct a structured trace, let's show that we can
     
    164166] qed.
    165167
     168(* Need a way to choose whether a called function terminates.  Then,
     169     if the initial function terminates we generate a purely inductive structured trace,
     170     otherwise we start generating the coinductive one, and on every function call
     171       use the choice method again to decide whether to step over or keep going.
     172
     173Not quite what we need - have to decide on seeing each label whether we will see
     174another or hit a non-terminating call?
     175
     176Also - need the notion of well-labelled in order to break loops.
     177
     178
     179
     180outline:
     181
     182 does function terminate?
     183 - yes, get (bound on the number of steps until return), generate finite
     184        structure using bound as termination witness
     185 - no,  get (¬ bound on steps to return), start building infinite trace out of
     186        finite steps.  At calls, check for termination, generate appr. form.
     187
     188generating the finite parts:
     189
     190We start with the status after the call has been executed; well-labelling tells
     191us that this is a labelled state.  Now we want to generate a trace_label_return
     192and also return the remainder of the flat trace.
     193
     194*)
     195
     196(* [nth_is_return ge n depth s trace] says that after [n] steps of [trace] from
     197   [s] we reach the return state for the current function.  [depth] performs
     198   the call/return counting necessary for handling deeper function calls.
     199   It should be zero at the top level. *)
     200inductive nth_is_return (ge:genv) : nat → nat → ∀s. flat_trace io_out io_in ge s → Prop ≝
     201| nir_step : ∀n,s,tr,s',depth,EX,trace.
     202    RTLabs_classify s = cl_other →
     203    nth_is_return ge n depth s' trace →
     204    nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
     205| nir_call : ∀n,s,tr,s',depth,EX,trace.
     206    RTLabs_classify s = cl_call →
     207    nth_is_return ge n (S depth) s' trace →
     208    nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
     209| nir_ret : ∀n,s,tr,s',depth,EX,trace.
     210    RTLabs_classify s = cl_return →
     211    nth_is_return ge n depth s' trace →
     212    nth_is_return ge (S n) (S depth) s (ft_step ?? ge s tr s' EX trace)
     213| nir_base : ∀s,trace.
     214    RTLabs_classify s = cl_return →
     215    nth_is_return ge O O s trace
     216.
     217
     218discriminator nat.
     219
     220(* Find time until a nested call completes. *)
     221lemma nth_is_return_down : ∀ge,n,depth,s,trace.
     222  nth_is_return ge n (S depth) s trace →
     223  ∃m. nth_is_return ge m depth s trace.
     224#ge #n elim n
     225(* It's impossible to run out of time... *)
     226[ #depth #s #trace #H inversion H
     227  [ #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
     228  | #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
     229  | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
     230  | #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
     231  ]
     232| #n' #IH #depth #s #trace #H inversion H
     233  [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
     234    cases (IH depth s1' trace1 ?)
     235    [ #m' #H' %{(S m')} %1 //
     236    | //
     237    ]
     238  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
     239    cases (IH (S depth) s1' trace1 ?)
     240    [ #m' #H' %{(S m')} %2 //
     241    | //
     242    ]
     243  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
     244    cases (depth1) in H2 ⊢ %;
     245    [ #H2 %{O} %4 //
     246    | #depth' #H2 cases (IH depth' s1' trace1 ?)
     247      [ #m' #H' %{(S m')} %3 //
     248      | //
     249      ]
     250    ]
     251  | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct
     252  ]
     253] qed.
     254
     255lemma nth_is_return_call : ∀ge,n,s,tr,s',EX,trace.
     256  RTLabs_classify s = cl_call →
     257  nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
     258  ∃m. nth_is_return ge m O s' trace.
     259#ge #n #s #tr #s' #EX #trace #CLASS #H
     260inversion H
     261[ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥
     262  -H2 destruct >H1 in CLASS; #E destruct
     263| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
     264  @nth_is_return_down //
     265| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥
     266  -H2 destruct
     267| #s1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct
     268] qed.
     269
     270(* Is the only well-labelledness fact I need here that the current state is
     271   labelled?  That doesn't seem like it should be enough?
     272   
     273   Is this because the insertion of labels after jumps in LTL → LIN takes care
     274   of the cost proof's needs?  Is the important thing that every branch is
     275   followed by a label?  The LTL → LIN stage then only adds labels at merges.
     276    *)
     277let rec make_label_return n ge s
     278  (trace:flat_trace io_out io_in ge s)
     279  (TERMINATES:nth_is_return ge n O s trace)
     280  : Σs'.Σremainder:flat_trace io_out io_in ge s'.
     281      trace_label_return (RTLabs_status ge) s s' ≝
     282?.
Note: See TracChangeset for help on using the changeset viewer.