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 Label

open Sets

open Listb

open Star

open Frontend_misc

open CexecInd

open Casts

open ClassifyOp

open Smallstep

open Extra_bool

open FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

open Globalenvs

open Csem

open SmallstepExec

open Division

open Z

open BitVectorZ

open Pointers

open Values

open Events

open IOMonad

open IO

open Cexec

open TypeComparison

open SimplifyCasts

open MemProperties

open MemoryInjections

open Fresh

open SwitchRemoval

open FrontEndOps

open Cminor_syntax

open ToCminor

open BitVectorTrie

open Graphs

open Order

open Registers

open RTLabs_syntax

open ToRTLabs

open Deqsets_extra

open CostMisc

open Listb_extra

open CostSpec

open CostCheck

open CostInj

open State

open Bind_new

open BindLists

open Blocks

open TranslateUtils

open String

open LabelledObjects

open I8051

open BackEndOps

open Joint

open RTL

open RTLabsToRTL

open ERTL

open RegisterSet

open RTLToERTL

open Fixpoints

open Set_adt

open Liveness

open Interference

open Joint_LTL_LIN

open LTL

open ERTLToLTL

open LIN

open Linearise

open LTLToLIN

open ASM

open BitVectorTrieSet

open LINToASM

type pass =
| Clight_pass
| Clight_switch_removed_pass
| Clight_label_pass
| Clight_simplified_pass
| Cminor_pass
| Rtlabs_pass
| Rtl_separate_pass
| Rtl_uniq_pass
| Ertl_pass
| Ltl_pass
| Lin_pass
| Assembly_pass
| Object_code_pass

(** val pass_rect_Type4 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> pass -> 'a1 **)
let rec pass_rect_Type4 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
| Clight_pass -> h_clight_pass
| Clight_switch_removed_pass -> h_clight_switch_removed_pass
| Clight_label_pass -> h_clight_label_pass
| Clight_simplified_pass -> h_clight_simplified_pass
| Cminor_pass -> h_cminor_pass
| Rtlabs_pass -> h_rtlabs_pass
| Rtl_separate_pass -> h_rtl_separate_pass
| Rtl_uniq_pass -> h_rtl_uniq_pass
| Ertl_pass -> h_ertl_pass
| Ltl_pass -> h_ltl_pass
| Lin_pass -> h_lin_pass
| Assembly_pass -> h_assembly_pass
| Object_code_pass -> h_object_code_pass

(** val pass_rect_Type5 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> pass -> 'a1 **)
let rec pass_rect_Type5 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
| Clight_pass -> h_clight_pass
| Clight_switch_removed_pass -> h_clight_switch_removed_pass
| Clight_label_pass -> h_clight_label_pass
| Clight_simplified_pass -> h_clight_simplified_pass
| Cminor_pass -> h_cminor_pass
| Rtlabs_pass -> h_rtlabs_pass
| Rtl_separate_pass -> h_rtl_separate_pass
| Rtl_uniq_pass -> h_rtl_uniq_pass
| Ertl_pass -> h_ertl_pass
| Ltl_pass -> h_ltl_pass
| Lin_pass -> h_lin_pass
| Assembly_pass -> h_assembly_pass
| Object_code_pass -> h_object_code_pass

(** val pass_rect_Type3 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> pass -> 'a1 **)
let rec pass_rect_Type3 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
| Clight_pass -> h_clight_pass
| Clight_switch_removed_pass -> h_clight_switch_removed_pass
| Clight_label_pass -> h_clight_label_pass
| Clight_simplified_pass -> h_clight_simplified_pass
| Cminor_pass -> h_cminor_pass
| Rtlabs_pass -> h_rtlabs_pass
| Rtl_separate_pass -> h_rtl_separate_pass
| Rtl_uniq_pass -> h_rtl_uniq_pass
| Ertl_pass -> h_ertl_pass
| Ltl_pass -> h_ltl_pass
| Lin_pass -> h_lin_pass
| Assembly_pass -> h_assembly_pass
| Object_code_pass -> h_object_code_pass

(** val pass_rect_Type2 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> pass -> 'a1 **)
let rec pass_rect_Type2 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
| Clight_pass -> h_clight_pass
| Clight_switch_removed_pass -> h_clight_switch_removed_pass
| Clight_label_pass -> h_clight_label_pass
| Clight_simplified_pass -> h_clight_simplified_pass
| Cminor_pass -> h_cminor_pass
| Rtlabs_pass -> h_rtlabs_pass
| Rtl_separate_pass -> h_rtl_separate_pass
| Rtl_uniq_pass -> h_rtl_uniq_pass
| Ertl_pass -> h_ertl_pass
| Ltl_pass -> h_ltl_pass
| Lin_pass -> h_lin_pass
| Assembly_pass -> h_assembly_pass
| Object_code_pass -> h_object_code_pass

(** val pass_rect_Type1 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> pass -> 'a1 **)
let rec pass_rect_Type1 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
| Clight_pass -> h_clight_pass
| Clight_switch_removed_pass -> h_clight_switch_removed_pass
| Clight_label_pass -> h_clight_label_pass
| Clight_simplified_pass -> h_clight_simplified_pass
| Cminor_pass -> h_cminor_pass
| Rtlabs_pass -> h_rtlabs_pass
| Rtl_separate_pass -> h_rtl_separate_pass
| Rtl_uniq_pass -> h_rtl_uniq_pass
| Ertl_pass -> h_ertl_pass
| Ltl_pass -> h_ltl_pass
| Lin_pass -> h_lin_pass
| Assembly_pass -> h_assembly_pass
| Object_code_pass -> h_object_code_pass

(** val pass_rect_Type0 :
    'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
    -> 'a1 -> 'a1 -> pass -> 'a1 **)
let rec pass_rect_Type0 h_clight_pass h_clight_switch_removed_pass h_clight_label_pass h_clight_simplified_pass h_cminor_pass h_rtlabs_pass h_rtl_separate_pass h_rtl_uniq_pass h_ertl_pass h_ltl_pass h_lin_pass h_assembly_pass h_object_code_pass = function
| Clight_pass -> h_clight_pass
| Clight_switch_removed_pass -> h_clight_switch_removed_pass
| Clight_label_pass -> h_clight_label_pass
| Clight_simplified_pass -> h_clight_simplified_pass
| Cminor_pass -> h_cminor_pass
| Rtlabs_pass -> h_rtlabs_pass
| Rtl_separate_pass -> h_rtl_separate_pass
| Rtl_uniq_pass -> h_rtl_uniq_pass
| Ertl_pass -> h_ertl_pass
| Ltl_pass -> h_ltl_pass
| Lin_pass -> h_lin_pass
| Assembly_pass -> h_assembly_pass
| Object_code_pass -> h_object_code_pass

(** val pass_inv_rect_Type4 :
    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let pass_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
  let hcut = pass_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
  in
  hcut __

(** val pass_inv_rect_Type3 :
    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let pass_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
  let hcut = pass_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
  in
  hcut __

(** val pass_inv_rect_Type2 :
    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let pass_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
  let hcut = pass_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
  in
  hcut __

(** val pass_inv_rect_Type1 :
    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let pass_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
  let hcut = pass_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
  in
  hcut __

(** val pass_inv_rect_Type0 :
    pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__
    -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
    (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let pass_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 =
  let hcut = pass_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 hterm
  in
  hcut __

(** val pass_discr : pass -> pass -> __ **)
let pass_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Clight_pass -> Obj.magic (fun _ dH -> dH)
     | Clight_switch_removed_pass -> Obj.magic (fun _ dH -> dH)
     | Clight_label_pass -> Obj.magic (fun _ dH -> dH)
     | Clight_simplified_pass -> Obj.magic (fun _ dH -> dH)
     | Cminor_pass -> Obj.magic (fun _ dH -> dH)
     | Rtlabs_pass -> Obj.magic (fun _ dH -> dH)
     | Rtl_separate_pass -> Obj.magic (fun _ dH -> dH)
     | Rtl_uniq_pass -> Obj.magic (fun _ dH -> dH)
     | Ertl_pass -> Obj.magic (fun _ dH -> dH)
     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
     | Lin_pass -> Obj.magic (fun _ dH -> dH)
     | Assembly_pass -> Obj.magic (fun _ dH -> dH)
     | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y

(** val pass_jmdiscr : pass -> pass -> __ **)
let pass_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | Clight_pass -> Obj.magic (fun _ dH -> dH)
     | Clight_switch_removed_pass -> Obj.magic (fun _ dH -> dH)
     | Clight_label_pass -> Obj.magic (fun _ dH -> dH)
     | Clight_simplified_pass -> Obj.magic (fun _ dH -> dH)
     | Cminor_pass -> Obj.magic (fun _ dH -> dH)
     | Rtlabs_pass -> Obj.magic (fun _ dH -> dH)
     | Rtl_separate_pass -> Obj.magic (fun _ dH -> dH)
     | Rtl_uniq_pass -> Obj.magic (fun _ dH -> dH)
     | Ertl_pass -> Obj.magic (fun _ dH -> dH)
     | Ltl_pass -> Obj.magic (fun _ dH -> dH)
     | Lin_pass -> Obj.magic (fun _ dH -> dH)
     | Assembly_pass -> Obj.magic (fun _ dH -> dH)
     | Object_code_pass -> Obj.magic (fun _ dH -> dH)) y

type 'x with_stack_model = ('x, AST.ident -> Nat.nat Types.option) Types.prod

type syntax_of_pass = __

type observe_pass = pass -> syntax_of_pass -> Types.unit0

(** val front_end :
    observe_pass -> Csyntax.clight_program -> ((CostLabel.costlabel,
    Csyntax.clight_program) Types.prod, RTLabs_syntax.rTLabs_program)
    Types.prod Errors.res **)
let front_end observe p =
  let i = Obj.magic observe Clight_pass p in
  let p0 = SwitchRemoval.program_switch_removal p in
  let i0 = Obj.magic observe Clight_switch_removed_pass p0 in
  let { Types.fst = p'; Types.snd = init_cost } = Label.clight_label p0 in
  let i1 = Obj.magic observe Clight_label_pass p' in
  let p1 = SimplifyCasts.simplify_program p' in
  let i2 = Obj.magic observe Clight_simplified_pass p1 in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (ToCminor.clight_to_cminor p1)) (fun p2 ->
      let i3 = observe Cminor_pass p2 in
      let p3 = ToRTLabs.cminor_to_rtlabs (Obj.magic p2) in
      let i4 = Obj.magic observe Rtlabs_pass p3 in
      Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic (CostCheck.check_cost_program_prf p3)) (fun _ ->
        Monad.m_bind0 (Monad.max_def Errors.res0)
          (Obj.magic (CostInj.check_program_cost_injectivity_prf p3))
          (fun _ ->
          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
            { Types.fst = init_cost; Types.snd = p' }; Types.snd = p3 }))))

open Uses

(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
let compute_fixpoint = Compute_fixpoints.compute_fixpoint
 
(** val colour_graph : Interference.coloured_graph_computer **)
let colour_graph = Compute_colouring.colour_graph
 
open AssocList

(** val lookup_stack_cost :
    Joint.params -> Joint.joint_program -> PreIdentifiers.identifier ->
    Nat.nat Types.option **)
let lookup_stack_cost p p0 id =
  AssocList.assoc_list_lookup id
    (Identifiers.eq_identifier PreIdentifiers.SymbolTag)
    (Joint.stack_cost p p0)

(** val back_end :
    observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
    (((ASM.pseudo_assembly_program, CostLabel.costlabel) Types.prod,
    Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res **)
let back_end observe init_cost p =
  let p0 = RTLabsToRTL.rtlabs_to_rtl init_cost p in
  let st = lookup_stack_cost (Joint.graph_params_to_params RTL.rTL) p0 in
  let i =
    Obj.magic observe Rtl_separate_pass { Types.fst = p0; Types.snd = st }
  in
  let i0 = Obj.magic observe Rtl_uniq_pass { Types.fst = p0; Types.snd = st }
  in
  let p1 = RTLToERTL.rtl_to_ertl p0 in
  let st0 = lookup_stack_cost (Joint.graph_params_to_params ERTL.eRTL) p1 in
  let i1 = Obj.magic observe Ertl_pass { Types.fst = p1; Types.snd = st0 } in
  let { Types.fst = eta2; Types.snd = max_stack } =
    ERTLToLTL.ertl_to_ltl compute_fixpoint colour_graph p1
  in
  let { Types.fst = p2; Types.snd = stack_cost } = eta2 in
  let st1 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p2 in
  let i2 = Obj.magic observe Ltl_pass { Types.fst = p2; Types.snd = st1 } in
  let st2 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p2 in
  let p3 = LTLToLIN.ltl_to_lin p2 in
  let st3 = lookup_stack_cost (Joint.lin_params_to_params LIN.lIN) p3 in
  let i3 = Obj.magic observe Lin_pass { Types.fst = p3; Types.snd = st3 } in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic
        (Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
          (LINToASM.lin_to_asm p3))) (fun p4 ->
      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
        { Types.fst = p4; Types.snd = init_cost }; Types.snd = stack_cost };
        Types.snd = max_stack }))

open Assembly

open Status

open Fetch

open PolicyFront

open PolicyStep

open Policy

(** val assembler :
    observe_pass -> ASM.pseudo_assembly_program -> ASM.labelled_object_code
    Errors.res **)
let assembler observe p =
prerr_endline "Y1";
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic
        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
          (Policy.jump_expansion' p))) (fun sigma_pol ->
prerr_endline "Y2";
      let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
      let i =
        Obj.magic observe Assembly_pass { Types.fst = { Types.fst = p;
          Types.snd = sigma }; Types.snd = pol }
      in
prerr_endline "Y3";
      let p0 = Assembly.assembly p sigma pol in
prerr_endline "Y4";
      let i0 = Obj.magic observe Object_code_pass (Types.pi1 p0) in
prerr_endline "Y5";
      Obj.magic (Errors.OK (Types.pi1 p0))))

open StructuredTraces

open AbstractStatus

open StatusProofs

open Interpret

open ASMCosts

(** val lift_out_of_sigma :
    'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1 ->
    'a2 **)
let lift_out_of_sigma dflt dec m a_sig =
  match dec a_sig with
  | Types.Inl _ -> m a_sig
  | Types.Inr _ -> dflt

(** val lift_cost_map_back_to_front :
    ASM.labelled_object_code -> StructuredTraces.as_cost_map ->
    Label.clight_cost_map **)
let lift_cost_map_back_to_front oc asm_cost_map =
  lift_out_of_sigma Nat.O
    (Obj.magic
      (BitVectorTrie.strong_decidable_in_codomain
        (Identifiers.deq_identifier PreIdentifiers.CostTag) (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))))))))))))))))
        (Obj.magic oc.ASM.costlabels))) asm_cost_map

open UtilBranch

open ASMCostsSplit

type compiler_output = { c_labelled_object_code : ASM.labelled_object_code;
                         c_stack_cost : Joint.stack_cost_model;
                         c_max_stack : Nat.nat;
                         c_init_costlabel : CostLabel.costlabel;
                         c_labelled_clight : Csyntax.clight_program;
                         c_clight_cost_map : Label.clight_cost_map }

(** val compiler_output_rect_Type4 :
    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
    'a1) -> compiler_output -> 'a1 **)
let rec compiler_output_rect_Type4 h_mk_compiler_output x_185 =
  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
    c_clight_cost_map = c_clight_cost_map0 } = x_185
  in
  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0

(** val compiler_output_rect_Type5 :
    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
    'a1) -> compiler_output -> 'a1 **)
let rec compiler_output_rect_Type5 h_mk_compiler_output x_187 =
  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
    c_clight_cost_map = c_clight_cost_map0 } = x_187
  in
  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0

(** val compiler_output_rect_Type3 :
    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
    'a1) -> compiler_output -> 'a1 **)
let rec compiler_output_rect_Type3 h_mk_compiler_output x_189 =
  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
    c_clight_cost_map = c_clight_cost_map0 } = x_189
  in
  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0

(** val compiler_output_rect_Type2 :
    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
    'a1) -> compiler_output -> 'a1 **)
let rec compiler_output_rect_Type2 h_mk_compiler_output x_191 =
  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
    c_clight_cost_map = c_clight_cost_map0 } = x_191
  in
  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0

(** val compiler_output_rect_Type1 :
    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
    'a1) -> compiler_output -> 'a1 **)
let rec compiler_output_rect_Type1 h_mk_compiler_output x_193 =
  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
    c_clight_cost_map = c_clight_cost_map0 } = x_193
  in
  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0

(** val compiler_output_rect_Type0 :
    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
    'a1) -> compiler_output -> 'a1 **)
let rec compiler_output_rect_Type0 h_mk_compiler_output x_195 =
  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
    c_clight_cost_map = c_clight_cost_map0 } = x_195
  in
  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0

(** val c_labelled_object_code :
    compiler_output -> ASM.labelled_object_code **)
let rec c_labelled_object_code xxx =
  xxx.c_labelled_object_code

(** val c_stack_cost : compiler_output -> Joint.stack_cost_model **)
let rec c_stack_cost xxx =
  xxx.c_stack_cost

(** val c_max_stack : compiler_output -> Nat.nat **)
let rec c_max_stack xxx =
  xxx.c_max_stack

(** val c_init_costlabel : compiler_output -> CostLabel.costlabel **)
let rec c_init_costlabel xxx =
  xxx.c_init_costlabel

(** val c_labelled_clight : compiler_output -> Csyntax.clight_program **)
let rec c_labelled_clight xxx =
  xxx.c_labelled_clight

(** val c_clight_cost_map : compiler_output -> Label.clight_cost_map **)
let rec c_clight_cost_map xxx =
  xxx.c_clight_cost_map

(** val compiler_output_inv_rect_Type4 :
    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
let compiler_output_inv_rect_Type4 hterm h1 =
  let hcut = compiler_output_rect_Type4 h1 hterm in hcut __

(** val compiler_output_inv_rect_Type3 :
    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
let compiler_output_inv_rect_Type3 hterm h1 =
  let hcut = compiler_output_rect_Type3 h1 hterm in hcut __

(** val compiler_output_inv_rect_Type2 :
    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
let compiler_output_inv_rect_Type2 hterm h1 =
  let hcut = compiler_output_rect_Type2 h1 hterm in hcut __

(** val compiler_output_inv_rect_Type1 :
    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
let compiler_output_inv_rect_Type1 hterm h1 =
  let hcut = compiler_output_rect_Type1 h1 hterm in hcut __

(** val compiler_output_inv_rect_Type0 :
    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
let compiler_output_inv_rect_Type0 hterm h1 =
  let hcut = compiler_output_rect_Type0 h1 hterm in hcut __

(** val compiler_output_jmdiscr :
    compiler_output -> compiler_output -> __ **)
let compiler_output_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
       c_init_costlabel = a3; c_labelled_clight = a4; c_clight_cost_map =
       a5 } = x
     in
    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y

(** val compile :
    observe_pass -> Csyntax.clight_program -> compiler_output Errors.res **)
let compile observe p =
  Obj.magic
    (Monad.m_bind3 (Monad.max_def Errors.res0)
      (Obj.magic (front_end observe p)) (fun init_cost p' p0 ->
      Monad.m_bind3 (Monad.max_def Errors.res0)
        (Obj.magic (back_end observe init_cost p0))
        (fun p_init_costlabel stack_cost max_stack ->
        let { Types.fst = p1; Types.snd = init_costlabel } = p_init_costlabel
        in
        Monad.m_bind0 (Monad.max_def Errors.res0)
          (Obj.magic (assembler observe p1)) (fun p2 ->
          let k = ASMCostsSplit.aSM_cost_map p2 in
          let k' = lift_cost_map_back_to_front p2 k in
          Monad.m_return0 (Monad.max_def Errors.res0)
            { c_labelled_object_code = p2; c_stack_cost = stack_cost;
            c_max_stack = max_stack; c_init_costlabel = init_costlabel;
            c_labelled_clight = p'; c_clight_cost_map = k' }))))