open Preamble

open Fetch

open Hide

open Division

open Z

open BitVectorZ

open Pointers

open Coqlib

open Values

open Events

open IOMonad

open IO

open Sets

open Listb

open StructuredTraces

open AbstractStatus

open BitVectorTrie

open String

open Exp

open Arithmetic

open Vector

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open LabelledObjects

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Div_and_mod

open Util

open List

open Lists

open Bool

open Relations

open Nat

open Positive

open Identifiers

open CostLabel

open ASM

open Types

open Hints_declaration

open Core_notation

open Pts

open Logic

open Jmeq

open Russell

open Status

open StatusProofs

open Interpret

open ASMCosts

open Stacksize

open SmallstepExec

open Executions

open Measurable

(** val mk_trans_system_of_abstract_status :
    StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
    (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
let mk_trans_system_of_abstract_status s as_eval =
  { SmallstepExec.is_final = (fun x -> s.StructuredTraces.as_result);
    SmallstepExec.step = (fun x status ->
    let tr =
      match StructuredTraces.as_label s status with
      | Types.None -> Events.e0
      | Types.Some cst -> Events.echarge cst
    in
    Obj.magic
      (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (as_eval status)
        (fun status' ->
        Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = tr;
          Types.snd = status' }))) }

(** val mk_fullexec_of_abstract_status :
    StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
    __ -> (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
let mk_fullexec_of_abstract_status s as_eval as_init =
  { SmallstepExec.es1 = (mk_trans_system_of_abstract_status s as_eval);
    SmallstepExec.make_global = (fun x -> Obj.magic Types.It);
    SmallstepExec.make_initial_state = (fun x ->
    Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) as_init)) }

(** val mk_preclassified_system_of_abstract_status :
    StructuredTraces.abstract_status -> (__ -> __ Monad.max_def__o__monad) ->
    __ -> Measurable.preclassified_system **)
let mk_preclassified_system_of_abstract_status s as_eval as_init =
  { Measurable.pcs_exec = (mk_fullexec_of_abstract_status s as_eval as_init);
    Measurable.pcs_labelled = (fun x st ->
    Bool.notb (PositiveMap.is_none (StructuredTraces.as_label s st)));
    Measurable.pcs_classify = (fun x -> s.StructuredTraces.as_classify);
    Measurable.pcs_callee = (fun x st _ ->
    s.StructuredTraces.as_call_ident st) }

(** val oC_preclassified_system :
    ASM.labelled_object_code -> Measurable.preclassified_system **)
let oC_preclassified_system c =
  mk_preclassified_system_of_abstract_status (ASMCosts.oC_abstract_status c)
    (fun st ->
    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
      (Interpret.execute_1 c.ASM.cm (Obj.magic st)))
    (Obj.magic (Status.initialise_status c.ASM.cm))

open Assembly

(** val execute_1_pseudo_instruction' :
    ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
    -> (BitVector.word -> Bool.bool) -> Status.pseudoStatus ->
    Status.pseudoStatus **)
let execute_1_pseudo_instruction' cm addr_of_label addr_of_symbol sigma policy status =
  Interpret.execute_1_pseudo_instruction cm (fun x _ ->
    Assembly.ticks_of cm addr_of_label sigma policy x) addr_of_label
    addr_of_symbol status

(** val classify_pseudo_instruction :
    ASM.pseudo_instruction -> StructuredTraces.status_class **)
let classify_pseudo_instruction = function
| ASM.Instruction pre -> AbstractStatus.aSM_classify00 pre
| ASM.Comment x -> StructuredTraces.Cl_other
| ASM.Cost x -> StructuredTraces.Cl_other
| ASM.Jmp x -> StructuredTraces.Cl_other
| ASM.Jnz (x, x0, x1) -> StructuredTraces.Cl_jump
| ASM.Call x -> StructuredTraces.Cl_call
| ASM.Mov (x, x0, x1) -> StructuredTraces.Cl_other

(** val aSM_classify :
    ASM.pseudo_assembly_program -> Status.pseudoStatus ->
    StructuredTraces.status_class **)
let aSM_classify cm s =
  classify_pseudo_instruction
    (ASM.fetch_pseudo_instruction cm.ASM.code s.Status.program_counter).Types.fst

(** val aSM_as_label_of_pc :
    ASM.pseudo_assembly_program -> BitVector.word -> CostLabel.costlabel
    Types.option **)
let aSM_as_label_of_pc prog pc =
  match (ASM.fetch_pseudo_instruction prog.ASM.code pc).Types.fst with
  | ASM.Instruction x -> Types.None
  | ASM.Comment x -> Types.None
  | ASM.Cost label -> Types.Some label
  | ASM.Jmp x -> Types.None
  | ASM.Jnz (x, x0, x1) -> Types.None
  | ASM.Call x -> Types.None
  | ASM.Mov (x, x0, x1) -> Types.None

(** val aSM_as_result :
    ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
    Status.pseudoStatus -> Integers.int Types.option **)
let aSM_as_result prog addr_of_labels st =
  let finaladdr = addr_of_labels prog.ASM.final_label in
  ASMCosts.as_result_of_finaladdr prog st finaladdr

open AssocList

(** val aSM_as_call_ident :
    ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
    -> (BitVector.word -> Bool.bool) -> Status.pseudoStatus Types.sig0 ->
    AST.ident **)
let aSM_as_call_ident prog addr_of_label addr_of_symbol sigma policy s0 =
  let st =
    execute_1_pseudo_instruction' prog addr_of_label addr_of_symbol sigma
      policy (Types.pi1 s0)
  in
  let { Types.fst = lbl; Types.snd = instr } =
    Util.nth_safe
      (Arithmetic.nat_of_bitvector (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)))))))))))))))) st.Status.program_counter) prog.ASM.code
  in
  (match lbl with
   | Types.None -> assert false (* absurd case *)
   | Types.Some lbl' ->
     (match AssocList.assoc_list_lookup lbl'
              (Identifiers.eq_identifier PreIdentifiers.ASMTag)
              prog.ASM.renamed_symbols with
      | Types.None -> assert false (* absurd case *)
      | Types.Some id -> id))

(** val aSM_abstract_status :
    ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
    (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
    -> (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
let aSM_abstract_status prog addr_of_label addr_of_symbol sigma policy =
  { StructuredTraces.as_pc = AbstractStatus.word_deqset;
    StructuredTraces.as_pc_of = (Obj.magic (Status.program_counter prog));
    StructuredTraces.as_classify = (Obj.magic (aSM_classify prog));
    StructuredTraces.as_label_of_pc = (Obj.magic (aSM_as_label_of_pc prog));
    StructuredTraces.as_result =
    (Obj.magic (aSM_as_result prog addr_of_label));
    StructuredTraces.as_call_ident =
    (Obj.magic
      (aSM_as_call_ident prog addr_of_label addr_of_symbol sigma policy));
    StructuredTraces.as_tailcall_ident = (fun clearme ->
    let st = clearme in
    (match (ASM.fetch_pseudo_instruction prog.ASM.code
             (Obj.magic st).Status.program_counter).Types.fst with
     | ASM.Instruction clearme0 ->
       (match clearme0 with
        | ASM.ADD (x, y) ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.ADDC (x, y) ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.SUBB (x, y) ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.INC x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.DEC x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.MUL (x, y) ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.DIV (x, y) ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.DA x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.JC x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
        | ASM.JNC x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
        | ASM.JB (x, y) ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
        | ASM.JNB (x, y) ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
        | ASM.JBC (x, y) ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
        | ASM.JZ x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
        | ASM.JNZ x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
        | ASM.CJNE (x, y) ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
        | ASM.DJNZ (x, y) ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
        | ASM.ANL x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.ORL x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.XRL x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.CLR x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.CPL x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.RL x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.RLC x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.RR x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.RRC x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.SWAP x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.MOV x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.MOVX x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.SETB x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.PUSH x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.POP x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.XCH (x, y) ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.XCHD (x, y) ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.RET ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
        | ASM.RETI ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_return StructuredTraces.Cl_tailcall __)
        | ASM.NOP ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
        | ASM.JMP x ->
          (fun _ ->
            Obj.magic StructuredTraces.status_class_discr
              StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __))
     | ASM.Comment x ->
       (fun _ ->
         Obj.magic StructuredTraces.status_class_discr
           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     | ASM.Cost x ->
       (fun _ ->
         Obj.magic StructuredTraces.status_class_discr
           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     | ASM.Jmp x ->
       (fun _ ->
         Obj.magic StructuredTraces.status_class_discr
           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)
     | ASM.Jnz (x, y, abs) ->
       (fun _ ->
         Obj.magic StructuredTraces.status_class_discr
           StructuredTraces.Cl_jump StructuredTraces.Cl_tailcall __)
     | ASM.Call x ->
       (fun _ ->
         Obj.magic StructuredTraces.status_class_discr
           StructuredTraces.Cl_call StructuredTraces.Cl_tailcall __)
     | ASM.Mov (x, y, abs) ->
       (fun _ ->
         Obj.magic StructuredTraces.status_class_discr
           StructuredTraces.Cl_other StructuredTraces.Cl_tailcall __)) __) }

(** val aSM_preclassified_system :
    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
    (BitVector.word -> Bool.bool) -> Measurable.preclassified_system **)
let aSM_preclassified_system c sigma policy =
  let label_map = (Fetch.create_label_cost_map c.ASM.code).Types.fst in
  let symbol_map = Status.construct_datalabels c.ASM.preamble in
  let addr_of_label = fun x ->
    Arithmetic.bitvector_of_nat (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))))))))))))))))
      (Identifiers.lookup_def PreIdentifiers.ASMTag label_map x Nat.O)
  in
  let addr_of_symbol = fun x ->
    Identifiers.lookup_def PreIdentifiers.ASMTag symbol_map x
      (addr_of_label x)
  in
  mk_preclassified_system_of_abstract_status
    (aSM_abstract_status c addr_of_label addr_of_symbol sigma policy)
    (fun st ->
    Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
      (execute_1_pseudo_instruction' c addr_of_label addr_of_symbol sigma
        policy (Obj.magic st))) (Obj.magic (Status.initialise_status c))

(** val aSM_status :
    ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
    (BitVector.word -> Bool.bool) -> StructuredTraces.abstract_status **)
let aSM_status c sigma policy =
  let label_map = (Fetch.create_label_cost_map c.ASM.code).Types.fst in
  let symbol_map = Status.construct_datalabels c.ASM.preamble in
  let addr_of_label = fun x ->
    Arithmetic.bitvector_of_nat (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))))))))))))))))
      (Identifiers.lookup_def PreIdentifiers.ASMTag label_map x Nat.O)
  in
  let addr_of_symbol = fun x ->
    Identifiers.lookup_def PreIdentifiers.ASMTag symbol_map x
      (addr_of_label x)
  in
  aSM_abstract_status c addr_of_label addr_of_symbol sigma policy