source: extracted/translateUtils.mli @ 2968

Last change on this file since 2968 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: 14.1 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
25open BitVectorTrie
26
27open Graphs
28
29open I8051
30
31open Order
32
33open Registers
34
35open CostLabel
36
37open Hide
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open Div_and_mod
78
79open Jmeq
80
81open Russell
82
83open List
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Types
92
93open Bool
94
95open Relations
96
97open Nat
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Positive
108
109open Z
110
111open BitVectorZ
112
113open Pointers
114
115open ByteValues
116
117open BackEndOps
118
119open Joint
120
121open State
122
123open Bind_new
124
125open BindLists
126
127open Blocks
128
129open Deqsets_extra
130
131val fresh_label :
132  Joint.params -> AST.ident List.list -> Graphs.label
133  Monad.smax_def__o__monad
134
135val fresh_register :
136  Joint.params -> AST.ident List.list -> Registers.register
137  Monad.smax_def__o__monad
138
139val adds_graph_pre :
140  Joint.graph_params -> AST.ident List.list -> (Graphs.label -> 'a1 ->
141  Joint.joint_seq) -> 'a1 List.list -> Graphs.label -> Graphs.label
142  Monad.smax_def__o__monad
143
144val adds_graph_post :
145  Joint.graph_params -> AST.ident List.list -> Joint.joint_seq List.list ->
146  Graphs.label -> Graphs.label Monad.smax_def__o__monad
147
148val adds_graph :
149  Joint.graph_params -> AST.ident List.list -> Blocks.step_block ->
150  Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
151  Joint.joint_internal_function
152
153val fin_adds_graph :
154  Joint.graph_params -> AST.ident List.list -> Blocks.fin_block ->
155  Graphs.label -> Joint.joint_internal_function ->
156  Joint.joint_internal_function
157
158val append_seq_list :
159  Joint.params -> AST.ident List.list -> Blocks.bind_step_block ->
160  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new ->
161  Blocks.bind_step_block
162
163val b_adds_graph :
164  Joint.graph_params -> AST.ident List.list -> Blocks.bind_step_block ->
165  Graphs.label -> Graphs.label -> Joint.joint_internal_function ->
166  Joint.joint_internal_function
167
168val b_fin_adds_graph :
169  Joint.graph_params -> AST.ident List.list -> Blocks.bind_fin_block ->
170  Graphs.label -> Joint.joint_internal_function ->
171  Joint.joint_internal_function
172
173val step_registers :
174  Joint.uns_params -> AST.ident List.list -> Joint.joint_step ->
175  Registers.register List.list
176
177val fin_step_registers :
178  Joint.uns_params -> Joint.joint_fin_step -> Registers.register List.list
179
180type b_graph_translate_data = { init_ret : __; init_params : __;
181                                init_stack_size : Nat.nat;
182                                added_prologue : Joint.joint_seq List.list;
183                                new_regs : Registers.register List.list;
184                                f_step : (Graphs.label -> Joint.joint_step ->
185                                         Blocks.bind_step_block);
186                                f_fin : (Graphs.label -> Joint.joint_fin_step
187                                        -> Blocks.bind_fin_block) }
188
189val b_graph_translate_data_rect_Type4 :
190  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
191  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
192  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
193  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
194  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
195
196val b_graph_translate_data_rect_Type5 :
197  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
198  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
199  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
200  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
201  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
202
203val b_graph_translate_data_rect_Type3 :
204  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
205  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
206  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
207  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
208  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
209
210val b_graph_translate_data_rect_Type2 :
211  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
212  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
213  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
214  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
215  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
216
217val b_graph_translate_data_rect_Type1 :
218  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
219  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
220  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
221  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
222  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
223
224val b_graph_translate_data_rect_Type0 :
225  Joint.graph_params -> Joint.graph_params -> AST.ident List.list -> (__ ->
226  __ -> Nat.nat -> Joint.joint_seq List.list -> Registers.register List.list
227  -> (Graphs.label -> Joint.joint_step -> Blocks.bind_step_block) ->
228  (Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block) -> __ -> __
229  -> __ -> __ -> 'a1) -> b_graph_translate_data -> 'a1
230
231val init_ret :
232  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
233  b_graph_translate_data -> __
234
235val init_params :
236  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
237  b_graph_translate_data -> __
238
239val init_stack_size :
240  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
241  b_graph_translate_data -> Nat.nat
242
243val added_prologue :
244  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
245  b_graph_translate_data -> Joint.joint_seq List.list
246
247val new_regs :
248  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
249  b_graph_translate_data -> Registers.register List.list
250
251val f_step :
252  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
253  b_graph_translate_data -> Graphs.label -> Joint.joint_step ->
254  Blocks.bind_step_block
255
256val f_fin :
257  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
258  b_graph_translate_data -> Graphs.label -> Joint.joint_fin_step ->
259  Blocks.bind_fin_block
260
261val b_graph_translate_data_inv_rect_Type4 :
262  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
263  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
264  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
265  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
266  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
267
268val b_graph_translate_data_inv_rect_Type3 :
269  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
270  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
271  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
272  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
273  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
274
275val b_graph_translate_data_inv_rect_Type2 :
276  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
277  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
278  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
279  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
280  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
281
282val b_graph_translate_data_inv_rect_Type1 :
283  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
284  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
285  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
286  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
287  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
288
289val b_graph_translate_data_inv_rect_Type0 :
290  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
291  b_graph_translate_data -> (__ -> __ -> Nat.nat -> Joint.joint_seq List.list
292  -> Registers.register List.list -> (Graphs.label -> Joint.joint_step ->
293  Blocks.bind_step_block) -> (Graphs.label -> Joint.joint_fin_step ->
294  Blocks.bind_fin_block) -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
295
296val b_graph_translate_data_jmdiscr :
297  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
298  b_graph_translate_data -> b_graph_translate_data -> __
299
300type bound_b_graph_translate_data =
301  (Registers.register, b_graph_translate_data) Bind_new.bind_new Types.sig0
302
303val get_first_costlabel :
304  Joint.params -> AST.ident List.list -> Joint.joint_closed_internal_function
305  -> (CostLabel.costlabel, __) Types.prod
306
307val b_graph_translate_props_rect_Type4 :
308  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
309  b_graph_translate_data -> Joint.joint_closed_internal_function ->
310  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
311  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
312  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
313
314val b_graph_translate_props_rect_Type5 :
315  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
316  b_graph_translate_data -> Joint.joint_closed_internal_function ->
317  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
318  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
319  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
320
321val b_graph_translate_props_rect_Type3 :
322  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
323  b_graph_translate_data -> Joint.joint_closed_internal_function ->
324  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
325  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
326  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
327
328val b_graph_translate_props_rect_Type2 :
329  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
330  b_graph_translate_data -> Joint.joint_closed_internal_function ->
331  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
332  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
333  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
334
335val b_graph_translate_props_rect_Type1 :
336  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
337  b_graph_translate_data -> Joint.joint_closed_internal_function ->
338  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
339  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
340  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
341
342val b_graph_translate_props_rect_Type0 :
343  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
344  b_graph_translate_data -> Joint.joint_closed_internal_function ->
345  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
346  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
347  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
348
349val b_graph_translate_props_inv_rect_Type4 :
350  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
351  b_graph_translate_data -> Joint.joint_closed_internal_function ->
352  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
353  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
354  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
355
356val b_graph_translate_props_inv_rect_Type3 :
357  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
358  b_graph_translate_data -> Joint.joint_closed_internal_function ->
359  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
360  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
361  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
362
363val b_graph_translate_props_inv_rect_Type2 :
364  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
365  b_graph_translate_data -> Joint.joint_closed_internal_function ->
366  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
367  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
368  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
369
370val b_graph_translate_props_inv_rect_Type1 :
371  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
372  b_graph_translate_data -> Joint.joint_closed_internal_function ->
373  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
374  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
375  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
376
377val b_graph_translate_props_inv_rect_Type0 :
378  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
379  b_graph_translate_data -> Joint.joint_closed_internal_function ->
380  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
381  List.list) -> (Graphs.label -> Registers.register List.list) -> (__ -> __
382  -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
383
384val b_graph_translate_props_jmdiscr :
385  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
386  b_graph_translate_data -> Joint.joint_closed_internal_function ->
387  Joint.joint_closed_internal_function -> (Graphs.label -> Graphs.label
388  List.list) -> (Graphs.label -> Registers.register List.list) -> __
389
390val pair_swap : ('a1, 'a2) Types.prod -> ('a2, 'a1) Types.prod
391
392val b_graph_translate :
393  Joint.graph_params -> Joint.graph_params -> AST.ident List.list ->
394  bound_b_graph_translate_data -> Joint.joint_closed_internal_function ->
395  Joint.joint_closed_internal_function Types.sig0
396
397val b_graph_transform_program :
398  Joint.graph_params -> Joint.graph_params -> (AST.ident List.list ->
399  Joint.joint_closed_internal_function -> bound_b_graph_translate_data) ->
400  Joint.joint_program -> Joint.joint_program
401
402val added_registers :
403  Joint.graph_params -> AST.ident List.list -> Joint.joint_internal_function
404  -> (Graphs.label -> Registers.register List.list) -> Registers.register
405  List.list
406
Note: See TracBrowser for help on using the repository browser.