source: extracted/csem.mli @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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