source: extracted/cminor_semantics.ml @ 2810

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

Cminor semantics exported.

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