source: extracted/rTLabs_semantics.mli @ 2649

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

...
File size: 9.8 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21open ErrorMessages
22
23open Option
24
25open Setoids
26
27open Monad
28
29open Jmeq
30
31open Russell
32
33open Positive
34
35open PreIdentifiers
36
37open Errors
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 Arithmetic
76
77open Vector
78
79open Div_and_mod
80
81open Util
82
83open FoldStuff
84
85open BitVector
86
87open Extranat
88
89open Integers
90
91open AST
92
93open Globalenvs
94
95open CostLabel
96
97open Events
98
99open IOMonad
100
101open IO
102
103open SmallstepExec
104
105open BitVectorTrie
106
107open Graphs
108
109open Order
110
111open Registers
112
113open FrontEndOps
114
115open RTLabs_syntax
116
117type genv = RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t
118
119type frame = { func : RTLabs_syntax.internal_function;
120               locals : Values.val0 Registers.register_env;
121               next : Graphs.label; sp : Pointers.block;
122               retdst : Registers.register Types.option }
123
124val frame_rect_Type4 :
125  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
126  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
127  'a1) -> frame -> 'a1
128
129val frame_rect_Type5 :
130  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
131  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
132  'a1) -> frame -> 'a1
133
134val frame_rect_Type3 :
135  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
136  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
137  'a1) -> frame -> 'a1
138
139val frame_rect_Type2 :
140  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
141  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
142  'a1) -> frame -> 'a1
143
144val frame_rect_Type1 :
145  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
146  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
147  'a1) -> frame -> 'a1
148
149val frame_rect_Type0 :
150  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
151  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
152  'a1) -> frame -> 'a1
153
154val func : frame -> RTLabs_syntax.internal_function
155
156val locals : frame -> Values.val0 Registers.register_env
157
158val next : frame -> Graphs.label
159
160val sp : frame -> Pointers.block
161
162val retdst : frame -> Registers.register Types.option
163
164val frame_inv_rect_Type4 :
165  frame -> (RTLabs_syntax.internal_function -> Values.val0
166  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
167  Registers.register Types.option -> __ -> 'a1) -> 'a1
168
169val frame_inv_rect_Type3 :
170  frame -> (RTLabs_syntax.internal_function -> Values.val0
171  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
172  Registers.register Types.option -> __ -> 'a1) -> 'a1
173
174val frame_inv_rect_Type2 :
175  frame -> (RTLabs_syntax.internal_function -> Values.val0
176  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
177  Registers.register Types.option -> __ -> 'a1) -> 'a1
178
179val frame_inv_rect_Type1 :
180  frame -> (RTLabs_syntax.internal_function -> Values.val0
181  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
182  Registers.register Types.option -> __ -> 'a1) -> 'a1
183
184val frame_inv_rect_Type0 :
185  frame -> (RTLabs_syntax.internal_function -> Values.val0
186  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
187  Registers.register Types.option -> __ -> 'a1) -> 'a1
188
189val frame_jmdiscr : frame -> frame -> __
190
191val adv : Graphs.label -> frame -> frame
192
193type state0 =
194| State of frame * frame List.list * GenMem.mem1
195| Callstate of RTLabs_syntax.internal_function AST.fundef
196   * Values.val0 List.list * Registers.register Types.option
197   * frame List.list * GenMem.mem1
198| Returnstate of Values.val0 Types.option * Registers.register Types.option
199   * frame List.list * GenMem.mem1
200| Finalstate of Integers.int
201
202val state_rect_Type4 :
203  (frame -> frame List.list -> GenMem.mem1 -> 'a1) ->
204  (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
205  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
206  -> (Values.val0 Types.option -> Registers.register Types.option -> frame
207  List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
208
209val state_rect_Type5 :
210  (frame -> frame List.list -> GenMem.mem1 -> 'a1) ->
211  (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
212  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
213  -> (Values.val0 Types.option -> Registers.register Types.option -> frame
214  List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
215
216val state_rect_Type3 :
217  (frame -> frame List.list -> GenMem.mem1 -> 'a1) ->
218  (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
219  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
220  -> (Values.val0 Types.option -> Registers.register Types.option -> frame
221  List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
222
223val state_rect_Type2 :
224  (frame -> frame List.list -> GenMem.mem1 -> 'a1) ->
225  (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
226  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
227  -> (Values.val0 Types.option -> Registers.register Types.option -> frame
228  List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
229
230val state_rect_Type1 :
231  (frame -> frame List.list -> GenMem.mem1 -> 'a1) ->
232  (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
233  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
234  -> (Values.val0 Types.option -> Registers.register Types.option -> frame
235  List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
236
237val state_rect_Type0 :
238  (frame -> frame List.list -> GenMem.mem1 -> 'a1) ->
239  (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
240  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
241  -> (Values.val0 Types.option -> Registers.register Types.option -> frame
242  List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
243
244val state_inv_rect_Type4 :
245  state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
246  (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
247  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
248  'a1) -> (Values.val0 Types.option -> Registers.register Types.option ->
249  frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1)
250  -> 'a1
251
252val state_inv_rect_Type3 :
253  state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
254  (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
255  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
256  'a1) -> (Values.val0 Types.option -> Registers.register Types.option ->
257  frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1)
258  -> 'a1
259
260val state_inv_rect_Type2 :
261  state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
262  (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
263  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
264  'a1) -> (Values.val0 Types.option -> Registers.register Types.option ->
265  frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1)
266  -> 'a1
267
268val state_inv_rect_Type1 :
269  state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
270  (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
271  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
272  'a1) -> (Values.val0 Types.option -> Registers.register Types.option ->
273  frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1)
274  -> 'a1
275
276val state_inv_rect_Type0 :
277  state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
278  (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
279  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
280  'a1) -> (Values.val0 Types.option -> Registers.register Types.option ->
281  frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1)
282  -> 'a1
283
284val state_discr : state0 -> state0 -> __
285
286val state_jmdiscr : state0 -> state0 -> __
287
288val build_state :
289  frame -> frame List.list -> GenMem.mem1 -> Graphs.label -> state0
290
291val next_instruction : frame -> RTLabs_syntax.statement
292
293val init_locals :
294  (Registers.register, AST.typ) Types.prod List.list -> Values.val0
295  Registers.register_env
296
297val reg_store :
298  PreIdentifiers.identifier -> Values.val0 -> Values.val0
299  Identifiers.identifier_map -> Values.val0 Identifiers.identifier_map
300  Errors.res
301
302val params_store :
303  (Registers.register, AST.typ) Types.prod List.list -> Values.val0 List.list
304  -> Values.val0 Registers.register_env -> Values.val0 Registers.register_env
305  Errors.res
306
307val reg_retrieve :
308  Values.val0 Registers.register_env -> Registers.register -> Values.val0
309  Errors.res
310
311val eval_statement :
312  genv -> state0 -> (IO.io_out, IO.io_in, (Events.trace, state0) Types.prod)
313  IOMonad.iO
314
315val rTLabs_is_final : state0 -> Integers.int Types.option
316
317val rTLabs_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
318
319val make_global0 : RTLabs_syntax.rTLabs_program -> genv
320
321val make_initial_state0 : RTLabs_syntax.rTLabs_program -> state0 Errors.res
322
323val rTLabs_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
324
325val bind_ok :
326  'a1 Errors.res -> ('a1 -> 'a2 Errors.res) -> 'a2 -> ('a1 -> __ -> __ ->
327  'a3) -> 'a3
328
329val func_block_of_exec :
330  genv -> state0 -> Events.trace -> RTLabs_syntax.internal_function
331  AST.fundef -> Values.val0 List.list -> Registers.register Types.option ->
332  frame List.list -> GenMem.mem1 -> Pointers.block Types.sig0
333
Note: See TracBrowser for help on using the repository browser.