source: extracted/lINToASM.mli @ 3001

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

New extraction.

File size: 9.2 KB
RevLine 
[2717]1open Preamble
2
[2773]3open Deqsets
4
5open Setoids
6
7open Monad
8
9open Option
10
11open Extranat
12
13open Vector
14
[2717]15open Div_and_mod
16
17open Jmeq
18
19open Russell
20
[2773]21open List
22
23open Util
24
25open FoldStuff
26
[2717]27open Bool
28
29open Relations
30
31open Nat
32
[2773]33open BitVector
34
[2717]35open Hints_declaration
36
37open Core_notation
38
39open Pts
40
41open Logic
42
43open Types
44
45open BitVectorTrie
46
47open BitVectorTrieSet
48
[2773]49open State
50
[2717]51open String
52
[2773]53open Exp
[2717]54
[2773]55open Arithmetic
[2717]56
[2773]57open Integers
[2717]58
[2773]59open AST
[2717]60
[2773]61open LabelledObjects
[2717]62
63open Proper
64
65open PositiveMap
66
67open ErrorMessages
68
69open PreIdentifiers
70
71open Errors
72
73open Extralib
74
[2773]75open Lists
[2717]76
[2773]77open Positive
[2717]78
[2773]79open Identifiers
[2717]80
[2773]81open CostLabel
[2717]82
[2773]83open ASM
[2717]84
[2951]85open Extra_bool
86
87open Coqlib
88
89open Values
90
91open FrontEndVal
92
93open GenMem
94
95open FrontEndMem
96
97open Globalenvs
98
[2773]99open Sets
[2717]100
[2773]101open Listb
[2717]102
[2773]103open Graphs
[2717]104
[2773]105open I8051
[2717]106
[2773]107open Order
[2717]108
[2773]109open Registers
[2717]110
[2773]111open Hide
112
113open Division
114
[2717]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;
[2773]133                      ident_map : ASM.identifier Identifiers.identifier_map;
134                      label_map : ASM.identifier Identifiers.identifier_map
[2717]135                                  Identifiers.identifier_map;
[2979]136                      address_map : BitVector.word Identifiers.identifier_map;
137                      fresh_cost_label : Positive.pos }
[2717]138
139val aSM_universe_rect_Type4 :
[2773]140  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
141  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
142  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
[2979]143  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
[2717]144
145val aSM_universe_rect_Type5 :
[2773]146  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
147  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
148  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
[2979]149  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
[2717]150
151val aSM_universe_rect_Type3 :
[2773]152  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
153  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
154  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
[2979]155  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
[2717]156
157val aSM_universe_rect_Type2 :
[2773]158  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
159  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
160  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
[2979]161  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
[2717]162
163val aSM_universe_rect_Type1 :
[2773]164  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
165  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
166  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
[2979]167  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
[2717]168
169val aSM_universe_rect_Type0 :
[2773]170  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
171  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
172  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
[2979]173  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
[2717]174
175val id_univ : AST.ident List.list -> aSM_universe -> Identifiers.universe
176
177val current_funct : AST.ident List.list -> aSM_universe -> AST.ident
178
179val ident_map :
[2773]180  AST.ident List.list -> aSM_universe -> ASM.identifier
[2717]181  Identifiers.identifier_map
182
183val label_map :
[2773]184  AST.ident List.list -> aSM_universe -> ASM.identifier
[2717]185  Identifiers.identifier_map Identifiers.identifier_map
186
187val address_map :
188  AST.ident List.list -> aSM_universe -> BitVector.word
189  Identifiers.identifier_map
190
[2979]191val fresh_cost_label : AST.ident List.list -> aSM_universe -> Positive.pos
192
[2717]193val aSM_universe_inv_rect_Type4 :
194  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
[2773]195  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
[2717]196  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
[2979]197  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
[2717]198
199val aSM_universe_inv_rect_Type3 :
200  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
[2773]201  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
[2717]202  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
[2979]203  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
[2717]204
205val aSM_universe_inv_rect_Type2 :
206  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
[2773]207  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
[2717]208  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
[2979]209  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
[2717]210
211val aSM_universe_inv_rect_Type1 :
212  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
[2773]213  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
[2717]214  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
[2979]215  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
[2717]216
217val aSM_universe_inv_rect_Type0 :
218  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
[2773]219  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
[2717]220  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
[2979]221  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
[2717]222
223val aSM_universe_jmdiscr :
224  AST.ident List.list -> aSM_universe -> aSM_universe -> __
225
[2979]226val report_cost :
227  AST.ident List.list -> CostLabel.costlabel -> Types.unit0
228  Monad.smax_def__o__monad
229
[2717]230val new_ASM_universe : Joint.joint_program -> aSM_universe
231
232val identifier_of_label :
[2773]233  AST.ident List.list -> Graphs.label -> ASM.identifier
[2717]234  Monad.smax_def__o__monad
235
236val identifier_of_ident :
[2773]237  AST.ident List.list -> AST.ident -> ASM.identifier Monad.smax_def__o__monad
[2717]238
239val start_funct_translation :
240  AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod ->
241  Types.unit0 Monad.smax_def__o__monad
242
243val address_of_ident :
244  __ List.list -> __ -> ASM.subaddressing_mode Monad.smax_def__o__monad
245
246val aSM_fresh :
[2773]247  AST.ident List.list -> ASM.identifier Monad.smax_def__o__monad
[2717]248
249val register_address : I8051.register -> ASM.subaddressing_mode
250
251val vector_cast :
252  Nat.nat -> Nat.nat -> 'a1 -> 'a1 Vector.vector -> 'a1 Vector.vector
253
254val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode
255
256type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj
257
258val data_of_int : BitVector.byte -> ASM.addressing_mode
259
260val data16_of_int : Nat.nat -> ASM.addressing_mode
261
262val accumulator_address : ASM.addressing_mode
263
264val asm_other_bit : ASM.addressing_mode
265
266val translate_statements :
267  AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction
268  Monad.smax_def__o__monad
269
270val build_translated_statement : AST.ident List.list -> lin_statement -> __
271
272val translate_code : AST.ident List.list -> lin_statement List.list -> __
273
274val translate_fun_def :
275  AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod -> __
276
[2986]277type init_mutable = { virtual_dptr : Z.z; actual_dptr : Z.z;
278                      built : ASM.labelled_instruction List.list }
[2951]279
[2986]280val init_mutable_rect_Type4 :
281  (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
282  -> 'a1
283
284val init_mutable_rect_Type5 :
285  (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
286  -> 'a1
287
288val init_mutable_rect_Type3 :
289  (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
290  -> 'a1
291
292val init_mutable_rect_Type2 :
293  (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
294  -> 'a1
295
296val init_mutable_rect_Type1 :
297  (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
298  -> 'a1
299
300val init_mutable_rect_Type0 :
301  (Z.z -> Z.z -> ASM.labelled_instruction List.list -> 'a1) -> init_mutable
302  -> 'a1
303
304val virtual_dptr : init_mutable -> Z.z
305
306val actual_dptr : init_mutable -> Z.z
307
308val built : init_mutable -> ASM.labelled_instruction List.list
309
310val init_mutable_inv_rect_Type4 :
311  init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list -> __ ->
312  'a1) -> 'a1
313
314val init_mutable_inv_rect_Type3 :
315  init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list -> __ ->
316  'a1) -> 'a1
317
318val init_mutable_inv_rect_Type2 :
319  init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list -> __ ->
320  'a1) -> 'a1
321
322val init_mutable_inv_rect_Type1 :
323  init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list -> __ ->
324  'a1) -> 'a1
325
326val init_mutable_inv_rect_Type0 :
327  init_mutable -> (Z.z -> Z.z -> ASM.labelled_instruction List.list -> __ ->
328  'a1) -> 'a1
329
330val init_mutable_discr : init_mutable -> init_mutable -> __
331
332val init_mutable_jmdiscr : init_mutable -> init_mutable -> __
333
334val store_byte : BitVector.byte -> init_mutable -> init_mutable
335
[2951]336val do_store_init_data :
[2986]337  AST.ident List.list -> aSM_universe -> AST.init_data -> init_mutable ->
338  init_mutable
[2951]339
340val do_store_init_data_list :
341  AST.ident List.list -> aSM_universe -> Z.z -> AST.init_data List.list ->
342  ASM.labelled_instruction List.list
343
[2986]344val translate_premain :
345  LIN.lin_program -> ASM.identifier -> ASM.labelled_instruction List.list
[2951]346  Monad.smax_def__o__monad
347
[2773]348val get_symboltable :
349  AST.ident List.list -> (ASM.identifier, AST.ident) Types.prod List.list
350  Monad.smax_def__o__monad
[2717]351
[2773]352val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program Types.option
353
Note: See TracBrowser for help on using the repository browser.