source: extracted/cminor_semantics.ml @ 2827

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

Everything extracted again.

File size: 36.1 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open Extralib
12
13open Lists
14
15open Identifiers
16
17open Integers
18
19open AST
20
21open Division
22
23open Exp
24
25open Arithmetic
26
27open Extranat
28
29open Vector
30
31open FoldStuff
32
33open BitVector
34
35open Z
36
37open BitVectorZ
38
39open Pointers
40
41open ErrorMessages
42
43open Option
44
45open Setoids
46
47open Monad
48
49open Positive
50
51open PreIdentifiers
52
53open Errors
54
55open Div_and_mod
56
57open Jmeq
58
59open Russell
60
61open Util
62
63open Bool
64
65open Relations
66
67open Nat
68
69open List
70
71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
79open Types
80
81open Coqlib
82
83open Values
84
85open Events
86
87open FrontEndVal
88
89open Hide
90
91open ByteValues
92
93open GenMem
94
95open FrontEndMem
96
97open IOMonad
98
99open IO
100
101open Extra_bool
102
103open Globalenvs
104
105open SmallstepExec
106
107open FrontEndOps
108
109open Cminor_syntax
110
111type env = Values.val0 Identifiers.identifier_map
112
113type genv = Cminor_syntax.internal_function AST.fundef Globalenvs.genv_t
114
115type cont =
116| Kend
117| Kseq of Cminor_syntax.stmt * cont
118| Kblock of cont
119
120(** val cont_rect_Type4 :
121    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
122    -> cont -> 'a1 **)
123let rec cont_rect_Type4 h_Kend h_Kseq h_Kblock = function
124| Kend -> h_Kend
125| Kseq (x_70, x_69) ->
126  h_Kseq x_70 x_69 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_69)
127| Kblock x_71 -> h_Kblock x_71 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_71)
128
129(** val cont_rect_Type3 :
130    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
131    -> cont -> 'a1 **)
132let rec cont_rect_Type3 h_Kend h_Kseq h_Kblock = function
133| Kend -> h_Kend
134| Kseq (x_84, x_83) ->
135  h_Kseq x_84 x_83 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_83)
136| Kblock x_85 -> h_Kblock x_85 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_85)
137
138(** val cont_rect_Type2 :
139    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
140    -> cont -> 'a1 **)
141let rec cont_rect_Type2 h_Kend h_Kseq h_Kblock = function
142| Kend -> h_Kend
143| Kseq (x_91, x_90) ->
144  h_Kseq x_91 x_90 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_90)
145| Kblock x_92 -> h_Kblock x_92 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_92)
146
147(** val cont_rect_Type1 :
148    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
149    -> cont -> 'a1 **)
150let rec cont_rect_Type1 h_Kend h_Kseq h_Kblock = function
151| Kend -> h_Kend
152| Kseq (x_98, x_97) ->
153  h_Kseq x_98 x_97 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_97)
154| Kblock x_99 -> h_Kblock x_99 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_99)
155
156(** val cont_rect_Type0 :
157    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
158    -> cont -> 'a1 **)
159let rec cont_rect_Type0 h_Kend h_Kseq h_Kblock = function
160| Kend -> h_Kend
161| Kseq (x_105, x_104) ->
162  h_Kseq x_105 x_104 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_104)
163| Kblock x_106 ->
164  h_Kblock x_106 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_106)
165
166(** val cont_inv_rect_Type4 :
167    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
168    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
169let cont_inv_rect_Type4 hterm h1 h2 h3 =
170  let hcut = cont_rect_Type4 h1 h2 h3 hterm in hcut __
171
172(** val cont_inv_rect_Type3 :
173    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
174    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
175let cont_inv_rect_Type3 hterm h1 h2 h3 =
176  let hcut = cont_rect_Type3 h1 h2 h3 hterm in hcut __
177
178(** val cont_inv_rect_Type2 :
179    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
180    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
181let cont_inv_rect_Type2 hterm h1 h2 h3 =
182  let hcut = cont_rect_Type2 h1 h2 h3 hterm in hcut __
183
184(** val cont_inv_rect_Type1 :
185    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
186    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
187let cont_inv_rect_Type1 hterm h1 h2 h3 =
188  let hcut = cont_rect_Type1 h1 h2 h3 hterm in hcut __
189
190(** val cont_inv_rect_Type0 :
191    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
192    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
193let cont_inv_rect_Type0 hterm h1 h2 h3 =
194  let hcut = cont_rect_Type0 h1 h2 h3 hterm in hcut __
195
196(** val cont_discr : cont -> cont -> __ **)
197let cont_discr x y =
198  Logic.eq_rect_Type2 x
199    (match x with
200     | Kend -> Obj.magic (fun _ dH -> dH)
201     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
202     | Kblock a0 -> Obj.magic (fun _ dH -> dH __)) y
203
204(** val cont_jmdiscr : cont -> cont -> __ **)
205let cont_jmdiscr x y =
206  Logic.eq_rect_Type2 x
207    (match x with
208     | Kend -> Obj.magic (fun _ dH -> dH)
209     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
210     | Kblock a0 -> Obj.magic (fun _ dH -> dH __)) y
211
212type stack =
213| SStop
214| Scall of (AST.ident, AST.typ) Types.prod Types.option
215   * Cminor_syntax.internal_function * Pointers.block * env * cont * 
216   stack
217
218(** val stack_rect_Type4 :
219    'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
220    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
221    cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
222let rec stack_rect_Type4 h_SStop h_Scall = function
223| SStop -> h_SStop
224| Scall (dest, f, x_165, en, k, x_161) ->
225  h_Scall dest f x_165 en __ __ k __ x_161
226    (stack_rect_Type4 h_SStop h_Scall x_161)
227
228(** val stack_rect_Type3 :
229    'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
230    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
231    cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
232let rec stack_rect_Type3 h_SStop h_Scall = function
233| SStop -> h_SStop
234| Scall (dest, f, x_181, en, k, x_177) ->
235  h_Scall dest f x_181 en __ __ k __ x_177
236    (stack_rect_Type3 h_SStop h_Scall x_177)
237
238(** val stack_rect_Type2 :
239    'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
240    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
241    cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
242let rec stack_rect_Type2 h_SStop h_Scall = function
243| SStop -> h_SStop
244| Scall (dest, f, x_189, en, k, x_185) ->
245  h_Scall dest f x_189 en __ __ k __ x_185
246    (stack_rect_Type2 h_SStop h_Scall x_185)
247
248(** val stack_rect_Type1 :
249    'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
250    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
251    cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
252let rec stack_rect_Type1 h_SStop h_Scall = function
253| SStop -> h_SStop
254| Scall (dest, f, x_197, en, k, x_193) ->
255  h_Scall dest f x_197 en __ __ k __ x_193
256    (stack_rect_Type1 h_SStop h_Scall x_193)
257
258(** val stack_rect_Type0 :
259    'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
260    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
261    cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
262let rec stack_rect_Type0 h_SStop h_Scall = function
263| SStop -> h_SStop
264| Scall (dest, f, x_205, en, k, x_201) ->
265  h_Scall dest f x_205 en __ __ k __ x_201
266    (stack_rect_Type0 h_SStop h_Scall x_201)
267
268(** val stack_inv_rect_Type4 :
269    stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
270    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
271    cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
272let stack_inv_rect_Type4 hterm h1 h2 =
273  let hcut = stack_rect_Type4 h1 h2 hterm in hcut __
274
275(** val stack_inv_rect_Type3 :
276    stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
277    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
278    cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
279let stack_inv_rect_Type3 hterm h1 h2 =
280  let hcut = stack_rect_Type3 h1 h2 hterm in hcut __
281
282(** val stack_inv_rect_Type2 :
283    stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
284    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
285    cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
286let stack_inv_rect_Type2 hterm h1 h2 =
287  let hcut = stack_rect_Type2 h1 h2 hterm in hcut __
288
289(** val stack_inv_rect_Type1 :
290    stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
291    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
292    cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
293let stack_inv_rect_Type1 hterm h1 h2 =
294  let hcut = stack_rect_Type1 h1 h2 hterm in hcut __
295
296(** val stack_inv_rect_Type0 :
297    stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
298    Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
299    cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
300let stack_inv_rect_Type0 hterm h1 h2 =
301  let hcut = stack_rect_Type0 h1 h2 hterm in hcut __
302
303(** val stack_jmdiscr : stack -> stack -> __ **)
304let stack_jmdiscr x y =
305  Logic.eq_rect_Type2 x
306    (match x with
307     | SStop -> Obj.magic (fun _ dH -> dH)
308     | Scall (a0, a1, a2, a3, a6, a8) ->
309       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __)) y
310
311type state =
312| State of Cminor_syntax.internal_function * Cminor_syntax.stmt * env
313   * GenMem.mem * Pointers.block * cont * stack
314| Callstate of AST.ident * Cminor_syntax.internal_function AST.fundef
315   * Values.val0 List.list * GenMem.mem * stack
316| Returnstate of Values.val0 Types.option * GenMem.mem * stack
317| Finalstate of Integers.int
318
319(** val state_rect_Type4 :
320    (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
321    -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
322    (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
323    List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
324    GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
325let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
326| State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
327| Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
328| Returnstate (v, m, st) -> h_Returnstate v m st
329| Finalstate r -> h_Finalstate r
330
331(** val state_rect_Type5 :
332    (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
333    -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
334    (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
335    List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
336    GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
337let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
338| State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
339| Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
340| Returnstate (v, m, st) -> h_Returnstate v m st
341| Finalstate r -> h_Finalstate r
342
343(** val state_rect_Type3 :
344    (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
345    -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
346    (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
347    List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
348    GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
349let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
350| State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
351| Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
352| Returnstate (v, m, st) -> h_Returnstate v m st
353| Finalstate r -> h_Finalstate r
354
355(** val state_rect_Type2 :
356    (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
357    -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
358    (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
359    List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
360    GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
361let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
362| State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
363| Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
364| Returnstate (v, m, st) -> h_Returnstate v m st
365| Finalstate r -> h_Finalstate r
366
367(** val state_rect_Type1 :
368    (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
369    -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
370    (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
371    List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
372    GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
373let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
374| State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
375| Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
376| Returnstate (v, m, st) -> h_Returnstate v m st
377| Finalstate r -> h_Finalstate r
378
379(** val state_rect_Type0 :
380    (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
381    -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
382    (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
383    List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
384    GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
385let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
386| State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
387| Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
388| Returnstate (v, m, st) -> h_Returnstate v m st
389| Finalstate r -> h_Finalstate r
390
391(** val state_inv_rect_Type4 :
392    state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
393    __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
394    'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
395    Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
396    (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
397    (Integers.int -> __ -> 'a1) -> 'a1 **)
398let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
399  let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __
400
401(** val state_inv_rect_Type3 :
402    state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
403    __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
404    'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
405    Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
406    (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
407    (Integers.int -> __ -> 'a1) -> 'a1 **)
408let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
409  let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __
410
411(** val state_inv_rect_Type2 :
412    state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
413    __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
414    'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
415    Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
416    (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
417    (Integers.int -> __ -> 'a1) -> 'a1 **)
418let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
419  let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __
420
421(** val state_inv_rect_Type1 :
422    state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
423    __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
424    'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
425    Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
426    (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
427    (Integers.int -> __ -> 'a1) -> 'a1 **)
428let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
429  let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __
430
431(** val state_inv_rect_Type0 :
432    state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
433    __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
434    'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
435    Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
436    (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
437    (Integers.int -> __ -> 'a1) -> 'a1 **)
438let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
439  let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __
440
441(** val state_jmdiscr : state -> state -> __ **)
442let state_jmdiscr x y =
443  Logic.eq_rect_Type2 x
444    (match x with
445     | State (a0, a1, a2, a5, a6, a7, a9) ->
446       Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)
447     | Callstate (a0, a1, a2, a3, a4) ->
448       Obj.magic (fun _ dH -> dH __ __ __ __ __)
449     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
450     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
451
452(** val eval_expr :
453    genv -> AST.typ -> Cminor_syntax.expr -> env -> Pointers.block ->
454    GenMem.mem -> (Events.trace, Values.val0) Types.prod Errors.res **)
455let rec eval_expr ge ty0 e en sp m =
456  (match e with
457   | Cminor_syntax.Id (x, i) ->
458     (fun _ ->
459       let r = Identifiers.lookup_present PreIdentifiers.SymbolTag en i in
460       Errors.OK { Types.fst = Events.e0; Types.snd = r })
461   | Cminor_syntax.Cst (x, c) ->
462     (fun _ ->
463       Obj.magic
464         (Monad.m_bind0 (Monad.max_def Errors.res0)
465           (Obj.magic
466             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedConstant)
467               (FrontEndOps.eval_constant x (Globalenvs.find_symbol ge) sp c)))
468           (fun r ->
469           Obj.magic (Errors.OK { Types.fst = Events.e0; Types.snd = r }))))
470   | Cminor_syntax.Op1 (ty, ty', op, e') ->
471     (fun _ ->
472       Obj.magic
473         (Monad.m_bind2 (Monad.max_def Errors.res0)
474           (Obj.magic (eval_expr ge ty e' en sp m)) (fun tr v ->
475           Monad.m_bind0 (Monad.max_def Errors.res0)
476             (Obj.magic
477               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
478                 (FrontEndOps.eval_unop ty ty' op v))) (fun r ->
479             Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r })))))
480   | Cminor_syntax.Op2 (ty1, ty2, ty', op, e1, e2) ->
481     (fun _ ->
482       Obj.magic
483         (Monad.m_bind2 (Monad.max_def Errors.res0)
484           (Obj.magic (eval_expr ge ty1 e1 en sp m)) (fun tr1 v1 ->
485           Monad.m_bind2 (Monad.max_def Errors.res0)
486             (Obj.magic (eval_expr ge ty2 e2 en sp m)) (fun tr2 v2 ->
487             Monad.m_bind0 (Monad.max_def Errors.res0)
488               (Obj.magic
489                 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
490                   (FrontEndOps.eval_binop m ty1 ty2 ty' op v1 v2)))
491               (fun r ->
492               Obj.magic (Errors.OK { Types.fst = (Events.eapp tr1 tr2);
493                 Types.snd = r }))))))
494   | Cminor_syntax.Mem (ty, e0) ->
495     (fun _ ->
496       Obj.magic
497         (Monad.m_bind2 (Monad.max_def Errors.res0)
498           (Obj.magic (eval_expr ge AST.ASTptr e0 en sp m)) (fun tr v ->
499           Monad.m_bind0 (Monad.max_def Errors.res0)
500             (Obj.magic
501               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
502                 (FrontEndMem.loadv ty m v))) (fun r ->
503             Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r })))))
504   | Cminor_syntax.Cond (sz, sg, ty, e', e1, e2) ->
505     (fun _ ->
506       Obj.magic
507         (Monad.m_bind2 (Monad.max_def Errors.res0)
508           (Obj.magic (eval_expr ge (AST.ASTint (sz, sg)) e' en sp m))
509           (fun tr v ->
510           Monad.m_bind0 (Monad.max_def Errors.res0)
511             (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
512             Monad.m_bind2 (Monad.max_def Errors.res0)
513               (Obj.magic
514                 (eval_expr ge ty
515                   (match b with
516                    | Bool.True -> e1
517                    | Bool.False -> e2) en sp m)) (fun tr' r ->
518               Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr');
519                 Types.snd = r }))))))
520   | Cminor_syntax.Ecost (ty, l, e') ->
521     (fun _ ->
522       Obj.magic
523         (Monad.m_bind2 (Monad.max_def Errors.res0)
524           (Obj.magic (eval_expr ge ty e' en sp m)) (fun tr r ->
525           Obj.magic (Errors.OK { Types.fst =
526             (Events.eapp (Events.echarge l) tr); Types.snd = r }))))) __
527
528(** val k_exit :
529    Nat.nat -> cont -> Cminor_syntax.internal_function -> env -> cont
530    Types.sig0 Errors.res **)
531let rec k_exit n k f en =
532  (match k with
533   | Kend -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadState))
534   | Kseq (x, k') -> (fun _ -> k_exit n k' f en)
535   | Kblock k' ->
536     (fun _ ->
537       match n with
538       | Nat.O -> Errors.OK k'
539       | Nat.S m -> k_exit m k' f en)) __
540
541(** val find_case :
542    AST.intsize -> AST.bvint -> (AST.bvint, 'a1) Types.prod List.list -> 'a1
543    -> 'a1 **)
544let rec find_case sz i cs default =
545  match cs with
546  | List.Nil -> default
547  | List.Cons (h, t) ->
548    let { Types.fst = hi; Types.snd = a } = h in
549    (match BitVector.eq_bv (AST.bitsize_of_intsize sz) i hi with
550     | Bool.True -> a
551     | Bool.False -> find_case sz i t default)
552
553(** val find_label :
554    PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
555    Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
556    Types.prod Types.sig0 Types.option **)
557let rec find_label l s k f en =
558  (match s with
559   | Cminor_syntax.St_skip -> (fun _ -> Types.None)
560   | Cminor_syntax.St_assign (x, x0, x1) -> (fun _ -> Types.None)
561   | Cminor_syntax.St_store (x, x0, x1) -> (fun _ -> Types.None)
562   | Cminor_syntax.St_call (x, x0, x1) -> (fun _ -> Types.None)
563   | Cminor_syntax.St_seq (s1, s2) ->
564     (fun _ ->
565       match find_label l s1 (Kseq (s2, k)) f en with
566       | Types.None -> find_label l s2 k f en
567       | Types.Some sk -> Types.Some sk)
568   | Cminor_syntax.St_ifthenelse (x, x0, x1, s1, s2) ->
569     (fun _ ->
570       match find_label l s1 k f en with
571       | Types.None -> find_label l s2 k f en
572       | Types.Some sk -> Types.Some sk)
573   | Cminor_syntax.St_return x -> (fun _ -> Types.None)
574   | Cminor_syntax.St_label (l', s') ->
575     (fun _ ->
576       match Identifiers.identifier_eq PreIdentifiers.Label l l' with
577       | Types.Inl _ -> Types.Some { Types.fst = s'; Types.snd = k }
578       | Types.Inr _ -> find_label l s' k f en)
579   | Cminor_syntax.St_goto x -> (fun _ -> Types.None)
580   | Cminor_syntax.St_cost (x, s') -> (fun _ -> find_label l s' k f en)) __
581
582(** val find_label_always :
583    PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
584    Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
585    Types.prod Types.sig0 **)
586let find_label_always l s k f en =
587  (match find_label l s k f en with
588   | Types.None -> (fun _ -> assert false (* absurd case *))
589   | Types.Some sk -> (fun _ -> sk)) __
590
591(** val bind_params :
592    Values.val0 List.list -> (AST.ident, AST.typ) Types.prod List.list -> env
593    Types.sig0 Errors.res **)
594let rec bind_params vs ids =
595  match vs with
596  | List.Nil ->
597    (match ids with
598     | List.Nil -> Errors.OK (Identifiers.empty_map PreIdentifiers.SymbolTag)
599     | List.Cons (x, x0) ->
600       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters))
601  | List.Cons (v, vt) ->
602    (match ids with
603     | List.Nil ->
604       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)
605     | List.Cons (idh, idt) ->
606       let { Types.fst = id; Types.snd = ty } = idh in
607       Obj.magic
608         (Monad.m_bind0 (Monad.max_def Errors.res0)
609           (Obj.magic (bind_params vt idt)) (fun en ->
610           Obj.magic (Errors.OK
611             (Identifiers.add PreIdentifiers.SymbolTag (Types.pi1 en)
612               idh.Types.fst v)))))
613
614(** val init_locals :
615    env -> (AST.ident, AST.typ) Types.prod List.list -> env **)
616let init_locals =
617  List.foldr (fun idty en ->
618    Identifiers.add PreIdentifiers.SymbolTag en idty.Types.fst Values.Vundef)
619
620(** val trace_map_inv :
621    ('a1 -> __ -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list
622    -> (Events.trace, 'a2 List.list) Types.prod Errors.res **)
623let rec trace_map_inv f l =
624  (match l with
625   | List.Nil ->
626     (fun _ -> Errors.OK { Types.fst = Events.e0; Types.snd = List.Nil })
627   | List.Cons (h, t) ->
628     (fun _ ->
629       Obj.magic
630         (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic f h __)
631           (fun tr h' ->
632           Monad.m_bind2 (Monad.max_def Errors.res0)
633             (Obj.magic (trace_map_inv f t)) (fun tr' t' ->
634             Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr');
635               Types.snd = (List.Cons (h', t')) })))))) __
636
637(** val eval_step :
638    genv -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod)
639    IOMonad.iO **)
640let eval_step ge = function
641| State (f, s, en, m, sp, k, st0) ->
642  IOMonad.err_to_io
643    ((match s with
644      | Cminor_syntax.St_skip ->
645        (fun _ ->
646          (match k with
647           | Kend ->
648             (fun _ ->
649               Obj.magic
650                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
651                   Events.e0; Types.snd = (Returnstate (Types.None,
652                   (GenMem.free m sp), st0)) }))
653           | Kseq (s', k') ->
654             (fun _ ->
655               Obj.magic
656                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
657                   Events.e0; Types.snd = (State (f, s', en, m, sp, k',
658                   st0)) }))
659           | Kblock k' ->
660             (fun _ ->
661               Obj.magic
662                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
663                   Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip,
664                   en, m, sp, k', st0)) }))) __)
665      | Cminor_syntax.St_assign (x, id, e) ->
666        (fun _ ->
667          Obj.magic
668            (Monad.m_bind2 (Monad.max_def Errors.res0)
669              (Obj.magic (eval_expr ge x e en sp m)) (fun tr v ->
670              let en' =
671                Identifiers.update_present PreIdentifiers.SymbolTag en id v
672              in
673              Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
674                Types.snd = (State (f, Cminor_syntax.St_skip, en', m, sp, k,
675                st0)) })))
676      | Cminor_syntax.St_store (ty, edst, e) ->
677        (fun _ ->
678          Obj.magic
679            (Monad.m_bind2 (Monad.max_def Errors.res0)
680              (Obj.magic (eval_expr ge AST.ASTptr edst en sp m))
681              (fun tr vdst ->
682              Monad.m_bind2 (Monad.max_def Errors.res0)
683                (Obj.magic (eval_expr ge ty e en sp m)) (fun tr' v ->
684                Monad.m_bind0 (Monad.max_def Errors.res0)
685                  (Obj.magic
686                    (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
687                      (FrontEndMem.storev ty m vdst v))) (fun m' ->
688                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
689                    (Events.eapp tr tr'); Types.snd = (State (f,
690                    Cminor_syntax.St_skip, en, m', sp, k, st0)) })))))
691      | Cminor_syntax.St_call (dst, ef, args) ->
692        (fun _ ->
693          Obj.magic
694            (Monad.m_bind2 (Monad.max_def Errors.res0)
695              (Obj.magic (eval_expr ge AST.ASTptr ef en sp m)) (fun tr vf ->
696              Monad.m_bind2 (Monad.max_def Errors.res0)
697                (Obj.magic
698                  (Errors.opt_to_res
699                    (Errors.msg ErrorMessages.BadFunctionValue)
700                    (Globalenvs.find_funct_id ge vf))) (fun fd id ->
701                Monad.m_bind2 (Monad.max_def Errors.res0)
702                  (Obj.magic
703                    (trace_map_inv (fun e ->
704                      let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
705                      (fun _ -> eval_expr ge ty e0 en sp m)) args))
706                  (fun tr' vargs ->
707                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
708                    (Events.eapp tr tr'); Types.snd = (Callstate (id, fd,
709                    vargs, m, (Scall (dst, f, sp, en, k, st0)))) })))))
710      | Cminor_syntax.St_seq (s1, s2) ->
711        (fun _ ->
712          Obj.magic
713            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
714              Events.e0; Types.snd = (State (f, s1, en, m, sp, (Kseq (s2,
715              k)), st0)) }))
716      | Cminor_syntax.St_ifthenelse (x, x0, e, strue, sfalse) ->
717        (fun _ ->
718          Obj.magic
719            (Monad.m_bind2 (Monad.max_def Errors.res0)
720              (Obj.magic (eval_expr ge (AST.ASTint (x, x0)) e en sp m))
721              (fun tr v ->
722              Monad.m_bind0 (Monad.max_def Errors.res0)
723                (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
724                Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
725                  Types.snd = (State (f,
726                  (match b with
727                   | Bool.True -> strue
728                   | Bool.False -> sfalse), en, m, sp, k, st0)) }))))
729      | Cminor_syntax.St_return eo ->
730        (match eo with
731         | Types.None ->
732           (fun _ ->
733             Obj.magic
734               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
735                 Events.e0; Types.snd = (Returnstate (Types.None,
736                 (GenMem.free m sp), st0)) }))
737         | Types.Some e ->
738           let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
739           (fun _ ->
740           Obj.magic
741             (Monad.m_bind2 (Monad.max_def Errors.res0)
742               (Obj.magic (eval_expr ge ty e0 en sp m)) (fun tr v ->
743               Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
744                 Types.snd = (Returnstate ((Types.Some v),
745                 (GenMem.free m sp), st0)) }))))
746      | Cminor_syntax.St_label (l, s') ->
747        (fun _ ->
748          Obj.magic
749            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
750              Events.e0; Types.snd = (State (f, s', en, m, sp, k, st0)) }))
751      | Cminor_syntax.St_goto l ->
752        (fun _ ->
753          let sk = find_label_always l f.Cminor_syntax.f_body Kend f en in
754          Obj.magic
755            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
756              Events.e0; Types.snd = (State (f, sk.Types.fst, en, m, sp,
757              sk.Types.snd, st0)) }))
758      | Cminor_syntax.St_cost (l, s') ->
759        (fun _ ->
760          Obj.magic
761            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
762              (Events.echarge l); Types.snd = (State (f, s', en, m, sp, k,
763              st0)) }))) __)
764| Callstate (x, fd, args, m, st0) ->
765  (match fd with
766   | AST.Internal f ->
767     IOMonad.err_to_io
768       (let { Types.fst = m'; Types.snd = sp } =
769          GenMem.alloc m (Z.z_of_nat Nat.O)
770            (Z.z_of_nat f.Cminor_syntax.f_stacksize)
771        in
772       Obj.magic
773         (Monad.m_bind0 (Monad.max_def Errors.res0)
774           (Obj.magic (bind_params args f.Cminor_syntax.f_params)) (fun en ->
775           Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
776             Events.e0; Types.snd = (State (f, f.Cminor_syntax.f_body,
777             (init_locals (Types.pi1 en) f.Cminor_syntax.f_vars), m', sp,
778             Kend, st0)) })))
779   | AST.External fn ->
780     Obj.magic
781       (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
782         (Obj.magic
783           (IOMonad.err_to_io
784             (IO.check_eventval_list args fn.AST.ef_sig.AST.sig_args)))
785         (fun evargs ->
786         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
787           (Obj.magic
788             (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
789           (fun evres ->
790           let res =
791             match fn.AST.ef_sig.AST.sig_res with
792             | Types.None -> Types.None
793             | Types.Some x0 ->
794               Types.Some (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)
795           in
796           Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
797             (Events.eextcall fn.AST.ef_id evargs
798               (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
799             Types.snd = (Returnstate (res, m, st0)) }))))
800| Returnstate (result, m, st0) ->
801  IOMonad.err_to_io
802    (match st0 with
803     | SStop ->
804       (match result with
805        | Types.None ->
806          Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
807        | Types.Some v ->
808          (match v with
809           | Values.Vundef ->
810             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
811           | Values.Vint (sz, r) ->
812             (match sz with
813              | AST.I8 ->
814                (fun x -> Errors.Error
815                  (Errors.msg ErrorMessages.ReturnMismatch))
816              | AST.I16 ->
817                (fun x -> Errors.Error
818                  (Errors.msg ErrorMessages.ReturnMismatch))
819              | AST.I32 ->
820                (fun r0 ->
821                  Obj.magic
822                    (Monad.m_return0 (Monad.max_def Errors.res0)
823                      { Types.fst = Events.e0; Types.snd = (Finalstate r0) })))
824               r
825           | Values.Vnull ->
826             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
827           | Values.Vptr x ->
828             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)))
829     | Scall (dst, f, sp, en, k, st') ->
830       (match result with
831        | Types.None ->
832          (match dst with
833           | Types.None ->
834             Obj.magic
835               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
836                 Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip, en,
837                 m, sp, k, st')) })
838           | Types.Some x ->
839             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
840        | Types.Some v ->
841          (match dst with
842           | Types.None ->
843             (fun _ -> Errors.Error
844               (Errors.msg ErrorMessages.ReturnMismatch))
845           | Types.Some idty ->
846             (fun _ ->
847               Obj.magic
848                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
849                   Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip,
850                   (Identifiers.update_present PreIdentifiers.SymbolTag en
851                     idty.Types.fst v), m, sp, k, st')) }))) __))
852| Finalstate r ->
853  IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.BadState))
854
855(** val is_final : state -> Integers.int Types.option **)
856let is_final = function
857| State (x, x0, x1, x4, x5, x6, x8) -> Types.None
858| Callstate (x, x0, x1, x2, x3) -> Types.None
859| Returnstate (x, x0, x1) -> Types.None
860| Finalstate r -> Types.Some r
861
862(** val cminor_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
863let cminor_exec =
864  { SmallstepExec.is_final = (fun x -> Obj.magic is_final);
865    SmallstepExec.step = (Obj.magic eval_step) }
866
867(** val make_global : Cminor_syntax.cminor_program -> genv **)
868let make_global p =
869  Globalenvs.globalenv (fun x -> x) p
870
871(** val make_initial_state :
872    Cminor_syntax.cminor_program -> state Errors.res **)
873let make_initial_state p =
874  let ge = make_global p in
875  Obj.magic
876    (Monad.m_bind0 (Monad.max_def Errors.res0)
877      (Obj.magic (Globalenvs.init_mem (fun x -> x) p)) (fun m ->
878      Monad.m_bind0 (Monad.max_def Errors.res0)
879        (Obj.magic
880          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
881            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
882        Monad.m_bind0 (Monad.max_def Errors.res0)
883          (Obj.magic
884            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
885              (Globalenvs.find_funct_ptr ge b))) (fun f ->
886          Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m,
887            SStop)))))))
888
889(** val cminor_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
890let cminor_fullexec =
891  { SmallstepExec.es1 = cminor_exec; SmallstepExec.make_global =
892    (Obj.magic make_global); SmallstepExec.make_initial_state =
893    (Obj.magic make_initial_state) }
894
895(** val make_noinit_global : Cminor_syntax.cminor_noinit_program -> genv **)
896let make_noinit_global p =
897  Globalenvs.globalenv (fun x -> List.Cons ((AST.Init_space x), List.Nil)) p
898
899(** val make_initial_noinit_state :
900    Cminor_syntax.cminor_noinit_program -> state Errors.res **)
901let make_initial_noinit_state p =
902  let ge = make_noinit_global p in
903  Obj.magic
904    (Monad.m_bind0 (Monad.max_def Errors.res0)
905      (Obj.magic
906        (Globalenvs.init_mem (fun x -> List.Cons ((AST.Init_space x),
907          List.Nil)) p)) (fun m ->
908      Monad.m_bind0 (Monad.max_def Errors.res0)
909        (Obj.magic
910          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
911            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
912        Monad.m_bind0 (Monad.max_def Errors.res0)
913          (Obj.magic
914            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
915              (Globalenvs.find_funct_ptr ge b))) (fun f ->
916          Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m,
917            SStop)))))))
918
919(** val cminor_noinit_fullexec :
920    (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
921let cminor_noinit_fullexec =
922  { SmallstepExec.es1 = cminor_exec; SmallstepExec.make_global =
923    (Obj.magic make_noinit_global); SmallstepExec.make_initial_state =
924    (Obj.magic make_initial_noinit_state) }
925
Note: See TracBrowser for help on using the repository browser.