source: extracted/rTL_semantics.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: 7.8 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 RTL
152
153type reg_sp = { reg_sp_env : ByteValues.beval Identifiers.identifier_map;
154                stackp : ByteValues.xpointer }
155
156val reg_sp_rect_Type4 :
157  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
158  -> reg_sp -> 'a1
159
160val reg_sp_rect_Type5 :
161  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
162  -> reg_sp -> 'a1
163
164val reg_sp_rect_Type3 :
165  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
166  -> reg_sp -> 'a1
167
168val reg_sp_rect_Type2 :
169  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
170  -> reg_sp -> 'a1
171
172val reg_sp_rect_Type1 :
173  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
174  -> reg_sp -> 'a1
175
176val reg_sp_rect_Type0 :
177  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
178  -> reg_sp -> 'a1
179
180val reg_sp_env : reg_sp -> ByteValues.beval Identifiers.identifier_map
181
182val stackp : reg_sp -> ByteValues.xpointer
183
184val reg_sp_inv_rect_Type4 :
185  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
186  ByteValues.xpointer -> __ -> 'a1) -> 'a1
187
188val reg_sp_inv_rect_Type3 :
189  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
190  ByteValues.xpointer -> __ -> 'a1) -> 'a1
191
192val reg_sp_inv_rect_Type2 :
193  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
194  ByteValues.xpointer -> __ -> 'a1) -> 'a1
195
196val reg_sp_inv_rect_Type1 :
197  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
198  ByteValues.xpointer -> __ -> 'a1) -> 'a1
199
200val reg_sp_inv_rect_Type0 :
201  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
202  ByteValues.xpointer -> __ -> 'a1) -> 'a1
203
204val reg_sp_discr : reg_sp -> reg_sp -> __
205
206val reg_sp_jmdiscr : reg_sp -> reg_sp -> __
207
208val dpi1__o__reg_sp_env__o__inject :
209  (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
210  Types.sig0
211
212val eject__o__reg_sp_env__o__inject :
213  reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map Types.sig0
214
215val reg_sp_env__o__inject :
216  reg_sp -> ByteValues.beval Identifiers.identifier_map Types.sig0
217
218val dpi1__o__reg_sp_env :
219  (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
220
221val eject__o__reg_sp_env :
222  reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map
223
224val reg_sp_store :
225  PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
226
227val reg_sp_retrieve :
228  reg_sp -> Registers.register -> ByteValues.beval Errors.res
229
230val reg_sp_empty : ByteValues.xpointer -> reg_sp
231
232type frame = { fr_ret_regs : Registers.register List.list;
233               fr_pc : ByteValues.program_counter;
234               fr_carry : ByteValues.bebit; fr_regs : reg_sp }
235
236val frame_rect_Type4 :
237  (Registers.register List.list -> ByteValues.program_counter ->
238  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
239
240val frame_rect_Type5 :
241  (Registers.register List.list -> ByteValues.program_counter ->
242  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
243
244val frame_rect_Type3 :
245  (Registers.register List.list -> ByteValues.program_counter ->
246  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
247
248val frame_rect_Type2 :
249  (Registers.register List.list -> ByteValues.program_counter ->
250  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
251
252val frame_rect_Type1 :
253  (Registers.register List.list -> ByteValues.program_counter ->
254  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
255
256val frame_rect_Type0 :
257  (Registers.register List.list -> ByteValues.program_counter ->
258  ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1
259
260val fr_ret_regs : frame -> Registers.register List.list
261
262val fr_pc : frame -> ByteValues.program_counter
263
264val fr_carry : frame -> ByteValues.bebit
265
266val fr_regs : frame -> reg_sp
267
268val frame_inv_rect_Type4 :
269  frame -> (Registers.register List.list -> ByteValues.program_counter ->
270  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
271
272val frame_inv_rect_Type3 :
273  frame -> (Registers.register List.list -> ByteValues.program_counter ->
274  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
275
276val frame_inv_rect_Type2 :
277  frame -> (Registers.register List.list -> ByteValues.program_counter ->
278  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
279
280val frame_inv_rect_Type1 :
281  frame -> (Registers.register List.list -> ByteValues.program_counter ->
282  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
283
284val frame_inv_rect_Type0 :
285  frame -> (Registers.register List.list -> ByteValues.program_counter ->
286  ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1
287
288val frame_discr : frame -> frame -> __
289
290val frame_jmdiscr : frame -> frame -> __
291
292val rTL_state_params : Joint_semantics.sem_state_params
293
294type rTL_state = Joint_semantics.state
295
296val rtl_arg_retrieve :
297  reg_sp -> Joint.psd_argument -> ByteValues.beval Errors.res
298
299val rtl_fetch_ra :
300  rTL_state -> (rTL_state, ByteValues.program_counter) Types.prod Errors.res
301
302val rtl_init_local : Registers.register -> reg_sp -> reg_sp
303
304val rtl_setup_call_separate :
305  Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
306  rTL_state -> rTL_state Errors.res
307
308val stackOverflow : ErrorMessages.errorMessage
309
310val rtl_setup_call_separate_overflow :
311  Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
312  rTL_state -> rTL_state Errors.res
313
314val rtl_setup_call_unique :
315  Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
316  rTL_state -> rTL_state Errors.res
317
318type rTL_state_pc = Joint_semantics.state_pc
319
320val rtl_save_frame : Registers.register List.list -> rTL_state_pc -> __
321
322val rtl_fetch_external_args :
323  AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
324  Values.val0 List.list Errors.res
325
326val rtl_set_result :
327  Values.val0 List.list -> Registers.register List.list -> rTL_state ->
328  rTL_state Errors.res
329
330val rtl_reg_store :
331  PreIdentifiers.identifier -> ByteValues.beval -> Joint_semantics.state ->
332  Joint_semantics.state
333
334val rtl_reg_retrieve :
335  Joint_semantics.state -> Registers.register -> ByteValues.beval Errors.res
336
337val rtl_read_result :
338  Registers.register List.list -> rTL_state -> ByteValues.beval List.list
339  Errors.res
340
341val rtl_pop_frame_separate :
342  Registers.register List.list -> rTL_state -> (rTL_state,
343  ByteValues.program_counter) Types.prod Errors.res
344
345val rtl_pop_frame_unique :
346  Registers.register List.list -> rTL_state -> (rTL_state,
347  ByteValues.program_counter) Types.prod Errors.res
348
349val block_of_register_pair :
350  Registers.register -> Registers.register -> rTL_state -> Pointers.block
351  Errors.res
352
353val eval_rtl_seq :
354  RTL.rtl_seq -> AST.ident -> rTL_state -> rTL_state Errors.res
355
356val reg_res_store :
357  PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
358  Errors.res
359
360val rTL_semantics_separate : SemanticsUtils.sem_graph_params
361
362val rTL_semantics_separate_overflow : SemanticsUtils.sem_graph_params
363
364val rTL_semantics_unique : SemanticsUtils.sem_graph_params
365
Note: See TracBrowser for help on using the repository browser.