open Preamble

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Extralib

open CostLabel

open PositiveMap

open Deqsets

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Extranat

open Vector

open FoldStuff

open BitVector

open Z

open BitVectorZ

open Pointers

open Coqlib

open Values

open Events

open Proper

open ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

open IOMonad

open IO

open SmallstepExec

open TypeComparison

open ClassifyOp

open Smallstep

open Csyntax

open Extra_bool

open FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

open Globalenvs

open Csem

(** val exec_bool_of_val :
    Values.val0 -> Csyntax.type0 -> Bool.bool Errors.res **)
let exec_bool_of_val v ty =
  match v with
  | Values.Vundef ->
    Errors.Error (Errors.msg ErrorMessages.ValueIsNotABoolean)
  | Values.Vint (sz, i) ->
    (match ty with
     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tint (sz', x) ->
       AST.intsize_eq_elim sz sz' i (fun i0 -> Errors.OK
         (Bool.notb
           (BitVector.eq_bv (AST.bitsize_of_intsize sz') i0
             (BitVector.zero (AST.bitsize_of_intsize sz'))))) (Errors.Error
         (Errors.msg ErrorMessages.TypeMismatch))
     | Csyntax.Tpointer x ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tarray (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tfunction (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tstruct (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tunion (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tcomp_ptr x ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
  | Values.Vnull ->
    (match ty with
     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tint (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tpointer x -> Errors.OK Bool.False
     | Csyntax.Tarray (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tfunction (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tstruct (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tunion (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tcomp_ptr x ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
  | Values.Vptr x ->
    (match ty with
     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tint (x0, x1) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tpointer x0 -> Errors.OK Bool.True
     | Csyntax.Tarray (x0, x1) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tfunction (x0, x1) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tstruct (x0, x1) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tunion (x0, x1) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tcomp_ptr x0 ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))

(** val try_cast_null :
    GenMem.mem -> AST.intsize -> BitVector.bitVector -> Csyntax.type0 ->
    Csyntax.type0 -> Values.val0 Errors.res **)
let try_cast_null m sz i ty ty' =
  match BitVector.eq_bv (AST.bitsize_of_intsize sz) i
          (BitVector.zero (AST.bitsize_of_intsize sz)) with
  | Bool.True ->
    (match ty with
     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadCast)
     | Csyntax.Tint (sz', x) ->
       (match AST.eq_intsize sz sz' with
        | Bool.True ->
          (match ty' with
           | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadCast)
           | Csyntax.Tint (x0, x1) ->
             Errors.Error (Errors.msg ErrorMessages.BadCast)
           | Csyntax.Tpointer x0 -> Errors.OK Values.Vnull
           | Csyntax.Tarray (x0, x1) -> Errors.OK Values.Vnull
           | Csyntax.Tfunction (x0, x1) -> Errors.OK Values.Vnull
           | Csyntax.Tstruct (x0, x1) ->
             Errors.Error (Errors.msg ErrorMessages.BadCast)
           | Csyntax.Tunion (x0, x1) ->
             Errors.Error (Errors.msg ErrorMessages.BadCast)
           | Csyntax.Tcomp_ptr x0 ->
             Errors.Error (Errors.msg ErrorMessages.BadCast))
        | Bool.False -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
     | Csyntax.Tpointer x -> Errors.Error (Errors.msg ErrorMessages.BadCast)
     | Csyntax.Tarray (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.BadCast)
     | Csyntax.Tfunction (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.BadCast)
     | Csyntax.Tstruct (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.BadCast)
     | Csyntax.Tunion (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.BadCast)
     | Csyntax.Tcomp_ptr x -> Errors.Error (Errors.msg ErrorMessages.BadCast))
  | Bool.False -> Errors.Error (Errors.msg ErrorMessages.BadCast)

(** val ptr_like_type : Csyntax.type0 -> Bool.bool **)
let ptr_like_type = function
| Csyntax.Tvoid -> Bool.False
| Csyntax.Tint (x, x0) -> Bool.False
| Csyntax.Tpointer x -> Bool.True
| Csyntax.Tarray (x, x0) -> Bool.True
| Csyntax.Tfunction (x, x0) -> Bool.True
| Csyntax.Tstruct (x, x0) -> Bool.False
| Csyntax.Tunion (x, x0) -> Bool.False
| Csyntax.Tcomp_ptr x -> Bool.False

(** val exec_cast :
    GenMem.mem -> Values.val0 -> Csyntax.type0 -> Csyntax.type0 ->
    Values.val0 Errors.res **)
let exec_cast m v ty ty' =
  match v with
  | Values.Vundef -> Errors.Error (Errors.msg ErrorMessages.BadCast)
  | Values.Vint (sz, i) ->
    (match ty with
     | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tint (sz1, si1) ->
       AST.intsize_eq_elim sz sz1 i (fun i0 ->
         match ty' with
         | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.BadCast)
         | Csyntax.Tint (sz2, si2) ->
           Errors.OK (Values.Vint (sz2, (Csem.cast_int_int sz1 si1 sz2 i0)))
         | Csyntax.Tpointer x ->
           Obj.magic
             (Monad.m_bind0 (Monad.max_def Errors.res0)
               (Obj.magic (try_cast_null m sz1 i0 ty ty')) (fun r ->
               Obj.magic (Errors.OK r)))
         | Csyntax.Tarray (x, x0) ->
           Obj.magic
             (Monad.m_bind0 (Monad.max_def Errors.res0)
               (Obj.magic (try_cast_null m sz1 i0 ty ty')) (fun r ->
               Obj.magic (Errors.OK r)))
         | Csyntax.Tfunction (x, x0) ->
           Obj.magic
             (Monad.m_bind0 (Monad.max_def Errors.res0)
               (Obj.magic (try_cast_null m sz1 i0 ty ty')) (fun r ->
               Obj.magic (Errors.OK r)))
         | Csyntax.Tstruct (x, x0) ->
           Errors.Error (Errors.msg ErrorMessages.BadCast)
         | Csyntax.Tunion (x, x0) ->
           Errors.Error (Errors.msg ErrorMessages.BadCast)
         | Csyntax.Tcomp_ptr x ->
           Errors.Error (Errors.msg ErrorMessages.BadCast)) (Errors.Error
         (Errors.msg ErrorMessages.BadCast))
     | Csyntax.Tpointer x ->
       Obj.magic
         (Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (try_cast_null m sz i ty ty')) (fun r ->
           Obj.magic (Errors.OK r)))
     | Csyntax.Tarray (x, x0) ->
       Obj.magic
         (Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (try_cast_null m sz i ty ty')) (fun r ->
           Obj.magic (Errors.OK r)))
     | Csyntax.Tfunction (x, x0) ->
       Obj.magic
         (Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (try_cast_null m sz i ty ty')) (fun r ->
           Obj.magic (Errors.OK r)))
     | Csyntax.Tstruct (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tunion (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     | Csyntax.Tcomp_ptr x ->
       Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
  | Values.Vnull ->
    (match Bool.andb (ptr_like_type ty) (ptr_like_type ty') with
     | Bool.True -> Errors.OK Values.Vnull
     | Bool.False -> Errors.Error (Errors.msg ErrorMessages.BadCast))
  | Values.Vptr ptr ->
    (match Bool.andb (ptr_like_type ty) (ptr_like_type ty') with
     | Bool.True -> Errors.OK (Values.Vptr ptr)
     | Bool.False -> Errors.Error (Errors.msg ErrorMessages.BadCast))

(** val load_value_of_type' :
    Csyntax.type0 -> GenMem.mem -> (Pointers.block, Pointers.offset)
    Types.prod -> Values.val0 Types.option **)
let load_value_of_type' ty m l =
  let { Types.fst = loc; Types.snd = ofs } = l in
  Csem.load_value_of_type ty m loc ofs

(** val exec_expr :
    Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr -> (Values.val0,
    Events.trace) Types.prod Errors.res **)
let rec exec_expr ge en m = function
| Csyntax.Expr (e', ty) ->
  (match e' with
   | Csyntax.Econst_int (sz, i) ->
     (match ty with
      | Csyntax.Tvoid ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
      | Csyntax.Tint (sz', x) ->
        (match AST.eq_intsize sz sz' with
         | Bool.True ->
           Errors.OK { Types.fst = (Values.Vint (sz, i)); Types.snd =
             Events.e0 }
         | Bool.False ->
           Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
      | Csyntax.Tpointer x ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
      | Csyntax.Tarray (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
      | Csyntax.Tfunction (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
      | Csyntax.Tstruct (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
      | Csyntax.Tunion (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
      | Csyntax.Tcomp_ptr x ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
   | Csyntax.Evar x ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def Errors.res0)
         (Obj.magic (exec_lvalue' ge en m e' ty)) (fun l tr ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic
             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
               (load_value_of_type' ty m l))) (fun v ->
           Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
   | Csyntax.Ederef x ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def Errors.res0)
         (Obj.magic (exec_lvalue' ge en m e' ty)) (fun l tr ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic
             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
               (load_value_of_type' ty m l))) (fun v ->
           Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
   | Csyntax.Eaddrof a ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def Errors.res0)
         (Obj.magic (exec_lvalue ge en m a)) (fun lo tr ->
         match ty with
         | Csyntax.Tvoid ->
           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
         | Csyntax.Tint (x, x0) ->
           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
         | Csyntax.Tpointer x ->
           let { Types.fst = loc; Types.snd = ofs } = lo in
           Obj.magic (Errors.OK { Types.fst = (Values.Vptr
             { Pointers.pblock = loc; Pointers.poff = ofs }); Types.snd =
             tr })
         | Csyntax.Tarray (x, x0) ->
           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
         | Csyntax.Tfunction (x, x0) ->
           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
         | Csyntax.Tstruct (x, x0) ->
           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
         | Csyntax.Tunion (x, x0) ->
           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
         | Csyntax.Tcomp_ptr x ->
           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))))
   | Csyntax.Eunop (op, a) ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def Errors.res0)
         (Obj.magic (exec_expr ge en m a)) (fun v1 tr ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic
             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
               (Csem.sem_unary_operation op v1 (Csyntax.typeof a))))
           (fun v -> Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
   | Csyntax.Ebinop (op, a1, a2) ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def Errors.res0)
         (Obj.magic (exec_expr ge en m a1)) (fun v1 tr1 ->
         Monad.m_bind2 (Monad.max_def Errors.res0)
           (Obj.magic (exec_expr ge en m a2)) (fun v2 tr2 ->
           Monad.m_bind0 (Monad.max_def Errors.res0)
             (Obj.magic
               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
                 (Csem.sem_binary_operation op v1 (Csyntax.typeof a1) v2
                   (Csyntax.typeof a2) m ty))) (fun v ->
             Obj.magic (Errors.OK { Types.fst = v; Types.snd =
               (Events.eapp tr1 tr2) })))))
   | Csyntax.Ecast (ty', a) ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def Errors.res0)
         (Obj.magic (exec_expr ge en m a)) (fun v tr ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (exec_cast m v (Csyntax.typeof a) ty')) (fun v' ->
           Obj.magic (Errors.OK { Types.fst = v'; Types.snd = tr }))))
   | Csyntax.Econdition (a1, a2, a3) ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def Errors.res0)
         (Obj.magic (exec_expr ge en m a1)) (fun v tr1 ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (exec_bool_of_val v (Csyntax.typeof a1))) (fun b ->
           Monad.m_bind2 (Monad.max_def Errors.res0)
             (match b with
              | Bool.True -> Obj.magic (exec_expr ge en m a2)
              | Bool.False -> Obj.magic (exec_expr ge en m a3))
             (fun v' tr2 ->
             Obj.magic (Errors.OK { Types.fst = v'; Types.snd =
               (Events.eapp tr1 tr2) })))))
   | Csyntax.Eandbool (a1, a2) ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def Errors.res0)
         (Obj.magic (exec_expr ge en m a1)) (fun v1 tr1 ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (exec_bool_of_val v1 (Csyntax.typeof a1))) (fun b1 ->
           match b1 with
           | Bool.True ->
             Monad.m_bind2 (Monad.max_def Errors.res0)
               (Obj.magic (exec_expr ge en m a2)) (fun v2 tr2 ->
               Monad.m_bind0 (Monad.max_def Errors.res0)
                 (Obj.magic (exec_bool_of_val v2 (Csyntax.typeof a2)))
                 (fun b2 ->
                 match Csem.cast_bool_to_target ty (Types.Some
                         (Values.of_bool b2)) with
                 | Types.None ->
                   Obj.magic (Errors.Error
                     (Errors.msg ErrorMessages.BadlyTypedTerm))
                 | Types.Some v20 ->
                   Obj.magic (Errors.OK { Types.fst = v20; Types.snd =
                     (Events.eapp tr1 tr2) })))
           | Bool.False ->
             (match Csem.cast_bool_to_target ty (Types.Some Values.vfalse) with
              | Types.None ->
                Obj.magic (Errors.Error
                  (Errors.msg ErrorMessages.BadlyTypedTerm))
              | Types.Some vfls ->
                Obj.magic (Errors.OK { Types.fst = vfls; Types.snd = tr1 })))))
   | Csyntax.Eorbool (a1, a2) ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def Errors.res0)
         (Obj.magic (exec_expr ge en m a1)) (fun v1 tr1 ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic (exec_bool_of_val v1 (Csyntax.typeof a1))) (fun b1 ->
           match b1 with
           | Bool.True ->
             (match Csem.cast_bool_to_target ty (Types.Some Values.vtrue) with
              | Types.None ->
                Obj.magic (Errors.Error
                  (Errors.msg ErrorMessages.BadlyTypedTerm))
              | Types.Some vtr ->
                Obj.magic (Errors.OK { Types.fst = vtr; Types.snd = tr1 }))
           | Bool.False ->
             Monad.m_bind2 (Monad.max_def Errors.res0)
               (Obj.magic (exec_expr ge en m a2)) (fun v2 tr2 ->
               Monad.m_bind0 (Monad.max_def Errors.res0)
                 (Obj.magic (exec_bool_of_val v2 (Csyntax.typeof a2)))
                 (fun b2 ->
                 match Csem.cast_bool_to_target ty (Types.Some
                         (Values.of_bool b2)) with
                 | Types.None ->
                   Obj.magic (Errors.Error
                     (Errors.msg ErrorMessages.BadlyTypedTerm))
                 | Types.Some v20 ->
                   Obj.magic (Errors.OK { Types.fst = v20; Types.snd =
                     (Events.eapp tr1 tr2) }))))))
   | Csyntax.Esizeof ty' ->
     (match ty with
      | Csyntax.Tvoid ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
      | Csyntax.Tint (sz, x) ->
        Errors.OK { Types.fst = (Values.Vint (sz,
          (AST.repr sz (Csyntax.sizeof ty')))); Types.snd = Events.e0 }
      | Csyntax.Tpointer x ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
      | Csyntax.Tarray (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
      | Csyntax.Tfunction (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
      | Csyntax.Tstruct (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
      | Csyntax.Tunion (x, x0) ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
      | Csyntax.Tcomp_ptr x ->
        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
   | Csyntax.Efield (x, x0) ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def Errors.res0)
         (Obj.magic (exec_lvalue' ge en m e' ty)) (fun l tr ->
         Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic
             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
               (load_value_of_type' ty m l))) (fun v ->
           Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
   | Csyntax.Ecost (l, a) ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def Errors.res0)
         (Obj.magic (exec_expr ge en m a)) (fun v tr ->
         Obj.magic (Errors.OK { Types.fst = v; Types.snd =
           (Events.eapp (Events.echarge l) tr) }))))
(** val exec_lvalue' :
    Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr_descr ->
    Csyntax.type0 -> ((Pointers.block, Pointers.offset) Types.prod,
    Events.trace) Types.prod Errors.res **)
and exec_lvalue' ge en m e' ty =
  match e' with
  | Csyntax.Econst_int (x, x0) ->
    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
  | Csyntax.Evar id ->
    (match Identifiers.lookup PreIdentifiers.SymbolTag en id with
     | Types.None ->
       Obj.magic
         (Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic
             (Errors.opt_to_res (List.Cons ((Errors.MSG
               ErrorMessages.UnknownIdentifier), (List.Cons ((Errors.CTX
               (PreIdentifiers.SymbolTag, id)), List.Nil))))
               (Globalenvs.find_symbol ge id))) (fun l ->
           Obj.magic (Errors.OK { Types.fst = { Types.fst = l; Types.snd =
             Pointers.zero_offset }; Types.snd = Events.e0 })))
     | Types.Some loc ->
       Errors.OK { Types.fst = { Types.fst = loc; Types.snd =
         Pointers.zero_offset }; Types.snd = Events.e0 })
  | Csyntax.Ederef a ->
    Obj.magic
      (Monad.m_bind2 (Monad.max_def Errors.res0)
        (Obj.magic (exec_expr ge en m a)) (fun v tr ->
        match v with
        | Values.Vundef ->
          Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
        | Values.Vint (x, x0) ->
          Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
        | Values.Vnull ->
          Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
        | Values.Vptr ptr ->
          Obj.magic (Errors.OK { Types.fst = { Types.fst =
            ptr.Pointers.pblock; Types.snd = ptr.Pointers.poff }; Types.snd =
            tr })))
  | Csyntax.Eaddrof x ->
    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
  | Csyntax.Eunop (x, x0) ->
    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
  | Csyntax.Ebinop (x, x0, x1) ->
    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
  | Csyntax.Ecast (x, x0) ->
    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
  | Csyntax.Econdition (x, x0, x1) ->
    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
  | Csyntax.Eandbool (x, x0) ->
    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
  | Csyntax.Eorbool (x, x0) ->
    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
  | Csyntax.Esizeof x ->
    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
  | Csyntax.Efield (a, i) ->
    (match Csyntax.typeof a with
     | Csyntax.Tvoid ->
       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     | Csyntax.Tint (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     | Csyntax.Tpointer x ->
       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     | Csyntax.Tarray (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     | Csyntax.Tfunction (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     | Csyntax.Tstruct (id, fList) ->
       Obj.magic
         (Monad.m_bind2 (Monad.max_def Errors.res0)
           (Obj.magic (exec_lvalue ge en m a)) (fun lofs tr ->
           Monad.m_bind0 (Monad.max_def Errors.res0)
             (Obj.magic (Csyntax.field_offset i fList)) (fun delta ->
             Obj.magic (Errors.OK { Types.fst = { Types.fst = lofs.Types.fst;
               Types.snd =
               (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
                 lofs.Types.snd (AST.repr AST.I16 delta)) }; Types.snd =
               tr }))))
     | Csyntax.Tunion (id, fList) ->
       Obj.magic
         (Monad.m_bind2 (Monad.max_def Errors.res0)
           (Obj.magic (exec_lvalue ge en m a)) (fun lofs tr ->
           Obj.magic (Errors.OK { Types.fst = lofs; Types.snd = tr })))
     | Csyntax.Tcomp_ptr x ->
       Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))
  | Csyntax.Ecost (x, x0) ->
    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
(** val exec_lvalue :
    Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr -> ((Pointers.block,
    Pointers.offset) Types.prod, Events.trace) Types.prod Errors.res **)
and exec_lvalue ge en m = function
| Csyntax.Expr (e', ty) -> exec_lvalue' ge en m e' ty

(** val exec_exprlist :
    Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr List.list ->
    (Values.val0 List.list, Events.trace) Types.prod Errors.res **)
let rec exec_exprlist ge e m = function
| List.Nil -> Errors.OK { Types.fst = List.Nil; Types.snd = Events.e0 }
| List.Cons (e1, es) ->
  Obj.magic
    (Monad.m_bind2 (Monad.max_def Errors.res0)
      (Obj.magic (exec_expr ge e m e1)) (fun v tr1 ->
      Monad.m_bind2 (Monad.max_def Errors.res0)
        (Obj.magic (exec_exprlist ge e m es)) (fun vs tr2 ->
        Obj.magic (Errors.OK { Types.fst = (List.Cons (v, vs)); Types.snd =
          (Events.eapp tr1 tr2) }))))

(** val exec_alloc_variables :
    Csem.env -> GenMem.mem -> (AST.ident, Csyntax.type0) Types.prod List.list
    -> (Csem.env, GenMem.mem) Types.prod **)
let rec exec_alloc_variables en m = function
| List.Nil -> { Types.fst = en; Types.snd = m }
| List.Cons (h, vars) ->
  let { Types.fst = id; Types.snd = ty } = h in
  let { Types.fst = m1; Types.snd = b1 } =
    GenMem.alloc m (Z.z_of_nat Nat.O) (Z.z_of_nat (Csyntax.sizeof ty))
  in
  exec_alloc_variables (Identifiers.add PreIdentifiers.SymbolTag en id b1) m1
    vars

(** val exec_bind_parameters :
    Csem.env -> GenMem.mem -> (AST.ident, Csyntax.type0) Types.prod List.list
    -> Values.val0 List.list -> GenMem.mem Errors.res **)
let rec exec_bind_parameters e m params vs =
  match params with
  | List.Nil ->
    (match vs with
     | List.Nil -> Errors.OK m
     | List.Cons (x, x0) ->
       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters))
  | List.Cons (idty, params') ->
    let { Types.fst = id; Types.snd = ty } = idty in
    (match vs with
     | List.Nil ->
       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)
     | List.Cons (v1, vl) ->
       Obj.magic
         (Monad.m_bind0 (Monad.max_def Errors.res0)
           (Obj.magic
             (Errors.opt_to_res (List.Cons ((Errors.MSG
               ErrorMessages.UnknownIdentifier), (List.Cons ((Errors.CTX
               (PreIdentifiers.SymbolTag, id)), List.Nil))))
               (Identifiers.lookup PreIdentifiers.SymbolTag e id))) (fun b ->
           Monad.m_bind0 (Monad.max_def Errors.res0)
             (Obj.magic
               (Errors.opt_to_res (List.Cons ((Errors.MSG
                 ErrorMessages.FailedStore), (List.Cons ((Errors.CTX
                 (PreIdentifiers.SymbolTag, id)), List.Nil))))
                 (Csem.store_value_of_type ty m b Pointers.zero_offset v1)))
             (fun m1 -> Obj.magic (exec_bind_parameters e m1 params' vl)))))

(** val is_is_call_cont : Csem.cont -> (__, __) Types.sum **)
let rec is_is_call_cont = function
| Csem.Kstop -> Types.Inl __
| Csem.Kseq (x, x0) -> Types.Inr __
| Csem.Kwhile (x, x0, x1) -> Types.Inr __
| Csem.Kdowhile (x, x0, x1) -> Types.Inr __
| Csem.Kfor2 (x, x0, x1, x2) -> Types.Inr __
| Csem.Kfor3 (x, x0, x1, x2) -> Types.Inr __
| Csem.Kswitch x -> Types.Inr __
| Csem.Kcall (x, x0, x1, x2) -> Types.Inl __

(** val is_Sskip : Csyntax.statement -> (__, __) Types.sum **)
let is_Sskip = function
| Csyntax.Sskip -> Types.Inl __
| Csyntax.Sassign (x, x0) -> Types.Inr __
| Csyntax.Scall (x, x0, x1) -> Types.Inr __
| Csyntax.Ssequence (x, x0) -> Types.Inr __
| Csyntax.Sifthenelse (x, x0, x1) -> Types.Inr __
| Csyntax.Swhile (x, x0) -> Types.Inr __
| Csyntax.Sdowhile (x, x0) -> Types.Inr __
| Csyntax.Sfor (x, x0, x1, x2) -> Types.Inr __
| Csyntax.Sbreak -> Types.Inr __
| Csyntax.Scontinue -> Types.Inr __
| Csyntax.Sreturn x -> Types.Inr __
| Csyntax.Sswitch (x, x0) -> Types.Inr __
| Csyntax.Slabel (x, x0) -> Types.Inr __
| Csyntax.Sgoto x -> Types.Inr __
| Csyntax.Scost (x, x0) -> Types.Inr __

(** val store_value_of_type' :
    Csyntax.type0 -> GenMem.mem -> (Pointers.block, Pointers.offset)
    Types.prod -> Values.val0 -> GenMem.mem Types.option **)
let store_value_of_type' ty m l v =
  let { Types.fst = loc; Types.snd = ofs } = l in
  Csem.store_value_of_type ty m loc ofs v

(** val exec_step :
    Csem.genv -> Csem.state -> (IO.io_out, IO.io_in, (Events.trace,
    Csem.state) Types.prod) IOMonad.iO **)
let rec exec_step ge = function
| Csem.State (f, s, k, e, m) ->
  (match s with
   | Csyntax.Sskip ->
     (match k with
      | Csem.Kstop ->
        (match f.Csyntax.fn_return with
         | Csyntax.Tvoid ->
           IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Returnstate
             (Values.Vundef, k,
             (GenMem.free_list m (Csem.blocks_of_env e)))) }
         | Csyntax.Tint (x, x0) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
         | Csyntax.Tpointer x ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
         | Csyntax.Tarray (x, x0) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
         | Csyntax.Tfunction (x, x0) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
         | Csyntax.Tstruct (x, x0) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
         | Csyntax.Tunion (x, x0) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
         | Csyntax.Tcomp_ptr x ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState))
      | Csem.Kseq (s0, k') ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s0, k',
          e, m)) }
      | Csem.Kwhile (a, s', k') ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
          (Csyntax.Swhile (a, s')), k', e, m)) }
      | Csem.Kdowhile (a, s', k') ->
        Obj.magic
          (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
            (let x = IOMonad.err_to_io (exec_expr ge e m a) in Obj.magic x)
            (fun v tr ->
            Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
              (Obj.magic
                (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a))))
              (fun b ->
              match b with
              | Bool.True ->
                Obj.magic
                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
                    (Csyntax.Sdowhile (a, s')), k', e, m)) })
              | Bool.False ->
                Obj.magic
                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
                    Csyntax.Sskip, k', e, m)) }))))
      | Csem.Kfor2 (a2, a3, s', k') ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, a3,
          (Csem.Kfor3 (a2, a3, s', k')), e, m)) }
      | Csem.Kfor3 (a2, a3, s', k') ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
          (Csyntax.Sfor (Csyntax.Sskip, a2, a3, s')), k', e, m)) }
      | Csem.Kswitch k' ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
          Csyntax.Sskip, k', e, m)) }
      | Csem.Kcall (x, x0, x1, x2) ->
        (match f.Csyntax.fn_return with
         | Csyntax.Tvoid ->
           IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Returnstate
             (Values.Vundef, k,
             (GenMem.free_list m (Csem.blocks_of_env e)))) }
         | Csyntax.Tint (x3, x4) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
         | Csyntax.Tpointer x3 ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
         | Csyntax.Tarray (x3, x4) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
         | Csyntax.Tfunction (x3, x4) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
         | Csyntax.Tstruct (x3, x4) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
         | Csyntax.Tunion (x3, x4) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
         | Csyntax.Tcomp_ptr x3 ->
           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)))
   | Csyntax.Sassign (a1, a2) ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
         (let x = IOMonad.err_to_io (exec_lvalue ge e m a1) in Obj.magic x)
         (fun l tr1 ->
         Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
           (let x = IOMonad.err_to_io (exec_expr ge e m a2) in Obj.magic x)
           (fun v2 tr2 ->
           Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
             (Obj.magic
               (IOMonad.opt_to_io (Errors.msg ErrorMessages.FailedStore)
                 (store_value_of_type' (Csyntax.typeof a1) m l v2)))
             (fun m' ->
             Obj.magic
               (IO.ret { Types.fst = (Events.eapp tr1 tr2); Types.snd =
                 (Csem.State (f, Csyntax.Sskip, k, e, m')) })))))
   | Csyntax.Scall (lhs, a, al) ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
         (let x = IOMonad.err_to_io (exec_expr ge e m a) in Obj.magic x)
         (fun vf tr2 ->
         Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
           (let x = IOMonad.err_to_io (exec_exprlist ge e m al) in
           Obj.magic x) (fun vargs tr3 ->
           Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
             (Obj.magic
               (IOMonad.opt_to_io (Errors.msg ErrorMessages.BadFunctionValue)
                 (Globalenvs.find_funct_id ge vf))) (fun fd id ->
             Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
               (Obj.magic
                 (IOMonad.err_to_io
                   (TypeComparison.assert_type_eq (Csyntax.type_of_fundef fd)
                     (Csem.fun_typeof a)))) (fun _ ->
               match lhs with
               | Types.None ->
                 Obj.magic
                   (IO.ret { Types.fst = (Events.eapp tr2 tr3); Types.snd =
                     (Csem.Callstate (id, fd, vargs, (Csem.Kcall (Types.None,
                     f, e, k)), m)) })
               | Types.Some lhs' ->
                 Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
                   (let x = IOMonad.err_to_io (exec_lvalue ge e m lhs') in
                   Obj.magic x) (fun locofs tr1 ->
                   Obj.magic
                     (IO.ret { Types.fst =
                       (Events.eapp tr1 (Events.eapp tr2 tr3)); Types.snd =
                       (Csem.Callstate (id, fd, vargs, (Csem.Kcall
                       ((Types.Some { Types.fst = locofs; Types.snd =
                       (Csyntax.typeof lhs') }), f, e, k)), m)) })))))))
   | Csyntax.Ssequence (s1, s2) ->
     IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s1,
       (Csem.Kseq (s2, k)), e, m)) }
   | Csyntax.Sifthenelse (a, s1, s2) ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
         (let x = IOMonad.err_to_io (exec_expr ge e m a) in Obj.magic x)
         (fun v tr ->
         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
           (Obj.magic
             (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a))))
           (fun b ->
           Obj.magic
             (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
               (match b with
                | Bool.True -> s1
                | Bool.False -> s2), k, e, m)) }))))
   | Csyntax.Swhile (a, s') ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
         (let x = IOMonad.err_to_io (exec_expr ge e m a) in Obj.magic x)
         (fun v tr ->
         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
           (Obj.magic
             (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a))))
           (fun b ->
           Obj.magic
             (IO.ret { Types.fst = tr; Types.snd =
               (match b with
                | Bool.True ->
                  Csem.State (f, s', (Csem.Kwhile (a, s', k)), e, m)
                | Bool.False -> Csem.State (f, Csyntax.Sskip, k, e, m)) }))))
   | Csyntax.Sdowhile (a, s') ->
     IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s',
       (Csem.Kdowhile (a, s', k)), e, m)) }
   | Csyntax.Sfor (a1, a2, a3, s') ->
     (match is_Sskip a1 with
      | Types.Inl _ ->
        Obj.magic
          (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
            (let x = IOMonad.err_to_io (exec_expr ge e m a2) in Obj.magic x)
            (fun v tr ->
            Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
              (Obj.magic
                (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a2))))
              (fun b ->
              Obj.magic
                (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
                  (match b with
                   | Bool.True -> s'
                   | Bool.False -> Csyntax.Sskip),
                  (match b with
                   | Bool.True -> Csem.Kfor2 (a2, a3, s', k)
                   | Bool.False -> k), e, m)) }))))
      | Types.Inr _ ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, a1,
          (Csem.Kseq ((Csyntax.Sfor (Csyntax.Sskip, a2, a3, s')), k)), e,
          m)) })
   | Csyntax.Sbreak ->
     (match k with
      | Csem.Kstop -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
      | Csem.Kseq (s', k') ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
          Csyntax.Sbreak, k', e, m)) }
      | Csem.Kwhile (a, s', k') ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
          Csyntax.Sskip, k', e, m)) }
      | Csem.Kdowhile (a, s', k') ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
          Csyntax.Sskip, k', e, m)) }
      | Csem.Kfor2 (a2, a3, s', k') ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
          Csyntax.Sskip, k', e, m)) }
      | Csem.Kfor3 (x, x0, x1, x2) ->
        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
      | Csem.Kswitch k' ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
          Csyntax.Sskip, k', e, m)) }
      | Csem.Kcall (x, x0, x1, x2) ->
        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState))
   | Csyntax.Scontinue ->
     (match k with
      | Csem.Kstop -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
      | Csem.Kseq (s', k') ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
          Csyntax.Scontinue, k', e, m)) }
      | Csem.Kwhile (a, s', k') ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
          (Csyntax.Swhile (a, s')), k', e, m)) }
      | Csem.Kdowhile (a, s', k') ->
        Obj.magic
          (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
            (let x = IOMonad.err_to_io (exec_expr ge e m a) in Obj.magic x)
            (fun v tr ->
            Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
              (Obj.magic
                (IOMonad.err_to_io (exec_bool_of_val v (Csyntax.typeof a))))
              (fun b ->
              match b with
              | Bool.True ->
                Obj.magic
                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
                    (Csyntax.Sdowhile (a, s')), k', e, m)) })
              | Bool.False ->
                Obj.magic
                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
                    Csyntax.Sskip, k', e, m)) }))))
      | Csem.Kfor2 (a2, a3, s', k') ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, a3,
          (Csem.Kfor3 (a2, a3, s', k')), e, m)) }
      | Csem.Kfor3 (x, x0, x1, x2) ->
        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
      | Csem.Kswitch k' ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
          Csyntax.Scontinue, k', e, m)) }
      | Csem.Kcall (x, x0, x1, x2) ->
        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState))
   | Csyntax.Sreturn a_opt ->
     (match a_opt with
      | Types.None ->
        (match f.Csyntax.fn_return with
         | Csyntax.Tvoid ->
           IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Returnstate
             (Values.Vundef, (Csem.call_cont k),
             (GenMem.free_list m (Csem.blocks_of_env e)))) }
         | Csyntax.Tint (x, x0) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
         | Csyntax.Tpointer x ->
           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
         | Csyntax.Tarray (x, x0) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
         | Csyntax.Tfunction (x, x0) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
         | Csyntax.Tstruct (x, x0) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
         | Csyntax.Tunion (x, x0) ->
           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
         | Csyntax.Tcomp_ptr x ->
           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
      | Types.Some a ->
        (match TypeComparison.type_eq_dec f.Csyntax.fn_return Csyntax.Tvoid with
         | Types.Inl _ ->
           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
         | Types.Inr _ ->
           Obj.magic
             (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
               (let x = IOMonad.err_to_io (exec_expr ge e m a) in
               Obj.magic x) (fun v tr ->
               Obj.magic
                 (IO.ret { Types.fst = tr; Types.snd = (Csem.Returnstate (v,
                   (Csem.call_cont k),
                   (GenMem.free_list m (Csem.blocks_of_env e)))) })))))
   | Csyntax.Sswitch (a, sl) ->
     Obj.magic
       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
         (let x = IOMonad.err_to_io (exec_expr ge e m a) in Obj.magic x)
         (fun v tr ->
         match v with
         | Values.Vundef ->
           Obj.magic (IOMonad.Wrong (Errors.msg ErrorMessages.TypeMismatch))
         | Values.Vint (sz, n) ->
           (match Csyntax.typeof a with
            | Csyntax.Tvoid ->
              Obj.magic (IOMonad.Wrong
                (Errors.msg ErrorMessages.TypeMismatch))
            | Csyntax.Tint (sz', x) ->
              (match TypeComparison.sz_eq_dec sz sz' with
               | Types.Inl _ ->
                 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
                   (Obj.magic
                     (IOMonad.opt_to_io
                       (Errors.msg ErrorMessages.TypeMismatch)
                       (Csem.select_switch sz n sl))) (fun sl' ->
                   Obj.magic
                     (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
                       (Csem.seq_of_labeled_statement sl'), (Csem.Kswitch k),
                       e, m)) }))
               | Types.Inr _ ->
                 Obj.magic (IOMonad.Wrong
                   (Errors.msg ErrorMessages.TypeMismatch)))
            | Csyntax.Tpointer x ->
              Obj.magic (IOMonad.Wrong
                (Errors.msg ErrorMessages.TypeMismatch))
            | Csyntax.Tarray (x, x0) ->
              Obj.magic (IOMonad.Wrong
                (Errors.msg ErrorMessages.TypeMismatch))
            | Csyntax.Tfunction (x, x0) ->
              Obj.magic (IOMonad.Wrong
                (Errors.msg ErrorMessages.TypeMismatch))
            | Csyntax.Tstruct (x, x0) ->
              Obj.magic (IOMonad.Wrong
                (Errors.msg ErrorMessages.TypeMismatch))
            | Csyntax.Tunion (x, x0) ->
              Obj.magic (IOMonad.Wrong
                (Errors.msg ErrorMessages.TypeMismatch))
            | Csyntax.Tcomp_ptr x ->
              Obj.magic (IOMonad.Wrong
                (Errors.msg ErrorMessages.TypeMismatch)))
         | Values.Vnull ->
           Obj.magic (IOMonad.Wrong (Errors.msg ErrorMessages.TypeMismatch))
         | Values.Vptr x ->
           Obj.magic (IOMonad.Wrong (Errors.msg ErrorMessages.TypeMismatch))))
   | Csyntax.Slabel (lbl, s') ->
     IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s', k, e,
       m)) }
   | Csyntax.Sgoto lbl ->
     (match Csem.find_label lbl f.Csyntax.fn_body (Csem.call_cont k) with
      | Types.None ->
        IOMonad.Wrong (List.Cons ((Errors.MSG ErrorMessages.UnknownLabel),
          (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, lbl)),
          List.Nil))))
      | Types.Some sk' ->
        let { Types.fst = s'; Types.snd = k' } = sk' in
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s', k',
          e, m)) })
   | Csyntax.Scost (lbl, s') ->
     IO.ret { Types.fst = (Events.echarge lbl); Types.snd = (Csem.State (f,
       s', k, e, m)) })
| Csem.Callstate (x, f0, vargs, k, m) ->
  (match f0 with
   | Csyntax.CL_Internal f ->
     let { Types.fst = e; Types.snd = m1 } =
       exec_alloc_variables Csem.empty_env m
         (List.append f.Csyntax.fn_params f.Csyntax.fn_vars)
     in
     Obj.magic
       (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
         (let x0 =
            IOMonad.err_to_io
              (exec_bind_parameters e m1 f.Csyntax.fn_params vargs)
          in
         Obj.magic x0) (fun m2 ->
         Obj.magic
           (IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
             f.Csyntax.fn_body, k, e, m2)) })))
   | Csyntax.CL_External (f, argtys, retty) ->
     Obj.magic
       (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
         (let x0 =
            IOMonad.err_to_io
              (IO.check_eventval_list vargs
                (Csyntax.typlist_of_typelist argtys))
          in
         Obj.magic x0) (fun evargs ->
         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
           (Obj.magic
             (IO.do_io f evargs
               (AST.proj_sig_res (Csyntax.signature_of_type argtys retty))))
           (fun evres ->
           Obj.magic
             (IO.ret { Types.fst =
               (Events.eextcall f evargs
                 (IO.mk_eventval
                   (AST.proj_sig_res
                     (Csyntax.signature_of_type argtys retty)) evres));
               Types.snd = (Csem.Returnstate
               ((IO.mk_val
                  (AST.proj_sig_res (Csyntax.signature_of_type argtys retty))
                  evres), k, m)) })))))
| Csem.Returnstate (res, k, m) ->
  (match k with
   | Csem.Kstop ->
     (match res with
      | Values.Vundef ->
        IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
      | Values.Vint (sz, r) ->
        (match sz with
         | AST.I8 ->
           (fun x -> IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
         | AST.I16 ->
           (fun x -> IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
         | AST.I32 ->
           (fun r0 ->
             IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Finalstate
               r0) })) r
      | Values.Vnull ->
        IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
      | Values.Vptr x ->
        IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
   | Csem.Kseq (x, x0) ->
     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
   | Csem.Kwhile (x, x0, x1) ->
     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
   | Csem.Kdowhile (x, x0, x1) ->
     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
   | Csem.Kfor2 (x, x0, x1, x2) ->
     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
   | Csem.Kfor3 (x, x0, x1, x2) ->
     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
   | Csem.Kswitch x -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
   | Csem.Kcall (r, f, e, k') ->
     (match r with
      | Types.None ->
        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
          Csyntax.Sskip, k', e, m)) }
      | Types.Some r' ->
        let { Types.fst = l; Types.snd = ty } = r' in
        Obj.magic
          (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
            (Obj.magic
              (IOMonad.opt_to_io (Errors.msg ErrorMessages.FailedStore)
                (store_value_of_type' ty m l res))) (fun m' ->
            Obj.magic
              (IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
                Csyntax.Sskip, k', e, m')) })))))
| Csem.Finalstate r -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)

(** val make_global : Csyntax.clight_program -> Csem.genv **)
let make_global p =
  Globalenvs.globalenv Types.fst p

(** val make_initial_state :
    Csyntax.clight_program -> Csem.state Errors.res **)
let rec make_initial_state p =
  let ge = make_global p in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (Globalenvs.init_mem Types.fst p)) (fun m0 ->
      Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic
          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
        Monad.m_bind0 (Monad.max_def Errors.res0)
          (Obj.magic
            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
              (Globalenvs.find_funct_ptr ge b))) (fun f ->
          Obj.magic (Errors.OK (Csem.Callstate (p.AST.prog_main, f, List.Nil,
            Csem.Kstop, m0)))))))

(** val is_final : Csem.state -> Integers.int Types.option **)
let rec is_final = function
| Csem.State (x, x0, x1, x2, x3) -> Types.None
| Csem.Callstate (x, x0, x1, x2, x3) -> Types.None
| Csem.Returnstate (x, x0, x1) -> Types.None
| Csem.Finalstate r -> Types.Some r

(** val is_final_state :
    Csem.state -> (Integers.int Types.sig0, __) Types.sum **)
let is_final_state st =
  Csem.state_rect_Type0 (fun f s k e m -> Types.Inr __) (fun vf f l k m ->
    Types.Inr __) (fun v k m -> Types.Inr __) (fun r -> Types.Inl r) st

(** val exec_steps :
    Nat.nat -> Csem.genv -> Csem.state -> (IO.io_out, IO.io_in,
    (Events.trace, Csem.state) Types.prod) IOMonad.iO **)
let rec exec_steps n ge s =
  match is_final_state s with
  | Types.Inl x -> IO.ret { Types.fst = Events.e0; Types.snd = s }
  | Types.Inr _ ->
    (match n with
     | Nat.O -> IO.ret { Types.fst = Events.e0; Types.snd = s }
     | Nat.S n' ->
       Obj.magic
         (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
           (Obj.magic (exec_step ge s)) (fun t s' ->
           Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
             (Obj.magic (exec_steps n' ge s')) (fun t' s'' ->
             Obj.magic
               (IO.ret { Types.fst = (Events.eapp t t'); Types.snd = s'' })))))

(** val clight_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
let clight_exec =
  { SmallstepExec.is_final = (fun x -> Obj.magic is_final);
    SmallstepExec.step = (Obj.magic exec_step) }

(** val clight_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
let clight_fullexec =
  { SmallstepExec.es1 = clight_exec; SmallstepExec.make_global =
    (Obj.magic make_global); SmallstepExec.make_initial_state =
    (Obj.magic make_initial_state) }