source: driver/extracted/cminor_semantics.ml @ 3106

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

New extraction

File size: 36.2 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_23729, x_23728) ->
126  h_Kseq x_23729 x_23728 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_23728)
127| Kblock x_23730 ->
128  h_Kblock x_23730 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_23730)
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_23743, x_23742) ->
136  h_Kseq x_23743 x_23742 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_23742)
137| Kblock x_23744 ->
138  h_Kblock x_23744 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_23744)
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_23750, x_23749) ->
146  h_Kseq x_23750 x_23749 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_23749)
147| Kblock x_23751 ->
148  h_Kblock x_23751 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_23751)
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_23757, x_23756) ->
156  h_Kseq x_23757 x_23756 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_23756)
157| Kblock x_23758 ->
158  h_Kblock x_23758 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_23758)
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_23764, x_23763) ->
166  h_Kseq x_23764 x_23763 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_23763)
167| Kblock x_23765 ->
168  h_Kblock x_23765 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_23765)
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_23824, en, k, x_23820) ->
229  h_Scall dest f x_23824 en __ __ k __ x_23820
230    (stack_rect_Type4 h_SStop h_Scall x_23820)
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_23840, en, k, x_23836) ->
239  h_Scall dest f x_23840 en __ __ k __ x_23836
240    (stack_rect_Type3 h_SStop h_Scall x_23836)
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_23848, en, k, x_23844) ->
249  h_Scall dest f x_23848 en __ __ k __ x_23844
250    (stack_rect_Type2 h_SStop h_Scall x_23844)
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_23856, en, k, x_23852) ->
259  h_Scall dest f x_23856 en __ __ k __ x_23852
260    (stack_rect_Type1 h_SStop h_Scall x_23852)
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_23864, en, k, x_23860) ->
269  h_Scall dest f x_23864 en __ __ k __ x_23860
270    (stack_rect_Type0 h_SStop h_Scall x_23860)
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 = e0 } = e in
709                      (fun _ -> eval_expr ge ty e0 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 = e0 } = e in
743           (fun _ ->
744           Obj.magic
745             (Monad.m_bind2 (Monad.max_def Errors.res0)
746               (Obj.magic (eval_expr ge ty e0 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 fn.AST.ef_sig.AST.sig_args)))
789         (fun evargs ->
790         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
791           (Obj.magic
792             (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
793           (fun evres ->
794           let res =
795             match fn.AST.ef_sig.AST.sig_res with
796             | Types.None -> Types.None
797             | Types.Some x0 ->
798               Types.Some (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)
799           in
800           Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
801             (Events.eextcall fn.AST.ef_id evargs
802               (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
803             Types.snd = (Returnstate (res, m, st0)) }))))
804| Returnstate (result, m, st0) ->
805  IOMonad.err_to_io
806    (match st0 with
807     | SStop ->
808       (match result with
809        | Types.None ->
810          Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
811        | Types.Some v ->
812          (match v with
813           | Values.Vundef ->
814             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
815           | Values.Vint (sz, r) ->
816             (match sz with
817              | AST.I8 ->
818                (fun x -> Errors.Error
819                  (Errors.msg ErrorMessages.ReturnMismatch))
820              | AST.I16 ->
821                (fun x -> Errors.Error
822                  (Errors.msg ErrorMessages.ReturnMismatch))
823              | AST.I32 ->
824                (fun r0 ->
825                  Obj.magic
826                    (Monad.m_return0 (Monad.max_def Errors.res0)
827                      { Types.fst = Events.e0; Types.snd = (Finalstate r0) })))
828               r
829           | Values.Vnull ->
830             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
831           | Values.Vptr x ->
832             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)))
833     | Scall (dst, f, sp, en, k, st') ->
834       (match result with
835        | Types.None ->
836          (match dst with
837           | Types.None ->
838             Obj.magic
839               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
840                 Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip, en,
841                 m, sp, k, st')) })
842           | Types.Some x ->
843             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
844        | Types.Some v ->
845          (match dst with
846           | Types.None ->
847             (fun _ -> Errors.Error
848               (Errors.msg ErrorMessages.ReturnMismatch))
849           | Types.Some idty ->
850             (fun _ ->
851               Obj.magic
852                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
853                   Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip,
854                   (Identifiers.update_present PreIdentifiers.SymbolTag en
855                     idty.Types.fst v), m, sp, k, st')) }))) __))
856| Finalstate r ->
857  IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.BadState))
858
859(** val is_final : state -> Integers.int Types.option **)
860let is_final = function
861| State (x, x0, x1, x4, x5, x6, x8) -> Types.None
862| Callstate (x, x0, x1, x2, x3) -> Types.None
863| Returnstate (x, x0, x1) -> Types.None
864| Finalstate r -> Types.Some r
865
866(** val cminor_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
867let cminor_exec =
868  { SmallstepExec.is_final = (fun x -> Obj.magic is_final);
869    SmallstepExec.step = (Obj.magic eval_step) }
870
871(** val make_global : Cminor_syntax.cminor_program -> genv **)
872let make_global p =
873  Globalenvs.globalenv (fun x -> x) p
874
875(** val make_initial_state :
876    Cminor_syntax.cminor_program -> state Errors.res **)
877let make_initial_state p =
878  let ge = make_global p in
879  Obj.magic
880    (Monad.m_bind0 (Monad.max_def Errors.res0)
881      (Obj.magic (Globalenvs.init_mem (fun x -> x) p)) (fun m ->
882      Monad.m_bind0 (Monad.max_def Errors.res0)
883        (Obj.magic
884          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
885            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
886        Monad.m_bind0 (Monad.max_def Errors.res0)
887          (Obj.magic
888            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
889              (Globalenvs.find_funct_ptr ge b))) (fun f ->
890          Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m,
891            SStop)))))))
892
893(** val cminor_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
894let cminor_fullexec =
895  { SmallstepExec.es1 = cminor_exec; SmallstepExec.make_global =
896    (Obj.magic make_global); SmallstepExec.make_initial_state =
897    (Obj.magic make_initial_state) }
898
899(** val make_noinit_global : Cminor_syntax.cminor_noinit_program -> genv **)
900let make_noinit_global p =
901  Globalenvs.globalenv (fun x -> List.Cons ((AST.Init_space x), List.Nil)) p
902
903(** val make_initial_noinit_state :
904    Cminor_syntax.cminor_noinit_program -> state Errors.res **)
905let make_initial_noinit_state p =
906  let ge = make_noinit_global p in
907  Obj.magic
908    (Monad.m_bind0 (Monad.max_def Errors.res0)
909      (Obj.magic
910        (Globalenvs.init_mem (fun x -> List.Cons ((AST.Init_space x),
911          List.Nil)) p)) (fun m ->
912      Monad.m_bind0 (Monad.max_def Errors.res0)
913        (Obj.magic
914          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
915            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
916        Monad.m_bind0 (Monad.max_def Errors.res0)
917          (Obj.magic
918            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
919              (Globalenvs.find_funct_ptr ge b))) (fun f ->
920          Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m,
921            SStop)))))))
922
923(** val cminor_noinit_fullexec :
924    (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
925let cminor_noinit_fullexec =
926  { SmallstepExec.es1 = cminor_exec; SmallstepExec.make_global =
927    (Obj.magic make_noinit_global); SmallstepExec.make_initial_state =
928    (Obj.magic make_initial_noinit_state) }
929
Note: See TracBrowser for help on using the repository browser.