source: extracted/eRTLptrToLTL.mli @ 2960

Last change on this file since 2960 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: 8.7 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 ERTLptr
132
133open Liveness
134
135open Interference
136
137open Deqsets_extra
138
139open State
140
141open Bind_new
142
143open BindLists
144
145open Blocks
146
147open TranslateUtils
148
149val dpi1__o__Reg_to_dec__o__inject :
150  (I8051.register, 'a1) Types.dPair -> Interference.decision Types.sig0
151
152val eject__o__Reg_to_dec__o__inject :
153  I8051.register Types.sig0 -> Interference.decision Types.sig0
154
155val reg_to_dec__o__inject :
156  I8051.register -> Interference.decision Types.sig0
157
158val dpi1__o__Reg_to_dec :
159  (I8051.register, 'a1) Types.dPair -> Interference.decision
160
161val eject__o__Reg_to_dec : I8051.register Types.sig0 -> Interference.decision
162
163type arg_decision =
164| Arg_decision_colour of I8051.register
165| Arg_decision_spill of Nat.nat
166| Arg_decision_imm of BitVector.byte
167
168val arg_decision_rect_Type4 :
169  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
170  arg_decision -> 'a1
171
172val arg_decision_rect_Type5 :
173  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
174  arg_decision -> 'a1
175
176val arg_decision_rect_Type3 :
177  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
178  arg_decision -> 'a1
179
180val arg_decision_rect_Type2 :
181  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
182  arg_decision -> 'a1
183
184val arg_decision_rect_Type1 :
185  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
186  arg_decision -> 'a1
187
188val arg_decision_rect_Type0 :
189  (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
190  arg_decision -> 'a1
191
192val arg_decision_inv_rect_Type4 :
193  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
194  (BitVector.byte -> __ -> 'a1) -> 'a1
195
196val arg_decision_inv_rect_Type3 :
197  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
198  (BitVector.byte -> __ -> 'a1) -> 'a1
199
200val arg_decision_inv_rect_Type2 :
201  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
202  (BitVector.byte -> __ -> 'a1) -> 'a1
203
204val arg_decision_inv_rect_Type1 :
205  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
206  (BitVector.byte -> __ -> 'a1) -> 'a1
207
208val arg_decision_inv_rect_Type0 :
209  arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
210  (BitVector.byte -> __ -> 'a1) -> 'a1
211
212val arg_decision_discr : arg_decision -> arg_decision -> __
213
214val arg_decision_jmdiscr : arg_decision -> arg_decision -> __
215
216val dpi1__o__Reg_to_arg_dec__o__inject :
217  (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0
218
219val eject__o__Reg_to_arg_dec__o__inject :
220  I8051.register Types.sig0 -> arg_decision Types.sig0
221
222val reg_to_arg_dec__o__inject : I8051.register -> arg_decision Types.sig0
223
224val dpi1__o__Reg_to_arg_dec :
225  (I8051.register, 'a1) Types.dPair -> arg_decision
226
227val eject__o__Reg_to_arg_dec : I8051.register Types.sig0 -> arg_decision
228
229val preserve_carry_bit :
230  AST.ident List.list -> Bool.bool -> Joint.joint_seq List.list ->
231  Joint.joint_seq List.list
232
233val a : Types.unit0
234
235val dpi1__o__beval_of_byte__o__inject :
236  (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval Types.sig0
237
238val eject__o__beval_of_byte__o__inject :
239  BitVector.byte Types.sig0 -> ByteValues.beval Types.sig0
240
241val beval_of_byte__o__inject : BitVector.byte -> ByteValues.beval Types.sig0
242
243val dpi1__o__beval_of_byte :
244  (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval
245
246val eject__o__beval_of_byte : BitVector.byte Types.sig0 -> ByteValues.beval
247
248val set_dp_by_offset :
249  AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
250
251val get_stack :
252  AST.ident List.list -> Nat.nat -> I8051.register -> Nat.nat ->
253  Joint.joint_seq List.list
254
255val set_stack_not_a :
256  AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
257  Joint.joint_seq List.list
258
259val set_stack_a :
260  AST.ident List.list -> Nat.nat -> Nat.nat -> Joint.joint_seq List.list
261
262val set_stack :
263  AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
264  Joint.joint_seq List.list
265
266val set_stack_int :
267  AST.ident List.list -> Nat.nat -> Nat.nat -> BitVector.byte ->
268  Joint.joint_seq List.list
269
270val move :
271  AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
272  arg_decision -> Joint.joint_seq List.list
273
274val arg_is_spilled : arg_decision -> Bool.bool
275
276val is_spilled : Interference.decision -> Bool.bool
277
278val newframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
279
280val delframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
281
282val commutative : BackEndOps.op2 -> Bool.bool
283
284val uses_carry : BackEndOps.op2 -> Bool.bool
285
286val sets_carry : BackEndOps.op2 -> Bool.bool
287
288val translate_op2 :
289  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
290  Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
291  List.list
292
293val translate_op2_smart :
294  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
295  Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
296  List.list
297
298val dec_to_arg_dec : Interference.decision -> arg_decision
299
300val reg_to_dec__o__dec_arg_dec__o__inject :
301  I8051.register -> arg_decision Types.sig0
302
303val dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject :
304  (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0
305
306val eject__o__Reg_to_dec__o__dec_arg_dec__o__inject :
307  I8051.register Types.sig0 -> arg_decision Types.sig0
308
309val dpi1__o__dec_arg_dec__o__inject :
310  (Interference.decision, 'a1) Types.dPair -> arg_decision Types.sig0
311
312val eject__o__dec_arg_dec__o__inject :
313  Interference.decision Types.sig0 -> arg_decision Types.sig0
314
315val dec_arg_dec__o__inject : Interference.decision -> arg_decision Types.sig0
316
317val reg_to_dec__o__dec_arg_dec : I8051.register -> arg_decision
318
319val dpi1__o__Reg_to_dec__o__dec_arg_dec :
320  (I8051.register, 'a1) Types.dPair -> arg_decision
321
322val eject__o__Reg_to_dec__o__dec_arg_dec :
323  I8051.register Types.sig0 -> arg_decision
324
325val dpi1__o__dec_arg_dec :
326  (Interference.decision, 'a1) Types.dPair -> arg_decision
327
328val eject__o__dec_arg_dec : Interference.decision Types.sig0 -> arg_decision
329
330val translate_op1 :
331  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op1 ->
332  Interference.decision -> Interference.decision -> Joint.joint_seq List.list
333
334val translate_opaccs :
335  AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.opAccs ->
336  Interference.decision -> Interference.decision -> arg_decision ->
337  arg_decision -> Joint.joint_seq List.list
338
339val move_to_dp :
340  AST.ident List.list -> Nat.nat -> arg_decision -> arg_decision ->
341  Joint.joint_seq List.list
342
343val translate_store :
344  AST.ident List.list -> Nat.nat -> Bool.bool -> arg_decision -> arg_decision
345  -> arg_decision -> Joint.joint_seq List.list
346
347val translate_load :
348  AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
349  arg_decision -> arg_decision -> Joint.joint_seq List.list
350
351val translate_address :
352  __ List.list -> Nat.nat -> Bool.bool -> __ -> Interference.decision ->
353  Interference.decision -> Joint.joint_seq List.list
354
355val translate_low_address :
356  AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
357  Graphs.label -> Joint.joint_seq List.list
358
359val translate_high_address :
360  AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
361  Graphs.label -> Joint.joint_seq List.list
362
363val translate_step :
364  AST.ident List.list -> Joint.joint_internal_function -> Nat.nat ->
365  Fixpoints.valuation -> Interference.coloured_graph -> Nat.nat ->
366  Graphs.label -> Joint.joint_step -> Blocks.bind_step_block
367
368val translate_fin_step :
369  AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
370  Blocks.bind_fin_block
371
372val translate_data :
373  Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
374  AST.ident List.list -> Joint.joint_closed_internal_function ->
375  (Registers.register, TranslateUtils.b_graph_translate_data)
376  Bind_new.bind_new
377
378val ertlptr_to_ltl :
379  Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
380  ERTLptr.ertlptr_program -> ((LTL.ltl_program, Joint.stack_cost_model)
381  Types.prod, Nat.nat) Types.prod
382
Note: See TracBrowser for help on using the repository browser.