source: extracted/measurable.ml @ 2890

Last change on this file since 2890 was 2890, checked in by sacerdot, 7 years ago

Exported again, now the execution is correct up to LIN for a simple program.

File size: 21.0 KB
Line 
1open Preamble
2
3open IO
4
5open CostLabel
6
7open PositiveMap
8
9open Deqsets
10
11open Lists
12
13open Identifiers
14
15open AST
16
17open Division
18
19open Z
20
21open BitVectorZ
22
23open Pointers
24
25open Coqlib
26
27open Values
28
29open Events
30
31open Exp
32
33open Arithmetic
34
35open Vector
36
37open FoldStuff
38
39open BitVector
40
41open Extranat
42
43open Integers
44
45open Proper
46
47open ErrorMessages
48
49open Option
50
51open Setoids
52
53open Monad
54
55open Positive
56
57open PreIdentifiers
58
59open Errors
60
61open IOMonad
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open Util
70
71open Bool
72
73open Relations
74
75open Nat
76
77open List
78
79open Hints_declaration
80
81open Core_notation
82
83open Pts
84
85open Logic
86
87open Types
88
89open Extralib
90
91open SmallstepExec
92
93open Executions
94
95open Hide
96
97open Sets
98
99open Listb
100
101open StructuredTraces
102
103type classified_system = { cs_exec : (IO.io_out, IO.io_in)
104                                     SmallstepExec.fullexec; cs_global : 
105                           __; cs_labelled : (__ -> Bool.bool);
106                           cs_classify : (__ ->
107                                         StructuredTraces.status_class);
108                           cs_callee : (__ -> __ -> AST.ident) }
109
110(** val classified_system_rect_Type4 :
111    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
112    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
113    'a1) -> classified_system -> 'a1 **)
114let rec classified_system_rect_Type4 h_mk_classified_system x_25416 =
115  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
116    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
117    x_25416
118  in
119  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
120    cs_callee0
121
122(** val classified_system_rect_Type5 :
123    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
124    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
125    'a1) -> classified_system -> 'a1 **)
126let rec classified_system_rect_Type5 h_mk_classified_system x_25418 =
127  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
128    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
129    x_25418
130  in
131  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
132    cs_callee0
133
134(** val classified_system_rect_Type3 :
135    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
136    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
137    'a1) -> classified_system -> 'a1 **)
138let rec classified_system_rect_Type3 h_mk_classified_system x_25420 =
139  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
140    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
141    x_25420
142  in
143  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
144    cs_callee0
145
146(** val classified_system_rect_Type2 :
147    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
148    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
149    'a1) -> classified_system -> 'a1 **)
150let rec classified_system_rect_Type2 h_mk_classified_system x_25422 =
151  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
152    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
153    x_25422
154  in
155  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
156    cs_callee0
157
158(** val classified_system_rect_Type1 :
159    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
160    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
161    'a1) -> classified_system -> 'a1 **)
162let rec classified_system_rect_Type1 h_mk_classified_system x_25424 =
163  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
164    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
165    x_25424
166  in
167  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
168    cs_callee0
169
170(** val classified_system_rect_Type0 :
171    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
172    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
173    'a1) -> classified_system -> 'a1 **)
174let rec classified_system_rect_Type0 h_mk_classified_system x_25426 =
175  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
176    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
177    x_25426
178  in
179  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
180    cs_callee0
181
182(** val cs_exec :
183    classified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
184let rec cs_exec xxx =
185  xxx.cs_exec
186
187(** val cs_global : classified_system -> __ **)
188let rec cs_global xxx =
189  xxx.cs_global
190
191(** val cs_labelled : classified_system -> __ -> Bool.bool **)
192let rec cs_labelled xxx =
193  xxx.cs_labelled
194
195(** val cs_classify :
196    classified_system -> __ -> StructuredTraces.status_class **)
197let rec cs_classify xxx =
198  xxx.cs_classify
199
200(** val cs_callee0 : classified_system -> __ -> AST.ident **)
201let rec cs_callee0 xxx s =
202  (xxx.cs_callee) s __
203
204(** val classified_system_inv_rect_Type4 :
205    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
206    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
207    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
208let classified_system_inv_rect_Type4 hterm h1 =
209  let hcut = classified_system_rect_Type4 h1 hterm in hcut __
210
211(** val classified_system_inv_rect_Type3 :
212    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
213    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
214    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
215let classified_system_inv_rect_Type3 hterm h1 =
216  let hcut = classified_system_rect_Type3 h1 hterm in hcut __
217
218(** val classified_system_inv_rect_Type2 :
219    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
220    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
221    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
222let classified_system_inv_rect_Type2 hterm h1 =
223  let hcut = classified_system_rect_Type2 h1 hterm in hcut __
224
225(** val classified_system_inv_rect_Type1 :
226    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
227    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
228    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
229let classified_system_inv_rect_Type1 hterm h1 =
230  let hcut = classified_system_rect_Type1 h1 hterm in hcut __
231
232(** val classified_system_inv_rect_Type0 :
233    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
234    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
235    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
236let classified_system_inv_rect_Type0 hterm h1 =
237  let hcut = classified_system_rect_Type0 h1 hterm in hcut __
238
239(** val cs_exec__o__es1 :
240    classified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
241let cs_exec__o__es1 x0 =
242  x0.cs_exec.SmallstepExec.es1
243
244type cs_state = __
245
246(** val intensional_event_of_event :
247    Events.event -> StructuredTraces.intensional_event List.list **)
248let intensional_event_of_event = function
249| Events.EVcost l -> List.Cons ((StructuredTraces.IEVcost l), List.Nil)
250| Events.EVextcall (x, x0, x1) -> List.Nil
251
252(** val intensional_events_of_events :
253    Events.trace -> StructuredTraces.intensional_event List.list **)
254let intensional_events_of_events tr =
255  List.flatten (List.map intensional_event_of_event tr)
256
257(** val intensional_trace_of_trace :
258    classified_system -> AST.ident List.list -> (cs_state, Events.trace)
259    Types.prod List.list -> (AST.ident List.list,
260    StructuredTraces.intensional_event List.list) Types.prod **)
261let rec intensional_trace_of_trace c callstack = function
262| List.Nil -> { Types.fst = callstack; Types.snd = List.Nil }
263| List.Cons (str, tl) ->
264  let { Types.fst = s; Types.snd = tr } = str in
265  let { Types.fst = callstack0; Types.snd = call_event } =
266    (match c.cs_classify s with
267     | StructuredTraces.Cl_return ->
268       (fun x ->
269         match callstack with
270         | List.Nil -> { Types.fst = List.Nil; Types.snd = List.Nil }
271         | List.Cons (id, tl0) ->
272           { Types.fst = tl0; Types.snd = (List.Cons
273             ((StructuredTraces.IEVret id), List.Nil)) })
274     | StructuredTraces.Cl_jump ->
275       (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
276     | StructuredTraces.Cl_call ->
277       (fun callee ->
278         let id = callee __ in
279         { Types.fst = (List.Cons (id, callstack)); Types.snd = (List.Cons
280         ((StructuredTraces.IEVcall id), List.Nil)) })
281     | StructuredTraces.Cl_tailcall ->
282       (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
283     | StructuredTraces.Cl_other ->
284       (fun x -> { Types.fst = callstack; Types.snd = List.Nil })) (fun _ ->
285      cs_callee0 c s)
286  in
287  let other_events = intensional_events_of_events tr in
288  let { Types.fst = callstack1; Types.snd = rem } =
289    intensional_trace_of_trace c callstack0 tl
290  in
291  { Types.fst = callstack1; Types.snd =
292  (List.append call_event (List.append other_events rem)) }
293
294(** val normal_state : classified_system -> cs_state -> Bool.bool **)
295let normal_state c s =
296  match c.cs_classify s with
297  | StructuredTraces.Cl_return -> Bool.False
298  | StructuredTraces.Cl_jump -> Bool.True
299  | StructuredTraces.Cl_call -> Bool.False
300  | StructuredTraces.Cl_tailcall -> Bool.False
301  | StructuredTraces.Cl_other -> Bool.True
302
303(** val measure_stack :
304    (AST.ident -> Nat.nat) -> Nat.nat -> StructuredTraces.intensional_event
305    List.list -> (Nat.nat, Nat.nat) Types.prod **)
306let measure_stack costs start =
307  Util.foldl (fun x ev ->
308    match ev with
309    | StructuredTraces.IEVcost x0 -> x
310    | StructuredTraces.IEVcall id ->
311      let { Types.fst = current_stack; Types.snd = max_stack } = x in
312      let new_stack = Nat.plus current_stack (costs id) in
313      { Types.fst = new_stack; Types.snd = (Nat.max new_stack max_stack) }
314    | StructuredTraces.IEVtailcall (x0, x1) -> x
315    | StructuredTraces.IEVret id ->
316      let { Types.fst = current_stack; Types.snd = max_stack } = x in
317      { Types.fst = (Nat.minus current_stack (costs id)); Types.snd =
318      max_stack }) { Types.fst = start; Types.snd = start }
319
320(** val max_stack :
321    (AST.ident -> Nat.nat) -> Nat.nat -> StructuredTraces.intensional_event
322    List.list -> Nat.nat **)
323let max_stack costs start trace =
324  (measure_stack costs start trace).Types.snd
325
326(** val will_return_aux :
327    classified_system -> Nat.nat -> (cs_state, Events.trace) Types.prod
328    List.list -> Bool.bool **)
329let rec will_return_aux c depth = function
330| List.Nil -> Bool.False
331| List.Cons (h, tl) ->
332  let { Types.fst = s; Types.snd = tr } = h in
333  (match c.cs_classify s with
334   | StructuredTraces.Cl_return ->
335     (match depth with
336      | Nat.O ->
337        (match tl with
338         | List.Nil -> Bool.True
339         | List.Cons (x, x0) -> Bool.False)
340      | Nat.S d -> will_return_aux c d tl)
341   | StructuredTraces.Cl_jump -> will_return_aux c depth tl
342   | StructuredTraces.Cl_call -> will_return_aux c (Nat.S depth) tl
343   | StructuredTraces.Cl_tailcall -> will_return_aux c depth tl
344   | StructuredTraces.Cl_other -> will_return_aux c depth tl)
345
346(** val will_return' :
347    classified_system -> (cs_state, Events.trace) Types.prod List.list ->
348    Bool.bool **)
349let will_return' c =
350  will_return_aux c Nat.O
351
352type preclassified_system = { pcs_exec : (IO.io_out, IO.io_in)
353                                         SmallstepExec.fullexec;
354                              pcs_labelled : (__ -> __ -> Bool.bool);
355                              pcs_classify : (__ -> __ ->
356                                             StructuredTraces.status_class);
357                              pcs_callee : (__ -> __ -> __ -> AST.ident) }
358
359(** val preclassified_system_rect_Type4 :
360    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
361    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
362    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
363let rec preclassified_system_rect_Type4 h_mk_preclassified_system x_25446 =
364  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
365    pcs_classify0; pcs_callee = pcs_callee0 } = x_25446
366  in
367  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
368
369(** val preclassified_system_rect_Type5 :
370    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
371    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
372    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
373let rec preclassified_system_rect_Type5 h_mk_preclassified_system x_25448 =
374  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
375    pcs_classify0; pcs_callee = pcs_callee0 } = x_25448
376  in
377  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
378
379(** val preclassified_system_rect_Type3 :
380    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
381    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
382    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
383let rec preclassified_system_rect_Type3 h_mk_preclassified_system x_25450 =
384  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
385    pcs_classify0; pcs_callee = pcs_callee0 } = x_25450
386  in
387  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
388
389(** val preclassified_system_rect_Type2 :
390    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
391    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
392    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
393let rec preclassified_system_rect_Type2 h_mk_preclassified_system x_25452 =
394  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
395    pcs_classify0; pcs_callee = pcs_callee0 } = x_25452
396  in
397  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
398
399(** val preclassified_system_rect_Type1 :
400    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
401    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
402    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
403let rec preclassified_system_rect_Type1 h_mk_preclassified_system x_25454 =
404  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
405    pcs_classify0; pcs_callee = pcs_callee0 } = x_25454
406  in
407  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
408
409(** val preclassified_system_rect_Type0 :
410    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
411    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
412    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
413let rec preclassified_system_rect_Type0 h_mk_preclassified_system x_25456 =
414  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
415    pcs_classify0; pcs_callee = pcs_callee0 } = x_25456
416  in
417  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
418
419(** val pcs_exec :
420    preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
421let rec pcs_exec xxx =
422  xxx.pcs_exec
423
424(** val pcs_labelled : preclassified_system -> __ -> __ -> Bool.bool **)
425let rec pcs_labelled xxx =
426  xxx.pcs_labelled
427
428(** val pcs_classify :
429    preclassified_system -> __ -> __ -> StructuredTraces.status_class **)
430let rec pcs_classify xxx =
431  xxx.pcs_classify
432
433(** val pcs_callee0 : preclassified_system -> __ -> __ -> AST.ident **)
434let rec pcs_callee0 xxx g s =
435  (xxx.pcs_callee) g s __
436
437(** val preclassified_system_inv_rect_Type4 :
438    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
439    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
440    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
441let preclassified_system_inv_rect_Type4 hterm h1 =
442  let hcut = preclassified_system_rect_Type4 h1 hterm in hcut __
443
444(** val preclassified_system_inv_rect_Type3 :
445    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
446    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
447    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
448let preclassified_system_inv_rect_Type3 hterm h1 =
449  let hcut = preclassified_system_rect_Type3 h1 hterm in hcut __
450
451(** val preclassified_system_inv_rect_Type2 :
452    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
453    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
454    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
455let preclassified_system_inv_rect_Type2 hterm h1 =
456  let hcut = preclassified_system_rect_Type2 h1 hterm in hcut __
457
458(** val preclassified_system_inv_rect_Type1 :
459    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
460    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
461    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
462let preclassified_system_inv_rect_Type1 hterm h1 =
463  let hcut = preclassified_system_rect_Type1 h1 hterm in hcut __
464
465(** val preclassified_system_inv_rect_Type0 :
466    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
467    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
468    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
469let preclassified_system_inv_rect_Type0 hterm h1 =
470  let hcut = preclassified_system_rect_Type0 h1 hterm in hcut __
471
472(** val pcs_exec__o__es1 :
473    preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
474let pcs_exec__o__es1 x0 =
475  x0.pcs_exec.SmallstepExec.es1
476
477(** val pcs_to_cs : preclassified_system -> __ -> classified_system **)
478let pcs_to_cs c g =
479  { cs_exec = c.pcs_exec; cs_global = g; cs_labelled = (c.pcs_labelled g);
480    cs_classify = (c.pcs_classify g); cs_callee = (fun x _ ->
481    pcs_callee0 c g x) }
482
483(** val observables :
484    preclassified_system -> __ -> Nat.nat -> Nat.nat ->
485    (StructuredTraces.intensional_event List.list,
486    StructuredTraces.intensional_event List.list) Types.prod Errors.res **)
487let observables c p m n =
488  let g = c.pcs_exec.SmallstepExec.make_global p in
489  let c' = pcs_to_cs c g in
490  Obj.magic
491    (Monad.m_bind0 (Monad.max_def Errors.res0)
492      (Obj.magic (c.pcs_exec.SmallstepExec.make_initial_state p)) (fun s0 ->
493      Monad.m_bind2 (Monad.max_def Errors.res0)
494        (Obj.magic (SmallstepExec.exec_steps m c'.cs_exec g s0))
495        (fun prefix s1 ->
496        Monad.m_bind2 (Monad.max_def Errors.res0)
497          (Obj.magic (SmallstepExec.exec_steps n c'.cs_exec g s1))
498          (fun interesting s2 ->
499          let { Types.fst = cs; Types.snd = prefix' } =
500            intensional_trace_of_trace c' List.Nil prefix
501          in
502          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = prefix';
503            Types.snd =
504            (intensional_trace_of_trace c' cs interesting).Types.snd }))))
505
506(** val observe_all_in_measurable :
507    Nat.nat -> classified_system -> (StructuredTraces.intensional_event ->
508    Types.unit0) -> AST.ident List.list -> __ ->
509    (StructuredTraces.intensional_event List.list, Integers.int Errors.res)
510    Types.prod **)
511let rec observe_all_in_measurable n fx observe callstack s =
512  match n with
513  | Nat.O ->
514    let res =
515      match (cs_exec__o__es1 fx).SmallstepExec.is_final fx.cs_global s with
516      | Types.None -> Errors.Error (Errors.msg ErrorMessages.NotTerminated)
517      | Types.Some r -> Errors.OK r
518    in
519    { Types.fst = List.Nil; Types.snd = res }
520  | Nat.S m ->
521    (match (cs_exec__o__es1 fx).SmallstepExec.is_final fx.cs_global s with
522     | Types.None ->
523       (match (cs_exec__o__es1 fx).SmallstepExec.step fx.cs_global s with
524        | IOMonad.Interact (x, x0) ->
525          { Types.fst = List.Nil; Types.snd = (Errors.Error
526            (Errors.msg ErrorMessages.UnexpectedIO)) }
527        | IOMonad.Value trs ->
528          let costevents =
529            List.flatten (List.map intensional_event_of_event trs.Types.fst)
530          in
531          let { Types.fst = callstack0; Types.snd = callevent } =
532            (match fx.cs_classify s with
533             | StructuredTraces.Cl_return ->
534               (fun x ->
535                 match callstack with
536                 | List.Nil -> { Types.fst = List.Nil; Types.snd = List.Nil }
537                 | List.Cons (id, tl) ->
538                   { Types.fst = tl; Types.snd = (List.Cons
539                     ((StructuredTraces.IEVret id), List.Nil)) })
540             | StructuredTraces.Cl_jump ->
541               (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
542             | StructuredTraces.Cl_call ->
543               (fun callee ->
544                 let id = callee __ in
545                 { Types.fst = (List.Cons (id, callstack)); Types.snd =
546                 (List.Cons ((StructuredTraces.IEVcall id), List.Nil)) })
547             | StructuredTraces.Cl_tailcall ->
548               (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
549             | StructuredTraces.Cl_other ->
550               (fun x -> { Types.fst = callstack; Types.snd = List.Nil }))
551              (fun _ -> cs_callee0 fx s)
552          in
553          let events = List.append costevents callevent in
554          let dummy = List.map observe events in
555          let { Types.fst = tl; Types.snd = res } =
556            observe_all_in_measurable m fx observe callstack0 trs.Types.snd
557          in
558          { Types.fst = (List.append events tl); Types.snd = res }
559        | IOMonad.Wrong m0 ->
560          { Types.fst = List.Nil; Types.snd = (Errors.Error m0) })
561     | Types.Some r -> { Types.fst = List.Nil; Types.snd = (Errors.OK r) })
562
Note: See TracBrowser for help on using the repository browser.