source: extracted/compiler.ml @ 2620

open Preamble

open CostLabel

open Proper

open PositiveMap

open Deqsets

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Lists

open Positive

open Identifiers

open Coqlib

open Floats

open Arithmetic

open Char

open String

open Vector

open Div_and_mod

open Jmeq

open Russell

open List

open Util

open FoldStuff

open BitVector

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 CexecSound

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 Initialisation

open BitVectorTrie

open Graphs

open Order

open Registers

open RTLabs_syntax

open ToRTLabs

(** val front_end :
    Csyntax.clight_program -> ((CostLabel.costlabel, Csyntax.clight_program)
    Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res **)
let front_end p =
  let p0 = SwitchRemoval.program_switch_removal p in
  let { Types.fst = p'; Types.snd = init_cost } = Label.clight_label p0 in
  let p3 = SimplifyCasts.simplify_program p' in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (ToCminor.clight_to_cminor p3)) (fun p4 ->
      let p5 = ToRTLabs.cminor_to_rtlabs init_cost p4 in
      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
        init_cost; Types.snd = p' }; Types.snd = p5 }))

open LabelledObjects

open ASM

(** val back_end :
    RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program **)
let back_end x =
  failwith "AXIOM TO BE REALIZED"

type object_code = BitVector.byte List.list

type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie

(** val assembler :
    ASM.pseudo_assembly_program -> (object_code, costlabel_map) Types.prod
    Errors.res **)
let assembler x =
  failwith "AXIOM TO BE REALIZED"

open StructuredTraces

open AbstractStatus

open Status

open StatusProofs

open Interpret

open Fetch

open ASMCosts

(** val lift_cost_map_back_to_front :
    Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
    CostLabel.costlabel BitVectorTrie.bitVectorTrie -> (CostLabel.costlabel
    -> (__, __) Types.sum) -> StructuredTraces.as_cost_map ->
    Label.clight_cost_map **)
let lift_cost_map_back_to_front clight code_memory lbls dec k asm_cost_map =
  StructuredTraces.lift_sigma_map_id Nat.O dec k asm_cost_map

open UtilBranch

open ASMCostsSplit

(** val compile :
    Csyntax.clight_program -> ((object_code, costlabel_map) Types.prod,
    (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
    Errors.res **)
let compile p =
  Obj.magic
    (Monad.m_bind3 (Monad.max_def Errors.res0) (Obj.magic (front_end p))
      (fun init_cost p' p0 ->
      let p3 = back_end p0 in
      Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p3))
        (fun p4 ->
        let k = ASMCostsSplit.aSM_cost_map p4 in
        let k' =
          lift_cost_map_back_to_front p'
            (Fetch.load_code_memory p4.Types.fst) p4.Types.snd (assert false
            (* absurd case *)) k
        in
        Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = p4;
          Types.snd = { Types.dpi1 = p'; Types.dpi2 = k' } })))