source: extracted/csem.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 13.6 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Values
6
7open FrontEndVal
8
9open Hide
10
11open ByteValues
12
13open Division
14
15open Z
16
17open BitVectorZ
18
19open Pointers
20
21open GenMem
22
23open FrontEndMem
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open Extralib
32
33open Lists
34
35open Identifiers
36
37open Coqlib
38
39open Floats
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 Option
60
61open Setoids
62
63open Monad
64
65open Jmeq
66
67open Russell
68
69open Positive
70
71open Char
72
73open String
74
75open PreIdentifiers
76
77open Bool
78
79open Relations
80
81open Nat
82
83open List
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Types
94
95open Errors
96
97open Globalenvs
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 Csyntax.clight_fundef * Values.val0 List.list * cont
320   * 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) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
327  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) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
333  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) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
339  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) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
345  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) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
351  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) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
357  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) -> (Csyntax.clight_fundef -> Values.val0
363  List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
364  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) -> (Csyntax.clight_fundef -> Values.val0
369  List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
370  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) -> (Csyntax.clight_fundef -> Values.val0
375  List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
376  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) -> (Csyntax.clight_fundef -> Values.val0
381  List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
382  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) -> (Csyntax.clight_fundef -> Values.val0
387  List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
388  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.