1 | include "common/Executions.ma". |
---|
2 | include "common/StructuredTraces.ma". (* just for status_class *) |
---|
3 | |
---|
4 | (* A small-step executable semantics, together with some kind of global |
---|
5 | environment, notion of cost labelled state, classification function and |
---|
6 | stack costs. *) |
---|
7 | |
---|
8 | record classified_system : Type[2] ≝ { |
---|
9 | cs_exec :> fullexec io_out io_in; |
---|
10 | cs_global : global … cs_exec; |
---|
11 | cs_labelled : state … cs_exec cs_global → bool; |
---|
12 | cs_classify : state … cs_exec cs_global → status_class; |
---|
13 | cs_callee : ∀s. match cs_classify … s with [ cl_call ⇒ True | _ ⇒ False ] → ident |
---|
14 | }. |
---|
15 | |
---|
16 | definition cs_state : classified_system → Type[0] ≝ |
---|
17 | λC. state … C (cs_global … C). |
---|
18 | |
---|
19 | (* Ideally we would also allow measurable traces to be from one cost label to |
---|
20 | another (in the same function call), but due to time constraints we'll stick |
---|
21 | to ending measurable traces at the end of the function only. |
---|
22 | *) |
---|
23 | |
---|
24 | definition trace_is_label_to_return : ∀C. list (cs_state … C × trace) → Prop ≝ |
---|
25 | λC,x. ∃tr1,s1,x',tr2,s2. x = 〈s1,tr1〉::(x'@[〈s2,tr2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return. |
---|
26 | |
---|
27 | definition intensional_event_of_event : event → list intensional_event ≝ |
---|
28 | λev. match ev with |
---|
29 | [ EVcost l ⇒ [ IEVcost l ] |
---|
30 | | EVextcall _ _ _ ⇒ [ ] (* No equivalent, but there shouldn't be any for now *) |
---|
31 | ]. |
---|
32 | |
---|
33 | definition intensional_events_of_events : trace → list intensional_event ≝ |
---|
34 | λtr. flatten ? (map ?? intensional_event_of_event tr). |
---|
35 | |
---|
36 | let rec intensional_trace_of_trace C (callstack:list ident) (trace:list (cs_state … C × trace)) on trace : list ident × (list intensional_event) ≝ |
---|
37 | match trace with |
---|
38 | [ nil ⇒ 〈callstack, [ ]〉 |
---|
39 | | cons str tl ⇒ |
---|
40 | let 〈s,tr〉 ≝ str in |
---|
41 | let 〈callstack, call_event〉 ≝ |
---|
42 | match cs_classify C s return λx. (match x with [ cl_call ⇒ True | _ ⇒ False ] → ident) → list ident × (list intensional_event) with |
---|
43 | [ cl_call ⇒ λcallee. let id ≝ callee I in 〈id::callstack, [IEVcall id]〉 |
---|
44 | | cl_return ⇒ λ_. match callstack with [ nil ⇒ 〈[ ], [ ]〉 | cons id tl ⇒ 〈tl, [IEVret id]〉 ] |
---|
45 | | _ ⇒ λ_. 〈callstack, [ ]〉 |
---|
46 | ] (cs_callee C s) in |
---|
47 | let other_events ≝ intensional_events_of_events tr in |
---|
48 | let 〈callstack,rem〉 ≝ intensional_trace_of_trace C callstack tl in |
---|
49 | 〈callstack, call_event@other_events@rem〉 |
---|
50 | ]. |
---|
51 | |
---|
52 | definition normal_state : ∀C:classified_system. cs_state … C → bool ≝ |
---|
53 | λC,s. match cs_classify C s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
54 | |
---|
55 | lemma normal_state_inv : ∀C,s. |
---|
56 | normal_state C s → |
---|
57 | cs_classify C s = cl_other ∨ cs_classify C s = cl_jump. |
---|
58 | #C #s whd in ⊢ (?% → ?); cases (cs_classify C s) /2/ * |
---|
59 | qed. |
---|
60 | |
---|
61 | lemma int_trace_of_normal : ∀C,callstack,s,tr,trace. |
---|
62 | normal_state C s → |
---|
63 | intensional_trace_of_trace C callstack (〈s,tr〉::trace) = |
---|
64 | (let 〈stk',tl〉 ≝ intensional_trace_of_trace C callstack trace in |
---|
65 | 〈stk', (intensional_events_of_events tr)@tl〉). |
---|
66 | #C #callstack #s #tr #trace #NORMAL |
---|
67 | whd in ⊢ (??%?); |
---|
68 | generalize in match (cs_callee C s); |
---|
69 | cases (normal_state_inv … NORMAL) |
---|
70 | #CL >CL normalize nodelta #_ |
---|
71 | cases (intensional_trace_of_trace C callstack trace) |
---|
72 | #callstack' #tl normalize nodelta |
---|
73 | % |
---|
74 | qed. |
---|
75 | |
---|
76 | lemma flatten_append : ∀A,l1,l2. |
---|
77 | flatten A (l1@l2) = (flatten A l1)@(flatten A l2). |
---|
78 | #A #l1 #l2 |
---|
79 | elim l1 |
---|
80 | [ % |
---|
81 | | #h #t #IH whd in ⊢ (??%(??%?)); |
---|
82 | change with (flatten ??) in match (foldr ?????); >IH |
---|
83 | change with (flatten ??) in match (foldr ?????); |
---|
84 | >associative_append % |
---|
85 | ] qed. |
---|
86 | |
---|
87 | |
---|
88 | lemma int_events_append : ∀tr1,tr2. |
---|
89 | intensional_events_of_events (tr1@tr2) = (intensional_events_of_events tr1)@(intensional_events_of_events tr2). |
---|
90 | #tr1 #tr2 |
---|
91 | change with (flatten ??) in ⊢ (??%(??%%)); |
---|
92 | <map_append >flatten_append % |
---|
93 | qed. |
---|
94 | |
---|
95 | |
---|
96 | lemma int_trace_irr : ∀C,callstack,s,trace. |
---|
97 | normal_state C s → |
---|
98 | intensional_trace_of_trace C callstack (〈s,E0〉::trace) = intensional_trace_of_trace C callstack trace. |
---|
99 | #C #callstate #s #trace #NORMAL >(int_trace_of_normal … NORMAL) |
---|
100 | cases (intensional_trace_of_trace ???) // |
---|
101 | qed. |
---|
102 | |
---|
103 | lemma int_trace_append : ∀C,callstack,s,t1,t2,trace. |
---|
104 | normal_state C s → |
---|
105 | intensional_trace_of_trace C callstack (〈s,t1@t2〉::trace) = intensional_trace_of_trace C callstack (〈s,t1〉::〈s,t2〉::trace). |
---|
106 | #C #callstack #s #t1 #t2 #trace #NORMAL |
---|
107 | >(int_trace_of_normal … NORMAL) |
---|
108 | >(int_trace_of_normal … NORMAL) |
---|
109 | >(int_trace_of_normal … NORMAL) |
---|
110 | cases (intensional_trace_of_trace ???) #callstack' #trace' |
---|
111 | normalize nodelta |
---|
112 | >int_events_append |
---|
113 | >associative_append % |
---|
114 | qed. |
---|
115 | |
---|
116 | lemma build_eq_trace : ∀C,C',callstack,s,trace,rem,rem'. |
---|
117 | normal_state C s → |
---|
118 | all … (λstr. normal_state C' (\fst str)) trace → |
---|
119 | intensional_trace_of_trace C callstack rem = intensional_trace_of_trace C' callstack rem' → |
---|
120 | intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem'). |
---|
121 | #C #C' #callstack #s #trace #rem #rem' #NORMAL #NORMAL' |
---|
122 | >(int_trace_of_normal … NORMAL) |
---|
123 | cases (intensional_trace_of_trace C callstack rem) #callstack' #trace' |
---|
124 | #REM whd in ⊢ (??%?); |
---|
125 | elim trace in NORMAL' ⊢ %; |
---|
126 | [ #_ @REM |
---|
127 | | * #s' #tr' #tl #IH #NORMAL' |
---|
128 | cases (andb_Prop_true … NORMAL') #NORMALs #NORMALtl |
---|
129 | >int_trace_of_normal |
---|
130 | [ <(IH NORMALtl) whd in match (gather_trace ??); whd in ⊢ (???%); |
---|
131 | >int_events_append >associative_append % |
---|
132 | | @NORMALs |
---|
133 | ] |
---|
134 | ] qed. |
---|
135 | |
---|
136 | lemma int_trace_append' : ∀C,t1,t2,callstack. |
---|
137 | intensional_trace_of_trace C callstack (t1@t2) = |
---|
138 | (let 〈cs',t1'〉 ≝ intensional_trace_of_trace C callstack t1 in |
---|
139 | let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C cs' t2 in |
---|
140 | 〈cs'', t1'@t2'〉). |
---|
141 | #C #t1 #t2 elim t1 |
---|
142 | [ #callstack whd in match ([ ]@t2); whd in ⊢ (???%); |
---|
143 | cases (intensional_trace_of_trace ???) #cs' #trace' % |
---|
144 | | * #s #tr #tl #IH |
---|
145 | #callstack |
---|
146 | whd in match (intensional_trace_of_trace ???); |
---|
147 | whd in match (intensional_trace_of_trace ???); |
---|
148 | generalize in match (cs_callee C s); |
---|
149 | cases (cs_classify C s) |
---|
150 | normalize nodelta #callee |
---|
151 | [ cases callstack [2: #cshd #cdtl] normalize nodelta ] |
---|
152 | >IH cases (intensional_trace_of_trace C ? tl) #cs' #tl' |
---|
153 | normalize nodelta |
---|
154 | cases (intensional_trace_of_trace C ? t2) #cs'' #tl'' |
---|
155 | normalize nodelta >associative_append >associative_append |
---|
156 | % |
---|
157 | ] qed. |
---|
158 | |
---|
159 | lemma int_trace_normal_cs : ∀C,callstack,trace. |
---|
160 | all ? (λstr. normal_state C (\fst str)) trace → |
---|
161 | callstack = \fst (intensional_trace_of_trace C callstack trace). |
---|
162 | #C #callstack #trace elim trace |
---|
163 | [ // |
---|
164 | | * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl |
---|
165 | >(int_trace_of_normal … N1) |
---|
166 | >(IH Ntl) in ⊢ (??%?); |
---|
167 | cases (intensional_trace_of_trace ???) /2/ |
---|
168 | ] qed. |
---|
169 | |
---|
170 | lemma int_trace_append_normal : ∀C,t1,t2,callstack. |
---|
171 | all ? (λstr. normal_state C (\fst str)) t1 → |
---|
172 | intensional_trace_of_trace C callstack (t1@t2) = |
---|
173 | (let t1' ≝ \snd (intensional_trace_of_trace C callstack t1) in |
---|
174 | let 〈cs'',t2'〉 ≝ intensional_trace_of_trace C callstack t2 in |
---|
175 | 〈cs'', t1'@t2'〉). |
---|
176 | #C #t1 #t2 #callstack #NORMAL lapply (int_trace_append' C t1 t2 callstack) |
---|
177 | lapply (int_trace_normal_cs C callstack t1 NORMAL) |
---|
178 | cases (intensional_trace_of_trace ?? t1) #cs #tl #E destruct // |
---|
179 | qed. |
---|
180 | |
---|
181 | lemma build_return_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem'. |
---|
182 | cs_classify C s = cl_return → |
---|
183 | cs_classify C' s' = cl_return → |
---|
184 | all ? (λstr. normal_state C' (\fst str)) trace' → |
---|
185 | intensional_trace_of_trace C (tail … callstack) rem = intensional_trace_of_trace C' (tail … callstack) rem' → |
---|
186 | let trace ≝ 〈s',tr〉::trace' in |
---|
187 | intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem'). |
---|
188 | #C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL #E |
---|
189 | whd |
---|
190 | whd in ⊢ (??%%); normalize nodelta |
---|
191 | generalize in match (cs_callee C s); generalize in match (cs_callee C' s'); |
---|
192 | >CL >CL' normalize nodelta #_ #_ |
---|
193 | cases callstack in E ⊢ %; [2: #stkhd #stktl] |
---|
194 | normalize nodelta |
---|
195 | cases (intensional_trace_of_trace ?? rem) #cs_rem #ev_rem normalize nodelta |
---|
196 | >(int_trace_append_normal … NORMAL) normalize nodelta |
---|
197 | cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E |
---|
198 | destruct @eq_f @eq_f |
---|
199 | whd in match (gather_trace ??); >int_events_append |
---|
200 | >associative_append @eq_f |
---|
201 | elim trace in NORMAL ⊢ %; |
---|
202 | [ 1,3: #_ % |
---|
203 | | 2,4: |
---|
204 | * #s1 #tr1 #tl #IH |
---|
205 | #N cases (andb_Prop_true … N) #N1 #Ntl |
---|
206 | whd in match (gather_trace ??); >int_events_append |
---|
207 | >associative_append >(IH Ntl) |
---|
208 | >(int_trace_of_normal … N1) |
---|
209 | cases (intensional_trace_of_trace ?? tl) |
---|
210 | #cs' #tl' >associative_append % |
---|
211 | ] qed. |
---|
212 | |
---|
213 | lemma generalize_callee : ∀C,s,H. ∀P: ? → ? → Prop. |
---|
214 | (∀f. P f (f H)) → |
---|
215 | P (cs_callee C s) (cs_callee C s H). |
---|
216 | #C #s #H #P #f @f |
---|
217 | qed. |
---|
218 | |
---|
219 | lemma build_call_trace : ∀C,C',callstack,s,s',tr,trace',rem,rem',H,H'. |
---|
220 | all ? (λstr. normal_state C' (\fst str)) trace' → |
---|
221 | intensional_trace_of_trace C (cs_callee C s H::callstack) rem = intensional_trace_of_trace C' (cs_callee C s H::callstack) rem' → |
---|
222 | cs_callee C s H = cs_callee C' s' H' → |
---|
223 | let trace ≝ 〈s',tr〉::trace' in |
---|
224 | intensional_trace_of_trace C callstack (〈s,gather_trace … trace〉::rem) = intensional_trace_of_trace C' callstack (trace@rem'). |
---|
225 | #C #C' #callstack #s #s' #tr #trace #rem #rem' #CL #CL' #NORMAL |
---|
226 | whd in ⊢ (? → ? → %); |
---|
227 | whd in ⊢ (? → ? → ??%%); normalize nodelta |
---|
228 | @generalize_callee |
---|
229 | @generalize_callee |
---|
230 | cases (cs_classify C s) in CL ⊢ %; * cases (cs_classify C' s') in CL' ⊢ %; * |
---|
231 | normalize nodelta #calleef #calleef' #E #CALLEE <CALLEE |
---|
232 | cases (intensional_trace_of_trace ?? rem) in E ⊢ %; #cs_rem #ev_rem normalize nodelta |
---|
233 | >(int_trace_append_normal … NORMAL) normalize nodelta |
---|
234 | cases (intensional_trace_of_trace ?? rem') #cs_rem' #ev_rem' normalize nodelta #E |
---|
235 | destruct @eq_f @eq_f |
---|
236 | whd in match (gather_trace ??); >int_events_append |
---|
237 | >associative_append @eq_f |
---|
238 | elim trace in NORMAL ⊢ %; |
---|
239 | [ 1,3: #_ % |
---|
240 | | 2,4: |
---|
241 | * #s1 #tr1 #tl #IH |
---|
242 | #N cases (andb_Prop_true … N) #N1 #Ntl |
---|
243 | whd in match (gather_trace ??); >int_events_append |
---|
244 | >associative_append >(IH Ntl) |
---|
245 | >(int_trace_of_normal … N1) |
---|
246 | cases (intensional_trace_of_trace ?? tl) |
---|
247 | #cs' #tl' >associative_append % |
---|
248 | ] qed. |
---|
249 | |
---|
250 | |
---|
251 | definition measure_stack : (ident → nat) → nat → list intensional_event → nat × nat ≝ |
---|
252 | λcosts,start. |
---|
253 | foldl ?? (λx. λev. |
---|
254 | match ev with |
---|
255 | [ IEVcall id ⇒ |
---|
256 | let 〈current_stack,max_stack〉 ≝ x in |
---|
257 | let new_stack ≝ current_stack + costs id in |
---|
258 | 〈new_stack, max new_stack max_stack〉 |
---|
259 | | IEVret id ⇒ |
---|
260 | let 〈current_stack,max_stack〉 ≝ x in |
---|
261 | 〈current_stack - costs id, max_stack〉 |
---|
262 | | _ ⇒ x |
---|
263 | ]) 〈start,start〉. |
---|
264 | |
---|
265 | definition max_stack : (ident → nat) → nat → list intensional_event → nat ≝ |
---|
266 | λcosts, start, trace. \snd (measure_stack costs start trace). |
---|
267 | |
---|
268 | lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f. |
---|
269 | (∀acc,el. P acc → P (f acc el)) → |
---|
270 | ∀l,acc. P acc → |
---|
271 | P (foldl A B f acc l). |
---|
272 | #A #B #P #f #IH #l elim l |
---|
273 | [ // |
---|
274 | | #h #t #IH' #acc #H @IH' @IH @H |
---|
275 | ] qed. |
---|
276 | (* |
---|
277 | lemma max_stack_step : ∀C,a,m,a',m',tr,s. |
---|
278 | measure_stack_aux C 〈a,m〉 〈s,tr〉 = 〈a',m'〉 → |
---|
279 | m' = max m a'. |
---|
280 | #C #a #m #a' #m' #tr #s |
---|
281 | whd in match (measure_stack_aux ???); |
---|
282 | generalize in match (cs_stack C s); cases (cs_classify C s) #f |
---|
283 | normalize nodelta #E destruct // |
---|
284 | qed. |
---|
285 | |
---|
286 | lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',str. |
---|
287 | measure_stack_aux C 〈a,m1〉 str = 〈a1',m1'〉 → |
---|
288 | measure_stack_aux C 〈a,m2〉 str = 〈a2',m2'〉 → |
---|
289 | a1' = a2'. |
---|
290 | #C #a #a1' #a2' #m1 #m2 #m1' #m2' * #s #tr |
---|
291 | whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???); |
---|
292 | generalize in match (cs_stack C s); cases (cs_classify C s) #f |
---|
293 | normalize nodelta |
---|
294 | #E1 #E2 destruct |
---|
295 | % |
---|
296 | qed. |
---|
297 | |
---|
298 | |
---|
299 | lemma max_stack_steps : ∀C,trace,a,m. |
---|
300 | \snd (foldl … (measure_stack_aux C) 〈a,m〉 trace) = |
---|
301 | max m (\snd (foldl … (measure_stack_aux C) 〈a,0〉 trace)). |
---|
302 | #C #trace elim trace |
---|
303 | [ #a #m >max_n_O % |
---|
304 | | * #tr #s #tl #IH #a #m |
---|
305 | whd in match (foldl ?????); |
---|
306 | letin x ≝ (measure_stack_aux ???) lapply (refl ? x) cases x in ⊢ (???% → %); #a' #m' #M |
---|
307 | whd in match (foldl ??? 〈a,O〉 ?); |
---|
308 | letin y ≝ (measure_stack_aux ? 〈a,O〉 ?) lapply (refl ? y) cases y in ⊢ (???% → %); #a'' #m'' #M' |
---|
309 | >(IH a'') >IH |
---|
310 | >(max_stack_step … M) |
---|
311 | >(max_stack_step … M') >max_O_n >(max_stack_step' … M M') >associative_max % |
---|
312 | ] qed. |
---|
313 | |
---|
314 | lemma max_stack_append : ∀C,c1,ex1,ex2. |
---|
315 | max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2). |
---|
316 | #C #c1 #ex1 #ex2 |
---|
317 | whd in match (max_stack ???); whd in match (stack_after ???); |
---|
318 | whd in match (max_stack ?? (ex1@ex2)); |
---|
319 | whd in match (measure_stack ???); whd in match (measure_stack ?? (ex1@ex2)); |
---|
320 | generalize in match O; generalize in match c1; elim ex1 |
---|
321 | [ #c #m whd in ⊢ (??(?%?)%); >max_stack_steps % |
---|
322 | | * #tr #s #tl #IH #c #m |
---|
323 | whd in match (foldl ?????); whd in ⊢ (???(???%)); |
---|
324 | lapply (refl ? (measure_stack_aux C 〈c1,m〉 〈tr,s〉)) |
---|
325 | cases (measure_stack_aux ???) in ⊢ (???% → %); #a' #m' #M |
---|
326 | >IH % |
---|
327 | ] qed. |
---|
328 | *) |
---|
329 | |
---|
330 | (* Check that the trace ends with the return from the starting function and one |
---|
331 | further state. *) |
---|
332 | |
---|
333 | let rec will_return_aux C (depth:nat) |
---|
334 | (trace:list (cs_state … C × trace)) on trace : bool ≝ |
---|
335 | match trace with |
---|
336 | [ nil ⇒ false |
---|
337 | | cons h tl ⇒ |
---|
338 | let 〈s,tr〉 ≝ h in |
---|
339 | match cs_classify C s with |
---|
340 | [ cl_call ⇒ will_return_aux C (S depth) tl |
---|
341 | | cl_return ⇒ |
---|
342 | match depth with |
---|
343 | (* The state after the return will appear in the structured trace, but |
---|
344 | not here because it is the second part of the pair returned by |
---|
345 | exec_steps. *) |
---|
346 | [ O ⇒ match tl with [ nil ⇒ true | _ ⇒ false ] |
---|
347 | | S d ⇒ will_return_aux C d tl |
---|
348 | ] |
---|
349 | | _ ⇒ will_return_aux C depth tl |
---|
350 | ] |
---|
351 | ]. |
---|
352 | definition will_return' : ∀C. list (cs_state … C × trace) → bool ≝ λC. will_return_aux C O. |
---|
353 | |
---|
354 | (* Like classified_system, but we don't fix the global environment so that we |
---|
355 | talk about the program separately. *) |
---|
356 | |
---|
357 | record preclassified_system : Type[2] ≝ { |
---|
358 | pcs_exec :> fullexec io_out io_in; |
---|
359 | pcs_labelled : ∀g. state … pcs_exec g → bool; |
---|
360 | pcs_classify : ∀g. state … pcs_exec g → status_class; |
---|
361 | pcs_callee : ∀g,s. match pcs_classify g s with [ cl_call ⇒ True | _ ⇒ False ] → ident |
---|
362 | }. |
---|
363 | |
---|
364 | definition pcs_to_cs : ∀C:preclassified_system. global … C → classified_system ≝ |
---|
365 | λC,g. |
---|
366 | mk_classified_system (pcs_exec C) g (pcs_labelled C ?) (pcs_classify C ?) (pcs_callee C ?). |
---|
367 | |
---|
368 | (* FIXME: this definition is unreasonable because it presumes we can easily |
---|
369 | identify the change in stack usage from return states, but that information |
---|
370 | is rather implicit (we only really record the function called in the |
---|
371 | extended RTLabs states when building the structured traces). *) |
---|
372 | |
---|
373 | definition measurable : ∀C:preclassified_system. |
---|
374 | ∀p:program ?? C. nat → nat → |
---|
375 | (ident → nat) (* stack cost *) → |
---|
376 | nat → Prop ≝ |
---|
377 | λC,p,m,n,stack_cost,max_allowed_stack. ∃s0,prefix,s1,interesting,s2. |
---|
378 | let g ≝ make_global … (pcs_exec … C) p in |
---|
379 | let C' ≝ pcs_to_cs C g in |
---|
380 | make_initial_state … p = OK ? s0 ∧ |
---|
381 | exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧ |
---|
382 | exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧ |
---|
383 | trace_is_label_to_return C' interesting ∧ |
---|
384 | bool_to_Prop (will_return' C' interesting) ∧ |
---|
385 | le (max_stack stack_cost 0 (\snd (intensional_trace_of_trace C' [ ] (prefix@interesting)))) max_allowed_stack. |
---|
386 | |
---|
387 | (* TODO: probably ought to be elsewhere; use exec_steps instead |
---|
388 | |
---|
389 | Note that this does not include stack space |
---|
390 | *) |
---|
391 | |
---|
392 | definition observables : ∀C:preclassified_system. program ?? C → nat → nat → res ((list intensional_event) × (list intensional_event)) ≝ |
---|
393 | λC,p,m,n. |
---|
394 | let g ≝ make_global … (pcs_exec … C) p in |
---|
395 | let C' ≝ pcs_to_cs C g in |
---|
396 | ! s0 ← make_initial_state … p; |
---|
397 | ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0; |
---|
398 | ! 〈interesting,s2〉 ← exec_steps n ?? (cs_exec … C') g s1; |
---|
399 | let 〈cs,prefix'〉 ≝ intensional_trace_of_trace C' [ ] prefix in |
---|
400 | return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉. |
---|
401 | |
---|
402 | (* CSC: Main debug function for the extracted code. |
---|
403 | It returns the list of all observed states and their observables, |
---|
404 | the last state and the reason for stopping execution. If the last |
---|
405 | state is final, it also returns the exit value. *) |
---|
406 | let rec observe_all_in_measurable (n:nat) (fx:classified_system) |
---|
407 | (observe: intensional_event → unit) (callstack: list ident) |
---|
408 | (s:state … fx (cs_global fx)) : |
---|
409 | list intensional_event × (res int) ≝ |
---|
410 | match n with |
---|
411 | [ O ⇒ |
---|
412 | let res ≝ |
---|
413 | match is_final … fx (cs_global … fx) s with |
---|
414 | [ Some r ⇒ OK … r |
---|
415 | | None ⇒ Error … (msg NotTerminated) ] |
---|
416 | in |
---|
417 | 〈[ ],res〉 |
---|
418 | | S m ⇒ |
---|
419 | match is_final … fx (cs_global … fx) s with |
---|
420 | [ Some r ⇒ 〈[ ],OK … r〉 |
---|
421 | | None ⇒ |
---|
422 | match step … fx (cs_global … fx) s with |
---|
423 | [ Value trs ⇒ |
---|
424 | let costevents ≝ flatten ? (map … intensional_event_of_event (\fst trs)) in |
---|
425 | let 〈callstack,callevent〉 ≝ |
---|
426 | match cs_classify fx s |
---|
427 | return λy. (match y with [cl_call ⇒ True | _ ⇒ False] → ident) → |
---|
428 | list ident × (list intensional_event) |
---|
429 | with |
---|
430 | [ cl_call ⇒ |
---|
431 | λcallee. let id ≝ callee I in |
---|
432 | 〈id::callstack,[IEVcall id]〉 |
---|
433 | | cl_return ⇒ λ_. |
---|
434 | match callstack with |
---|
435 | [ nil ⇒ 〈[ ],[ ]〉 |
---|
436 | | cons id tl ⇒ 〈tl,[IEVret id]〉] |
---|
437 | | _ ⇒ λ_. 〈callstack, [ ]〉 |
---|
438 | ] (cs_callee fx s) in |
---|
439 | let events ≝ costevents@callevent in |
---|
440 | let dummy : list unit ≝ map ?? observe events in |
---|
441 | let 〈tl,res〉 ≝ |
---|
442 | observe_all_in_measurable m fx observe callstack (\snd trs) in |
---|
443 | 〈events@tl,res〉 |
---|
444 | | Interact _ _ ⇒ 〈[ ],Error … (msg UnexpectedIO)〉 |
---|
445 | | Wrong m ⇒ 〈[ ],Error … m〉 |
---|
446 | ] |
---|
447 | ] |
---|
448 | ]. |
---|