open Preamble

open BitVectorTrie

open Graphs

open Order

open Registers

open FrontEndOps

open RTLabs_syntax

open SmallstepExec

open CostLabel

open Events

open IOMonad

open IO

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open Hide

open ByteValues

open Division

open Z

open BitVectorZ

open Pointers

open GenMem

open FrontEndMem

open Proper

open PositiveMap

open Deqsets

open Extralib

open Lists

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open Globalenvs

open ErrorMessages

open Option

open Setoids

open Monad

open Jmeq

open Russell

open Positive

open PreIdentifiers

open Errors

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open RTLabs_semantics

type rTLabs_state = RTLabs_semantics.state

type rTLabs_genv = RTLabs_semantics.genv

open Sets

open Listb

open StructuredTraces

open CostSpec

open Deqsets_extra

(** val status_class_jmdiscr :
    StructuredTraces.status_class -> StructuredTraces.status_class -> __ **)
let status_class_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | StructuredTraces.Cl_return -> Obj.magic (fun _ dH -> dH)
     | StructuredTraces.Cl_jump -> Obj.magic (fun _ dH -> dH)
     | StructuredTraces.Cl_call -> Obj.magic (fun _ dH -> dH)
     | StructuredTraces.Cl_tailcall -> Obj.magic (fun _ dH -> dH)
     | StructuredTraces.Cl_other -> Obj.magic (fun _ dH -> dH)) y

type rTLabs_ext_state = { ras_state : RTLabs_semantics.state;
                          ras_fn_stack : Pointers.block List.list }

(** val rTLabs_ext_state_rect_Type4 :
    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
let rec rTLabs_ext_state_rect_Type4 ge h_mk_RTLabs_ext_state x_24320 =
  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24320 in
  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __

(** val rTLabs_ext_state_rect_Type5 :
    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
let rec rTLabs_ext_state_rect_Type5 ge h_mk_RTLabs_ext_state x_24322 =
  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24322 in
  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __

(** val rTLabs_ext_state_rect_Type3 :
    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
let rec rTLabs_ext_state_rect_Type3 ge h_mk_RTLabs_ext_state x_24324 =
  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24324 in
  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __

(** val rTLabs_ext_state_rect_Type2 :
    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
let rec rTLabs_ext_state_rect_Type2 ge h_mk_RTLabs_ext_state x_24326 =
  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24326 in
  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __

(** val rTLabs_ext_state_rect_Type1 :
    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
let rec rTLabs_ext_state_rect_Type1 ge h_mk_RTLabs_ext_state x_24328 =
  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24328 in
  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __

(** val rTLabs_ext_state_rect_Type0 :
    RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
let rec rTLabs_ext_state_rect_Type0 ge h_mk_RTLabs_ext_state x_24330 =
  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_24330 in
  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __

(** val ras_state :
    RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state **)
let rec ras_state ge xxx =
  xxx.ras_state

(** val ras_fn_stack :
    RTLabs_semantics.genv -> rTLabs_ext_state -> Pointers.block List.list **)
let rec ras_fn_stack ge xxx =
  xxx.ras_fn_stack

(** val rTLabs_ext_state_inv_rect_Type4 :
    RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
    Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
let rTLabs_ext_state_inv_rect_Type4 x1 hterm h1 =
  let hcut = rTLabs_ext_state_rect_Type4 x1 h1 hterm in hcut __

(** val rTLabs_ext_state_inv_rect_Type3 :
    RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
    Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
let rTLabs_ext_state_inv_rect_Type3 x1 hterm h1 =
  let hcut = rTLabs_ext_state_rect_Type3 x1 h1 hterm in hcut __

(** val rTLabs_ext_state_inv_rect_Type2 :
    RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
    Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
let rTLabs_ext_state_inv_rect_Type2 x1 hterm h1 =
  let hcut = rTLabs_ext_state_rect_Type2 x1 h1 hterm in hcut __

(** val rTLabs_ext_state_inv_rect_Type1 :
    RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
    Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
let rTLabs_ext_state_inv_rect_Type1 x1 hterm h1 =
  let hcut = rTLabs_ext_state_rect_Type1 x1 h1 hterm in hcut __

(** val rTLabs_ext_state_inv_rect_Type0 :
    RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
    Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1 **)
let rTLabs_ext_state_inv_rect_Type0 x1 hterm h1 =
  let hcut = rTLabs_ext_state_rect_Type0 x1 h1 hterm in hcut __

(** val rTLabs_ext_state_discr :
    RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __ **)
let rTLabs_ext_state_discr a1 x y =
  Logic.eq_rect_Type2 x
    (let { ras_state = a0; ras_fn_stack = a10 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val rTLabs_ext_state_jmdiscr :
    RTLabs_semantics.genv -> rTLabs_ext_state -> rTLabs_ext_state -> __ **)
let rTLabs_ext_state_jmdiscr a1 x y =
  Logic.eq_rect_Type2 x
    (let { ras_state = a0; ras_fn_stack = a10 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val dpi1__o__Ras_state__o__inject :
    RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
    RTLabs_semantics.state Types.sig0 **)
let dpi1__o__Ras_state__o__inject x1 x3 =
  x3.Types.dpi1.ras_state

(** val eject__o__Ras_state__o__inject :
    RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
    RTLabs_semantics.state Types.sig0 **)
let eject__o__Ras_state__o__inject x1 x3 =
  (Types.pi1 x3).ras_state

(** val ras_state__o__inject :
    RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state
    Types.sig0 **)
let ras_state__o__inject x1 x2 =
  x2.ras_state

(** val dpi1__o__Ras_state :
    RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
    RTLabs_semantics.state **)
let dpi1__o__Ras_state x0 x2 =
  x2.Types.dpi1.ras_state

(** val eject__o__Ras_state :
    RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
    RTLabs_semantics.state **)
let eject__o__Ras_state x0 x2 =
  (Types.pi1 x2).ras_state

(** val next_state :
    RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state ->
    Events.trace -> rTLabs_ext_state **)
let next_state ge s s' t =
  { ras_state = s'; ras_fn_stack =
    ((match s' with
      | RTLabs_semantics.State (x, x0, x1) -> (fun _ -> s.ras_fn_stack)
      | RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) ->
        (fun _ -> List.Cons
          ((Types.pi1
             (RTLabs_semantics.func_block_of_exec ge s.ras_state t x x0 x1 x2
               x3 x4)), s.ras_fn_stack))
      | RTLabs_semantics.Returnstate (x, x0, x1, x2) ->
        (fun _ -> List.tail s.ras_fn_stack)
      | RTLabs_semantics.Finalstate x -> (fun _ -> List.Nil)) __) }

(** val rTLabs_classify :
    RTLabs_semantics.state -> StructuredTraces.status_class **)
let rTLabs_classify = function
| RTLabs_semantics.State (f, x, x0) ->
  (match RTLabs_semantics.next_instruction f with
   | RTLabs_syntax.St_skip x1 -> StructuredTraces.Cl_other
   | RTLabs_syntax.St_cost (x1, x2) -> StructuredTraces.Cl_other
   | RTLabs_syntax.St_const (x1, x2, x3, x4) -> StructuredTraces.Cl_other
   | RTLabs_syntax.St_op1 (x1, x2, x3, x4, x5, x6) ->
     StructuredTraces.Cl_other
   | RTLabs_syntax.St_op2 (x1, x2, x3, x4, x5, x6, x7, x8) ->
     StructuredTraces.Cl_other
   | RTLabs_syntax.St_load (x1, x2, x3, x4) -> StructuredTraces.Cl_other
   | RTLabs_syntax.St_store (x1, x2, x3, x4) -> StructuredTraces.Cl_other
   | RTLabs_syntax.St_call_id (x1, x2, x3, x4) -> StructuredTraces.Cl_other
   | RTLabs_syntax.St_call_ptr (x1, x2, x3, x4) -> StructuredTraces.Cl_other
   | RTLabs_syntax.St_cond (x1, x2, x3) -> StructuredTraces.Cl_jump
   | RTLabs_syntax.St_return -> StructuredTraces.Cl_other)
| RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) ->
  StructuredTraces.Cl_call
| RTLabs_semantics.Returnstate (x, x0, x1, x2) -> StructuredTraces.Cl_return
| RTLabs_semantics.Finalstate x -> StructuredTraces.Cl_other

(** val rTLabs_cost : RTLabs_semantics.state -> Bool.bool **)
let rTLabs_cost = function
| RTLabs_semantics.State (f, fs, m) ->
  CostSpec.is_cost_label (RTLabs_semantics.next_instruction f)
| RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) -> Bool.False
| RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Bool.False
| RTLabs_semantics.Finalstate x -> Bool.False

(** val rTLabs_cost_label :
    RTLabs_semantics.state -> CostLabel.costlabel Types.option **)
let rTLabs_cost_label = function
| RTLabs_semantics.State (f, fs, m) ->
  CostSpec.cost_label_of (RTLabs_semantics.next_instruction f)
| RTLabs_semantics.Callstate (x, x0, x1, x2, x3, x4) -> Types.None
| RTLabs_semantics.Returnstate (x, x0, x1, x2) -> Types.None
| RTLabs_semantics.Finalstate x -> Types.None

type rTLabs_pc =
| Rapc_state of Pointers.block * Graphs.label
| Rapc_call of Graphs.label Types.option * Pointers.block
| Rapc_ret of Pointers.block Types.option
| Rapc_fin

(** val rTLabs_pc_rect_Type4 :
    (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
    Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
    rTLabs_pc -> 'a1 **)
let rec rTLabs_pc_rect_Type4 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
| Rapc_state (x_24356, x_24355) -> h_rapc_state x_24356 x_24355
| Rapc_call (x_24358, x_24357) -> h_rapc_call x_24358 x_24357
| Rapc_ret x_24359 -> h_rapc_ret x_24359
| Rapc_fin -> h_rapc_fin

(** val rTLabs_pc_rect_Type5 :
    (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
    Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
    rTLabs_pc -> 'a1 **)
let rec rTLabs_pc_rect_Type5 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
| Rapc_state (x_24366, x_24365) -> h_rapc_state x_24366 x_24365
| Rapc_call (x_24368, x_24367) -> h_rapc_call x_24368 x_24367
| Rapc_ret x_24369 -> h_rapc_ret x_24369
| Rapc_fin -> h_rapc_fin

(** val rTLabs_pc_rect_Type3 :
    (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
    Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
    rTLabs_pc -> 'a1 **)
let rec rTLabs_pc_rect_Type3 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
| Rapc_state (x_24376, x_24375) -> h_rapc_state x_24376 x_24375
| Rapc_call (x_24378, x_24377) -> h_rapc_call x_24378 x_24377
| Rapc_ret x_24379 -> h_rapc_ret x_24379
| Rapc_fin -> h_rapc_fin

(** val rTLabs_pc_rect_Type2 :
    (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
    Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
    rTLabs_pc -> 'a1 **)
let rec rTLabs_pc_rect_Type2 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
| Rapc_state (x_24386, x_24385) -> h_rapc_state x_24386 x_24385
| Rapc_call (x_24388, x_24387) -> h_rapc_call x_24388 x_24387
| Rapc_ret x_24389 -> h_rapc_ret x_24389
| Rapc_fin -> h_rapc_fin

(** val rTLabs_pc_rect_Type1 :
    (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
    Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
    rTLabs_pc -> 'a1 **)
let rec rTLabs_pc_rect_Type1 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
| Rapc_state (x_24396, x_24395) -> h_rapc_state x_24396 x_24395
| Rapc_call (x_24398, x_24397) -> h_rapc_call x_24398 x_24397
| Rapc_ret x_24399 -> h_rapc_ret x_24399
| Rapc_fin -> h_rapc_fin

(** val rTLabs_pc_rect_Type0 :
    (Pointers.block -> Graphs.label -> 'a1) -> (Graphs.label Types.option ->
    Pointers.block -> 'a1) -> (Pointers.block Types.option -> 'a1) -> 'a1 ->
    rTLabs_pc -> 'a1 **)
let rec rTLabs_pc_rect_Type0 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
| Rapc_state (x_24406, x_24405) -> h_rapc_state x_24406 x_24405
| Rapc_call (x_24408, x_24407) -> h_rapc_call x_24408 x_24407
| Rapc_ret x_24409 -> h_rapc_ret x_24409
| Rapc_fin -> h_rapc_fin

(** val rTLabs_pc_inv_rect_Type4 :
    rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
    (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
    (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let rTLabs_pc_inv_rect_Type4 hterm h1 h2 h3 h4 =
  let hcut = rTLabs_pc_rect_Type4 h1 h2 h3 h4 hterm in hcut __

(** val rTLabs_pc_inv_rect_Type3 :
    rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
    (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
    (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let rTLabs_pc_inv_rect_Type3 hterm h1 h2 h3 h4 =
  let hcut = rTLabs_pc_rect_Type3 h1 h2 h3 h4 hterm in hcut __

(** val rTLabs_pc_inv_rect_Type2 :
    rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
    (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
    (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let rTLabs_pc_inv_rect_Type2 hterm h1 h2 h3 h4 =
  let hcut = rTLabs_pc_rect_Type2 h1 h2 h3 h4 hterm in hcut __

(** val rTLabs_pc_inv_rect_Type1 :
    rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
    (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
    (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let rTLabs_pc_inv_rect_Type1 hterm h1 h2 h3 h4 =
  let hcut = rTLabs_pc_rect_Type1 h1 h2 h3 h4 hterm in hcut __

(** val rTLabs_pc_inv_rect_Type0 :
    rTLabs_pc -> (Pointers.block -> Graphs.label -> __ -> 'a1) ->
    (Graphs.label Types.option -> Pointers.block -> __ -> 'a1) ->
    (Pointers.block Types.option -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let rTLabs_pc_inv_rect_Type0 hterm h1 h2 h3 h4 =
  let hcut = rTLabs_pc_rect_Type0 h1 h2 h3 h4 hterm in hcut __

(** val rTLabs_pc_discr : rTLabs_pc -> rTLabs_pc -> __ **)
let rTLabs_pc_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Rapc_state (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Rapc_call (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Rapc_ret a0 -> Obj.magic (fun _ dH -> dH __)
     | Rapc_fin -> Obj.magic (fun _ dH -> dH)) y

(** val rTLabs_pc_jmdiscr : rTLabs_pc -> rTLabs_pc -> __ **)
let rTLabs_pc_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Rapc_state (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Rapc_call (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
     | Rapc_ret a0 -> Obj.magic (fun _ dH -> dH __)
     | Rapc_fin -> Obj.magic (fun _ dH -> dH)) y

(** val rTLabs_pc_eq : rTLabs_pc -> rTLabs_pc -> Bool.bool **)
let rTLabs_pc_eq x y =
  match x with
  | Rapc_state (b1, l1) ->
    (match y with
     | Rapc_state (b2, l2) ->
       Bool.andb (Pointers.eq_block b1 b2)
         (Identifiers.eq_identifier PreIdentifiers.LabelTag l1 l2)
     | Rapc_call (x0, x1) -> Bool.False
     | Rapc_ret x0 -> Bool.False
     | Rapc_fin -> Bool.False)
  | Rapc_call (o1, b1) ->
    (match y with
     | Rapc_state (x0, x1) -> Bool.False
     | Rapc_call (o2, b2) ->
       Bool.andb
         (Deqsets.eqb
           (Deqsets.deqOption
             (Identifiers.deq_identifier PreIdentifiers.LabelTag))
           (Obj.magic o1) (Obj.magic o2)) (Pointers.eq_block b1 b2)
     | Rapc_ret x0 -> Bool.False
     | Rapc_fin -> Bool.False)
  | Rapc_ret b1 ->
    (match y with
     | Rapc_state (x0, x1) -> Bool.False
     | Rapc_call (x0, x1) -> Bool.False
     | Rapc_ret b2 ->
       Deqsets.eqb (Deqsets.deqOption Pointers.block_eq) (Obj.magic b1)
         (Obj.magic b2)
     | Rapc_fin -> Bool.False)
  | Rapc_fin ->
    (match y with
     | Rapc_state (x0, x1) -> Bool.False
     | Rapc_call (x0, x1) -> Bool.False
     | Rapc_ret x0 -> Bool.False
     | Rapc_fin -> Bool.True)

(** val rTLabs_deqset : Deqsets.deqSet **)
let rTLabs_deqset =
  Obj.magic rTLabs_pc_eq

(** val rTLabs_ext_state_to_pc :
    RTLabs_semantics.genv -> rTLabs_ext_state -> __ **)
let rTLabs_ext_state_to_pc ge s =
  let { ras_state = s'; ras_fn_stack = stk } = s in
  (match s' with
   | RTLabs_semantics.State (f, fs, m) ->
     (match stk with
      | List.Nil -> (fun _ -> assert false (* absurd case *))
      | List.Cons (b, x) ->
        (fun _ -> Obj.magic (Rapc_state (b, f.RTLabs_semantics.next))))
   | RTLabs_semantics.Callstate (x, x0, x1, x2, fs, x3) ->
     (match stk with
      | List.Nil -> (fun _ _ -> assert false (* absurd case *))
      | List.Cons (b, x4) ->
        (fun _ _ ->
          Obj.magic (Rapc_call
            ((match fs with
              | List.Nil -> Types.None
              | List.Cons (f, x6) -> Types.Some f.RTLabs_semantics.next), b))))
       __
   | RTLabs_semantics.Returnstate (x, x0, x1, x2) ->
     (match stk with
      | List.Nil -> (fun _ -> Obj.magic (Rapc_ret Types.None))
      | List.Cons (b, x3) -> (fun _ -> Obj.magic (Rapc_ret (Types.Some b))))
   | RTLabs_semantics.Finalstate x -> (fun _ -> Obj.magic Rapc_fin)) __

(** val rTLabs_pc_to_cost_label :
    RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t -> rTLabs_pc
    -> CostLabel.costlabel Types.option **)
let rTLabs_pc_to_cost_label ge = function
| Rapc_state (b, l) ->
  (match Globalenvs.find_funct_ptr ge b with
   | Types.None -> Types.None
   | Types.Some fd ->
     (match fd with
      | AST.Internal f ->
        (match Identifiers.lookup PreIdentifiers.LabelTag
                 f.RTLabs_syntax.f_graph l with
         | Types.None -> Types.None
         | Types.Some s -> CostSpec.cost_label_of s)
      | AST.External x -> Types.None))
| Rapc_call (x, x0) -> Types.None
| Rapc_ret x -> Types.None
| Rapc_fin -> Types.None

(** val rTLabs_call_ident :
    RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 -> AST.ident **)
let rTLabs_call_ident ge s =
  let s0 = s in
  (let { ras_state = s'; ras_fn_stack = stk } = s0 in
  (match s' with
   | RTLabs_semantics.State (f, x, x0) ->
     (fun _ -> assert false (* absurd case *))
   | RTLabs_semantics.Callstate (fid, x, x0, x1, x2, x3) -> (fun _ -> fid)
   | RTLabs_semantics.Returnstate (x, x0, x1, x2) ->
     (fun _ -> assert false (* absurd case *))
   | RTLabs_semantics.Finalstate x ->
     (fun _ -> assert false (* absurd case *)))) __

(** val rTLabs_status :
    RTLabs_semantics.genv -> StructuredTraces.abstract_status **)
let rTLabs_status ge =
  { StructuredTraces.as_pc = rTLabs_deqset; StructuredTraces.as_pc_of =
    (Obj.magic (rTLabs_ext_state_to_pc ge)); StructuredTraces.as_classify =
    (fun h -> rTLabs_classify (Obj.magic h).ras_state);
    StructuredTraces.as_label_of_pc =
    (Obj.magic (rTLabs_pc_to_cost_label ge)); StructuredTraces.as_result =
    (fun h -> RTLabs_semantics.rTLabs_is_final (Obj.magic h).ras_state);
    StructuredTraces.as_call_ident = (Obj.magic (rTLabs_call_ident ge));
    StructuredTraces.as_tailcall_ident = (fun s -> assert false
    (* absurd case *)) }

(** val eval_ext_statement :
    RTLabs_semantics.genv -> rTLabs_ext_state -> (IO.io_out, IO.io_in,
    (Events.trace, rTLabs_ext_state) Types.prod) IOMonad.iO **)
let eval_ext_statement ge s =
  (match RTLabs_semantics.eval_statement ge s.ras_state with
   | IOMonad.Interact (o, k) ->
     (fun x -> IOMonad.Wrong (Errors.msg ErrorMessages.UnexpectedIO))
   | IOMonad.Value ts ->
     (fun next -> IOMonad.Value { Types.fst = ts.Types.fst; Types.snd =
       (next ts.Types.snd ts.Types.fst __) })
   | IOMonad.Wrong m -> (fun x -> IOMonad.Wrong m)) (fun x x0 _ ->
    next_state ge s x x0)

(** val rTLabs_ext_exec :
    (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
let rTLabs_ext_exec =
  { SmallstepExec.is_final = (fun x h ->
    RTLabs_semantics.rTLabs_is_final (Obj.magic h).ras_state);
    SmallstepExec.step = (Obj.magic eval_ext_statement) }

(** val make_ext_initial_state :
    RTLabs_syntax.rTLabs_program -> rTLabs_ext_state Errors.res **)
let make_ext_initial_state p =
  let ge = RTLabs_semantics.make_global p in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (Globalenvs.init_mem (fun x -> x) p)) (fun m ->
      let main = p.AST.prog_main in
      Obj.magic
        (Errors.bind_eq
          (Errors.opt_to_res (List.Cons ((Errors.MSG
            ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
            (PreIdentifiers.SymbolTag, main)), List.Nil))))
            (Globalenvs.find_symbol ge main)) (fun b _ ->
          Errors.bind_eq
            (Errors.opt_to_res (List.Cons ((Errors.MSG
              ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
              (PreIdentifiers.SymbolTag, main)), List.Nil))))
              (Globalenvs.find_funct_ptr ge b)) (fun f _ ->
            let s = RTLabs_semantics.Callstate (main, f, List.Nil,
              Types.None, List.Nil, m)
            in
            Obj.magic
              (Monad.m_return0 (Monad.max_def Errors.res0) { ras_state = s;
                ras_fn_stack = (List.Cons (b, List.Nil)) }))))))

(** val rTLabs_ext_fullexec :
    (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
let rTLabs_ext_fullexec =
  { SmallstepExec.es1 = rTLabs_ext_exec; SmallstepExec.make_global =
    (Obj.magic RTLabs_semantics.make_global);
    SmallstepExec.make_initial_state = (Obj.magic make_ext_initial_state) }