source: extracted/traces.mli @ 2960

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

New extraction, it diverges in RTL execution now.

File size: 9.7 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                           ev_genv : Joint_semantics.genv }
155
156val evaluation_params_rect_Type4 :
157  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
158  -> 'a1) -> evaluation_params -> 'a1
159
160val evaluation_params_rect_Type5 :
161  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
162  -> 'a1) -> evaluation_params -> 'a1
163
164val evaluation_params_rect_Type3 :
165  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
166  -> 'a1) -> evaluation_params -> 'a1
167
168val evaluation_params_rect_Type2 :
169  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
170  -> 'a1) -> evaluation_params -> 'a1
171
172val evaluation_params_rect_Type1 :
173  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
174  -> 'a1) -> evaluation_params -> 'a1
175
176val evaluation_params_rect_Type0 :
177  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
178  -> 'a1) -> evaluation_params -> 'a1
179
180val globals :
181  Joint_semantics.sem_params -> evaluation_params -> AST.ident List.list
182
183val ev_genv :
184  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
185
186val evaluation_params_inv_rect_Type4 :
187  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
188  Joint_semantics.genv -> __ -> 'a1) -> 'a1
189
190val evaluation_params_inv_rect_Type3 :
191  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
192  Joint_semantics.genv -> __ -> 'a1) -> 'a1
193
194val evaluation_params_inv_rect_Type2 :
195  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
196  Joint_semantics.genv -> __ -> 'a1) -> 'a1
197
198val evaluation_params_inv_rect_Type1 :
199  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
200  Joint_semantics.genv -> __ -> 'a1) -> 'a1
201
202val evaluation_params_inv_rect_Type0 :
203  Joint_semantics.sem_params -> evaluation_params -> (AST.ident List.list ->
204  Joint_semantics.genv -> __ -> 'a1) -> 'a1
205
206val evaluation_params_discr :
207  Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> __
208
209val evaluation_params_jmdiscr :
210  Joint_semantics.sem_params -> evaluation_params -> evaluation_params -> __
211
212val dpi1__o__ev_genv__o__inject :
213  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
214  Joint_semantics.genv Types.sig0
215
216val dpi1__o__ev_genv__o__genv_to_genv_t__o__inject :
217  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
218  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
219  Types.sig0
220
221val dpi1__o__ev_genv__o__genv_to_genv_t :
222  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
223  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
224
225val eject__o__ev_genv__o__inject :
226  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
227  Joint_semantics.genv Types.sig0
228
229val eject__o__ev_genv__o__genv_to_genv_t__o__inject :
230  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
231  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
232  Types.sig0
233
234val eject__o__ev_genv__o__genv_to_genv_t :
235  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
236  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
237
238val ev_genv__o__genv_to_genv_t :
239  Joint_semantics.sem_params -> evaluation_params ->
240  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
241
242val ev_genv__o__genv_to_genv_t__o__inject :
243  Joint_semantics.sem_params -> evaluation_params ->
244  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
245  Types.sig0
246
247val ev_genv__o__inject :
248  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.genv
249  Types.sig0
250
251val dpi1__o__ev_genv :
252  Joint_semantics.sem_params -> (evaluation_params, 'a1) Types.dPair ->
253  Joint_semantics.genv
254
255val eject__o__ev_genv :
256  Joint_semantics.sem_params -> evaluation_params Types.sig0 ->
257  Joint_semantics.genv
258
259type prog_params = { prog_spars : Joint_semantics.sem_params;
260                     prog : Joint.joint_program;
261                     stack_sizes : (AST.ident -> Nat.nat Types.option) }
262
263val prog_params_rect_Type4 :
264  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
265  Types.option) -> 'a1) -> prog_params -> 'a1
266
267val prog_params_rect_Type5 :
268  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
269  Types.option) -> 'a1) -> prog_params -> 'a1
270
271val prog_params_rect_Type3 :
272  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
273  Types.option) -> 'a1) -> prog_params -> 'a1
274
275val prog_params_rect_Type2 :
276  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
277  Types.option) -> 'a1) -> prog_params -> 'a1
278
279val prog_params_rect_Type1 :
280  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
281  Types.option) -> 'a1) -> prog_params -> 'a1
282
283val prog_params_rect_Type0 :
284  (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
285  Types.option) -> 'a1) -> prog_params -> 'a1
286
287val prog_spars : prog_params -> Joint_semantics.sem_params
288
289val prog : prog_params -> Joint.joint_program
290
291val stack_sizes : prog_params -> AST.ident -> Nat.nat Types.option
292
293val prog_params_inv_rect_Type4 :
294  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
295  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
296
297val prog_params_inv_rect_Type3 :
298  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
299  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
300
301val prog_params_inv_rect_Type2 :
302  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
303  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
304
305val prog_params_inv_rect_Type1 :
306  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
307  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
308
309val prog_params_inv_rect_Type0 :
310  prog_params -> (Joint_semantics.sem_params -> Joint.joint_program ->
311  (AST.ident -> Nat.nat Types.option) -> __ -> 'a1) -> 'a1
312
313val prog_params_jmdiscr : prog_params -> prog_params -> __
314
315val prog_spars__o__spp' : prog_params -> Joint_semantics.serialized_params
316
317val prog_spars__o__spp'__o__msu_pars :
318  prog_params -> Joint.joint_closed_internal_function
319  Joint_semantics.sem_unserialized_params
320
321val prog_spars__o__spp'__o__msu_pars__o__st_pars :
322  prog_params -> Joint_semantics.sem_state_params
323
324val prog_spars__o__spp'__o__spp : prog_params -> Joint.params
325
326val prog_spars__o__spp'__o__spp__o__stmt_pars :
327  prog_params -> Joint.stmt_params
328
329val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
330  prog_params -> Joint.uns_params
331
332val prog_spars__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
333  prog_params -> Joint.unserialized_params
334
335val joint_make_global : prog_params -> evaluation_params
336
337val joint_make_global__o__ev_genv : prog_params -> Joint_semantics.genv
338
339val joint_make_global__o__ev_genv__o__genv_to_genv_t :
340  prog_params -> Joint.joint_closed_internal_function AST.fundef
341  Globalenvs.genv_t
342
343val joint_make_global__o__ev_genv__o__genv_to_genv_t__o__inject :
344  prog_params -> Joint.joint_closed_internal_function AST.fundef
345  Globalenvs.genv_t Types.sig0
346
347val joint_make_global__o__ev_genv__o__inject :
348  prog_params -> Joint_semantics.genv Types.sig0
349
350val joint_make_global__o__inject :
351  prog_params -> evaluation_params Types.sig0
352
353val make_initial_state : prog_params -> Joint_semantics.state_pc
354
355val joint_classify_step :
356  Joint.unserialized_params -> AST.ident List.list -> Joint.joint_step ->
357  StructuredTraces.status_class
358
359val joint_classify_final :
360  Joint.unserialized_params -> Joint.joint_fin_step ->
361  StructuredTraces.status_class
362
363val joint_classify :
364  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
365  -> StructuredTraces.status_class
366
367val joint_call_ident :
368  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
369  -> AST.ident
370
371val joint_tailcall_ident :
372  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
373  -> AST.ident
374
375val pcDeq : Deqsets.deqSet
376
377val cost_label_of_stmt :
378  Joint_semantics.sem_params -> evaluation_params -> Joint.joint_statement ->
379  CostLabel.costlabel Types.option
380
381val joint_label_of_pc :
382  Joint_semantics.sem_params -> evaluation_params ->
383  ByteValues.program_counter -> CostLabel.costlabel Types.option
384
385val exit_pc' : ByteValues.program_counter
386
387val joint_final :
388  Joint_semantics.sem_params -> evaluation_params -> Joint_semantics.state_pc
389  -> Integers.int Types.option
390
391val joint_abstract_status : prog_params -> StructuredTraces.abstract_status
392
393val joint_status :
394  Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident -> Nat.nat
395  Types.option) -> StructuredTraces.abstract_status
396
Note: See TracBrowser for help on using the repository browser.