source: driver/extracted/cexec.ml @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

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