source: extracted/abstractStatus.ml @ 2746

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

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