source: driver/extracted/abstractStatus.ml @ 3106

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

New extraction.

File size: 4.0 KB
Line 
1open Preamble
2
3open Hide
4
5open Integers
6
7open AST
8
9open Division
10
11open Exp
12
13open Arithmetic
14
15open Extranat
16
17open Vector
18
19open FoldStuff
20
21open BitVector
22
23open Z
24
25open BitVectorZ
26
27open Pointers
28
29open Coqlib
30
31open Values
32
33open Events
34
35open IOMonad
36
37open IO
38
39open Sets
40
41open Listb
42
43open Proper
44
45open PositiveMap
46
47open Deqsets
48
49open ErrorMessages
50
51open PreIdentifiers
52
53open Errors
54
55open Extralib
56
57open Setoids
58
59open Monad
60
61open Option
62
63open Div_and_mod
64
65open Russell
66
67open Util
68
69open List
70
71open Lists
72
73open Nat
74
75open Positive
76
77open Types
78
79open Identifiers
80
81open CostLabel
82
83open Jmeq
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Relations
94
95open Bool
96
97open StructuredTraces
98
99open BitVectorTrie
100
101open String
102
103open LabelledObjects
104
105open ASM
106
107open Status
108
109open Fetch
110
111(** val aSM_classify00 :
112    'a1 ASM.preinstruction -> StructuredTraces.status_class **)
113let 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 **)
154let 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_instruction :
164    BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
165    ASM.instruction **)
166let current_instruction code_memory s =
167  (Fetch.fetch code_memory s.Status.program_counter).Types.fst.Types.fst
168
169(** val current_instruction_label :
170    BitVector.byte BitVectorTrie.bitVectorTrie -> ASM.costlabel_map ->
171    Status.status -> CostLabel.costlabel Types.option **)
172let 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
177
178(** val word_deqset : Deqsets.deqSet **)
179let word_deqset =
180  Obj.magic
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)))))))))))))))))
184
185(** val oC_classify :
186    BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
187    StructuredTraces.status_class **)
188let oC_classify code_memory s =
189  aSM_classify0 (current_instruction code_memory s)
190
Note: See TracBrowser for help on using the repository browser.