extracted/rTLabs_abstract.ml

   1 open Preamble
   2
   3 open BitVectorTrie
   4
   5 open Graphs
   6
   7 open Order
   8
   9 open Registers
  10
  11 open FrontEndOps
  12
  13 open RTLabs_syntax
  14
  15 open SmallstepExec
  16
  17 open CostLabel
  18
  19 open Events
  20
  21 open IOMonad
  22
  23 open IO
  24
  25 open Extra_bool
  26
  27 open Coqlib
  28
  29 open Values
  30
  31 open FrontEndVal
  32
  33 open Hide
  34
  35 open ByteValues
  36
  37 open Division
  38
  39 open Z
  40
  41 open BitVectorZ
  42
  43 open Pointers
  44
  45 open GenMem
  46
  47 open FrontEndMem
  48
  49 open Proper
  50
  51 open PositiveMap
  52
  53 open Deqsets
  54
  55 open Extralib
  56
  57 open Lists
  58
  59 open Identifiers
  60
  61 open Exp
  62
  63 open Arithmetic
  64
  65 open Vector
  66
  67 open Div_and_mod
  68
  69 open Util
  70
  71 open FoldStuff
  72
  73 open BitVector
  74
  75 open Extranat
  76
  77 open Integers
  78
  79 open AST
  80
  81 open Globalenvs
  82
  83 open ErrorMessages
  84
  85 open Option
  86
  87 open Setoids
  88
  89 open Monad
  90
  91 open Jmeq
  92
  93 open Russell
  94
  95 open Positive
  96
  97 open PreIdentifiers
  98
  99 open Errors
 100
 101 open Bool
 102
 103 open Relations
 104
 105 open Nat
 106
 107 open Hints_declaration
 108
 109 open Core_notation
 110
 111 open Pts
 112
 113 open Logic
 114
 115 open Types
 116
 117 open List
 118
 119 open RTLabs_semantics
 120
 121 type rTLabs_state = RTLabs_semantics.state
 122
 123 type rTLabs_genv = RTLabs_semantics.genv
 124
 125 open Sets
 126
 127 open Listb
 128
 129 open StructuredTraces
 130
 131 open CostSpec
 132
 133 open Deqsets_extra
 134
 135 (** val status_class_jmdiscr :
 136     StructuredTraces.status_class -> StructuredTraces.status_class -> __ **)
 137 let status_class_jmdiscr x y =
 138   Logic.eq_rect_Type2 x
 139     (match x with
 140      | StructuredTraces.Cl_return -> Obj.magic (fun _ dH -> dH)
 141      | StructuredTraces.Cl_jump -> Obj.magic (fun _ dH -> dH)
 142      | StructuredTraces.Cl_call -> Obj.magic (fun _ dH -> dH)
 143      | StructuredTraces.Cl_tailcall -> Obj.magic (fun _ dH -> dH)
 144      | StructuredTraces.Cl_other -> Obj.magic (fun _ dH -> dH)) y
 145
 146 type rTLabs_ext_state = { ras_state : RTLabs_semantics.state;
 147                           ras_fn_stack : Pointers.block List.list }
 148
 149 (** val rTLabs_ext_state_rect_Type4 :
 150     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
 151     List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
 152 let rec rTLabs_ext_state_rect_Type4 ge h_mk_RTLabs_ext_state x_24320 =
 153   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24320 in
 154   h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
 155
 156 (** val rTLabs_ext_state_rect_Type5 :
 157     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
 158     List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
 159 let rec rTLabs_ext_state_rect_Type5 ge h_mk_RTLabs_ext_state x_24322 =
 160   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24322 in
 161   h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
 162
 163 (** val rTLabs_ext_state_rect_Type3 :
 164     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
 165     List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
 166 let rec rTLabs_ext_state_rect_Type3 ge h_mk_RTLabs_ext_state x_24324 =
 167   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24324 in
 168   h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
 169
 170 (** val rTLabs_ext_state_rect_Type2 :
 171     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
 172     List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
 173 let rec rTLabs_ext_state_rect_Type2 ge h_mk_RTLabs_ext_state x_24326 =
 174   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24326 in
 175   h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
 176
 177 (** val rTLabs_ext_state_rect_Type1 :
 178     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
 179     List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
 180 let rec rTLabs_ext_state_rect_Type1 ge h_mk_RTLabs_ext_state x_24328 =
 181   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24328 in
 182   h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
 183
 184 (** val rTLabs_ext_state_rect_Type0 :
 185     RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
 186     List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
 187 let rec rTLabs_ext_state_rect_Type0 ge h_mk_RTLabs_ext_state x_24330 =
 188   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24330 in
 189   h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
 190
 191 (** val ras_state :
 192     RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state **)
 193 let rec ras_state ge xxx =
 194   xxx.ras_state
 195
 196 (** val ras_fn_stack :
 197     RTLabs_semantics.genv -> rTLabs_ext_state -> Pointers.block List.list **)
 198 let rec ras_fn_stack ge xxx =
 199   xxx.ras_fn_stack
 200
 201 (** val rTLabs_ext_state_inv_rect_Type4 :
 202     RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
 203     Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
 204 let rTLabs_ext_state_inv_rect_Type4 x1 hterm h1 =
 205   let hcut = rTLabs_ext_state_rect_Type4 x1 h1 hterm in hcut __
 206
 207 (** val rTLabs_ext_state_inv_rect_Type3 :
 208     RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
 209     Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
 210 let rTLabs_ext_state_inv_rect_Type3 x1 hterm h1 =
 211   let hcut = rTLabs_ext_state_rect_Type3 x1 h1 hterm in hcut __
 212
 213 (** val rTLabs_ext_state_inv_rect_Type2 :
 214     RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
 215     Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
 216 let rTLabs_ext_state_inv_rect_Type2 x1 hterm h1 =
 217   let hcut = rTLabs_ext_state_rect_Type2 x1 h1 hterm in hcut __
 218
 219 (** val rTLabs_ext_state_inv_rect_Type1 :
 220     RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
 221     Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
 222 let rTLabs_ext_state_inv_rect_Type1 x1 hterm h1 =
 223   let hcut = rTLabs_ext_state_rect_Type1 x1 h1 hterm in hcut __
 224
 225 (** val rTLabs_ext_state_inv_rect_Type0 :
 226     RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
 227     Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
 228 let rTLabs_ext_state_inv_rect_Type0 x1 hterm h1 =
 229   let hcut = rTLabs_ext_state_rect_Type0 x1 h1 hterm in hcut __
 230
 231 (** val rTLabs_ext_state_discr :
 232     RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __ **)
 233 let rTLabs_ext_state_discr a1 x y =
 234   Logic.eq_rect_Type2 x
 235     (let { ras_state = a0; ras_fn_stack = a10 } = x in
 236     Obj.magic (fun _ dH -> dH __ __ __)) y
 237
 238 (** val rTLabs_ext_state_jmdiscr :
 239     RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __ **)
 240 let rTLabs_ext_state_jmdiscr a1 x y =
 241   Logic.eq_rect_Type2 x
 242     (let { ras_state = a0; ras_fn_stack = a10 } = x in
 243     Obj.magic (fun _ dH -> dH __ __ __)) y
 244
 245 (** val dpi1__o__Ras_state__o__inject :
 246     RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
 247     RTLabs_semantics.state Types.sig0 **)
 248 let dpi1__o__Ras_state__o__inject x1 x3 =
 249   x3.Types.dpi1.ras_state
 250
 251 (** val eject__o__Ras_state__o__inject :
 252     RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
 253     RTLabs_semantics.state Types.sig0 **)
 254 let eject__o__Ras_state__o__inject x1 x3 =
 255   (Types.pi1 x3).ras_state
 256
 257 (** val ras_state__o__inject :
 258     RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state
 259     Types.sig0 **)
 260 let ras_state__o__inject x1 x2 =
 261   x2.ras_state
 262
 263 (** val dpi1__o__Ras_state :
 264     RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
 265     RTLabs_semantics.state **)
 266 let dpi1__o__Ras_state x0 x2 =
 267   x2.Types.dpi1.ras_state
 268
 269 (** val eject__o__Ras_state :
 270     RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
 271     RTLabs_semantics.state **)
 272 let eject__o__Ras_state x0 x2 =
 273   (Types.pi1 x2).ras_state
 274
 275 (** val next_state :
 276     RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state ->
 277     Events.trace -> rTLabs_ext_state **)
 278 let next_state ge s s' t =
 279   { ras_state = s'; ras_fn_stack =
 280     ((match s' with
 281       | RTLabs_semantics.State (x, x0, x1) -> (fun _ -> s.ras_fn_stack)
 282       | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) ->
 283         (fun _ -> List.Cons
 284           ((Types.pi1
 285              (RTLabs_semantics.func_block_of_exec ge s.ras_state t x x0 x1 x2
 286                x3 x4)), s.ras_fn_stack))
 287       | RTLabs_semantics.Returnstate (x, x0, x1, x2) ->
 288         (fun _ -> List.tail s.ras_fn_stack)
 289       | RTLabs_semantics.Finalstate x -> (fun _ -> List.Nil)) __) }
 290
 291 (** val rTLabs_classify :
 292     RTLabs_semantics.state -> StructuredTraces.status_class **)
 293 let rTLabs_classify = function
 294 | RTLabs_semantics.State (f, x, x0) ->
 295   (match RTLabs_semantics.next_instruction f with
 296    | RTLabs_syntax.St_skip x1 -> StructuredTraces.Cl_other
 297    | RTLabs_syntax.St_cost (x1, x2) -> StructuredTraces.Cl_other
 298    | RTLabs_syntax.St_const (x1, x2, x3, x4) -> StructuredTraces.Cl_other
 299    | RTLabs_syntax.St_op1 (x1, x2, x3, x4, x5, x6) ->
 300      StructuredTraces.Cl_other
 301    | RTLabs_syntax.St_op2 (x1, x2, x3, x4, x5, x6, x7, x8) ->
 302      StructuredTraces.Cl_other
 303    | RTLabs_syntax.St_load (x1, x2, x3, x4) -> StructuredTraces.Cl_other
 304    | RTLabs_syntax.St_store (x1, x2, x3, x4) -> StructuredTraces.Cl_other
 305    | RTLabs_syntax.St_call_id (x1, x2, x3, x4) -> StructuredTraces.Cl_other
 306    | RTLabs_syntax.St_call_ptr (x1, x2, x3, x4) -> StructuredTraces.Cl_other
 307    | RTLabs_syntax.St_cond (x1, x2, x3) -> StructuredTraces.Cl_jump
 308    | RTLabs_syntax.St_return -> StructuredTraces.Cl_other)
 309 | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) ->
 310   StructuredTraces.Cl_call
 311 | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> StructuredTraces.Cl_return
 312 | RTLabs_semantics.Finalstate x -> StructuredTraces.Cl_other
 313
 314 (** val rTLabs_cost : RTLabs_semantics.state -> Bool.bool **)
 315 let rTLabs_cost = function
 316 | RTLabs_semantics.State (f, fs, m) ->
 317   CostSpec.is_cost_label (RTLabs_semantics.next_instruction f)
 318 | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) -> Bool.False
 319 | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Bool.False
 320 | RTLabs_semantics.Finalstate x -> Bool.False
 321
 322 (** val rTLabs_cost_label :
 323     RTLabs_semantics.state -> CostLabel.costlabel Types.option **)
 324 let rTLabs_cost_label = function
 325 | RTLabs_semantics.State (f, fs, m) ->
 326   CostSpec.cost_label_of (RTLabs_semantics.next_instruction f)
 327 | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) -> Types.None
 328 | RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Types.None
 329 | RTLabs_semantics.Finalstate x -> Types.None
 330
 331 type rTLabs_pc =
 332 | Rapc_state of Pointers.block * Graphs.label
 333 | Rapc_call of Graphs.label Types.option * Pointers.block
 334 | Rapc_ret of Pointers.block Types.option
 335 | Rapc_fin
 336
 337 (** val rTLabs_pc_rect_Type4 :
 338     (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
 339     Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
 340     rTLabs_pc -> 'a1 **)
 341 let rec rTLabs_pc_rect_Type4 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
 342 | Rapc_state (x_24356, x_24355) -> h_rapc_state x_24356 x_24355
 343 | Rapc_call (x_24358, x_24357) -> h_rapc_call x_24358 x_24357
 344 | Rapc_ret x_24359 -> h_rapc_ret x_24359
 345 | Rapc_fin -> h_rapc_fin
 346
 347 (** val rTLabs_pc_rect_Type5 :
 348     (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
 349     Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
 350     rTLabs_pc -> 'a1 **)
 351 let rec rTLabs_pc_rect_Type5 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
 352 | Rapc_state (x_24366, x_24365) -> h_rapc_state x_24366 x_24365
 353 | Rapc_call (x_24368, x_24367) -> h_rapc_call x_24368 x_24367
 354 | Rapc_ret x_24369 -> h_rapc_ret x_24369
 355 | Rapc_fin -> h_rapc_fin
 356
 357 (** val rTLabs_pc_rect_Type3 :
 358     (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
 359     Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
 360     rTLabs_pc -> 'a1 **)
 361 let rec rTLabs_pc_rect_Type3 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
 362 | Rapc_state (x_24376, x_24375) -> h_rapc_state x_24376 x_24375
 363 | Rapc_call (x_24378, x_24377) -> h_rapc_call x_24378 x_24377
 364 | Rapc_ret x_24379 -> h_rapc_ret x_24379
 365 | Rapc_fin -> h_rapc_fin
 366
 367 (** val rTLabs_pc_rect_Type2 :
 368     (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
 369     Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
 370     rTLabs_pc -> 'a1 **)
 371 let rec rTLabs_pc_rect_Type2 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
 372 | Rapc_state (x_24386, x_24385) -> h_rapc_state x_24386 x_24385
 373 | Rapc_call (x_24388, x_24387) -> h_rapc_call x_24388 x_24387
 374 | Rapc_ret x_24389 -> h_rapc_ret x_24389
 375 | Rapc_fin -> h_rapc_fin
 376
 377 (** val rTLabs_pc_rect_Type1 :
 378     (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
 379     Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
 380     rTLabs_pc -> 'a1 **)
 381 let rec rTLabs_pc_rect_Type1 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
 382 | Rapc_state (x_24396, x_24395) -> h_rapc_state x_24396 x_24395
 383 | Rapc_call (x_24398, x_24397) -> h_rapc_call x_24398 x_24397
 384 | Rapc_ret x_24399 -> h_rapc_ret x_24399
 385 | Rapc_fin -> h_rapc_fin
 386
 387 (** val rTLabs_pc_rect_Type0 :
 388     (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
 389     Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
 390     rTLabs_pc -> 'a1 **)
 391 let rec rTLabs_pc_rect_Type0 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
 392 | Rapc_state (x_24406, x_24405) -> h_rapc_state x_24406 x_24405
 393 | Rapc_call (x_24408, x_24407) -> h_rapc_call x_24408 x_24407
 394 | Rapc_ret x_24409 -> h_rapc_ret x_24409
 395 | Rapc_fin -> h_rapc_fin
 396
 397 (** val rTLabs_pc_inv_rect_Type4 :
 398     rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
 399     (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
 400     (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 401 let rTLabs_pc_inv_rect_Type4 hterm h1 h2 h3 h4 =
 402   let hcut = rTLabs_pc_rect_Type4 h1 h2 h3 h4 hterm in hcut __
 403
 404 (** val rTLabs_pc_inv_rect_Type3 :
 405     rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
 406     (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
 407     (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 408 let rTLabs_pc_inv_rect_Type3 hterm h1 h2 h3 h4 =
 409   let hcut = rTLabs_pc_rect_Type3 h1 h2 h3 h4 hterm in hcut __
 410
 411 (** val rTLabs_pc_inv_rect_Type2 :
 412     rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
 413     (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
 414     (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 415 let rTLabs_pc_inv_rect_Type2 hterm h1 h2 h3 h4 =
 416   let hcut = rTLabs_pc_rect_Type2 h1 h2 h3 h4 hterm in hcut __
 417
 418 (** val rTLabs_pc_inv_rect_Type1 :
 419     rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
 420     (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
 421     (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 422 let rTLabs_pc_inv_rect_Type1 hterm h1 h2 h3 h4 =
 423   let hcut = rTLabs_pc_rect_Type1 h1 h2 h3 h4 hterm in hcut __
 424
 425 (** val rTLabs_pc_inv_rect_Type0 :
 426     rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
 427     (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
 428     (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 429 let rTLabs_pc_inv_rect_Type0 hterm h1 h2 h3 h4 =
 430   let hcut = rTLabs_pc_rect_Type0 h1 h2 h3 h4 hterm in hcut __
 431
 432 (** val rTLabs_pc_discr : rTLabs_pc -> rTLabs_pc -> __ **)
 433 let rTLabs_pc_discr x y =
 434   Logic.eq_rect_Type2 x
 435     (match x with
 436      | Rapc_state (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 437      | Rapc_call (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 438      | Rapc_ret a0 -> Obj.magic (fun _ dH -> dH __)
 439      | Rapc_fin -> Obj.magic (fun _ dH -> dH)) y
 440
 441 (** val rTLabs_pc_jmdiscr : rTLabs_pc -> rTLabs_pc -> __ **)
 442 let rTLabs_pc_jmdiscr x y =
 443   Logic.eq_rect_Type2 x
 444     (match x with
 445      | Rapc_state (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 446      | Rapc_call (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 447      | Rapc_ret a0 -> Obj.magic (fun _ dH -> dH __)
 448      | Rapc_fin -> Obj.magic (fun _ dH -> dH)) y
 449
 450 (** val rTLabs_pc_eq : rTLabs_pc -> rTLabs_pc -> Bool.bool **)
 451 let rTLabs_pc_eq x y =
 452   match x with
 453   | Rapc_state (b1, l1) ->
 454     (match y with
 455      | Rapc_state (b2, l2) ->
 456        Bool.andb (Pointers.eq_block b1 b2)
 457          (Identifiers.eq_identifier PreIdentifiers.LabelTag l1 l2)
 458      | Rapc_call (x0, x1) -> Bool.False
 459      | Rapc_ret x0 -> Bool.False
 460      | Rapc_fin -> Bool.False)
 461   | Rapc_call (o1, b1) ->
 462     (match y with
 463      | Rapc_state (x0, x1) -> Bool.False
 464      | Rapc_call (o2, b2) ->
 465        Bool.andb
 466          (Deqsets.eqb
 467            (Deqsets.deqOption
 468              (Identifiers.deq_identifier PreIdentifiers.LabelTag))
 469            (Obj.magic o1) (Obj.magic o2)) (Pointers.eq_block b1 b2)
 470      | Rapc_ret x0 -> Bool.False
 471      | Rapc_fin -> Bool.False)
 472   | Rapc_ret b1 ->
 473     (match y with
 474      | Rapc_state (x0, x1) -> Bool.False
 475      | Rapc_call (x0, x1) -> Bool.False
 476      | Rapc_ret b2 ->
 477        Deqsets.eqb (Deqsets.deqOption Pointers.block_eq) (Obj.magic b1)
 478          (Obj.magic b2)
 479      | Rapc_fin -> Bool.False)
 480   | Rapc_fin ->
 481     (match y with
 482      | Rapc_state (x0, x1) -> Bool.False
 483      | Rapc_call (x0, x1) -> Bool.False
 484      | Rapc_ret x0 -> Bool.False
 485      | Rapc_fin -> Bool.True)
 486
 487 (** val rTLabs_deqset : Deqsets.deqSet **)
 488 let rTLabs_deqset =
 489   Obj.magic rTLabs_pc_eq
 490
 491 (** val rTLabs_ext_state_to_pc :
 492     RTLabs_semantics.genv -> rTLabs_ext_state -> __ **)
 493 let rTLabs_ext_state_to_pc ge s =
 494   let { ras_state = s'; ras_fn_stack = stk } = s in
 495   (match s' with
 496    | RTLabs_semantics.State (f, fs, m) ->
 497      (match stk with
 498       | List.Nil -> (fun _ -> assert false (* absurd case *))
 499       | List.Cons (b, x) ->
 500         (fun _ -> Obj.magic (Rapc_state (b, f.RTLabs_semantics.next))))
 501    | RTLabs_semantics.Callstate (x, x0, x1, x2, fs, x3) ->
 502      (match stk with
 503       | List.Nil -> (fun _ _ -> assert false (* absurd case *))
 504       | List.Cons (b, x4) ->
 505         (fun _ _ ->
 506           Obj.magic (Rapc_call
 507             ((match fs with
 508               | List.Nil -> Types.None
 509               | List.Cons (f, x6) -> Types.Some f.RTLabs_semantics.next), b))))
 510        __
 511    | RTLabs_semantics.Returnstate (x, x0, x1, x2) ->
 512      (match stk with
 513       | List.Nil -> (fun _ -> Obj.magic (Rapc_ret Types.None))
 514       | List.Cons (b, x3) -> (fun _ -> Obj.magic (Rapc_ret (Types.Some b))))
 515    | RTLabs_semantics.Finalstate x -> (fun _ -> Obj.magic Rapc_fin)) __
 516
 517 (** val rTLabs_pc_to_cost_label :
 518     RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t -> rTLabs_pc
 519     -> CostLabel.costlabel Types.option **)
 520 let rTLabs_pc_to_cost_label ge = function
 521 | Rapc_state (b, l) ->
 522   (match Globalenvs.find_funct_ptr ge b with
 523    | Types.None -> Types.None
 524    | Types.Some fd ->
 525      (match fd with
 526       | AST.Internal f ->
 527         (match Identifiers.lookup PreIdentifiers.LabelTag
 528                  f.RTLabs_syntax.f_graph l with
 529          | Types.None -> Types.None
 530          | Types.Some s -> CostSpec.cost_label_of s)
 531       | AST.External x -> Types.None))
 532 | Rapc_call (x, x0) -> Types.None
 533 | Rapc_ret x -> Types.None
 534 | Rapc_fin -> Types.None
 535
 536 (** val rTLabs_call_ident :
 537     RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 -> AST.ident **)
 538 let rTLabs_call_ident ge s =
 539   let s0 = s in
 540   (let { ras_state = s'; ras_fn_stack = stk } = s0 in
 541   (match s' with
 542    | RTLabs_semantics.State (f, x, x0) ->
 543      (fun _ -> assert false (* absurd case *))
 544    | RTLabs_semantics.Callstate (fid, x, x0, x1, x2, x3) -> (fun _ -> fid)
 545    | RTLabs_semantics.Returnstate (x, x0, x1, x2) ->
 546      (fun _ -> assert false (* absurd case *))
 547    | RTLabs_semantics.Finalstate x ->
 548      (fun _ -> assert false (* absurd case *)))) __
 549
 550 (** val rTLabs_status :
 551     RTLabs_semantics.genv -> StructuredTraces.abstract_status **)
 552 let rTLabs_status ge =
 553   { StructuredTraces.as_pc = rTLabs_deqset; StructuredTraces.as_pc_of =
 554     (Obj.magic (rTLabs_ext_state_to_pc ge)); StructuredTraces.as_classify =
 555     (fun h -> rTLabs_classify (Obj.magic h).ras_state);
 556     StructuredTraces.as_label_of_pc =
 557     (Obj.magic (rTLabs_pc_to_cost_label ge)); StructuredTraces.as_result =
 558     (fun h -> RTLabs_semantics.rTLabs_is_final (Obj.magic h).ras_state);
 559     StructuredTraces.as_call_ident = (Obj.magic (rTLabs_call_ident ge));
 560     StructuredTraces.as_tailcall_ident = (fun s -> assert false
 561     (* absurd case *)) }
 562
 563 (** val eval_ext_statement :
 564     RTLabs_semantics.genv -> rTLabs_ext_state -> (IO.io_out, IO.io_in,
 565     (Events.trace, rTLabs_ext_state) Types.prod) IOMonad.iO **)
 566 let eval_ext_statement ge s =
 567   (match RTLabs_semantics.eval_statement ge s.ras_state with
 568    | IOMonad.Interact (o, k) ->
 569      (fun x -> IOMonad.Wrong (Errors.msg ErrorMessages.UnexpectedIO))
 570    | IOMonad.Value ts ->
 571      (fun next -> IOMonad.Value { Types.fst = ts.Types.fst; Types.snd =
 572        (next ts.Types.snd ts.Types.fst __) })
 573    | IOMonad.Wrong m -> (fun x -> IOMonad.Wrong m)) (fun x x0 _ ->
 574     next_state ge s x x0)
 575
 576 (** val rTLabs_ext_exec :
 577     (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
 578 let rTLabs_ext_exec =
 579   { SmallstepExec.is_final = (fun x h ->
 580     RTLabs_semantics.rTLabs_is_final (Obj.magic h).ras_state);
 581     SmallstepExec.step = (Obj.magic eval_ext_statement) }
 582
 583 (** val make_ext_initial_state :
 584     RTLabs_syntax.rTLabs_program -> rTLabs_ext_state Errors.res **)
 585 let make_ext_initial_state p =
 586   let ge = RTLabs_semantics.make_global p in
 587   Obj.magic
 588     (Monad.m_bind0 (Monad.max_def Errors.res0)
 589       (Obj.magic (Globalenvs.init_mem (fun x -> x) p)) (fun m ->
 590       let main = p.AST.prog_main in
 591       Obj.magic
 592         (Errors.bind_eq
 593           (Errors.opt_to_res (List.Cons ((Errors.MSG
 594             ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
 595             (PreIdentifiers.SymbolTag, main)), List.Nil))))
 596             (Globalenvs.find_symbol ge main)) (fun b _ ->
 597           Errors.bind_eq
 598             (Errors.opt_to_res (List.Cons ((Errors.MSG
 599               ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
 600               (PreIdentifiers.SymbolTag, main)), List.Nil))))
 601               (Globalenvs.find_funct_ptr ge b)) (fun f _ ->
 602             let s = RTLabs_semantics.Callstate (main, f, List.Nil,
 603               Types.None, List.Nil, m)
 604             in
 605             Obj.magic
 606               (Monad.m_return0 (Monad.max_def Errors.res0) { ras_state = s;
 607                 ras_fn_stack = (List.Cons (b, List.Nil)) }))))))
 608
 609 (** val rTLabs_ext_fullexec :
 610     (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
 611 let rTLabs_ext_fullexec =
 612   { SmallstepExec.es1 = rTLabs_ext_exec; SmallstepExec.make_global =
 613     (Obj.magic RTLabs_semantics.make_global);
 614     SmallstepExec.make_initial_state = (Obj.magic make_ext_initial_state) }
 615