open Preamble

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open GenMem

open FrontEndMem

open Globalenvs

open String

open Sets

open Listb

open LabelledObjects

open BitVectorTrie

open Graphs

open I8051

open Order

open Registers

open CostLabel

open Hide

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Setoids

open Monad

open Option

open Extranat

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

open Types

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Positive

open Z

open BitVectorZ

open Pointers

open ByteValues

open BackEndOps

open Joint

open State

open Bind_new

open BindLists

open Blocks

open Deqsets_extra

val fresh_label :
  Joint.params -> AST.ident List.list -> Graphs.label
  Monad.smax_def__o__monad

val fresh_register :
  Joint.params -> AST.ident List.list -> Registers.register
  Monad.smax_def__o__monad

val adds_graph_pre :
  Joint.graph_params -> AST.ident List.list -> (Graphs.label -> 'a1 ->
  Joint.joint_seq) -> 'a1 List.list -> Graphs.label -> Graphs.label
  Monad.smax_def__o__monad

val adds_graph_post :
  Joint.graph_params -> AST.ident List.list -> Joint.joint_seq List.list ->
  Graphs.label -> Graphs.label Monad.smax_def__o__monad

val adds_graph :
  Joint.graph_params -> AST.ident List.list -> Blocks.step_block ->
  Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
  Joint.joint_internal_function

val fin_adds_graph :
  Joint.graph_params -> AST.ident List.list -> Blocks.fin_block ->
  Graphs.label -> Joint.joint_internal_function ->
  Joint.joint_internal_function

val b_adds_graph :
  Joint.graph_params -> AST.ident List.list -> Blocks.bind_step_block ->
  Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
  Joint.joint_internal_function

val b_fin_adds_graph :
  Joint.graph_params -> AST.ident List.list -> Blocks.bind_fin_block ->
  Graphs.label -> Joint.joint_internal_function ->
  Joint.joint_internal_function

val step_registers :
  Joint.uns_params -> AST.ident List.list -> Joint.joint_step ->
  Registers.register List.list

val fin_step_registers :
  Joint.uns_params -> Joint.joint_fin_step -> Registers.register List.list

type b_graph_translate_data = { init_ret : __; init_params : __;
                                init_stack_size : Nat.nat;
                                added_prologue : Joint.joint_seq List.list;
                                new_regs : Registers.register List.list;
                                f_step : (Graphs.label -> Joint.joint_step ->
                                         Blocks.bind_step_block);
                                f_fin : (Graphs.label -> Joint.joint_fin_step
                                        -> Blocks.bind_fin_block) }

val b_graph_translate_data_rect_Type4 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1

val b_graph_translate_data_rect_Type5 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1

val b_graph_translate_data_rect_Type3 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1

val b_graph_translate_data_rect_Type2 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1

val b_graph_translate_data_rect_Type1 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1

val b_graph_translate_data_rect_Type0 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1

val init_ret :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> __

val init_params :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> __

val init_stack_size :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Nat.nat

val added_prologue :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Joint.joint_seq List.list

val new_regs :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Registers.register List.list

val f_step :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Graphs.label -> Joint.joint_step ->
  Blocks.bind_step_block

val f_fin :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Graphs.label -> Joint.joint_fin_step ->
  Blocks.bind_fin_block

val b_graph_translate_data_inv_rect_Type4 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_data_inv_rect_Type3 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_data_inv_rect_Type2 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_data_inv_rect_Type1 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_data_inv_rect_Type0 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_data_jmdiscr :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> b_graph_translate_data -> __

type bound_b_graph_translate_data =
  (Registers.register, b_graph_translate_data) Bind_new.bind_new Types.sig0

val get_first_costlabel_next :
  Joint.params -> AST.ident List.list -> Joint.joint_closed_internal_function
  -> (CostLabel.costlabel, __) Types.prod

val get_first_costlabel :
  Joint.params -> AST.ident List.list -> Joint.joint_closed_internal_function
  -> CostLabel.costlabel

val not_emptyb : 'a1 List.list -> Bool.bool

val b_graph_translate_props_rect_Type4 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Joint.joint_closed_internal_function ->
  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_props_rect_Type5 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Joint.joint_closed_internal_function ->
  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_props_rect_Type3 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Joint.joint_closed_internal_function ->
  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_props_rect_Type2 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Joint.joint_closed_internal_function ->
  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_props_rect_Type1 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Joint.joint_closed_internal_function ->
  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_props_rect_Type0 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Joint.joint_closed_internal_function ->
  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_props_inv_rect_Type4 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Joint.joint_closed_internal_function ->
  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_props_inv_rect_Type3 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Joint.joint_closed_internal_function ->
  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_props_inv_rect_Type2 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Joint.joint_closed_internal_function ->
  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_props_inv_rect_Type1 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Joint.joint_closed_internal_function ->
  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_props_inv_rect_Type0 :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Joint.joint_closed_internal_function ->
  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val b_graph_translate_props_jmdiscr :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  b_graph_translate_data -> Joint.joint_closed_internal_function ->
  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
  List.list) -> (Graphs.label -> Registers.register List.list) -> __

val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod

val set_entry :
  AST.ident List.list -> Joint.params -> Joint.joint_internal_function -> __
  -> Joint.joint_internal_function

val b_graph_translate :
  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
  bound_b_graph_translate_data -> Joint.joint_closed_internal_function ->
  Joint.joint_closed_internal_function Types.sig0

val b_graph_transform_program :
  Joint.graph_params -> Joint.graph_params -> (AST.ident List.list ->
  Joint.joint_closed_internal_function -> bound_b_graph_translate_data) ->
  Joint.joint_program -> Joint.joint_program

val added_registers :
  Joint.graph_params -> AST.ident List.list -> Joint.joint_internal_function
  -> (Graphs.label -> Registers.register List.list) -> Registers.register
  List.list