open Preamble

open UtilBranch

open ASMCostsSplit

open StructuredTraces

open AbstractStatus

open StatusProofs

open Interpret

open ASMCosts

open Status

open Fetch

open Assembly

open PolicyFront

open PolicyStep

open Policy

open AssocList

open Uses

open ASM

open BitVectorTrieSet

open LINToASM

open LIN

open Linearise

open LTLToLIN

open Fixpoints

open Set_adt

open Liveness

open Interference

open Joint_LTL_LIN

open LTL

open ERTLToLTL

open ERTL

open RegisterSet

open RTLToERTL

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 CostInj

open Deqsets_extra

open CostMisc

open Listb_extra

open CostSpec

open CostCheck

open BitVectorTrie

open Graphs

open Order

open Registers

open RTLabs_syntax

open ToRTLabs

open FrontEndOps

open Cminor_syntax

open ToCminor

open MemProperties

open MemoryInjections

open Fresh

open SwitchRemoval

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

open Stacksize

open Executions

open Measurable

open Clight_abstract

open Clight_classified_system

open Cminor_semantics

open Cminor_abstract

open Cminor_classified_system

open RTLabs_semantics

open RTLabs_abstract

open RTLabs_classified_system

open ExtraMonads

open ExtraGlobalenvs

open I8051bis

open BEMem

open Joint_semantics

open SemanticsUtils

open Traces

open Joint_fullexec

open RTL_semantics

open ERTL_semantics

open Joint_LTL_LIN_semantics

open LTL_semantics

open LIN_semantics

open Interpret2

type preclassified_system_pass =
  Measurable.preclassified_system
  (* singleton inductive, whose constructor was mk_preclassified_system_pass *)

(** val preclassified_system_pass_rect_Type4 :
    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    preclassified_system_pass -> 'a1 **)
let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_3 =
  let pcs_pcs = x_3 in h_mk_preclassified_system_pass pcs_pcs __

(** val preclassified_system_pass_rect_Type5 :
    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    preclassified_system_pass -> 'a1 **)
let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_5 =
  let pcs_pcs = x_5 in h_mk_preclassified_system_pass pcs_pcs __

(** val preclassified_system_pass_rect_Type3 :
    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    preclassified_system_pass -> 'a1 **)
let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_7 =
  let pcs_pcs = x_7 in h_mk_preclassified_system_pass pcs_pcs __

(** val preclassified_system_pass_rect_Type2 :
    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    preclassified_system_pass -> 'a1 **)
let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_9 =
  let pcs_pcs = x_9 in h_mk_preclassified_system_pass pcs_pcs __

(** val preclassified_system_pass_rect_Type1 :
    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    preclassified_system_pass -> 'a1 **)
let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_11 =
  let pcs_pcs = x_11 in h_mk_preclassified_system_pass pcs_pcs __

(** val preclassified_system_pass_rect_Type0 :
    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    preclassified_system_pass -> 'a1 **)
let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_13 =
  let pcs_pcs = x_13 in h_mk_preclassified_system_pass pcs_pcs __

(** val pcs_pcs :
    Compiler.pass -> preclassified_system_pass ->
    Measurable.preclassified_system **)
let rec pcs_pcs p xxx =
  let yyy = xxx in yyy

(** val preclassified_system_pass_inv_rect_Type4 :
    Compiler.pass -> preclassified_system_pass ->
    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
let preclassified_system_pass_inv_rect_Type4 x1 hterm h1 =
  let hcut = preclassified_system_pass_rect_Type4 x1 h1 hterm in hcut __

(** val preclassified_system_pass_inv_rect_Type3 :
    Compiler.pass -> preclassified_system_pass ->
    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
let preclassified_system_pass_inv_rect_Type3 x1 hterm h1 =
  let hcut = preclassified_system_pass_rect_Type3 x1 h1 hterm in hcut __

(** val preclassified_system_pass_inv_rect_Type2 :
    Compiler.pass -> preclassified_system_pass ->
    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
let preclassified_system_pass_inv_rect_Type2 x1 hterm h1 =
  let hcut = preclassified_system_pass_rect_Type2 x1 h1 hterm in hcut __

(** val preclassified_system_pass_inv_rect_Type1 :
    Compiler.pass -> preclassified_system_pass ->
    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
let preclassified_system_pass_inv_rect_Type1 x1 hterm h1 =
  let hcut = preclassified_system_pass_rect_Type1 x1 h1 hterm in hcut __

(** val preclassified_system_pass_inv_rect_Type0 :
    Compiler.pass -> preclassified_system_pass ->
    (Measurable.preclassified_system -> __ -> __ -> 'a1) -> 'a1 **)
let preclassified_system_pass_inv_rect_Type0 x1 hterm h1 =
  let hcut = preclassified_system_pass_rect_Type0 x1 h1 hterm in hcut __

(** val pcs_pcs__o__pcs_exec :
    Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
    SmallstepExec.fullexec **)
let pcs_pcs__o__pcs_exec x0 x1 =
  (pcs_pcs x0 x1).Measurable.pcs_exec

(** val pcs_pcs__o__pcs_exec__o__es1 :
    Compiler.pass -> preclassified_system_pass -> (IO.io_out, IO.io_in)
    SmallstepExec.trans_system **)
let pcs_pcs__o__pcs_exec__o__es1 x0 x1 =
  Measurable.pcs_exec__o__es1 (pcs_pcs x0 x1)

(** val preclassified_system_of_pass :
    Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass **)
let preclassified_system_of_pass = function
| Compiler.Clight_pass -> (fun x -> Clight_classified_system.clight_pcs)
| Compiler.Clight_switch_removed_pass ->
  (fun x -> Clight_classified_system.clight_pcs)
| Compiler.Clight_label_pass ->
  (fun x -> Clight_classified_system.clight_pcs)
| Compiler.Clight_simplified_pass ->
  (fun x -> Clight_classified_system.clight_pcs)
| Compiler.Cminor_pass -> (fun x -> Cminor_classified_system.cminor_pcs)
| Compiler.Rtlabs_pass -> (fun x -> RTLabs_classified_system.rTLabs_pcs)
| Compiler.Rtl_separate_pass ->
  (fun x ->
    Joint_fullexec.joint_preclassified_system
      (SemanticsUtils.sem_graph_params_to_sem_params
        RTL_semantics.rTL_semantics_separate))
| Compiler.Rtl_uniq_pass ->
  (fun x ->
    Joint_fullexec.joint_preclassified_system
      (SemanticsUtils.sem_graph_params_to_sem_params
        RTL_semantics.rTL_semantics_unique))
| Compiler.Ertl_pass ->
  (fun x ->
    Joint_fullexec.joint_preclassified_system
      (SemanticsUtils.sem_graph_params_to_sem_params
        ERTL_semantics.eRTL_semantics))
| Compiler.Ltl_pass ->
  (fun x ->
    Joint_fullexec.joint_preclassified_system
      (SemanticsUtils.sem_graph_params_to_sem_params
        LTL_semantics.lTL_semantics))
| Compiler.Lin_pass ->
  (fun x ->
    Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics)
| Compiler.Assembly_pass ->
  (fun prog ->
    let { Types.fst = eta4; Types.snd = policy } = Obj.magic prog in
    let { Types.fst = code; Types.snd = sigma } = eta4 in
    Interpret2.aSM_preclassified_system code sigma policy)
| Compiler.Object_code_pass ->
  (fun prog -> Interpret2.oC_preclassified_system (Obj.magic prog))

(** val run_and_print :
    Compiler.pass -> Compiler.syntax_of_pass -> Nat.nat -> (Compiler.pass ->
    Types.unit0) -> (StructuredTraces.intensional_event -> Types.unit0) ->
    (Errors.errmsg -> Types.unit0) -> (Integers.int -> Types.unit0) ->
    Types.unit0 **)
let run_and_print pass prog n print_pass print_event print_error print_exit =
  let res =
    let pcs = preclassified_system_of_pass pass prog in
    let prog0 = prog in
    let g = (pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0
    in
    Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic
        ((pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_initial_state
          prog0)) (fun s0 ->
      let i = print_pass pass in
      let { Types.fst = trace; Types.snd = res } =
        Measurable.observe_all_in_measurable n
          (Measurable.pcs_to_cs (pcs_pcs pass pcs)
            ((pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0))
          print_event List.Nil s0
      in
      Obj.magic res)
  in
  (match Obj.magic res with
   | Errors.OK n0 -> print_exit n0
   | Errors.Error msg -> print_error msg)