source: extracted/rTLabsToRTL.mli @ 2817

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

The compiler now computes also the stack cost model.

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