source: extracted/abstractStatus.ml @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 7 years ago

...

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