source: extracted/cminor_semantics.ml @ 3001

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

New extraction.

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