source: driver/extracted/eRTLToLTL.mli @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 8.5 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open GenMem
12
13open FrontEndMem
14
15open Globalenvs
16
17open String
18
19open Sets
20
21open Listb
22
23open LabelledObjects
24
25open BitVectorTrie
26
27open Graphs
28
29open I8051
30
31open Order
32
33open Registers
34
35open CostLabel
36
37open Hide
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open ErrorMessages
46
47open PreIdentifiers
48
49open Errors
50
51open Extralib
52
53open Lists
54
55open Identifiers
56
57open Integers
58
59open AST
60
61open Division
62
63open Exp
64
65open Arithmetic
66
67open Setoids
68
69open Monad
70
71open Option
72
73open Extranat
74
75open Vector
76
77open Div_and_mod
78
79open Jmeq
80
81open Russell
82
83open List
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Types
92
93open Bool
94
95open Relations
96
97open Nat
98
99open Hints_declaration
100
101open Core_notation
102
103open Pts
104
105open Logic
106
107open Positive
108
109open Z
110
111open BitVectorZ
112
113open Pointers
114
115open ByteValues
116
117open BackEndOps
118
119open Joint
120
121open Joint_LTL_LIN
122
123open LTL
124
125open Fixpoints
126
127open Set_adt
128
129open ERTL
130
131open Liveness
132
133open Interference
134
135open Deqsets_extra
136
137open State
138
139open Bind_new
140
141open BindLists
142
143open Blocks
144
145open TranslateUtils
146
147val dpi1__o__Reg_to_dec__o__inject :
148  (I8051.register, 'a1) Types.dPair -> Interference.decision Types.sig0
149
150val eject__o__Reg_to_dec__o__inject :
151  I8051.register Types.sig0 -> Interference.decision Types.sig0
152
153val reg_to_dec__o__inject :
154  I8051.register -> Interference.decision Types.sig0
155
156val dpi1__o__Reg_to_dec :
157  (I8051.register, 'a1) Types.dPair -> Interference.decision
158
159val eject__o__Reg_to_dec : I8051.register Types.sig0 -> Interference.decision
160
161type arg_decision =
162| Arg_decision_colour of I8051.register
163| Arg_decision_spill of Nat.nat
164| Arg_decision_imm of BitVector.byte
165
166val arg_decision_rect_Type4 :
167  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
168  arg_decision -> 'a1
169
170val arg_decision_rect_Type5 :
171  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
172  arg_decision -> 'a1
173
174val arg_decision_rect_Type3 :
175  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
176  arg_decision -> 'a1
177
178val arg_decision_rect_Type2 :
179  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
180  arg_decision -> 'a1
181
182val arg_decision_rect_Type1 :
183  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
184  arg_decision -> 'a1
185
186val arg_decision_rect_Type0 :
187  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
188  arg_decision -> 'a1
189
190val arg_decision_inv_rect_Type4 :
191  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
192  (BitVector.byte -> __ -> 'a1) -> 'a1
193
194val arg_decision_inv_rect_Type3 :
195  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
196  (BitVector.byte -> __ -> 'a1) -> 'a1
197
198val arg_decision_inv_rect_Type2 :
199  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
200  (BitVector.byte -> __ -> 'a1) -> 'a1
201
202val arg_decision_inv_rect_Type1 :
203  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
204  (BitVector.byte -> __ -> 'a1) -> 'a1
205
206val arg_decision_inv_rect_Type0 :
207  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
208  (BitVector.byte -> __ -> 'a1) -> 'a1
209
210val arg_decision_discr : arg_decision -> arg_decision -> __
211
212val arg_decision_jmdiscr : arg_decision -> arg_decision -> __
213
214val dpi1__o__Reg_to_arg_dec__o__inject :
215  (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0
216
217val eject__o__Reg_to_arg_dec__o__inject :
218  I8051.register Types.sig0 -> arg_decision Types.sig0
219
220val reg_to_arg_dec__o__inject : I8051.register -> arg_decision Types.sig0
221
222val dpi1__o__Reg_to_arg_dec :
223  (I8051.register, 'a1) Types.dPair -> arg_decision
224
225val eject__o__Reg_to_arg_dec : I8051.register Types.sig0 -> arg_decision
226
227val preserve_carry_bit :
228  AST.ident List.list -> Bool.bool -> Joint.joint_seq List.list ->
229  Joint.joint_seq List.list
230
231val a : Types.unit0
232
233val dpi1__o__beval_of_byte__o__inject :
234  (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval Types.sig0
235
236val eject__o__beval_of_byte__o__inject :
237  BitVector.byte Types.sig0 -> ByteValues.beval Types.sig0
238
239val beval_of_byte__o__inject : BitVector.byte -> ByteValues.beval Types.sig0
240
241val dpi1__o__beval_of_byte :
242  (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval
243
244val eject__o__beval_of_byte : BitVector.byte Types.sig0 -> ByteValues.beval
245
246val set_dp_by_offset :
247  AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
248
249val get_stack :
250  AST.ident List.list -> Nat.nat -> I8051.register -> Nat.nat ->
251  Joint.joint_seq List.list
252
253val set_stack_not_a :
254  AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
255  Joint.joint_seq List.list
256
257val set_stack_a :
258  AST.ident List.list -> Nat.nat -> Nat.nat -> Joint.joint_seq List.list
259
260val set_stack :
261  AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
262  Joint.joint_seq List.list
263
264val set_stack_int :
265  AST.ident List.list -> Nat.nat -> Nat.nat -> BitVector.byte ->
266  Joint.joint_seq List.list
267
268val move :
269  AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
270  arg_decision -> Joint.joint_seq List.list
271
272val arg_is_spilled : arg_decision -> Bool.bool
273
274val is_spilled : Interference.decision -> Bool.bool
275
276val newframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
277
278val delframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
279
280val commutative : BackEndOps.op2 -> Bool.bool
281
282val uses_carry : BackEndOps.op2 -> Bool.bool
283
284val sets_carry : BackEndOps.op2 -> Bool.bool
285
286val translate_op2 :
287  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
288  Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
289  List.list
290
291val translate_op2_smart :
292  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
293  Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
294  List.list
295
296val dec_to_arg_dec : Interference.decision -> arg_decision
297
298val reg_to_dec__o__dec_arg_dec__o__inject :
299  I8051.register -> arg_decision Types.sig0
300
301val dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject :
302  (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0
303
304val eject__o__Reg_to_dec__o__dec_arg_dec__o__inject :
305  I8051.register Types.sig0 -> arg_decision Types.sig0
306
307val dpi1__o__dec_arg_dec__o__inject :
308  (Interference.decision, 'a1) Types.dPair -> arg_decision Types.sig0
309
310val eject__o__dec_arg_dec__o__inject :
311  Interference.decision Types.sig0 -> arg_decision Types.sig0
312
313val dec_arg_dec__o__inject : Interference.decision -> arg_decision Types.sig0
314
315val reg_to_dec__o__dec_arg_dec : I8051.register -> arg_decision
316
317val dpi1__o__Reg_to_dec__o__dec_arg_dec :
318  (I8051.register, 'a1) Types.dPair -> arg_decision
319
320val eject__o__Reg_to_dec__o__dec_arg_dec :
321  I8051.register Types.sig0 -> arg_decision
322
323val dpi1__o__dec_arg_dec :
324  (Interference.decision, 'a1) Types.dPair -> arg_decision
325
326val eject__o__dec_arg_dec : Interference.decision Types.sig0 -> arg_decision
327
328val translate_op1 :
329  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op1 ->
330  Interference.decision -> Interference.decision -> Joint.joint_seq List.list
331
332val translate_opaccs :
333  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.opAccs ->
334  Interference.decision -> Interference.decision -> arg_decision ->
335  arg_decision -> Joint.joint_seq List.list
336
337val move_to_dp :
338  AST.ident List.list -> Nat.nat -> arg_decision -> arg_decision ->
339  Joint.joint_seq List.list
340
341val translate_store :
342  AST.ident List.list -> Nat.nat -> Bool.bool -> arg_decision -> arg_decision
343  -> arg_decision -> Joint.joint_seq List.list
344
345val translate_load :
346  AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
347  arg_decision -> arg_decision -> Joint.joint_seq List.list
348
349val translate_address :
350  __ List.list -> Nat.nat -> Bool.bool -> __ -> BitVector.word ->
351  Interference.decision -> Interference.decision -> Joint.joint_seq List.list
352
353val translate_step :
354  AST.ident List.list -> Joint.joint_internal_function -> Nat.nat ->
355  Fixpoints.valuation -> Interference.coloured_graph -> Nat.nat ->
356  Graphs.label -> Joint.joint_step -> Blocks.bind_step_block
357
358val translate_fin_step :
359  AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
360  Blocks.bind_fin_block
361
362val translate_data :
363  Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
364  AST.ident List.list -> Joint.joint_closed_internal_function ->
365  (Registers.register, TranslateUtils.b_graph_translate_data)
366  Bind_new.bind_new
367
368val ertl_to_ltl :
369  Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
370  ERTL.ertl_program -> ((LTL.ltl_program, Joint.stack_cost_model) Types.prod,
371  Nat.nat) Types.prod
372
Note: See TracBrowser for help on using the repository browser.