source: extracted/lINToASM.mli @ 3043

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 9.3 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                      fresh_cost_label : Positive.pos }
137
138val aSM_universe_rect_Type4 :
139  (Identifiers.universe -> AST.ident -> ASM.identifier
140  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
141  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
142
143val aSM_universe_rect_Type5 :
144  (Identifiers.universe -> AST.ident -> ASM.identifier
145  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
146  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
147
148val aSM_universe_rect_Type3 :
149  (Identifiers.universe -> AST.ident -> ASM.identifier
150  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
151  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
152
153val aSM_universe_rect_Type2 :
154  (Identifiers.universe -> AST.ident -> ASM.identifier
155  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
156  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
157
158val aSM_universe_rect_Type1 :
159  (Identifiers.universe -> AST.ident -> ASM.identifier
160  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
161  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
162
163val aSM_universe_rect_Type0 :
164  (Identifiers.universe -> AST.ident -> ASM.identifier
165  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
166  Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
167
168val id_univ : aSM_universe -> Identifiers.universe
169
170val current_funct : aSM_universe -> AST.ident
171
172val ident_map : aSM_universe -> ASM.identifier Identifiers.identifier_map
173
174val label_map :
175  aSM_universe -> ASM.identifier Identifiers.identifier_map
176  Identifiers.identifier_map
177
178val fresh_cost_label : aSM_universe -> Positive.pos
179
180val aSM_universe_inv_rect_Type4 :
181  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
182  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
183  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
184
185val aSM_universe_inv_rect_Type3 :
186  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
187  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
188  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
189
190val aSM_universe_inv_rect_Type2 :
191  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
192  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
193  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
194
195val aSM_universe_inv_rect_Type1 :
196  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
197  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
198  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
199
200val aSM_universe_inv_rect_Type0 :
201  aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier
202  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
203  Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1
204
205val aSM_universe_discr : aSM_universe -> aSM_universe -> __
206
207val aSM_universe_jmdiscr : aSM_universe -> aSM_universe -> __
208
209val report_cost : CostLabel.costlabel -> Types.unit0 Monad.smax_def__o__monad
210
211val identifier_of_label :
212  Graphs.label -> ASM.identifier Monad.smax_def__o__monad
213
214val identifier_of_ident :
215  AST.ident -> ASM.identifier Monad.smax_def__o__monad
216
217val new_ASM_universe : Joint.joint_program -> aSM_universe
218
219val start_funct_translation :
220  AST.ident List.list -> AST.ident List.list -> (AST.ident,
221  Joint.joint_function) Types.prod -> Types.unit0 Monad.smax_def__o__monad
222
223val aSM_fresh : ASM.identifier Monad.smax_def__o__monad
224
225val register_address : I8051.register -> ASM.subaddressing_mode
226
227val vector_cast :
228  Nat.nat -> Nat.nat -> 'a1 -> 'a1 Vector.vector -> 'a1 Vector.vector
229
230val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode
231
232type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj
233
234val data_of_int : BitVector.byte -> ASM.addressing_mode
235
236val data16_of_int : Nat.nat -> ASM.addressing_mode
237
238val accumulator_address : ASM.addressing_mode
239
240val asm_other_bit : ASM.addressing_mode
241
242val one_word : BitVector.word
243
244val translate_statements :
245  AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction
246  Monad.smax_def__o__monad
247
248val build_translated_statement : AST.ident List.list -> lin_statement -> __
249
250val translate_code : AST.ident List.list -> lin_statement List.list -> __
251
252val translate_fun_def :
253  AST.ident List.list -> AST.ident List.list -> (AST.ident,
254  Joint.joint_function) Types.prod -> __
255
256type init_mutable = { virtual_dptr : Z.z; actual_dptr : Z.z;
257                      built_code : ASM.labelled_instruction List.list
258                                   List.list;
259                      built_preamble : (ASM.identifier, BitVector.word)
260                                       Types.prod List.list }
261
262val init_mutable_rect_Type4 :
263  (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
264  (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
265  init_mutable -> 'a1
266
267val init_mutable_rect_Type5 :
268  (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
269  (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
270  init_mutable -> 'a1
271
272val init_mutable_rect_Type3 :
273  (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
274  (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
275  init_mutable -> 'a1
276
277val init_mutable_rect_Type2 :
278  (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
279  (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
280  init_mutable -> 'a1
281
282val init_mutable_rect_Type1 :
283  (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
284  (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
285  init_mutable -> 'a1
286
287val init_mutable_rect_Type0 :
288  (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list ->
289  (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) ->
290  init_mutable -> 'a1
291
292val virtual_dptr : init_mutable -> Z.z
293
294val actual_dptr : init_mutable -> Z.z
295
296val built_code : init_mutable -> ASM.labelled_instruction List.list List.list
297
298val built_preamble :
299  init_mutable -> (ASM.identifier, BitVector.word) Types.prod List.list
300
301val init_mutable_inv_rect_Type4 :
302  init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list
303  -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
304  'a1
305
306val init_mutable_inv_rect_Type3 :
307  init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list
308  -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
309  'a1
310
311val init_mutable_inv_rect_Type2 :
312  init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list
313  -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
314  'a1
315
316val init_mutable_inv_rect_Type1 :
317  init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list
318  -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
319  'a1
320
321val init_mutable_inv_rect_Type0 :
322  init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list List.list
323  -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) ->
324  'a1
325
326val init_mutable_discr : init_mutable -> init_mutable -> __
327
328val init_mutable_jmdiscr : init_mutable -> init_mutable -> __
329
330val store_byte_or_Identifier :
331  (BitVector.byte, (ASM.word_side, ASM.identifier) Types.prod) Types.sum ->
332  init_mutable -> init_mutable
333
334val do_store_init_data :
335  AST.init_data -> init_mutable Monad.smax_def__o__monad -> init_mutable
336  Monad.smax_def__o__monad
337
338val do_store_global :
339  ((AST.ident, AST.region) Types.prod, AST.init_data List.list) Types.prod ->
340  init_mutable Monad.smax_def__o__monad -> init_mutable
341  Monad.smax_def__o__monad
342
343val reversed_flatten_aux :
344  'a1 List.list -> 'a1 List.list List.list -> 'a1 List.list
345
346val translate_premain :
347  LIN.lin_program -> ASM.identifier -> (ASM.labelled_instruction List.list,
348  (ASM.identifier, BitVector.word) Types.prod List.list) Types.prod
349  Monad.smax_def__o__monad
350
351val get_symboltable :
352  (ASM.identifier, AST.ident) Types.prod List.list Monad.smax_def__o__monad
353
354val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program Types.option
355
Note: See TracBrowser for help on using the repository browser.