source: extracted/rTLabsToRTL.mli @ 2867

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

New extraction after indianess bug fixes by Paolo.

File size: 10.9 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_aux :
241  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
242  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
243  Joint.joint_seq List.list
244
245val translate_op :
246  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
247  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
248  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
249
250val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list
251
252val translate_op_asym_unsigned :
253  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
254  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
255  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
256
257val zero_args : Nat.nat -> Joint.psd_argument List.list Types.sig0
258
259val one_args : Nat.nat -> Joint.psd_argument List.list Types.sig0
260
261val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat
262
263val translate_cst :
264  AST.typ -> AST.ident List.list -> FrontEndOps.constant Types.sig0 ->
265  Registers.register List.list -> (Registers.register, Joint.joint_seq
266  List.list) Bind_new.bind_new
267
268val translate_move :
269  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
270  List.list -> Joint.joint_seq List.list
271
272val sign_mask :
273  AST.ident List.list -> Registers.register -> Joint.psd_argument ->
274  Joint.joint_seq List.list
275
276val translate_cast_signed :
277  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
278  -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
279
280val translate_fill_with_zero :
281  AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
282  List.list
283
284val last : 'a1 List.list -> 'a1 Types.option
285
286val translate_op_asym_signed :
287  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
288  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
289  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
290
291val translate_cast :
292  AST.ident List.list -> AST.signedness -> Registers.register List.list ->
293  Registers.register List.list -> (Registers.register, Joint.joint_seq
294  List.list) Bind_new.bind_new
295
296val translate_notint :
297  AST.ident List.list -> Registers.register List.list -> Registers.register
298  List.list -> Joint.joint_seq List.list
299
300val translate_negint :
301  AST.ident List.list -> Registers.register List.list -> Registers.register
302  List.list -> (Registers.register, Joint.joint_seq List.list)
303  Bind_new.bind_new
304
305val translate_notbool :
306  AST.ident List.list -> Registers.register List.list -> Registers.register
307  List.list -> (Registers.register, Joint.joint_seq List.list)
308  Bind_new.bind_new
309
310val translate_op1 :
311  AST.ident List.list -> AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
312  Registers.register List.list -> Registers.register List.list ->
313  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
314
315val translate_mul_i :
316  AST.ident List.list -> Registers.register -> Registers.register -> Nat.nat
317  -> Registers.register List.list -> Joint.psd_argument List.list ->
318  Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 ->
319  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new ->
320  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
321
322val translate_mul :
323  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
324  List.list -> Joint.psd_argument List.list -> (Registers.register,
325  Joint.joint_seq List.list) Bind_new.bind_new
326
327val translate_divumodu8 :
328  AST.ident List.list -> Bool.bool -> Registers.register List.list ->
329  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
330  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
331
332val foldr2 :
333  ('a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> 'a1 List.list -> 'a2 List.list -> 'a3
334
335val translate_ne :
336  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
337  List.list -> Joint.psd_argument List.list -> (Registers.register,
338  Joint.joint_seq List.list) Bind_new.bind_new
339
340val translate_toggle_bool :
341  AST.ident List.list -> Registers.register List.list -> (Registers.register,
342  Joint.joint_seq List.list) Bind_new.bind_new
343
344val translate_lt_unsigned :
345  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
346  List.list -> Joint.psd_argument List.list -> (Registers.register,
347  Joint.joint_seq List.list) Bind_new.bind_new
348
349val shift_signed :
350  AST.ident List.list -> Registers.register -> Joint.psd_argument List.list
351  -> (Joint.psd_argument List.list, Joint.joint_seq List.list) Types.prod
352  Types.sig0
353
354val translate_lt_signed :
355  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
356  List.list -> Joint.psd_argument List.list -> (Registers.register,
357  Joint.joint_seq List.list) Bind_new.bind_new
358
359val translate_lt :
360  Bool.bool -> AST.ident List.list -> Registers.register List.list ->
361  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
362  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
363
364val translate_cmp :
365  Bool.bool -> AST.ident List.list -> Integers.comparison ->
366  Registers.register List.list -> Joint.psd_argument List.list ->
367  Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq)
368  BindLists.bind_list
369
370val translate_op2 :
371  AST.ident List.list -> AST.typ -> AST.typ -> AST.typ ->
372  FrontEndOps.binary_operation -> Registers.register List.list ->
373  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
374  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
375
376val translate_cond :
377  AST.ident List.list -> Registers.register List.list -> Graphs.label ->
378  Blocks.bind_step_block
379
380val translate_load :
381  AST.ident List.list -> Joint.psd_argument List.list -> Registers.register
382  List.list -> (Registers.register, Joint.joint_seq List.list)
383  Bind_new.bind_new
384
385val translate_store :
386  AST.ident List.list -> Joint.psd_argument List.list -> Joint.psd_argument
387  List.list -> (Registers.register, Joint.joint_seq List.list)
388  Bind_new.bind_new
389
390val ensure_bind_step_block :
391  Joint.params -> AST.ident List.list -> (Registers.register, Joint.joint_seq
392  List.list) Bind_new.bind_new -> Blocks.bind_step_block
393
394val translate_statement :
395  AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
396  -> local_env -> RTLabs_syntax.statement -> ((Blocks.bind_step_block,
397  Blocks.bind_fin_block) Types.sum, __) Types.dPair
398
399val translate_internal :
400  AST.ident List.list -> RTLabs_syntax.internal_function ->
401  Joint.joint_closed_internal_function
402
403val rtlabs_to_rtl : RTLabs_syntax.rTLabs_program -> RTL.rtl_program
404
Note: See TracBrowser for help on using the repository browser.