source: driver/extracted/eRTL.mli @ 3106

Last change on this file since 3106 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: 10.5 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
121type move_dst =
122| PSD of Registers.register
123| HDW of I8051.register
124
125val move_dst_rect_Type4 :
126  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
127
128val move_dst_rect_Type5 :
129  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
130
131val move_dst_rect_Type3 :
132  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
133
134val move_dst_rect_Type2 :
135  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
136
137val move_dst_rect_Type1 :
138  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
139
140val move_dst_rect_Type0 :
141  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
142
143val move_dst_inv_rect_Type4 :
144  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
145  'a1) -> 'a1
146
147val move_dst_inv_rect_Type3 :
148  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
149  'a1) -> 'a1
150
151val move_dst_inv_rect_Type2 :
152  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
153  'a1) -> 'a1
154
155val move_dst_inv_rect_Type1 :
156  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
157  'a1) -> 'a1
158
159val move_dst_inv_rect_Type0 :
160  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
161  'a1) -> 'a1
162
163val move_dst_discr : move_dst -> move_dst -> __
164
165val move_dst_jmdiscr : move_dst -> move_dst -> __
166
167type move_src = move_dst Joint.argument
168
169val move_src_from_dst : move_dst -> move_src
170
171val dpi1__o__move_dst_to_src__o__inject :
172  (move_dst, 'a1) Types.dPair -> move_src Types.sig0
173
174val eject__o__move_dst_to_src__o__inject :
175  move_dst Types.sig0 -> move_src Types.sig0
176
177val move_dst_to_src__o__inject : move_dst -> move_src Types.sig0
178
179val dpi1__o__move_dst_to_src : (move_dst, 'a1) Types.dPair -> move_src
180
181val eject__o__move_dst_to_src : move_dst Types.sig0 -> move_src
182
183val psd_argument_move_src : Joint.psd_argument -> move_src
184
185val byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
186  BitVector.byte -> move_src Types.sig0
187
188val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
189  (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
190
191val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
192  (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
193
194val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
195  (Registers.register, 'a1) Types.dPair -> move_src Types.sig0
196
197val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
198  BitVector.byte Types.sig0 -> move_src Types.sig0
199
200val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
201  BitVector.byte Types.sig0 -> move_src Types.sig0
202
203val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
204  Registers.register Types.sig0 -> move_src Types.sig0
205
206val reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
207  Registers.register -> move_src Types.sig0
208
209val dpi1__o__psd_argument_to_move_src__o__inject :
210  (Joint.psd_argument, 'a1) Types.dPair -> move_src Types.sig0
211
212val eject__o__psd_argument_to_move_src__o__inject :
213  Joint.psd_argument Types.sig0 -> move_src Types.sig0
214
215val psd_argument_to_move_src__o__inject :
216  Joint.psd_argument -> move_src Types.sig0
217
218val byte_to_psd_argument__o__psd_argument_to_move_src :
219  BitVector.byte -> move_src
220
221val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
222  (BitVector.byte, 'a1) Types.dPair -> move_src
223
224val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src :
225  (BitVector.byte, 'a1) Types.dPair -> move_src
226
227val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src :
228  (Registers.register, 'a1) Types.dPair -> move_src
229
230val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
231  BitVector.byte Types.sig0 -> move_src
232
233val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src :
234  BitVector.byte Types.sig0 -> move_src
235
236val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src :
237  Registers.register Types.sig0 -> move_src
238
239val reg_to_psd_argument__o__psd_argument_to_move_src :
240  Registers.register -> move_src
241
242val dpi1__o__psd_argument_to_move_src :
243  (Joint.psd_argument, 'a1) Types.dPair -> move_src
244
245val eject__o__psd_argument_to_move_src :
246  Joint.psd_argument Types.sig0 -> move_src
247
248type ertl_seq =
249| Ertl_new_frame
250| Ertl_del_frame
251| Ertl_frame_size of Registers.register
252
253val ertl_seq_rect_Type4 :
254  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
255
256val ertl_seq_rect_Type5 :
257  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
258
259val ertl_seq_rect_Type3 :
260  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
261
262val ertl_seq_rect_Type2 :
263  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
264
265val ertl_seq_rect_Type1 :
266  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
267
268val ertl_seq_rect_Type0 :
269  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
270
271val ertl_seq_inv_rect_Type4 :
272  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
273  -> 'a1
274
275val ertl_seq_inv_rect_Type3 :
276  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
277  -> 'a1
278
279val ertl_seq_inv_rect_Type2 :
280  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
281  -> 'a1
282
283val ertl_seq_inv_rect_Type1 :
284  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
285  -> 'a1
286
287val ertl_seq_inv_rect_Type0 :
288  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
289  -> 'a1
290
291val ertl_seq_discr : ertl_seq -> ertl_seq -> __
292
293val ertl_seq_jmdiscr : ertl_seq -> ertl_seq -> __
294
295val eRTL_uns : Joint.unserialized_params
296
297val regs_from_move_dst : move_dst -> Registers.register List.list
298
299val regs_from_move_src : move_src -> Registers.register List.list
300
301val ertl_ext_seq_regs : ertl_seq -> Registers.register List.list
302
303val eRTL_functs : Joint.get_pseudo_reg_functs
304
305val eRTL : Joint.graph_params
306
307type ertl_program = Joint.joint_program
308
309val dpi1__o__reg_to_ertl_snd_argument__o__inject :
310  (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
311
312val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
313  (Registers.register, 'a1) Types.dPair -> move_src Types.sig0
314
315val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
316  (Registers.register, 'a1) Types.dPair -> move_src
317
318val eject__o__reg_to_ertl_snd_argument__o__inject :
319  Registers.register Types.sig0 -> Joint.psd_argument Types.sig0
320
321val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
322  Registers.register Types.sig0 -> move_src Types.sig0
323
324val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
325  Registers.register Types.sig0 -> move_src
326
327val reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
328  Registers.register -> move_src
329
330val reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
331  Registers.register -> move_src Types.sig0
332
333val reg_to_ertl_snd_argument__o__inject :
334  Registers.register -> Joint.psd_argument Types.sig0
335
336val dpi1__o__reg_to_ertl_snd_argument :
337  (Registers.register, 'a1) Types.dPair -> Joint.psd_argument
338
339val eject__o__reg_to_ertl_snd_argument :
340  Registers.register Types.sig0 -> Joint.psd_argument
341
342val dpi1__o__byte_to_ertl_snd_argument__o__inject :
343  (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
344
345val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
346  (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
347
348val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
349  (BitVector.byte, 'a1) Types.dPair -> move_src
350
351val eject__o__byte_to_ertl_snd_argument__o__inject :
352  BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0
353
354val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
355  BitVector.byte Types.sig0 -> move_src Types.sig0
356
357val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
358  BitVector.byte Types.sig0 -> move_src
359
360val byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
361  BitVector.byte -> move_src
362
363val byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
364  BitVector.byte -> move_src Types.sig0
365
366val byte_to_ertl_snd_argument__o__inject :
367  BitVector.byte -> Joint.psd_argument Types.sig0
368
369val dpi1__o__byte_to_ertl_snd_argument :
370  (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument
371
372val eject__o__byte_to_ertl_snd_argument :
373  BitVector.byte Types.sig0 -> Joint.psd_argument
374
375val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq
376
377val dpi1__o__ertl_seq_to_joint_seq__o__inject :
378  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq Types.sig0
379
380val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
381  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step Types.sig0
382
383val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step :
384  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
385
386val eject__o__ertl_seq_to_joint_seq__o__inject :
387  AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0
388
389val eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
390  AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0
391
392val eject__o__ertl_seq_to_joint_seq__o__seq_to_step :
393  AST.ident List.list -> __ Types.sig0 -> Joint.joint_step
394
395val ertl_seq_to_joint_seq__o__seq_to_step :
396  AST.ident List.list -> __ -> Joint.joint_step
397
398val ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
399  AST.ident List.list -> __ -> Joint.joint_step Types.sig0
400
401val ertl_seq_to_joint_seq__o__inject :
402  AST.ident List.list -> __ -> Joint.joint_seq Types.sig0
403
404val dpi1__o__ertl_seq_to_joint_seq :
405  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
406
407val eject__o__ertl_seq_to_joint_seq :
408  AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq
409
410val eRTL_premain : ertl_program -> Joint.joint_closed_internal_function
411
Note: See TracBrowser for help on using the repository browser.