source: extracted/cminor_semantics.ml @ 2746

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

...

File size: 35.9 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 Arithmetic
24
25open Extranat
26
27open Vector
28
29open FoldStuff
30
31open BitVector
32
33open Z
34
35open BitVectorZ
36
37open Pointers
38
39open ErrorMessages
40
41open Option
42
43open Setoids
44
45open Monad
46
47open Positive
48
49open PreIdentifiers
50
51open Errors
52
53open Div_and_mod
54
55open Jmeq
56
57open Russell
58
59open Util
60
61open Bool
62
63open Relations
64
65open Nat
66
67open List
68
69open Hints_declaration
70
71open Core_notation
72
73open Pts
74
75open Logic
76
77open Types
78
79open Coqlib
80
81open Values
82
83open Events
84
85open FrontEndVal
86
87open Hide
88
89open ByteValues
90
91open GenMem
92
93open FrontEndMem
94
95open IOMonad
96
97open IO
98
99open Extra_bool
100
101open Globalenvs
102
103open SmallstepExec
104
105open FrontEndOps
106
107open Cminor_syntax
108
109type env = Values.val0 Identifiers.identifier_map
110
111type genv = Cminor_syntax.internal_function AST.fundef Globalenvs.genv_t
112
113type cont =
114| Kend
115| Kseq of Cminor_syntax.stmt * cont
116| Kblock of cont
117
118(** val cont_rect_Type4 :
119    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
120    -> cont -> 'a1 **)
121let rec cont_rect_Type4 h_Kend h_Kseq h_Kblock = function
122| Kend -> h_Kend
123| Kseq (x_10, x_9) ->
124  h_Kseq x_10 x_9 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_9)
125| Kblock x_11 -> h_Kblock x_11 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_11)
126
127(** val cont_rect_Type3 :
128    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
129    -> cont -> 'a1 **)
130let rec cont_rect_Type3 h_Kend h_Kseq h_Kblock = function
131| Kend -> h_Kend
132| Kseq (x_24, x_23) ->
133  h_Kseq x_24 x_23 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_23)
134| Kblock x_25 -> h_Kblock x_25 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_25)
135
136(** val cont_rect_Type2 :
137    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
138    -> cont -> 'a1 **)
139let rec cont_rect_Type2 h_Kend h_Kseq h_Kblock = function
140| Kend -> h_Kend
141| Kseq (x_31, x_30) ->
142  h_Kseq x_31 x_30 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_30)
143| Kblock x_32 -> h_Kblock x_32 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_32)
144
145(** val cont_rect_Type1 :
146    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
147    -> cont -> 'a1 **)
148let rec cont_rect_Type1 h_Kend h_Kseq h_Kblock = function
149| Kend -> h_Kend
150| Kseq (x_38, x_37) ->
151  h_Kseq x_38 x_37 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_37)
152| Kblock x_39 -> h_Kblock x_39 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_39)
153
154(** val cont_rect_Type0 :
155    'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
156    -> cont -> 'a1 **)
157let rec cont_rect_Type0 h_Kend h_Kseq h_Kblock = function
158| Kend -> h_Kend
159| Kseq (x_45, x_44) ->
160  h_Kseq x_45 x_44 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_44)
161| Kblock x_46 -> h_Kblock x_46 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_46)
162
163(** val cont_inv_rect_Type4 :
164    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
165    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
166let cont_inv_rect_Type4 hterm h1 h2 h3 =
167  let hcut = cont_rect_Type4 h1 h2 h3 hterm in hcut __
168
169(** val cont_inv_rect_Type3 :
170    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
171    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
172let cont_inv_rect_Type3 hterm h1 h2 h3 =
173  let hcut = cont_rect_Type3 h1 h2 h3 hterm in hcut __
174
175(** val cont_inv_rect_Type2 :
176    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
177    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
178let cont_inv_rect_Type2 hterm h1 h2 h3 =
179  let hcut = cont_rect_Type2 h1 h2 h3 hterm in hcut __
180
181(** val cont_inv_rect_Type1 :
182    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
183    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
184let cont_inv_rect_Type1 hterm h1 h2 h3 =
185  let hcut = cont_rect_Type1 h1 h2 h3 hterm in hcut __
186
187(** val cont_inv_rect_Type0 :
188    cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
189    -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
190let cont_inv_rect_Type0 hterm h1 h2 h3 =
191  let hcut = cont_rect_Type0 h1 h2 h3 hterm in hcut __
192
193(** val cont_discr : cont -> cont -> __ **)
194let cont_discr x y =
195  Logic.eq_rect_Type2 x
196    (match x with
197     | Kend -> Obj.magic (fun _ dH -> dH)
198     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
199     | Kblock a0 -> Obj.magic (fun _ dH -> dH __)) y
200
201(** val cont_jmdiscr : cont -> cont -> __ **)
202let cont_jmdiscr x y =
203  Logic.eq_rect_Type2 x
204    (match x with
205     | Kend -> Obj.magic (fun _ dH -> dH)
206     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
207     | Kblock a0 -> Obj.magic (fun _ dH -> dH __)) y
208
209type cont_inv = __
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 state0 =
311| State of Cminor_syntax.internal_function * Cminor_syntax.stmt * env
312   * GenMem.mem1 * Pointers.block * cont * stack
313| Callstate of Cminor_syntax.internal_function AST.fundef
314   * Values.val0 List.list * GenMem.mem1 * stack
315| Returnstate of Values.val0 Types.option * GenMem.mem1 * stack
316| Finalstate of Integers.int
317
318(** val state_rect_Type4 :
319    (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
320    -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
321    (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list ->
322    GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1
323    -> stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> '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 (fd, args, m, st) -> h_Callstate 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.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
333    (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list ->
334    GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1
335    -> stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> '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 (fd, args, m, st) -> h_Callstate 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.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
345    (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list ->
346    GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1
347    -> stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> '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 (fd, args, m, st) -> h_Callstate 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.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
357    (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list ->
358    GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1
359    -> stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> '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 (fd, args, m, st) -> h_Callstate 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.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
369    (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list ->
370    GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1
371    -> stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> '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 (fd, args, m, st) -> h_Callstate 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.mem1 -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
381    (Cminor_syntax.internal_function AST.fundef -> Values.val0 List.list ->
382    GenMem.mem1 -> stack -> 'a1) -> (Values.val0 Types.option -> GenMem.mem1
383    -> stack -> 'a1) -> (Integers.int -> 'a1) -> state0 -> '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 (fd, args, m, st) -> h_Callstate 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    state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env
392    -> __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __
393    -> 'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0
394    List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0
395    Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __
396    -> '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    state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env
402    -> __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __
403    -> 'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0
404    List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0
405    Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __
406    -> '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    state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env
412    -> __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __
413    -> 'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0
414    List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0
415    Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __
416    -> '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    state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env
422    -> __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __
423    -> 'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0
424    List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0
425    Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __
426    -> '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    state0 -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env
432    -> __ -> __ -> GenMem.mem1 -> Pointers.block -> cont -> __ -> stack -> __
433    -> 'a1) -> (Cminor_syntax.internal_function AST.fundef -> Values.val0
434    List.list -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Values.val0
435    Types.option -> GenMem.mem1 -> stack -> __ -> 'a1) -> (Integers.int -> __
436    -> '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 : state0 -> state0 -> __ **)
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) -> Obj.magic (fun _ dH -> dH __ __ __ __)
447     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
448     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
449
450(** val eval_expr :
451    genv -> AST.typ -> Cminor_syntax.expr -> env -> Pointers.block ->
452    GenMem.mem1 -> (Events.trace, Values.val0) Types.prod Errors.res **)
453let rec eval_expr ge ty0 e1 en sp m =
454  (match e1 with
455   | Cminor_syntax.Id (x, i) ->
456     (fun _ ->
457       let r = Identifiers.lookup_present PreIdentifiers.SymbolTag en i in
458       Errors.OK { Types.fst = Events.e0; Types.snd = r })
459   | Cminor_syntax.Cst (x, c) ->
460     (fun _ ->
461       Obj.magic
462         (Monad.m_bind0 (Monad.max_def Errors.res0)
463           (Obj.magic
464             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedConstant)
465               (FrontEndOps.eval_constant x (Globalenvs.find_symbol ge) sp c)))
466           (fun r ->
467           Obj.magic (Errors.OK { Types.fst = Events.e0; Types.snd = r }))))
468   | Cminor_syntax.Op1 (ty, ty', op0, e') ->
469     (fun _ ->
470       Obj.magic
471         (Monad.m_bind2 (Monad.max_def Errors.res0)
472           (Obj.magic (eval_expr ge ty e' en sp m)) (fun tr v ->
473           Monad.m_bind0 (Monad.max_def Errors.res0)
474             (Obj.magic
475               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
476                 (FrontEndOps.eval_unop ty ty' op0 v))) (fun r ->
477             Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r })))))
478   | Cminor_syntax.Op2 (ty1, ty2, ty', op0, e2, e3) ->
479     (fun _ ->
480       Obj.magic
481         (Monad.m_bind2 (Monad.max_def Errors.res0)
482           (Obj.magic (eval_expr ge ty1 e2 en sp m)) (fun tr1 v1 ->
483           Monad.m_bind2 (Monad.max_def Errors.res0)
484             (Obj.magic (eval_expr ge ty2 e3 en sp m)) (fun tr2 v2 ->
485             Monad.m_bind0 (Monad.max_def Errors.res0)
486               (Obj.magic
487                 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
488                   (FrontEndOps.eval_binop m ty1 ty2 ty' op0 v1 v2)))
489               (fun r ->
490               Obj.magic (Errors.OK { Types.fst = (Events.eapp tr1 tr2);
491                 Types.snd = r }))))))
492   | Cminor_syntax.Mem (ty, e2) ->
493     (fun _ ->
494       Obj.magic
495         (Monad.m_bind2 (Monad.max_def Errors.res0)
496           (Obj.magic (eval_expr ge AST.ASTptr e2 en sp m)) (fun tr v ->
497           Monad.m_bind0 (Monad.max_def Errors.res0)
498             (Obj.magic
499               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
500                 (FrontEndMem.loadv ty m v))) (fun r ->
501             Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r })))))
502   | Cminor_syntax.Cond (sz, sg, ty, e', e2, e3) ->
503     (fun _ ->
504       Obj.magic
505         (Monad.m_bind2 (Monad.max_def Errors.res0)
506           (Obj.magic (eval_expr ge (AST.ASTint (sz, sg)) e' en sp m))
507           (fun tr v ->
508           Monad.m_bind0 (Monad.max_def Errors.res0)
509             (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
510             Monad.m_bind2 (Monad.max_def Errors.res0)
511               (Obj.magic
512                 (eval_expr ge ty
513                   (match b with
514                    | Bool.True -> e2
515                    | Bool.False -> e3) en sp m)) (fun tr' r ->
516               Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr');
517                 Types.snd = r }))))))
518   | Cminor_syntax.Ecost (ty, l, e') ->
519     (fun _ ->
520       Obj.magic
521         (Monad.m_bind2 (Monad.max_def Errors.res0)
522           (Obj.magic (eval_expr ge ty e' en sp m)) (fun tr r ->
523           Obj.magic (Errors.OK { Types.fst =
524             (Events.eapp (Events.echarge l) tr); Types.snd = r }))))) __
525
526(** val k_exit :
527    Nat.nat -> cont -> Cminor_syntax.internal_function -> env -> cont
528    Types.sig0 Errors.res **)
529let rec k_exit n k f en =
530  (match k with
531   | Kend -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadState))
532   | Kseq (x, k') -> (fun _ -> k_exit n k' f en)
533   | Kblock k' ->
534     (fun _ ->
535       match n with
536       | Nat.O -> Errors.OK k'
537       | Nat.S m -> k_exit m k' f en)) __
538
539(** val find_case :
540    AST.intsize -> AST.bvint -> (AST.bvint, 'a1) Types.prod List.list -> 'a1
541    -> 'a1 **)
542let rec find_case sz i cs default =
543  match cs with
544  | List.Nil -> default
545  | List.Cons (h, t) ->
546    let { Types.fst = hi; Types.snd = a } = h in
547    (match BitVector.eq_bv (AST.bitsize_of_intsize sz) i hi with
548     | Bool.True -> a
549     | Bool.False -> find_case sz i t default)
550
551(** val find_label :
552    PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
553    Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
554    Types.prod Types.sig0 Types.option **)
555let rec find_label l s k f en =
556  (match s with
557   | Cminor_syntax.St_skip -> (fun _ -> Types.None)
558   | Cminor_syntax.St_assign (x, x0, x1) -> (fun _ -> Types.None)
559   | Cminor_syntax.St_store (x, x0, x1) -> (fun _ -> Types.None)
560   | Cminor_syntax.St_call (x, x0, x1) -> (fun _ -> Types.None)
561   | Cminor_syntax.St_seq (s1, s2) ->
562     (fun _ ->
563       match find_label l s1 (Kseq (s2, k)) f en with
564       | Types.None -> find_label l s2 k f en
565       | Types.Some sk -> Types.Some sk)
566   | Cminor_syntax.St_ifthenelse (x, x0, x1, s1, s2) ->
567     (fun _ ->
568       match find_label l s1 k f en with
569       | Types.None -> find_label l s2 k f en
570       | Types.Some sk -> Types.Some sk)
571   | Cminor_syntax.St_return x -> (fun _ -> Types.None)
572   | Cminor_syntax.St_label (l', s') ->
573     (fun _ ->
574       match Identifiers.identifier_eq PreIdentifiers.Label l l' with
575       | Types.Inl _ -> Types.Some { Types.fst = s'; Types.snd = k }
576       | Types.Inr _ -> find_label l s' k f en)
577   | Cminor_syntax.St_goto x -> (fun _ -> Types.None)
578   | Cminor_syntax.St_cost (x, s') -> (fun _ -> find_label l s' k f en)) __
579
580(** val find_label_always :
581    PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
582    Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
583    Types.prod Types.sig0 **)
584let find_label_always l s k f en =
585  (match find_label l s k f en with
586   | Types.None -> (fun _ -> assert false (* absurd case *))
587   | Types.Some sk -> (fun _ -> sk)) __
588
589(** val bind_params :
590    Values.val0 List.list -> (AST.ident, AST.typ) Types.prod List.list -> env
591    Types.sig0 Errors.res **)
592let rec bind_params vs ids =
593  match vs with
594  | List.Nil ->
595    (match ids with
596     | List.Nil -> Errors.OK (Identifiers.empty_map PreIdentifiers.SymbolTag)
597     | List.Cons (x, x0) ->
598       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters))
599  | List.Cons (v, vt) ->
600    (match ids with
601     | List.Nil ->
602       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)
603     | List.Cons (idh, idt) ->
604       let { Types.fst = id; Types.snd = ty } = idh in
605       Obj.magic
606         (Monad.m_bind0 (Monad.max_def Errors.res0)
607           (Obj.magic (bind_params vt idt)) (fun en ->
608           Obj.magic (Errors.OK
609             (Identifiers.add PreIdentifiers.SymbolTag (Types.pi1 en)
610               idh.Types.fst v)))))
611
612(** val init_locals :
613    env -> (AST.ident, AST.typ) Types.prod List.list -> env **)
614let init_locals =
615  List.foldr (fun idty en ->
616    Identifiers.add PreIdentifiers.SymbolTag en idty.Types.fst Values.Vundef)
617
618(** val trace_map_inv :
619    ('a1 -> __ -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list
620    -> (Events.trace, 'a2 List.list) Types.prod Errors.res **)
621let rec trace_map_inv f l =
622  (match l with
623   | List.Nil ->
624     (fun _ -> Errors.OK { Types.fst = Events.e0; Types.snd = List.Nil })
625   | List.Cons (h, t) ->
626     (fun _ ->
627       Obj.magic
628         (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic f h __)
629           (fun tr h' ->
630           Monad.m_bind2 (Monad.max_def Errors.res0)
631             (Obj.magic (trace_map_inv f t)) (fun tr' t' ->
632             Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr');
633               Types.snd = (List.Cons (h', t')) })))))) __
634
635(** val eval_step :
636    genv -> state0 -> (IO.io_out, IO.io_in, (Events.trace, state0)
637    Types.prod) IOMonad.iO **)
638let eval_step ge = function
639| State (f, s, en, m, sp, k, st0) ->
640  IOMonad.err_to_io
641    ((match s with
642      | Cminor_syntax.St_skip ->
643        (fun _ ->
644          (match k with
645           | Kend ->
646             (fun _ ->
647               Obj.magic
648                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
649                   Events.e0; Types.snd = (Returnstate (Types.None,
650                   (GenMem.free m sp), st0)) }))
651           | Kseq (s', k') ->
652             (fun _ ->
653               Obj.magic
654                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
655                   Events.e0; Types.snd = (State (f, s', en, m, sp, k',
656                   st0)) }))
657           | Kblock k' ->
658             (fun _ ->
659               Obj.magic
660                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
661                   Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip,
662                   en, m, sp, k', st0)) }))) __)
663      | Cminor_syntax.St_assign (x, id, e1) ->
664        (fun _ ->
665          Obj.magic
666            (Monad.m_bind2 (Monad.max_def Errors.res0)
667              (Obj.magic (eval_expr ge x e1 en sp m)) (fun tr v ->
668              let en' =
669                Identifiers.update_present PreIdentifiers.SymbolTag en id v
670              in
671              Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
672                Types.snd = (State (f, Cminor_syntax.St_skip, en', m, sp, k,
673                st0)) })))
674      | Cminor_syntax.St_store (ty, edst, e1) ->
675        (fun _ ->
676          Obj.magic
677            (Monad.m_bind2 (Monad.max_def Errors.res0)
678              (Obj.magic (eval_expr ge AST.ASTptr edst en sp m))
679              (fun tr vdst ->
680              Monad.m_bind2 (Monad.max_def Errors.res0)
681                (Obj.magic (eval_expr ge ty e1 en sp m)) (fun tr' v ->
682                Monad.m_bind0 (Monad.max_def Errors.res0)
683                  (Obj.magic
684                    (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
685                      (FrontEndMem.storev ty m vdst v))) (fun m' ->
686                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
687                    (Events.eapp tr tr'); Types.snd = (State (f,
688                    Cminor_syntax.St_skip, en, m', sp, k, st0)) })))))
689      | Cminor_syntax.St_call (dst, ef, args) ->
690        (fun _ ->
691          Obj.magic
692            (Monad.m_bind2 (Monad.max_def Errors.res0)
693              (Obj.magic (eval_expr ge AST.ASTptr ef en sp m)) (fun tr vf ->
694              Monad.m_bind0 (Monad.max_def Errors.res0)
695                (Obj.magic
696                  (Errors.opt_to_res
697                    (Errors.msg ErrorMessages.BadFunctionValue)
698                    (Globalenvs.find_funct ge vf))) (fun fd ->
699                Monad.m_bind2 (Monad.max_def Errors.res0)
700                  (Obj.magic
701                    (trace_map_inv (fun e1 ->
702                      let { Types.dpi1 = ty; Types.dpi2 = e2 } = e1 in
703                      (fun _ -> eval_expr ge ty e2 en sp m)) args))
704                  (fun tr' vargs ->
705                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
706                    (Events.eapp tr tr'); Types.snd = (Callstate (fd, vargs,
707                    m, (Scall (dst, f, sp, en, k, st0)))) })))))
708      | Cminor_syntax.St_seq (s1, s2) ->
709        (fun _ ->
710          Obj.magic
711            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
712              Events.e0; Types.snd = (State (f, s1, en, m, sp, (Kseq (s2,
713              k)), st0)) }))
714      | Cminor_syntax.St_ifthenelse (x, x0, e1, strue, sfalse) ->
715        (fun _ ->
716          Obj.magic
717            (Monad.m_bind2 (Monad.max_def Errors.res0)
718              (Obj.magic (eval_expr ge (AST.ASTint (x, x0)) e1 en sp m))
719              (fun tr v ->
720              Monad.m_bind0 (Monad.max_def Errors.res0)
721                (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
722                Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
723                  Types.snd = (State (f,
724                  (match b with
725                   | Bool.True -> strue
726                   | Bool.False -> sfalse), en, m, sp, k, st0)) }))))
727      | Cminor_syntax.St_return eo ->
728        (match eo with
729         | Types.None ->
730           (fun _ ->
731             Obj.magic
732               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
733                 Events.e0; Types.snd = (Returnstate (Types.None,
734                 (GenMem.free m sp), st0)) }))
735         | Types.Some e1 ->
736           let { Types.dpi1 = ty; Types.dpi2 = e2 } = e1 in
737           (fun _ ->
738           Obj.magic
739             (Monad.m_bind2 (Monad.max_def Errors.res0)
740               (Obj.magic (eval_expr ge ty e2 en sp m)) (fun tr v ->
741               Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
742                 Types.snd = (Returnstate ((Types.Some v),
743                 (GenMem.free m sp), st0)) }))))
744      | Cminor_syntax.St_label (l, s') ->
745        (fun _ ->
746          Obj.magic
747            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
748              Events.e0; Types.snd = (State (f, s', en, m, sp, k, st0)) }))
749      | Cminor_syntax.St_goto l ->
750        (fun _ ->
751          let sk = find_label_always l f.Cminor_syntax.f_body Kend f en in
752          Obj.magic
753            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
754              Events.e0; Types.snd = (State (f, sk.Types.fst, en, m, sp,
755              sk.Types.snd, st0)) }))
756      | Cminor_syntax.St_cost (l, s') ->
757        (fun _ ->
758          Obj.magic
759            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
760              (Events.echarge l); Types.snd = (State (f, s', en, m, sp, k,
761              st0)) }))) __)
762| Callstate (fd, args, m, st0) ->
763  (match fd with
764   | AST.Internal f ->
765     IOMonad.err_to_io
766       (let { Types.fst = m'; Types.snd = sp } =
767          GenMem.alloc m (Z.z_of_nat Nat.O)
768            (Z.z_of_nat f.Cminor_syntax.f_stacksize)
769        in
770       Obj.magic
771         (Monad.m_bind0 (Monad.max_def Errors.res0)
772           (Obj.magic (bind_params args f.Cminor_syntax.f_params)) (fun en ->
773           Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
774             Events.e0; Types.snd = (State (f, f.Cminor_syntax.f_body,
775             (init_locals (Types.pi1 en) f.Cminor_syntax.f_vars), m', sp,
776             Kend, st0)) })))
777   | AST.External fn ->
778     Obj.magic
779       (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
780         (Obj.magic
781           (IOMonad.err_to_io
782             (IO.check_eventval_list args fn.AST.ef_sig.AST.sig_args)))
783         (fun evargs ->
784         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
785           (Obj.magic
786             (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
787           (fun evres ->
788           let res1 =
789             match fn.AST.ef_sig.AST.sig_res with
790             | Types.None -> Types.None
791             | Types.Some x ->
792               Types.Some (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)
793           in
794           Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
795             (Events.eextcall fn.AST.ef_id evargs
796               (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
797             Types.snd = (Returnstate (res1, m, st0)) }))))
798| Returnstate (result, m, st0) ->
799  IOMonad.err_to_io
800    (match st0 with
801     | SStop ->
802       (match result with
803        | Types.None ->
804          Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
805        | Types.Some v ->
806          (match v with
807           | Values.Vundef ->
808             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
809           | Values.Vint (sz, r) ->
810             (match sz with
811              | AST.I8 ->
812                (fun x -> Errors.Error
813                  (Errors.msg ErrorMessages.ReturnMismatch))
814              | AST.I16 ->
815                (fun x -> Errors.Error
816                  (Errors.msg ErrorMessages.ReturnMismatch))
817              | AST.I32 ->
818                (fun r5 ->
819                  Obj.magic
820                    (Monad.m_return0 (Monad.max_def Errors.res0)
821                      { Types.fst = Events.e0; Types.snd = (Finalstate r5) })))
822               r
823           | Values.Vnull ->
824             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
825           | Values.Vptr x ->
826             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)))
827     | Scall (dst, f, sp, en, k, st') ->
828       (match result with
829        | Types.None ->
830          (match dst with
831           | Types.None ->
832             Obj.magic
833               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
834                 Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip, en,
835                 m, sp, k, st')) })
836           | Types.Some x ->
837             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
838        | Types.Some v ->
839          (match dst with
840           | Types.None ->
841             (fun _ -> Errors.Error
842               (Errors.msg ErrorMessages.ReturnMismatch))
843           | Types.Some idty ->
844             (fun _ ->
845               Obj.magic
846                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
847                   Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip,
848                   (Identifiers.update_present PreIdentifiers.SymbolTag en
849                     idty.Types.fst v), m, sp, k, st')) }))) __))
850| Finalstate r ->
851  IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.BadState))
852
853(** val is_final0 : state0 -> Integers.int Types.option **)
854let is_final0 = function
855| State (x, x0, x1, x4, x5, x6, x8) -> Types.None
856| Callstate (x, x0, x1, x2) -> Types.None
857| Returnstate (x, x0, x1) -> Types.None
858| Finalstate r -> Types.Some r
859
860(** val cminor_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
861let cminor_exec =
862  { SmallstepExec.is_final = (fun x -> Obj.magic is_final0);
863    SmallstepExec.step = (Obj.magic eval_step) }
864
865(** val make_global0 : Cminor_syntax.cminor_program -> genv **)
866let make_global0 p =
867  Globalenvs.globalenv (fun x -> x) p
868
869(** val make_initial_state0 :
870    Cminor_syntax.cminor_program -> state0 Errors.res **)
871let make_initial_state0 p =
872  let ge = make_global0 p in
873  Obj.magic
874    (Monad.m_bind0 (Monad.max_def Errors.res0)
875      (Obj.magic (Globalenvs.init_mem (fun x -> x) p)) (fun m ->
876      Monad.m_bind0 (Monad.max_def Errors.res0)
877        (Obj.magic
878          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
879            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
880        Monad.m_bind0 (Monad.max_def Errors.res0)
881          (Obj.magic
882            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
883              (Globalenvs.find_funct_ptr ge b))) (fun f ->
884          Obj.magic (Errors.OK (Callstate (f, List.Nil, m, SStop)))))))
885
886(** val cminor_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
887let cminor_fullexec =
888  { SmallstepExec.es1 = cminor_exec; SmallstepExec.make_global =
889    (Obj.magic make_global0); SmallstepExec.make_initial_state =
890    (Obj.magic make_initial_state0) }
891
892(** val make_noinit_global : Cminor_syntax.cminor_noinit_program -> genv **)
893let make_noinit_global p =
894  Globalenvs.globalenv (fun x -> List.Cons ((AST.Init_space x), List.Nil)) p
895
896(** val make_initial_noinit_state :
897    Cminor_syntax.cminor_noinit_program -> state0 Errors.res **)
898let make_initial_noinit_state p =
899  let ge = make_noinit_global p in
900  Obj.magic
901    (Monad.m_bind0 (Monad.max_def Errors.res0)
902      (Obj.magic
903        (Globalenvs.init_mem (fun x -> List.Cons ((AST.Init_space x),
904          List.Nil)) p)) (fun m ->
905      Monad.m_bind0 (Monad.max_def Errors.res0)
906        (Obj.magic
907          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
908            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
909        Monad.m_bind0 (Monad.max_def Errors.res0)
910          (Obj.magic
911            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
912              (Globalenvs.find_funct_ptr ge b))) (fun f ->
913          Obj.magic (Errors.OK (Callstate (f, List.Nil, m, SStop)))))))
914
915(** val cminor_noinit_fullexec :
916    (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
917let cminor_noinit_fullexec =
918  { SmallstepExec.es1 = cminor_exec; SmallstepExec.make_global =
919    (Obj.magic make_noinit_global); SmallstepExec.make_initial_state =
920    (Obj.magic make_initial_noinit_state) }
921
Note: See TracBrowser for help on using the repository browser.