extracted/measurable.ml

   1 open Preamble
   2
   3 open IO
   4
   5 open CostLabel
   6
   7 open PositiveMap
   8
   9 open Deqsets
  10
  11 open Lists
  12
  13 open Identifiers
  14
  15 open AST
  16
  17 open Division
  18
  19 open Z
  20
  21 open BitVectorZ
  22
  23 open Pointers
  24
  25 open Coqlib
  26
  27 open Values
  28
  29 open Events
  30
  31 open Exp
  32
  33 open Arithmetic
  34
  35 open Vector
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Extranat
  42
  43 open Integers
  44
  45 open Proper
  46
  47 open ErrorMessages
  48
  49 open Option
  50
  51 open Setoids
  52
  53 open Monad
  54
  55 open Positive
  56
  57 open PreIdentifiers
  58
  59 open Errors
  60
  61 open IOMonad
  62
  63 open Div_and_mod
  64
  65 open Jmeq
  66
  67 open Russell
  68
  69 open Util
  70
  71 open Bool
  72
  73 open Relations
  74
  75 open Nat
  76
  77 open List
  78
  79 open Hints_declaration
  80
  81 open Core_notation
  82
  83 open Pts
  84
  85 open Logic
  86
  87 open Types
  88
  89 open Extralib
  90
  91 open SmallstepExec
  92
  93 open Executions
  94
  95 open Hide
  96
  97 open Sets
  98
  99 open Listb
 100
 101 open StructuredTraces
 102
 103 open Stacksize
 104
 105 type 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 **)
 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 } =
 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 **)
 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 } =
 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 **)
 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 } =
 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 **)
 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 } =
 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 **)
 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 } =
 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 **)
 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 } =
 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 **)
 186 let rec cs_exec xxx =
 187   xxx.cs_exec
 188
 189 (** val cs_global : classified_system -> __ **)
 190 let rec cs_global xxx =
 191   xxx.cs_global
 192
 193 (** val cs_labelled : classified_system -> __ -> Bool.bool **)
 194 let rec cs_labelled xxx =
 195   xxx.cs_labelled
 196
 197 (** val cs_classify :
 198     classified_system -> __ -> StructuredTraces.status_class **)
 199 let rec cs_classify xxx =
 200   xxx.cs_classify
 201
 202 (** val cs_callee0 : classified_system -> __ -> AST.ident **)
 203 let 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 **)
 210 let 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 **)
 217 let 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 **)
 224 let 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 **)
 231 let 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 **)
 238 let 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 **)
 243 let cs_exec__o__es1 x0 =
 244   x0.cs_exec.SmallstepExec.es1
 245
 246 type cs_state = __
 247
 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
 253
 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)
 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 **)
 262 let 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 **)
 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
 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 **)
 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
 310
 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)
 317
 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 ->
 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 **)
 341 let will_return' c =
 342   will_return_aux c Nat.O
 343
 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) }
 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 **)
 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
 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 **)
 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
 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 **)
 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
 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 **)
 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
 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 **)
 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
 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 **)
 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
 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 **)
 413 let rec pcs_exec xxx =
 414   xxx.pcs_exec
 415
 416 (** val pcs_labelled : preclassified_system -> __ -> __ -> Bool.bool **)
 417 let rec pcs_labelled xxx =
 418   xxx.pcs_labelled
 419
 420 (** val pcs_classify :
 421     preclassified_system -> __ -> __ -> StructuredTraces.status_class **)
 422 let rec pcs_classify xxx =
 423   xxx.pcs_classify
 424
 425 (** val pcs_callee0 : preclassified_system -> __ -> __ -> AST.ident **)
 426 let 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 **)
 433 let 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 **)
 440 let 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 **)
 447 let 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 **)
 454 let 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 **)
 461 let 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 **)
 466 let pcs_exec__o__es1 x0 =
 467   x0.pcs_exec.SmallstepExec.es1
 468
 469 (** val pcs_to_cs : preclassified_system -> __ -> classified_system **)
 470 let 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 **)
 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
 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 **)
 503 let 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