source: extracted/abstractStatus.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 4.1 KB
Line 
1open Preamble
2
3open LabelledObjects
4
5open Coqlib
6
7open Floats
8
9open Arithmetic
10
11open Integers
12
13open AST
14
15open CostLabel
16
17open Proper
18
19open PositiveMap
20
21open Deqsets
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 Char
42
43open String
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 BitVectorTrie
82
83open Status
84
85open Fetch
86
87open Sets
88
89open Listb
90
91open StructuredTraces
92
93(** val aSM_classify00 :
94    'a1 ASM.preinstruction -> StructuredTraces.status_class **)
95let aSM_classify00 = function
96| ASM.ADD (x, x0) -> StructuredTraces.Cl_other
97| ASM.ADDC (x, x0) -> StructuredTraces.Cl_other
98| ASM.SUBB (x, x0) -> StructuredTraces.Cl_other
99| ASM.INC x -> StructuredTraces.Cl_other
100| ASM.DEC x -> StructuredTraces.Cl_other
101| ASM.MUL (x, x0) -> StructuredTraces.Cl_other
102| ASM.DIV (x, x0) -> StructuredTraces.Cl_other
103| ASM.DA x -> StructuredTraces.Cl_other
104| ASM.JC x -> StructuredTraces.Cl_jump
105| ASM.JNC x -> StructuredTraces.Cl_jump
106| ASM.JB (x, x0) -> StructuredTraces.Cl_jump
107| ASM.JNB (x, x0) -> StructuredTraces.Cl_jump
108| ASM.JBC (x, x0) -> StructuredTraces.Cl_jump
109| ASM.JZ x -> StructuredTraces.Cl_jump
110| ASM.JNZ x -> StructuredTraces.Cl_jump
111| ASM.CJNE (x, x0) -> StructuredTraces.Cl_jump
112| ASM.DJNZ (x, x0) -> StructuredTraces.Cl_jump
113| ASM.ANL x -> StructuredTraces.Cl_other
114| ASM.ORL x -> StructuredTraces.Cl_other
115| ASM.XRL x -> StructuredTraces.Cl_other
116| ASM.CLR x -> StructuredTraces.Cl_other
117| ASM.CPL x -> StructuredTraces.Cl_other
118| ASM.RL x -> StructuredTraces.Cl_other
119| ASM.RLC x -> StructuredTraces.Cl_other
120| ASM.RR x -> StructuredTraces.Cl_other
121| ASM.RRC x -> StructuredTraces.Cl_other
122| ASM.SWAP x -> StructuredTraces.Cl_other
123| ASM.MOV x -> StructuredTraces.Cl_other
124| ASM.MOVX x -> StructuredTraces.Cl_other
125| ASM.SETB x -> StructuredTraces.Cl_other
126| ASM.PUSH x -> StructuredTraces.Cl_other
127| ASM.POP x -> StructuredTraces.Cl_other
128| ASM.XCH (x, x0) -> StructuredTraces.Cl_other
129| ASM.XCHD (x, x0) -> StructuredTraces.Cl_other
130| ASM.RET -> StructuredTraces.Cl_return
131| ASM.RETI -> StructuredTraces.Cl_return
132| ASM.NOP -> StructuredTraces.Cl_other
133
134(** val aSM_classify0 : ASM.instruction -> StructuredTraces.status_class **)
135let aSM_classify0 = function
136| ASM.ACALL x -> StructuredTraces.Cl_call
137| ASM.LCALL x -> StructuredTraces.Cl_call
138| ASM.AJMP x -> StructuredTraces.Cl_other
139| ASM.LJMP x -> StructuredTraces.Cl_other
140| ASM.SJMP x -> StructuredTraces.Cl_other
141| ASM.JMP x -> StructuredTraces.Cl_call
142| ASM.MOVC (x, x0) -> StructuredTraces.Cl_other
143| ASM.RealInstruction pre -> aSM_classify00 pre
144
145(** val current_instruction0 :
146    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
147    ASM.instruction **)
148let current_instruction0 code_memory program_counter0 =
149  (Fetch.fetch code_memory program_counter0).Types.fst.Types.fst
150
151(** val current_instruction :
152    BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
153    ASM.instruction **)
154let current_instruction code_memory s =
155  current_instruction0 code_memory s.Status.program_counter
156
157(** val current_instruction_label :
158    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
159    BitVectorTrie.bitVectorTrie -> Status.status -> CostLabel.costlabel
160    Types.option **)
161let current_instruction_label code_memory cost_labels s =
162  let pc = s.Status.program_counter in
163  BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
164    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
165    Nat.O)))))))))))))))) pc cost_labels
166
167(** val word_deqset : Deqsets.deqSet **)
168let word_deqset =
169  Obj.magic
170    (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
171      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
172      Nat.O)))))))))))))))))
173
174(** val aSM_classify :
175    BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
176    StructuredTraces.status_class **)
177let aSM_classify code_memory s =
178  aSM_classify0 (current_instruction code_memory s)
179
Note: See TracBrowser for help on using the repository browser.