open Preamble

open ExtraMonads

open Deqsets_extra

open State

open Bind_new

open BindLists

open Blocks

open TranslateUtils

open ExtraGlobalenvs

open I8051bis

open String

open Sets

open Listb

open LabelledObjects

open BitVectorTrie

open Graphs

open I8051

open Order

open Registers

open BackEndOps

open Joint

open BEMem

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 ErrorMessages

open Option

open Setoids

open Monad

open Jmeq

open Russell

open Positive

open PreIdentifiers

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Errors

open Globalenvs

open Joint_semantics

open SemanticsUtils

open StructuredTraces

type evaluation_params = { globals : AST.ident List.list;
                           ev_genv : Joint_semantics.genv }

(** val evaluation_params_rect_Type4 :
    Joint_semantics.sem_params -> (AST.ident List.list ->
    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_25115 =
  let { globals = globals0; ev_genv = ev_genv0 } = x_25115 in
  h_mk_evaluation_params globals0 ev_genv0

(** val evaluation_params_rect_Type5 :
    Joint_semantics.sem_params -> (AST.ident List.list ->
    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_25117 =
  let { globals = globals0; ev_genv = ev_genv0 } = x_25117 in
  h_mk_evaluation_params globals0 ev_genv0

(** val evaluation_params_rect_Type3 :
    Joint_semantics.sem_params -> (AST.ident List.list ->
    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_25119 =
  let { globals = globals0; ev_genv = ev_genv0 } = x_25119 in
  h_mk_evaluation_params globals0 ev_genv0

(** val evaluation_params_rect_Type2 :
    Joint_semantics.sem_params -> (AST.ident List.list ->
    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_25121 =
  let { globals = globals0; ev_genv = ev_genv0 } = x_25121 in
  h_mk_evaluation_params globals0 ev_genv0

(** val evaluation_params_rect_Type1 :
    Joint_semantics.sem_params -> (AST.ident List.list ->
    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_25123 =
  let { globals = globals0; ev_genv = ev_genv0 } = x_25123 in
  h_mk_evaluation_params globals0 ev_genv0

(** val evaluation_params_rect_Type0 :
    Joint_semantics.sem_params -> (AST.ident List.list ->
    Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_25125 =
  let { globals = globals0; ev_genv = ev_genv0 } = x_25125 in
  h_mk_evaluation_params globals0 ev_genv0

(** val globals :
    Joint_semantics.sem_params -> evaluation_params -> AST.ident List.list **)
let rec globals p xxx =
  xxx.globals

(** val ev_genv :
    Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv **)
let rec ev_genv p xxx =
  xxx.ev_genv

(** val evaluation_params_inv_rect_Type4 :
    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
let evaluation_params_inv_rect_Type4 x1 hterm h1 =
  let hcut = evaluation_params_rect_Type4 x1 h1 hterm in hcut __

(** val evaluation_params_inv_rect_Type3 :
    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
let evaluation_params_inv_rect_Type3 x1 hterm h1 =
  let hcut = evaluation_params_rect_Type3 x1 h1 hterm in hcut __

(** val evaluation_params_inv_rect_Type2 :
    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
let evaluation_params_inv_rect_Type2 x1 hterm h1 =
  let hcut = evaluation_params_rect_Type2 x1 h1 hterm in hcut __

(** val evaluation_params_inv_rect_Type1 :
    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
let evaluation_params_inv_rect_Type1 x1 hterm h1 =
  let hcut = evaluation_params_rect_Type1 x1 h1 hterm in hcut __

(** val evaluation_params_inv_rect_Type0 :
    Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list
    -> Joint_semantics.genv -> __ -> 'a1) -> 'a1 **)
let evaluation_params_inv_rect_Type0 x1 hterm h1 =
  let hcut = evaluation_params_rect_Type0 x1 h1 hterm in hcut __

(** val evaluation_params_discr :
    Joint_semantics.sem_params -> evaluation_params -> evaluation_params ->
    __ **)
let evaluation_params_discr a1 x y =
  Logic.eq_rect_Type2 x
    (let { globals = a0; ev_genv = a10 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val evaluation_params_jmdiscr :
    Joint_semantics.sem_params -> evaluation_params -> evaluation_params ->
    __ **)
let evaluation_params_jmdiscr a1 x y =
  Logic.eq_rect_Type2 x
    (let { globals = a0; ev_genv = a10 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val dpi1__o__ev_genv__o__inject :
    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
    Joint_semantics.genv Types.sig0 **)
let dpi1__o__ev_genv__o__inject x0 x2 =
  x2.Types.dpi1.ev_genv

(** val dpi1__o__ev_genv__o__ge__o__inject :
    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    Types.sig0 **)
let dpi1__o__ev_genv__o__ge__o__inject x0 x2 =
  Joint_semantics.ge__o__inject x2.Types.dpi1.globals x2.Types.dpi1.ev_genv

(** val dpi1__o__ev_genv__o__ge :
    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
let dpi1__o__ev_genv__o__ge x0 x2 =
  x2.Types.dpi1.ev_genv.Joint_semantics.ge

(** val eject__o__ev_genv__o__inject :
    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
    Joint_semantics.genv Types.sig0 **)
let eject__o__ev_genv__o__inject x0 x2 =
  (Types.pi1 x2).ev_genv

(** val eject__o__ev_genv__o__ge__o__inject :
    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    Types.sig0 **)
let eject__o__ev_genv__o__ge__o__inject x0 x2 =
  Joint_semantics.ge__o__inject (Types.pi1 x2).globals (Types.pi1 x2).ev_genv

(** val eject__o__ev_genv__o__ge :
    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
let eject__o__ev_genv__o__ge x0 x2 =
  (Types.pi1 x2).ev_genv.Joint_semantics.ge

(** val ev_genv__o__ge :
    Joint_semantics.sem_params -> evaluation_params ->
    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t **)
let ev_genv__o__ge x0 x1 =
  x1.ev_genv.Joint_semantics.ge

(** val ev_genv__o__ge__o__inject :
    Joint_semantics.sem_params -> evaluation_params ->
    Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
    Types.sig0 **)
let ev_genv__o__ge__o__inject x0 x1 =
  Joint_semantics.ge__o__inject x1.globals x1.ev_genv

(** val ev_genv__o__inject :
    Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
    Types.sig0 **)
let ev_genv__o__inject x0 x1 =
  x1.ev_genv

(** val dpi1__o__ev_genv :
    Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
    Joint_semantics.genv **)
let dpi1__o__ev_genv x0 x2 =
  x2.Types.dpi1.ev_genv

(** val eject__o__ev_genv :
    Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
    Joint_semantics.genv **)
let eject__o__ev_genv x0 x2 =
  (Types.pi1 x2).ev_genv

type prog_params = { prog_spars : Joint_semantics.sem_params;
                     prog : Joint.joint_program;
                     stack_sizes : (AST.ident -> Nat.nat Types.option) }

(** val prog_params_rect_Type4 :
    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
let rec prog_params_rect_Type4 h_mk_prog_params x_25141 =
  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    stack_sizes0 } = x_25141
  in
  h_mk_prog_params prog_spars0 prog0 stack_sizes0

(** val prog_params_rect_Type5 :
    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
let rec prog_params_rect_Type5 h_mk_prog_params x_25143 =
  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    stack_sizes0 } = x_25143
  in
  h_mk_prog_params prog_spars0 prog0 stack_sizes0

(** val prog_params_rect_Type3 :
    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
let rec prog_params_rect_Type3 h_mk_prog_params x_25145 =
  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    stack_sizes0 } = x_25145
  in
  h_mk_prog_params prog_spars0 prog0 stack_sizes0

(** val prog_params_rect_Type2 :
    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
let rec prog_params_rect_Type2 h_mk_prog_params x_25147 =
  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    stack_sizes0 } = x_25147
  in
  h_mk_prog_params prog_spars0 prog0 stack_sizes0

(** val prog_params_rect_Type1 :
    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
let rec prog_params_rect_Type1 h_mk_prog_params x_25149 =
  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    stack_sizes0 } = x_25149
  in
  h_mk_prog_params prog_spars0 prog0 stack_sizes0

(** val prog_params_rect_Type0 :
    (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
let rec prog_params_rect_Type0 h_mk_prog_params x_25151 =
  let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
    stack_sizes0 } = x_25151
  in
  h_mk_prog_params prog_spars0 prog0 stack_sizes0

(** val prog_spars : prog_params -> Joint_semantics.sem_params **)
let rec prog_spars xxx =
  xxx.prog_spars

(** val prog : prog_params -> Joint.joint_program **)
let rec prog xxx =
  xxx.prog

(** val stack_sizes : prog_params -> AST.ident -> Nat.nat Types.option **)
let rec stack_sizes xxx =
  xxx.stack_sizes

(** val prog_params_inv_rect_Type4 :
    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
let prog_params_inv_rect_Type4 hterm h1 =
  let hcut = prog_params_rect_Type4 h1 hterm in hcut __

(** val prog_params_inv_rect_Type3 :
    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
let prog_params_inv_rect_Type3 hterm h1 =
  let hcut = prog_params_rect_Type3 h1 hterm in hcut __

(** val prog_params_inv_rect_Type2 :
    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
let prog_params_inv_rect_Type2 hterm h1 =
  let hcut = prog_params_rect_Type2 h1 hterm in hcut __

(** val prog_params_inv_rect_Type1 :
    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
let prog_params_inv_rect_Type1 hterm h1 =
  let hcut = prog_params_rect_Type1 h1 hterm in hcut __

(** val prog_params_inv_rect_Type0 :
    prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
    (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1 **)
let prog_params_inv_rect_Type0 hterm h1 =
  let hcut = prog_params_rect_Type0 h1 hterm in hcut __

(** val prog_params_jmdiscr : prog_params -> prog_params -> __ **)
let prog_params_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { prog_spars = a0; prog = a1; stack_sizes = a2 } = x in
    Obj.magic (fun _ dH -> dH __ __ __)) y

(** val prog_spars__o__spp' :
    prog_params -> Joint_semantics.serialized_params **)
let prog_spars__o__spp' x0 =
  x0.prog_spars.Joint_semantics.spp'

(** val prog_spars__o__spp'__o__msu_pars :
    prog_params -> Joint.joint_closed_internal_function
    Joint_semantics.sem_unserialized_params **)
let prog_spars__o__spp'__o__msu_pars x0 =
  Joint_semantics.spp'__o__msu_pars x0.prog_spars

(** val prog_spars__o__spp'__o__msu_pars__o__st_pars :
    prog_params -> Joint_semantics.sem_state_params **)
let prog_spars__o__spp'__o__msu_pars__o__st_pars x0 =
  Joint_semantics.spp'__o__msu_pars__o__st_pars x0.prog_spars

(** val prog_spars__o__spp'__o__spp : prog_params -> Joint.params **)
let prog_spars__o__spp'__o__spp x0 =
  Joint_semantics.spp'__o__spp x0.prog_spars

(** val prog_spars__o__spp'__o__spp__o__stmt_pars :
    prog_params -> Joint.stmt_params **)
let prog_spars__o__spp'__o__spp__o__stmt_pars x0 =
  Joint_semantics.spp'__o__spp__o__stmt_pars x0.prog_spars

(** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
    prog_params -> Joint.uns_params **)
let prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars x0.prog_spars

(** val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
    prog_params -> Joint.unserialized_params **)
let prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
  Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
    x0.prog_spars

(** val joint_make_global : prog_params -> evaluation_params **)
let joint_make_global p =
  { globals =
    (Joint.prog_names (Joint_semantics.spp'__o__spp p.prog_spars) p.prog);
    ev_genv =
    (SemanticsUtils.joint_globalenv p.prog_spars p.prog p.stack_sizes) }

(** val joint_make_global__o__ev_genv :
    prog_params -> Joint_semantics.genv **)
let joint_make_global__o__ev_genv x0 =
  (joint_make_global x0).ev_genv

(** val joint_make_global__o__ev_genv__o__ge :
    prog_params -> Joint.joint_closed_internal_function AST.fundef
    Globalenvs.genv_t **)
let joint_make_global__o__ev_genv__o__ge x0 =
  ev_genv__o__ge x0.prog_spars (joint_make_global x0)

(** val joint_make_global__o__ev_genv__o__ge__o__inject :
    prog_params -> Joint.joint_closed_internal_function AST.fundef
    Globalenvs.genv_t Types.sig0 **)
let joint_make_global__o__ev_genv__o__ge__o__inject x0 =
  ev_genv__o__ge__o__inject x0.prog_spars (joint_make_global x0)

(** val joint_make_global__o__ev_genv__o__inject :
    prog_params -> Joint_semantics.genv Types.sig0 **)
let joint_make_global__o__ev_genv__o__inject x0 =
  ev_genv__o__inject x0.prog_spars (joint_make_global x0)

(** val joint_make_global__o__inject :
    prog_params -> evaluation_params Types.sig0 **)
let joint_make_global__o__inject x0 =
  joint_make_global x0

(** val make_initial_state :
    prog_params -> Joint_semantics.state_pc Errors.res **)
let make_initial_state pars =
  let p = pars.prog in
  let ge = ev_genv pars.prog_spars in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (Globalenvs.init_mem (fun x -> x) p.Joint.joint_prog))
      (fun m0 ->
      (let { Types.fst = m; Types.snd = spb } =
         GenMem.alloc m0 (Z.z_of_nat Nat.O) I8051bis.external_ram_size
       in
      (fun _ ->
      let globals_size =
        Joint.globals_stacksize
          (Joint_semantics.spp'__o__spp pars.prog_spars) p
      in
      let spp = { Pointers.pblock = spb; Pointers.poff =
        (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S Nat.O))))))))))))))))
          (Z.zopp (Z.z_of_nat (Nat.S globals_size)))) }
      in
      let main = p.Joint.joint_prog.AST.prog_main in
      let st = { Joint_semantics.st_frms = (Types.Some
        (prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_framesT);
        Joint_semantics.istack = Joint_semantics.Empty_is;
        Joint_semantics.carry = (ByteValues.BBbit Bool.False);
        Joint_semantics.regs =
        ((prog_spars__o__spp'__o__msu_pars__o__st_pars pars).Joint_semantics.empty_regsT
          spp); Joint_semantics.m = m; Joint_semantics.stack_usage =
        globals_size }
      in
      Monad.m_return0 (Monad.max_def Errors.res0)
        { Joint_semantics.st_no_pc =
        (Joint_semantics.set_sp
          (prog_spars__o__spp'__o__msu_pars__o__st_pars pars) spp st);
        Joint_semantics.pc = Joint_semantics.init_pc;
        Joint_semantics.last_pop = (Joint_semantics.null_pc Positive.One) }))
        __))

(** val joint_classify_step :
    Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
    StructuredTraces.status_class **)
let joint_classify_step p g = function
| Joint.COST_LABEL x -> StructuredTraces.Cl_other
| Joint.CALL (f, args, dest) -> StructuredTraces.Cl_call
| Joint.COND (x, x0) -> StructuredTraces.Cl_jump
| Joint.Step_seq x -> StructuredTraces.Cl_other

(** val joint_classify_final :
    Joint.unserialized_params -> Joint.joint_fin_step ->
    StructuredTraces.status_class **)
let joint_classify_final p = function
| Joint.GOTO x -> StructuredTraces.Cl_other
| Joint.RETURN -> StructuredTraces.Cl_return
| Joint.TAILCALL (f, args) -> StructuredTraces.Cl_tailcall

(** val joint_classify :
    Joint_semantics.sem_params -> evaluation_params ->
    Joint_semantics.state_pc -> StructuredTraces.status_class **)
let joint_classify p pars st =
  match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
          st.Joint_semantics.pc with
  | Errors.OK i_fn_s ->
    (match i_fn_s.Types.snd with
     | Joint.Sequential (s, x) ->
       joint_classify_step
         (Joint.uns_pars__o__u_pars
           (Joint_semantics.spp'__o__spp__o__stmt_pars p)) pars.globals s
     | Joint.Final s ->
       joint_classify_final
         (Joint.uns_pars__o__u_pars
           (Joint_semantics.spp'__o__spp__o__stmt_pars p)) s
     | Joint.FCOND (x0, x1, x2) -> StructuredTraces.Cl_jump)
  | Errors.Error x -> StructuredTraces.Cl_other

(** val joint_call_ident :
    Joint_semantics.sem_params -> evaluation_params ->
    Joint_semantics.state_pc -> AST.ident **)
let joint_call_ident p pars st =
  let dummy = Positive.One in
  (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
           st.Joint_semantics.pc with
   | Errors.OK x ->
     (match x.Types.snd with
      | Joint.Sequential (s, next) ->
        (match s with
         | Joint.COST_LABEL x0 -> dummy
         | Joint.CALL (f', args, dest) ->
           (match Obj.magic
                    (Monad.m_bind0 (Monad.max_def Errors.res0)
                      (Joint_semantics.block_of_call p pars.globals
                        pars.ev_genv f' st.Joint_semantics.st_no_pc)
                      (fun bl ->
                      Obj.magic
                        (Joint_semantics.fetch_internal_function pars.globals
                          pars.ev_genv bl))) with
            | Errors.OK i_f -> i_f.Types.fst
            | Errors.Error x0 -> dummy)
         | Joint.COND (x0, x1) -> dummy
         | Joint.Step_seq x0 -> dummy)
      | Joint.Final x0 -> dummy
      | Joint.FCOND (x0, x1, x2) -> dummy)
   | Errors.Error x -> dummy)

(** val joint_tailcall_ident :
    Joint_semantics.sem_params -> evaluation_params ->
    Joint_semantics.state_pc -> AST.ident **)
let joint_tailcall_ident p pars st =
  let dummy = Positive.One in
  (match Joint_semantics.fetch_statement p pars.globals pars.ev_genv
           st.Joint_semantics.pc with
   | Errors.OK x ->
     (match x.Types.snd with
      | Joint.Sequential (x0, x1) -> dummy
      | Joint.Final s ->
        (match s with
         | Joint.GOTO x0 -> dummy
         | Joint.RETURN -> dummy
         | Joint.TAILCALL (f', args) ->
           (match Obj.magic
                    (Monad.m_bind0 (Monad.max_def Errors.res0)
                      (Joint_semantics.block_of_call p pars.globals
                        pars.ev_genv f' st.Joint_semantics.st_no_pc)
                      (fun bl ->
                      Obj.magic
                        (Joint_semantics.fetch_internal_function pars.globals
                          pars.ev_genv bl))) with
            | Errors.OK i_f -> i_f.Types.fst
            | Errors.Error x0 -> dummy))
      | Joint.FCOND (x0, x1, x2) -> dummy)
   | Errors.Error x -> dummy)

(** val pcDeq : Deqsets.deqSet **)
let pcDeq =
  Obj.magic ByteValues.eq_program_counter

(** val cost_label_of_stmt :
    Joint.stmt_params -> AST.ident List.list -> Joint.joint_statement ->
    CostLabel.costlabel Types.option **)
let cost_label_of_stmt p g = function
| Joint.Sequential (s0, x) ->
  (match s0 with
   | Joint.COST_LABEL lbl -> Types.Some lbl
   | Joint.CALL (x0, x1, x2) -> Types.None
   | Joint.COND (x0, x1) -> Types.None
   | Joint.Step_seq x0 -> Types.None)
| Joint.Final x -> Types.None
| Joint.FCOND (x0, x1, x2) -> Types.None

(** val joint_label_of_pc :
    Joint_semantics.sem_params -> evaluation_params ->
    ByteValues.program_counter -> CostLabel.costlabel Types.option **)
let joint_label_of_pc p pars pc =
  match Joint_semantics.fetch_statement p pars.globals pars.ev_genv pc with
  | Errors.OK fn_stmt ->
    cost_label_of_stmt (Joint_semantics.spp'__o__spp__o__stmt_pars p)
      pars.globals fn_stmt.Types.snd
  | Errors.Error x -> Types.None

(** val exit_pc' : ByteValues.program_counter **)
let exit_pc' =
  { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O)));
    ByteValues.pc_offset = (Positive.P1 Positive.One) }

(** val joint_final :
    Joint_semantics.sem_params -> evaluation_params ->
    Joint_semantics.state_pc -> Integers.int Types.option **)
let joint_final p pars st =
  let ge = pars.ev_genv in
  (match ByteValues.eq_program_counter st.Joint_semantics.pc exit_pc' with
   | Bool.True ->
     let ret =
       (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main
     in
     (match Obj.magic
              (Monad.m_bind0 (Monad.max_def Errors.res0)
                (Obj.magic
                  (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result
                    pars.globals ge.Joint_semantics.ge ret
                    st.Joint_semantics.st_no_pc)) (fun vals ->
                Obj.magic (ByteValues.word_of_list_beval vals))) with
      | Errors.OK v -> Types.Some v
      | Errors.Error x -> Types.Some (BitVector.maximum Integers.wordsize))
   | Bool.False -> Types.None)

(** val joint_abstract_status :
    prog_params -> StructuredTraces.abstract_status **)
let joint_abstract_status p =
  { StructuredTraces.as_pc = pcDeq; StructuredTraces.as_pc_of =
    (Obj.magic
      (Joint_semantics.pc (prog_spars__o__spp'__o__msu_pars__o__st_pars p)));
    StructuredTraces.as_classify =
    (Obj.magic (joint_classify p.prog_spars (joint_make_global p)));
    StructuredTraces.as_label_of_pc =
    (Obj.magic (joint_label_of_pc p.prog_spars (joint_make_global p)));
    StructuredTraces.as_result =
    (Obj.magic (joint_final p.prog_spars (joint_make_global p)));
    StructuredTraces.as_call_ident = (fun st ->
    joint_call_ident p.prog_spars (joint_make_global p)
      (Types.pi1 (Obj.magic st))); StructuredTraces.as_tailcall_ident =
    (fun st ->
    joint_tailcall_ident p.prog_spars (joint_make_global p)
      (Types.pi1 (Obj.magic st))) }

(** val joint_status :
    Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
    Nat.nat Types.option) -> StructuredTraces.abstract_status **)
let joint_status p prog0 stacksizes =
  joint_abstract_status { prog_spars = p; prog = prog0; stack_sizes =
    stacksizes }