source: driver/extracted/measurable.ml @ 3106

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

New extraction

File size: 20.6 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
103open Stacksize
104
105type classified_system = { cs_exec : (IO.io_out, IO.io_in)
106                                     SmallstepExec.fullexec; cs_global : 
107                           __; cs_labelled : (__ -> Bool.bool);
108                           cs_classify : (__ ->
109                                         StructuredTraces.status_class);
110                           cs_callee : (__ -> __ -> AST.ident) }
111
112(** val classified_system_rect_Type4 :
113    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
114    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
115    'a1) -> classified_system -> 'a1 **)
116let rec classified_system_rect_Type4 h_mk_classified_system x_23662 =
117  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
118    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
119    x_23662
120  in
121  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
122    cs_callee0
123
124(** val classified_system_rect_Type5 :
125    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
126    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
127    'a1) -> classified_system -> 'a1 **)
128let rec classified_system_rect_Type5 h_mk_classified_system x_23664 =
129  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
130    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
131    x_23664
132  in
133  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
134    cs_callee0
135
136(** val classified_system_rect_Type3 :
137    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
138    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
139    'a1) -> classified_system -> 'a1 **)
140let rec classified_system_rect_Type3 h_mk_classified_system x_23666 =
141  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
142    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
143    x_23666
144  in
145  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
146    cs_callee0
147
148(** val classified_system_rect_Type2 :
149    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
150    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
151    'a1) -> classified_system -> 'a1 **)
152let rec classified_system_rect_Type2 h_mk_classified_system x_23668 =
153  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
154    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
155    x_23668
156  in
157  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
158    cs_callee0
159
160(** val classified_system_rect_Type1 :
161    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
162    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
163    'a1) -> classified_system -> 'a1 **)
164let rec classified_system_rect_Type1 h_mk_classified_system x_23670 =
165  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
166    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
167    x_23670
168  in
169  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
170    cs_callee0
171
172(** val classified_system_rect_Type0 :
173    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool)
174    -> (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) ->
175    'a1) -> classified_system -> 'a1 **)
176let rec classified_system_rect_Type0 h_mk_classified_system x_23672 =
177  let { cs_exec = cs_exec0; cs_global = cs_global0; cs_labelled =
178    cs_labelled0; cs_classify = cs_classify0; cs_callee = cs_callee0 } =
179    x_23672
180  in
181  h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
182    cs_callee0
183
184(** val cs_exec :
185    classified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
186let rec cs_exec xxx =
187  xxx.cs_exec
188
189(** val cs_global : classified_system -> __ **)
190let rec cs_global xxx =
191  xxx.cs_global
192
193(** val cs_labelled : classified_system -> __ -> Bool.bool **)
194let rec cs_labelled xxx =
195  xxx.cs_labelled
196
197(** val cs_classify :
198    classified_system -> __ -> StructuredTraces.status_class **)
199let rec cs_classify xxx =
200  xxx.cs_classify
201
202(** val cs_callee0 : classified_system -> __ -> AST.ident **)
203let rec cs_callee0 xxx s =
204  (xxx.cs_callee) s __
205
206(** val classified_system_inv_rect_Type4 :
207    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
208    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
209    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
210let classified_system_inv_rect_Type4 hterm h1 =
211  let hcut = classified_system_rect_Type4 h1 hterm in hcut __
212
213(** val classified_system_inv_rect_Type3 :
214    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
215    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
216    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
217let classified_system_inv_rect_Type3 hterm h1 =
218  let hcut = classified_system_rect_Type3 h1 hterm in hcut __
219
220(** val classified_system_inv_rect_Type2 :
221    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
222    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
223    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
224let classified_system_inv_rect_Type2 hterm h1 =
225  let hcut = classified_system_rect_Type2 h1 hterm in hcut __
226
227(** val classified_system_inv_rect_Type1 :
228    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
229    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
230    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
231let classified_system_inv_rect_Type1 hterm h1 =
232  let hcut = classified_system_rect_Type1 h1 hterm in hcut __
233
234(** val classified_system_inv_rect_Type0 :
235    classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __
236    -> (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ ->
237    __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
238let classified_system_inv_rect_Type0 hterm h1 =
239  let hcut = classified_system_rect_Type0 h1 hterm in hcut __
240
241(** val cs_exec__o__es1 :
242    classified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
243let cs_exec__o__es1 x0 =
244  x0.cs_exec.SmallstepExec.es1
245
246type cs_state = __
247
248(** val intensional_event_of_event :
249    Events.event -> StructuredTraces.intensional_event List.list **)
250let intensional_event_of_event = function
251| Events.EVcost l -> List.Cons ((StructuredTraces.IEVcost l), List.Nil)
252| Events.EVextcall (x, x0, x1) -> List.Nil
253
254(** val intensional_events_of_events :
255    Events.trace -> StructuredTraces.intensional_event List.list **)
256let intensional_events_of_events tr =
257  List.flatten (List.map intensional_event_of_event tr)
258
259(** val intensional_state_change :
260    classified_system -> AST.ident List.list -> __ -> (AST.ident List.list,
261    StructuredTraces.intensional_event List.list) Types.prod **)
262let intensional_state_change c callstack s =
263  (match c.cs_classify s with
264   | StructuredTraces.Cl_return ->
265     (fun x ->
266       match callstack with
267       | List.Nil -> { Types.fst = List.Nil; Types.snd = List.Nil }
268       | List.Cons (id, tl) ->
269         { Types.fst = tl; Types.snd = (List.Cons ((StructuredTraces.IEVret
270           id), List.Nil)) })
271   | StructuredTraces.Cl_jump ->
272     (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
273   | StructuredTraces.Cl_call ->
274     (fun callee ->
275       let id = callee __ in
276       { Types.fst = (List.Cons (id, callstack)); Types.snd = (List.Cons
277       ((StructuredTraces.IEVcall id), List.Nil)) })
278   | StructuredTraces.Cl_tailcall ->
279     (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
280   | StructuredTraces.Cl_other ->
281     (fun x -> { Types.fst = callstack; Types.snd = List.Nil })) (fun _ ->
282    cs_callee0 c s)
283
284(** val intensional_trace_of_trace :
285    classified_system -> AST.ident List.list -> (cs_state, Events.trace)
286    Types.prod List.list -> (AST.ident List.list,
287    StructuredTraces.intensional_event List.list) Types.prod **)
288let rec intensional_trace_of_trace c callstack = function
289| List.Nil -> { Types.fst = callstack; Types.snd = List.Nil }
290| List.Cons (str, tl) ->
291  let { Types.fst = s; Types.snd = tr } = str in
292  let { Types.fst = callstack0; Types.snd = call_event } =
293    intensional_state_change c callstack s
294  in
295  let other_events = intensional_events_of_events tr in
296  let { Types.fst = callstack1; Types.snd = rem } =
297    intensional_trace_of_trace c callstack0 tl
298  in
299  { Types.fst = callstack1; Types.snd =
300  (List.append call_event (List.append other_events rem)) }
301
302(** val normal_state : classified_system -> cs_state -> Bool.bool **)
303let normal_state c s =
304  match c.cs_classify s with
305  | StructuredTraces.Cl_return -> Bool.False
306  | StructuredTraces.Cl_jump -> Bool.True
307  | StructuredTraces.Cl_call -> Bool.False
308  | StructuredTraces.Cl_tailcall -> Bool.False
309  | StructuredTraces.Cl_other -> Bool.True
310
311(** val measure_stack :
312    (AST.ident -> Nat.nat Types.option) -> Stacksize.stacksize_info ->
313    StructuredTraces.intensional_event List.list -> Stacksize.stacksize_info **)
314let measure_stack costs start ev =
315  Stacksize.update_stacksize_info costs start
316    (Stacksize.extract_call_ud_from_observables ev)
317
318(** val will_return_aux :
319    classified_system -> Nat.nat -> (cs_state, Events.trace) Types.prod
320    List.list -> Bool.bool **)
321let rec will_return_aux c depth = function
322| List.Nil -> Bool.False
323| List.Cons (h, tl) ->
324  let { Types.fst = s; Types.snd = tr } = h in
325  (match c.cs_classify s with
326   | StructuredTraces.Cl_return ->
327     (match depth with
328      | Nat.O ->
329        (match tl with
330         | List.Nil -> Bool.True
331         | List.Cons (x, x0) -> Bool.False)
332      | Nat.S d -> will_return_aux c d tl)
333   | StructuredTraces.Cl_jump -> will_return_aux c depth tl
334   | StructuredTraces.Cl_call -> will_return_aux c (Nat.S depth) tl
335   | StructuredTraces.Cl_tailcall -> will_return_aux c depth tl
336   | StructuredTraces.Cl_other -> will_return_aux c depth tl)
337
338(** val will_return' :
339    classified_system -> (cs_state, Events.trace) Types.prod List.list ->
340    Bool.bool **)
341let will_return' c =
342  will_return_aux c Nat.O
343
344type preclassified_system = { pcs_exec : (IO.io_out, IO.io_in)
345                                         SmallstepExec.fullexec;
346                              pcs_labelled : (__ -> __ -> Bool.bool);
347                              pcs_classify : (__ -> __ ->
348                                             StructuredTraces.status_class);
349                              pcs_callee : (__ -> __ -> __ -> AST.ident) }
350
351(** val preclassified_system_rect_Type4 :
352    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
353    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
354    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
355let rec preclassified_system_rect_Type4 h_mk_preclassified_system x_23692 =
356  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
357    pcs_classify0; pcs_callee = pcs_callee0 } = x_23692
358  in
359  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
360
361(** val preclassified_system_rect_Type5 :
362    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
363    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
364    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
365let rec preclassified_system_rect_Type5 h_mk_preclassified_system x_23694 =
366  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
367    pcs_classify0; pcs_callee = pcs_callee0 } = x_23694
368  in
369  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
370
371(** val preclassified_system_rect_Type3 :
372    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
373    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
374    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
375let rec preclassified_system_rect_Type3 h_mk_preclassified_system x_23696 =
376  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
377    pcs_classify0; pcs_callee = pcs_callee0 } = x_23696
378  in
379  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
380
381(** val preclassified_system_rect_Type2 :
382    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
383    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
384    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
385let rec preclassified_system_rect_Type2 h_mk_preclassified_system x_23698 =
386  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
387    pcs_classify0; pcs_callee = pcs_callee0 } = x_23698
388  in
389  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
390
391(** val preclassified_system_rect_Type1 :
392    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
393    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
394    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
395let rec preclassified_system_rect_Type1 h_mk_preclassified_system x_23700 =
396  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
397    pcs_classify0; pcs_callee = pcs_callee0 } = x_23700
398  in
399  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
400
401(** val preclassified_system_rect_Type0 :
402    ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool)
403    -> (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
404    AST.ident) -> 'a1) -> preclassified_system -> 'a1 **)
405let rec preclassified_system_rect_Type0 h_mk_preclassified_system x_23702 =
406  let { pcs_exec = pcs_exec0; pcs_labelled = pcs_labelled0; pcs_classify =
407    pcs_classify0; pcs_callee = pcs_callee0 } = x_23702
408  in
409  h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
410
411(** val pcs_exec :
412    preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
413let rec pcs_exec xxx =
414  xxx.pcs_exec
415
416(** val pcs_labelled : preclassified_system -> __ -> __ -> Bool.bool **)
417let rec pcs_labelled xxx =
418  xxx.pcs_labelled
419
420(** val pcs_classify :
421    preclassified_system -> __ -> __ -> StructuredTraces.status_class **)
422let rec pcs_classify xxx =
423  xxx.pcs_classify
424
425(** val pcs_callee0 : preclassified_system -> __ -> __ -> AST.ident **)
426let rec pcs_callee0 xxx g s =
427  (xxx.pcs_callee) g s __
428
429(** val preclassified_system_inv_rect_Type4 :
430    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
431    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
432    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
433let preclassified_system_inv_rect_Type4 hterm h1 =
434  let hcut = preclassified_system_rect_Type4 h1 hterm in hcut __
435
436(** val preclassified_system_inv_rect_Type3 :
437    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
438    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
439    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
440let preclassified_system_inv_rect_Type3 hterm h1 =
441  let hcut = preclassified_system_rect_Type3 h1 hterm in hcut __
442
443(** val preclassified_system_inv_rect_Type2 :
444    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
445    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
446    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
447let preclassified_system_inv_rect_Type2 hterm h1 =
448  let hcut = preclassified_system_rect_Type2 h1 hterm in hcut __
449
450(** val preclassified_system_inv_rect_Type1 :
451    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
452    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
453    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
454let preclassified_system_inv_rect_Type1 hterm h1 =
455  let hcut = preclassified_system_rect_Type1 h1 hterm in hcut __
456
457(** val preclassified_system_inv_rect_Type0 :
458    preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
459    (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
460    (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1 **)
461let preclassified_system_inv_rect_Type0 hterm h1 =
462  let hcut = preclassified_system_rect_Type0 h1 hterm in hcut __
463
464(** val pcs_exec__o__es1 :
465    preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
466let pcs_exec__o__es1 x0 =
467  x0.pcs_exec.SmallstepExec.es1
468
469(** val pcs_to_cs : preclassified_system -> __ -> classified_system **)
470let pcs_to_cs c g =
471  { cs_exec = c.pcs_exec; cs_global = g; cs_labelled = (c.pcs_labelled g);
472    cs_classify = (c.pcs_classify g); cs_callee = (fun x _ ->
473    pcs_callee0 c g x) }
474
475(** val observables :
476    preclassified_system -> __ -> Nat.nat -> Nat.nat ->
477    (StructuredTraces.intensional_event List.list,
478    StructuredTraces.intensional_event List.list) Types.prod Errors.res **)
479let observables c p m n =
480  let g = c.pcs_exec.SmallstepExec.make_global p in
481  let c' = pcs_to_cs c g in
482  Obj.magic
483    (Monad.m_bind0 (Monad.max_def Errors.res0)
484      (Obj.magic (c.pcs_exec.SmallstepExec.make_initial_state p)) (fun s0 ->
485      Monad.m_bind2 (Monad.max_def Errors.res0)
486        (Obj.magic (SmallstepExec.exec_steps m c'.cs_exec g s0))
487        (fun prefix s1 ->
488        Monad.m_bind2 (Monad.max_def Errors.res0)
489          (Obj.magic (SmallstepExec.exec_steps n c'.cs_exec g s1))
490          (fun interesting s2 ->
491          let { Types.fst = cs; Types.snd = prefix' } =
492            intensional_trace_of_trace c' List.Nil prefix
493          in
494          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = prefix';
495            Types.snd =
496            (intensional_trace_of_trace c' cs interesting).Types.snd }))))
497
498(** val observe_all_in_measurable :
499    Nat.nat -> classified_system -> (StructuredTraces.intensional_event ->
500    Types.unit0) -> AST.ident List.list -> __ ->
501    (StructuredTraces.intensional_event List.list, Integers.int Errors.res)
502    Types.prod **)
503let rec observe_all_in_measurable n fx observe callstack s =
504  match n with
505  | Nat.O ->
506    let res =
507      match (cs_exec__o__es1 fx).SmallstepExec.is_final fx.cs_global s with
508      | Types.None -> Errors.Error (Errors.msg ErrorMessages.NotTerminated)
509      | Types.Some r -> Errors.OK r
510    in
511    { Types.fst = List.Nil; Types.snd = res }
512  | Nat.S m ->
513    (match (cs_exec__o__es1 fx).SmallstepExec.is_final fx.cs_global s with
514     | Types.None ->
515       (match (cs_exec__o__es1 fx).SmallstepExec.step fx.cs_global s with
516        | IOMonad.Interact (x, x0) ->
517          { Types.fst = List.Nil; Types.snd = (Errors.Error
518            (Errors.msg ErrorMessages.UnexpectedIO)) }
519        | IOMonad.Value trs ->
520          let costevents =
521            List.flatten (List.map intensional_event_of_event trs.Types.fst)
522          in
523          let { Types.fst = callstack0; Types.snd = callevent } =
524            (match fx.cs_classify s with
525             | StructuredTraces.Cl_return ->
526               (fun x ->
527                 match callstack with
528                 | List.Nil -> { Types.fst = List.Nil; Types.snd = List.Nil }
529                 | List.Cons (id, tl) ->
530                   { Types.fst = tl; Types.snd = (List.Cons
531                     ((StructuredTraces.IEVret id), List.Nil)) })
532             | StructuredTraces.Cl_jump ->
533               (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
534             | StructuredTraces.Cl_call ->
535               (fun callee ->
536                 let id = callee __ in
537                 { Types.fst = (List.Cons (id, callstack)); Types.snd =
538                 (List.Cons ((StructuredTraces.IEVcall id), List.Nil)) })
539             | StructuredTraces.Cl_tailcall ->
540               (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
541             | StructuredTraces.Cl_other ->
542               (fun x -> { Types.fst = callstack; Types.snd = List.Nil }))
543              (fun _ -> cs_callee0 fx s)
544          in
545          let events = List.append costevents callevent in
546          let dummy = List.map observe events in
547          let { Types.fst = tl; Types.snd = res } =
548            observe_all_in_measurable m fx observe callstack0 trs.Types.snd
549          in
550          { Types.fst = (List.append events tl); Types.snd = res }
551        | IOMonad.Wrong m0 ->
552          { Types.fst = List.Nil; Types.snd = (Errors.Error m0) })
553     | Types.Some r -> { Types.fst = List.Nil; Types.snd = (Errors.OK r) })
554
Note: See TracBrowser for help on using the repository browser.