extracted/rTLabs_semantics.ml

   1 open Preamble
   2
   3 open Bool
   4
   5 open Relations
   6
   7 open Nat
   8
   9 open Hints_declaration
  10
  11 open Core_notation
  12
  13 open Pts
  14
  15 open Logic
  16
  17 open Types
  18
  19 open List
  20
  21 open ErrorMessages
  22
  23 open Option
  24
  25 open Setoids
  26
  27 open Monad
  28
  29 open Jmeq
  30
  31 open Russell
  32
  33 open Positive
  34
  35 open PreIdentifiers
  36
  37 open Errors
  38
  39 open Extra_bool
  40
  41 open Coqlib
  42
  43 open Values
  44
  45 open FrontEndVal
  46
  47 open Hide
  48
  49 open ByteValues
  50
  51 open Division
  52
  53 open Z
  54
  55 open BitVectorZ
  56
  57 open Pointers
  58
  59 open GenMem
  60
  61 open FrontEndMem
  62
  63 open Proper
  64
  65 open PositiveMap
  66
  67 open Deqsets
  68
  69 open Extralib
  70
  71 open Lists
  72
  73 open Identifiers
  74
  75 open Exp
  76
  77 open Arithmetic
  78
  79 open Vector
  80
  81 open Div_and_mod
  82
  83 open Util
  84
  85 open FoldStuff
  86
  87 open BitVector
  88
  89 open Extranat
  90
  91 open Integers
  92
  93 open AST
  94
  95 open Globalenvs
  96
  97 open CostLabel
  98
  99 open Events
 100
 101 open IOMonad
 102
 103 open IO
 104
 105 open SmallstepExec
 106
 107 open BitVectorTrie
 108
 109 open Graphs
 110
 111 open Order
 112
 113 open Registers
 114
 115 open FrontEndOps
 116
 117 open RTLabs_syntax
 118
 119 type genv = RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t
 120
 121 type frame = { func : RTLabs_syntax.internal_function;
 122                locals : Values.val0 Registers.register_env;
 123                next : Graphs.label; sp : Pointers.block;
 124                retdst : Registers.register Types.option }
 125
 126 (** val frame_rect_Type4 :
 127     (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
 128     Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
 129     -> 'a1) -> frame -> 'a1 **)
 130 let rec frame_rect_Type4 h_mk_frame x_23982 =
 131   let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
 132     retdst0 } = x_23982
 133   in
 134   h_mk_frame func0 locals0 next0 __ sp0 retdst0
 135
 136 (** val frame_rect_Type5 :
 137     (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
 138     Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
 139     -> 'a1) -> frame -> 'a1 **)
 140 let rec frame_rect_Type5 h_mk_frame x_23984 =
 141   let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
 142     retdst0 } = x_23984
 143   in
 144   h_mk_frame func0 locals0 next0 __ sp0 retdst0
 145
 146 (** val frame_rect_Type3 :
 147     (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
 148     Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
 149     -> 'a1) -> frame -> 'a1 **)
 150 let rec frame_rect_Type3 h_mk_frame x_23986 =
 151   let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
 152     retdst0 } = x_23986
 153   in
 154   h_mk_frame func0 locals0 next0 __ sp0 retdst0
 155
 156 (** val frame_rect_Type2 :
 157     (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
 158     Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
 159     -> 'a1) -> frame -> 'a1 **)
 160 let rec frame_rect_Type2 h_mk_frame x_23988 =
 161   let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
 162     retdst0 } = x_23988
 163   in
 164   h_mk_frame func0 locals0 next0 __ sp0 retdst0
 165
 166 (** val frame_rect_Type1 :
 167     (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
 168     Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
 169     -> 'a1) -> frame -> 'a1 **)
 170 let rec frame_rect_Type1 h_mk_frame x_23990 =
 171   let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
 172     retdst0 } = x_23990
 173   in
 174   h_mk_frame func0 locals0 next0 __ sp0 retdst0
 175
 176 (** val frame_rect_Type0 :
 177     (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
 178     Graphs.label -> __ -> Pointers.block -> Registers.register Types.option
 179     -> 'a1) -> frame -> 'a1 **)
 180 let rec frame_rect_Type0 h_mk_frame x_23992 =
 181   let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
 182     retdst0 } = x_23992
 183   in
 184   h_mk_frame func0 locals0 next0 __ sp0 retdst0
 185
 186 (** val func : frame -> RTLabs_syntax.internal_function **)
 187 let rec func xxx =
 188   xxx.func
 189
 190 (** val locals : frame -> Values.val0 Registers.register_env **)
 191 let rec locals xxx =
 192   xxx.locals
 193
 194 (** val next : frame -> Graphs.label **)
 195 let rec next xxx =
 196   xxx.next
 197
 198 (** val sp : frame -> Pointers.block **)
 199 let rec sp xxx =
 200   xxx.sp
 201
 202 (** val retdst : frame -> Registers.register Types.option **)
 203 let rec retdst xxx =
 204   xxx.retdst
 205
 206 (** val frame_inv_rect_Type4 :
 207     frame -> (RTLabs_syntax.internal_function -> Values.val0
 208     Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
 209     Registers.register Types.option -> __ -> 'a1) -> 'a1 **)
 210 let frame_inv_rect_Type4 hterm h1 =
 211   let hcut = frame_rect_Type4 h1 hterm in hcut __
 212
 213 (** val frame_inv_rect_Type3 :
 214     frame -> (RTLabs_syntax.internal_function -> Values.val0
 215     Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
 216     Registers.register Types.option -> __ -> 'a1) -> 'a1 **)
 217 let frame_inv_rect_Type3 hterm h1 =
 218   let hcut = frame_rect_Type3 h1 hterm in hcut __
 219
 220 (** val frame_inv_rect_Type2 :
 221     frame -> (RTLabs_syntax.internal_function -> Values.val0
 222     Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
 223     Registers.register Types.option -> __ -> 'a1) -> 'a1 **)
 224 let frame_inv_rect_Type2 hterm h1 =
 225   let hcut = frame_rect_Type2 h1 hterm in hcut __
 226
 227 (** val frame_inv_rect_Type1 :
 228     frame -> (RTLabs_syntax.internal_function -> Values.val0
 229     Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
 230     Registers.register Types.option -> __ -> 'a1) -> 'a1 **)
 231 let frame_inv_rect_Type1 hterm h1 =
 232   let hcut = frame_rect_Type1 h1 hterm in hcut __
 233
 234 (** val frame_inv_rect_Type0 :
 235     frame -> (RTLabs_syntax.internal_function -> Values.val0
 236     Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
 237     Registers.register Types.option -> __ -> 'a1) -> 'a1 **)
 238 let frame_inv_rect_Type0 hterm h1 =
 239   let hcut = frame_rect_Type0 h1 hterm in hcut __
 240
 241 (** val frame_jmdiscr : frame -> frame -> __ **)
 242 let frame_jmdiscr x y =
 243   Logic.eq_rect_Type2 x
 244     (let { func = a0; locals = a1; next = a2; sp = a4; retdst = a5 } = x in
 245     Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
 246
 247 (** val adv : Graphs.label -> frame -> frame **)
 248 let adv l f =
 249   { func = f.func; locals = f.locals; next = l; sp = f.sp; retdst =
 250     f.retdst }
 251
 252 type state =
 253 | State of frame * frame List.list * GenMem.mem
 254 | Callstate of AST.ident * RTLabs_syntax.internal_function AST.fundef
 255    * Values.val0 List.list * Registers.register Types.option
 256    * frame List.list * GenMem.mem
 257 | Returnstate of Values.val0 Types.option * Registers.register Types.option
 258    * frame List.list * GenMem.mem
 259 | Finalstate of Integers.int
 260
 261 (** val state_rect_Type4 :
 262     (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
 263     RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 264     Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1)
 265     -> (Values.val0 Types.option -> Registers.register Types.option -> frame
 266     List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
 267 let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
 268 | State (f, fs, m) -> h_State f fs m
 269 | Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m
 270 | Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m
 271 | Finalstate r -> h_Finalstate r
 272
 273 (** val state_rect_Type5 :
 274     (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
 275     RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 276     Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1)
 277     -> (Values.val0 Types.option -> Registers.register Types.option -> frame
 278     List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
 279 let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
 280 | State (f, fs, m) -> h_State f fs m
 281 | Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m
 282 | Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m
 283 | Finalstate r -> h_Finalstate r
 284
 285 (** val state_rect_Type3 :
 286     (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
 287     RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 288     Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1)
 289     -> (Values.val0 Types.option -> Registers.register Types.option -> frame
 290     List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
 291 let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
 292 | State (f, fs, m) -> h_State f fs m
 293 | Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m
 294 | Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m
 295 | Finalstate r -> h_Finalstate r
 296
 297 (** val state_rect_Type2 :
 298     (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
 299     RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 300     Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1)
 301     -> (Values.val0 Types.option -> Registers.register Types.option -> frame
 302     List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
 303 let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
 304 | State (f, fs, m) -> h_State f fs m
 305 | Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m
 306 | Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m
 307 | Finalstate r -> h_Finalstate r
 308
 309 (** val state_rect_Type1 :
 310     (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
 311     RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 312     Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1)
 313     -> (Values.val0 Types.option -> Registers.register Types.option -> frame
 314     List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
 315 let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
 316 | State (f, fs, m) -> h_State f fs m
 317 | Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m
 318 | Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m
 319 | Finalstate r -> h_Finalstate r
 320
 321 (** val state_rect_Type0 :
 322     (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
 323     RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 324     Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1)
 325     -> (Values.val0 Types.option -> Registers.register Types.option -> frame
 326     List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
 327 let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
 328 | State (f, fs, m) -> h_State f fs m
 329 | Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m
 330 | Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m
 331 | Finalstate r -> h_Finalstate r
 332
 333 (** val state_inv_rect_Type4 :
 334     state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 335     (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
 336     List.list -> Registers.register Types.option -> frame List.list ->
 337     GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option ->
 338     Registers.register Types.option -> frame List.list -> GenMem.mem -> __ ->
 339     'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
 340 let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
 341   let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __
 342
 343 (** val state_inv_rect_Type3 :
 344     state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 345     (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
 346     List.list -> Registers.register Types.option -> frame List.list ->
 347     GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option ->
 348     Registers.register Types.option -> frame List.list -> GenMem.mem -> __ ->
 349     'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
 350 let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
 351   let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __
 352
 353 (** val state_inv_rect_Type2 :
 354     state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 355     (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
 356     List.list -> Registers.register Types.option -> frame List.list ->
 357     GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option ->
 358     Registers.register Types.option -> frame List.list -> GenMem.mem -> __ ->
 359     'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
 360 let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
 361   let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __
 362
 363 (** val state_inv_rect_Type1 :
 364     state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 365     (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
 366     List.list -> Registers.register Types.option -> frame List.list ->
 367     GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option ->
 368     Registers.register Types.option -> frame List.list -> GenMem.mem -> __ ->
 369     'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
 370 let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
 371   let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __
 372
 373 (** val state_inv_rect_Type0 :
 374     state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
 375     (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
 376     List.list -> Registers.register Types.option -> frame List.list ->
 377     GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option ->
 378     Registers.register Types.option -> frame List.list -> GenMem.mem -> __ ->
 379     'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
 380 let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
 381   let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __
 382
 383 (** val state_jmdiscr : state -> state -> __ **)
 384 let state_jmdiscr x y =
 385   Logic.eq_rect_Type2 x
 386     (match x with
 387      | State (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 388      | Callstate (a0, a1, a2, a3, a4, a5) ->
 389        Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
 390      | Returnstate (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 391      | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
 392
 393 (** val build_state :
 394     frame -> frame List.list -> GenMem.mem -> Graphs.label -> state **)
 395 let build_state f fs m n =
 396   State ((adv n f), fs, m)
 397
 398 (** val next_instruction : frame -> RTLabs_syntax.statement **)
 399 let next_instruction f =
 400   Identifiers.lookup_present PreIdentifiers.LabelTag
 401     f.func.RTLabs_syntax.f_graph f.next
 402
 403 (** val init_locals :
 404     (Registers.register, AST.typ) Types.prod List.list -> Values.val0
 405     Registers.register_env **)
 406 let init_locals =
 407   List.foldr (fun idt en ->
 408     let { Types.fst = id; Types.snd = ty } = idt in
 409     Identifiers.add PreIdentifiers.RegisterTag en id Values.Vundef)
 410     (Identifiers.empty_map PreIdentifiers.RegisterTag)
 411
 412 (** val reg_store :
 413     PreIdentifiers.identifier -> Values.val0 -> Values.val0
 414     Identifiers.identifier_map -> Values.val0 Identifiers.identifier_map
 415     Errors.res **)
 416 let reg_store reg v locals0 =
 417   Identifiers.update PreIdentifiers.RegisterTag locals0 reg v
 418
 419 (** val params_store :
 420     (Registers.register, AST.typ) Types.prod List.list -> Values.val0
 421     List.list -> Values.val0 Registers.register_env -> Values.val0
 422     Registers.register_env Errors.res **)
 423 let rec params_store rs vs locals0 =
 424   match rs with
 425   | List.Nil ->
 426     (match vs with
 427      | List.Nil -> Errors.OK locals0
 428      | List.Cons (x, x0) ->
 429        Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters))
 430   | List.Cons (rt, rst) ->
 431     (match vs with
 432      | List.Nil ->
 433        Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)
 434      | List.Cons (v, vst) ->
 435        let { Types.fst = r; Types.snd = ty } = rt in
 436        let locals' = Identifiers.add PreIdentifiers.RegisterTag locals0 r v
 437        in
 438        params_store rst vst locals')
 439
 440 (** val reg_retrieve :
 441     Values.val0 Registers.register_env -> Registers.register -> Values.val0
 442     Errors.res **)
 443 let reg_retrieve locals0 reg =
 444   Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadRegister),
 445     (List.Cons ((Errors.CTX (PreIdentifiers.RegisterTag, reg)), List.Nil))))
 446     (Identifiers.lookup PreIdentifiers.RegisterTag locals0 reg)
 447
 448 (** val eval_statement :
 449     genv -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod)
 450     IOMonad.iO **)
 451 let eval_statement ge = function
 452 | State (f, fs, m) ->
 453   let s = next_instruction f in
 454   (match s with
 455    | RTLabs_syntax.St_skip l ->
 456      (fun _ ->
 457        Obj.magic
 458          (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
 459            Events.e0; Types.snd = (build_state f fs m l) }))
 460    | RTLabs_syntax.St_cost (cl, l) ->
 461      (fun _ ->
 462        Obj.magic
 463          (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
 464            (Events.echarge cl); Types.snd = (build_state f fs m l) }))
 465    | RTLabs_syntax.St_const (x, r, cst, l) ->
 466      (fun _ ->
 467        IOMonad.err_to_io
 468          (Obj.magic
 469            (Monad.m_bind0 (Monad.max_def Errors.res0)
 470              (Obj.magic
 471                (Errors.opt_to_res (Errors.msg ErrorMessages.FailedConstant)
 472                  (FrontEndOps.eval_constant x (Globalenvs.find_symbol ge)
 473                    f.sp cst))) (fun v ->
 474              Monad.m_bind0 (Monad.max_def Errors.res0)
 475                (Obj.magic (reg_store r v f.locals)) (fun locals0 ->
 476                Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 477                  Events.e0; Types.snd = (State ({ func = f.func; locals =
 478                  locals0; next = l; sp = f.sp; retdst = f.retdst }, fs, m)) })))))
 479    | RTLabs_syntax.St_op1 (x, x0, op, dst, src, l) ->
 480      (fun _ ->
 481        IOMonad.err_to_io
 482          (Obj.magic
 483            (Monad.m_bind0 (Monad.max_def Errors.res0)
 484              (Obj.magic (reg_retrieve f.locals src)) (fun v ->
 485              Monad.m_bind0 (Monad.max_def Errors.res0)
 486                (Obj.magic
 487                  (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
 488                    (FrontEndOps.eval_unop x0 x op v))) (fun v' ->
 489                Monad.m_bind0 (Monad.max_def Errors.res0)
 490                  (Obj.magic (reg_store dst v' f.locals)) (fun locals0 ->
 491                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 492                    Events.e0; Types.snd = (State ({ func = f.func; locals =
 493                    locals0; next = l; sp = f.sp; retdst = f.retdst }, fs,
 494                    m)) }))))))
 495    | RTLabs_syntax.St_op2 (x, x0, x1, op, dst, src1, src2, l) ->
 496      (fun _ ->
 497        IOMonad.err_to_io
 498          (Obj.magic
 499            (Monad.m_bind0 (Monad.max_def Errors.res0)
 500              (Obj.magic (reg_retrieve f.locals src1)) (fun v1 ->
 501              Monad.m_bind0 (Monad.max_def Errors.res0)
 502                (Obj.magic (reg_retrieve f.locals src2)) (fun v2 ->
 503                Monad.m_bind0 (Monad.max_def Errors.res0)
 504                  (Obj.magic
 505                    (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
 506                      (FrontEndOps.eval_binop m x0 x1 x op v1 v2))) (fun v' ->
 507                  Monad.m_bind0 (Monad.max_def Errors.res0)
 508                    (Obj.magic (reg_store dst v' f.locals)) (fun locals0 ->
 509                    Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 510                      Events.e0; Types.snd = (State ({ func = f.func; locals =
 511                      locals0; next = l; sp = f.sp; retdst = f.retdst }, fs,
 512                      m)) })))))))
 513    | RTLabs_syntax.St_load (chunk, addr, dst, l) ->
 514      (fun _ ->
 515        IOMonad.err_to_io
 516          (Obj.magic
 517            (Monad.m_bind0 (Monad.max_def Errors.res0)
 518              (Obj.magic (reg_retrieve f.locals addr)) (fun vaddr ->
 519              Monad.m_bind0 (Monad.max_def Errors.res0)
 520                (Obj.magic
 521                  (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
 522                    (FrontEndMem.loadv chunk m vaddr))) (fun v ->
 523                Monad.m_bind0 (Monad.max_def Errors.res0)
 524                  (Obj.magic (reg_store dst v f.locals)) (fun locals0 ->
 525                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 526                    Events.e0; Types.snd = (State ({ func = f.func; locals =
 527                    locals0; next = l; sp = f.sp; retdst = f.retdst }, fs,
 528                    m)) }))))))
 529    | RTLabs_syntax.St_store (chunk, addr, src, l) ->
 530      (fun _ ->
 531        IOMonad.err_to_io
 532          (Obj.magic
 533            (Monad.m_bind0 (Monad.max_def Errors.res0)
 534              (Obj.magic (reg_retrieve f.locals addr)) (fun vaddr ->
 535              Monad.m_bind0 (Monad.max_def Errors.res0)
 536                (Obj.magic (reg_retrieve f.locals src)) (fun v ->
 537                Monad.m_bind0 (Monad.max_def Errors.res0)
 538                  (Obj.magic
 539                    (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
 540                      (FrontEndMem.storev chunk m vaddr v))) (fun m' ->
 541                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 542                    Events.e0; Types.snd = (build_state f fs m' l) }))))))
 543    | RTLabs_syntax.St_call_id (id, args, dst, l) ->
 544      (fun _ ->
 545        IOMonad.err_to_io
 546          (Obj.magic
 547            (Monad.m_bind0 (Monad.max_def Errors.res0)
 548              (Obj.magic
 549                (Errors.opt_to_res (List.Cons ((Errors.MSG
 550                  ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
 551                  (PreIdentifiers.SymbolTag, id)), List.Nil))))
 552                  (Globalenvs.find_symbol ge id))) (fun b ->
 553              Monad.m_bind0 (Monad.max_def Errors.res0)
 554                (Obj.magic
 555                  (Errors.opt_to_res (List.Cons ((Errors.MSG
 556                    ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
 557                    (PreIdentifiers.SymbolTag, id)), List.Nil))))
 558                    (Globalenvs.find_funct_ptr ge b))) (fun fd ->
 559                Monad.m_bind0 (Monad.max_def Errors.res0)
 560                  (Monad.m_list_map (Monad.max_def Errors.res0)
 561                    (Obj.magic (reg_retrieve f.locals)) args) (fun vs ->
 562                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 563                    Events.e0; Types.snd = (Callstate (id, fd, vs, dst,
 564                    (List.Cons ((adv l f), fs)), m)) }))))))
 565    | RTLabs_syntax.St_call_ptr (frs, args, dst, l) ->
 566      (fun _ ->
 567        IOMonad.err_to_io
 568          (Obj.magic
 569            (Monad.m_bind0 (Monad.max_def Errors.res0)
 570              (Obj.magic (reg_retrieve f.locals frs)) (fun fv ->
 571              Monad.m_bind2 (Monad.max_def Errors.res0)
 572                (Obj.magic
 573                  (Errors.opt_to_res (Errors.msg ErrorMessages.BadFunction)
 574                    (Globalenvs.find_funct_id ge fv))) (fun fd id ->
 575                Monad.m_bind0 (Monad.max_def Errors.res0)
 576                  (Monad.m_list_map (Monad.max_def Errors.res0)
 577                    (Obj.magic (reg_retrieve f.locals)) args) (fun vs ->
 578                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 579                    Events.e0; Types.snd = (Callstate (id, fd, vs, dst,
 580                    (List.Cons ((adv l f), fs)), m)) }))))))
 581    | RTLabs_syntax.St_cond (src, ltrue, lfalse) ->
 582      (fun _ ->
 583        IOMonad.err_to_io
 584          (Obj.magic
 585            (Monad.m_bind0 (Monad.max_def Errors.res0)
 586              (Obj.magic (reg_retrieve f.locals src)) (fun v ->
 587              Monad.m_bind0 (Monad.max_def Errors.res0)
 588                (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
 589                Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 590                  Events.e0; Types.snd =
 591                  (build_state f fs m
 592                    (match b with
 593                     | Bool.True -> ltrue
 594                     | Bool.False -> lfalse)) })))))
 595    | RTLabs_syntax.St_return ->
 596      (fun _ ->
 597        IOMonad.err_to_io
 598          (Obj.magic
 599            (Monad.m_bind0 (Monad.max_def Errors.res0)
 600              (match f.func.RTLabs_syntax.f_result with
 601               | Types.None ->
 602                 Monad.m_return0 (Monad.max_def Errors.res0) Types.None
 603               | Types.Some rt ->
 604                 let { Types.fst = r; Types.snd = ty } = rt in
 605                 Monad.m_bind0 (Monad.max_def Errors.res0)
 606                   (Obj.magic (reg_retrieve f.locals r)) (fun v ->
 607                   Monad.m_return0 (Monad.max_def Errors.res0) (Types.Some v)))
 608              (fun v ->
 609              Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 610                Events.e0; Types.snd = (Returnstate (v, f.retdst, fs,
 611                (GenMem.free m f.sp))) }))))) __
 612 | Callstate (x, fd, params, dst, fs, m) ->
 613   (match fd with
 614    | AST.Internal fn ->
 615      IOMonad.err_to_io
 616        (Obj.magic
 617          (Monad.m_bind0 (Monad.max_def Errors.res0)
 618            (Obj.magic
 619              (params_store fn.RTLabs_syntax.f_params params
 620                (init_locals fn.RTLabs_syntax.f_locals))) (fun locals0 ->
 621            let { Types.fst = m'; Types.snd = sp0 } =
 622              GenMem.alloc m (Z.z_of_nat Nat.O)
 623                (Z.z_of_nat fn.RTLabs_syntax.f_stacksize)
 624            in
 625            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 626              Events.e0; Types.snd = (State ({ func = fn; locals = locals0;
 627              next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp = sp0; retdst =
 628              dst }, fs, m')) })))
 629    | AST.External fn ->
 630      Obj.magic
 631        (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
 632          (Obj.magic
 633            (IOMonad.err_to_io
 634              (IO.check_eventval_list params fn.AST.ef_sig.AST.sig_args)))
 635          (fun evargs ->
 636          Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
 637            (Obj.magic
 638              (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
 639            (fun evres ->
 640            Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
 641              (Events.eextcall fn.AST.ef_id evargs
 642                (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
 643              Types.snd = (Returnstate ((Types.Some
 644              (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)), dst, fs,
 645              m)) }))))
 646 | Returnstate (v, dst, fs, m) ->
 647   (match fs with
 648    | List.Nil ->
 649      (fun _ ->
 650        (match v with
 651         | Types.None ->
 652           (fun _ ->
 653             IOMonad.err_to_io (Errors.Error
 654               (Errors.msg ErrorMessages.ReturnMismatch)))
 655         | Types.Some v' ->
 656           (fun _ ->
 657             (match v' with
 658              | Values.Vundef ->
 659                (fun _ ->
 660                  IOMonad.err_to_io (Errors.Error
 661                    (Errors.msg ErrorMessages.ReturnMismatch)))
 662              | Values.Vint (sz, r) ->
 663                (fun _ ->
 664                  IOMonad.err_to_io
 665                    ((match sz with
 666                      | AST.I8 ->
 667                        (fun x -> Errors.Error
 668                          (Errors.msg ErrorMessages.ReturnMismatch))
 669                      | AST.I16 ->
 670                        (fun x -> Errors.Error
 671                          (Errors.msg ErrorMessages.ReturnMismatch))
 672                      | AST.I32 ->
 673                        (fun r0 ->
 674                          Obj.magic
 675                            (Monad.m_return0 (Monad.max_def Errors.res0)
 676                              { Types.fst = Events.e0; Types.snd = (Finalstate
 677                              r0) }))) r))
 678              | Values.Vnull ->
 679                (fun _ ->
 680                  IOMonad.err_to_io (Errors.Error
 681                    (Errors.msg ErrorMessages.ReturnMismatch)))
 682              | Values.Vptr x ->
 683                (fun _ ->
 684                  IOMonad.err_to_io (Errors.Error
 685                    (Errors.msg ErrorMessages.ReturnMismatch)))) __)) __)
 686    | List.Cons (f, fs') ->
 687      (fun _ ->
 688        IOMonad.err_to_io
 689          (Obj.magic
 690            (Monad.m_bind0 (Monad.max_def Errors.res0)
 691              (match dst with
 692               | Types.None ->
 693                 (match v with
 694                  | Types.None -> Obj.magic (Errors.OK f.locals)
 695                  | Types.Some x ->
 696                    Obj.magic (Errors.Error
 697                      (Errors.msg ErrorMessages.ReturnMismatch)))
 698               | Types.Some d ->
 699                 (match v with
 700                  | Types.None ->
 701                    Obj.magic (Errors.Error
 702                      (Errors.msg ErrorMessages.ReturnMismatch))
 703                  | Types.Some v' -> Obj.magic (reg_store d v' f.locals)))
 704              (fun locals0 ->
 705              Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 706                Events.e0; Types.snd = (State ({ func = f.func; locals =
 707                locals0; next = f.next; sp = f.sp; retdst = f.retdst }, fs',
 708                m)) }))))) __
 709 | Finalstate r ->
 710   IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.FinalState))
 711
 712 (** val rTLabs_is_final : state -> Integers.int Types.option **)
 713 let rTLabs_is_final = function
 714 | State (x, x0, x1) -> Types.None
 715 | Callstate (x, x0, x1, x2, x3, x4) -> Types.None
 716 | Returnstate (x, x0, x1, x2) -> Types.None
 717 | Finalstate r -> Types.Some r
 718
 719 (** val rTLabs_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
 720 let rTLabs_exec =
 721   { SmallstepExec.is_final = (fun x -> Obj.magic rTLabs_is_final);
 722     SmallstepExec.step = (Obj.magic eval_statement) }
 723
 724 (** val make_global : RTLabs_syntax.rTLabs_program -> genv **)
 725 let make_global p =
 726   Globalenvs.globalenv (fun x -> x) p
 727
 728 (** val make_initial_state :
 729     RTLabs_syntax.rTLabs_program -> state Errors.res **)
 730 let make_initial_state p =
 731   let ge = make_global p in
 732   Obj.magic
 733     (Monad.m_bind0 (Monad.max_def Errors.res0)
 734       (Obj.magic (Globalenvs.init_mem (fun x -> x) p)) (fun m ->
 735       let main = p.AST.prog_main in
 736       Monad.m_bind0 (Monad.max_def Errors.res0)
 737         (Obj.magic
 738           (Errors.opt_to_res (List.Cons ((Errors.MSG
 739             ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
 740             (PreIdentifiers.SymbolTag, main)), List.Nil))))
 741             (Globalenvs.find_symbol ge main))) (fun b ->
 742         Monad.m_bind0 (Monad.max_def Errors.res0)
 743           (Obj.magic
 744             (Errors.opt_to_res (List.Cons ((Errors.MSG
 745               ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
 746               (PreIdentifiers.SymbolTag, main)), List.Nil))))
 747               (Globalenvs.find_funct_ptr ge b))) (fun f ->
 748           Obj.magic (Errors.OK (Callstate (main, f, List.Nil, Types.None,
 749             List.Nil, m)))))))
 750
 751 (** val rTLabs_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
 752 let rTLabs_fullexec =
 753   { SmallstepExec.es1 = rTLabs_exec; SmallstepExec.make_global =
 754     (Obj.magic make_global); SmallstepExec.make_initial_state =
 755     (Obj.magic make_initial_state) }
 756
 757 (** val bind_ok :
 758     'a1 Errors.res -> ('a1 -> 'a2 Errors.res) -> 'a2 -> ('a1 -> __ -> __ ->
 759     'a3) -> 'a3 **)
 760 let bind_ok clearme f v x =
 761   (match clearme with
 762    | Errors.OK a -> (fun f0 v0 _ h _ -> h a __ __)
 763    | Errors.Error m ->
 764      (fun f0 v0 _ h _ ->
 765        Obj.magic Errors.res_discr (Errors.Error m) (Errors.OK v0) __)) f v __
 766     x __
 767
 768 (** val jmeq_hackT : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2 **)
 769 let jmeq_hackT x y auto =
 770   auto __
 771
 772 (** val func_block_of_exec :
 773     genv -> state -> Events.trace -> AST.ident ->
 774     RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
 775     Registers.register Types.option -> frame List.list -> GenMem.mem ->
 776     Pointers.block Types.sig0 **)
 777 let func_block_of_exec ge clearme t fid fd args dst fs m =
 778   (match clearme with
 779    | State (clearme0, x, x0) ->
 780      (let { func = func0; locals = locals0; next = next0; sp = sp0; retdst =
 781         dst0 } = clearme0
 782       in
 783      (fun fs0 m0 tr fid0 fd0 args0 dst' fs' m' ->
 784      (match next_instruction { func = func0; locals = locals0; next = next0;
 785               sp = sp0; retdst = dst0 } with
 786       | RTLabs_syntax.St_skip l ->
 787         (fun _ _ ->
 788           jmeq_hackT (IOMonad.Value { Types.fst = Events.e0; Types.snd =
 789             (build_state { func = func0; locals = locals0; next = next0; sp =
 790               sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value { Types.fst =
 791             tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })
 792             (fun _ ->
 793             Obj.magic IOMonad.iO_jmdiscr (IOMonad.Value { Types.fst =
 794               Events.e0; Types.snd =
 795               (build_state { func = func0; locals = locals0; next = next0;
 796                 sp = sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value
 797               { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
 798               dst', fs', m')) }) __ (fun _ ->
 799               Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0;
 800                 Types.snd =
 801                 (build_state { func = func0; locals = locals0; next = next0;
 802                   sp = sp0; retdst = dst0 } fs0 m0 l) } { Types.fst = tr;
 803                 Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }
 804                 __ (fun _ ->
 805                 Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
 806                   Obj.magic state_jmdiscr (State
 807                     ((adv l { func = func0; locals = locals0; next = next0;
 808                        sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate
 809                     (fid0, fd0, args0, dst', fs', m')) __) tr __ __))))
 810       | RTLabs_syntax.St_cost (c, l) ->
 811         (fun _ _ ->
 812           jmeq_hackT (IOMonad.Value { Types.fst = (Events.echarge c);
 813             Types.snd =
 814             (build_state { func = func0; locals = locals0; next = next0; sp =
 815               sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value { Types.fst =
 816             tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })
 817             (fun _ ->
 818             Obj.magic IOMonad.iO_jmdiscr (IOMonad.Value { Types.fst =
 819               (Events.echarge c); Types.snd =
 820               (build_state { func = func0; locals = locals0; next = next0;
 821                 sp = sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value
 822               { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
 823               dst', fs', m')) }) __ (fun _ ->
 824               Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
 825                 (Events.echarge c); Types.snd =
 826                 (build_state { func = func0; locals = locals0; next = next0;
 827                   sp = sp0; retdst = dst0 } fs0 m0 l) } { Types.fst = tr;
 828                 Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }
 829                 __ (fun _ ->
 830                 Logic.eq_rect_Type0 (List.Cons ((Events.EVcost c), List.Nil))
 831                   (fun _ _ _ ->
 832                   Obj.magic state_jmdiscr (State
 833                     ((adv l { func = func0; locals = locals0; next = next0;
 834                        sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate
 835                     (fid0, fd0, args0, dst', fs', m')) __) tr __ __))))
 836       | RTLabs_syntax.St_const (t0, r, c, l) ->
 837         (fun _ _ ->
 838           IOMonad.bind_res_value
 839             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedConstant)
 840               (FrontEndOps.eval_constant t0 (Globalenvs.find_symbol ge) sp0
 841                 c)) (fun v ->
 842             Obj.magic
 843               (Monad.m_bind0 (Monad.max_def Errors.res0)
 844                 (Obj.magic (reg_store r v locals0)) (fun locals1 ->
 845                 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 846                   Events.e0; Types.snd = (State ({ func = func0; locals =
 847                   locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))
 848             { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst',
 849             fs', m')) } (fun v _ _ ->
 850             bind_ok (reg_store r v locals0) (fun x1 ->
 851               Obj.magic
 852                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 853                   Events.e0; Types.snd = (State ({ func = func0; locals = x1;
 854                   next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))
 855               { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
 856               dst', fs', m')) } (fun locals' _ _ ->
 857               jmeq_hackT
 858                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 859                   Events.e0; Types.snd = (State ({ func = func0; locals =
 860                   locals'; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
 861                 (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
 862                   (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ ->
 863                 Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
 864                   Events.e0; Types.snd = (State ({ func = func0; locals =
 865                   locals'; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
 866                   (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0,
 867                   fd0, args0, dst', fs', m')) }) __ (fun _ ->
 868                   Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0;
 869                     Types.snd = (State ({ func = func0; locals = locals';
 870                     next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }
 871                     { Types.fst = tr; Types.snd = (Callstate (fid0, fd0,
 872                     args0, dst', fs', m')) } __ (fun _ ->
 873                     Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
 874                       Obj.magic state_jmdiscr (State ({ func = func0;
 875                         locals = locals'; next = l; sp = sp0; retdst =
 876                         dst0 }, fs0, m0)) (Callstate (fid0, fd0, args0, dst',
 877                         fs', m')) __) tr __ __))))))
 878       | RTLabs_syntax.St_op1 (t1, t2, op, r1, r2, l) ->
 879         (fun _ _ ->
 880           IOMonad.bind_res_value (reg_retrieve locals0 r2) (fun v ->
 881             Obj.magic
 882               (Monad.m_bind0 (Monad.max_def Errors.res0)
 883                 (Obj.magic
 884                   (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
 885                     (FrontEndOps.eval_unop t2 t1 op v))) (fun v' ->
 886                 Monad.m_bind0 (Monad.max_def Errors.res0)
 887                   (Obj.magic (reg_store r1 v' locals0)) (fun locals1 ->
 888                   Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 889                     Events.e0; Types.snd = (State ({ func = func0; locals =
 890                     locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))))
 891             { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst',
 892             fs', m')) } (fun v _ _ ->
 893             bind_ok
 894               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
 895                 (FrontEndOps.eval_unop t2 t1 op v)) (fun x1 ->
 896               Obj.magic
 897                 (Monad.m_bind0 (Monad.max_def Errors.res0)
 898                   (Obj.magic (reg_store r1 x1 locals0)) (fun locals1 ->
 899                   Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 900                     Events.e0; Types.snd = (State ({ func = func0; locals =
 901                     locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))
 902               { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
 903               dst', fs', m')) } (fun v' _ _ ->
 904               bind_ok (reg_store r1 v' locals0) (fun x1 ->
 905                 Obj.magic
 906                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 907                     Events.e0; Types.snd = (State ({ func = func0; locals =
 908                     x1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))
 909                 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
 910                 dst', fs', m')) } (fun loc _ _ ->
 911                 jmeq_hackT
 912                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 913                     Events.e0; Types.snd = (State ({ func = func0; locals =
 914                     loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
 915                   (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
 916                     (Callstate (fid0, fd0, args0, dst', fs', m')) }))
 917                   (fun _ ->
 918                   Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
 919                     Events.e0; Types.snd = (State ({ func = func0; locals =
 920                     loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
 921                     (Errors.OK { Types.fst = tr; Types.snd = (Callstate
 922                     (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ ->
 923                     Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
 924                       Events.e0; Types.snd = (State ({ func = func0; locals =
 925                       loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }
 926                       { Types.fst = tr; Types.snd = (Callstate (fid0, fd0,
 927                       args0, dst', fs', m')) } __ (fun _ ->
 928                       Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
 929                         Obj.magic state_jmdiscr (State ({ func = func0;
 930                           locals = loc; next = l; sp = sp0; retdst = dst0 },
 931                           fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs',
 932                           m')) __) tr __ __)))))))
 933       | RTLabs_syntax.St_op2 (t1, t2, t', op, r1, r2, r3, l) ->
 934         (fun _ _ ->
 935           IOMonad.bind_res_value (reg_retrieve locals0 r2) (fun v1 ->
 936             Obj.magic
 937               (Monad.m_bind0 (Monad.max_def Errors.res0)
 938                 (Obj.magic (reg_retrieve locals0 r3)) (fun v2 ->
 939                 Monad.m_bind0 (Monad.max_def Errors.res0)
 940                   (Obj.magic
 941                     (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
 942                       (FrontEndOps.eval_binop m0 t2 t' t1 op v1 v2)))
 943                   (fun v' ->
 944                   Monad.m_bind0 (Monad.max_def Errors.res0)
 945                     (Obj.magic (reg_store r1 v' locals0)) (fun locals1 ->
 946                     Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 947                       Events.e0; Types.snd = (State ({ func = func0; locals =
 948                       locals1; next = l; sp = sp0; retdst = dst0 }, fs0,
 949                       m0)) }))))) { Types.fst = tr; Types.snd = (Callstate
 950             (fid0, fd0, args0, dst', fs', m')) } (fun v1 _ _ ->
 951             bind_ok (reg_retrieve locals0 r3) (fun x1 ->
 952               Obj.magic
 953                 (Monad.m_bind0 (Monad.max_def Errors.res0)
 954                   (Obj.magic
 955                     (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
 956                       (FrontEndOps.eval_binop m0 t2 t' t1 op v1 x1)))
 957                   (fun v' ->
 958                   Monad.m_bind0 (Monad.max_def Errors.res0)
 959                     (Obj.magic (reg_store r1 v' locals0)) (fun locals1 ->
 960                     Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 961                       Events.e0; Types.snd = (State ({ func = func0; locals =
 962                       locals1; next = l; sp = sp0; retdst = dst0 }, fs0,
 963                       m0)) })))) { Types.fst = tr; Types.snd = (Callstate
 964               (fid0, fd0, args0, dst', fs', m')) } (fun v2 _ _ ->
 965               bind_ok
 966                 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
 967                   (FrontEndOps.eval_binop m0 t2 t' t1 op v1 v2)) (fun x1 ->
 968                 Obj.magic
 969                   (Monad.m_bind0 (Monad.max_def Errors.res0)
 970                     (Obj.magic (reg_store r1 x1 locals0)) (fun locals1 ->
 971                     Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 972                       Events.e0; Types.snd = (State ({ func = func0; locals =
 973                       locals1; next = l; sp = sp0; retdst = dst0 }, fs0,
 974                       m0)) }))) { Types.fst = tr; Types.snd = (Callstate
 975                 (fid0, fd0, args0, dst', fs', m')) } (fun v' _ _ ->
 976                 bind_ok (reg_store r1 v' locals0) (fun x1 ->
 977                   Obj.magic
 978                     (Monad.m_return0 (Monad.max_def Errors.res0)
 979                       { Types.fst = Events.e0; Types.snd = (State ({ func =
 980                       func0; locals = x1; next = l; sp = sp0; retdst =
 981                       dst0 }, fs0, m0)) })) { Types.fst = tr; Types.snd =
 982                   (Callstate (fid0, fd0, args0, dst', fs', m')) }
 983                   (fun loc _ _ ->
 984                   jmeq_hackT
 985                     (Monad.m_return0 (Monad.max_def Errors.res0)
 986                       { Types.fst = Events.e0; Types.snd = (State ({ func =
 987                       func0; locals = loc; next = l; sp = sp0; retdst =
 988                       dst0 }, fs0, m0)) })
 989                     (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
 990                       (Callstate (fid0, fd0, args0, dst', fs', m')) }))
 991                     (fun _ ->
 992                     Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
 993                       Events.e0; Types.snd = (State ({ func = func0; locals =
 994                       loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
 995                       (Errors.OK { Types.fst = tr; Types.snd = (Callstate
 996                       (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ ->
 997                       Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
 998                         Events.e0; Types.snd = (State ({ func = func0;
 999                         locals = loc; next = l; sp = sp0; retdst = dst0 },
1000                         fs0, m0)) } { Types.fst = tr; Types.snd = (Callstate
1001                         (fid0, fd0, args0, dst', fs', m')) } __ (fun _ ->
1002                         Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1003                           Obj.magic state_jmdiscr (State ({ func = func0;
1004                             locals = loc; next = l; sp = sp0; retdst =
1005                             dst0 }, fs0, m0)) (Callstate (fid0, fd0, args0,
1006                             dst', fs', m')) __) tr __ __))))))))
1007       | RTLabs_syntax.St_load (ch, r1, r2, l) ->
1008         (fun _ _ ->
1009           IOMonad.bind_res_value (reg_retrieve locals0 r1) (fun vaddr ->
1010             Obj.magic
1011               (Monad.m_bind0 (Monad.max_def Errors.res0)
1012                 (Obj.magic
1013                   (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
1014                     (FrontEndMem.loadv ch m0 vaddr))) (fun v ->
1015                 Monad.m_bind0 (Monad.max_def Errors.res0)
1016                   (Obj.magic (reg_store r2 v locals0)) (fun locals1 ->
1017                   Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1018                     Events.e0; Types.snd = (State ({ func = func0; locals =
1019                     locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))))
1020             { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst',
1021             fs', m')) } (fun v _ _ ->
1022             bind_ok
1023               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
1024                 (FrontEndMem.loadv ch m0 v)) (fun x1 ->
1025               Obj.magic
1026                 (Monad.m_bind0 (Monad.max_def Errors.res0)
1027                   (Obj.magic (reg_store r2 x1 locals0)) (fun locals1 ->
1028                   Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1029                     Events.e0; Types.snd = (State ({ func = func0; locals =
1030                     locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))
1031               { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
1032               dst', fs', m')) } (fun v' _ _ ->
1033               bind_ok (reg_store r2 v' locals0) (fun x1 ->
1034                 Obj.magic
1035                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1036                     Events.e0; Types.snd = (State ({ func = func0; locals =
1037                     x1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))
1038                 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
1039                 dst', fs', m')) } (fun loc _ _ ->
1040                 jmeq_hackT
1041                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1042                     Events.e0; Types.snd = (State ({ func = func0; locals =
1043                     loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
1044                   (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1045                     (Callstate (fid0, fd0, args0, dst', fs', m')) }))
1046                   (fun _ ->
1047                   Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1048                     Events.e0; Types.snd = (State ({ func = func0; locals =
1049                     loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })
1050                     (Errors.OK { Types.fst = tr; Types.snd = (Callstate
1051                     (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ ->
1052                     Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
1053                       Events.e0; Types.snd = (State ({ func = func0; locals =
1054                       loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }
1055                       { Types.fst = tr; Types.snd = (Callstate (fid0, fd0,
1056                       args0, dst', fs', m')) } __ (fun _ ->
1057                       Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1058                         Obj.magic state_jmdiscr (State ({ func = func0;
1059                           locals = loc; next = l; sp = sp0; retdst = dst0 },
1060                           fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs',
1061                           m')) __) tr __ __)))))))
1062       | RTLabs_syntax.St_store (ch, r1, r2, l) ->
1063         (fun _ _ ->
1064           IOMonad.bind_res_value (reg_retrieve locals0 r1) (fun vaddr ->
1065             Obj.magic
1066               (Monad.m_bind0 (Monad.max_def Errors.res0)
1067                 (Obj.magic (reg_retrieve locals0 r2)) (fun v ->
1068                 Monad.m_bind0 (Monad.max_def Errors.res0)
1069                   (Obj.magic
1070                     (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
1071                       (FrontEndMem.storev ch m0 vaddr v))) (fun m'0 ->
1072                   Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1073                     Events.e0; Types.snd =
1074                     (build_state { func = func0; locals = locals0; next =
1075                       next0; sp = sp0; retdst = dst0 } fs0 m'0 l) }))))
1076             { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst',
1077             fs', m')) } (fun v _ _ ->
1078             bind_ok (reg_retrieve locals0 r2) (fun x1 ->
1079               Obj.magic
1080                 (Monad.m_bind0 (Monad.max_def Errors.res0)
1081                   (Obj.magic
1082                     (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
1083                       (FrontEndMem.storev ch m0 v x1))) (fun m'0 ->
1084                   Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1085                     Events.e0; Types.snd =
1086                     (build_state { func = func0; locals = locals0; next =
1087                       next0; sp = sp0; retdst = dst0 } fs0 m'0 l) })))
1088               { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
1089               dst', fs', m')) } (fun v' _ _ ->
1090               bind_ok
1091                 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
1092                   (FrontEndMem.storev ch m0 v v')) (fun x1 ->
1093                 Obj.magic
1094                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1095                     Events.e0; Types.snd =
1096                     (build_state { func = func0; locals = locals0; next =
1097                       next0; sp = sp0; retdst = dst0 } fs0 x1 l) }))
1098                 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
1099                 dst', fs', m')) } (fun loc _ _ ->
1100                 jmeq_hackT
1101                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1102                     Events.e0; Types.snd =
1103                     (build_state { func = func0; locals = locals0; next =
1104                       next0; sp = sp0; retdst = dst0 } fs0 loc l) })
1105                   (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1106                     (Callstate (fid0, fd0, args0, dst', fs', m')) }))
1107                   (fun _ ->
1108                   Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1109                     Events.e0; Types.snd =
1110                     (build_state { func = func0; locals = locals0; next =
1111                       next0; sp = sp0; retdst = dst0 } fs0 loc l) })
1112                     (Errors.OK { Types.fst = tr; Types.snd = (Callstate
1113                     (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ ->
1114                     Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
1115                       Events.e0; Types.snd =
1116                       (build_state { func = func0; locals = locals0; next =
1117                         next0; sp = sp0; retdst = dst0 } fs0 loc l) }
1118                       { Types.fst = tr; Types.snd = (Callstate (fid0, fd0,
1119                       args0, dst', fs', m')) } __ (fun _ ->
1120                       Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1121                         Obj.magic state_jmdiscr (State
1122                           ((adv l { func = func0; locals = locals0; next =
1123                              next0; sp = sp0; retdst = dst0 }), fs0, loc))
1124                           (Callstate (fid0, fd0, args0, dst', fs', m')) __)
1125                         tr __ __)))))))
1126       | RTLabs_syntax.St_call_id (x1, rs, or0, l) ->
1127         (fun _ _ ->
1128           IOMonad.bind_res_value
1129             (Errors.opt_to_res (List.Cons ((Errors.MSG
1130               ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX
1131               (PreIdentifiers.SymbolTag, x1)), List.Nil))))
1132               (Globalenvs.find_symbol ge x1)) (fun b ->
1133             Obj.magic
1134               (Monad.m_bind0 (Monad.max_def Errors.res0)
1135                 (Obj.magic
1136                   (Errors.opt_to_res (List.Cons ((Errors.MSG
1137                     ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1138                     (PreIdentifiers.SymbolTag, x1)), List.Nil))))
1139                     (Globalenvs.find_funct_ptr ge b))) (fun fd1 ->
1140                 Monad.m_bind0 (Monad.max_def Errors.res0)
1141                   (Monad.m_list_map (Monad.max_def Errors.res0)
1142                     (Obj.magic (reg_retrieve locals0)) rs) (fun vs ->
1143                   Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1144                     Events.e0; Types.snd = (Callstate (x1, fd1, vs, or0,
1145                     (List.Cons
1146                     ((adv l { func = func0; locals = locals0; next = next0;
1147                        sp = sp0; retdst = dst0 }), fs0)), m0)) }))))
1148             { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst',
1149             fs', m')) } (fun v _ _ ->
1150             bind_ok
1151               (Errors.opt_to_res (List.Cons ((Errors.MSG
1152                 ErrorMessages.BadFunction), (List.Cons ((Errors.CTX
1153                 (PreIdentifiers.SymbolTag, x1)), List.Nil))))
1154                 (Globalenvs.find_funct_ptr ge v)) (fun x2 ->
1155               Obj.magic
1156                 (Monad.m_bind0 (Monad.max_def Errors.res0)
1157                   (Monad.m_list_map (Monad.max_def Errors.res0)
1158                     (Obj.magic (reg_retrieve locals0)) rs) (fun vs ->
1159                   Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1160                     Events.e0; Types.snd = (Callstate (x1, x2, vs, or0,
1161                     (List.Cons
1162                     ((adv l { func = func0; locals = locals0; next = next0;
1163                        sp = sp0; retdst = dst0 }), fs0)), m0)) })))
1164               { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
1165               dst', fs', m')) } (fun fd' _ _ ->
1166               bind_ok
1167                 (Obj.magic
1168                   (Monad.m_list_map (Monad.max_def Errors.res0)
1169                     (Obj.magic (reg_retrieve locals0)) rs)) (fun x2 ->
1170                 Obj.magic
1171                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1172                     Events.e0; Types.snd = (Callstate (x1, fd', x2, or0,
1173                     (List.Cons
1174                     ((adv l { func = func0; locals = locals0; next = next0;
1175                        sp = sp0; retdst = dst0 }), fs0)), m0)) }))
1176                 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
1177                 dst', fs', m')) } (fun vs _ _ ->
1178                 jmeq_hackT
1179                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1180                     Events.e0; Types.snd = (Callstate (x1, fd', vs, or0,
1181                     (List.Cons
1182                     ((adv l { func = func0; locals = locals0; next = next0;
1183                        sp = sp0; retdst = dst0 }), fs0)), m0)) })
1184                   (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1185                     (Callstate (fid0, fd0, args0, dst', fs', m')) }))
1186                   (fun _ ->
1187                   Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1188                     List.Nil; Types.snd = (Callstate (x1, fd', vs, or0,
1189                     (List.Cons ({ func = func0; locals = locals0; next = l;
1190                     sp = sp0; retdst = dst0 }, fs0)), m0)) }) (Errors.OK
1191                     { Types.fst = tr; Types.snd = (Callstate (fid0, fd0,
1192                     args0, dst', fs', m')) }) __ (fun _ ->
1193                     Obj.magic Globalenvs.prod_jmdiscr { Types.fst = List.Nil;
1194                       Types.snd = (Callstate (x1, fd', vs, or0, (List.Cons
1195                       ({ func = func0; locals = locals0; next = l; sp = sp0;
1196                       retdst = dst0 }, fs0)), m0)) } { Types.fst = tr;
1197                       Types.snd = (Callstate (fid0, fd0, args0, dst', fs',
1198                       m')) } __ (fun _ ->
1199                       Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1200                         Obj.magic state_jmdiscr (Callstate (x1, fd', vs, or0,
1201                           (List.Cons ({ func = func0; locals = locals0;
1202                           next = l; sp = sp0; retdst = dst0 }, fs0)), m0))
1203                           (Callstate (fid0, fd0, args0, dst', fs', m')) __
1204                           (fun _ ->
1205                           Extralib.eq_rect_Type0_r fid0 (fun _ _ _ _ _ _ _ ->
1206                             Extralib.eq_rect_Type0_r fd0 (fun _ _ _ _ _ ->
1207                               Extralib.eq_rect_Type0_r args0
1208                                 (fun _ _ _ _ _ ->
1209                                 Extralib.eq_rect_Type0_r dst'
1210                                   (fun _ _ _ _ _ ->
1211                                   Logic.eq_rect_Type0 (List.Cons ({ func =
1212                                     func0; locals = locals0; next = l; sp =
1213                                     sp0; retdst = dst0 }, fs0))
1214                                     (fun _ _ _ _ ->
1215                                     Extralib.eq_rect_Type0_r m' (fun _ _ _ ->
1216                                       Logic.streicherK (Errors.OK
1217                                         { Types.fst = List.Nil; Types.snd =
1218                                         (Callstate (fid0, fd0, args0, dst',
1219                                         (List.Cons ({ func = func0; locals =
1220                                         locals0; next = l; sp = sp0; retdst =
1221                                         dst0 }, fs0)), m')) })
1222                                         (Logic.streicherK { Types.fst =
1223                                           List.Nil; Types.snd = (Callstate
1224                                           (fid0, fd0, args0, dst', (List.Cons
1225                                           ({ func = func0; locals = locals0;
1226                                           next = l; sp = sp0; retdst =
1227                                           dst0 }, fs0)), m')) }
1228                                           (Logic.streicherK (Callstate (fid0,
1229                                             fd0, args0, dst', (List.Cons
1230                                             ({ func = func0; locals =
1231                                             locals0; next = l; sp = sp0;
1232                                             retdst = dst0 }, fs0)), m')) v)))
1233                                       m0 __ __ __) fs' __ __ __) or0 __ __ __
1234                                   __) vs __ __ __ __) fd' __ __ __ __) x1 __
1235                             __ __ __ __ __)) tr __ __)))))))
1236       | RTLabs_syntax.St_call_ptr (x1, rs, or0, l) ->
1237         (fun _ _ ->
1238           IOMonad.bind_res_value (reg_retrieve locals0 x1) (fun fv ->
1239             Obj.magic
1240               (Monad.m_bind2 (Monad.max_def Errors.res0)
1241                 (Obj.magic
1242                   (Errors.opt_to_res (Errors.msg ErrorMessages.BadFunction)
1243                     (Globalenvs.find_funct_id ge fv))) (fun fd1 id ->
1244                 Monad.m_bind0 (Monad.max_def Errors.res0)
1245                   (Monad.m_list_map (Monad.max_def Errors.res0)
1246                     (Obj.magic (reg_retrieve locals0)) rs) (fun vs ->
1247                   Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1248                     Events.e0; Types.snd = (Callstate (id, fd1, vs, or0,
1249                     (List.Cons
1250                     ((adv l { func = func0; locals = locals0; next = next0;
1251                        sp = sp0; retdst = dst0 }), fs0)), m0)) }))))
1252             { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst',
1253             fs', m')) } (fun v _ _ ->
1254             bind_ok
1255               (Errors.opt_to_res (Errors.msg ErrorMessages.BadFunction)
1256                 (Globalenvs.find_funct_id ge v)) (fun x2 ->
1257               Obj.magic
1258                 (Monad.m_bind0 (Monad.max_def Errors.res0)
1259                   (Monad.m_list_map (Monad.max_def Errors.res0)
1260                     (Obj.magic (reg_retrieve locals0)) rs) (fun vs ->
1261                   Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1262                     Events.e0; Types.snd = (Callstate (x2.Types.snd,
1263                     x2.Types.fst, vs, or0, (List.Cons
1264                     ((adv l { func = func0; locals = locals0; next = next0;
1265                        sp = sp0; retdst = dst0 }), fs0)), m0)) })))
1266               { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
1267               dst', fs', m')) } (fun fd' _ _ ->
1268               bind_ok
1269                 (Obj.magic
1270                   (Monad.m_list_map (Monad.max_def Errors.res0)
1271                     (Obj.magic (reg_retrieve locals0)) rs)) (fun x2 ->
1272                 Obj.magic
1273                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1274                     Events.e0; Types.snd = (Callstate (fd'.Types.snd,
1275                     fd'.Types.fst, x2, or0, (List.Cons
1276                     ((adv l { func = func0; locals = locals0; next = next0;
1277                        sp = sp0; retdst = dst0 }), fs0)), m0)) }))
1278                 { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0,
1279                 dst', fs', m')) } (fun vs _ _ ->
1280                 jmeq_hackT
1281                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1282                     Events.e0; Types.snd = (Callstate (fd'.Types.snd,
1283                     fd'.Types.fst, vs, or0, (List.Cons
1284                     ((adv l { func = func0; locals = locals0; next = next0;
1285                        sp = sp0; retdst = dst0 }), fs0)), m0)) })
1286                   (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1287                     (Callstate (fid0, fd0, args0, dst', fs', m')) }))
1288                   (fun _ ->
1289                   Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1290                     List.Nil; Types.snd = (Callstate (fd'.Types.snd,
1291                     fd'.Types.fst, vs, or0, (List.Cons ({ func = func0;
1292                     locals = locals0; next = l; sp = sp0; retdst = dst0 },
1293                     fs0)), m0)) }) (Errors.OK { Types.fst = tr; Types.snd =
1294                     (Callstate (fid0, fd0, args0, dst', fs', m')) }) __
1295                     (fun _ ->
1296                     Obj.magic Globalenvs.prod_jmdiscr { Types.fst = List.Nil;
1297                       Types.snd = (Callstate (fd'.Types.snd, fd'.Types.fst,
1298                       vs, or0, (List.Cons ({ func = func0; locals = locals0;
1299                       next = l; sp = sp0; retdst = dst0 }, fs0)), m0)) }
1300                       { Types.fst = tr; Types.snd = (Callstate (fid0, fd0,
1301                       args0, dst', fs', m')) } __ (fun _ ->
1302                       Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1303                         Obj.magic state_jmdiscr (Callstate (fd'.Types.snd,
1304                           fd'.Types.fst, vs, or0, (List.Cons ({ func = func0;
1305                           locals = locals0; next = l; sp = sp0; retdst =
1306                           dst0 }, fs0)), m0)) (Callstate (fid0, fd0, args0,
1307                           dst', fs', m')) __ (fun _ ->
1308                           Logic.eq_rect_Type0 fd'.Types.snd (fun _ _ _ _ ->
1309                             Logic.eq_rect_Type0 fd'.Types.fst (fun _ _ _ _ ->
1310                               Extralib.eq_rect_Type0_r args0
1311                                 (fun _ _ _ _ _ ->
1312                                 Extralib.eq_rect_Type0_r dst'
1313                                   (fun _ _ _ _ _ ->
1314                                   Logic.eq_rect_Type0 (List.Cons ({ func =
1315                                     func0; locals = locals0; next = l; sp =
1316                                     sp0; retdst = dst0 }, fs0))
1317                                     (fun _ _ _ _ ->
1318                                     Extralib.eq_rect_Type0_r m' (fun _ _ _ ->
1319                                       Logic.streicherK (Errors.OK
1320                                         { Types.fst = List.Nil; Types.snd =
1321                                         (Callstate (fd'.Types.snd,
1322                                         fd'.Types.fst, args0, dst',
1323                                         (List.Cons ({ func = func0; locals =
1324                                         locals0; next = l; sp = sp0; retdst =
1325                                         dst0 }, fs0)), m')) })
1326                                         (Logic.streicherK { Types.fst =
1327                                           List.Nil; Types.snd = (Callstate
1328                                           (fd'.Types.snd, fd'.Types.fst,
1329                                           args0, dst', (List.Cons ({ func =
1330                                           func0; locals = locals0; next = l;
1331                                           sp = sp0; retdst = dst0 }, fs0)),
1332                                           m')) }
1333                                           (Logic.streicherK (Callstate
1334                                             (fd'.Types.snd, fd'.Types.fst,
1335                                             args0, dst', (List.Cons ({ func =
1336                                             func0; locals = locals0; next =
1337                                             l; sp = sp0; retdst = dst0 },
1338                                             fs0)), m'))
1339                                             ((match v with
1340                                               | Values.Vundef ->
1341                                                 (fun _ ->
1342                                                   Obj.magic Errors.res_discr
1343                                                     (Errors.Error (List.Cons
1344                                                     ((Errors.MSG
1345                                                     ErrorMessages.BadFunction),
1346                                                     List.Nil))) (Errors.OK
1347                                                     fd') __)
1348                                               | Values.Vint (a, b) ->
1349                                                 (fun _ ->
1350                                                   Obj.magic Errors.res_discr
1351                                                     (Errors.Error (List.Cons
1352                                                     ((Errors.MSG
1353                                                     ErrorMessages.BadFunction),
1354                                                     List.Nil))) (Errors.OK
1355                                                     fd') __)
1356                                               | Values.Vnull ->
1357                                                 (fun _ ->
1358                                                   Obj.magic Errors.res_discr
1359                                                     (Errors.Error (List.Cons
1360                                                     ((Errors.MSG
1361                                                     ErrorMessages.BadFunction),
1362                                                     List.Nil))) (Errors.OK
1363                                                     fd') __)
1364                                               | Values.Vptr clearme1 ->
1365                                                 let { Pointers.pblock = b;
1366                                                   Pointers.poff = off } =
1367                                                   clearme1
1368                                                 in
1369                                                 let { Types.fst = fd'';
1370                                                   Types.snd = fid' } = fd'
1371                                                 in
1372                                                 (fun _ -> b)) __)))) m0 __ __
1373                                       __) fs' __ __ __) or0 __ __ __ __) vs
1374                                 __ __ __ __) fd0 __ __ __) fid0 __ __ __)) tr
1375                         __ __)))))))
1376       | RTLabs_syntax.St_cond (r, l1, l2) ->
1377         (fun _ _ ->
1378           IOMonad.bind_res_value (reg_retrieve locals0 r) (fun v ->
1379             Obj.magic
1380               (Monad.m_bind0 (Monad.max_def Errors.res0)
1381                 (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
1382                 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1383                   Events.e0; Types.snd =
1384                   (build_state { func = func0; locals = locals0; next =
1385                     next0; sp = sp0; retdst = dst0 } fs0 m0
1386                     (match b with
1387                      | Bool.True -> l1
1388                      | Bool.False -> l2)) }))) { Types.fst = tr; Types.snd =
1389             (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v _ _ ->
1390             bind_ok (Values.eval_bool_of_val v) (fun x1 ->
1391               Obj.magic
1392                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1393                   Events.e0; Types.snd =
1394                   (build_state { func = func0; locals = locals0; next =
1395                     next0; sp = sp0; retdst = dst0 } fs0 m0
1396                     (match x1 with
1397                      | Bool.True -> l1
1398                      | Bool.False -> l2)) })) { Types.fst = tr; Types.snd =
1399               (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun b _ _ ->
1400               jmeq_hackT
1401                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1402                   Events.e0; Types.snd =
1403                   (build_state { func = func0; locals = locals0; next =
1404                     next0; sp = sp0; retdst = dst0 } fs0 m0
1405                     (match b with
1406                      | Bool.True -> l1
1407                      | Bool.False -> l2)) })
1408                 (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1409                   (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ ->
1410                 Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1411                   Events.e0; Types.snd =
1412                   (build_state { func = func0; locals = locals0; next =
1413                     next0; sp = sp0; retdst = dst0 } fs0 m0
1414                     (match b with
1415                      | Bool.True -> l1
1416                      | Bool.False -> l2)) }) (Errors.OK { Types.fst = tr;
1417                   Types.snd = (Callstate (fid0, fd0, args0, dst', fs',
1418                   m')) }) __ (fun _ ->
1419                   Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0;
1420                     Types.snd =
1421                     (build_state { func = func0; locals = locals0; next =
1422                       next0; sp = sp0; retdst = dst0 } fs0 m0
1423                       (match b with
1424                        | Bool.True -> l1
1425                        | Bool.False -> l2)) } { Types.fst = tr; Types.snd =
1426                     (Callstate (fid0, fd0, args0, dst', fs', m')) } __
1427                     (fun _ ->
1428                     Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1429                       Obj.magic state_jmdiscr (State
1430                         ((adv
1431                            (match b with
1432                             | Bool.True -> l1
1433                             | Bool.False -> l2) { func = func0; locals =
1434                            locals0; next = next0; sp = sp0; retdst = dst0 }),
1435                         fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs',
1436                         m')) __) tr __ __))))))
1437       | RTLabs_syntax.St_return ->
1438         (fun _ _ ->
1439           IOMonad.bind_res_value
1440             (match func0.RTLabs_syntax.f_result with
1441              | Types.None ->
1442                Obj.magic
1443                  (Monad.m_return0 (Monad.max_def Errors.res0) Types.None)
1444              | Types.Some rt ->
1445                let { Types.fst = r; Types.snd = ty } = rt in
1446                Obj.magic
1447                  (Monad.m_bind0 (Monad.max_def Errors.res0)
1448                    (Obj.magic (reg_retrieve locals0 r)) (fun v ->
1449                    Monad.m_return0 (Monad.max_def Errors.res0) (Types.Some v))))
1450             (fun v ->
1451             Obj.magic
1452               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1453                 Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1454                 (GenMem.free m0 sp0))) })) { Types.fst = tr; Types.snd =
1455             (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v ->
1456             match func0.RTLabs_syntax.f_result with
1457             | Types.None ->
1458               (fun _ _ ->
1459                 jmeq_hackT
1460                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1461                     Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1462                     (GenMem.free m0 sp0))) })
1463                   (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1464                     (Callstate (fid0, fd0, args0, dst', fs', m')) }))
1465                   (fun _ ->
1466                   Obj.magic Errors.res_discr (Errors.OK Types.None)
1467                     (Errors.OK v) __
1468                     (Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1469                       Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1470                       (GenMem.free m0 sp0))) }) (Errors.OK { Types.fst = tr;
1471                       Types.snd = (Callstate (fid0, fd0, args0, dst', fs',
1472                       m')) }) __ (fun _ ->
1473                       Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
1474                         Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1475                         (GenMem.free m0 sp0))) } { Types.fst = tr;
1476                         Types.snd = (Callstate (fid0, fd0, args0, dst', fs',
1477                         m')) } __ (fun _ ->
1478                         Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1479                           Obj.magic state_jmdiscr (Returnstate (v, dst0, fs0,
1480                             (GenMem.free m0 sp0))) (Callstate (fid0, fd0,
1481                             args0, dst', fs', m')) __) tr __ __)))))
1482             | Types.Some clearme1 ->
1483               let { Types.fst = r; Types.snd = t0 } = clearme1 in
1484               (fun _ ->
1485               bind_ok (reg_retrieve locals0 r) (fun x1 ->
1486                 Obj.magic
1487                   (Monad.m_return0 (Monad.max_def Errors.res0) (Types.Some
1488                     x1))) v (fun v0 _ _ _ ->
1489                 jmeq_hackT
1490                   (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1491                     Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1492                     (GenMem.free m0 sp0))) })
1493                   (Obj.magic (Errors.OK { Types.fst = tr; Types.snd =
1494                     (Callstate (fid0, fd0, args0, dst', fs', m')) }))
1495                   (fun _ ->
1496                   Obj.magic Errors.res_discr (Errors.OK (Types.Some v0))
1497                     (Errors.OK v) __
1498                     (Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1499                       Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1500                       (GenMem.free m0 sp0))) }) (Errors.OK { Types.fst = tr;
1501                       Types.snd = (Callstate (fid0, fd0, args0, dst', fs',
1502                       m')) }) __ (fun _ ->
1503                       Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
1504                         Events.e0; Types.snd = (Returnstate (v, dst0, fs0,
1505                         (GenMem.free m0 sp0))) } { Types.fst = tr;
1506                         Types.snd = (Callstate (fid0, fd0, args0, dst', fs',
1507                         m')) } __ (fun _ ->
1508                         Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1509                           Obj.magic state_jmdiscr (Returnstate (v, dst0, fs0,
1510                             (GenMem.free m0 sp0))) (Callstate (fid0, fd0,
1511                             args0, dst', fs', m')) __) tr __ __))))))))) __))
1512        x x0
1513    | Callstate (vf, clearme0, x, x0, x1, x2) ->
1514      (match clearme0 with
1515       | AST.Internal fn ->
1516         (fun args0 retdst0 stk m0 tr vf' fd' args' dst' fs' m' _ ->
1517           IOMonad.bind_res_value
1518             (params_store fn.RTLabs_syntax.f_params args0
1519               (init_locals fn.RTLabs_syntax.f_locals)) (fun locals0 ->
1520             let { Types.fst = m'0; Types.snd = sp0 } =
1521               GenMem.alloc m0 (Z.z_of_nat Nat.O)
1522                 (Z.z_of_nat fn.RTLabs_syntax.f_stacksize)
1523             in
1524             Obj.magic
1525               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1526                 Events.e0; Types.snd = (State ({ func = fn; locals = locals0;
1527                 next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp = sp0;
1528                 retdst = retdst0 }, stk, m'0)) })) { Types.fst = tr;
1529             Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }
1530             (fun loc _ ->
1531             let { Types.fst = m'0; Types.snd = b } =
1532               GenMem.alloc m0 (Z.z_of_nat Nat.O)
1533                 (Z.z_of_nat fn.RTLabs_syntax.f_stacksize)
1534             in
1535             (fun _ ->
1536             jmeq_hackT (Errors.OK { Types.fst = Events.e0; Types.snd = (State
1537               ({ func = fn; locals = loc; next =
1538               (Types.pi1 fn.RTLabs_syntax.f_entry); sp = b; retdst =
1539               retdst0 }, stk, m'0)) }) (Errors.OK { Types.fst = tr;
1540               Types.snd = (Callstate (vf', fd', args', dst', fs', m')) })
1541               (fun _ ->
1542               Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1543                 Events.e0; Types.snd = (State ({ func = fn; locals = loc;
1544                 next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp = b; retdst =
1545                 retdst0 }, stk, m'0)) }) (Errors.OK { Types.fst = tr;
1546                 Types.snd = (Callstate (vf', fd', args', dst', fs', m')) })
1547                 __ (fun _ ->
1548                 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0;
1549                   Types.snd = (State ({ func = fn; locals = loc; next =
1550                   (Types.pi1 fn.RTLabs_syntax.f_entry); sp = b; retdst =
1551                   retdst0 }, stk, m'0)) } { Types.fst = tr; Types.snd =
1552                   (Callstate (vf', fd', args', dst', fs', m')) } __ (fun _ ->
1553                   Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1554                     Obj.magic state_jmdiscr (State ({ func = fn; locals =
1555                       loc; next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp =
1556                       b; retdst = retdst0 }, stk, m'0)) (Callstate (vf', fd',
1557                       args', dst', fs', m')) __) tr __ __))))))
1558       | AST.External fn ->
1559         (fun args0 retdst0 stk m0 tr vf' fd' args' dst' fs' m' _ ->
1560           IOMonad.bindIO_value
1561             (IOMonad.err_to_io
1562               (IO.check_eventval_list args0 fn.AST.ef_sig.AST.sig_args))
1563             (fun evargs ->
1564             Obj.magic
1565               (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
1566                 (Obj.magic
1567                   (IO.do_io fn.AST.ef_id evargs
1568                     (AST.proj_sig_res fn.AST.ef_sig))) (fun evres ->
1569                 Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
1570                   (Events.eextcall fn.AST.ef_id evargs
1571                     (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
1572                   Types.snd = (Returnstate ((Types.Some
1573                   (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)),
1574                   retdst0, stk, m0)) }))) { Types.fst = tr; Types.snd =
1575             (Callstate (vf', fd', args', dst', fs', m')) } (fun evargs _ _ ->
1576             Obj.magic IOMonad.iO_discr (IOMonad.Interact ({ IO.io_function =
1577               fn.AST.ef_id; IO.io_args = evargs; IO.io_in_typ =
1578               (AST.proj_sig_res fn.AST.ef_sig) }, (fun res ->
1579               IOMonad.bindIO (IOMonad.Value res) (fun evres ->
1580                 Obj.magic
1581                   (Monad.m_return0 (Monad.max_def IOMonad.iOMonad)
1582                     { Types.fst =
1583                     (Events.eextcall fn.AST.ef_id evargs
1584                       (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
1585                     Types.snd = (Returnstate ((Types.Some
1586                     (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)),
1587                     retdst0, stk, m0)) }))))) (IOMonad.Value { Types.fst =
1588               tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) })
1589               __))) x x0 x1 x2
1590    | Returnstate (v, r, clearme0, x) ->
1591      (match clearme0 with
1592       | List.Nil ->
1593         (fun m0 tr vf' fd' args' dst' fs' m' ->
1594           match v with
1595           | Types.None ->
1596             (fun _ ->
1597               Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons
1598                 ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil)))
1599                 (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf',
1600                 fd', args', dst', fs', m')) }) __)
1601           | Types.Some clearme1 ->
1602             (match clearme1 with
1603              | Values.Vundef ->
1604                (fun _ ->
1605                  Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons
1606                    ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil)))
1607                    (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate
1608                    (vf', fd', args', dst', fs', m')) }) __)
1609              | Values.Vint (clearme2, x0) ->
1610                (match clearme2 with
1611                 | AST.I8 ->
1612                   (fun r0 _ ->
1613                     jmeq_hackT (IOMonad.Wrong (List.Cons ((Errors.MSG
1614                       ErrorMessages.ReturnMismatch), List.Nil)))
1615                       (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate
1616                       (vf', fd', args', dst', fs', m')) }) (fun _ ->
1617                       Obj.magic IOMonad.iO_jmdiscr (IOMonad.Wrong (List.Cons
1618                         ((Errors.MSG ErrorMessages.ReturnMismatch),
1619                         List.Nil))) (IOMonad.Value { Types.fst = tr;
1620                         Types.snd = (Callstate (vf', fd', args', dst', fs',
1621                         m')) }) __))
1622                 | AST.I16 ->
1623                   (fun r0 _ ->
1624                     jmeq_hackT (IOMonad.Wrong (List.Cons ((Errors.MSG
1625                       ErrorMessages.ReturnMismatch), List.Nil)))
1626                       (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate
1627                       (vf', fd', args', dst', fs', m')) }) (fun _ ->
1628                       Obj.magic IOMonad.iO_jmdiscr (IOMonad.Wrong (List.Cons
1629                         ((Errors.MSG ErrorMessages.ReturnMismatch),
1630                         List.Nil))) (IOMonad.Value { Types.fst = tr;
1631                         Types.snd = (Callstate (vf', fd', args', dst', fs',
1632                         m')) }) __))
1633                 | AST.I32 ->
1634                   (fun r0 _ ->
1635                     jmeq_hackT (IOMonad.Value { Types.fst = List.Nil;
1636                       Types.snd = (Finalstate r0) }) (IOMonad.Value
1637                       { Types.fst = tr; Types.snd = (Callstate (vf', fd',
1638                       args', dst', fs', m')) }) (fun _ ->
1639                       Obj.magic IOMonad.iO_jmdiscr (IOMonad.Value
1640                         { Types.fst = List.Nil; Types.snd = (Finalstate
1641                         r0) }) (IOMonad.Value { Types.fst = tr; Types.snd =
1642                         (Callstate (vf', fd', args', dst', fs', m')) }) __
1643                         (fun _ ->
1644                         Obj.magic Globalenvs.prod_jmdiscr { Types.fst =
1645                           List.Nil; Types.snd = (Finalstate r0) }
1646                           { Types.fst = tr; Types.snd = (Callstate (vf', fd',
1647                           args', dst', fs', m')) } __ (fun _ ->
1648                           Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1649                             Obj.magic state_jmdiscr (Finalstate r0)
1650                               (Callstate (vf', fd', args', dst', fs', m')) __)
1651                             tr __ __))))) x0
1652              | Values.Vnull ->
1653                (fun _ ->
1654                  Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons
1655                    ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil)))
1656                    (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate
1657                    (vf', fd', args', dst', fs', m')) }) __)
1658              | Values.Vptr a ->
1659                (fun _ ->
1660                  Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons
1661                    ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil)))
1662                    (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate
1663                    (vf', fd', args', dst', fs', m')) }) __)))
1664       | List.Cons (f, fs0) ->
1665         (fun m0 tr vf' fd' args' dst' fs' m' _ ->
1666           IOMonad.bind_res_value
1667             (match r with
1668              | Types.None ->
1669                (match v with
1670                 | Types.None -> Errors.OK f.locals
1671                 | Types.Some x0 ->
1672                   Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
1673              | Types.Some d ->
1674                (match v with
1675                 | Types.None ->
1676                   Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
1677                 | Types.Some v' -> reg_store d v' f.locals)) (fun locals0 ->
1678             Obj.magic
1679               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1680                 Events.e0; Types.snd = (State ({ func = f.func; locals =
1681                 locals0; next = f.next; sp = f.sp; retdst = f.retdst }, fs0,
1682                 m0)) })) { Types.fst = tr; Types.snd = (Callstate (vf', fd',
1683             args', dst', fs', m')) } (fun loc _ _ ->
1684             jmeq_hackT
1685               (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
1686                 Events.e0; Types.snd = (State ({ func = f.func; locals = loc;
1687                 next = f.next; sp = f.sp; retdst = f.retdst }, fs0, m0)) })
1688               (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = (Callstate
1689                 (vf', fd', args', dst', fs', m')) })) (fun _ ->
1690               Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst =
1691                 Events.e0; Types.snd = (State ({ func = f.func; locals = loc;
1692                 next = f.next; sp = f.sp; retdst = f.retdst }, fs0, m0)) })
1693                 (Errors.OK { Types.fst = tr; Types.snd = (Callstate (vf',
1694                 fd', args', dst', fs', m')) }) __ (fun _ ->
1695                 Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0;
1696                   Types.snd = (State ({ func = f.func; locals = loc; next =
1697                   f.next; sp = f.sp; retdst = f.retdst }, fs0, m0)) }
1698                   { Types.fst = tr; Types.snd = (Callstate (vf', fd', args',
1699                   dst', fs', m')) } __ (fun _ ->
1700                   Logic.eq_rect_Type0 List.Nil (fun _ _ _ ->
1701                     Obj.magic state_jmdiscr (State ({ func = f.func; locals =
1702                       loc; next = f.next; sp = f.sp; retdst = f.retdst },
1703                       fs0, m0)) (Callstate (vf', fd', args', dst', fs', m'))
1704                       __) tr __ __)))))) x
1705    | Finalstate r ->
1706      (fun tr vf' fd' args' dst' fs' m' _ ->
1707        Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons ((Errors.MSG
1708          ErrorMessages.FinalState), List.Nil))) (IOMonad.Value { Types.fst =
1709          tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __))
1710     t fid fd args dst fs m __
1711