source: extracted/compiler.ml @ 2717

open Preamble

open BitVectorTrie

open CostLabel

open Coqlib

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Lists

open Positive

open Identifiers

open Exp

open Arithmetic

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 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 Deqsets

open State

open Bind_new

open BindLists

open Blocks

open TranslateUtils

open AssocList

open String

open LabelledObjects

open I8051

open BackEndOps

open Joint

open RTL

open RTLabsToRTL

open ERTL

open RegisterSet

open RTLToERTL

open ERTLptr

open ERTLToERTLptr

open Fixpoints

open Set_adt

open Liveness

open Interference

open Joint_LTL_LIN

open LTL

open ERTLptrToLTL

open LIN

open Linearise

open LTLToLIN

open ASM

open BitVectorTrieSet

open LINToASM

(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
let compute_fixpoint _ =
  failwith "AXIOM TO BE REALIZED"

(** val colour_graph : Interference.coloured_graph_computer **)
let colour_graph _ =
  failwith "AXIOM TO BE REALIZED"

(** val back_end :
    RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program **)
let back_end p =
  let p0 = RTLabsToRTL.rtlabs_to_rtl p in
  let p3 = RTLToERTL.rtl_to_ertl p0 in
  let p4 = ERTLToERTLptr.ertl_to_ertlptr p3 in
  let p5 = ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p4 in
  let p6 = LTLToLIN.ltl_to_lin p5 in LINToASM.lin_to_asm p6

type object_code = BitVector.byte List.list

type costlabel_map1 = CostLabel.costlabel BitVectorTrie.bitVectorTrie

open Assembly

open Status

open Fetch

open PolicyFront

open PolicyStep

open Policy

(** val assembler :
    ASM.pseudo_assembly_program -> (object_code, costlabel_map1) Types.prod
    Errors.res **)
let assembler p =
  let { Types.fst = preamble0; Types.snd = list_instr } = p in
  let p' = { Types.fst = preamble0; Types.snd = list_instr } in
  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' (Types.coerc_pair_sigma p'))))
      (fun sigma_pol ->
      let sigma0 = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
      Obj.magic (Errors.OK (Types.pi1 (Assembly.assembly p sigma0 pol)))))

open StructuredTraces

open AbstractStatus

open StatusProofs

open Interpret

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_map1) 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' } })))