source: extracted/traces.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: 8.2 KB
Line 
1open Preamble
2
3open ExtraMonads
4
5open Deqsets_extra
6
7open State
8
9open Bind_new
10
11open BindLists
12
13open Blocks
14
15open TranslateUtils
16
17open ExtraGlobalenvs
18
19open I8051bis
20
21open String
22
23open Sets
24
25open Listb
26
27open LabelledObjects
28
29open BitVectorTrie
30
31open Graphs
32
33open I8051
34
35open Order
36
37open Registers
38
39open BackEndOps
40
41open Joint
42
43open BEMem
44
45open CostLabel
46
47open Events
48
49open IOMonad
50
51open IO
52
53open Extra_bool
54
55open Coqlib
56
57open Values
58
59open FrontEndVal
60
61open Hide
62
63open ByteValues
64
65open Division
66
67open Z
68
69open BitVectorZ
70
71open Pointers
72
73open GenMem
74
75open FrontEndMem
76
77open Proper
78
79open PositiveMap
80
81open Deqsets
82
83open Extralib
84
85open Lists
86
87open Identifiers
88
89open Exp
90
91open Arithmetic
92
93open Vector
94
95open Div_and_mod
96
97open Util
98
99open FoldStuff
100
101open BitVector
102
103open Extranat
104
105open Integers
106
107open AST
108
109open ErrorMessages
110
111open Option
112
113open Setoids
114
115open Monad
116
117open Jmeq
118
119open Russell
120
121open Positive
122
123open PreIdentifiers
124
125open Bool
126
127open Relations
128
129open Nat
130
131open List
132
133open Hints_declaration
134
135open Core_notation
136
137open Pts
138
139open Logic
140
141open Types
142
143open Errors
144
145open Globalenvs
146
147open Joint_semantics
148
149open SemanticsUtils
150
151open StructuredTraces
152
153type evaluation_params = { globals : AST.ident List.list;
154                           sparams : Joint_semantics.sem_params;
155                           ev_genv : Joint_semantics.genv }
156
157val evaluation_params_rect_Type4 :
158  (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
159  -> 'a1) -> evaluation_params -> 'a1
160
161val evaluation_params_rect_Type5 :
162  (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
163  -> 'a1) -> evaluation_params -> 'a1
164
165val evaluation_params_rect_Type3 :
166  (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
167  -> 'a1) -> evaluation_params -> 'a1
168
169val evaluation_params_rect_Type2 :
170  (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
171  -> 'a1) -> evaluation_params -> 'a1
172
173val evaluation_params_rect_Type1 :
174  (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
175  -> 'a1) -> evaluation_params -> 'a1
176
177val evaluation_params_rect_Type0 :
178  (AST.ident List.list -> Joint_semantics.sem_params -> Joint_semantics.genv
179  -> 'a1) -> evaluation_params -> 'a1
180
181val globals : evaluation_params -> AST.ident List.list
182
183val sparams : evaluation_params -> Joint_semantics.sem_params
184
185val ev_genv : evaluation_params -> Joint_semantics.genv
186
187val evaluation_params_inv_rect_Type4 :
188  evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
189  Joint_semantics.genv -> __ -> 'a1) -> 'a1
190
191val evaluation_params_inv_rect_Type3 :
192  evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
193  Joint_semantics.genv -> __ -> 'a1) -> 'a1
194
195val evaluation_params_inv_rect_Type2 :
196  evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
197  Joint_semantics.genv -> __ -> 'a1) -> 'a1
198
199val evaluation_params_inv_rect_Type1 :
200  evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
201  Joint_semantics.genv -> __ -> 'a1) -> 'a1
202
203val evaluation_params_inv_rect_Type0 :
204  evaluation_params -> (AST.ident List.list -> Joint_semantics.sem_params ->
205  Joint_semantics.genv -> __ -> 'a1) -> 'a1
206
207val evaluation_params_jmdiscr : evaluation_params -> evaluation_params -> __
208
209val sparams__o__spp' : evaluation_params -> Joint_semantics.serialized_params
210
211val sparams__o__spp'__o__msu_pars :
212  evaluation_params -> Joint.joint_closed_internal_function
213  Joint_semantics.sem_unserialized_params
214
215val sparams__o__spp'__o__msu_pars__o__st_pars :
216  evaluation_params -> Joint_semantics.sem_state_params
217
218val sparams__o__spp'__o__spp : evaluation_params -> Joint.params
219
220val sparams__o__spp'__o__spp__o__stmt_pars :
221  evaluation_params -> Joint.stmt_params
222
223val sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
224  evaluation_params -> Joint.uns_params
225
226val sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
227  evaluation_params -> Joint.unserialized_params
228
229type prog_params = { prog_spars : Joint_semantics.sem_params;
230                     prog : Joint.joint_program;
231                     stack_sizes : (AST.ident -> Nat.nat Types.option) }
232
233val prog_params_rect_Type4 :
234  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
235  Types.option) -> 'a1) -> prog_params -> 'a1
236
237val prog_params_rect_Type5 :
238  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
239  Types.option) -> 'a1) -> prog_params -> 'a1
240
241val prog_params_rect_Type3 :
242  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
243  Types.option) -> 'a1) -> prog_params -> 'a1
244
245val prog_params_rect_Type2 :
246  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
247  Types.option) -> 'a1) -> prog_params -> 'a1
248
249val prog_params_rect_Type1 :
250  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
251  Types.option) -> 'a1) -> prog_params -> 'a1
252
253val prog_params_rect_Type0 :
254  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
255  Types.option) -> 'a1) -> prog_params -> 'a1
256
257val prog_spars : prog_params -> Joint_semantics.sem_params
258
259val prog : prog_params -> Joint.joint_program
260
261val stack_sizes : prog_params -> AST.ident -> Nat.nat Types.option
262
263val prog_params_inv_rect_Type4 :
264  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
265  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
266
267val prog_params_inv_rect_Type3 :
268  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
269  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
270
271val prog_params_inv_rect_Type2 :
272  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
273  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
274
275val prog_params_inv_rect_Type1 :
276  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
277  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
278
279val prog_params_inv_rect_Type0 :
280  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
281  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
282
283val prog_params_jmdiscr : prog_params -> prog_params -> __
284
285val make_global : prog_params -> evaluation_params
286
287val prog_params_to_ev_params__o__sparams :
288  prog_params -> Joint_semantics.sem_params
289
290val prog_params_to_ev_params__o__sparams__o__spp' :
291  prog_params -> Joint_semantics.serialized_params
292
293val prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars :
294  prog_params -> Joint.joint_closed_internal_function
295  Joint_semantics.sem_unserialized_params
296
297val prog_params_to_ev_params__o__sparams__o__spp'__o__msu_pars__o__st_pars :
298  prog_params -> Joint_semantics.sem_state_params
299
300val prog_params_to_ev_params__o__sparams__o__spp'__o__spp :
301  prog_params -> Joint.params
302
303val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars :
304  prog_params -> Joint.stmt_params
305
306val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
307  prog_params -> Joint.uns_params
308
309val prog_params_to_ev_params__o__sparams__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
310  prog_params -> Joint.unserialized_params
311
312val make_initial_state : prog_params -> Joint_semantics.state_pc
313
314val joint_classify_step :
315  evaluation_params -> Joint.joint_step -> StructuredTraces.status_class
316
317val joint_classify_final :
318  evaluation_params -> Joint.joint_fin_step -> StructuredTraces.status_class
319
320val joint_classify :
321  evaluation_params -> Joint_semantics.state_pc ->
322  StructuredTraces.status_class
323
324val joint_call_ident :
325  evaluation_params -> Joint_semantics.state_pc -> AST.ident
326
327val joint_tailcall_ident :
328  evaluation_params -> Joint_semantics.state_pc -> AST.ident
329
330val pcDeq : Deqsets.deqSet
331
332val cost_label_of_stmt :
333  evaluation_params -> Joint.joint_statement -> CostLabel.costlabel
334  Types.option
335
336val joint_label_of_pc :
337  evaluation_params -> ByteValues.program_counter -> CostLabel.costlabel
338  Types.option
339
340val exit_pc' : ByteValues.program_counter
341
342val joint_final :
343  Joint_semantics.sem_params -> AST.ident List.list -> Joint_semantics.genv
344  -> Joint_semantics.state_pc -> Integers.int Types.option
345
346val joint_abstract_status : prog_params -> StructuredTraces.abstract_status
347
348val joint_status :
349  Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
350  Types.option) -> StructuredTraces.abstract_status
351
Note: See TracBrowser for help on using the repository browser.