source: extracted/semanticsUtils.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: 13.8 KB
Line 
1open Preamble
2
3open ExtraGlobalenvs
4
5open I8051bis
6
7open String
8
9open Sets
10
11open Listb
12
13open LabelledObjects
14
15open BitVectorTrie
16
17open Graphs
18
19open I8051
20
21open Order
22
23open Registers
24
25open BackEndOps
26
27open Joint
28
29open BEMem
30
31open CostLabel
32
33open Events
34
35open IOMonad
36
37open IO
38
39open Extra_bool
40
41open Coqlib
42
43open Values
44
45open FrontEndVal
46
47open Hide
48
49open ByteValues
50
51open Division
52
53open Z
54
55open BitVectorZ
56
57open Pointers
58
59open GenMem
60
61open FrontEndMem
62
63open Proper
64
65open PositiveMap
66
67open Deqsets
68
69open Extralib
70
71open Lists
72
73open Identifiers
74
75open Exp
76
77open Arithmetic
78
79open Vector
80
81open Div_and_mod
82
83open Util
84
85open FoldStuff
86
87open BitVector
88
89open Extranat
90
91open Integers
92
93open AST
94
95open ErrorMessages
96
97open Option
98
99open Setoids
100
101open Monad
102
103open Jmeq
104
105open Russell
106
107open Positive
108
109open PreIdentifiers
110
111open Bool
112
113open Relations
114
115open Nat
116
117open List
118
119open Hints_declaration
120
121open Core_notation
122
123open Pts
124
125open Logic
126
127open Types
128
129open Errors
130
131open Globalenvs
132
133open Joint_semantics
134
135open Deqsets_extra
136
137open State
138
139open Bind_new
140
141open BindLists
142
143open Blocks
144
145open TranslateUtils
146
147open ExtraMonads
148
149val reg_store :
150  PreIdentifiers.identifier -> ByteValues.beval -> ByteValues.beval
151  Identifiers.identifier_map -> ByteValues.beval Identifiers.identifier_map
152
153val reg_retrieve :
154  ByteValues.beval Registers.register_env -> Registers.register ->
155  ByteValues.beval Errors.res
156
157type hw_register_env = { reg_env : ByteValues.beval
158                                   BitVectorTrie.bitVectorTrie;
159                         other_bit : ByteValues.bebit }
160
161val hw_register_env_rect_Type4 :
162  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
163  -> hw_register_env -> 'a1
164
165val hw_register_env_rect_Type5 :
166  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
167  -> hw_register_env -> 'a1
168
169val hw_register_env_rect_Type3 :
170  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
171  -> hw_register_env -> 'a1
172
173val hw_register_env_rect_Type2 :
174  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
175  -> hw_register_env -> 'a1
176
177val hw_register_env_rect_Type1 :
178  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
179  -> hw_register_env -> 'a1
180
181val hw_register_env_rect_Type0 :
182  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
183  -> hw_register_env -> 'a1
184
185val reg_env : hw_register_env -> ByteValues.beval BitVectorTrie.bitVectorTrie
186
187val other_bit : hw_register_env -> ByteValues.bebit
188
189val hw_register_env_inv_rect_Type4 :
190  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
191  ByteValues.bebit -> __ -> 'a1) -> 'a1
192
193val hw_register_env_inv_rect_Type3 :
194  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
195  ByteValues.bebit -> __ -> 'a1) -> 'a1
196
197val hw_register_env_inv_rect_Type2 :
198  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
199  ByteValues.bebit -> __ -> 'a1) -> 'a1
200
201val hw_register_env_inv_rect_Type1 :
202  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
203  ByteValues.bebit -> __ -> 'a1) -> 'a1
204
205val hw_register_env_inv_rect_Type0 :
206  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
207  ByteValues.bebit -> __ -> 'a1) -> 'a1
208
209val hw_register_env_discr : hw_register_env -> hw_register_env -> __
210
211val hw_register_env_jmdiscr : hw_register_env -> hw_register_env -> __
212
213val hwreg_retrieve : hw_register_env -> I8051.register -> ByteValues.beval
214
215val hwreg_store :
216  I8051.register -> ByteValues.beval -> hw_register_env -> hw_register_env
217
218val hwreg_set_other : ByteValues.bebit -> hw_register_env -> hw_register_env
219
220val hwreg_retrieve_sp : hw_register_env -> ByteValues.xpointer Errors.res
221
222val hwreg_store_sp :
223  hw_register_env -> ByteValues.xpointer -> hw_register_env
224
225val init_hw_register_env : ByteValues.xpointer -> hw_register_env
226
227type sem_graph_params = { sgp_pars : Joint.uns_params;
228                          sgp_sup : (__ -> __
229                                    Joint_semantics.sem_unserialized_params);
230                          graph_pre_main_generator : (Joint.joint_program ->
231                                                     Joint.joint_closed_internal_function) }
232
233val sem_graph_params_rect_Type4 :
234  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
235  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
236  sem_graph_params -> 'a1
237
238val sem_graph_params_rect_Type5 :
239  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
240  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
241  sem_graph_params -> 'a1
242
243val sem_graph_params_rect_Type3 :
244  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
245  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
246  sem_graph_params -> 'a1
247
248val sem_graph_params_rect_Type2 :
249  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
250  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
251  sem_graph_params -> 'a1
252
253val sem_graph_params_rect_Type1 :
254  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
255  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
256  sem_graph_params -> 'a1
257
258val sem_graph_params_rect_Type0 :
259  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
260  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
261  sem_graph_params -> 'a1
262
263val sgp_pars : sem_graph_params -> Joint.uns_params
264
265val sgp_sup0 :
266  sem_graph_params -> 'a1 Joint_semantics.sem_unserialized_params
267
268val graph_pre_main_generator :
269  sem_graph_params -> Joint.joint_program ->
270  Joint.joint_closed_internal_function
271
272val sem_graph_params_inv_rect_Type4 :
273  sem_graph_params -> (Joint.uns_params -> (__ -> __
274  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
275  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
276
277val sem_graph_params_inv_rect_Type3 :
278  sem_graph_params -> (Joint.uns_params -> (__ -> __
279  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
280  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
281
282val sem_graph_params_inv_rect_Type2 :
283  sem_graph_params -> (Joint.uns_params -> (__ -> __
284  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
285  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
286
287val sem_graph_params_inv_rect_Type1 :
288  sem_graph_params -> (Joint.uns_params -> (__ -> __
289  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
290  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
291
292val sem_graph_params_inv_rect_Type0 :
293  sem_graph_params -> (Joint.uns_params -> (__ -> __
294  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
295  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
296
297val sem_graph_params_jmdiscr : sem_graph_params -> sem_graph_params -> __
298
299val sem_graph_params_to_graph_params : sem_graph_params -> Joint.graph_params
300
301val sem_graph_params_to_sem_params :
302  sem_graph_params -> Joint_semantics.sem_params
303
304val sem_params_from_sem_graph_params__o__spp' :
305  sem_graph_params -> Joint_semantics.serialized_params
306
307val sem_params_from_sem_graph_params__o__spp'__o__msu_pars :
308  sem_graph_params -> Joint.joint_closed_internal_function
309  Joint_semantics.sem_unserialized_params
310
311val sem_params_from_sem_graph_params__o__spp'__o__msu_pars__o__st_pars :
312  sem_graph_params -> Joint_semantics.sem_state_params
313
314val sem_params_from_sem_graph_params__o__spp'__o__spp :
315  sem_graph_params -> Joint.params
316
317val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars :
318  sem_graph_params -> Joint.stmt_params
319
320val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
321  sem_graph_params -> Joint.uns_params
322
323val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
324  sem_graph_params -> Joint.unserialized_params
325
326type sem_lin_params = { slp_pars : Joint.uns_params;
327                        slp_sup : (__ -> __
328                                  Joint_semantics.sem_unserialized_params);
329                        lin_pre_main_generator : (Joint.joint_program ->
330                                                 Joint.joint_closed_internal_function) }
331
332val sem_lin_params_rect_Type4 :
333  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
334  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
335  sem_lin_params -> 'a1
336
337val sem_lin_params_rect_Type5 :
338  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
339  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
340  sem_lin_params -> 'a1
341
342val sem_lin_params_rect_Type3 :
343  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
344  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
345  sem_lin_params -> 'a1
346
347val sem_lin_params_rect_Type2 :
348  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
349  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
350  sem_lin_params -> 'a1
351
352val sem_lin_params_rect_Type1 :
353  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
354  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
355  sem_lin_params -> 'a1
356
357val sem_lin_params_rect_Type0 :
358  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
359  (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) ->
360  sem_lin_params -> 'a1
361
362val slp_pars : sem_lin_params -> Joint.uns_params
363
364val slp_sup0 : sem_lin_params -> 'a1 Joint_semantics.sem_unserialized_params
365
366val lin_pre_main_generator :
367  sem_lin_params -> Joint.joint_program ->
368  Joint.joint_closed_internal_function
369
370val sem_lin_params_inv_rect_Type4 :
371  sem_lin_params -> (Joint.uns_params -> (__ -> __
372  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
373  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
374
375val sem_lin_params_inv_rect_Type3 :
376  sem_lin_params -> (Joint.uns_params -> (__ -> __
377  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
378  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
379
380val sem_lin_params_inv_rect_Type2 :
381  sem_lin_params -> (Joint.uns_params -> (__ -> __
382  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
383  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
384
385val sem_lin_params_inv_rect_Type1 :
386  sem_lin_params -> (Joint.uns_params -> (__ -> __
387  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
388  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
389
390val sem_lin_params_inv_rect_Type0 :
391  sem_lin_params -> (Joint.uns_params -> (__ -> __
392  Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
393  Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1
394
395val sem_lin_params_jmdiscr : sem_lin_params -> sem_lin_params -> __
396
397val sem_lin_params_to_lin_params : sem_lin_params -> Joint.lin_params
398
399val sem_lin_params_to_sem_params :
400  sem_lin_params -> Joint_semantics.sem_params
401
402val sem_params_from_sem_lin_params__o__spp' :
403  sem_lin_params -> Joint_semantics.serialized_params
404
405val sem_params_from_sem_lin_params__o__spp'__o__msu_pars :
406  sem_lin_params -> Joint.joint_closed_internal_function
407  Joint_semantics.sem_unserialized_params
408
409val sem_params_from_sem_lin_params__o__spp'__o__msu_pars__o__st_pars :
410  sem_lin_params -> Joint_semantics.sem_state_params
411
412val sem_params_from_sem_lin_params__o__spp'__o__spp :
413  sem_lin_params -> Joint.params
414
415val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars :
416  sem_lin_params -> Joint.stmt_params
417
418val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
419  sem_lin_params -> Joint.uns_params
420
421val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
422  sem_lin_params -> Joint.unserialized_params
423
424val pre_main_id : AST.ident
425
426val joint_globalenv :
427  Joint_semantics.sem_params -> Joint.joint_program ->
428  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
429
430val match_genv_t_rect_Type4 :
431  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
432  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
433
434val match_genv_t_rect_Type5 :
435  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
436  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
437
438val match_genv_t_rect_Type3 :
439  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
440  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
441
442val match_genv_t_rect_Type2 :
443  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
444  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
445
446val match_genv_t_rect_Type1 :
447  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
448  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
449
450val match_genv_t_rect_Type0 :
451  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
452  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
453
454val match_genv_t_inv_rect_Type4 :
455  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
456  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
457
458val match_genv_t_inv_rect_Type3 :
459  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
460  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
461
462val match_genv_t_inv_rect_Type2 :
463  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
464  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
465
466val match_genv_t_inv_rect_Type1 :
467  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
468  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
469
470val match_genv_t_inv_rect_Type0 :
471  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
472  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
473
474val match_genv_t_discr :
475  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
476  Globalenvs.genv_t -> __
477
478val match_genv_t_jmdiscr :
479  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
480  Globalenvs.genv_t -> __
481
Note: See TracBrowser for help on using the repository browser.