source: driver/extracted/rTLabsToRTL.mli @ 3106

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

New extraction, bugs fixed.

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