source: extracted/rTLabsToRTL.mli @ 2951

Last change on this file since 2951 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.8 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 Extra_bool
108
109open Globalenvs
110
111open String
112
113open Sets
114
115open Listb
116
117open LabelledObjects
118
119open I8051
120
121open BackEndOps
122
123open Joint
124
125open RTL
126
127open Deqsets_extra
128
129open State
130
131open Bind_new
132
133open BindLists
134
135open Blocks
136
137open TranslateUtils
138
139val size_of_sig_type : AST.typ -> Nat.nat
140
141type register_type =
142| Register_int of Registers.register
143| Register_ptr of Registers.register * Registers.register
144
145val register_type_rect_Type4 :
146  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
147  'a1) -> register_type -> 'a1
148
149val register_type_rect_Type5 :
150  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
151  'a1) -> register_type -> 'a1
152
153val register_type_rect_Type3 :
154  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
155  'a1) -> register_type -> 'a1
156
157val register_type_rect_Type2 :
158  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
159  'a1) -> register_type -> 'a1
160
161val register_type_rect_Type1 :
162  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
163  'a1) -> register_type -> 'a1
164
165val register_type_rect_Type0 :
166  (Registers.register -> 'a1) -> (Registers.register -> Registers.register ->
167  'a1) -> register_type -> 'a1
168
169val register_type_inv_rect_Type4 :
170  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
171  -> Registers.register -> __ -> 'a1) -> 'a1
172
173val register_type_inv_rect_Type3 :
174  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
175  -> Registers.register -> __ -> 'a1) -> 'a1
176
177val register_type_inv_rect_Type2 :
178  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
179  -> Registers.register -> __ -> 'a1) -> 'a1
180
181val register_type_inv_rect_Type1 :
182  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
183  -> Registers.register -> __ -> 'a1) -> 'a1
184
185val register_type_inv_rect_Type0 :
186  register_type -> (Registers.register -> __ -> 'a1) -> (Registers.register
187  -> Registers.register -> __ -> 'a1) -> 'a1
188
189val register_type_discr : register_type -> register_type -> __
190
191val register_type_jmdiscr : register_type -> register_type -> __
192
193type local_env = Registers.register List.list Identifiers.identifier_map
194
195val find_local_env :
196  PreIdentifiers.identifier -> local_env -> Registers.register List.list
197
198val find_local_env_arg :
199  Registers.register -> local_env -> Joint.psd_argument List.list
200
201val m_iter : Monad.monad -> ('a1 -> __) -> Nat.nat -> __ -> __
202
203val fresh_registers :
204  Joint.params -> AST.ident List.list -> Nat.nat -> Registers.register
205  List.list Monad.smax_def__o__monad
206
207val map_list_local_env :
208  Registers.register List.list Identifiers.identifier_map ->
209  (Registers.register, AST.typ) Types.prod List.list -> Registers.register
210  List.list
211
212val initialize_local_env :
213  AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
214  -> local_env Monad.smax_def__o__monad
215
216val initialize_locals_params_ret :
217  AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
218  -> (Registers.register, AST.typ) Types.prod List.list ->
219  (Registers.register, AST.typ) Types.prod Types.option -> local_env
220  Monad.smax_def__o__monad
221
222val make_addr : 'a1 List.list -> ('a1, 'a1) Types.prod
223
224val find_and_addr :
225  PreIdentifiers.identifier -> local_env -> (Registers.register,
226  Registers.register) Types.prod
227
228val find_and_addr_arg :
229  Registers.register -> local_env -> (Joint.psd_argument, Joint.psd_argument)
230  Types.prod
231
232val rtl_args :
233  Registers.register List.list -> local_env -> Joint.psd_argument List.list
234
235val vrsplit :
236  Nat.nat -> Nat.nat -> 'a1 Vector.vector -> 'a1 Vector.vector List.list
237  Types.sig0
238
239val split_into_bytes :
240  AST.intsize -> AST.bvint -> BitVector.byte List.list Types.sig0
241
242val list_inject_All_aux : 'a1 List.list -> 'a1 Types.sig0 List.list
243
244val translate_op_aux :
245  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
246  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
247  Joint.joint_seq List.list
248
249val translate_op :
250  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
251  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
252  Joint.joint_seq List.list
253
254val cast_list : 'a1 -> Nat.nat -> 'a1 List.list -> 'a1 List.list
255
256val translate_op_asym_unsigned :
257  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
258  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
259  Joint.joint_seq List.list
260
261val zero_args : Nat.nat -> Joint.psd_argument List.list Types.sig0
262
263val one_args : Nat.nat -> Joint.psd_argument List.list Types.sig0
264
265val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat
266
267val translate_cst :
268  AST.typ -> AST.ident List.list -> FrontEndOps.constant Types.sig0 ->
269  Registers.register List.list -> (Registers.register, Joint.joint_seq
270  List.list) Bind_new.bind_new
271
272val translate_move :
273  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
274  List.list -> Joint.joint_seq List.list
275
276val sign_mask :
277  AST.ident List.list -> Registers.register -> Joint.psd_argument ->
278  Joint.joint_seq List.list
279
280val translate_cast_signed :
281  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
282  -> (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
283
284val translate_fill_with_zero :
285  AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
286  List.list
287
288val last : 'a1 List.list -> 'a1 Types.option
289
290val translate_op_asym_signed :
291  AST.ident List.list -> BackEndOps.op2 -> Registers.register List.list ->
292  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
293  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
294
295val translate_cast :
296  AST.ident List.list -> AST.signedness -> Registers.register List.list ->
297  Registers.register List.list -> (Registers.register, Joint.joint_seq
298  List.list) Bind_new.bind_new
299
300val translate_notint :
301  AST.ident List.list -> Registers.register List.list -> Registers.register
302  List.list -> Joint.joint_seq List.list
303
304val translate_negint :
305  AST.ident List.list -> Registers.register List.list -> Registers.register
306  List.list -> Joint.joint_seq List.list
307
308val translate_notbool :
309  AST.ident List.list -> Registers.register List.list -> Registers.register
310  List.list -> (Registers.register, Joint.joint_seq List.list)
311  Bind_new.bind_new
312
313val translate_op1 :
314  AST.ident List.list -> AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
315  Registers.register List.list -> Registers.register List.list ->
316  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
317
318val translate_mul_i :
319  AST.ident List.list -> Registers.register -> Registers.register -> Nat.nat
320  -> Registers.register List.list -> Joint.psd_argument List.list ->
321  Joint.psd_argument List.list -> Nat.nat -> Nat.nat Types.sig0 ->
322  Joint.joint_seq List.list -> Joint.joint_seq List.list
323
324val translate_mul :
325  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
326  List.list -> Joint.psd_argument List.list -> (Registers.register,
327  Joint.joint_seq List.list) Bind_new.bind_new
328
329val translate_divumodu8 :
330  AST.ident List.list -> Bool.bool -> Registers.register List.list ->
331  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
332  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
333
334val foldr2 :
335  ('a1 -> 'a2 -> 'a3 -> 'a3) -> 'a3 -> 'a1 List.list -> 'a2 List.list -> 'a3
336
337val translate_ne :
338  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
339  List.list -> Joint.psd_argument List.list -> (Registers.register,
340  Joint.joint_seq List.list) Bind_new.bind_new
341
342val translate_toggle_bool :
343  AST.ident List.list -> Registers.register List.list -> (Registers.register,
344  Joint.joint_seq List.list) Bind_new.bind_new
345
346val translate_lt_unsigned :
347  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
348  List.list -> Joint.psd_argument List.list -> (Registers.register,
349  Joint.joint_seq List.list) Bind_new.bind_new
350
351val shift_signed :
352  AST.ident List.list -> Registers.register -> Joint.psd_argument List.list
353  -> (Joint.psd_argument List.list, Joint.joint_seq List.list) Types.prod
354  Types.sig0
355
356val translate_lt_signed :
357  AST.ident List.list -> Registers.register List.list -> Joint.psd_argument
358  List.list -> Joint.psd_argument List.list -> (Registers.register,
359  Joint.joint_seq List.list) Bind_new.bind_new
360
361val translate_lt :
362  Bool.bool -> AST.ident List.list -> Registers.register List.list ->
363  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
364  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
365
366val translate_cmp :
367  Bool.bool -> AST.ident List.list -> Integers.comparison ->
368  Registers.register List.list -> Joint.psd_argument List.list ->
369  Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq)
370  BindLists.bind_list
371
372val translate_op2 :
373  AST.ident List.list -> AST.typ -> AST.typ -> AST.typ ->
374  FrontEndOps.binary_operation -> Registers.register List.list ->
375  Joint.psd_argument List.list -> Joint.psd_argument List.list ->
376  (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new
377
378val translate_cond :
379  AST.ident List.list -> Registers.register List.list -> Graphs.label ->
380  Blocks.bind_step_block
381
382val translate_load :
383  AST.ident List.list -> Joint.psd_argument List.list -> Registers.register
384  List.list -> (Registers.register, Joint.joint_seq List.list)
385  Bind_new.bind_new
386
387val translate_store :
388  AST.ident List.list -> Joint.psd_argument List.list -> Joint.psd_argument
389  List.list -> (Registers.register, Joint.joint_seq List.list)
390  Bind_new.bind_new
391
392val ensure_bind_step_block :
393  Joint.params -> AST.ident List.list -> (Registers.register, Joint.joint_seq
394  List.list) Bind_new.bind_new -> Blocks.bind_step_block
395
396val translate_statement :
397  AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
398  -> local_env -> RTLabs_syntax.statement -> ((Blocks.bind_step_block,
399  Blocks.bind_fin_block) Types.sum, __) Types.dPair
400
401val translate_internal :
402  AST.ident List.list -> RTLabs_syntax.internal_function ->
403  Joint.joint_closed_internal_function
404
405val rtlabs_to_rtl :
406  CostLabel.costlabel -> RTLabs_syntax.rTLabs_program -> RTL.rtl_program
407
Note: See TracBrowser for help on using the repository browser.