source: src/RTLabs/Traces.ma @ 1565

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

Note that RTLabs ought to classify branches as "jumps" (in the
structural traces sense), and define a notion of well-cost-labelling.

File size: 12.5 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. *)
280
281definition is_cost_label : statement → Prop ≝
282λs. match s with [ St_cost _ _ ⇒ True | _ ⇒ False ].
283
284let rec All_All A (P:A → Prop) (Q:∀a. P a → Prop) l (H:All A P l) on l : Prop ≝
285match l return λl.All A P l → Prop with
286[ nil ⇒ λ_. True
287| cons h t ⇒ λH. Q h (proj1 … H) ∧ All_All A P Q t (proj2 … H)
288] H.
289
290definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝
291λf,s. match s return λs. labels_present ? s → Prop with
292[ St_cond _ l1 l2 ⇒ λH.
293    is_cost_label (lookup_present … (f_graph f) l1 ?) ∧
294    is_cost_label (lookup_present … (f_graph f) l2 ?)
295| St_jumptable _ ls ⇒ λH.
296    All_All … (λl,H. is_cost_label (lookup_present … (f_graph f) l H)) ls H
297| _ ⇒ λ_. True
298]. whd in H;
299[ @(proj1 … H)
300| @(proj2 … H)
301] qed.
302
303definition well_cost_labelled_fn : internal_function → Prop ≝
304λf. (∀l,s. ∀H:lookup … (f_graph f) l = Some ? s.
305          well_cost_labelled_statement f s (f_closed f …)) ∧
306    is_cost_label (lookup_present … (f_graph f) (f_entry f) ?).
307[ 2: @H | skip | cases (f_entry f) // ] qed.
308
309(* We need to ensure that any code we come across is well-cost-labelled.  We may
310   get function code from either the global environment or the state. *)
311
312definition well_cost_labelled_ge : genv → Prop ≝
313λge. ∀v,f. find_funct ?? ge v = Some ? (Internal ? f) → well_cost_labelled_fn f.
314
315definition well_cost_labelled_state : state → Prop ≝
316λs. match s with
317[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
318| Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
319                          All ? (λf. well_cost_labelled_fn (func f)) fs
320| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
321].
322
323let rec make_label_return n ge s
324  (trace: flat_trace io_out io_in ge s)
325  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
326  (STATE_COSTLABELLED: well_cost_labelled_state s)
327  (TERMINATES: nth_is_return ge n O s trace)
328  : Σs'.Σremainder:flat_trace io_out io_in ge s'.
329      trace_label_return (RTLabs_status ge) s s' ≝
330?.
Note: See TracBrowser for help on using the repository browser.