source: extracted/lINToASM.mli @ 2960

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 7.2 KB
Line 
1open Preamble
2
3open Deqsets
4
5open Setoids
6
7open Monad
8
9open Option
10
11open Extranat
12
13open Vector
14
15open Div_and_mod
16
17open Jmeq
18
19open Russell
20
21open List
22
23open Util
24
25open FoldStuff
26
27open Bool
28
29open Relations
30
31open Nat
32
33open BitVector
34
35open Hints_declaration
36
37open Core_notation
38
39open Pts
40
41open Logic
42
43open Types
44
45open BitVectorTrie
46
47open BitVectorTrieSet
48
49open State
50
51open String
52
53open Exp
54
55open Arithmetic
56
57open Integers
58
59open AST
60
61open LabelledObjects
62
63open Proper
64
65open PositiveMap
66
67open ErrorMessages
68
69open PreIdentifiers
70
71open Errors
72
73open Extralib
74
75open Lists
76
77open Positive
78
79open Identifiers
80
81open CostLabel
82
83open ASM
84
85open Extra_bool
86
87open Coqlib
88
89open Values
90
91open FrontEndVal
92
93open GenMem
94
95open FrontEndMem
96
97open Globalenvs
98
99open Sets
100
101open Listb
102
103open Graphs
104
105open I8051
106
107open Order
108
109open Registers
110
111open Hide
112
113open Division
114
115open Z
116
117open BitVectorZ
118
119open Pointers
120
121open ByteValues
122
123open BackEndOps
124
125open Joint
126
127open Joint_LTL_LIN
128
129open LIN
130
131type aSM_universe = { id_univ : Identifiers.universe;
132                      current_funct : AST.ident;
133                      ident_map : ASM.identifier Identifiers.identifier_map;
134                      label_map : ASM.identifier Identifiers.identifier_map
135                                  Identifiers.identifier_map;
136                      address_map : BitVector.word Identifiers.identifier_map }
137
138val aSM_universe_rect_Type4 :
139  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
140  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
141  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
142  __ -> 'a1) -> aSM_universe -> 'a1
143
144val aSM_universe_rect_Type5 :
145  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
146  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
147  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
148  __ -> 'a1) -> aSM_universe -> 'a1
149
150val aSM_universe_rect_Type3 :
151  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
152  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
153  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
154  __ -> 'a1) -> aSM_universe -> 'a1
155
156val aSM_universe_rect_Type2 :
157  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
158  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
159  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
160  __ -> 'a1) -> aSM_universe -> 'a1
161
162val aSM_universe_rect_Type1 :
163  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
164  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
165  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
166  __ -> 'a1) -> aSM_universe -> 'a1
167
168val aSM_universe_rect_Type0 :
169  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
170  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
171  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
172  __ -> 'a1) -> aSM_universe -> 'a1
173
174val id_univ : AST.ident List.list -> aSM_universe -> Identifiers.universe
175
176val current_funct : AST.ident List.list -> aSM_universe -> AST.ident
177
178val ident_map :
179  AST.ident List.list -> aSM_universe -> ASM.identifier
180  Identifiers.identifier_map
181
182val label_map :
183  AST.ident List.list -> aSM_universe -> ASM.identifier
184  Identifiers.identifier_map Identifiers.identifier_map
185
186val address_map :
187  AST.ident List.list -> aSM_universe -> BitVector.word
188  Identifiers.identifier_map
189
190val aSM_universe_inv_rect_Type4 :
191  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
192  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
193  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
194  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
195
196val aSM_universe_inv_rect_Type3 :
197  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
198  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
199  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
200  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
201
202val aSM_universe_inv_rect_Type2 :
203  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
204  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
205  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
206  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
207
208val aSM_universe_inv_rect_Type1 :
209  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
210  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
211  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
212  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
213
214val aSM_universe_inv_rect_Type0 :
215  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
216  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
217  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
218  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
219
220val aSM_universe_jmdiscr :
221  AST.ident List.list -> aSM_universe -> aSM_universe -> __
222
223val new_ASM_universe : Joint.joint_program -> aSM_universe
224
225val identifier_of_label :
226  AST.ident List.list -> Graphs.label -> ASM.identifier
227  Monad.smax_def__o__monad
228
229val identifier_of_ident :
230  AST.ident List.list -> AST.ident -> ASM.identifier Monad.smax_def__o__monad
231
232val start_funct_translation :
233  AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod ->
234  Types.unit0 Monad.smax_def__o__monad
235
236val address_of_ident :
237  __ List.list -> __ -> ASM.subaddressing_mode Monad.smax_def__o__monad
238
239val aSM_fresh :
240  AST.ident List.list -> ASM.identifier Monad.smax_def__o__monad
241
242val register_address : I8051.register -> ASM.subaddressing_mode
243
244val vector_cast :
245  Nat.nat -> Nat.nat -> 'a1 -> 'a1 Vector.vector -> 'a1 Vector.vector
246
247val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode
248
249type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj
250
251val data_of_int : BitVector.byte -> ASM.addressing_mode
252
253val data16_of_int : Nat.nat -> ASM.addressing_mode
254
255val accumulator_address : ASM.addressing_mode
256
257val asm_other_bit : ASM.addressing_mode
258
259val translate_statements :
260  AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction
261  Monad.smax_def__o__monad
262
263val build_translated_statement : AST.ident List.list -> lin_statement -> __
264
265val translate_code : AST.ident List.list -> lin_statement List.list -> __
266
267val translate_fun_def :
268  AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod -> __
269
270val store_bytes :
271  BitVector.byte List.list -> ASM.labelled_instruction List.list
272
273val do_store_init_data :
274  AST.ident List.list -> aSM_universe -> Z.z -> AST.init_data ->
275  ASM.labelled_instruction List.list
276
277val do_store_init_data_list :
278  AST.ident List.list -> aSM_universe -> Z.z -> AST.init_data List.list ->
279  ASM.labelled_instruction List.list
280
281val translate_initialization :
282  LIN.lin_program -> ASM.labelled_instruction List.list
283  Monad.smax_def__o__monad
284
285val get_symboltable :
286  AST.ident List.list -> (ASM.identifier, AST.ident) Types.prod List.list
287  Monad.smax_def__o__monad
288
289val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program Types.option
290
Note: See TracBrowser for help on using the repository browser.