1 | |
---|
2 | include "RTLabs/semantics.ma". |
---|
3 | include "common/StructuredTraces.ma". |
---|
4 | |
---|
5 | discriminator status_class. |
---|
6 | |
---|
7 | (* NB: For RTLabs we only classify branching behaviour as jumps. Other jumps |
---|
8 | will be added later (LTL → LIN). *) |
---|
9 | |
---|
10 | definition 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 | |
---|
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). |
---|
29 | |
---|
30 | definition 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 | |
---|
61 | coinductive 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? *) |
---|
67 | coinductive 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 | |
---|
72 | let 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 ≝ |
---|
75 | let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in |
---|
76 | match 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 | |
---|
140 | let 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 ≝ |
---|
144 | let ge ≝ make_global … p in |
---|
145 | let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in |
---|
146 | match 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 | |
---|
181 | Not quite what we need - have to decide on seeing each label whether we will see |
---|
182 | another or hit a non-terminating call? |
---|
183 | |
---|
184 | Also - need the notion of well-labelled in order to break loops. |
---|
185 | |
---|
186 | |
---|
187 | |
---|
188 | outline: |
---|
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 | |
---|
196 | generating the finite parts: |
---|
197 | |
---|
198 | We start with the status after the call has been executed; well-labelling tells |
---|
199 | us that this is a labelled state. Now we want to generate a trace_label_return |
---|
200 | and 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. *) |
---|
208 | inductive 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 | |
---|
226 | discriminator nat. |
---|
227 | |
---|
228 | (* Find time until a nested call completes. *) |
---|
229 | lemma 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 | |
---|
263 | lemma 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 |
---|
268 | inversion 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 | |
---|
281 | definition is_cost_label : statement → Prop ≝ |
---|
282 | λs. match s with [ St_cost _ _ ⇒ True | _ ⇒ False ]. |
---|
283 | |
---|
284 | let rec All_All A (P:A → Prop) (Q:∀a. P a → Prop) l (H:All A P l) on l : Prop ≝ |
---|
285 | match 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 | |
---|
290 | definition 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 | |
---|
303 | definition 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 | |
---|
312 | definition well_cost_labelled_ge : genv → Prop ≝ |
---|
313 | λge. ∀v,f. find_funct ?? ge v = Some ? (Internal ? f) → well_cost_labelled_fn f. |
---|
314 | |
---|
315 | definition 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 | |
---|
323 | let 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 | ?. |
---|