19 open Hints_declaration
117 (** val exec_bool_of_val :
118 Values.val0 -> Csyntax.type0 -> Bool.bool Errors.res **)
119 let exec_bool_of_val v ty =
122 Errors.Error (Errors.msg ErrorMessages.ValueIsNotABoolean)
123 | Values.Vint (sz, i) ->
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
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))
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))
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))
177 (** val try_cast_null :
178 GenMem.mem -> AST.intsize -> BitVector.bitVector -> Csyntax.type0 ->
179 Csyntax.type0 -> Values.val0 Errors.res **)
180 let 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
185 | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadCast)
186 | Csyntax.Tint (sz', x) ->
187 (match AST.eq_intsize sz sz' 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)
215 (** val ptr_like_type : Csyntax.type0 -> Bool.bool **)
216 let 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
227 GenMem.mem -> Values.val0 -> Csyntax.type0 -> Csyntax.type0 ->
228 Values.val0 Errors.res **)
229 let exec_cast m v ty ty' =
231 | Values.Vundef -> Errors.Error (Errors.msg ErrorMessages.BadCast)
232 | Values.Vint (sz, i) ->
234 | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
235 | Csyntax.Tint (sz1, si1) ->
236 AST.intsize_eq_elim sz sz1 i (fun i0 ->
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 ->
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) ->
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) ->
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 ->
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) ->
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) ->
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))
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))
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))
293 (** val load_value_of_type' :
294 Csyntax.type0 -> GenMem.mem -> (Pointers.block, Pointers.offset)
295 Types.prod -> Values.val0 Types.option **)
296 let 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
301 Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr -> (Values.val0,
302 Events.trace) Types.prod Errors.res **)
303 let rec exec_expr ge en m = function
304 | Csyntax.Expr (e', ty) ->
306 | Csyntax.Econst_int (sz, i) ->
309 Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
310 | Csyntax.Tint (sz', x) ->
311 (match AST.eq_intsize sz sz' with
313 Errors.OK { Types.fst = (Values.Vint (sz, i)); Types.snd =
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))
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)
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 ->
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)
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 ->
349 (Monad.m_bind2 (Monad.max_def Errors.res0)
350 (Obj.magic (exec_lvalue ge en m a)) (fun lo tr ->
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 =
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) ->
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)
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) ->
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)
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) ->
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) ->
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)
408 | Bool.True -> Obj.magic (exec_expr ge en m a2)
409 | Bool.False -> Obj.magic (exec_expr ge en m a3))
411 Obj.magic (Errors.OK { Types.fst = v'; Types.snd =
412 (Events.eapp tr1 tr2) })))))
413 | Csyntax.Eandbool (a1, a2) ->
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 ->
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)))
426 match Csem.cast_bool_to_target ty (Types.Some
427 (Values.of_bool b2)) with
429 Obj.magic (Errors.Error
430 (Errors.msg ErrorMessages.BadlyTypedTerm))
432 Obj.magic (Errors.OK { Types.fst = v20; Types.snd =
433 (Events.eapp tr1 tr2) })))
435 (match Csem.cast_bool_to_target ty (Types.Some Values.vfalse) with
437 Obj.magic (Errors.Error
438 (Errors.msg ErrorMessages.BadlyTypedTerm))
440 Obj.magic (Errors.OK { Types.fst = vfls; Types.snd = tr1 })))))
441 | Csyntax.Eorbool (a1, a2) ->
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 ->
449 (match Csem.cast_bool_to_target ty (Types.Some Values.vtrue) with
451 Obj.magic (Errors.Error
452 (Errors.msg ErrorMessages.BadlyTypedTerm))
454 Obj.magic (Errors.OK { Types.fst = vtr; Types.snd = tr1 }))
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)))
461 match Csem.cast_bool_to_target ty (Types.Some
462 (Values.of_bool b2)) with
464 Obj.magic (Errors.Error
465 (Errors.msg ErrorMessages.BadlyTypedTerm))
467 Obj.magic (Errors.OK { Types.fst = v20; Types.snd =
468 (Events.eapp tr1 tr2) }))))))
469 | Csyntax.Esizeof ty' ->
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) ->
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)
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) ->
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 **)
507 and exec_lvalue' ge en m e' ty =
509 | Csyntax.Econst_int (x, x0) ->
510 Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
512 (match Identifiers.lookup PreIdentifiers.SymbolTag en id with
515 (Monad.m_bind0 (Monad.max_def Errors.res0)
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 })))
524 Errors.OK { Types.fst = { Types.fst = loc; Types.snd =
525 Pointers.zero_offset }; Types.snd = Events.e0 })
526 | Csyntax.Ederef a ->
528 (Monad.m_bind2 (Monad.max_def Errors.res0)
529 (Obj.magic (exec_expr ge en m a)) (fun v tr ->
532 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
533 | Values.Vint (x, x0) ->
534 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
536 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
538 Obj.magic (Errors.OK { Types.fst = { Types.fst =
539 ptr.Pointers.pblock; Types.snd = ptr.Pointers.poff }; Types.snd =
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
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) ->
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;
577 (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
578 lofs.Types.snd (AST.repr AST.I16 delta)) }; Types.snd =
580 | Csyntax.Tunion (id, fList) ->
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 **)
592 and exec_lvalue ge en m = function
593 | Csyntax.Expr (e', ty) -> exec_lvalue' ge en m e' ty
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 **)
598 let 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) ->
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) }))))
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 **)
612 let 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))
619 exec_alloc_variables (Identifiers.add PreIdentifiers.SymbolTag en id b1) m1
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 **)
625 let rec exec_bind_parameters e m params vs =
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
636 Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)
637 | List.Cons (v1, vl) ->
639 (Monad.m_bind0 (Monad.max_def Errors.res0)
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)
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)))))
653 (** val is_is_call_cont : Csem.cont -> (__, __) Types.sum **)
654 let 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 __
664 (** val is_Sskip : Csyntax.statement -> (__, __) Types.sum **)
665 let 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 __
682 (** val store_value_of_type' :
683 Csyntax.type0 -> GenMem.mem -> (Pointers.block, Pointers.offset)
684 Types.prod -> Values.val0 -> GenMem.mem Types.option **)
685 let 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
690 Csem.genv -> Csem.state -> (IO.io_out, IO.io_in, (Events.trace,
691 Csem.state) Types.prod) IOMonad.iO **)
692 let rec exec_step ge = function
693 | Csem.State (f, s, k, e, m) ->
698 (match f.Csyntax.fn_return with
700 IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Returnstate
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',
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') ->
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)
728 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
730 (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a))))
735 (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
736 (Csyntax.Sdowhile (a, s')), k', e, m)) })
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)) }
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
753 IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Returnstate
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) ->
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)
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)
778 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
780 (IOMonad.opt_to_io (Errors.msg ErrorMessages.FailedStore)
781 (store_value_of_type' (Csyntax.typeof a1) m l v2)))
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) ->
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)
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)
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)
801 (TypeComparison.assert_type_eq (Csyntax.type_of_fundef fd)
802 (Csem.fun_typeof a)))) (fun _ ->
806 (IO.ret { Types.fst = (Events.eapp tr2 tr3); Types.snd =
807 (Csem.Callstate (id, fd, vargs, (Csem.Kcall (Types.None,
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 ->
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) ->
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)
827 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
829 (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a))))
832 (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
835 | Bool.False -> s2), k, e, m)) }))))
836 | Csyntax.Swhile (a, s') ->
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)
841 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
843 (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a))))
846 (IO.ret { Types.fst = tr; Types.snd =
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
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)
861 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
863 (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a2))))
866 (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
869 | Bool.False -> Csyntax.Sskip),
871 | Bool.True -> Csem.Kfor2 (a2, a3, s', k)
872 | Bool.False -> k), e, m)) }))))
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,
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)
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 ->
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') ->
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)
913 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
915 (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a))))
920 (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
921 (Csyntax.Sdowhile (a, s')), k', e, m)) })
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)
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 ->
939 (match f.Csyntax.fn_return with
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))
959 (match TypeComparison.type_eq_dec f.Csyntax.fn_return Csyntax.Tvoid with
961 IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
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 ->
968 (IO.ret { Types.fst = tr; Types.snd = (Csem.Returnstate (v,
970 (GenMem.free_list m (Csem.blocks_of_env e)))) })))))
971 | Csyntax.Sswitch (a, sl) ->
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)
978 Obj.magic (IOMonad.Wrong (Errors.msg ErrorMessages.TypeMismatch))
979 | Values.Vint (sz, n) ->
980 (match Csyntax.typeof a with
982 Obj.magic (IOMonad.Wrong
983 (Errors.msg ErrorMessages.TypeMismatch))
984 | Csyntax.Tint (sz', x) ->
985 (match TypeComparison.sz_eq_dec sz sz' with
987 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
990 (Errors.msg ErrorMessages.TypeMismatch)
991 (Csem.select_switch sz n sl))) (fun sl' ->
993 (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
994 (Csem.seq_of_labeled_statement sl'), (Csem.Kswitch k),
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)))
1018 Obj.magic (IOMonad.Wrong (Errors.msg ErrorMessages.TypeMismatch))
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,
1024 | Csyntax.Sgoto lbl ->
1025 (match Csem.find_label lbl f.Csyntax.fn_body (Csem.call_cont k) with
1027 IOMonad.Wrong (List.Cons ((Errors.MSG ErrorMessages.UnknownLabel),
1028 (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, lbl)),
1031 let { Types.fst = s'; Types.snd = k' } = sk' in
1032 IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s', k',
1034 | Csyntax.Scost (lbl, s') ->
1035 IO.ret { Types.fst = (Events.echarge lbl); Types.snd = (Csem.State (f,
1037 | Csem.Callstate (x, f0, vargs, k, m) ->
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)
1045 (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
1048 (exec_bind_parameters e m1 f.Csyntax.fn_params vargs)
1050 Obj.magic x0) (fun m2 ->
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) ->
1056 (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
1059 (IO.check_eventval_list vargs
1060 (Csyntax.typlist_of_typelist argtys))
1062 Obj.magic x0) (fun evargs ->
1063 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
1066 (AST.proj_sig_res (Csyntax.signature_of_type argtys retty))))
1069 (IO.ret { Types.fst =
1070 (Events.eextcall f evargs
1073 (Csyntax.signature_of_type argtys retty)) evres));
1074 Types.snd = (Csem.Returnstate
1076 (AST.proj_sig_res (Csyntax.signature_of_type argtys retty))
1077 evres), k, m)) })))))
1078 | Csem.Returnstate (res, k, m) ->
1083 IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
1084 | Values.Vint (sz, r) ->
1087 (fun x -> IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
1089 (fun x -> IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
1092 IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Finalstate
1095 IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
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') ->
1112 IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
1113 Csyntax.Sskip, k', e, m)) }
1115 let { Types.fst = l; Types.snd = ty } = r' in
1117 (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
1119 (IOMonad.opt_to_io (Errors.msg ErrorMessages.FailedStore)
1120 (store_value_of_type' ty m l res))) (fun m' ->
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)
1126 (** val make_global : Csyntax.clight_program -> Csem.genv **)
1128 Globalenvs.globalenv Types.fst p
1130 (** val make_initial_state :
1131 Csyntax.clight_program -> Csem.state Errors.res **)
1132 let rec make_initial_state p =
1133 let ge = make_global p in
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)
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)
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)))))))
1148 (** val is_final : Csem.state -> Integers.int Types.option **)
1149 let 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
1155 (** val is_final_state :
1156 Csem.state -> (Integers.int Types.sig0, __) Types.sum **)
1157 let 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
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 **)
1164 let 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 }
1169 | Nat.O -> IO.ret { Types.fst = Events.e0; Types.snd = s }
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'' ->
1177 (IO.ret { Types.fst = (Events.eapp t t'); Types.snd = s'' })))))
1179 (** val clight_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
1181 { SmallstepExec.is_final = (fun x -> Obj.magic is_final);
1182 SmallstepExec.step = (Obj.magic exec_step) }
1184 (** val clight_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
1185 let 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) }