extracted/abstractStatus.ml

   1 open Preamble
   2
   3 open Hide
   4
   5 open Integers
   6
   7 open AST
   8
   9 open Division
  10
  11 open Exp
  12
  13 open Arithmetic
  14
  15 open Extranat
  16
  17 open Vector
  18
  19 open FoldStuff
  20
  21 open BitVector
  22
  23 open Z
  24
  25 open BitVectorZ
  26
  27 open Pointers
  28
  29 open Coqlib
  30
  31 open Values
  32
  33 open Events
  34
  35 open IOMonad
  36
  37 open IO
  38
  39 open Sets
  40
  41 open Listb
  42
  43 open Proper
  44
  45 open PositiveMap
  46
  47 open Deqsets
  48
  49 open ErrorMessages
  50
  51 open PreIdentifiers
  52
  53 open Errors
  54
  55 open Extralib
  56
  57 open Setoids
  58
  59 open Monad
  60
  61 open Option
  62
  63 open Div_and_mod
  64
  65 open Russell
  66
  67 open Util
  68
  69 open List
  70
  71 open Lists
  72
  73 open Nat
  74
  75 open Positive
  76
  77 open Types
  78
  79 open Identifiers
  80
  81 open CostLabel
  82
  83 open Jmeq
  84
  85 open Hints_declaration
  86
  87 open Core_notation
  88
  89 open Pts
  90
  91 open Logic
  92
  93 open Relations
  94
  95 open Bool
  96
  97 open StructuredTraces
  98
  99 open BitVectorTrie
 100
 101 open String
 102
 103 open LabelledObjects
 104
 105 open ASM
 106
 107 open Status
 108
 109 open Fetch
 110
 111 (** val aSM_classify00 :
 112     'a1 ASM.preinstruction -> StructuredTraces.status_class **)
 113 let aSM_classify00 = function
 114 | ASM.ADD (x, x0) -> StructuredTraces.Cl_other
 115 | ASM.ADDC (x, x0) -> StructuredTraces.Cl_other
 116 | ASM.SUBB (x, x0) -> StructuredTraces.Cl_other
 117 | ASM.INC x -> StructuredTraces.Cl_other
 118 | ASM.DEC x -> StructuredTraces.Cl_other
 119 | ASM.MUL (x, x0) -> StructuredTraces.Cl_other
 120 | ASM.DIV (x, x0) -> StructuredTraces.Cl_other
 121 | ASM.DA x -> StructuredTraces.Cl_other
 122 | ASM.JC x -> StructuredTraces.Cl_jump
 123 | ASM.JNC x -> StructuredTraces.Cl_jump
 124 | ASM.JB (x, x0) -> StructuredTraces.Cl_jump
 125 | ASM.JNB (x, x0) -> StructuredTraces.Cl_jump
 126 | ASM.JBC (x, x0) -> StructuredTraces.Cl_jump
 127 | ASM.JZ x -> StructuredTraces.Cl_jump
 128 | ASM.JNZ x -> StructuredTraces.Cl_jump
 129 | ASM.CJNE (x, x0) -> StructuredTraces.Cl_jump
 130 | ASM.DJNZ (x, x0) -> StructuredTraces.Cl_jump
 131 | ASM.ANL x -> StructuredTraces.Cl_other
 132 | ASM.ORL x -> StructuredTraces.Cl_other
 133 | ASM.XRL x -> StructuredTraces.Cl_other
 134 | ASM.CLR x -> StructuredTraces.Cl_other
 135 | ASM.CPL x -> StructuredTraces.Cl_other
 136 | ASM.RL x -> StructuredTraces.Cl_other
 137 | ASM.RLC x -> StructuredTraces.Cl_other
 138 | ASM.RR x -> StructuredTraces.Cl_other
 139 | ASM.RRC x -> StructuredTraces.Cl_other
 140 | ASM.SWAP x -> StructuredTraces.Cl_other
 141 | ASM.MOV x -> StructuredTraces.Cl_other
 142 | ASM.MOVX x -> StructuredTraces.Cl_other
 143 | ASM.SETB x -> StructuredTraces.Cl_other
 144 | ASM.PUSH x -> StructuredTraces.Cl_other
 145 | ASM.POP x -> StructuredTraces.Cl_other
 146 | ASM.XCH (x, x0) -> StructuredTraces.Cl_other
 147 | ASM.XCHD (x, x0) -> StructuredTraces.Cl_other
 148 | ASM.RET -> StructuredTraces.Cl_return
 149 | ASM.RETI -> StructuredTraces.Cl_return
 150 | ASM.NOP -> StructuredTraces.Cl_other
 151 | ASM.JMP x -> StructuredTraces.Cl_call
 152
 153 (** val aSM_classify0 : ASM.instruction -> StructuredTraces.status_class **)
 154 let aSM_classify0 = function
 155 | ASM.ACALL x -> StructuredTraces.Cl_call
 156 | ASM.LCALL x -> StructuredTraces.Cl_call
 157 | ASM.AJMP x -> StructuredTraces.Cl_other
 158 | ASM.LJMP x -> StructuredTraces.Cl_other
 159 | ASM.SJMP x -> StructuredTraces.Cl_other
 160 | ASM.MOVC (x, x0) -> StructuredTraces.Cl_other
 161 | ASM.RealInstruction pre -> aSM_classify00 pre
 162
 163 (** val current_instruction0 :
 164     BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
 165     ASM.instruction **)
 166 let current_instruction0 code_memory program_counter =
 167   (Fetch.fetch code_memory program_counter).Types.fst.Types.fst
 168
 169 (** val current_instruction :
 170     BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
 171     ASM.instruction **)
 172 let current_instruction code_memory s =
 173   current_instruction0 code_memory s.Status.program_counter
 174
 175 (** val current_instruction_label :
 176     BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
 177     BitVectorTrie.bitVectorTrie -> Status.status -> CostLabel.costlabel
 178     Types.option **)
 179 let current_instruction_label code_memory cost_labels s =
 180   let pc = s.Status.program_counter in
 181   BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 182     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 183     Nat.O)))))))))))))))) pc cost_labels
 184
 185 (** val word_deqset : Deqsets.deqSet **)
 186 let word_deqset =
 187   Obj.magic
 188     (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 189       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 190       Nat.O)))))))))))))))))
 191
 192 (** val oC_classify :
 193     BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
 194     StructuredTraces.status_class **)
 195 let oC_classify code_memory s =
 196   aSM_classify0 (current_instruction code_memory s)
 197