source: extracted/lINToASM.mli @ 2963

Last change on this file since 2963 was 2963, checked in by sacerdot, 8 years ago

Bug fixed: the pre-main for the final code is now

COST k1
initialization code
CALL main

l: COST k2

Jmp l

with l the label of the final state. In this way the static analysis on the
object code does not diverge.

File size: 7.6 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                      fresh_cost_label : Positive.pos }
138
139val aSM_universe_rect_Type4 :
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 ->
143  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
144
145val aSM_universe_rect_Type5 :
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 ->
149  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
150
151val aSM_universe_rect_Type3 :
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 ->
155  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
156
157val aSM_universe_rect_Type2 :
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 ->
161  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
162
163val aSM_universe_rect_Type1 :
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 ->
167  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
168
169val aSM_universe_rect_Type0 :
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 ->
173  __ -> Positive.pos -> 'a1) -> aSM_universe -> 'a1
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 :
180  AST.ident List.list -> aSM_universe -> ASM.identifier
181  Identifiers.identifier_map
182
183val label_map :
184  AST.ident List.list -> aSM_universe -> ASM.identifier
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
191val fresh_cost_label : AST.ident List.list -> aSM_universe -> Positive.pos
192
193val aSM_universe_inv_rect_Type4 :
194  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
195  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
196  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
197  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
198
199val aSM_universe_inv_rect_Type3 :
200  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
201  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
202  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
203  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
204
205val aSM_universe_inv_rect_Type2 :
206  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
207  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
208  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
209  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
210
211val aSM_universe_inv_rect_Type1 :
212  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
213  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
214  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
215  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
216
217val aSM_universe_inv_rect_Type0 :
218  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
219  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
220  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
221  Identifiers.identifier_map -> __ -> Positive.pos -> __ -> 'a1) -> 'a1
222
223val aSM_universe_jmdiscr :
224  AST.ident List.list -> aSM_universe -> aSM_universe -> __
225
226val report_cost :
227  AST.ident List.list -> CostLabel.costlabel -> Types.unit0
228  Monad.smax_def__o__monad
229
230val new_ASM_universe : Joint.joint_program -> aSM_universe
231
232val identifier_of_label :
233  AST.ident List.list -> Graphs.label -> ASM.identifier
234  Monad.smax_def__o__monad
235
236val identifier_of_ident :
237  AST.ident List.list -> AST.ident -> ASM.identifier Monad.smax_def__o__monad
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 :
247  AST.ident List.list -> ASM.identifier Monad.smax_def__o__monad
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
277val store_bytes :
278  BitVector.byte List.list -> ASM.labelled_instruction List.list
279
280val do_store_init_data :
281  AST.ident List.list -> aSM_universe -> Z.z -> AST.init_data ->
282  ASM.labelled_instruction List.list
283
284val do_store_init_data_list :
285  AST.ident List.list -> aSM_universe -> Z.z -> AST.init_data List.list ->
286  ASM.labelled_instruction List.list
287
288val translate_initialization :
289  LIN.lin_program -> ASM.labelled_instruction List.list
290  Monad.smax_def__o__monad
291
292val get_symboltable :
293  AST.ident List.list -> (ASM.identifier, AST.ident) Types.prod List.list
294  Monad.smax_def__o__monad
295
296val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program Types.option
297
Note: See TracBrowser for help on using the repository browser.