source: extracted/eRTL.mli @ 2797

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

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File size: 10.3 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open BitVectorTrie
12
13open Graphs
14
15open I8051
16
17open Order
18
19open Registers
20
21open CostLabel
22
23open Hide
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
53open Setoids
54
55open Monad
56
57open Option
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open List
70
71open Util
72
73open FoldStuff
74
75open BitVector
76
77open Types
78
79open Bool
80
81open Relations
82
83open Nat
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107type move_dst =
108| PSD of Registers.register
109| HDW of I8051.register
110
111val move_dst_rect_Type4 :
112  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
113
114val move_dst_rect_Type5 :
115  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
116
117val move_dst_rect_Type3 :
118  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
119
120val move_dst_rect_Type2 :
121  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
122
123val move_dst_rect_Type1 :
124  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
125
126val move_dst_rect_Type0 :
127  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
128
129val move_dst_inv_rect_Type4 :
130  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
131  'a1) -> 'a1
132
133val move_dst_inv_rect_Type3 :
134  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
135  'a1) -> 'a1
136
137val move_dst_inv_rect_Type2 :
138  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
139  'a1) -> 'a1
140
141val move_dst_inv_rect_Type1 :
142  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
143  'a1) -> 'a1
144
145val move_dst_inv_rect_Type0 :
146  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
147  'a1) -> 'a1
148
149val move_dst_discr : move_dst -> move_dst -> __
150
151val move_dst_jmdiscr : move_dst -> move_dst -> __
152
153type move_src = move_dst Joint.argument
154
155val move_src_from_dst : move_dst -> move_src
156
157val dpi1__o__move_dst_to_src__o__inject :
158  (move_dst, 'a1) Types.dPair -> move_src Types.sig0
159
160val eject__o__move_dst_to_src__o__inject :
161  move_dst Types.sig0 -> move_src Types.sig0
162
163val move_dst_to_src__o__inject : move_dst -> move_src Types.sig0
164
165val dpi1__o__move_dst_to_src : (move_dst, 'a1) Types.dPair -> move_src
166
167val eject__o__move_dst_to_src : move_dst Types.sig0 -> move_src
168
169val psd_argument_move_src : Joint.psd_argument -> move_src
170
171val byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
172  BitVector.byte -> move_src Types.sig0
173
174val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
175  (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
176
177val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
178  (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
179
180val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
181  (Registers.register, 'a1) Types.dPair -> move_src Types.sig0
182
183val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
184  BitVector.byte Types.sig0 -> move_src Types.sig0
185
186val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
187  BitVector.byte Types.sig0 -> move_src Types.sig0
188
189val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
190  Registers.register Types.sig0 -> move_src Types.sig0
191
192val reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
193  Registers.register -> move_src Types.sig0
194
195val dpi1__o__psd_argument_to_move_src__o__inject :
196  (Joint.psd_argument, 'a1) Types.dPair -> move_src Types.sig0
197
198val eject__o__psd_argument_to_move_src__o__inject :
199  Joint.psd_argument Types.sig0 -> move_src Types.sig0
200
201val psd_argument_to_move_src__o__inject :
202  Joint.psd_argument -> move_src Types.sig0
203
204val byte_to_psd_argument__o__psd_argument_to_move_src :
205  BitVector.byte -> move_src
206
207val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
208  (BitVector.byte, 'a1) Types.dPair -> move_src
209
210val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src :
211  (BitVector.byte, 'a1) Types.dPair -> move_src
212
213val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src :
214  (Registers.register, 'a1) Types.dPair -> move_src
215
216val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
217  BitVector.byte Types.sig0 -> move_src
218
219val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src :
220  BitVector.byte Types.sig0 -> move_src
221
222val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src :
223  Registers.register Types.sig0 -> move_src
224
225val reg_to_psd_argument__o__psd_argument_to_move_src :
226  Registers.register -> move_src
227
228val dpi1__o__psd_argument_to_move_src :
229  (Joint.psd_argument, 'a1) Types.dPair -> move_src
230
231val eject__o__psd_argument_to_move_src :
232  Joint.psd_argument Types.sig0 -> move_src
233
234type ertl_seq =
235| Ertl_new_frame
236| Ertl_del_frame
237| Ertl_frame_size of Registers.register
238
239val ertl_seq_rect_Type4 :
240  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
241
242val ertl_seq_rect_Type5 :
243  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
244
245val ertl_seq_rect_Type3 :
246  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
247
248val ertl_seq_rect_Type2 :
249  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
250
251val ertl_seq_rect_Type1 :
252  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
253
254val ertl_seq_rect_Type0 :
255  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
256
257val ertl_seq_inv_rect_Type4 :
258  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
259  -> 'a1
260
261val ertl_seq_inv_rect_Type3 :
262  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
263  -> 'a1
264
265val ertl_seq_inv_rect_Type2 :
266  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
267  -> 'a1
268
269val ertl_seq_inv_rect_Type1 :
270  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
271  -> 'a1
272
273val ertl_seq_inv_rect_Type0 :
274  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
275  -> 'a1
276
277val ertl_seq_discr : ertl_seq -> ertl_seq -> __
278
279val ertl_seq_jmdiscr : ertl_seq -> ertl_seq -> __
280
281val eRTL_uns : Joint.unserialized_params
282
283val regs_from_move_dst : move_dst -> Registers.register List.list
284
285val regs_from_move_src : move_src -> Registers.register List.list
286
287val ertl_ext_seq_regs : ertl_seq -> Registers.register List.list
288
289val eRTL_functs : Joint.get_pseudo_reg_functs
290
291val eRTL : Joint.graph_params
292
293type ertl_program = Joint.joint_program
294
295val dpi1__o__reg_to_ertl_snd_argument__o__inject :
296  (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
297
298val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
299  (Registers.register, 'a1) Types.dPair -> move_src Types.sig0
300
301val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
302  (Registers.register, 'a1) Types.dPair -> move_src
303
304val eject__o__reg_to_ertl_snd_argument__o__inject :
305  Registers.register Types.sig0 -> Joint.psd_argument Types.sig0
306
307val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
308  Registers.register Types.sig0 -> move_src Types.sig0
309
310val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
311  Registers.register Types.sig0 -> move_src
312
313val reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
314  Registers.register -> move_src
315
316val reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
317  Registers.register -> move_src Types.sig0
318
319val reg_to_ertl_snd_argument__o__inject :
320  Registers.register -> Joint.psd_argument Types.sig0
321
322val dpi1__o__reg_to_ertl_snd_argument :
323  (Registers.register, 'a1) Types.dPair -> Joint.psd_argument
324
325val eject__o__reg_to_ertl_snd_argument :
326  Registers.register Types.sig0 -> Joint.psd_argument
327
328val dpi1__o__byte_to_ertl_snd_argument__o__inject :
329  (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
330
331val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
332  (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
333
334val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
335  (BitVector.byte, 'a1) Types.dPair -> move_src
336
337val eject__o__byte_to_ertl_snd_argument__o__inject :
338  BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0
339
340val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
341  BitVector.byte Types.sig0 -> move_src Types.sig0
342
343val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
344  BitVector.byte Types.sig0 -> move_src
345
346val byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
347  BitVector.byte -> move_src
348
349val byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
350  BitVector.byte -> move_src Types.sig0
351
352val byte_to_ertl_snd_argument__o__inject :
353  BitVector.byte -> Joint.psd_argument Types.sig0
354
355val dpi1__o__byte_to_ertl_snd_argument :
356  (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument
357
358val eject__o__byte_to_ertl_snd_argument :
359  BitVector.byte Types.sig0 -> Joint.psd_argument
360
361val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq
362
363val dpi1__o__ertl_seq_to_joint_seq__o__inject :
364  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq Types.sig0
365
366val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
367  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step Types.sig0
368
369val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step :
370  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
371
372val eject__o__ertl_seq_to_joint_seq__o__inject :
373  AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0
374
375val eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
376  AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0
377
378val eject__o__ertl_seq_to_joint_seq__o__seq_to_step :
379  AST.ident List.list -> __ Types.sig0 -> Joint.joint_step
380
381val ertl_seq_to_joint_seq__o__seq_to_step :
382  AST.ident List.list -> __ -> Joint.joint_step
383
384val ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
385  AST.ident List.list -> __ -> Joint.joint_step Types.sig0
386
387val ertl_seq_to_joint_seq__o__inject :
388  AST.ident List.list -> __ -> Joint.joint_seq Types.sig0
389
390val dpi1__o__ertl_seq_to_joint_seq :
391  AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
392
393val eject__o__ertl_seq_to_joint_seq :
394  AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq
395
Note: See TracBrowser for help on using the repository browser.