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
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;
136                      address_map : BitVector.word Identifiers.identifier_map }
137
138val aSM_universe_rect_Type4 :
[2773]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
[2717]143
144val aSM_universe_rect_Type5 :
[2773]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
[2717]149
150val aSM_universe_rect_Type3 :
[2773]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
[2717]155
156val aSM_universe_rect_Type2 :
[2773]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
[2717]161
162val aSM_universe_rect_Type1 :
[2773]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
[2717]167
168val aSM_universe_rect_Type0 :
[2773]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
[2717]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 :
[2773]179  AST.ident List.list -> aSM_universe -> ASM.identifier
[2717]180  Identifiers.identifier_map
181
182val label_map :
[2773]183  AST.ident List.list -> aSM_universe -> ASM.identifier
[2717]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
[2773]192  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
[2717]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
[2773]198  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
[2717]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
[2773]204  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
[2717]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
[2773]210  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
[2717]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
[2773]216  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
[2717]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 :
[2773]226  AST.ident List.list -> Graphs.label -> ASM.identifier
[2717]227  Monad.smax_def__o__monad
228
229val identifier_of_ident :
[2773]230  AST.ident List.list -> AST.ident -> ASM.identifier Monad.smax_def__o__monad
[2717]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 :
[2773]240  AST.ident List.list -> ASM.identifier Monad.smax_def__o__monad
[2717]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
[2951]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
[2773]285val get_symboltable :
286  AST.ident List.list -> (ASM.identifier, AST.ident) Types.prod List.list
287  Monad.smax_def__o__monad
[2717]288
[2773]289val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program Types.option
290
Note: See TracBrowser for help on using the repository browser.