open Preamble

open CostLabel

open Coqlib

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

open Extranat

open Bool

open Relations

open Nat

open Integers

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open AST

open Csyntax

open TypeComparison

open ClassifyOp

open Fresh

val gather_mem_vars_addr : Csyntax.expr -> Identifiers.identifier_set

val gather_mem_vars_expr : Csyntax.expr -> Identifiers.identifier_set

val gather_mem_vars_ls :
  Csyntax.labeled_statements -> Identifiers.identifier_set

val gather_mem_vars_stmt : Csyntax.statement -> Identifiers.identifier_set

type var_type =
| Global of AST.region
| Stack of Nat.nat
| Local

val var_type_rect_Type4 :
  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1

val var_type_rect_Type5 :
  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1

val var_type_rect_Type3 :
  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1

val var_type_rect_Type2 :
  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1

val var_type_rect_Type1 :
  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1

val var_type_rect_Type0 :
  (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1

val var_type_inv_rect_Type4 :
  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
  'a1) -> 'a1

val var_type_inv_rect_Type3 :
  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
  'a1) -> 'a1

val var_type_inv_rect_Type2 :
  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
  'a1) -> 'a1

val var_type_inv_rect_Type1 :
  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
  'a1) -> 'a1

val var_type_inv_rect_Type0 :
  var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
  'a1) -> 'a1

val var_type_discr : var_type -> var_type -> __

val var_type_jmdiscr : var_type -> var_type -> __

type var_types =
  (var_type, Csyntax.type0) Types.prod Identifiers.identifier_map

val lookup' :
  var_types -> PreIdentifiers.identifier -> (var_type, Csyntax.type0)
  Types.prod Errors.res

val always_alloc : Csyntax.type0 -> Bool.bool

val characterise_vars :
  ((AST.ident, AST.region) Types.prod, Csyntax.type0) Types.prod List.list ->
  Csyntax.function0 -> (var_types, Nat.nat) Types.prod

open FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

open Division

open Z

open BitVectorZ

open Pointers

open Values

open FrontEndOps

open Cminor_syntax

val type_should_eq : Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 Errors.res

val region_should_eq : AST.region -> AST.region -> 'a1 -> 'a1 Errors.res

val typ_should_eq : AST.typ -> AST.typ -> 'a1 -> 'a1 Errors.res

val translate_unop :
  AST.typ -> AST.typ -> Csyntax.unary_operation ->
  FrontEndOps.unary_operation Errors.res

val fix_ptr_type :
  Csyntax.type0 -> Nat.nat Types.option -> Cminor_syntax.expr ->
  Cminor_syntax.expr

val translate_add :
  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res

val translate_sub :
  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res

val translate_mul :
  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res

val translate_div :
  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res

val translate_mod :
  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res

val translate_shr :
  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res

val complete_cmp :
  Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res

val translate_cmp :
  Integers.comparison -> Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 ->
  Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res

val translate_misc_aop :
  Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> (AST.intsize ->
  AST.signedness -> FrontEndOps.binary_operation) -> Cminor_syntax.expr ->
  Cminor_syntax.expr -> Cminor_syntax.expr Errors.res

val translate_binop :
  Csyntax.binary_operation -> Csyntax.type0 -> Cminor_syntax.expr ->
  Csyntax.type0 -> Cminor_syntax.expr -> Csyntax.type0 -> Cminor_syntax.expr
  Errors.res

val translate_cast :
  Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr Types.sig0 ->
  Cminor_syntax.expr Types.sig0 Errors.res

val cm_zero : AST.intsize -> AST.signedness -> Cminor_syntax.expr

val cm_one : AST.intsize -> AST.signedness -> Cminor_syntax.expr

val translate_addr :
  var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res

val translate_expr :
  var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res

type destination =
| IdDest of AST.ident
| MemDest of Cminor_syntax.expr Types.sig0

val destination_rect_Type4 :
  var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
  Types.sig0 -> 'a1) -> destination -> 'a1

val destination_rect_Type5 :
  var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
  Types.sig0 -> 'a1) -> destination -> 'a1

val destination_rect_Type3 :
  var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
  Types.sig0 -> 'a1) -> destination -> 'a1

val destination_rect_Type2 :
  var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
  Types.sig0 -> 'a1) -> destination -> 'a1

val destination_rect_Type1 :
  var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
  Types.sig0 -> 'a1) -> destination -> 'a1

val destination_rect_Type0 :
  var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
  Types.sig0 -> 'a1) -> destination -> 'a1

val destination_inv_rect_Type4 :
  var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
  (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1

val destination_inv_rect_Type3 :
  var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
  (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1

val destination_inv_rect_Type2 :
  var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
  (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1

val destination_inv_rect_Type1 :
  var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
  (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1

val destination_inv_rect_Type0 :
  var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
  (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1

val destination_discr :
  var_types -> AST.typ -> destination -> destination -> __

val destination_jmdiscr :
  var_types -> AST.typ -> destination -> destination -> __

val translate_dest : var_types -> Csyntax.expr -> destination Errors.res

type lenv = PreIdentifiers.identifier Identifiers.identifier_map

val lookup_label :
  lenv -> PreIdentifiers.identifier -> PreIdentifiers.identifier Errors.res

type labgen = { labuniverse : Identifiers.universe;
                label_genlist : PreIdentifiers.identifier List.list }

val labgen_rect_Type4 :
  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
  -> labgen -> 'a1

val labgen_rect_Type5 :
  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
  -> labgen -> 'a1

val labgen_rect_Type3 :
  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
  -> labgen -> 'a1

val labgen_rect_Type2 :
  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
  -> labgen -> 'a1

val labgen_rect_Type1 :
  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
  -> labgen -> 'a1

val labgen_rect_Type0 :
  (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> 'a1)
  -> labgen -> 'a1

val labuniverse : labgen -> Identifiers.universe

val label_genlist : labgen -> PreIdentifiers.identifier List.list

val labgen_inv_rect_Type4 :
  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
  __ -> __ -> 'a1) -> 'a1

val labgen_inv_rect_Type3 :
  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
  __ -> __ -> 'a1) -> 'a1

val labgen_inv_rect_Type2 :
  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
  __ -> __ -> 'a1) -> 'a1

val labgen_inv_rect_Type1 :
  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
  __ -> __ -> 'a1) -> 'a1

val labgen_inv_rect_Type0 :
  labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
  __ -> __ -> 'a1) -> 'a1

val labgen_discr : labgen -> labgen -> __

val labgen_jmdiscr : labgen -> labgen -> __

val generate_fresh_label :
  labgen -> (PreIdentifiers.identifier, labgen) Types.prod Types.sig0

val labels_defined_switch : Csyntax.labeled_statements -> AST.ident List.list

val labels_defined : Csyntax.statement -> AST.ident List.list

val m_option_map :
  ('a1 -> 'a2 Errors.res) -> 'a1 Types.option -> 'a2 Types.option Errors.res

val translate_expr_sigma :
  var_types -> Csyntax.expr -> (AST.typ, Cminor_syntax.expr) Types.dPair
  Types.sig0 Errors.res

val add_tmps :
  var_types -> (AST.ident, Csyntax.type0) Types.prod List.list -> var_types

type tmpgen = { tmp_universe : Identifiers.universe;
                tmp_env : (AST.ident, Csyntax.type0) Types.prod List.list }

val tmpgen_rect_Type4 :
  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1

val tmpgen_rect_Type5 :
  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1

val tmpgen_rect_Type3 :
  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1

val tmpgen_rect_Type2 :
  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1

val tmpgen_rect_Type1 :
  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1

val tmpgen_rect_Type0 :
  var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) Types.prod
  List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1

val tmp_universe : var_types -> tmpgen -> Identifiers.universe

val tmp_env :
  var_types -> tmpgen -> (AST.ident, Csyntax.type0) Types.prod List.list

val tmpgen_inv_rect_Type4 :
  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1

val tmpgen_inv_rect_Type3 :
  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1

val tmpgen_inv_rect_Type2 :
  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1

val tmpgen_inv_rect_Type1 :
  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1

val tmpgen_inv_rect_Type0 :
  var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
  Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1

val tmpgen_discr : var_types -> tmpgen -> tmpgen -> __

val tmpgen_jmdiscr : var_types -> tmpgen -> tmpgen -> __

val alloc_tmp :
  var_types -> Csyntax.type0 -> tmpgen -> (AST.ident, tmpgen) Types.prod

val mklabels :
  labgen -> ((PreIdentifiers.identifier, PreIdentifiers.identifier)
  Types.prod, labgen) Types.prod

type convert_flag =
| DoNotConvert
| ConvertTo of PreIdentifiers.identifier * PreIdentifiers.identifier

val convert_flag_rect_Type4 :
  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
  convert_flag -> 'a1

val convert_flag_rect_Type5 :
  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
  convert_flag -> 'a1

val convert_flag_rect_Type3 :
  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
  convert_flag -> 'a1

val convert_flag_rect_Type2 :
  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
  convert_flag -> 'a1

val convert_flag_rect_Type1 :
  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
  convert_flag -> 'a1

val convert_flag_rect_Type0 :
  'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
  convert_flag -> 'a1

val convert_flag_inv_rect_Type4 :
  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1

val convert_flag_inv_rect_Type3 :
  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1

val convert_flag_inv_rect_Type2 :
  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1

val convert_flag_inv_rect_Type1 :
  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1

val convert_flag_inv_rect_Type0 :
  convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
  PreIdentifiers.identifier -> __ -> 'a1) -> 'a1

val convert_flag_discr : convert_flag -> convert_flag -> __

val convert_flag_jmdiscr : convert_flag -> convert_flag -> __

val labels_of_flag : convert_flag -> PreIdentifiers.identifier List.list

val translate_statement :
  var_types -> tmpgen -> labgen -> lenv -> convert_flag -> AST.typ
  Types.option -> Csyntax.statement -> ((tmpgen, labgen) Types.prod,
  Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res

val alloc_params_main :
  var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag -> AST.typ
  Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list ->
  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 ->
  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0
  Errors.res

val alloc_params :
  var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag -> AST.typ
  Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list ->
  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0 ->
  ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod Types.sig0
  Errors.res

val populate_lenv :
  AST.ident List.list -> labgen -> lenv -> (lenv Types.sig0, labgen)
  Types.prod Errors.res

val build_label_env :
  Csyntax.statement -> (lenv Types.sig0, labgen) Types.prod Errors.res

val translate_function :
  Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0)
  Types.prod List.list -> Csyntax.function0 ->
  Cminor_syntax.internal_function Errors.res

val translate_fundef :
  Identifiers.universe -> ((AST.ident, AST.region) Types.prod, Csyntax.type0)
  Types.prod List.list -> Csyntax.clight_fundef ->
  Cminor_syntax.internal_function AST.fundef Errors.res

val map_partial_All :
  ('a1 -> __ -> 'a2 Errors.res) -> 'a1 List.list -> 'a2 List.list Errors.res

val clight_to_cminor :
  Csyntax.clight_program -> Cminor_syntax.cminor_program Errors.res