source: src/RTLabs/Traces.ma @ 1563

Last change on this file since 1563 was 1563, checked in by campbell, 9 years ago

A little progress on constructing RTLabs structured traces.

File size: 10.4 KB
Line 
1
2include "RTLabs/semantics.ma".
3include "common/StructuredTraces.ma".
4
5discriminator status_class.
6
7(* NB: we do not consider jumps in the traces of RTLabs programs. *)
8
9definition RTLabs_classify : state → status_class ≝
10λs. match s with
11[ State _ _ _ ⇒ cl_other
12| Callstate _ _ _ _ _ ⇒ cl_call
13| Returnstate _ _ _ _ ⇒ cl_return
14].
15
16inductive RTLabs_stmt_cost : statement → Prop ≝
17| stmt_cost : ∀c,l. RTLabs_stmt_cost (St_cost c l).
18
19inductive RTLabs_cost : state → Prop ≝
20| cost_instr : ∀f,fs,m.
21    RTLabs_stmt_cost (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) →
22    RTLabs_cost (State f fs m).
23
24definition RTLabs_status : genv → abstract_status ≝
25λge.
26  mk_abstract_status
27    state
28    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
29    (λs,c. RTLabs_classify s = c)
30    RTLabs_cost
31    (λs,s'. match s with
32      [ dp s p ⇒
33        match s return λs. RTLabs_classify s = cl_call → ? with
34        [ Callstate fd args dst stk m ⇒
35          λ_. match s' with
36          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
37          | _ ⇒ False
38          ]
39        | State f fs m ⇒ λH.⊥
40        | _ ⇒ λH.⊥
41        ] p
42      ]).
43[ normalize in H; destruct
44| normalize in H; destruct
45] qed.
46
47(* Before attempting to construct a structured trace, let's show that we can
48   form flat traces with evidence that they were constructed from an execution.
49   
50   For now we don't consider I/O. *)
51
52
53coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
54| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
55| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
56| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
57
58(* add I/O? *)
59coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
60| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
61| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
62| ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
63
64let corec make_flat_trace ge s
65  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
66  flat_trace io_out io_in ge s ≝
67let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
68match e return λx. e = x → ? with
69[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
70| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?)
71| e_wrong m ⇒ λE. ft_wrong … s m ?
72| e_interact o f ⇒ λE. ⊥
73] (refl ? e).
74[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
75  cases (eval_statement ge s)
76  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
77  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
78    >(?:is_final ????? = RTLabs_is_final s1) //
79    lapply (refl ? (RTLabs_is_final s1))
80    cases (RTLabs_is_final s1) in ⊢ (???% → %);
81    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
82    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
83    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
84    ]
85  | *: #m whd in ⊢ (??%? → ?); #E destruct
86  ]
87| whd in E:(??%?); >exec_inf_aux_unfold in E;
88  cases (eval_statement ge s)
89  [ #O #K whd in ⊢ (??%? → ?); #E destruct
90  | * #tr #s1 whd in ⊢ (??%? → ?);
91    cases (is_final ?????)
92    [ whd in ⊢ (??%? → ?); #E destruct @refl
93    | #i whd in ⊢ (??%? → ?); #E destruct
94    ]
95  | #m whd in ⊢ (??%? → ?); #E destruct
96  ]
97| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
98  cases (eval_statement ge s)
99  [ #O #K whd in ⊢ (??%? → ?); #E destruct
100  | * #tr #s1 whd in ⊢ (??%? → ?);
101    cases (is_final ?????)
102    [ whd in ⊢ (??%? → ?); #E
103      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
104      destruct
105      inversion H
106      [ #a #b #c #E1 destruct
107      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
108      | #m #E1 destruct
109      ]
110    | #i whd in ⊢ (??%? → ?); #E destruct
111    ]
112  | #m whd in ⊢ (??%? → ?); #E destruct
113  ]
114| whd in E:(??%?); >exec_inf_aux_unfold in E;
115  cases (eval_statement ge s)
116  [ #O #K whd in ⊢ (??%? → ?); #E destruct
117  | * #tr1 #s1 whd in ⊢ (??%? → ?);
118    cases (is_final ?????)
119    [ whd in ⊢ (??%? → ?); #E destruct
120    | #i whd in ⊢ (??%? → ?); #E destruct
121    ]
122  | #m whd in ⊢ (??%? → ?); #E destruct @refl
123  ]
124| whd in E:(??%?); >E in H; #H
125  inversion H
126  [ #a #b #c #E destruct
127  | #a #b #c #d #E1 destruct
128  | #m #E1 destruct
129  ]
130] qed.
131
132let corec make_whole_flat_trace p s
133  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
134  (I:make_initial_state ??? p = OK ? s) :
135  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
136let ge ≝ make_global … p in
137let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
138match e return λx. e = x → ? with
139[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
140| e_step _ _ e' ⇒ λE. make_flat_trace ge s ?
141| e_wrong m ⇒ λE. ⊥
142| e_interact o f ⇒ λE. ⊥
143] (refl ? e).
144[ whd in E:(??%?); >exec_inf_aux_unfold in E;
145  whd in ⊢ (??%? → ?);
146  >(?:is_final ????? = RTLabs_is_final s) //
147  lapply (refl ? (RTLabs_is_final s))
148  cases (RTLabs_is_final s) in ⊢ (???% → %);
149  [ #_ whd in ⊢ (??%? → ?); #E destruct
150  | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct
151  ]
152| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
153  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
154  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
155    [ #a #b #c #E1 destruct
156    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
157      @H1
158    | #m #E1 destruct
159    ]
160  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
161  ]
162| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
163  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
164| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
165  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
166] qed.
167
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 TracBrowser for help on using the repository browser.