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 | definition is_cost_label : statement → bool ≝ |
---|
23 | λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ]. |
---|
24 | |
---|
25 | definition RTLabs_cost : state → bool ≝ |
---|
26 | λs. match s with |
---|
27 | [ State f fs m ⇒ |
---|
28 | is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) |
---|
29 | | _ ⇒ false |
---|
30 | ]. |
---|
31 | |
---|
32 | definition RTLabs_status : genv → abstract_status ≝ |
---|
33 | λge. |
---|
34 | mk_abstract_status |
---|
35 | state |
---|
36 | (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉) |
---|
37 | (λs,c. RTLabs_classify s = c) |
---|
38 | (λs. RTLabs_cost s = true) |
---|
39 | (λs,s'. match s with |
---|
40 | [ dp s p ⇒ |
---|
41 | match s return λs. RTLabs_classify s = cl_call → ? with |
---|
42 | [ Callstate fd args dst stk m ⇒ |
---|
43 | λ_. match s' with |
---|
44 | [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ] |
---|
45 | | _ ⇒ False |
---|
46 | ] |
---|
47 | | State f fs m ⇒ λH.⊥ |
---|
48 | | _ ⇒ λH.⊥ |
---|
49 | ] p |
---|
50 | ]). |
---|
51 | [ normalize in H; destruct |
---|
52 | | whd in H:(??%?); |
---|
53 | cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H; |
---|
54 | normalize try #a try #b try #c try #d try #e try #g try #h destruct |
---|
55 | ] qed. |
---|
56 | |
---|
57 | (* Before attempting to construct a structured trace, let's show that we can |
---|
58 | form flat traces with evidence that they were constructed from an execution. |
---|
59 | |
---|
60 | For now we don't consider I/O. *) |
---|
61 | |
---|
62 | |
---|
63 | coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝ |
---|
64 | | noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c) |
---|
65 | | noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e) |
---|
66 | | noio_wrong : ∀m. exec_no_io o i (e_wrong … m). |
---|
67 | |
---|
68 | (* add I/O? *) |
---|
69 | coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝ |
---|
70 | | ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s |
---|
71 | | ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s |
---|
72 | | ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s. |
---|
73 | |
---|
74 | let corec make_flat_trace ge s |
---|
75 | (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) : |
---|
76 | flat_trace io_out io_in ge s ≝ |
---|
77 | let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in |
---|
78 | match e return λx. e = x → ? with |
---|
79 | [ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?) |
---|
80 | | e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ?) |
---|
81 | | e_wrong m ⇒ λE. ft_wrong … s m ? |
---|
82 | | e_interact o f ⇒ λE. ⊥ |
---|
83 | ] (refl ? e). |
---|
84 | [ 1,2: whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
85 | cases (eval_statement ge s) |
---|
86 | [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
87 | | 2,5: * #tr #s1 whd in ⊢ (??%? → ?); |
---|
88 | >(?:is_final ????? = RTLabs_is_final s1) // |
---|
89 | lapply (refl ? (RTLabs_is_final s1)) |
---|
90 | cases (RTLabs_is_final s1) in ⊢ (???% → %); |
---|
91 | [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct |
---|
92 | | #i #_ whd in ⊢ (??%? → ?); #E destruct /2/ @refl |
---|
93 | | #i #E whd in ⊢ (??%? → ?); #E2 destruct >E % #E' destruct |
---|
94 | ] |
---|
95 | | *: #m whd in ⊢ (??%? → ?); #E destruct |
---|
96 | ] |
---|
97 | | whd in E:(??%?); >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 destruct @refl |
---|
103 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
104 | ] |
---|
105 | | #m whd in ⊢ (??%? → ?); #E destruct |
---|
106 | ] |
---|
107 | | whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E; |
---|
108 | cases (eval_statement ge s) |
---|
109 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
110 | | * #tr #s1 whd in ⊢ (??%? → ?); |
---|
111 | cases (is_final ?????) |
---|
112 | [ whd in ⊢ (??%? → ?); #E |
---|
113 | change with (eval_statement ge s1) in E:(??(??????(?????%))?); |
---|
114 | destruct |
---|
115 | inversion H |
---|
116 | [ #a #b #c #E1 destruct |
---|
117 | | #trx #sx #ex #H1 #E2 #E3 destruct @H1 |
---|
118 | | #m #E1 destruct |
---|
119 | ] |
---|
120 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
121 | ] |
---|
122 | | #m whd in ⊢ (??%? → ?); #E destruct |
---|
123 | ] |
---|
124 | | whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
125 | cases (eval_statement ge s) |
---|
126 | [ #O #K whd in ⊢ (??%? → ?); #E destruct |
---|
127 | | * #tr1 #s1 whd in ⊢ (??%? → ?); |
---|
128 | cases (is_final ?????) |
---|
129 | [ whd in ⊢ (??%? → ?); #E destruct |
---|
130 | | #i whd in ⊢ (??%? → ?); #E destruct |
---|
131 | ] |
---|
132 | | #m whd in ⊢ (??%? → ?); #E destruct @refl |
---|
133 | ] |
---|
134 | | whd in E:(??%?); >E in H; #H |
---|
135 | inversion H |
---|
136 | [ #a #b #c #E destruct |
---|
137 | | #a #b #c #d #E1 destruct |
---|
138 | | #m #E1 destruct |
---|
139 | ] |
---|
140 | ] qed. |
---|
141 | |
---|
142 | let corec make_whole_flat_trace p s |
---|
143 | (H:exec_no_io … (exec_inf … RTLabs_fullexec p)) |
---|
144 | (I:make_initial_state ??? p = OK ? s) : |
---|
145 | flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝ |
---|
146 | let ge ≝ make_global … p in |
---|
147 | let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in |
---|
148 | match e return λx. e = x → ? with |
---|
149 | [ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ? |
---|
150 | | e_step _ _ e' ⇒ λE. make_flat_trace ge s ? |
---|
151 | | e_wrong m ⇒ λE. ⊥ |
---|
152 | | e_interact o f ⇒ λE. ⊥ |
---|
153 | ] (refl ? e). |
---|
154 | [ whd in E:(??%?); >exec_inf_aux_unfold in E; |
---|
155 | whd in ⊢ (??%? → ?); |
---|
156 | >(?:is_final ????? = RTLabs_is_final s) // |
---|
157 | lapply (refl ? (RTLabs_is_final s)) |
---|
158 | cases (RTLabs_is_final s) in ⊢ (???% → %); |
---|
159 | [ #_ whd in ⊢ (??%? → ?); #E destruct |
---|
160 | | #i #E whd in ⊢ (??%? → ?); #E2 % #E3 destruct |
---|
161 | ] |
---|
162 | | whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?); |
---|
163 | >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????) |
---|
164 | [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H |
---|
165 | [ #a #b #c #E1 destruct |
---|
166 | | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1) |
---|
167 | @H1 |
---|
168 | | #m #E1 destruct |
---|
169 | ] |
---|
170 | | #i whd in ⊢ (??%? → ???% → ?); #E destruct |
---|
171 | ] |
---|
172 | | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); |
---|
173 | cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct |
---|
174 | | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?); |
---|
175 | cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct |
---|
176 | ] qed. |
---|
177 | |
---|
178 | (* Need a way to choose whether a called function terminates. Then, |
---|
179 | if the initial function terminates we generate a purely inductive structured trace, |
---|
180 | otherwise we start generating the coinductive one, and on every function call |
---|
181 | use the choice method again to decide whether to step over or keep going. |
---|
182 | |
---|
183 | Not quite what we need - have to decide on seeing each label whether we will see |
---|
184 | another or hit a non-terminating call? |
---|
185 | |
---|
186 | Also - need the notion of well-labelled in order to break loops. |
---|
187 | |
---|
188 | |
---|
189 | |
---|
190 | outline: |
---|
191 | |
---|
192 | does function terminate? |
---|
193 | - yes, get (bound on the number of steps until return), generate finite |
---|
194 | structure using bound as termination witness |
---|
195 | - no, get (¬ bound on steps to return), start building infinite trace out of |
---|
196 | finite steps. At calls, check for termination, generate appr. form. |
---|
197 | |
---|
198 | generating the finite parts: |
---|
199 | |
---|
200 | We start with the status after the call has been executed; well-labelling tells |
---|
201 | us that this is a labelled state. Now we want to generate a trace_label_return |
---|
202 | and also return the remainder of the flat trace. |
---|
203 | |
---|
204 | *) |
---|
205 | |
---|
206 | (* [will_return ge depth s trace] says that after a finite number of steps of |
---|
207 | [trace] from [s] we reach the return state for the current function. [depth] |
---|
208 | performs the call/return counting necessary for handling deeper function |
---|
209 | calls. It should be zero at the top level. *) |
---|
210 | inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Prop ≝ |
---|
211 | | wr_step : ∀s,tr,s',depth,EX,trace. |
---|
212 | RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → |
---|
213 | will_return ge depth s' trace → |
---|
214 | will_return ge depth s (ft_step ?? ge s tr s' EX trace) |
---|
215 | | wr_call : ∀s,tr,s',depth,EX,trace. |
---|
216 | RTLabs_classify s = cl_call → |
---|
217 | will_return ge (S depth) s' trace → |
---|
218 | will_return ge depth s (ft_step ?? ge s tr s' EX trace) |
---|
219 | | wr_ret : ∀s,tr,s',depth,EX,trace. |
---|
220 | RTLabs_classify s = cl_return → |
---|
221 | will_return ge depth s' trace → |
---|
222 | will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace) |
---|
223 | (* Note that we require the ability to make a step after the return (this |
---|
224 | corresponds to somewhere that will be guaranteed to be a label at the |
---|
225 | end of the compilation chain). *) |
---|
226 | | wr_base : ∀s,tr,s',EX,trace. |
---|
227 | RTLabs_classify s = cl_return → |
---|
228 | will_return ge O s (ft_step ?? ge s tr s' EX trace) |
---|
229 | . |
---|
230 | |
---|
231 | discriminator nat. |
---|
232 | |
---|
233 | lemma will_return_call : ∀ge,depth,s,trace. |
---|
234 | will_return ge depth s trace → |
---|
235 | will_return ge (pred depth) s trace. |
---|
236 | #ge #depth #s #trace #H elim H |
---|
237 | [ #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %1 // |
---|
238 | | #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %2 // |
---|
239 | cases d in H1 H2 ⊢ %; // |
---|
240 | | #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 |
---|
241 | cases d in H1 H2 ⊢ %; [ #H1 #H2 %4 // | /2/ ] |
---|
242 | | #s1 #tr #s2 #EX #trc #CL %4 // |
---|
243 | ] qed. |
---|
244 | |
---|
245 | (* |
---|
246 | (* If we'll return then we must return from calls. *) |
---|
247 | lemma will_return_call : ∀ge,depth,s,trace. |
---|
248 | will_return ge (S depth) s trace → |
---|
249 | will_return ge depth s trace. |
---|
250 | #ge #depth #s #trace #H elim H in ⊢ ?; |
---|
251 | [ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/ |
---|
252 | | #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/ |
---|
253 | | #H204 #H205 #H206 #H207 #H208 #H209 #H210 #H211 #H212 #H213 /2/ |
---|
254 | | #H215 #H216 #H217 #H218 #H219 #H220 #H221 |
---|
255 | inversion H221 |
---|
256 | [ #H223 #H224 #H225 #H226 #H227 #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 destruct >H220 in H229; * #E destruct |
---|
257 | | #H237 #H238 #H239 #H240 #H241 #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 destruct >H220 in H243; #E destruct |
---|
258 | | #H265 #H266 #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 destruct |
---|
259 | | #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 destruct |
---|
260 | ] qed. check will_return_call. |
---|
261 | | #H130 #H131 #H132 #H133 #H134 #H135 |
---|
262 | inversion H |
---|
263 | [ #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 #H199 #H200 #H201 #H202 destruct |
---|
264 | cases H196 #E destruct |
---|
265 | |
---|
266 | |
---|
267 | let rec will_return_call ge depth s trace (H:will_return ge (S depth) s trace) |
---|
268 | on H : will_return ge depth s trace ≝ |
---|
269 | match H return λSdepth,s,trace. λ_. S depth = Sdepth → will_return ge depth s trace with |
---|
270 | [ wr_step s tr s' d EX trace CL H' ⇒ λE. wr_step ge s tr s' ? EX trace CL ? |
---|
271 | | wr_call s tr s' d EX trace CL H' ⇒ λE. ? |
---|
272 | | wr_ret s tr s' d EX trace CL H' ⇒ λE. ? |
---|
273 | | wr_base s tr s' EX trace CL ⇒ λE. ? |
---|
274 | ] (refl ? (S depth)). |
---|
275 | [ @(match E return λx,E. will_return ? x ?? → will_return ge ??? with [ refl ⇒ λH''.? ] H') |
---|
276 | @(will_return_call … H'') |
---|
277 | | *: cases daemon ] qed. |
---|
278 | | %2 /2/ |
---|
279 | | destruct cases d in H' ⊢ %; |
---|
280 | [ #H' @wr_base // |
---|
281 | | #d' #H' %3 /2/ |
---|
282 | ] |
---|
283 | | destruct |
---|
284 | ] qed. |
---|
285 | |
---|
286 | (* If we'll return then we must return from calls. *) |
---|
287 | lemma will_return_call : ∀ge,depth,s,trace. |
---|
288 | will_return ge (S depth) s trace → |
---|
289 | will_return ge depth s trace. |
---|
290 | #ge #depth #s #trace #H lapply (refl ? (S depth)) |
---|
291 | generalize in ⊢ (???(?%) → ??%??); elim H in ⊢ (∀_.???% → %); |
---|
292 | [ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %1 /2/ |
---|
293 | | #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %2 /2/ @H3 |
---|
294 | |
---|
295 | discriminator nat. |
---|
296 | |
---|
297 | |
---|
298 | |
---|
299 | (* Find time until a nested call completes. *) |
---|
300 | lemma nth_is_return_down : ∀ge,n,depth,s,trace. |
---|
301 | nth_is_return ge n (S depth) s trace → |
---|
302 | ∃m. nth_is_return ge m depth s trace. |
---|
303 | #ge #n elim n |
---|
304 | (* It's impossible to run out of time... *) |
---|
305 | [ #depth #s #trace #H inversion H |
---|
306 | [ #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct |
---|
307 | | #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct |
---|
308 | | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct |
---|
309 | | #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct |
---|
310 | ] |
---|
311 | | #n' #IH #depth #s #trace #H inversion H |
---|
312 | [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct |
---|
313 | cases (IH depth s1' trace1 ?) |
---|
314 | [ #m' #H' %{(S m')} %1 // |
---|
315 | | // |
---|
316 | ] |
---|
317 | | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct |
---|
318 | cases (IH (S depth) s1' trace1 ?) |
---|
319 | [ #m' #H' %{(S m')} %2 // |
---|
320 | | // |
---|
321 | ] |
---|
322 | | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct |
---|
323 | cases (depth1) in H2 ⊢ %; |
---|
324 | [ #H2 %{O} %4 // |
---|
325 | | #depth' #H2 cases (IH depth' s1' trace1 ?) |
---|
326 | [ #m' #H' %{(S m')} %3 // |
---|
327 | | // |
---|
328 | ] |
---|
329 | ] |
---|
330 | | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct |
---|
331 | ] |
---|
332 | ] qed. |
---|
333 | |
---|
334 | lemma nth_is_return_call : ∀ge,n,s,tr,s',EX,trace. |
---|
335 | RTLabs_classify s = cl_call → |
---|
336 | nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) → |
---|
337 | ∃m. nth_is_return ge m O s' trace. |
---|
338 | #ge #n #s #tr #s' #EX #trace #CLASS #H |
---|
339 | inversion H |
---|
340 | [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 * #H1 #H2 #_ #E1 #E2 #E3 @⊥ |
---|
341 | -H2 destruct >H1 in CLASS; #E destruct |
---|
342 | | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct |
---|
343 | @nth_is_return_down // |
---|
344 | | #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥ |
---|
345 | -H2 destruct |
---|
346 | | #s1 #tr1 #s1' #EX1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct |
---|
347 | ] qed. |
---|
348 | |
---|
349 | lemma nth_is_return_notfn : ∀ge,n,s,tr,s',EX,trace. |
---|
350 | RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → |
---|
351 | nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) → |
---|
352 | nth_is_return ge (pred n) O s' trace. |
---|
353 | #ge #n #s #tr #s' #EX #trace * #CL #TERM inversion TERM |
---|
354 | [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // |
---|
355 | | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct >H40 in CL; #E destruct |
---|
356 | | #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 destruct |
---|
357 | | #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct >H70 in CL; #E destruct |
---|
358 | | #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 destruct // |
---|
359 | | #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct >H100 in CL; #E destruct |
---|
360 | | #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 destruct |
---|
361 | | #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 destruct >H130 in CL; #E destruct |
---|
362 | ] qed. |
---|
363 | *) |
---|
364 | |
---|
365 | lemma will_return_notfn : ∀ge,s,tr,s',EX,trace. |
---|
366 | RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → |
---|
367 | will_return ge O s (ft_step ?? ge s tr s' EX trace) → |
---|
368 | will_return ge O s' trace. |
---|
369 | #ge #s #tr #s' #EX #trace * #CL #TERM inversion TERM |
---|
370 | [ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct // |
---|
371 | | #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 destruct >CL in H310; #E destruct |
---|
372 | | #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 destruct |
---|
373 | | #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 destruct >CL in H337; #E destruct |
---|
374 | | #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct // |
---|
375 | | #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 destruct >CL in H363; #E destruct |
---|
376 | | #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 destruct |
---|
377 | | #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 destruct >CL in H390; #E destruct |
---|
378 | ] qed. |
---|
379 | |
---|
380 | (* We require that labels appear after branch instructions and at the start of |
---|
381 | functions. The first is required for preciseness, the latter for soundness. |
---|
382 | We will make a separate requirement for there to be a finite number of steps |
---|
383 | between labels to catch loops for soundness (is this sufficient?). *) |
---|
384 | |
---|
385 | definition well_cost_labelled_statement : ∀f:internal_function. ∀s. labels_present (f_graph f) s → Prop ≝ |
---|
386 | λf,s. match s return λs. labels_present ? s → Prop with |
---|
387 | [ St_cond _ l1 l2 ⇒ λH. |
---|
388 | is_cost_label (lookup_present … (f_graph f) l1 ?) = true ∧ |
---|
389 | is_cost_label (lookup_present … (f_graph f) l2 ?) = true |
---|
390 | | St_jumptable _ ls ⇒ λH. |
---|
391 | (* I did have a dependent version of All here, but it's a pain. *) |
---|
392 | All … (λl. ∃H. is_cost_label (lookup_present … (f_graph f) l H) = true) ls |
---|
393 | | _ ⇒ λ_. True |
---|
394 | ]. whd in H; |
---|
395 | [ @(proj1 … H) |
---|
396 | | @(proj2 … H) |
---|
397 | ] qed. |
---|
398 | |
---|
399 | definition well_cost_labelled_fn : internal_function → Prop ≝ |
---|
400 | λf. (∀l. ∀H:present … (f_graph f) l. |
---|
401 | well_cost_labelled_statement f (lookup_present … (f_graph f) l H) (f_closed f l …)) ∧ |
---|
402 | is_cost_label (lookup_present … (f_graph f) (f_entry f) ?) = true. |
---|
403 | [ @lookup_lookup_present | cases (f_entry f) // ] qed. |
---|
404 | |
---|
405 | (* We need to ensure that any code we come across is well-cost-labelled. We may |
---|
406 | get function code from either the global environment or the state. *) |
---|
407 | |
---|
408 | definition well_cost_labelled_ge : genv → Prop ≝ |
---|
409 | λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → well_cost_labelled_fn f. |
---|
410 | |
---|
411 | definition well_cost_labelled_state : state → Prop ≝ |
---|
412 | λs. match s with |
---|
413 | [ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs |
---|
414 | | Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧ |
---|
415 | All ? (λf. well_cost_labelled_fn (func f)) fs |
---|
416 | | Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs |
---|
417 | ]. |
---|
418 | |
---|
419 | lemma well_cost_labelled_state_step : ∀ge,s,tr,s'. |
---|
420 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
421 | well_cost_labelled_ge ge → |
---|
422 | well_cost_labelled_state s → |
---|
423 | well_cost_labelled_state s'. |
---|
424 | #ge #s #tr' #s' #EV cases (eval_perserves … EV) |
---|
425 | [ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % // |
---|
426 | | #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/ |
---|
427 | | #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/ |
---|
428 | | #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/ |
---|
429 | | #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2 |
---|
430 | | #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % // |
---|
431 | ] qed. |
---|
432 | |
---|
433 | lemma rtlabs_jump_inv : ∀s. |
---|
434 | RTLabs_classify s = cl_jump → |
---|
435 | ∃f,fs,m. s = State f fs m ∧ |
---|
436 | let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in |
---|
437 | (∃r,l1,l2. stmt = St_cond r l1 l2) ∨ (∃r,ls. stmt = St_jumptable r ls). |
---|
438 | * |
---|
439 | [ #f #fs #m #E |
---|
440 | %{f} %{fs} %{m} % |
---|
441 | [ @refl |
---|
442 | | whd in E:(??%?); cases (lookup_present ? statement ???) in E ⊢ %; |
---|
443 | try (normalize try #A try #B try #C try #D try #F try #G try #H destruct) |
---|
444 | [ %1 %{A} %{B} %{C} @refl |
---|
445 | | %2 %{A} %{B} @refl |
---|
446 | ] |
---|
447 | ] |
---|
448 | | normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct |
---|
449 | | normalize #H8 #H9 #H10 #H11 #H12 destruct |
---|
450 | ] qed. |
---|
451 | |
---|
452 | lemma well_cost_labelled_jump : ∀ge,s,tr,s'. |
---|
453 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
454 | well_cost_labelled_state s → |
---|
455 | RTLabs_classify s = cl_jump → |
---|
456 | RTLabs_cost s' = true. |
---|
457 | #ge #s #tr #s' #EV #H #CL |
---|
458 | cases (rtlabs_jump_inv s CL) |
---|
459 | #fr * #fs * #m * #Es * |
---|
460 | [ * #r * #l1 * #l2 #Estmt |
---|
461 | >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs |
---|
462 | >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); |
---|
463 | >Estmt #LP whd in ⊢ (??%? → ?); |
---|
464 | (* replace with lemma on successors? *) |
---|
465 | @bindIO_value #v #Ev @bindIO_value * #Eb whd in ⊢ (??%? → ?); #E destruct |
---|
466 | lapply (Hbody (next fr) (next_ok fr)) |
---|
467 | generalize in ⊢ (???% → ?); |
---|
468 | >Estmt #LP' |
---|
469 | whd in ⊢ (% → ?); |
---|
470 | * #H1 #H2 [ @H1 | @H2 ] |
---|
471 | | * #r * #ls #Estmt |
---|
472 | >Es in H; whd in ⊢ (% → ?); * * #Hbody #_ #Hfs |
---|
473 | >Es in EV; whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); |
---|
474 | >Estmt #LP whd in ⊢ (??%? → ?); |
---|
475 | (* replace with lemma on successors? *) |
---|
476 | @bindIO_value #a cases a [ | #sz #i | #f | #r | #ptr ] #Ea whd in ⊢ (??%? → ?); |
---|
477 | [ 2: (* later *) |
---|
478 | | *: #E destruct |
---|
479 | ] |
---|
480 | lapply (Hbody (next fr) (next_ok fr)) |
---|
481 | generalize in ⊢ (???% → ?); >Estmt #LP' whd in ⊢ (% → ?); #CP |
---|
482 | generalize in ⊢ (??(?%)? → ?); |
---|
483 | cases (nth_opt label (nat_of_bitvector (bitsize_of_intsize sz) i) ls) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?); |
---|
484 | [ #E1 #E2 whd in E2:(??%?); destruct |
---|
485 | | #l' #E1 #E2 whd in E2:(??%?); destruct |
---|
486 | cases (All_nth ???? CP ? E1) |
---|
487 | #H1 #H2 @H2 |
---|
488 | ] |
---|
489 | ] qed. |
---|
490 | |
---|
491 | lemma rtlabs_call_inv : ∀s. |
---|
492 | RTLabs_classify s = cl_call → |
---|
493 | ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m. |
---|
494 | * [ #f #fs #m whd in ⊢ (??%? → ?); |
---|
495 | cases (lookup_present … (next f) (next_ok f)) normalize |
---|
496 | try #A try #B try #C try #D try #E try #F try #G destruct |
---|
497 | | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl |
---|
498 | | normalize #H411 #H412 #H413 #H414 #H415 destruct |
---|
499 | ] qed. |
---|
500 | |
---|
501 | lemma well_cost_labelled_call : ∀ge,s,tr,s'. |
---|
502 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
503 | well_cost_labelled_state s → |
---|
504 | RTLabs_classify s = cl_call → |
---|
505 | RTLabs_cost s' = true. |
---|
506 | #ge #s #tr #s' #EV #WCL #CL |
---|
507 | cases (rtlabs_call_inv s CL) |
---|
508 | #fd * #args * #dst * #stk * #m #E >E in EV WCL; |
---|
509 | whd in ⊢ (??%? → % → ?); |
---|
510 | cases fd |
---|
511 | [ #fn whd in ⊢ (??%? → % → ?); |
---|
512 | @bindIO_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any) |
---|
513 | #m' #b whd in ⊢ (??%? → ?); #E' destruct |
---|
514 | * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3 |
---|
515 | @WCL2 |
---|
516 | | #fn whd in ⊢ (??%? → % → ?); |
---|
517 | @bindIO_value #evargs #Eargs |
---|
518 | @bindIO_value #evres #Eres |
---|
519 | normalize in Eres; destruct |
---|
520 | ] qed. |
---|
521 | |
---|
522 | (* Don't need to know that labels break loops because we have termination. *) |
---|
523 | |
---|
524 | record trace_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ { |
---|
525 | new_state : state; |
---|
526 | remainder : flat_trace io_out io_in ge new_state; |
---|
527 | cost_labelled : well_cost_labelled_state new_state; |
---|
528 | new_trace : T new_state |
---|
529 | }. |
---|
530 | |
---|
531 | record sub_trace_result (ge:genv) (T:trace_ends_with_ret → state → Type[0]) : Type[0] ≝ { |
---|
532 | ends : trace_ends_with_ret; |
---|
533 | trace_res :> trace_result ge (T ends); |
---|
534 | terminates : |
---|
535 | (* We handle returns specially *) |
---|
536 | match ends with |
---|
537 | [ doesnt_end_with_ret ⇒ will_return ge O (new_state ?? trace_res) (remainder ?? trace_res) |
---|
538 | | ends_with_ret ⇒ True |
---|
539 | ] |
---|
540 | }. |
---|
541 | |
---|
542 | definition replace_sub_trace : ∀ge,T1,T2. |
---|
543 | ∀r:sub_trace_result ge T1. T2 (ends … r) (new_state … r) →sub_trace_result ge T2 ≝ |
---|
544 | λge,T1,T2,r,trace. |
---|
545 | mk_sub_trace_result ge T2 |
---|
546 | (ends … r) |
---|
547 | (mk_trace_result ge (T2 (ends … r)) |
---|
548 | (new_state … r) |
---|
549 | (remainder … r) |
---|
550 | (cost_labelled … r) |
---|
551 | trace |
---|
552 | ) |
---|
553 | (terminates … r) |
---|
554 | . |
---|
555 | |
---|
556 | definition replace_trace : ∀ge,T1,T2. |
---|
557 | ∀r:trace_result ge T1. T2 (new_state … r) → trace_result ge T2 ≝ |
---|
558 | λge,T1,T2,r,trace. |
---|
559 | mk_trace_result ge T2 |
---|
560 | (new_state … r) |
---|
561 | (remainder … r) |
---|
562 | (cost_labelled … r) |
---|
563 | trace |
---|
564 | . |
---|
565 | |
---|
566 | let rec make_label_return ge s |
---|
567 | (trace: flat_trace io_out io_in ge s) |
---|
568 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
569 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
570 | (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) |
---|
571 | (TERMINATES: will_return ge O s trace) |
---|
572 | : trace_result ge (trace_label_return (RTLabs_status ge) s) ≝ |
---|
573 | |
---|
574 | let r ≝ make_label_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES in |
---|
575 | match ends … r return λx. trace_label_label ? x ?? → match x with [doesnt_end_with_ret⇒ ?|_⇒ ?] → ? with |
---|
576 | [ ends_with_ret ⇒ λtll,term. |
---|
577 | replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll) |
---|
578 | | doesnt_end_with_ret ⇒ λtll,term. |
---|
579 | let r' ≝ make_label_return ge (new_state … r) |
---|
580 | (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? term in |
---|
581 | replace_trace … r' |
---|
582 | (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r')) |
---|
583 | ] (new_trace … r) (terminates … r) |
---|
584 | |
---|
585 | and make_label_label ge s |
---|
586 | (trace: flat_trace io_out io_in ge s) |
---|
587 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
588 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
589 | (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) |
---|
590 | (TERMINATES: will_return ge O s trace) |
---|
591 | : sub_trace_result ge (λends. trace_label_label (RTLabs_status ge) ends s) ≝ |
---|
592 | let r ≝ make_any_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES in |
---|
593 | replace_sub_trace ??? r |
---|
594 | (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) |
---|
595 | |
---|
596 | and make_any_label ge s |
---|
597 | (trace: flat_trace io_out io_in ge s) |
---|
598 | (ENV_COSTLABELLED: well_cost_labelled_ge ge) |
---|
599 | (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) |
---|
600 | (TERMINATES: will_return ge O s trace) |
---|
601 | : sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) ≝ |
---|
602 | match trace return λs,trace. well_cost_labelled_state s → will_return ??? trace → sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) with |
---|
603 | [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ? |
---|
604 | | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES. |
---|
605 | match RTLabs_classify start return λx. RTLabs_classify start = x → ? with |
---|
606 | [ cl_other ⇒ λCL. |
---|
607 | match RTLabs_cost next return λx. RTLabs_cost next = x → ? with |
---|
608 | [ true ⇒ λCS. |
---|
609 | mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ? |
---|
610 | | false ⇒ λCS. |
---|
611 | let r ≝ make_any_label ge next trace' ENV_COSTLABELLED ?? in |
---|
612 | replace_sub_trace ??? r |
---|
613 | (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??) |
---|
614 | ] (refl ??) |
---|
615 | | cl_jump ⇒ λCL. |
---|
616 | mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ? |
---|
617 | | cl_call ⇒ λCL. |
---|
618 | let r ≝ make_label_return ge next trace' ENV_COSTLABELLED ??? in |
---|
619 | let r' ≝ make_any_label ge (new_state … r) (remainder … r) ENV_COSTLABELLED ?? in |
---|
620 | replace_sub_trace ??? r' |
---|
621 | (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r')) |
---|
622 | | cl_return ⇒ λCL. |
---|
623 | mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) ends_with_ret (mk_trace_result ge ? next trace' ? (tal_base_return (RTLabs_status ge) start next ? CL)) ? |
---|
624 | ] (refl ? (RTLabs_classify start)) |
---|
625 | | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥ |
---|
626 | ] STATE_COSTLABELLED TERMINATES. |
---|
627 | |
---|
628 | [ @(trace_label_label_label … tll) |
---|
629 | | |
---|
630 | | %{tr} @EV |
---|
631 | | @(well_cost_labelled_state_step … EV) // |
---|
632 | | @I |
---|
633 | | %{tr} @EV |
---|
634 | | % whd in ⊢ (% → ?); >CL #E destruct |
---|
635 | | @(well_cost_labelled_jump … EV) // |
---|
636 | | @(well_cost_labelled_state_step … EV) // |
---|
637 | | @(will_return_notfn … TERMINATES) %2 @CL |
---|
638 | | (* oh dear *) |
---|
639 | | %{tr} @EV |
---|
640 | | @(cost_labelled … r) |
---|
641 | | |
---|
642 | | |
---|
643 | | |
---|
644 | |
---|
645 | @(well_cost_labelled_state_step … EV) // |
---|
646 | | % whd in ⊢ (% → ?); >CL #E destruct |
---|
647 | | @CS |
---|
648 | | @(nth_is_return_notfn … TERMINATES) %1 @CL |
---|
649 | | % whd in ⊢ (% → ?); >CS #E destruct |
---|
650 | | @CL |
---|
651 | | %{tr} @EV |
---|
652 | | @(well_cost_labelled_state_step … EV) // |
---|
653 | | @(nth_is_return_notfn … TERMINATES) %1 @CL |
---|
654 | | inversion TERMINATES |
---|
655 | [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 -TERMINATES destruct |
---|
656 | | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 -TERMINATES destruct |
---|
657 | | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 -TERMINATES destruct |
---|
658 | | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 -TERMINATES destruct |
---|
659 | ] |
---|
660 | | |
---|
661 | |
---|
662 | |
---|
663 | |
---|
664 | (* FIXME: there's trouble at the end of the program because we can't make a step |
---|
665 | away from the final return. *) |
---|