source: src/RTLabs/Traces.ma @ 1574

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

A little more progress on traces on RTLabs.

File size: 15.9 KB
Line 
1
2include "RTLabs/semantics.ma".
3include "common/StructuredTraces.ma".
4
5discriminator status_class.
6
7(* NB: For RTLabs we only classify branching behaviour as jumps.  Other jumps
8       will be added later (LTL → LIN). *)
9
10definition RTLabs_classify : state → status_class ≝
11λs. match s with
12[ State f _ _ ⇒
13    match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with
14    [ St_cond _ _ _ ⇒ cl_jump
15    | St_jumptable _ _ ⇒ cl_jump
16    | _ ⇒ cl_other
17    ]
18| Callstate _ _ _ _ _ ⇒ cl_call
19| Returnstate _ _ _ _ ⇒ cl_return
20].
21
22inductive RTLabs_stmt_cost : statement → Prop ≝
23| stmt_cost : ∀c,l. RTLabs_stmt_cost (St_cost c l).
24
25inductive 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).
29
30definition RTLabs_status : genv → abstract_status ≝
31λge.
32  mk_abstract_status
33    state
34    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
35    (λs,c. RTLabs_classify s = c)
36    RTLabs_cost
37    (λs,s'. match s with
38      [ dp s p ⇒
39        match s return λs. RTLabs_classify s = cl_call → ? with
40        [ Callstate fd args dst stk m ⇒
41          λ_. match s' with
42          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
43          | _ ⇒ False
44          ]
45        | State f fs m ⇒ λH.⊥
46        | _ ⇒ λH.⊥
47        ] p
48      ]).
49[ normalize in H; destruct
50| whd in H:(??%?);
51  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
52  normalize try #a try #b try #c try #d try #e try #g try #h destruct
53] qed.
54
55(* Before attempting to construct a structured trace, let's show that we can
56   form flat traces with evidence that they were constructed from an execution.
57   
58   For now we don't consider I/O. *)
59
60
61coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
62| noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
63| noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
64| noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
65
66(* add I/O? *)
67coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
68| ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
69| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s
70| ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s.
71
72let corec make_flat_trace ge s
73  (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
74  flat_trace io_out io_in ge s ≝
75let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
76match e return λx. e = x → ? with
77[ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
78| e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?)
79| e_wrong m ⇒ λE. ft_wrong … s m ?
80| e_interact o f ⇒ λE. ⊥
81] (refl ? e).
82[ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E;
83  cases (eval_statement ge s)
84  [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
85  | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
86    >(?:is_final ????? = RTLabs_is_final s1) //
87    lapply (refl ? (RTLabs_is_final s1))
88    cases (RTLabs_is_final s1) in ⊢ (???% → %);
89    [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct
90    | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl
91    | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct
92    ]
93  | *: #m whd in ⊢ (??%? → ?); #E destruct
94  ]
95| whd in E:(??%?); >exec_inf_aux_unfold in E;
96  cases (eval_statement ge s)
97  [ #O #K whd in ⊢ (??%? → ?); #E destruct
98  | * #tr #s1 whd in ⊢ (??%? → ?);
99    cases (is_final ?????)
100    [ whd in ⊢ (??%? → ?); #E destruct @refl
101    | #i whd in ⊢ (??%? → ?); #E destruct
102    ]
103  | #m whd in ⊢ (??%? → ?); #E destruct
104  ]
105| whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
106  cases (eval_statement ge s)
107  [ #O #K whd in ⊢ (??%? → ?); #E destruct
108  | * #tr #s1 whd in ⊢ (??%? → ?);
109    cases (is_final ?????)
110    [ whd in ⊢ (??%? → ?); #E
111      change with (eval_statement ge s1) in E:(??(??????(?????%))?);
112      destruct
113      inversion H
114      [ #a #b #c #E1 destruct
115      | #trx #sx #ex #H1 #E2 #E3 destruct @H1
116      | #m #E1 destruct
117      ]
118    | #i whd in ⊢ (??%? → ?); #E destruct
119    ]
120  | #m whd in ⊢ (??%? → ?); #E destruct
121  ]
122| whd in E:(??%?); >exec_inf_aux_unfold in E;
123  cases (eval_statement ge s)
124  [ #O #K whd in ⊢ (??%? → ?); #E destruct
125  | * #tr1 #s1 whd in ⊢ (??%? → ?);
126    cases (is_final ?????)
127    [ whd in ⊢ (??%? → ?); #E destruct
128    | #i whd in ⊢ (??%? → ?); #E destruct
129    ]
130  | #m whd in ⊢ (??%? → ?); #E destruct @refl
131  ]
132| whd in E:(??%?); >E in H; #H
133  inversion H
134  [ #a #b #c #E destruct
135  | #a #b #c #d #E1 destruct
136  | #m #E1 destruct
137  ]
138] qed.
139
140let corec make_whole_flat_trace p s
141  (H:exec_no_io … (exec_inf … RTLabs_fullexec p))
142  (I:make_initial_state ??? p = OK ? s) :
143  flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
144let ge ≝ make_global … p in
145let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
146match e return λx. e = x → ? with
147[ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
148| e_step _ _ e' ⇒ λE. make_flat_trace ge s ?
149| e_wrong m ⇒ λE. ⊥
150| e_interact o f ⇒ λE. ⊥
151] (refl ? e).
152[ whd in E:(??%?); >exec_inf_aux_unfold in E;
153  whd in ⊢ (??%? → ?);
154  >(?:is_final ????? = RTLabs_is_final s) //
155  lapply (refl ? (RTLabs_is_final s))
156  cases (RTLabs_is_final s) in ⊢ (???% → %);
157  [ #_ whd in ⊢ (??%? → ?); #E destruct
158  | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct
159  ]
160| whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
161  >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
162  [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
163    [ #a #b #c #E1 destruct
164    | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
165      @H1
166    | #m #E1 destruct
167    ]
168  | #i whd in ⊢ (??%? → ???% → ?); #E destruct
169  ]
170| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
171  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
172| whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
173  cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
174] qed.
175
176(* Need a way to choose whether a called function terminates.  Then,
177     if the initial function terminates we generate a purely inductive structured trace,
178     otherwise we start generating the coinductive one, and on every function call
179       use the choice method again to decide whether to step over or keep going.
180
181Not quite what we need - have to decide on seeing each label whether we will see
182another or hit a non-terminating call?
183
184Also - need the notion of well-labelled in order to break loops.
185
186
187
188outline:
189
190 does function terminate?
191 - yes, get (bound on the number of steps until return), generate finite
192        structure using bound as termination witness
193 - no,  get (¬ bound on steps to return), start building infinite trace out of
194        finite steps.  At calls, check for termination, generate appr. form.
195
196generating the finite parts:
197
198We start with the status after the call has been executed; well-labelling tells
199us that this is a labelled state.  Now we want to generate a trace_label_return
200and also return the remainder of the flat trace.
201
202*)
203
204(* [nth_is_return ge n depth s trace] says that after [n] steps of [trace] from
205   [s] we reach the return state for the current function.  [depth] performs
206   the call/return counting necessary for handling deeper function calls.
207   It should be zero at the top level. *)
208inductive nth_is_return (ge:genv) : nat → nat → ∀s. flat_trace io_out io_in ge s → Prop ≝
209| nir_step : ∀n,s,tr,s',depth,EX,trace.
210    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
211    nth_is_return ge n depth s' trace →
212    nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
213| nir_call : ∀n,s,tr,s',depth,EX,trace.
214    RTLabs_classify s = cl_call →
215    nth_is_return ge n (S depth) s' trace →
216    nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
217| nir_ret : ∀n,s,tr,s',depth,EX,trace.
218    RTLabs_classify s = cl_return →
219    nth_is_return ge n depth s' trace →
220    nth_is_return ge (S n) (S depth) s (ft_step ?? ge s tr s' EX trace)
221| nir_base : ∀s,trace.
222    RTLabs_classify s = cl_return →
223    nth_is_return ge O O s trace
224.
225
226discriminator nat.
227
228(* Find time until a nested call completes. *)
229lemma nth_is_return_down : ∀ge,n,depth,s,trace.
230  nth_is_return ge n (S depth) s trace →
231  ∃m. nth_is_return ge m depth s trace.
232#ge #n elim n
233(* It's impossible to run out of time... *)
234[ #depth #s #trace #H inversion H
235  [ #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
236  | #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct
237  | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
238  | #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
239  ]
240| #n' #IH #depth #s #trace #H inversion H
241  [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
242    cases (IH depth s1' trace1 ?)
243    [ #m' #H' %{(S m')} %1 //
244    | //
245    ]
246  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
247    cases (IH (S depth) s1' trace1 ?)
248    [ #m' #H' %{(S m')} %2 //
249    | //
250    ]
251  | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
252    cases (depth1) in H2 ⊢ %;
253    [ #H2 %{O} %4 //
254    | #depth' #H2 cases (IH depth' s1' trace1 ?)
255      [ #m' #H' %{(S m')} %3 //
256      | //
257      ]
258    ]
259  | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct
260  ]
261] qed.
262
263lemma nth_is_return_call : ∀ge,n,s,tr,s',EX,trace.
264  RTLabs_classify s = cl_call →
265  nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) →
266  ∃m. nth_is_return ge m O s' trace.
267#ge #n #s #tr #s' #EX #trace #CLASS #H
268inversion H
269[ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 * #H1 #H2 #_ #E1 #E2 #E3 @⊥
270  -H2 destruct >H1 in CLASS; #E destruct
271| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct
272  @nth_is_return_down //
273| #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥
274  -H2 destruct
275| #s1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct
276] qed.
277
278(* We require that labels appear after branch instructions and at the start of
279   functions.  The first is required for preciseness, the latter for soundness.
280   We will make a separate requirement for there to be a finite number of steps
281   between labels to catch loops for soundness (is this sufficient?). *)
282
283definition is_cost_label : statement → Prop ≝
284λs. match s with [ St_cost _ _ ⇒ True | _ ⇒ False ].
285
286let rec All_All A (P:A → Prop) (Q:∀a. P a → Prop) l (H:All A P l) on l : Prop ≝
287match l return λl.All A P l → Prop with
288[ nil ⇒ λ_. True
289| cons h t ⇒ λH. Q h (proj1 … H) ∧ All_All A P Q t (proj2 … H)
290] H.
291
292definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
293λf,s. match s return λs. labels_present ? s → Prop with
294[ St_cond _ l1 l2 ⇒ λH.
295    is_cost_label (lookup_present … (f_graph f) l1 ?) ∧
296    is_cost_label (lookup_present … (f_graph f) l2 ?)
297| St_jumptable _ ls ⇒ λH.
298    All_All … (λl,H. is_cost_label (lookup_present … (f_graph f) l H)) ls H
299| _ ⇒ λ_. True
300]. whd in H;
301[ @(proj1 … H)
302| @(proj2 … H)
303] qed.
304
305definition well_cost_labelled_fn : internal_function → Prop ≝
306λf. (∀l,s. ∀H:lookup … (f_graph f) l = Some ? s.
307          well_cost_labelled_statement f s (f_closed f …)) ∧
308    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?).
309[ 2: @H | skip | cases (f_entry f) // ] qed.
310
311(* We need to ensure that any code we come across is well-cost-labelled.  We may
312   get function code from either the global environment or the state. *)
313
314definition well_cost_labelled_ge : genv → Prop ≝
315λge. ∀v,f. find_funct ?? ge v = Some ? (Internal ? f) → well_cost_labelled_fn f.
316
317definition well_cost_labelled_state : state → Prop ≝
318λs. match s with
319[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
320| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
321                          All ? (λf. well_cost_labelled_fn (func f)) fs
322| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
323].
324
325(* Don't need to know that labels break loops because we have termination. *)
326
327record make_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {
328  new_state : state;
329  termination_count : nat;
330  remainder : flat_trace io_out io_in ge new_state;
331  terminates : nth_is_return ge termination_count O new_state remainder;
332  cost_labelled : well_cost_labelled_state new_state;
333  new_trace : T new_state
334}.
335
336definition replace_new_trace : ∀ge,T1,T2.
337  ∀r:make_result ge T1. T2 (new_state … r) → make_result ge T2 ≝
338λge,T1,T2,r,trace.
339  mk_make_result ge T2
340    (new_state … r)
341    (termination_count … r)
342    (remainder … r)
343    (terminates … r)
344    (cost_labelled … r)
345    trace.
346
347let rec make_label_return n ge s
348  (trace: flat_trace io_out io_in ge s)
349  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
350  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
351  (STATEMENT_COSTLABEL: RTLabs_cost s)              (* current statement is a cost label *)
352  (TERMINATES: nth_is_return ge n O s trace)
353  : make_result ge (trace_label_return (RTLabs_status ge) s) ≝
354
355  let r ≝ make_label_label n ge s trace ???? in
356  match new_trace … r with
357  [ dp ends tll ⇒
358    match ends return λx. trace_label_label ? x ?? → ? with
359    [ ends_with_ret ⇒ λtll.
360        replace_new_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll)
361    | doesnt_end_with_ret ⇒ λtll.
362        let r' ≝ make_label_return (termination_count … r) ge (new_state … r)
363                   (remainder … r) ??? (terminates … r) in
364          replace_new_trace … r'
365            (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r'))
366    ] tll
367  ]
368
369and make_label_label n ge s
370  (trace: flat_trace io_out io_in ge s)
371  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
372  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
373  (STATEMENT_COSTLABEL: RTLabs_cost s)              (* current statement is a cost label *)
374  (TERMINATES: nth_is_return ge n O s trace)
375  : make_result ge (λs'. Σends. trace_label_label (RTLabs_status ge) ends s s') ≝
376let r ≝ make_any_label n ge s trace ??? in
377match new_trace … r with
378[ dp ends tr ⇒
379  replace_new_trace ??? r
380    (dp ?? ends (tll_base (RTLabs_status ge) ends s (new_state … r) tr STATEMENT_COSTLABEL))
381]
382
383and make_any_label n ge s
384  (trace: flat_trace io_out io_in ge s)
385  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
386  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
387  (TERMINATES: nth_is_return ge n O s trace)
388  : make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') ≝
389match 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.
394
395[ //
396| //
397| @(trace_label_label_label … tll)
398| //
399| //
400| //
401| //
402| //
403| //
404| //
405|
406|
407| inversion TERMINATES
408  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 -TERMINATES destruct
409  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 -TERMINATES destruct
410  | #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
412 
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. *)
Note: See TracBrowser for help on using the repository browser.