source: extracted/cexec.ml @ 2746

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

Exported again.

File size: 48.2 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Extralib
30
31open BitVectorTrie
32
33open CostLabel
34
35open PositiveMap
36
37open Deqsets
38
39open Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
53open Extranat
54
55open Vector
56
57open FoldStuff
58
59open BitVector
60
61open Z
62
63open BitVectorZ
64
65open Pointers
66
67open Coqlib
68
69open Values
70
71open Events
72
73open Proper
74
75open ErrorMessages
76
77open Option
78
79open Setoids
80
81open Monad
82
83open Positive
84
85open PreIdentifiers
86
87open Errors
88
89open IOMonad
90
91open IO
92
93open SmallstepExec
94
95open TypeComparison
96
97open ClassifyOp
98
99open Smallstep
100
101open Csyntax
102
103open Extra_bool
104
105open FrontEndVal
106
107open Hide
108
109open ByteValues
110
111open GenMem
112
113open FrontEndMem
114
115open Globalenvs
116
117open Csem
118
119(** val exec_bool_of_val :
120    Values.val0 -> Csyntax.type0 -> Bool.bool Errors.res **)
121let exec_bool_of_val v ty =
122  match v with
123  | Values.Vundef ->
124    Errors.Error (Errors.msg ErrorMessages.ValueIsNotABoolean)
125  | Values.Vint (sz, i) ->
126    (match ty with
127     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
128     | Csyntax.Tint (sz', x) ->
129       AST.intsize_eq_elim sz sz' i (fun i0 -> Errors.OK
130         (Bool.notb
131           (BitVector.eq_bv (AST.bitsize_of_intsize sz') i0
132             (BitVector.zero (AST.bitsize_of_intsize sz'))))) (Errors.Error
133         (Errors.msg ErrorMessages.TypeMismatch))
134     | Csyntax.Tpointer x ->
135       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
136     | Csyntax.Tarray (x, x0) ->
137       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
138     | Csyntax.Tfunction (x, x0) ->
139       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
140     | Csyntax.Tstruct (x, x0) ->
141       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
142     | Csyntax.Tunion (x, x0) ->
143       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
144     | Csyntax.Tcomp_ptr x ->
145       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
146  | Values.Vnull ->
147    (match ty with
148     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
149     | Csyntax.Tint (x, x0) ->
150       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
151     | Csyntax.Tpointer x -> Errors.OK Bool.False
152     | Csyntax.Tarray (x, x0) ->
153       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
154     | Csyntax.Tfunction (x, x0) ->
155       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
156     | Csyntax.Tstruct (x, x0) ->
157       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
158     | Csyntax.Tunion (x, x0) ->
159       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
160     | Csyntax.Tcomp_ptr x ->
161       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
162  | Values.Vptr x ->
163    (match ty with
164     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
165     | Csyntax.Tint (x0, x1) ->
166       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
167     | Csyntax.Tpointer x0 -> Errors.OK Bool.True
168     | Csyntax.Tarray (x0, x1) ->
169       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
170     | Csyntax.Tfunction (x0, x1) ->
171       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
172     | Csyntax.Tstruct (x0, x1) ->
173       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
174     | Csyntax.Tunion (x0, x1) ->
175       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
176     | Csyntax.Tcomp_ptr x0 ->
177       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
178
179(** val try_cast_null :
180    GenMem.mem1 -> AST.intsize -> BitVector.bitVector -> Csyntax.type0 ->
181    Csyntax.type0 -> Values.val0 Errors.res **)
182let try_cast_null m sz i ty ty' =
183  match BitVector.eq_bv (AST.bitsize_of_intsize sz) i
184          (BitVector.zero (AST.bitsize_of_intsize sz)) with
185  | Bool.True ->
186    (match ty with
187     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadCast)
188     | Csyntax.Tint (sz', x) ->
189       (match AST.eq_intsize sz sz' with
190        | Bool.True ->
191          (match ty' with
192           | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadCast)
193           | Csyntax.Tint (x0, x1) ->
194             Errors.Error (Errors.msg ErrorMessages.BadCast)
195           | Csyntax.Tpointer x0 -> Errors.OK Values.Vnull
196           | Csyntax.Tarray (x0, x1) -> Errors.OK Values.Vnull
197           | Csyntax.Tfunction (x0, x1) -> Errors.OK Values.Vnull
198           | Csyntax.Tstruct (x0, x1) ->
199             Errors.Error (Errors.msg ErrorMessages.BadCast)
200           | Csyntax.Tunion (x0, x1) ->
201             Errors.Error (Errors.msg ErrorMessages.BadCast)
202           | Csyntax.Tcomp_ptr x0 ->
203             Errors.Error (Errors.msg ErrorMessages.BadCast))
204        | Bool.False -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
205     | Csyntax.Tpointer x -> Errors.Error (Errors.msg ErrorMessages.BadCast)
206     | Csyntax.Tarray (x, x0) ->
207       Errors.Error (Errors.msg ErrorMessages.BadCast)
208     | Csyntax.Tfunction (x, x0) ->
209       Errors.Error (Errors.msg ErrorMessages.BadCast)
210     | Csyntax.Tstruct (x, x0) ->
211       Errors.Error (Errors.msg ErrorMessages.BadCast)
212     | Csyntax.Tunion (x, x0) ->
213       Errors.Error (Errors.msg ErrorMessages.BadCast)
214     | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg ErrorMessages.BadCast))
215  | Bool.False -> Errors.Error (Errors.msg ErrorMessages.BadCast)
216
217(** val ptr_like_type : Csyntax.type0 -> Bool.bool **)
218let ptr_like_type = function
219| Csyntax.Tvoid -> Bool.False
220| Csyntax.Tint (x, x0) -> Bool.False
221| Csyntax.Tpointer x -> Bool.True
222| Csyntax.Tarray (x, x0) -> Bool.True
223| Csyntax.Tfunction (x, x0) -> Bool.True
224| Csyntax.Tstruct (x, x0) -> Bool.False
225| Csyntax.Tunion (x, x0) -> Bool.False
226| Csyntax.Tcomp_ptr x -> Bool.False
227
228(** val exec_cast :
229    GenMem.mem1 -> Values.val0 -> Csyntax.type0 -> Csyntax.type0 ->
230    Values.val0 Errors.res **)
231let exec_cast m v ty ty' =
232  match v with
233  | Values.Vundef -> Errors.Error (Errors.msg ErrorMessages.BadCast)
234  | Values.Vint (sz, i) ->
235    (match ty with
236     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
237     | Csyntax.Tint (sz1, si1) ->
238       AST.intsize_eq_elim sz sz1 i (fun i0 ->
239         match ty' with
240         | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadCast)
241         | Csyntax.Tint (sz2, si2) ->
242           Errors.OK (Values.Vint (sz2, (Csem.cast_int_int sz1 si1 sz2 i0)))
243         | Csyntax.Tpointer x ->
244           Obj.magic
245             (Monad.m_bind0 (Monad.max_def Errors.res0)
246               (Obj.magic (try_cast_null m sz1 i0 ty ty')) (fun r ->
247               Obj.magic (Errors.OK r)))
248         | Csyntax.Tarray (x, x0) ->
249           Obj.magic
250             (Monad.m_bind0 (Monad.max_def Errors.res0)
251               (Obj.magic (try_cast_null m sz1 i0 ty ty')) (fun r ->
252               Obj.magic (Errors.OK r)))
253         | Csyntax.Tfunction (x, x0) ->
254           Obj.magic
255             (Monad.m_bind0 (Monad.max_def Errors.res0)
256               (Obj.magic (try_cast_null m sz1 i0 ty ty')) (fun r ->
257               Obj.magic (Errors.OK r)))
258         | Csyntax.Tstruct (x, x0) ->
259           Errors.Error (Errors.msg ErrorMessages.BadCast)
260         | Csyntax.Tunion (x, x0) ->
261           Errors.Error (Errors.msg ErrorMessages.BadCast)
262         | Csyntax.Tcomp_ptr x ->
263           Errors.Error (Errors.msg ErrorMessages.BadCast)) (Errors.Error
264         (Errors.msg ErrorMessages.BadCast))
265     | Csyntax.Tpointer x ->
266       Obj.magic
267         (Monad.m_bind0 (Monad.max_def Errors.res0)
268           (Obj.magic (try_cast_null m sz i ty ty')) (fun r ->
269           Obj.magic (Errors.OK r)))
270     | Csyntax.Tarray (x, x0) ->
271       Obj.magic
272         (Monad.m_bind0 (Monad.max_def Errors.res0)
273           (Obj.magic (try_cast_null m sz i ty ty')) (fun r ->
274           Obj.magic (Errors.OK r)))
275     | Csyntax.Tfunction (x, x0) ->
276       Obj.magic
277         (Monad.m_bind0 (Monad.max_def Errors.res0)
278           (Obj.magic (try_cast_null m sz i ty ty')) (fun r ->
279           Obj.magic (Errors.OK r)))
280     | Csyntax.Tstruct (x, x0) ->
281       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
282     | Csyntax.Tunion (x, x0) ->
283       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
284     | Csyntax.Tcomp_ptr x ->
285       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
286  | Values.Vnull ->
287    (match Bool.andb (ptr_like_type ty) (ptr_like_type ty') with
288     | Bool.True -> Errors.OK Values.Vnull
289     | Bool.False -> Errors.Error (Errors.msg ErrorMessages.BadCast))
290  | Values.Vptr ptr ->
291    (match Bool.andb (ptr_like_type ty) (ptr_like_type ty') with
292     | Bool.True -> Errors.OK (Values.Vptr ptr)
293     | Bool.False -> Errors.Error (Errors.msg ErrorMessages.BadCast))
294
295(** val load_value_of_type' :
296    Csyntax.type0 -> GenMem.mem1 -> (Pointers.block, Pointers.offset)
297    Types.prod -> Values.val0 Types.option **)
298let load_value_of_type' ty m l =
299  let { Types.fst = loc; Types.snd = ofs } = l in
300  Csem.load_value_of_type ty m loc ofs
301
302(** val exec_expr :
303    Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr -> (Values.val0,
304    Events.trace) Types.prod Errors.res **)
305let rec exec_expr ge0 en m = function
306| Csyntax.Expr (e', ty) ->
307  (match e' with
308   | Csyntax.Econst_int (sz, i) ->
309     (match ty with
310      | Csyntax.Tvoid ->
311        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
312      | Csyntax.Tint (sz', x) ->
313        (match AST.eq_intsize sz sz' with
314         | Bool.True ->
315           Errors.OK { Types.fst = (Values.Vint (sz, i)); Types.snd =
316             Events.e0 }
317         | Bool.False ->
318           Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
319      | Csyntax.Tpointer x ->
320        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
321      | Csyntax.Tarray (x, x0) ->
322        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
323      | Csyntax.Tfunction (x, x0) ->
324        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
325      | Csyntax.Tstruct (x, x0) ->
326        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
327      | Csyntax.Tunion (x, x0) ->
328        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
329      | Csyntax.Tcomp_ptr x ->
330        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
331   | Csyntax.Evar x ->
332     Obj.magic
333       (Monad.m_bind2 (Monad.max_def Errors.res0)
334         (Obj.magic (exec_lvalue' ge0 en m e' ty)) (fun l tr ->
335         Monad.m_bind0 (Monad.max_def Errors.res0)
336           (Obj.magic
337             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
338               (load_value_of_type' ty m l))) (fun v ->
339           Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
340   | Csyntax.Ederef x ->
341     Obj.magic
342       (Monad.m_bind2 (Monad.max_def Errors.res0)
343         (Obj.magic (exec_lvalue' ge0 en m e' ty)) (fun l tr ->
344         Monad.m_bind0 (Monad.max_def Errors.res0)
345           (Obj.magic
346             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
347               (load_value_of_type' ty m l))) (fun v ->
348           Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
349   | Csyntax.Eaddrof a ->
350     Obj.magic
351       (Monad.m_bind2 (Monad.max_def Errors.res0)
352         (Obj.magic (exec_lvalue ge0 en m a)) (fun lo tr ->
353         match ty with
354         | Csyntax.Tvoid ->
355           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
356         | Csyntax.Tint (x, x0) ->
357           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
358         | Csyntax.Tpointer x ->
359           let { Types.fst = loc; Types.snd = ofs } = lo in
360           Obj.magic (Errors.OK { Types.fst = (Values.Vptr
361             { Pointers.pblock = loc; Pointers.poff = ofs }); Types.snd =
362             tr })
363         | Csyntax.Tarray (x, x0) ->
364           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
365         | Csyntax.Tfunction (x, x0) ->
366           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
367         | Csyntax.Tstruct (x, x0) ->
368           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
369         | Csyntax.Tunion (x, x0) ->
370           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
371         | Csyntax.Tcomp_ptr x ->
372           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))))
373   | Csyntax.Eunop (op0, a) ->
374     Obj.magic
375       (Monad.m_bind2 (Monad.max_def Errors.res0)
376         (Obj.magic (exec_expr ge0 en m a)) (fun v1 tr ->
377         Monad.m_bind0 (Monad.max_def Errors.res0)
378           (Obj.magic
379             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
380               (Csem.sem_unary_operation op0 v1 (Csyntax.typeof a))))
381           (fun v -> Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
382   | Csyntax.Ebinop (op0, a1, a2) ->
383     Obj.magic
384       (Monad.m_bind2 (Monad.max_def Errors.res0)
385         (Obj.magic (exec_expr ge0 en m a1)) (fun v1 tr1 ->
386         Monad.m_bind2 (Monad.max_def Errors.res0)
387           (Obj.magic (exec_expr ge0 en m a2)) (fun v2 tr2 ->
388           Monad.m_bind0 (Monad.max_def Errors.res0)
389             (Obj.magic
390               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
391                 (Csem.sem_binary_operation op0 v1 (Csyntax.typeof a1) v2
392                   (Csyntax.typeof a2) m ty))) (fun v ->
393             Obj.magic (Errors.OK { Types.fst = v; Types.snd =
394               (Events.eapp tr1 tr2) })))))
395   | Csyntax.Ecast (ty', a) ->
396     Obj.magic
397       (Monad.m_bind2 (Monad.max_def Errors.res0)
398         (Obj.magic (exec_expr ge0 en m a)) (fun v tr ->
399         Monad.m_bind0 (Monad.max_def Errors.res0)
400           (Obj.magic (exec_cast m v (Csyntax.typeof a) ty')) (fun v' ->
401           Obj.magic (Errors.OK { Types.fst = v'; Types.snd = tr }))))
402   | Csyntax.Econdition (a1, a2, a3) ->
403     Obj.magic
404       (Monad.m_bind2 (Monad.max_def Errors.res0)
405         (Obj.magic (exec_expr ge0 en m a1)) (fun v tr1 ->
406         Monad.m_bind0 (Monad.max_def Errors.res0)
407           (Obj.magic (exec_bool_of_val v (Csyntax.typeof a1))) (fun b ->
408           Monad.m_bind2 (Monad.max_def Errors.res0)
409             (match b with
410              | Bool.True -> Obj.magic (exec_expr ge0 en m a2)
411              | Bool.False -> Obj.magic (exec_expr ge0 en m a3))
412             (fun v' tr2 ->
413             Obj.magic (Errors.OK { Types.fst = v'; Types.snd =
414               (Events.eapp tr1 tr2) })))))
415   | Csyntax.Eandbool (a1, a2) ->
416     Obj.magic
417       (Monad.m_bind2 (Monad.max_def Errors.res0)
418         (Obj.magic (exec_expr ge0 en m a1)) (fun v1 tr1 ->
419         Monad.m_bind0 (Monad.max_def Errors.res0)
420           (Obj.magic (exec_bool_of_val v1 (Csyntax.typeof a1))) (fun b1 ->
421           match b1 with
422           | Bool.True ->
423             Monad.m_bind2 (Monad.max_def Errors.res0)
424               (Obj.magic (exec_expr ge0 en m a2)) (fun v2 tr2 ->
425               Monad.m_bind0 (Monad.max_def Errors.res0)
426                 (Obj.magic (exec_bool_of_val v2 (Csyntax.typeof a2)))
427                 (fun b2 ->
428                 match Csem.cast_bool_to_target ty (Types.Some
429                         (Values.of_bool b2)) with
430                 | Types.None ->
431                   Obj.magic (Errors.Error
432                     (Errors.msg ErrorMessages.BadlyTypedTerm))
433                 | Types.Some v20 ->
434                   Obj.magic (Errors.OK { Types.fst = v20; Types.snd =
435                     (Events.eapp tr1 tr2) })))
436           | Bool.False ->
437             (match Csem.cast_bool_to_target ty (Types.Some Values.vfalse) with
438              | Types.None ->
439                Obj.magic (Errors.Error
440                  (Errors.msg ErrorMessages.BadlyTypedTerm))
441              | Types.Some vfls ->
442                Obj.magic (Errors.OK { Types.fst = vfls; Types.snd = tr1 })))))
443   | Csyntax.Eorbool (a1, a2) ->
444     Obj.magic
445       (Monad.m_bind2 (Monad.max_def Errors.res0)
446         (Obj.magic (exec_expr ge0 en m a1)) (fun v1 tr1 ->
447         Monad.m_bind0 (Monad.max_def Errors.res0)
448           (Obj.magic (exec_bool_of_val v1 (Csyntax.typeof a1))) (fun b1 ->
449           match b1 with
450           | Bool.True ->
451             (match Csem.cast_bool_to_target ty (Types.Some Values.vtrue) with
452              | Types.None ->
453                Obj.magic (Errors.Error
454                  (Errors.msg ErrorMessages.BadlyTypedTerm))
455              | Types.Some vtr ->
456                Obj.magic (Errors.OK { Types.fst = vtr; Types.snd = tr1 }))
457           | Bool.False ->
458             Monad.m_bind2 (Monad.max_def Errors.res0)
459               (Obj.magic (exec_expr ge0 en m a2)) (fun v2 tr2 ->
460               Monad.m_bind0 (Monad.max_def Errors.res0)
461                 (Obj.magic (exec_bool_of_val v2 (Csyntax.typeof a2)))
462                 (fun b2 ->
463                 match Csem.cast_bool_to_target ty (Types.Some
464                         (Values.of_bool b2)) with
465                 | Types.None ->
466                   Obj.magic (Errors.Error
467                     (Errors.msg ErrorMessages.BadlyTypedTerm))
468                 | Types.Some v20 ->
469                   Obj.magic (Errors.OK { Types.fst = v20; Types.snd =
470                     (Events.eapp tr1 tr2) }))))))
471   | Csyntax.Esizeof ty' ->
472     (match ty with
473      | Csyntax.Tvoid ->
474        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
475      | Csyntax.Tint (sz, x) ->
476        Errors.OK { Types.fst = (Values.Vint (sz,
477          (AST.repr0 sz (Csyntax.sizeof ty')))); Types.snd = Events.e0 }
478      | Csyntax.Tpointer x ->
479        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
480      | Csyntax.Tarray (x, x0) ->
481        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
482      | Csyntax.Tfunction (x, x0) ->
483        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
484      | Csyntax.Tstruct (x, x0) ->
485        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
486      | Csyntax.Tunion (x, x0) ->
487        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
488      | Csyntax.Tcomp_ptr x ->
489        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
490   | Csyntax.Efield (x, x0) ->
491     Obj.magic
492       (Monad.m_bind2 (Monad.max_def Errors.res0)
493         (Obj.magic (exec_lvalue' ge0 en m e' ty)) (fun l tr ->
494         Monad.m_bind0 (Monad.max_def Errors.res0)
495           (Obj.magic
496             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
497               (load_value_of_type' ty m l))) (fun v ->
498           Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
499   | Csyntax.Ecost (l, a) ->
500     Obj.magic
501       (Monad.m_bind2 (Monad.max_def Errors.res0)
502         (Obj.magic (exec_expr ge0 en m a)) (fun v tr ->
503         Obj.magic (Errors.OK { Types.fst = v; Types.snd =
504           (Events.eapp (Events.echarge l) tr) }))))
505(** val exec_lvalue' :
506    Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr_descr ->
507    Csyntax.type0 -> ((Pointers.block, Pointers.offset) Types.prod,
508    Events.trace) Types.prod Errors.res **)
509and exec_lvalue' ge0 en m e' ty =
510  match e' with
511  | Csyntax.Econst_int (x, x0) ->
512    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
513  | Csyntax.Evar id ->
514    (match Identifiers.lookup0 PreIdentifiers.SymbolTag en id with
515     | Types.None ->
516       Obj.magic
517         (Monad.m_bind0 (Monad.max_def Errors.res0)
518           (Obj.magic
519             (Errors.opt_to_res (List.Cons ((Errors.MSG
520               ErrorMessages.UnknownIdentifier), (List.Cons ((Errors.CTX
521               (PreIdentifiers.SymbolTag, id)), List.Nil))))
522               (Globalenvs.find_symbol ge0 id))) (fun l ->
523           Obj.magic (Errors.OK { Types.fst = { Types.fst = l; Types.snd =
524             Pointers.zero_offset }; Types.snd = Events.e0 })))
525     | Types.Some loc ->
526       Errors.OK { Types.fst = { Types.fst = loc; Types.snd =
527         Pointers.zero_offset }; Types.snd = Events.e0 })
528  | Csyntax.Ederef a ->
529    Obj.magic
530      (Monad.m_bind2 (Monad.max_def Errors.res0)
531        (Obj.magic (exec_expr ge0 en m a)) (fun v tr ->
532        match v with
533        | Values.Vundef ->
534          Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
535        | Values.Vint (x, x0) ->
536          Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
537        | Values.Vnull ->
538          Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
539        | Values.Vptr ptr ->
540          Obj.magic (Errors.OK { Types.fst = { Types.fst =
541            ptr.Pointers.pblock; Types.snd = ptr.Pointers.poff }; Types.snd =
542            tr })))
543  | Csyntax.Eaddrof x ->
544    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
545  | Csyntax.Eunop (x, x0) ->
546    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
547  | Csyntax.Ebinop (x, x0, x1) ->
548    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
549  | Csyntax.Ecast (x, x0) ->
550    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
551  | Csyntax.Econdition (x, x0, x1) ->
552    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
553  | Csyntax.Eandbool (x, x0) ->
554    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
555  | Csyntax.Eorbool (x, x0) ->
556    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
557  | Csyntax.Esizeof x ->
558    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
559  | Csyntax.Efield (a, i) ->
560    (match Csyntax.typeof a with
561     | Csyntax.Tvoid ->
562       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
563     | Csyntax.Tint (x, x0) ->
564       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
565     | Csyntax.Tpointer x ->
566       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
567     | Csyntax.Tarray (x, x0) ->
568       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
569     | Csyntax.Tfunction (x, x0) ->
570       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
571     | Csyntax.Tstruct (id, fList) ->
572       Obj.magic
573         (Monad.m_bind2 (Monad.max_def Errors.res0)
574           (Obj.magic (exec_lvalue ge0 en m a)) (fun lofs tr ->
575           Monad.m_bind0 (Monad.max_def Errors.res0)
576             (Obj.magic (Csyntax.field_offset i fList)) (fun delta ->
577             Obj.magic (Errors.OK { Types.fst = { Types.fst = lofs.Types.fst;
578               Types.snd =
579               (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
580                 lofs.Types.snd (AST.repr0 AST.I16 delta)) }; Types.snd =
581               tr }))))
582     | Csyntax.Tunion (id, fList) ->
583       Obj.magic
584         (Monad.m_bind2 (Monad.max_def Errors.res0)
585           (Obj.magic (exec_lvalue ge0 en m a)) (fun lofs tr ->
586           Obj.magic (Errors.OK { Types.fst = lofs; Types.snd = tr })))
587     | Csyntax.Tcomp_ptr x ->
588       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
589  | Csyntax.Ecost (x, x0) ->
590    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
591(** val exec_lvalue :
592    Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr ->
593    ((Pointers.block, Pointers.offset) Types.prod, Events.trace) Types.prod
594    Errors.res **)
595and exec_lvalue ge0 en m = function
596| Csyntax.Expr (e', ty) -> exec_lvalue' ge0 en m e' ty
597
598(** val exec_exprlist :
599    Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr List.list ->
600    (Values.val0 List.list, Events.trace) Types.prod Errors.res **)
601let rec exec_exprlist ge0 e1 m = function
602| List.Nil -> Errors.OK { Types.fst = List.Nil; Types.snd = Events.e0 }
603| List.Cons (e2, es) ->
604  Obj.magic
605    (Monad.m_bind2 (Monad.max_def Errors.res0)
606      (Obj.magic (exec_expr ge0 e1 m e2)) (fun v tr1 ->
607      Monad.m_bind2 (Monad.max_def Errors.res0)
608        (Obj.magic (exec_exprlist ge0 e1 m es)) (fun vs tr2 ->
609        Obj.magic (Errors.OK { Types.fst = (List.Cons (v, vs)); Types.snd =
610          (Events.eapp tr1 tr2) }))))
611
612(** val exec_alloc_variables :
613    Csem.env -> GenMem.mem1 -> (AST.ident, Csyntax.type0) Types.prod
614    List.list -> (Csem.env, GenMem.mem1) Types.prod **)
615let rec exec_alloc_variables en m = function
616| List.Nil -> { Types.fst = en; Types.snd = m }
617| List.Cons (h, vars) ->
618  let { Types.fst = id; Types.snd = ty } = h in
619  let { Types.fst = m1; Types.snd = b1 } =
620    GenMem.alloc m (Z.z_of_nat Nat.O) (Z.z_of_nat (Csyntax.sizeof ty))
621  in
622  exec_alloc_variables (Identifiers.add PreIdentifiers.SymbolTag en id b1) m1
623    vars
624
625(** val exec_bind_parameters :
626    Csem.env -> GenMem.mem1 -> (AST.ident, Csyntax.type0) Types.prod
627    List.list -> Values.val0 List.list -> GenMem.mem1 Errors.res **)
628let rec exec_bind_parameters e1 m params vs =
629  match params with
630  | List.Nil ->
631    (match vs with
632     | List.Nil -> Errors.OK m
633     | List.Cons (x, x0) ->
634       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters))
635  | List.Cons (idty, params') ->
636    let { Types.fst = id; Types.snd = ty } = idty in
637    (match vs with
638     | List.Nil ->
639       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)
640     | List.Cons (v1, vl) ->
641       Obj.magic
642         (Monad.m_bind0 (Monad.max_def Errors.res0)
643           (Obj.magic
644             (Errors.opt_to_res (List.Cons ((Errors.MSG
645               ErrorMessages.UnknownIdentifier), (List.Cons ((Errors.CTX
646               (PreIdentifiers.SymbolTag, id)), List.Nil))))
647               (Identifiers.lookup0 PreIdentifiers.SymbolTag e1 id)))
648           (fun b ->
649           Monad.m_bind0 (Monad.max_def Errors.res0)
650             (Obj.magic
651               (Errors.opt_to_res (List.Cons ((Errors.MSG
652                 ErrorMessages.FailedStore), (List.Cons ((Errors.CTX
653                 (PreIdentifiers.SymbolTag, id)), List.Nil))))
654                 (Csem.store_value_of_type ty m b Pointers.zero_offset v1)))
655             (fun m1 -> Obj.magic (exec_bind_parameters e1 m1 params' vl)))))
656
657(** val is_is_call_cont : Csem.cont -> (__, __) Types.sum **)
658let rec is_is_call_cont = function
659| Csem.Kstop -> Types.Inl __
660| Csem.Kseq (x, x0) -> Types.Inr __
661| Csem.Kwhile (x, x0, x1) -> Types.Inr __
662| Csem.Kdowhile (x, x0, x1) -> Types.Inr __
663| Csem.Kfor2 (x, x0, x1, x2) -> Types.Inr __
664| Csem.Kfor3 (x, x0, x1, x2) -> Types.Inr __
665| Csem.Kswitch x -> Types.Inr __
666| Csem.Kcall (x, x0, x1, x2) -> Types.Inl __
667
668(** val is_Sskip : Csyntax.statement -> (__, __) Types.sum **)
669let is_Sskip = function
670| Csyntax.Sskip -> Types.Inl __
671| Csyntax.Sassign (x, x0) -> Types.Inr __
672| Csyntax.Scall (x, x0, x1) -> Types.Inr __
673| Csyntax.Ssequence (x, x0) -> Types.Inr __
674| Csyntax.Sifthenelse (x, x0, x1) -> Types.Inr __
675| Csyntax.Swhile (x, x0) -> Types.Inr __
676| Csyntax.Sdowhile (x, x0) -> Types.Inr __
677| Csyntax.Sfor (x, x0, x1, x2) -> Types.Inr __
678| Csyntax.Sbreak -> Types.Inr __
679| Csyntax.Scontinue -> Types.Inr __
680| Csyntax.Sreturn x -> Types.Inr __
681| Csyntax.Sswitch (x, x0) -> Types.Inr __
682| Csyntax.Slabel (x, x0) -> Types.Inr __
683| Csyntax.Sgoto x -> Types.Inr __
684| Csyntax.Scost (x, x0) -> Types.Inr __
685
686(** val store_value_of_type' :
687    Csyntax.type0 -> GenMem.mem1 -> (Pointers.block, Pointers.offset)
688    Types.prod -> Values.val0 -> GenMem.mem1 Types.option **)
689let store_value_of_type' ty m l v =
690  let { Types.fst = loc; Types.snd = ofs } = l in
691  Csem.store_value_of_type ty m loc ofs v
692
693(** val exec_step :
694    Csem.genv0 -> Csem.state0 -> (IO.io_out, IO.io_in, (Events.trace,
695    Csem.state0) Types.prod) IOMonad.iO **)
696let rec exec_step ge0 = function
697| Csem.State (f, s, k, e1, m) ->
698  (match s with
699   | Csyntax.Sskip ->
700     (match k with
701      | Csem.Kstop ->
702        (match f.Csyntax.fn_return with
703         | Csyntax.Tvoid ->
704           IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Returnstate
705             (Values.Vundef, k,
706             (GenMem.free_list m (Csem.blocks_of_env e1)))) }
707         | Csyntax.Tint (x, x0) ->
708           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
709         | Csyntax.Tpointer x ->
710           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
711         | Csyntax.Tarray (x, x0) ->
712           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
713         | Csyntax.Tfunction (x, x0) ->
714           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
715         | Csyntax.Tstruct (x, x0) ->
716           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
717         | Csyntax.Tunion (x, x0) ->
718           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
719         | Csyntax.Tcomp_ptr x ->
720           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState))
721      | Csem.Kseq (s0, k') ->
722        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s0, k',
723          e1, m)) }
724      | Csem.Kwhile (a, s', k') ->
725        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
726          (Csyntax.Swhile (a, s')), k', e1, m)) }
727      | Csem.Kdowhile (a, s', k') ->
728        Obj.magic
729          (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
730            (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in Obj.magic x)
731            (fun v tr ->
732            Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
733              (Obj.magic
734                (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a))))
735              (fun b ->
736              match b with
737              | Bool.True ->
738                Obj.magic
739                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
740                    (Csyntax.Sdowhile (a, s')), k', e1, m)) })
741              | Bool.False ->
742                Obj.magic
743                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
744                    Csyntax.Sskip, k', e1, m)) }))))
745      | Csem.Kfor2 (a2, a3, s', k') ->
746        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, a3,
747          (Csem.Kfor3 (a2, a3, s', k')), e1, m)) }
748      | Csem.Kfor3 (a2, a3, s', k') ->
749        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
750          (Csyntax.Sfor (Csyntax.Sskip, a2, a3, s')), k', e1, m)) }
751      | Csem.Kswitch k' ->
752        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
753          Csyntax.Sskip, k', e1, m)) }
754      | Csem.Kcall (x, x0, x1, x2) ->
755        (match f.Csyntax.fn_return with
756         | Csyntax.Tvoid ->
757           IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Returnstate
758             (Values.Vundef, k,
759             (GenMem.free_list m (Csem.blocks_of_env e1)))) }
760         | Csyntax.Tint (x3, x4) ->
761           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
762         | Csyntax.Tpointer x3 ->
763           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
764         | Csyntax.Tarray (x3, x4) ->
765           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
766         | Csyntax.Tfunction (x3, x4) ->
767           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
768         | Csyntax.Tstruct (x3, x4) ->
769           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
770         | Csyntax.Tunion (x3, x4) ->
771           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
772         | Csyntax.Tcomp_ptr x3 ->
773           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)))
774   | Csyntax.Sassign (a1, a2) ->
775     Obj.magic
776       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
777         (let x = IOMonad.err_to_io (exec_lvalue ge0 e1 m a1) in Obj.magic x)
778         (fun l tr1 ->
779         Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
780           (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a2) in Obj.magic x)
781           (fun v2 tr2 ->
782           Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
783             (Obj.magic
784               (IOMonad.opt_to_io (Errors.msg ErrorMessages.FailedStore)
785                 (store_value_of_type' (Csyntax.typeof a1) m l v2)))
786             (fun m' ->
787             Obj.magic
788               (IO.ret { Types.fst = (Events.eapp tr1 tr2); Types.snd =
789                 (Csem.State (f, Csyntax.Sskip, k, e1, m')) })))))
790   | Csyntax.Scall (lhs, a, al) ->
791     Obj.magic
792       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
793         (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in Obj.magic x)
794         (fun vf tr2 ->
795         Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
796           (let x = IOMonad.err_to_io (exec_exprlist ge0 e1 m al) in
797           Obj.magic x) (fun vargs tr3 ->
798           Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
799             (Obj.magic
800               (IOMonad.opt_to_io (Errors.msg ErrorMessages.BadFunctionValue)
801                 (Globalenvs.find_funct_id ge0 vf))) (fun fd id ->
802             Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
803               (Obj.magic
804                 (IOMonad.err_to_io
805                   (TypeComparison.assert_type_eq (Csyntax.type_of_fundef fd)
806                     (Csem.fun_typeof a)))) (fun _ ->
807               match lhs with
808               | Types.None ->
809                 Obj.magic
810                   (IO.ret { Types.fst = (Events.eapp tr2 tr3); Types.snd =
811                     (Csem.Callstate (id, fd, vargs, (Csem.Kcall (Types.None,
812                     f, e1, k)), m)) })
813               | Types.Some lhs' ->
814                 Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
815                   (let x = IOMonad.err_to_io (exec_lvalue ge0 e1 m lhs') in
816                   Obj.magic x) (fun locofs tr1 ->
817                   Obj.magic
818                     (IO.ret { Types.fst =
819                       (Events.eapp tr1 (Events.eapp tr2 tr3)); Types.snd =
820                       (Csem.Callstate (id, fd, vargs, (Csem.Kcall
821                       ((Types.Some { Types.fst = locofs; Types.snd =
822                       (Csyntax.typeof lhs') }), f, e1, k)), m)) })))))))
823   | Csyntax.Ssequence (s1, s2) ->
824     IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s1,
825       (Csem.Kseq (s2, k)), e1, m)) }
826   | Csyntax.Sifthenelse (a, s1, s2) ->
827     Obj.magic
828       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
829         (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in Obj.magic x)
830         (fun v tr ->
831         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
832           (Obj.magic
833             (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a))))
834           (fun b ->
835           Obj.magic
836             (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
837               (match b with
838                | Bool.True -> s1
839                | Bool.False -> s2), k, e1, m)) }))))
840   | Csyntax.Swhile (a, s') ->
841     Obj.magic
842       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
843         (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in Obj.magic x)
844         (fun v tr ->
845         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
846           (Obj.magic
847             (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a))))
848           (fun b ->
849           Obj.magic
850             (IO.ret { Types.fst = tr; Types.snd =
851               (match b with
852                | Bool.True ->
853                  Csem.State (f, s', (Csem.Kwhile (a, s', k)), e1, m)
854                | Bool.False -> Csem.State (f, Csyntax.Sskip, k, e1, m)) }))))
855   | Csyntax.Sdowhile (a, s') ->
856     IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s',
857       (Csem.Kdowhile (a, s', k)), e1, m)) }
858   | Csyntax.Sfor (a1, a2, a3, s') ->
859     (match is_Sskip a1 with
860      | Types.Inl _ ->
861        Obj.magic
862          (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
863            (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a2) in
864            Obj.magic x) (fun v tr ->
865            Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
866              (Obj.magic
867                (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a2))))
868              (fun b ->
869              Obj.magic
870                (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
871                  (match b with
872                   | Bool.True -> s'
873                   | Bool.False -> Csyntax.Sskip),
874                  (match b with
875                   | Bool.True -> Csem.Kfor2 (a2, a3, s', k)
876                   | Bool.False -> k), e1, m)) }))))
877      | Types.Inr _ ->
878        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, a1,
879          (Csem.Kseq ((Csyntax.Sfor (Csyntax.Sskip, a2, a3, s')), k)), e1,
880          m)) })
881   | Csyntax.Sbreak ->
882     (match k with
883      | Csem.Kstop -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
884      | Csem.Kseq (s', k') ->
885        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
886          Csyntax.Sbreak, k', e1, m)) }
887      | Csem.Kwhile (a, s', k') ->
888        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
889          Csyntax.Sskip, k', e1, m)) }
890      | Csem.Kdowhile (a, s', k') ->
891        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
892          Csyntax.Sskip, k', e1, m)) }
893      | Csem.Kfor2 (a2, a3, s', k') ->
894        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
895          Csyntax.Sskip, k', e1, m)) }
896      | Csem.Kfor3 (x, x0, x1, x2) ->
897        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
898      | Csem.Kswitch k' ->
899        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
900          Csyntax.Sskip, k', e1, m)) }
901      | Csem.Kcall (x, x0, x1, x2) ->
902        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState))
903   | Csyntax.Scontinue ->
904     (match k with
905      | Csem.Kstop -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
906      | Csem.Kseq (s', k') ->
907        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
908          Csyntax.Scontinue, k', e1, m)) }
909      | Csem.Kwhile (a, s', k') ->
910        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
911          (Csyntax.Swhile (a, s')), k', e1, m)) }
912      | Csem.Kdowhile (a, s', k') ->
913        Obj.magic
914          (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
915            (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in Obj.magic x)
916            (fun v tr ->
917            Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
918              (Obj.magic
919                (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a))))
920              (fun b ->
921              match b with
922              | Bool.True ->
923                Obj.magic
924                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
925                    (Csyntax.Sdowhile (a, s')), k', e1, m)) })
926              | Bool.False ->
927                Obj.magic
928                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
929                    Csyntax.Sskip, k', e1, m)) }))))
930      | Csem.Kfor2 (a2, a3, s', k') ->
931        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, a3,
932          (Csem.Kfor3 (a2, a3, s', k')), e1, m)) }
933      | Csem.Kfor3 (x, x0, x1, x2) ->
934        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
935      | Csem.Kswitch k' ->
936        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
937          Csyntax.Scontinue, k', e1, m)) }
938      | Csem.Kcall (x, x0, x1, x2) ->
939        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState))
940   | Csyntax.Sreturn a_opt ->
941     (match a_opt with
942      | Types.None ->
943        (match f.Csyntax.fn_return with
944         | Csyntax.Tvoid ->
945           IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Returnstate
946             (Values.Vundef, (Csem.call_cont k),
947             (GenMem.free_list m (Csem.blocks_of_env e1)))) }
948         | Csyntax.Tint (x, x0) ->
949           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
950         | Csyntax.Tpointer x ->
951           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
952         | Csyntax.Tarray (x, x0) ->
953           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
954         | Csyntax.Tfunction (x, x0) ->
955           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
956         | Csyntax.Tstruct (x, x0) ->
957           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
958         | Csyntax.Tunion (x, x0) ->
959           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
960         | Csyntax.Tcomp_ptr x ->
961           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
962      | Types.Some a ->
963        (match TypeComparison.type_eq_dec f.Csyntax.fn_return Csyntax.Tvoid with
964         | Types.Inl _ ->
965           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
966         | Types.Inr _ ->
967           Obj.magic
968             (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
969               (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in
970               Obj.magic x) (fun v tr ->
971               Obj.magic
972                 (IO.ret { Types.fst = tr; Types.snd = (Csem.Returnstate (v,
973                   (Csem.call_cont k),
974                   (GenMem.free_list m (Csem.blocks_of_env e1)))) })))))
975   | Csyntax.Sswitch (a, sl) ->
976     Obj.magic
977       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
978         (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in Obj.magic x)
979         (fun v tr ->
980         match v with
981         | Values.Vundef ->
982           Obj.magic (IOMonad.Wrong (Errors.msg ErrorMessages.TypeMismatch))
983         | Values.Vint (sz, n) ->
984           (match Csyntax.typeof a with
985            | Csyntax.Tvoid ->
986              Obj.magic (IOMonad.Wrong
987                (Errors.msg ErrorMessages.TypeMismatch))
988            | Csyntax.Tint (sz', x) ->
989              (match TypeComparison.sz_eq_dec sz sz' with
990               | Types.Inl _ ->
991                 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
992                   (Obj.magic
993                     (IOMonad.opt_to_io
994                       (Errors.msg ErrorMessages.TypeMismatch)
995                       (Csem.select_switch sz n sl))) (fun sl' ->
996                   Obj.magic
997                     (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
998                       (Csem.seq_of_labeled_statement sl'), (Csem.Kswitch k),
999                       e1, m)) }))
1000               | Types.Inr _ ->
1001                 Obj.magic (IOMonad.Wrong
1002                   (Errors.msg ErrorMessages.TypeMismatch)))
1003            | Csyntax.Tpointer x ->
1004              Obj.magic (IOMonad.Wrong
1005                (Errors.msg ErrorMessages.TypeMismatch))
1006            | Csyntax.Tarray (x, x0) ->
1007              Obj.magic (IOMonad.Wrong
1008                (Errors.msg ErrorMessages.TypeMismatch))
1009            | Csyntax.Tfunction (x, x0) ->
1010              Obj.magic (IOMonad.Wrong
1011                (Errors.msg ErrorMessages.TypeMismatch))
1012            | Csyntax.Tstruct (x, x0) ->
1013              Obj.magic (IOMonad.Wrong
1014                (Errors.msg ErrorMessages.TypeMismatch))
1015            | Csyntax.Tunion (x, x0) ->
1016              Obj.magic (IOMonad.Wrong
1017                (Errors.msg ErrorMessages.TypeMismatch))
1018            | Csyntax.Tcomp_ptr x ->
1019              Obj.magic (IOMonad.Wrong
1020                (Errors.msg ErrorMessages.TypeMismatch)))
1021         | Values.Vnull ->
1022           Obj.magic (IOMonad.Wrong (Errors.msg ErrorMessages.TypeMismatch))
1023         | Values.Vptr x ->
1024           Obj.magic (IOMonad.Wrong (Errors.msg ErrorMessages.TypeMismatch))))
1025   | Csyntax.Slabel (lbl, s') ->
1026     IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s', k, e1,
1027       m)) }
1028   | Csyntax.Sgoto lbl ->
1029     (match Csem.find_label lbl f.Csyntax.fn_body (Csem.call_cont k) with
1030      | Types.None ->
1031        IOMonad.Wrong (List.Cons ((Errors.MSG ErrorMessages.UnknownLabel),
1032          (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, lbl)),
1033          List.Nil))))
1034      | Types.Some sk' ->
1035        let { Types.fst = s'; Types.snd = k' } = sk' in
1036        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s', k',
1037          e1, m)) })
1038   | Csyntax.Scost (lbl, s') ->
1039     IO.ret { Types.fst = (Events.echarge lbl); Types.snd = (Csem.State (f,
1040       s', k, e1, m)) })
1041| Csem.Callstate (x, f0, vargs, k, m) ->
1042  (match f0 with
1043   | Csyntax.CL_Internal f ->
1044     let { Types.fst = e1; Types.snd = m1 } =
1045       exec_alloc_variables Csem.empty_env m
1046         (List.append f.Csyntax.fn_params f.Csyntax.fn_vars)
1047     in
1048     Obj.magic
1049       (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
1050         (let x0 =
1051            IOMonad.err_to_io
1052              (exec_bind_parameters e1 m1 f.Csyntax.fn_params vargs)
1053          in
1054         Obj.magic x0) (fun m2 ->
1055         Obj.magic
1056           (IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
1057             f.Csyntax.fn_body, k, e1, m2)) })))
1058   | Csyntax.CL_External (f, argtys, retty) ->
1059     Obj.magic
1060       (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
1061         (let x0 =
1062            IOMonad.err_to_io
1063              (IO.check_eventval_list vargs
1064                (Csyntax.typlist_of_typelist argtys))
1065          in
1066         Obj.magic x0) (fun evargs ->
1067         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
1068           (Obj.magic
1069             (IO.do_io f evargs
1070               (AST.proj_sig_res (Csyntax.signature_of_type argtys retty))))
1071           (fun evres ->
1072           Obj.magic
1073             (IO.ret { Types.fst =
1074               (Events.eextcall f evargs
1075                 (IO.mk_eventval
1076                   (AST.proj_sig_res
1077                     (Csyntax.signature_of_type argtys retty)) evres));
1078               Types.snd = (Csem.Returnstate
1079               ((IO.mk_val
1080                  (AST.proj_sig_res (Csyntax.signature_of_type argtys retty))
1081                  evres), k, m)) })))))
1082| Csem.Returnstate (res1, k, m) ->
1083  (match k with
1084   | Csem.Kstop ->
1085     (match res1 with
1086      | Values.Vundef ->
1087        IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
1088      | Values.Vint (sz, r) ->
1089        (match sz with
1090         | AST.I8 ->
1091           (fun x -> IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
1092         | AST.I16 ->
1093           (fun x -> IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
1094         | AST.I32 ->
1095           (fun r5 ->
1096             IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Finalstate
1097               r5) })) r
1098      | Values.Vnull ->
1099        IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
1100      | Values.Vptr x ->
1101        IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
1102   | Csem.Kseq (x, x0) ->
1103     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
1104   | Csem.Kwhile (x, x0, x1) ->
1105     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
1106   | Csem.Kdowhile (x, x0, x1) ->
1107     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
1108   | Csem.Kfor2 (x, x0, x1, x2) ->
1109     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
1110   | Csem.Kfor3 (x, x0, x1, x2) ->
1111     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
1112   | Csem.Kswitch x -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
1113   | Csem.Kcall (r, f, e1, k') ->
1114     (match r with
1115      | Types.None ->
1116        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
1117          Csyntax.Sskip, k', e1, m)) }
1118      | Types.Some r' ->
1119        let { Types.fst = l; Types.snd = ty } = r' in
1120        Obj.magic
1121          (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
1122            (Obj.magic
1123              (IOMonad.opt_to_io (Errors.msg ErrorMessages.FailedStore)
1124                (store_value_of_type' ty m l res1))) (fun m' ->
1125            Obj.magic
1126              (IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
1127                Csyntax.Sskip, k', e1, m')) })))))
1128| Csem.Finalstate r -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
1129
1130(** val make_global0 : Csyntax.clight_program -> Csem.genv0 **)
1131let make_global0 p =
1132  Globalenvs.globalenv Types.fst p
1133
1134(** val make_initial_state0 :
1135    Csyntax.clight_program -> Csem.state0 Errors.res **)
1136let rec make_initial_state0 p =
1137  let ge0 = make_global0 p in
1138  Obj.magic
1139    (Monad.m_bind0 (Monad.max_def Errors.res0)
1140      (Obj.magic (Globalenvs.init_mem Types.fst p)) (fun m0 ->
1141      Monad.m_bind0 (Monad.max_def Errors.res0)
1142        (Obj.magic
1143          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
1144            (Globalenvs.find_symbol ge0 p.AST.prog_main))) (fun b ->
1145        Monad.m_bind0 (Monad.max_def Errors.res0)
1146          (Obj.magic
1147            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
1148              (Globalenvs.find_funct_ptr ge0 b))) (fun f ->
1149          Obj.magic (Errors.OK (Csem.Callstate (p.AST.prog_main, f, List.Nil,
1150            Csem.Kstop, m0)))))))
1151
1152(** val is_final0 : Csem.state0 -> Integers.int Types.option **)
1153let rec is_final0 = function
1154| Csem.State (x, x0, x1, x2, x3) -> Types.None
1155| Csem.Callstate (x, x0, x1, x2, x3) -> Types.None
1156| Csem.Returnstate (x, x0, x1) -> Types.None
1157| Csem.Finalstate r -> Types.Some r
1158
1159(** val is_final_state :
1160    Csem.state0 -> (Integers.int Types.sig0, __) Types.sum **)
1161let is_final_state st =
1162  Csem.state_rect_Type0 (fun f s k e1 m -> Types.Inr __) (fun vf f l k m ->
1163    Types.Inr __) (fun v k m -> Types.Inr __) (fun r -> Types.Inl r) st
1164
1165(** val exec_steps0 :
1166    Nat.nat -> Csem.genv0 -> Csem.state0 -> (IO.io_out, IO.io_in,
1167    (Events.trace, Csem.state0) Types.prod) IOMonad.iO **)
1168let rec exec_steps0 n ge0 s =
1169  match is_final_state s with
1170  | Types.Inl x -> IO.ret { Types.fst = Events.e0; Types.snd = s }
1171  | Types.Inr _ ->
1172    (match n with
1173     | Nat.O -> IO.ret { Types.fst = Events.e0; Types.snd = s }
1174     | Nat.S n' ->
1175       Obj.magic
1176         (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
1177           (Obj.magic (exec_step ge0 s)) (fun t s' ->
1178           Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
1179             (Obj.magic (exec_steps0 n' ge0 s')) (fun t' s'' ->
1180             Obj.magic
1181               (IO.ret { Types.fst = (Events.eapp t t'); Types.snd = s'' })))))
1182
1183(** val clight_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
1184let clight_exec =
1185  { SmallstepExec.is_final = (fun x -> Obj.magic is_final0);
1186    SmallstepExec.step = (Obj.magic exec_step) }
1187
1188(** val clight_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
1189let clight_fullexec =
1190  { SmallstepExec.es1 = clight_exec; SmallstepExec.make_global =
1191    (Obj.magic make_global0); SmallstepExec.make_initial_state =
1192    (Obj.magic make_initial_state0) }
1193
Note: See TracBrowser for help on using the repository browser.