source: extracted/rTLabs_semantics.mli @ 2636

Last change on this file since 2636 was 2636, checked in by campbell, 8 years ago

Extracted front-end.

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