source: extracted/rTLabsToRTL.mli @ 2746

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

Exported again.

File size: 10.7 KB
Line 
1open Preamble
2
3open Graphs
4
5open Order
6
7open Registers
8
9open FrontEndVal
10
11open Hide
12
13open ByteValues
14
15open GenMem
16
17open FrontEndMem
18
19open Division
20
21open Z
22
23open BitVectorZ
24
25open Pointers
26
27open Coqlib
28
29open Values
30
31open FrontEndOps
32
33open BitVectorTrie
34
35open CostLabel
36
37open Proper
38
39open PositiveMap
40
41open Deqsets
42
43open ErrorMessages
44
45open PreIdentifiers
46
47open Errors
48
49open Extralib
50
51open Setoids
52
53open Monad
54
55open Option
56
57open Lists
58
59open Positive
60
61open Identifiers
62
63open Exp
64
65open Arithmetic
66
67open Vector
68
69open Div_and_mod
70
71open Jmeq
72
73open Russell
74
75open List
76
77open Util
78
79open FoldStuff
80
81open BitVector
82
83open Extranat
84
85open Bool
86
87open Relations
88
89open Nat
90
91open Integers
92
93open Types
94
95open AST
96
97open Hints_declaration
98
99open Core_notation
100
101open Pts
102
103open Logic
104
105open RTLabs_syntax
106
107open String
108
109open Sets
110
111open Listb
112
113open LabelledObjects
114
115open I8051
116
117open BackEndOps
118
119open Joint
120
121open RTL
122
123open AssocList
124
125open Deqsets_extra
126
127open State
128
129open Bind_new
130
131open BindLists
132
133open Blocks
134
135open TranslateUtils
136
137val size_of_sig_type : AST.typ -> Nat.nat
138
139type register_type =
140| Register_int of Registers.register
141| Register_ptr of Registers.register * Registers.register
142
143val register_type_rect_Type4 :
144  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
145  'a1) -> register_type -> 'a1
146
147val register_type_rect_Type5 :
148  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
149  'a1) -> register_type -> 'a1
150
151val register_type_rect_Type3 :
152  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
153  'a1) -> register_type -> 'a1
154
155val register_type_rect_Type2 :
156  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
157  'a1) -> register_type -> 'a1
158
159val register_type_rect_Type1 :
160  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
161  'a1) -> register_type -> 'a1
162
163val register_type_rect_Type0 :
164  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
165  'a1) -> register_type -> 'a1
166
167val register_type_inv_rect_Type4 :
168  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
169  -> Registers.register -> __ -> 'a1) -> 'a1
170
171val register_type_inv_rect_Type3 :
172  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
173  -> Registers.register -> __ -> 'a1) -> 'a1
174
175val register_type_inv_rect_Type2 :
176  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
177  -> Registers.register -> __ -> 'a1) -> 'a1
178
179val register_type_inv_rect_Type1 :
180  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
181  -> Registers.register -> __ -> 'a1) -> 'a1
182
183val register_type_inv_rect_Type0 :
184  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
185  -> Registers.register -> __ -> 'a1) -> 'a1
186
187val register_type_discr : register_type -> register_type -> __
188
189val register_type_jmdiscr : register_type -> register_type -> __
190
191type local_env = Registers.register List.list Identifiers.identifier_map
192
193val find_local_env :
194  PreIdentifiers.identifier -> local_env -> Registers.register List.list
195
196val find_local_env_arg :
197  Registers.register -> local_env -> Joint.psd_argument List.list
198
199val m_iter : Monad.monad -> ('a1 -> __) -> Nat.nat -> __ -> __
200
201val fresh_registers :
202  Joint.params -> AST.ident List.list -> Nat.nat -> Registers.register
203  List.list Monad.smax_def__o__monad
204
205val map_list_local_env :
206  Registers.register List.list Identifiers.identifier_map ->
207  (Registers.register, AST.typ) Types.prod List.list -> Registers.register
208  List.list
209
210val initialize_local_env :
211  AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
212  -> local_env Monad.smax_def__o__monad
213
214val initialize_locals_params_ret :
215  AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
216  -> (Registers.register, AST.typ) Types.prod List.list ->
217  (Registers.register, AST.typ) Types.prod Types.option -> local_env
218  Monad.smax_def__o__monad
219
220val make_addr : 'a1 List.list -> ('a1, 'a1) Types.prod
221
222val find_and_addr :
223  PreIdentifiers.identifier -> local_env -> (Registers.register,
224  Registers.register) Types.prod
225
226val find_and_addr_arg :
227  Registers.register -> local_env -> (Joint.psd_argument, Joint.psd_argument)
228  Types.prod
229
230val rtl_args :
231  Registers.register List.list -> local_env -> Joint.psd_argument List.list
232
233val vrsplit :
234  Nat.nat -> Nat.nat -> 'a1 Vector.vector -> 'a1 Vector.vector List.list
235  Types.sig0
236
237val split_into_bytes :
238  AST.intsize -> AST.bvint -> BitVector.byte List.list Types.sig0
239
240val list_inject_All_aux : 'a1 List.list -> 'a1 Types.sig0 List.list
241
242val translate_op :
243  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
244  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
245  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
246
247val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list
248
249val translate_op_asym_unsigned :
250  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
251  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
252  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
253
254val nat_to_args :
255  Nat.nat -> Nat.nat -> Joint.psd_argument List.list Types.sig0
256
257val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat
258
259val translate_cst :
260  AST.typ -> AST.ident List.list -> FrontEndOps.constant Types.sig0 ->
261  Registers.register List.list -> (Registers.register, Joint.joint_seq
262  List.list) Bind_new.bind_new
263
264val translate_move :
265  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
266  List.list -> Joint.joint_seq List.list
267
268val sign_mask :
269  AST.ident List.list -> Registers.register -> Joint.psd_argument ->
270  Joint.joint_seq List.list
271
272val translate_cast_signed :
273  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
274  -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
275
276val translate_fill_with_zero :
277  AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
278  List.list
279
280val last : 'a1 List.list -> 'a1 Types.option
281
282val translate_op_asym_signed :
283  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
284  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
285  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
286
287val translate_cast :
288  AST.ident List.list -> AST.signedness -> Registers.register List.list ->
289  Registers.register List.list -> (Registers.register, Joint.joint_seq
290  List.list) Bind_new.bind_new
291
292val translate_notint :
293  AST.ident List.list -> Registers.register List.list -> Registers.register
294  List.list -> Joint.joint_seq List.list
295
296val translate_negint :
297  AST.ident List.list -> Registers.register List.list -> Registers.register
298  List.list -> (Registers.register, Joint.joint_seq List.list)
299  Bind_new.bind_new
300
301val translate_notbool :
302  AST.ident List.list -> Registers.register List.list -> Registers.register
303  List.list -> (Registers.register, Joint.joint_seq List.list)
304  Bind_new.bind_new
305
306val translate_op1 :
307  AST.ident List.list -> AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
308  Registers.register List.list -> Registers.register List.list ->
309  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
310
311val translate_mul_i :
312  AST.ident List.list -> Registers.register -> Registers.register -> Nat.nat
313  -> Registers.register List.list -> Joint.psd_argument List.list ->
314  Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 ->
315  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new ->
316  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
317
318val translate_mul :
319  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
320  List.list -> Joint.psd_argument List.list -> (Registers.register,
321  Joint.joint_seq List.list) Bind_new.bind_new
322
323val translate_divumodu8 :
324  AST.ident List.list -> Bool.bool -> Registers.register List.list ->
325  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
326  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
327
328val foldr2 :
329  ('a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> 'a1 List.list -> 'a2 List.list -> 'a3
330
331val translate_ne :
332  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
333  List.list -> Joint.psd_argument List.list -> (Registers.register,
334  Joint.joint_seq List.list) Bind_new.bind_new
335
336val translate_toggle_bool :
337  AST.ident List.list -> Registers.register List.list -> (Registers.register,
338  Joint.joint_seq List.list) Bind_new.bind_new
339
340val translate_lt_unsigned :
341  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
342  List.list -> Joint.psd_argument List.list -> (Registers.register,
343  Joint.joint_seq List.list) Bind_new.bind_new
344
345val shift_signed :
346  AST.ident List.list -> Registers.register -> Joint.psd_argument List.list
347  -> (Joint.psd_argument List.list, Joint.joint_seq List.list) Types.prod
348  Types.sig0
349
350val translate_lt_signed :
351  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
352  List.list -> Joint.psd_argument List.list -> (Registers.register,
353  Joint.joint_seq List.list) Bind_new.bind_new
354
355val translate_lt :
356  Bool.bool -> AST.ident List.list -> Registers.register List.list ->
357  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
358  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
359
360val translate_cmp :
361  Bool.bool -> AST.ident List.list -> Integers.comparison ->
362  Registers.register List.list -> Joint.psd_argument List.list ->
363  Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq)
364  BindLists.bind_list
365
366val translate_op2 :
367  AST.ident List.list -> AST.typ -> AST.typ -> AST.typ ->
368  FrontEndOps.binary_operation -> Registers.register List.list ->
369  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
370  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
371
372val translate_cond :
373  AST.ident List.list -> Registers.register List.list -> Graphs.label ->
374  Blocks.bind_step_block
375
376val translate_load :
377  AST.ident List.list -> Joint.psd_argument List.list -> Registers.register
378  List.list -> (Registers.register, Joint.joint_seq List.list)
379  Bind_new.bind_new
380
381val translate_store :
382  AST.ident List.list -> Joint.psd_argument List.list -> Joint.psd_argument
383  List.list -> (Registers.register, Joint.joint_seq List.list)
384  Bind_new.bind_new
385
386val ensure_bind_step_block :
387  Joint.params -> AST.ident List.list -> (Registers.register, Joint.joint_seq
388  List.list) Bind_new.bind_new -> Blocks.bind_step_block
389
390val translate_statement :
391  AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
392  -> local_env -> RTLabs_syntax.statement -> ((Blocks.bind_step_block,
393  Blocks.bind_fin_block) Types.sum, __) Types.dPair
394
395val translate_internal :
396  AST.ident List.list -> RTLabs_syntax.internal_function ->
397  Joint.joint_closed_internal_function
398
399val rtlabs_to_rtl : RTLabs_syntax.rTLabs_program -> RTL.rtl_program
400
Note: See TracBrowser for help on using the repository browser.