source: driver/extracted/rTL_semantics.mli @ 3106

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

New extraction, it diverges in RTL execution now.

File size: 7.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 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 rtl_setup_call_separate_overflow :
309  Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
310  rTL_state -> rTL_state Errors.res
311
312val rtl_setup_call_unique :
313  Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list ->
314  rTL_state -> rTL_state Errors.res
315
316type rTL_state_pc = Joint_semantics.state_pc
317
318val rtl_save_frame : Registers.register List.list -> rTL_state_pc -> __
319
320val rtl_fetch_external_args :
321  AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
322  Values.val0 List.list Errors.res
323
324val rtl_set_result :
325  Values.val0 List.list -> Registers.register List.list -> rTL_state ->
326  rTL_state Errors.res
327
328val rtl_reg_store :
329  PreIdentifiers.identifier -> ByteValues.beval -> Joint_semantics.state ->
330  Joint_semantics.state
331
332val rtl_reg_retrieve :
333  Joint_semantics.state -> Registers.register -> ByteValues.beval Errors.res
334
335val rtl_read_result :
336  Registers.register List.list -> rTL_state -> ByteValues.beval List.list
337  Errors.res
338
339val rtl_pop_frame_separate :
340  Registers.register List.list -> rTL_state -> (rTL_state,
341  ByteValues.program_counter) Types.prod Errors.res
342
343val rtl_pop_frame_unique :
344  Registers.register List.list -> rTL_state -> (rTL_state,
345  ByteValues.program_counter) Types.prod Errors.res
346
347val block_of_register_pair :
348  Registers.register -> Registers.register -> rTL_state -> Pointers.block
349  Errors.res
350
351val eval_rtl_seq :
352  RTL.rtl_seq -> AST.ident -> rTL_state -> rTL_state Errors.res
353
354val reg_res_store :
355  PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
356  Errors.res
357
358val rTL_semantics_separate : SemanticsUtils.sem_graph_params
359
360val rTL_semantics_separate_overflow : SemanticsUtils.sem_graph_params
361
362val rTL_semantics_unique : SemanticsUtils.sem_graph_params
363
Note: See TracBrowser for help on using the repository browser.