source: extracted/csem.mli @ 2649

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

...

File size: 13.6 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open Hide
12
13open ByteValues
14
15open Division
16
17open Z
18
19open BitVectorZ
20
21open Pointers
22
23open GenMem
24
25open FrontEndMem
26
27open Proper
28
29open PositiveMap
30
31open Deqsets
32
33open Extralib
34
35open Lists
36
37open Identifiers
38
39open Arithmetic
40
41open Vector
42
43open Div_and_mod
44
45open Util
46
47open FoldStuff
48
49open BitVector
50
51open Extranat
52
53open Integers
54
55open AST
56
57open ErrorMessages
58
59open Option
60
61open Setoids
62
63open Monad
64
65open Jmeq
66
67open Russell
68
69open Positive
70
71open PreIdentifiers
72
73open Bool
74
75open Relations
76
77open Nat
78
79open List
80
81open Hints_declaration
82
83open Core_notation
84
85open Pts
86
87open Logic
88
89open Types
90
91open Errors
92
93open Globalenvs
94
95open CostLabel
96
97open Csyntax
98
99open Events
100
101open Smallstep
102
103open TypeComparison
104
105open ClassifyOp
106
107val sem_neg : Values.val0 -> Csyntax.type0 -> Values.val0 Types.option
108
109val sem_notint : Values.val0 -> Values.val0 Types.option
110
111val sem_notbool : Values.val0 -> Csyntax.type0 -> Values.val0 Types.option
112
113val sem_add :
114  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
115  Types.option
116
117val sem_sub :
118  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
119  Csyntax.type0 -> Values.val0 Types.option
120
121val sem_mul :
122  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
123  Types.option
124
125val sem_div :
126  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
127  Types.option
128
129val sem_mod :
130  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
131  Types.option
132
133val sem_and : Values.val0 -> Values.val0 -> Values.val0 Types.option
134
135val sem_or : Values.val0 -> Values.val0 -> Values.val0 Types.option
136
137val sem_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option
138
139val sem_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option
140
141val sem_shr :
142  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
143  Types.option
144
145val sem_cmp_mismatch : Integers.comparison -> Values.val0 Types.option
146
147val sem_cmp_match : Integers.comparison -> Values.val0 Types.option
148
149val sem_cmp :
150  Integers.comparison -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
151  Csyntax.type0 -> GenMem.mem1 -> Values.val0 Types.option
152
153val cast_bool_to_target :
154  Csyntax.type0 -> Values.val0 Types.option -> Values.val0 Types.option
155
156val sem_unary_operation :
157  Csyntax.unary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
158  Types.option
159
160val sem_binary_operation :
161  Csyntax.binary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
162  Csyntax.type0 -> GenMem.mem1 -> Csyntax.type0 -> Values.val0 Types.option
163
164val cast_int_int :
165  AST.intsize -> AST.signedness -> AST.intsize -> BitVector.bitVector ->
166  BitVector.bitVector
167
168type genv0 = Csyntax.clight_fundef Globalenvs.genv_t
169
170type env = Pointers.block Identifiers.identifier_map
171
172val empty_env : env
173
174val load_value_of_type :
175  Csyntax.type0 -> GenMem.mem1 -> Pointers.block -> Pointers.offset ->
176  Values.val0 Types.option
177
178val store_value_of_type :
179  Csyntax.type0 -> GenMem.mem1 -> Pointers.block -> Pointers.offset ->
180  Values.val0 -> GenMem.mem1 Types.option
181
182val blocks_of_env : env -> Pointers.block List.list
183
184val select_switch :
185  AST.intsize -> BitVector.bitVector -> Csyntax.labeled_statements ->
186  Csyntax.labeled_statements Types.option
187
188val seq_of_labeled_statement :
189  Csyntax.labeled_statements -> Csyntax.statement
190
191type cont =
192| Kstop
193| Kseq of Csyntax.statement * cont
194| Kwhile of Csyntax.expr * Csyntax.statement * cont
195| Kdowhile of Csyntax.expr * Csyntax.statement * cont
196| Kfor2 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
197| Kfor3 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
198| Kswitch of cont
199| Kcall of ((Pointers.block, Pointers.offset) Types.prod, Csyntax.type0)
200           Types.prod Types.option * Csyntax.function0 * env * cont
201
202val cont_rect_Type4 :
203  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
204  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
205  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
206  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
207  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
208  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
209  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
210  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
211
212val cont_rect_Type3 :
213  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
214  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
215  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
216  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
217  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
218  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
219  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
220  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
221
222val cont_rect_Type2 :
223  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
224  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
225  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
226  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
227  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
228  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
229  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
230  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
231
232val cont_rect_Type1 :
233  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
234  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
235  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
236  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
237  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
238  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
239  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
240  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
241
242val cont_rect_Type0 :
243  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
244  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
245  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
246  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
247  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
248  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
249  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
250  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1
251
252val cont_inv_rect_Type4 :
253  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
254  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
255  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
256  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
257  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
258  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
259  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
260  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
261  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
262
263val cont_inv_rect_Type3 :
264  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
265  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
266  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
267  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
268  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
269  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
270  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
271  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
272  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
273
274val cont_inv_rect_Type2 :
275  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
276  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
277  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
278  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
279  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
280  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
281  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
282  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
283  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
284
285val cont_inv_rect_Type1 :
286  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
287  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
288  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
289  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
290  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
291  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
292  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
293  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
294  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
295
296val cont_inv_rect_Type0 :
297  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
298  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
299  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
300  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
301  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
302  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
303  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
304  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
305  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
306
307val cont_discr : cont -> cont -> __
308
309val cont_jmdiscr : cont -> cont -> __
310
311val call_cont : cont -> cont
312
313type state0 =
314| State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem1
315| Callstate of Csyntax.clight_fundef * Values.val0 List.list * cont
316   * GenMem.mem1
317| Returnstate of Values.val0 * cont * GenMem.mem1
318| Finalstate of Integers.int
319
320val state_rect_Type4 :
321  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
322  'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
323  GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
324  (Integers.int -> 'a1) -> state0 -> 'a1
325
326val state_rect_Type5 :
327  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
328  'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
329  GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
330  (Integers.int -> 'a1) -> state0 -> 'a1
331
332val state_rect_Type3 :
333  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
334  'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
335  GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
336  (Integers.int -> 'a1) -> state0 -> 'a1
337
338val state_rect_Type2 :
339  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
340  'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
341  GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
342  (Integers.int -> 'a1) -> state0 -> 'a1
343
344val state_rect_Type1 :
345  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
346  'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
347  GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
348  (Integers.int -> 'a1) -> state0 -> 'a1
349
350val state_rect_Type0 :
351  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
352  'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
353  GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
354  (Integers.int -> 'a1) -> state0 -> 'a1
355
356val state_inv_rect_Type4 :
357  state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
358  GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
359  List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
360  GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
361
362val state_inv_rect_Type3 :
363  state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
364  GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
365  List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
366  GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
367
368val state_inv_rect_Type2 :
369  state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
370  GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
371  List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
372  GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
373
374val state_inv_rect_Type1 :
375  state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
376  GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
377  List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
378  GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
379
380val state_inv_rect_Type0 :
381  state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
382  GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
383  List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
384  GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
385
386val state_discr : state0 -> state0 -> __
387
388val state_jmdiscr : state0 -> state0 -> __
389
390val find_label_ls :
391  Csyntax.label -> Csyntax.labeled_statements -> cont -> (Csyntax.statement,
392  cont) Types.prod Types.option
393
394val find_label :
395  Csyntax.label -> Csyntax.statement -> cont -> (Csyntax.statement, cont)
396  Types.prod Types.option
397
398val fun_typeof : Csyntax.expr -> Csyntax.type0
399
Note: See TracBrowser for help on using the repository browser.