source: extracted/abstractStatus.ml @ 2960

Last change on this file since 2960 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
RevLine 
[2601]1open Preamble
2
[2773]3open Hide
[2649]4
[2773]5open Integers
[2601]6
[2773]7open AST
[2717]8
[2773]9open Division
10
[2717]11open Exp
12
[2601]13open Arithmetic
14
[2773]15open Extranat
[2601]16
[2773]17open Vector
[2601]18
[2773]19open FoldStuff
[2601]20
[2773]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
[2601]43open Proper
44
45open PositiveMap
46
47open Deqsets
48
[2649]49open ErrorMessages
50
[2601]51open PreIdentifiers
52
53open Errors
54
55open Extralib
56
57open Setoids
58
59open Monad
60
61open Option
62
[2773]63open Div_and_mod
[2601]64
[2773]65open Russell
[2601]66
[2773]67open Util
[2601]68
[2773]69open List
[2601]70
[2773]71open Lists
[2601]72
[2773]73open Nat
[2601]74
[2773]75open Positive
[2601]76
77open Types
78
[2773]79open Identifiers
[2601]80
[2773]81open CostLabel
[2601]82
[2773]83open Jmeq
[2601]84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Relations
94
[2773]95open Bool
[2601]96
[2773]97open StructuredTraces
[2601]98
[2773]99open BitVectorTrie
100
101open String
102
103open LabelledObjects
104
[2601]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
[2717]151| ASM.JMP x -> StructuredTraces.Cl_call
[2601]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 **)
[2773]166let current_instruction0 code_memory program_counter =
167  (Fetch.fetch code_memory program_counter).Types.fst.Types.fst
[2601]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
[2905]192(** val oC_classify :
[2601]193    BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
194    StructuredTraces.status_class **)
[2905]195let oC_classify code_memory s =
[2601]196  aSM_classify0 (current_instruction code_memory s)
197
Note: See TracBrowser for help on using the repository browser.