extracted/cexec.ml

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