open Preamble

open Hide

open Integers

open AST

open Division

open Exp

open Arithmetic

open Extranat

open Vector

open FoldStuff

open BitVector

open Z

open BitVectorZ

open Pointers

open Coqlib

open Values

open Events

open IOMonad

open IO

open Sets

open Listb

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 Russell

open Util

open List

open Lists

open Nat

open Positive

open Types

open Identifiers

open CostLabel

open Jmeq

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

open Bool

open StructuredTraces

open BitVectorTrie

open String

open LabelledObjects

open ASM

open Status

open Fetch

(** val aSM_classify00 :
    'a1 ASM.preinstruction -> StructuredTraces.status_class **)
let aSM_classify00 = function
| ASM.ADD (x, x0) -> StructuredTraces.Cl_other
| ASM.ADDC (x, x0) -> StructuredTraces.Cl_other
| ASM.SUBB (x, x0) -> StructuredTraces.Cl_other
| ASM.INC x -> StructuredTraces.Cl_other
| ASM.DEC x -> StructuredTraces.Cl_other
| ASM.MUL (x, x0) -> StructuredTraces.Cl_other
| ASM.DIV (x, x0) -> StructuredTraces.Cl_other
| ASM.DA x -> StructuredTraces.Cl_other
| ASM.JC x -> StructuredTraces.Cl_jump
| ASM.JNC x -> StructuredTraces.Cl_jump
| ASM.JB (x, x0) -> StructuredTraces.Cl_jump
| ASM.JNB (x, x0) -> StructuredTraces.Cl_jump
| ASM.JBC (x, x0) -> StructuredTraces.Cl_jump
| ASM.JZ x -> StructuredTraces.Cl_jump
| ASM.JNZ x -> StructuredTraces.Cl_jump
| ASM.CJNE (x, x0) -> StructuredTraces.Cl_jump
| ASM.DJNZ (x, x0) -> StructuredTraces.Cl_jump
| ASM.ANL x -> StructuredTraces.Cl_other
| ASM.ORL x -> StructuredTraces.Cl_other
| ASM.XRL x -> StructuredTraces.Cl_other
| ASM.CLR x -> StructuredTraces.Cl_other
| ASM.CPL x -> StructuredTraces.Cl_other
| ASM.RL x -> StructuredTraces.Cl_other
| ASM.RLC x -> StructuredTraces.Cl_other
| ASM.RR x -> StructuredTraces.Cl_other
| ASM.RRC x -> StructuredTraces.Cl_other
| ASM.SWAP x -> StructuredTraces.Cl_other
| ASM.MOV x -> StructuredTraces.Cl_other
| ASM.MOVX x -> StructuredTraces.Cl_other
| ASM.SETB x -> StructuredTraces.Cl_other
| ASM.PUSH x -> StructuredTraces.Cl_other
| ASM.POP x -> StructuredTraces.Cl_other
| ASM.XCH (x, x0) -> StructuredTraces.Cl_other
| ASM.XCHD (x, x0) -> StructuredTraces.Cl_other
| ASM.RET -> StructuredTraces.Cl_return
| ASM.RETI -> StructuredTraces.Cl_return
| ASM.NOP -> StructuredTraces.Cl_other
| ASM.JMP x -> StructuredTraces.Cl_call

(** val aSM_classify0 : ASM.instruction -> StructuredTraces.status_class **)
let aSM_classify0 = function
| ASM.ACALL x -> StructuredTraces.Cl_call
| ASM.LCALL x -> StructuredTraces.Cl_call
| ASM.AJMP x -> StructuredTraces.Cl_other
| ASM.LJMP x -> StructuredTraces.Cl_other
| ASM.SJMP x -> StructuredTraces.Cl_other
| ASM.MOVC (x, x0) -> StructuredTraces.Cl_other
| ASM.RealInstruction pre -> aSM_classify00 pre

(** val current_instruction :
    BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
    ASM.instruction **)
let current_instruction code_memory s =
  (Fetch.fetch code_memory s.Status.program_counter).Types.fst.Types.fst

(** val current_instruction_label :
    BitVector.byte BitVectorTrie.bitVectorTrie -> ASM.costlabel_map ->
    Status.status -> CostLabel.costlabel Types.option **)
let current_instruction_label code_memory cost_labels s =
  let pc = s.Status.program_counter in
  BitVectorTrie.lookup_opt (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)))))))))))))))) pc cost_labels

(** val word_deqset : Deqsets.deqSet **)
let word_deqset =
  Obj.magic
    (BitVector.eq_bv (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)))))))))))))))))

(** val oC_classify :
    BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
    StructuredTraces.status_class **)
let oC_classify code_memory s =
  aSM_classify0 (current_instruction code_memory s)