source: extracted/abstractStatus.ml @ 2905

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

Semantics of ASM in place (up to return values and function call names).
The test example badly diverges in ASM after being ok in LIN.

File size: 4.2 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_instruction0 :
164    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
165    ASM.instruction **)
166let 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 **)
172let 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 **)
179let 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 **)
186let 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 **)
195let oC_classify code_memory s =
196  aSM_classify0 (current_instruction code_memory s)
197
Note: See TracBrowser for help on using the repository browser.