85 open Hints_declaration
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
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
163 (** val current_instruction :
164 BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
166 let current_instruction code_memory s =
167 (Fetch.fetch code_memory s.Status.program_counter).Types.fst.Types.fst
169 (** val current_instruction_label :
170 BitVector.byte BitVectorTrie.bitVectorTrie -> ASM.costlabel_map ->
171 Status.status -> CostLabel.costlabel Types.option **)
172 let current_instruction_label code_memory cost_labels s =
173 let pc = s.Status.program_counter in
174 BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
175 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
176 Nat.O)))))))))))))))) pc cost_labels
178 (** val word_deqset : Deqsets.deqSet **)
181 (BitVector.eq_bv (Nat.S (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
183 Nat.O)))))))))))))))))
185 (** val oC_classify :
186 BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
187 StructuredTraces.status_class **)
188 let oC_classify code_memory s =
189 aSM_classify0 (current_instruction code_memory s)