79 open Hints_declaration
101 open StructuredTraces
105 type classified_system = { cs_exec : (IO.io_out, IO.io_in)
106 SmallstepExec.fullexec; cs_global :
107 __; cs_labelled : (__ -> Bool.bool);
109 StructuredTraces.status_class);
110 cs_callee : (__ -> __ -> AST.ident) }
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 **)
116 let 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 } =
121 h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
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 **)
128 let 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 } =
133 h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
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 **)
140 let 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 } =
145 h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
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 **)
152 let 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 } =
157 h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
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 **)
164 let 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 } =
169 h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
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 **)
176 let 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 } =
181 h_mk_classified_system cs_exec0 cs_global0 cs_labelled0 cs_classify0
185 classified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
186 let rec cs_exec xxx =
189 (** val cs_global : classified_system -> __ **)
190 let rec cs_global xxx =
193 (** val cs_labelled : classified_system -> __ -> Bool.bool **)
194 let rec cs_labelled xxx =
197 (** val cs_classify :
198 classified_system -> __ -> StructuredTraces.status_class **)
199 let rec cs_classify xxx =
202 (** val cs_callee0 : classified_system -> __ -> AST.ident **)
203 let rec cs_callee0 xxx s =
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 **)
210 let classified_system_inv_rect_Type4 hterm h1 =
211 let hcut = classified_system_rect_Type4 h1 hterm in hcut __
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 **)
217 let classified_system_inv_rect_Type3 hterm h1 =
218 let hcut = classified_system_rect_Type3 h1 hterm in hcut __
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 **)
224 let classified_system_inv_rect_Type2 hterm h1 =
225 let hcut = classified_system_rect_Type2 h1 hterm in hcut __
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 **)
231 let classified_system_inv_rect_Type1 hterm h1 =
232 let hcut = classified_system_rect_Type1 h1 hterm in hcut __
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 **)
238 let classified_system_inv_rect_Type0 hterm h1 =
239 let hcut = classified_system_rect_Type0 h1 hterm in hcut __
241 (** val cs_exec__o__es1 :
242 classified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
243 let cs_exec__o__es1 x0 =
244 x0.cs_exec.SmallstepExec.es1
248 (** val intensional_event_of_event :
249 Events.event -> StructuredTraces.intensional_event List.list **)
250 let intensional_event_of_event = function
251 | Events.EVcost l -> List.Cons ((StructuredTraces.IEVcost l), List.Nil)
252 | Events.EVextcall (x, x0, x1) -> List.Nil
254 (** val intensional_events_of_events :
255 Events.trace -> StructuredTraces.intensional_event List.list **)
256 let intensional_events_of_events tr =
257 List.flatten (List.map intensional_event_of_event tr)
259 (** val intensional_state_change :
260 classified_system -> AST.ident List.list -> __ -> (AST.ident List.list,
261 StructuredTraces.intensional_event List.list) Types.prod **)
262 let intensional_state_change c callstack s =
263 (match c.cs_classify s with
264 | StructuredTraces.Cl_return ->
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
271 | StructuredTraces.Cl_jump ->
272 (fun x -> { Types.fst = callstack; Types.snd = List.Nil })
273 | StructuredTraces.Cl_call ->
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 _ ->
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 **)
288 let 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
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
299 { Types.fst = callstack1; Types.snd =
300 (List.append call_event (List.append other_events rem)) }
302 (** val normal_state : classified_system -> cs_state -> Bool.bool **)
303 let 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
311 (** val measure_stack :
312 (AST.ident -> Nat.nat Types.option) -> Stacksize.stacksize_info ->
313 StructuredTraces.intensional_event List.list -> Stacksize.stacksize_info **)
314 let measure_stack costs start ev =
315 Stacksize.update_stacksize_info costs start
316 (Stacksize.extract_call_ud_from_observables ev)
318 (** val will_return_aux :
319 classified_system -> Nat.nat -> (cs_state, Events.trace) Types.prod
320 List.list -> Bool.bool **)
321 let 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 ->
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)
338 (** val will_return' :
339 classified_system -> (cs_state, Events.trace) Types.prod List.list ->
342 will_return_aux c Nat.O
344 type 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) }
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 **)
355 let 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
359 h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
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 **)
365 let 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
369 h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
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 **)
375 let 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
379 h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
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 **)
385 let 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
389 h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
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 **)
395 let 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
399 h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
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 **)
405 let 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
409 h_mk_preclassified_system pcs_exec0 pcs_labelled0 pcs_classify0 pcs_callee0
412 preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
413 let rec pcs_exec xxx =
416 (** val pcs_labelled : preclassified_system -> __ -> __ -> Bool.bool **)
417 let rec pcs_labelled xxx =
420 (** val pcs_classify :
421 preclassified_system -> __ -> __ -> StructuredTraces.status_class **)
422 let rec pcs_classify xxx =
425 (** val pcs_callee0 : preclassified_system -> __ -> __ -> AST.ident **)
426 let rec pcs_callee0 xxx g s =
427 (xxx.pcs_callee) g s __
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 **)
433 let preclassified_system_inv_rect_Type4 hterm h1 =
434 let hcut = preclassified_system_rect_Type4 h1 hterm in hcut __
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 **)
440 let preclassified_system_inv_rect_Type3 hterm h1 =
441 let hcut = preclassified_system_rect_Type3 h1 hterm in hcut __
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 **)
447 let preclassified_system_inv_rect_Type2 hterm h1 =
448 let hcut = preclassified_system_rect_Type2 h1 hterm in hcut __
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 **)
454 let preclassified_system_inv_rect_Type1 hterm h1 =
455 let hcut = preclassified_system_rect_Type1 h1 hterm in hcut __
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 **)
461 let preclassified_system_inv_rect_Type0 hterm h1 =
462 let hcut = preclassified_system_rect_Type0 h1 hterm in hcut __
464 (** val pcs_exec__o__es1 :
465 preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
466 let pcs_exec__o__es1 x0 =
467 x0.pcs_exec.SmallstepExec.es1
469 (** val pcs_to_cs : preclassified_system -> __ -> classified_system **)
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 _ ->
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 **)
479 let 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
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))
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
494 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = prefix';
496 (intensional_trace_of_trace c' cs interesting).Types.snd }))))
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)
503 let rec observe_all_in_measurable n fx observe callstack s =
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
511 { Types.fst = List.Nil; Types.snd = res }
513 (match (cs_exec__o__es1 fx).SmallstepExec.is_final fx.cs_global s with
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 ->
521 List.flatten (List.map intensional_event_of_event trs.Types.fst)
523 let { Types.fst = callstack0; Types.snd = callevent } =
524 (match fx.cs_classify s with
525 | StructuredTraces.Cl_return ->
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 ->
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)
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
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) })