source: extracted/cexec.ml @ 2649

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

...

File size: 48.1 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 Arithmetic
48
49open Extranat
50
51open Vector
52
53open FoldStuff
54
55open BitVector
56
57open Z
58
59open BitVectorZ
60
61open Pointers
62
63open Coqlib
64
65open Values
66
67open Events
68
69open Proper
70
71open ErrorMessages
72
73open Option
74
75open Setoids
76
77open Monad
78
79open Positive
80
81open PreIdentifiers
82
83open Errors
84
85open IOMonad
86
87open IO
88
89open SmallstepExec
90
91open TypeComparison
92
93open ClassifyOp
94
95open Smallstep
96
97open Csyntax
98
99open Extra_bool
100
101open FrontEndVal
102
103open Hide
104
105open ByteValues
106
107open GenMem
108
109open FrontEndMem
110
111open Globalenvs
112
113open Csem
114
115(** val exec_bool_of_val :
116    Values.val0 -> Csyntax.type0 -> Bool.bool Errors.res **)
117let exec_bool_of_val v ty =
118  match v with
119  | Values.Vundef ->
120    Errors.Error (Errors.msg ErrorMessages.ValueIsNotABoolean)
121  | Values.Vint (sz, i) ->
122    (match ty with
123     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
124     | Csyntax.Tint (sz', x) ->
125       AST.intsize_eq_elim sz sz' i (fun i0 -> Errors.OK
126         (Bool.notb
127           (BitVector.eq_bv (AST.bitsize_of_intsize sz') i0
128             (BitVector.zero (AST.bitsize_of_intsize sz'))))) (Errors.Error
129         (Errors.msg ErrorMessages.TypeMismatch))
130     | Csyntax.Tpointer x ->
131       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
132     | Csyntax.Tarray (x, x0) ->
133       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
134     | Csyntax.Tfunction (x, x0) ->
135       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
136     | Csyntax.Tstruct (x, x0) ->
137       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
138     | Csyntax.Tunion (x, x0) ->
139       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
140     | Csyntax.Tcomp_ptr x ->
141       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
142  | Values.Vnull ->
143    (match ty with
144     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
145     | Csyntax.Tint (x, x0) ->
146       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
147     | Csyntax.Tpointer x -> Errors.OK Bool.False
148     | Csyntax.Tarray (x, x0) ->
149       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
150     | Csyntax.Tfunction (x, x0) ->
151       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
152     | Csyntax.Tstruct (x, x0) ->
153       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
154     | Csyntax.Tunion (x, x0) ->
155       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
156     | Csyntax.Tcomp_ptr x ->
157       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
158  | Values.Vptr x ->
159    (match ty with
160     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
161     | Csyntax.Tint (x0, x1) ->
162       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
163     | Csyntax.Tpointer x0 -> Errors.OK Bool.True
164     | Csyntax.Tarray (x0, x1) ->
165       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
166     | Csyntax.Tfunction (x0, x1) ->
167       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
168     | Csyntax.Tstruct (x0, x1) ->
169       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
170     | Csyntax.Tunion (x0, x1) ->
171       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
172     | Csyntax.Tcomp_ptr x0 ->
173       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
174
175(** val try_cast_null :
176    GenMem.mem1 -> AST.intsize -> BitVector.bitVector -> Csyntax.type0 ->
177    Csyntax.type0 -> Values.val0 Errors.res **)
178let try_cast_null m sz i ty ty' =
179  match BitVector.eq_bv (AST.bitsize_of_intsize sz) i
180          (BitVector.zero (AST.bitsize_of_intsize sz)) with
181  | Bool.True ->
182    (match ty with
183     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadCast)
184     | Csyntax.Tint (sz', x) ->
185       (match AST.eq_intsize sz sz' with
186        | Bool.True ->
187          (match ty' with
188           | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadCast)
189           | Csyntax.Tint (x0, x1) ->
190             Errors.Error (Errors.msg ErrorMessages.BadCast)
191           | Csyntax.Tpointer x0 -> Errors.OK Values.Vnull
192           | Csyntax.Tarray (x0, x1) -> Errors.OK Values.Vnull
193           | Csyntax.Tfunction (x0, x1) -> Errors.OK Values.Vnull
194           | Csyntax.Tstruct (x0, x1) ->
195             Errors.Error (Errors.msg ErrorMessages.BadCast)
196           | Csyntax.Tunion (x0, x1) ->
197             Errors.Error (Errors.msg ErrorMessages.BadCast)
198           | Csyntax.Tcomp_ptr x0 ->
199             Errors.Error (Errors.msg ErrorMessages.BadCast))
200        | Bool.False -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
201     | Csyntax.Tpointer x -> Errors.Error (Errors.msg ErrorMessages.BadCast)
202     | Csyntax.Tarray (x, x0) ->
203       Errors.Error (Errors.msg ErrorMessages.BadCast)
204     | Csyntax.Tfunction (x, x0) ->
205       Errors.Error (Errors.msg ErrorMessages.BadCast)
206     | Csyntax.Tstruct (x, x0) ->
207       Errors.Error (Errors.msg ErrorMessages.BadCast)
208     | Csyntax.Tunion (x, x0) ->
209       Errors.Error (Errors.msg ErrorMessages.BadCast)
210     | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg ErrorMessages.BadCast))
211  | Bool.False -> Errors.Error (Errors.msg ErrorMessages.BadCast)
212
213(** val ptr_like_type : Csyntax.type0 -> Bool.bool **)
214let ptr_like_type = function
215| Csyntax.Tvoid -> Bool.False
216| Csyntax.Tint (x, x0) -> Bool.False
217| Csyntax.Tpointer x -> Bool.True
218| Csyntax.Tarray (x, x0) -> Bool.True
219| Csyntax.Tfunction (x, x0) -> Bool.True
220| Csyntax.Tstruct (x, x0) -> Bool.False
221| Csyntax.Tunion (x, x0) -> Bool.False
222| Csyntax.Tcomp_ptr x -> Bool.False
223
224(** val exec_cast :
225    GenMem.mem1 -> Values.val0 -> Csyntax.type0 -> Csyntax.type0 ->
226    Values.val0 Errors.res **)
227let exec_cast m v ty ty' =
228  match v with
229  | Values.Vundef -> Errors.Error (Errors.msg ErrorMessages.BadCast)
230  | Values.Vint (sz, i) ->
231    (match ty with
232     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
233     | Csyntax.Tint (sz1, si1) ->
234       AST.intsize_eq_elim sz sz1 i (fun i0 ->
235         match ty' with
236         | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadCast)
237         | Csyntax.Tint (sz2, si2) ->
238           Errors.OK (Values.Vint (sz2, (Csem.cast_int_int sz1 si1 sz2 i0)))
239         | Csyntax.Tpointer x ->
240           Obj.magic
241             (Monad.m_bind0 (Monad.max_def Errors.res0)
242               (Obj.magic (try_cast_null m sz1 i0 ty ty')) (fun r ->
243               Obj.magic (Errors.OK r)))
244         | Csyntax.Tarray (x, x0) ->
245           Obj.magic
246             (Monad.m_bind0 (Monad.max_def Errors.res0)
247               (Obj.magic (try_cast_null m sz1 i0 ty ty')) (fun r ->
248               Obj.magic (Errors.OK r)))
249         | Csyntax.Tfunction (x, x0) ->
250           Obj.magic
251             (Monad.m_bind0 (Monad.max_def Errors.res0)
252               (Obj.magic (try_cast_null m sz1 i0 ty ty')) (fun r ->
253               Obj.magic (Errors.OK r)))
254         | Csyntax.Tstruct (x, x0) ->
255           Errors.Error (Errors.msg ErrorMessages.BadCast)
256         | Csyntax.Tunion (x, x0) ->
257           Errors.Error (Errors.msg ErrorMessages.BadCast)
258         | Csyntax.Tcomp_ptr x ->
259           Errors.Error (Errors.msg ErrorMessages.BadCast)) (Errors.Error
260         (Errors.msg ErrorMessages.BadCast))
261     | Csyntax.Tpointer x ->
262       Obj.magic
263         (Monad.m_bind0 (Monad.max_def Errors.res0)
264           (Obj.magic (try_cast_null m sz i ty ty')) (fun r ->
265           Obj.magic (Errors.OK r)))
266     | Csyntax.Tarray (x, x0) ->
267       Obj.magic
268         (Monad.m_bind0 (Monad.max_def Errors.res0)
269           (Obj.magic (try_cast_null m sz i ty ty')) (fun r ->
270           Obj.magic (Errors.OK r)))
271     | Csyntax.Tfunction (x, x0) ->
272       Obj.magic
273         (Monad.m_bind0 (Monad.max_def Errors.res0)
274           (Obj.magic (try_cast_null m sz i ty ty')) (fun r ->
275           Obj.magic (Errors.OK r)))
276     | Csyntax.Tstruct (x, x0) ->
277       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
278     | Csyntax.Tunion (x, x0) ->
279       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
280     | Csyntax.Tcomp_ptr x ->
281       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
282  | Values.Vnull ->
283    (match Bool.andb (ptr_like_type ty) (ptr_like_type ty') with
284     | Bool.True -> Errors.OK Values.Vnull
285     | Bool.False -> Errors.Error (Errors.msg ErrorMessages.BadCast))
286  | Values.Vptr ptr ->
287    (match Bool.andb (ptr_like_type ty) (ptr_like_type ty') with
288     | Bool.True -> Errors.OK (Values.Vptr ptr)
289     | Bool.False -> Errors.Error (Errors.msg ErrorMessages.BadCast))
290
291(** val load_value_of_type' :
292    Csyntax.type0 -> GenMem.mem1 -> (Pointers.block, Pointers.offset)
293    Types.prod -> Values.val0 Types.option **)
294let load_value_of_type' ty m l =
295  let { Types.fst = loc; Types.snd = ofs } = l in
296  Csem.load_value_of_type ty m loc ofs
297
298(** val exec_expr :
299    Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr -> (Values.val0,
300    Events.trace) Types.prod Errors.res **)
301let rec exec_expr ge0 en m = function
302| Csyntax.Expr (e', ty) ->
303  (match e' with
304   | Csyntax.Econst_int (sz, i) ->
305     (match ty with
306      | Csyntax.Tvoid ->
307        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
308      | Csyntax.Tint (sz', x) ->
309        (match AST.eq_intsize sz sz' with
310         | Bool.True ->
311           Errors.OK { Types.fst = (Values.Vint (sz, i)); Types.snd =
312             Events.e0 }
313         | Bool.False ->
314           Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
315      | Csyntax.Tpointer x ->
316        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
317      | Csyntax.Tarray (x, x0) ->
318        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
319      | Csyntax.Tfunction (x, x0) ->
320        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
321      | Csyntax.Tstruct (x, x0) ->
322        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
323      | Csyntax.Tunion (x, x0) ->
324        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
325      | Csyntax.Tcomp_ptr x ->
326        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
327   | Csyntax.Evar x ->
328     Obj.magic
329       (Monad.m_bind2 (Monad.max_def Errors.res0)
330         (Obj.magic (exec_lvalue' ge0 en m e' ty)) (fun l tr ->
331         Monad.m_bind0 (Monad.max_def Errors.res0)
332           (Obj.magic
333             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
334               (load_value_of_type' ty m l))) (fun v ->
335           Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
336   | Csyntax.Ederef x ->
337     Obj.magic
338       (Monad.m_bind2 (Monad.max_def Errors.res0)
339         (Obj.magic (exec_lvalue' ge0 en m e' ty)) (fun l tr ->
340         Monad.m_bind0 (Monad.max_def Errors.res0)
341           (Obj.magic
342             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
343               (load_value_of_type' ty m l))) (fun v ->
344           Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
345   | Csyntax.Eaddrof a ->
346     Obj.magic
347       (Monad.m_bind2 (Monad.max_def Errors.res0)
348         (Obj.magic (exec_lvalue ge0 en m a)) (fun lo tr ->
349         match ty with
350         | Csyntax.Tvoid ->
351           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
352         | Csyntax.Tint (x, x0) ->
353           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
354         | Csyntax.Tpointer x ->
355           let { Types.fst = loc; Types.snd = ofs } = lo in
356           Obj.magic (Errors.OK { Types.fst = (Values.Vptr
357             { Pointers.pblock = loc; Pointers.poff = ofs }); Types.snd =
358             tr })
359         | Csyntax.Tarray (x, x0) ->
360           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
361         | Csyntax.Tfunction (x, x0) ->
362           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
363         | Csyntax.Tstruct (x, x0) ->
364           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
365         | Csyntax.Tunion (x, x0) ->
366           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
367         | Csyntax.Tcomp_ptr x ->
368           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))))
369   | Csyntax.Eunop (op0, a) ->
370     Obj.magic
371       (Monad.m_bind2 (Monad.max_def Errors.res0)
372         (Obj.magic (exec_expr ge0 en m a)) (fun v1 tr ->
373         Monad.m_bind0 (Monad.max_def Errors.res0)
374           (Obj.magic
375             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
376               (Csem.sem_unary_operation op0 v1 (Csyntax.typeof a))))
377           (fun v -> Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
378   | Csyntax.Ebinop (op0, a1, a2) ->
379     Obj.magic
380       (Monad.m_bind2 (Monad.max_def Errors.res0)
381         (Obj.magic (exec_expr ge0 en m a1)) (fun v1 tr1 ->
382         Monad.m_bind2 (Monad.max_def Errors.res0)
383           (Obj.magic (exec_expr ge0 en m a2)) (fun v2 tr2 ->
384           Monad.m_bind0 (Monad.max_def Errors.res0)
385             (Obj.magic
386               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
387                 (Csem.sem_binary_operation op0 v1 (Csyntax.typeof a1) v2
388                   (Csyntax.typeof a2) m ty))) (fun v ->
389             Obj.magic (Errors.OK { Types.fst = v; Types.snd =
390               (Events.eapp tr1 tr2) })))))
391   | Csyntax.Ecast (ty', a) ->
392     Obj.magic
393       (Monad.m_bind2 (Monad.max_def Errors.res0)
394         (Obj.magic (exec_expr ge0 en m a)) (fun v tr ->
395         Monad.m_bind0 (Monad.max_def Errors.res0)
396           (Obj.magic (exec_cast m v (Csyntax.typeof a) ty')) (fun v' ->
397           Obj.magic (Errors.OK { Types.fst = v'; Types.snd = tr }))))
398   | Csyntax.Econdition (a1, a2, a3) ->
399     Obj.magic
400       (Monad.m_bind2 (Monad.max_def Errors.res0)
401         (Obj.magic (exec_expr ge0 en m a1)) (fun v tr1 ->
402         Monad.m_bind0 (Monad.max_def Errors.res0)
403           (Obj.magic (exec_bool_of_val v (Csyntax.typeof a1))) (fun b ->
404           Monad.m_bind2 (Monad.max_def Errors.res0)
405             (match b with
406              | Bool.True -> Obj.magic (exec_expr ge0 en m a2)
407              | Bool.False -> Obj.magic (exec_expr ge0 en m a3))
408             (fun v' tr2 ->
409             Obj.magic (Errors.OK { Types.fst = v'; Types.snd =
410               (Events.eapp tr1 tr2) })))))
411   | Csyntax.Eandbool (a1, a2) ->
412     Obj.magic
413       (Monad.m_bind2 (Monad.max_def Errors.res0)
414         (Obj.magic (exec_expr ge0 en m a1)) (fun v1 tr1 ->
415         Monad.m_bind0 (Monad.max_def Errors.res0)
416           (Obj.magic (exec_bool_of_val v1 (Csyntax.typeof a1))) (fun b1 ->
417           match b1 with
418           | Bool.True ->
419             Monad.m_bind2 (Monad.max_def Errors.res0)
420               (Obj.magic (exec_expr ge0 en m a2)) (fun v2 tr2 ->
421               Monad.m_bind0 (Monad.max_def Errors.res0)
422                 (Obj.magic (exec_bool_of_val v2 (Csyntax.typeof a2)))
423                 (fun b2 ->
424                 match Csem.cast_bool_to_target ty (Types.Some
425                         (Values.of_bool b2)) with
426                 | Types.None ->
427                   Obj.magic (Errors.Error
428                     (Errors.msg ErrorMessages.BadlyTypedTerm))
429                 | Types.Some v20 ->
430                   Obj.magic (Errors.OK { Types.fst = v20; Types.snd =
431                     (Events.eapp tr1 tr2) })))
432           | Bool.False ->
433             (match Csem.cast_bool_to_target ty (Types.Some Values.vfalse) with
434              | Types.None ->
435                Obj.magic (Errors.Error
436                  (Errors.msg ErrorMessages.BadlyTypedTerm))
437              | Types.Some vfls ->
438                Obj.magic (Errors.OK { Types.fst = vfls; Types.snd = tr1 })))))
439   | Csyntax.Eorbool (a1, a2) ->
440     Obj.magic
441       (Monad.m_bind2 (Monad.max_def Errors.res0)
442         (Obj.magic (exec_expr ge0 en m a1)) (fun v1 tr1 ->
443         Monad.m_bind0 (Monad.max_def Errors.res0)
444           (Obj.magic (exec_bool_of_val v1 (Csyntax.typeof a1))) (fun b1 ->
445           match b1 with
446           | Bool.True ->
447             (match Csem.cast_bool_to_target ty (Types.Some Values.vtrue) with
448              | Types.None ->
449                Obj.magic (Errors.Error
450                  (Errors.msg ErrorMessages.BadlyTypedTerm))
451              | Types.Some vtr ->
452                Obj.magic (Errors.OK { Types.fst = vtr; Types.snd = tr1 }))
453           | Bool.False ->
454             Monad.m_bind2 (Monad.max_def Errors.res0)
455               (Obj.magic (exec_expr ge0 en m a2)) (fun v2 tr2 ->
456               Monad.m_bind0 (Monad.max_def Errors.res0)
457                 (Obj.magic (exec_bool_of_val v2 (Csyntax.typeof a2)))
458                 (fun b2 ->
459                 match Csem.cast_bool_to_target ty (Types.Some
460                         (Values.of_bool b2)) with
461                 | Types.None ->
462                   Obj.magic (Errors.Error
463                     (Errors.msg ErrorMessages.BadlyTypedTerm))
464                 | Types.Some v20 ->
465                   Obj.magic (Errors.OK { Types.fst = v20; Types.snd =
466                     (Events.eapp tr1 tr2) }))))))
467   | Csyntax.Esizeof ty' ->
468     (match ty with
469      | Csyntax.Tvoid ->
470        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
471      | Csyntax.Tint (sz, x) ->
472        Errors.OK { Types.fst = (Values.Vint (sz,
473          (AST.repr0 sz (Csyntax.sizeof ty')))); Types.snd = Events.e0 }
474      | Csyntax.Tpointer x ->
475        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
476      | Csyntax.Tarray (x, x0) ->
477        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
478      | Csyntax.Tfunction (x, x0) ->
479        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
480      | Csyntax.Tstruct (x, x0) ->
481        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
482      | Csyntax.Tunion (x, x0) ->
483        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
484      | Csyntax.Tcomp_ptr x ->
485        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
486   | Csyntax.Efield (x, x0) ->
487     Obj.magic
488       (Monad.m_bind2 (Monad.max_def Errors.res0)
489         (Obj.magic (exec_lvalue' ge0 en m e' ty)) (fun l tr ->
490         Monad.m_bind0 (Monad.max_def Errors.res0)
491           (Obj.magic
492             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
493               (load_value_of_type' ty m l))) (fun v ->
494           Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
495   | Csyntax.Ecost (l, a) ->
496     Obj.magic
497       (Monad.m_bind2 (Monad.max_def Errors.res0)
498         (Obj.magic (exec_expr ge0 en m a)) (fun v tr ->
499         Obj.magic (Errors.OK { Types.fst = v; Types.snd =
500           (Events.eapp (Events.echarge l) tr) }))))
501(** val exec_lvalue' :
502    Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr_descr ->
503    Csyntax.type0 -> ((Pointers.block, Pointers.offset) Types.prod,
504    Events.trace) Types.prod Errors.res **)
505and exec_lvalue' ge0 en m e' ty =
506  match e' with
507  | Csyntax.Econst_int (x, x0) ->
508    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
509  | Csyntax.Evar id ->
510    (match Identifiers.lookup0 PreIdentifiers.SymbolTag en id with
511     | Types.None ->
512       Obj.magic
513         (Monad.m_bind0 (Monad.max_def Errors.res0)
514           (Obj.magic
515             (Errors.opt_to_res (List.Cons ((Errors.MSG
516               ErrorMessages.UnknownIdentifier), (List.Cons ((Errors.CTX
517               (PreIdentifiers.SymbolTag, id)), List.Nil))))
518               (Globalenvs.find_symbol ge0 id))) (fun l ->
519           Obj.magic (Errors.OK { Types.fst = { Types.fst = l; Types.snd =
520             Pointers.zero_offset }; Types.snd = Events.e0 })))
521     | Types.Some loc ->
522       Errors.OK { Types.fst = { Types.fst = loc; Types.snd =
523         Pointers.zero_offset }; Types.snd = Events.e0 })
524  | Csyntax.Ederef a ->
525    Obj.magic
526      (Monad.m_bind2 (Monad.max_def Errors.res0)
527        (Obj.magic (exec_expr ge0 en m a)) (fun v tr ->
528        match v with
529        | Values.Vundef ->
530          Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
531        | Values.Vint (x, x0) ->
532          Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
533        | Values.Vnull ->
534          Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
535        | Values.Vptr ptr ->
536          Obj.magic (Errors.OK { Types.fst = { Types.fst =
537            ptr.Pointers.pblock; Types.snd = ptr.Pointers.poff }; Types.snd =
538            tr })))
539  | Csyntax.Eaddrof x ->
540    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
541  | Csyntax.Eunop (x, x0) ->
542    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
543  | Csyntax.Ebinop (x, x0, x1) ->
544    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
545  | Csyntax.Ecast (x, x0) ->
546    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
547  | Csyntax.Econdition (x, x0, x1) ->
548    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
549  | Csyntax.Eandbool (x, x0) ->
550    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
551  | Csyntax.Eorbool (x, x0) ->
552    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
553  | Csyntax.Esizeof x ->
554    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
555  | Csyntax.Efield (a, i) ->
556    (match Csyntax.typeof a with
557     | Csyntax.Tvoid ->
558       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
559     | Csyntax.Tint (x, x0) ->
560       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
561     | Csyntax.Tpointer x ->
562       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
563     | Csyntax.Tarray (x, x0) ->
564       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
565     | Csyntax.Tfunction (x, x0) ->
566       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
567     | Csyntax.Tstruct (id, fList) ->
568       Obj.magic
569         (Monad.m_bind2 (Monad.max_def Errors.res0)
570           (Obj.magic (exec_lvalue ge0 en m a)) (fun lofs tr ->
571           Monad.m_bind0 (Monad.max_def Errors.res0)
572             (Obj.magic (Csyntax.field_offset i fList)) (fun delta ->
573             Obj.magic (Errors.OK { Types.fst = { Types.fst = lofs.Types.fst;
574               Types.snd =
575               (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
576                 lofs.Types.snd (AST.repr0 AST.I16 delta)) }; Types.snd =
577               tr }))))
578     | Csyntax.Tunion (id, fList) ->
579       Obj.magic
580         (Monad.m_bind2 (Monad.max_def Errors.res0)
581           (Obj.magic (exec_lvalue ge0 en m a)) (fun lofs tr ->
582           Obj.magic (Errors.OK { Types.fst = lofs; Types.snd = tr })))
583     | Csyntax.Tcomp_ptr x ->
584       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
585  | Csyntax.Ecost (x, x0) ->
586    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
587(** val exec_lvalue :
588    Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr ->
589    ((Pointers.block, Pointers.offset) Types.prod, Events.trace) Types.prod
590    Errors.res **)
591and exec_lvalue ge0 en m = function
592| Csyntax.Expr (e', ty) -> exec_lvalue' ge0 en m e' ty
593
594(** val exec_exprlist :
595    Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr List.list ->
596    (Values.val0 List.list, Events.trace) Types.prod Errors.res **)
597let rec exec_exprlist ge0 e1 m = function
598| List.Nil -> Errors.OK { Types.fst = List.Nil; Types.snd = Events.e0 }
599| List.Cons (e2, es) ->
600  Obj.magic
601    (Monad.m_bind2 (Monad.max_def Errors.res0)
602      (Obj.magic (exec_expr ge0 e1 m e2)) (fun v tr1 ->
603      Monad.m_bind2 (Monad.max_def Errors.res0)
604        (Obj.magic (exec_exprlist ge0 e1 m es)) (fun vs tr2 ->
605        Obj.magic (Errors.OK { Types.fst = (List.Cons (v, vs)); Types.snd =
606          (Events.eapp tr1 tr2) }))))
607
608(** val exec_alloc_variables :
609    Csem.env -> GenMem.mem1 -> (AST.ident, Csyntax.type0) Types.prod
610    List.list -> (Csem.env, GenMem.mem1) Types.prod **)
611let rec exec_alloc_variables en m = function
612| List.Nil -> { Types.fst = en; Types.snd = m }
613| List.Cons (h, vars) ->
614  let { Types.fst = id; Types.snd = ty } = h in
615  let { Types.fst = m1; Types.snd = b1 } =
616    GenMem.alloc m (Z.z_of_nat Nat.O) (Z.z_of_nat (Csyntax.sizeof ty))
617  in
618  exec_alloc_variables (Identifiers.add PreIdentifiers.SymbolTag en id b1) m1
619    vars
620
621(** val exec_bind_parameters :
622    Csem.env -> GenMem.mem1 -> (AST.ident, Csyntax.type0) Types.prod
623    List.list -> Values.val0 List.list -> GenMem.mem1 Errors.res **)
624let rec exec_bind_parameters e1 m params vs =
625  match params with
626  | List.Nil ->
627    (match vs with
628     | List.Nil -> Errors.OK m
629     | List.Cons (x, x0) ->
630       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters))
631  | List.Cons (idty, params') ->
632    let { Types.fst = id; Types.snd = ty } = idty in
633    (match vs with
634     | List.Nil ->
635       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)
636     | List.Cons (v1, vl) ->
637       Obj.magic
638         (Monad.m_bind0 (Monad.max_def Errors.res0)
639           (Obj.magic
640             (Errors.opt_to_res (List.Cons ((Errors.MSG
641               ErrorMessages.UnknownIdentifier), (List.Cons ((Errors.CTX
642               (PreIdentifiers.SymbolTag, id)), List.Nil))))
643               (Identifiers.lookup0 PreIdentifiers.SymbolTag e1 id)))
644           (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 e1 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.mem1 -> (Pointers.block, Pointers.offset)
684    Types.prod -> Values.val0 -> GenMem.mem1 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.genv0 -> Csem.state0 -> (IO.io_out, IO.io_in, (Events.trace,
691    Csem.state0) Types.prod) IOMonad.iO **)
692let rec exec_step ge0 = function
693| Csem.State (f, s, k, e1, 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 e1)))) }
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          e1, 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', e1, 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 ge0 e1 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', e1, m)) })
737              | Bool.False ->
738                Obj.magic
739                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
740                    Csyntax.Sskip, k', e1, 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')), e1, 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', e1, m)) }
747      | Csem.Kswitch k' ->
748        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
749          Csyntax.Sskip, k', e1, 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 e1)))) }
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 ge0 e1 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 ge0 e1 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, e1, 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 ge0 e1 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 ge0 e1 m al) in
793           Obj.magic x) (fun vargs tr3 ->
794           Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
795             (Obj.magic
796               (IOMonad.opt_to_io (Errors.msg ErrorMessages.BadFunctionValue)
797                 (Globalenvs.find_funct ge0 vf))) (fun fd ->
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 (fd, vargs, (Csem.Kcall (Types.None, f,
808                     e1, k)), m)) })
809               | Types.Some lhs' ->
810                 Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
811                   (let x = IOMonad.err_to_io (exec_lvalue ge0 e1 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 (fd, vargs, (Csem.Kcall ((Types.Some
817                       { Types.fst = locofs; Types.snd =
818                       (Csyntax.typeof lhs') }), f, e1, 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)), e1, 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 ge0 e1 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, e1, 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 ge0 e1 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)), e1, m)
850                | Bool.False -> Csem.State (f, Csyntax.Sskip, k, e1, 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)), e1, 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 ge0 e1 m a2) in
860            Obj.magic x) (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), e1, 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)), e1,
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', e1, m)) }
883      | Csem.Kwhile (a, s', k') ->
884        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
885          Csyntax.Sskip, k', e1, m)) }
886      | Csem.Kdowhile (a, s', k') ->
887        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
888          Csyntax.Sskip, k', e1, m)) }
889      | Csem.Kfor2 (a2, a3, s', k') ->
890        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
891          Csyntax.Sskip, k', e1, 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', e1, 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', e1, 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', e1, 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 ge0 e1 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', e1, m)) })
922              | Bool.False ->
923                Obj.magic
924                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
925                    Csyntax.Sskip, k', e1, 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')), e1, 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', e1, 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 e1)))) }
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 ge0 e1 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 e1)))) })))))
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 ge0 e1 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                       e1, 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, e1,
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          e1, m)) })
1034   | Csyntax.Scost (lbl, s') ->
1035     IO.ret { Types.fst = (Events.echarge lbl); Types.snd = (Csem.State (f,
1036       s', k, e1, m)) })
1037| Csem.Callstate (f0, vargs, k, m) ->
1038  (match f0 with
1039   | Csyntax.CL_Internal f ->
1040     let { Types.fst = e1; 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 x =
1047            IOMonad.err_to_io
1048              (exec_bind_parameters e1 m1 f.Csyntax.fn_params vargs)
1049          in
1050         Obj.magic x) (fun m2 ->
1051         Obj.magic
1052           (IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
1053             f.Csyntax.fn_body, k, e1, m2)) })))
1054   | Csyntax.CL_External (f, argtys, retty) ->
1055     Obj.magic
1056       (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
1057         (let x =
1058            IOMonad.err_to_io
1059              (IO.check_eventval_list vargs
1060                (Csyntax.typlist_of_typelist argtys))
1061          in
1062         Obj.magic x) (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 (res1, k, m) ->
1079  (match k with
1080   | Csem.Kstop ->
1081     (match res1 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 r5 ->
1092             IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Finalstate
1093               r5) })) 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, e1, k') ->
1110     (match r with
1111      | Types.None ->
1112        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
1113          Csyntax.Sskip, k', e1, 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 res1))) (fun m' ->
1121            Obj.magic
1122              (IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
1123                Csyntax.Sskip, k', e1, m')) })))))
1124| Csem.Finalstate r -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
1125
1126(** val make_global0 : Csyntax.clight_program -> Csem.genv0 **)
1127let make_global0 p =
1128  Globalenvs.globalenv Types.fst p
1129
1130(** val make_initial_state0 :
1131    Csyntax.clight_program -> Csem.state0 Errors.res **)
1132let rec make_initial_state0 p =
1133  let ge0 = make_global0 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 ge0 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 ge0 b))) (fun f ->
1145          Obj.magic (Errors.OK (Csem.Callstate (f, List.Nil, Csem.Kstop,
1146            m0)))))))
1147
1148(** val is_final0 : Csem.state0 -> Integers.int Types.option **)
1149let rec is_final0 = function
1150| Csem.State (x, x0, x1, x2, x3) -> Types.None
1151| Csem.Callstate (x, x0, x1, x2) -> 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.state0 -> (Integers.int Types.sig0, __) Types.sum **)
1157let is_final_state st =
1158  Csem.state_rect_Type0 (fun f s k e1 m -> Types.Inr __) (fun 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.genv0 -> Csem.state0 -> (IO.io_out, IO.io_in,
1163    (Events.trace, Csem.state0) Types.prod) IOMonad.iO **)
1164let rec exec_steps n ge0 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 ge0 s)) (fun t s' ->
1174           Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
1175             (Obj.magic (exec_steps n' ge0 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_final0);
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_global0); SmallstepExec.make_initial_state =
1188    (Obj.magic make_initial_state0) }
1189
Note: See TracBrowser for help on using the repository browser.