open Preamble open Bool open Relations open Nat open Hints_declaration open Core_notation open Pts open Logic open Types open List open ErrorMessages open Option open Setoids open Monad open Jmeq open Russell open Positive open PreIdentifiers open Errors open Extra_bool open Coqlib open Values open FrontEndVal open Hide open ByteValues open Division open Z open BitVectorZ open Pointers open GenMem open FrontEndMem open Proper open PositiveMap open Deqsets open Extralib open Lists open Identifiers open Exp open Arithmetic open Vector open Div_and_mod open Util open FoldStuff open BitVector open Extranat open Integers open AST open Globalenvs open CostLabel open Events open IOMonad open IO open SmallstepExec open BitVectorTrie open Graphs open Order open Registers open FrontEndOps open RTLabs_syntax type genv = RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t type frame = { func : RTLabs_syntax.internal_function; locals : Values.val0 Registers.register_env; next : Graphs.label; sp : Pointers.block; retdst : Registers.register Types.option } (** val frame_rect_Type4 : (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> 'a1) -> frame -> 'a1 **) let rec frame_rect_Type4 h_mk_frame x_23982 = let { func = func0; locals = locals0; next = next0; sp = sp0; retdst = retdst0 } = x_23982 in h_mk_frame func0 locals0 next0 __ sp0 retdst0 (** val frame_rect_Type5 : (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> 'a1) -> frame -> 'a1 **) let rec frame_rect_Type5 h_mk_frame x_23984 = let { func = func0; locals = locals0; next = next0; sp = sp0; retdst = retdst0 } = x_23984 in h_mk_frame func0 locals0 next0 __ sp0 retdst0 (** val frame_rect_Type3 : (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> 'a1) -> frame -> 'a1 **) let rec frame_rect_Type3 h_mk_frame x_23986 = let { func = func0; locals = locals0; next = next0; sp = sp0; retdst = retdst0 } = x_23986 in h_mk_frame func0 locals0 next0 __ sp0 retdst0 (** val frame_rect_Type2 : (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> 'a1) -> frame -> 'a1 **) let rec frame_rect_Type2 h_mk_frame x_23988 = let { func = func0; locals = locals0; next = next0; sp = sp0; retdst = retdst0 } = x_23988 in h_mk_frame func0 locals0 next0 __ sp0 retdst0 (** val frame_rect_Type1 : (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> 'a1) -> frame -> 'a1 **) let rec frame_rect_Type1 h_mk_frame x_23990 = let { func = func0; locals = locals0; next = next0; sp = sp0; retdst = retdst0 } = x_23990 in h_mk_frame func0 locals0 next0 __ sp0 retdst0 (** val frame_rect_Type0 : (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> 'a1) -> frame -> 'a1 **) let rec frame_rect_Type0 h_mk_frame x_23992 = let { func = func0; locals = locals0; next = next0; sp = sp0; retdst = retdst0 } = x_23992 in h_mk_frame func0 locals0 next0 __ sp0 retdst0 (** val func : frame -> RTLabs_syntax.internal_function **) let rec func xxx = xxx.func (** val locals : frame -> Values.val0 Registers.register_env **) let rec locals xxx = xxx.locals (** val next : frame -> Graphs.label **) let rec next xxx = xxx.next (** val sp : frame -> Pointers.block **) let rec sp xxx = xxx.sp (** val retdst : frame -> Registers.register Types.option **) let rec retdst xxx = xxx.retdst (** val frame_inv_rect_Type4 : frame -> (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> __ -> 'a1) -> 'a1 **) let frame_inv_rect_Type4 hterm h1 = let hcut = frame_rect_Type4 h1 hterm in hcut __ (** val frame_inv_rect_Type3 : frame -> (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> __ -> 'a1) -> 'a1 **) let frame_inv_rect_Type3 hterm h1 = let hcut = frame_rect_Type3 h1 hterm in hcut __ (** val frame_inv_rect_Type2 : frame -> (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> __ -> 'a1) -> 'a1 **) let frame_inv_rect_Type2 hterm h1 = let hcut = frame_rect_Type2 h1 hterm in hcut __ (** val frame_inv_rect_Type1 : frame -> (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> __ -> 'a1) -> 'a1 **) let frame_inv_rect_Type1 hterm h1 = let hcut = frame_rect_Type1 h1 hterm in hcut __ (** val frame_inv_rect_Type0 : frame -> (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env -> Graphs.label -> __ -> Pointers.block -> Registers.register Types.option -> __ -> 'a1) -> 'a1 **) let frame_inv_rect_Type0 hterm h1 = let hcut = frame_rect_Type0 h1 hterm in hcut __ (** val frame_jmdiscr : frame -> frame -> __ **) let frame_jmdiscr x y = Logic.eq_rect_Type2 x (let { func = a0; locals = a1; next = a2; sp = a4; retdst = a5 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y (** val adv : Graphs.label -> frame -> frame **) let adv l f = { func = f.func; locals = f.locals; next = l; sp = f.sp; retdst = f.retdst } type state = | State of frame * frame List.list * GenMem.mem | Callstate of AST.ident * RTLabs_syntax.internal_function AST.fundef * Values.val0 List.list * Registers.register Types.option * frame List.list * GenMem.mem | Returnstate of Values.val0 Types.option * Registers.register Types.option * frame List.list * GenMem.mem | Finalstate of Integers.int (** val state_rect_Type4 : (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **) let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function | State (f, fs, m) -> h_State f fs m | Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m | Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m | Finalstate r -> h_Finalstate r (** val state_rect_Type5 : (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **) let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function | State (f, fs, m) -> h_State f fs m | Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m | Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m | Finalstate r -> h_Finalstate r (** val state_rect_Type3 : (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **) let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function | State (f, fs, m) -> h_State f fs m | Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m | Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m | Finalstate r -> h_Finalstate r (** val state_rect_Type2 : (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **) let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function | State (f, fs, m) -> h_State f fs m | Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m | Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m | Finalstate r -> h_Finalstate r (** val state_rect_Type1 : (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **) let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function | State (f, fs, m) -> h_State f fs m | Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m | Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m | Finalstate r -> h_Finalstate r (** val state_rect_Type0 : (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **) let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function | State (f, fs, m) -> h_State f fs m | Callstate (id, fd, args, dst, stk, m) -> h_Callstate id fd args dst stk m | Returnstate (rtv, dst, stk, m) -> h_Returnstate rtv dst stk m | Finalstate r -> h_Finalstate r (** val state_inv_rect_Type4 : state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> Registers.register Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **) let state_inv_rect_Type4 hterm h1 h2 h3 h4 = let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __ (** val state_inv_rect_Type3 : state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> Registers.register Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **) let state_inv_rect_Type3 hterm h1 h2 h3 h4 = let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __ (** val state_inv_rect_Type2 : state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> Registers.register Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **) let state_inv_rect_Type2 hterm h1 h2 h3 h4 = let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __ (** val state_inv_rect_Type1 : state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> Registers.register Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **) let state_inv_rect_Type1 hterm h1 h2 h3 h4 = let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __ (** val state_inv_rect_Type0 : state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> Registers.register Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **) let state_inv_rect_Type0 hterm h1 h2 h3 h4 = let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __ (** val state_jmdiscr : state -> state -> __ **) let state_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | State (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __) | Callstate (a0, a1, a2, a3, a4, a5) -> Obj.magic (fun _ dH -> dH __ __ __ __ __ __) | Returnstate (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __) | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y (** val build_state : frame -> frame List.list -> GenMem.mem -> Graphs.label -> state **) let build_state f fs m n = State ((adv n f), fs, m) (** val next_instruction : frame -> RTLabs_syntax.statement **) let next_instruction f = Identifiers.lookup_present PreIdentifiers.LabelTag f.func.RTLabs_syntax.f_graph f.next (** val init_locals : (Registers.register, AST.typ) Types.prod List.list -> Values.val0 Registers.register_env **) let init_locals = List.foldr (fun idt en -> let { Types.fst = id; Types.snd = ty } = idt in Identifiers.add PreIdentifiers.RegisterTag en id Values.Vundef) (Identifiers.empty_map PreIdentifiers.RegisterTag) (** val reg_store : PreIdentifiers.identifier -> Values.val0 -> Values.val0 Identifiers.identifier_map -> Values.val0 Identifiers.identifier_map Errors.res **) let reg_store reg v locals0 = Identifiers.update PreIdentifiers.RegisterTag locals0 reg v (** val params_store : (Registers.register, AST.typ) Types.prod List.list -> Values.val0 List.list -> Values.val0 Registers.register_env -> Values.val0 Registers.register_env Errors.res **) let rec params_store rs vs locals0 = match rs with | List.Nil -> (match vs with | List.Nil -> Errors.OK locals0 | List.Cons (x, x0) -> Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)) | List.Cons (rt, rst) -> (match vs with | List.Nil -> Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters) | List.Cons (v, vst) -> let { Types.fst = r; Types.snd = ty } = rt in let locals' = Identifiers.add PreIdentifiers.RegisterTag locals0 r v in params_store rst vst locals') (** val reg_retrieve : Values.val0 Registers.register_env -> Registers.register -> Values.val0 Errors.res **) let reg_retrieve locals0 reg = Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadRegister), (List.Cons ((Errors.CTX (PreIdentifiers.RegisterTag, reg)), List.Nil)))) (Identifiers.lookup PreIdentifiers.RegisterTag locals0 reg) (** val eval_statement : genv -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod) IOMonad.iO **) let eval_statement ge = function | State (f, fs, m) -> let s = next_instruction f in (match s with | RTLabs_syntax.St_skip l -> (fun _ -> Obj.magic (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = Events.e0; Types.snd = (build_state f fs m l) })) | RTLabs_syntax.St_cost (cl, l) -> (fun _ -> Obj.magic (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = (Events.echarge cl); Types.snd = (build_state f fs m l) })) | RTLabs_syntax.St_const (x, r, cst, l) -> (fun _ -> IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.FailedConstant) (FrontEndOps.eval_constant x (Globalenvs.find_symbol ge) f.sp cst))) (fun v -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_store r v f.locals)) (fun locals0 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = f.func; locals = locals0; next = l; sp = f.sp; retdst = f.retdst }, fs, m)) }))))) | RTLabs_syntax.St_op1 (x, x0, op, dst, src, l) -> (fun _ -> IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve f.locals src)) (fun v -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp) (FrontEndOps.eval_unop x0 x op v))) (fun v' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_store dst v' f.locals)) (fun locals0 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = f.func; locals = locals0; next = l; sp = f.sp; retdst = f.retdst }, fs, m)) })))))) | RTLabs_syntax.St_op2 (x, x0, x1, op, dst, src1, src2, l) -> (fun _ -> IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve f.locals src1)) (fun v1 -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve f.locals src2)) (fun v2 -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp) (FrontEndOps.eval_binop m x0 x1 x op v1 v2))) (fun v' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_store dst v' f.locals)) (fun locals0 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = f.func; locals = locals0; next = l; sp = f.sp; retdst = f.retdst }, fs, m)) }))))))) | RTLabs_syntax.St_load (chunk, addr, dst, l) -> (fun _ -> IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve f.locals addr)) (fun vaddr -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad) (FrontEndMem.loadv chunk m vaddr))) (fun v -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_store dst v f.locals)) (fun locals0 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = f.func; locals = locals0; next = l; sp = f.sp; retdst = f.retdst }, fs, m)) })))))) | RTLabs_syntax.St_store (chunk, addr, src, l) -> (fun _ -> IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve f.locals addr)) (fun vaddr -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve f.locals src)) (fun v -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore) (FrontEndMem.storev chunk m vaddr v))) (fun m' -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (build_state f fs m' l) })))))) | RTLabs_syntax.St_call_id (id, args, dst, l) -> (fun _ -> IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil)))) (Globalenvs.find_symbol ge id))) (fun b -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil)))) (Globalenvs.find_funct_ptr ge b))) (fun fd -> Monad.m_bind0 (Monad.max_def Errors.res0) (Monad.m_list_map (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve f.locals)) args) (fun vs -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Callstate (id, fd, vs, dst, (List.Cons ((adv l f), fs)), m)) })))))) | RTLabs_syntax.St_call_ptr (frs, args, dst, l) -> (fun _ -> IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve f.locals frs)) (fun fv -> Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.BadFunction) (Globalenvs.find_funct_id ge fv))) (fun fd id -> Monad.m_bind0 (Monad.max_def Errors.res0) (Monad.m_list_map (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve f.locals)) args) (fun vs -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Callstate (id, fd, vs, dst, (List.Cons ((adv l f), fs)), m)) })))))) | RTLabs_syntax.St_cond (src, ltrue, lfalse) -> (fun _ -> IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve f.locals src)) (fun v -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Values.eval_bool_of_val v)) (fun b -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (build_state f fs m (match b with | Bool.True -> ltrue | Bool.False -> lfalse)) }))))) | RTLabs_syntax.St_return -> (fun _ -> IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (match f.func.RTLabs_syntax.f_result with | Types.None -> Monad.m_return0 (Monad.max_def Errors.res0) Types.None | Types.Some rt -> let { Types.fst = r; Types.snd = ty } = rt in Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve f.locals r)) (fun v -> Monad.m_return0 (Monad.max_def Errors.res0) (Types.Some v))) (fun v -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Returnstate (v, f.retdst, fs, (GenMem.free m f.sp))) }))))) __ | Callstate (x, fd, params, dst, fs, m) -> (match fd with | AST.Internal fn -> IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (params_store fn.RTLabs_syntax.f_params params (init_locals fn.RTLabs_syntax.f_locals))) (fun locals0 -> let { Types.fst = m'; Types.snd = sp0 } = GenMem.alloc m (Z.z_of_nat Nat.O) (Z.z_of_nat fn.RTLabs_syntax.f_stacksize) in Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = fn; locals = locals0; next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp = sp0; retdst = dst }, fs, m')) }))) | AST.External fn -> Obj.magic (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (Obj.magic (IOMonad.err_to_io (IO.check_eventval_list params fn.AST.ef_sig.AST.sig_args))) (fun evargs -> Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (Obj.magic (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig))) (fun evres -> Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = (Events.eextcall fn.AST.ef_id evargs (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres)); Types.snd = (Returnstate ((Types.Some (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)), dst, fs, m)) })))) | Returnstate (v, dst, fs, m) -> (match fs with | List.Nil -> (fun _ -> (match v with | Types.None -> (fun _ -> IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))) | Types.Some v' -> (fun _ -> (match v' with | Values.Vundef -> (fun _ -> IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))) | Values.Vint (sz, r) -> (fun _ -> IOMonad.err_to_io ((match sz with | AST.I8 -> (fun x -> Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)) | AST.I16 -> (fun x -> Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)) | AST.I32 -> (fun r0 -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Finalstate r0) }))) r)) | Values.Vnull -> (fun _ -> IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))) | Values.Vptr x -> (fun _ -> IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)))) __)) __) | List.Cons (f, fs') -> (fun _ -> IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (match dst with | Types.None -> (match v with | Types.None -> Obj.magic (Errors.OK f.locals) | Types.Some x -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))) | Types.Some d -> (match v with | Types.None -> Obj.magic (Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)) | Types.Some v' -> Obj.magic (reg_store d v' f.locals))) (fun locals0 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = f.func; locals = locals0; next = f.next; sp = f.sp; retdst = f.retdst }, fs', m)) }))))) __ | Finalstate r -> IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.FinalState)) (** val rTLabs_is_final : state -> Integers.int Types.option **) let rTLabs_is_final = function | State (x, x0, x1) -> Types.None | Callstate (x, x0, x1, x2, x3, x4) -> Types.None | Returnstate (x, x0, x1, x2) -> Types.None | Finalstate r -> Types.Some r (** val rTLabs_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system **) let rTLabs_exec = { SmallstepExec.is_final = (fun x -> Obj.magic rTLabs_is_final); SmallstepExec.step = (Obj.magic eval_statement) } (** val make_global : RTLabs_syntax.rTLabs_program -> genv **) let make_global p = Globalenvs.globalenv (fun x -> x) p (** val make_initial_state : RTLabs_syntax.rTLabs_program -> state Errors.res **) let make_initial_state p = let ge = make_global p in Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Globalenvs.init_mem (fun x -> x) p)) (fun m -> let main = p.AST.prog_main in Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, main)), List.Nil)))) (Globalenvs.find_symbol ge main))) (fun b -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, main)), List.Nil)))) (Globalenvs.find_funct_ptr ge b))) (fun f -> Obj.magic (Errors.OK (Callstate (main, f, List.Nil, Types.None, List.Nil, m))))))) (** val rTLabs_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec **) let rTLabs_fullexec = { SmallstepExec.es1 = rTLabs_exec; SmallstepExec.make_global = (Obj.magic make_global); SmallstepExec.make_initial_state = (Obj.magic make_initial_state) } (** val bind_ok : 'a1 Errors.res -> ('a1 -> 'a2 Errors.res) -> 'a2 -> ('a1 -> __ -> __ -> 'a3) -> 'a3 **) let bind_ok clearme f v x = (match clearme with | Errors.OK a -> (fun f0 v0 _ h _ -> h a __ __) | Errors.Error m -> (fun f0 v0 _ h _ -> Obj.magic Errors.res_discr (Errors.Error m) (Errors.OK v0) __)) f v __ x __ (** val jmeq_hackT : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2 **) let jmeq_hackT x y auto = auto __ (** val func_block_of_exec : genv -> state -> Events.trace -> AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list -> Registers.register Types.option -> frame List.list -> GenMem.mem -> Pointers.block Types.sig0 **) let func_block_of_exec ge clearme t fid fd args dst fs m = (match clearme with | State (clearme0, x, x0) -> (let { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } = clearme0 in (fun fs0 m0 tr fid0 fd0 args0 dst' fs' m' -> (match next_instruction { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } with | RTLabs_syntax.St_skip l -> (fun _ _ -> jmeq_hackT (IOMonad.Value { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) (fun _ -> Obj.magic IOMonad.iO_jmdiscr (IOMonad.Value { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 m0 l) } { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (State ((adv l { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs', m')) __) tr __ __)))) | RTLabs_syntax.St_cost (c, l) -> (fun _ _ -> jmeq_hackT (IOMonad.Value { Types.fst = (Events.echarge c); Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) (fun _ -> Obj.magic IOMonad.iO_jmdiscr (IOMonad.Value { Types.fst = (Events.echarge c); Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 m0 l) }) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = (Events.echarge c); Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 m0 l) } { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 (List.Cons ((Events.EVcost c), List.Nil)) (fun _ _ _ -> Obj.magic state_jmdiscr (State ((adv l { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs', m')) __) tr __ __)))) | RTLabs_syntax.St_const (t0, r, c, l) -> (fun _ _ -> IOMonad.bind_res_value (Errors.opt_to_res (Errors.msg ErrorMessages.FailedConstant) (FrontEndOps.eval_constant t0 (Globalenvs.find_symbol ge) sp0 c)) (fun v -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_store r v locals0)) (fun locals1 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v _ _ -> bind_ok (reg_store r v locals0) (fun x1 -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = x1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun locals' _ _ -> jmeq_hackT (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = locals'; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ -> Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = locals'; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = locals'; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) } { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (State ({ func = func0; locals = locals'; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs', m')) __) tr __ __)))))) | RTLabs_syntax.St_op1 (t1, t2, op, r1, r2, l) -> (fun _ _ -> IOMonad.bind_res_value (reg_retrieve locals0 r2) (fun v -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp) (FrontEndOps.eval_unop t2 t1 op v))) (fun v' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_store r1 v' locals0)) (fun locals1 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v _ _ -> bind_ok (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp) (FrontEndOps.eval_unop t2 t1 op v)) (fun x1 -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_store r1 x1 locals0)) (fun locals1 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v' _ _ -> bind_ok (reg_store r1 v' locals0) (fun x1 -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = x1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun loc _ _ -> jmeq_hackT (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ -> Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) } { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (State ({ func = func0; locals = loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs', m')) __) tr __ __))))))) | RTLabs_syntax.St_op2 (t1, t2, t', op, r1, r2, r3, l) -> (fun _ _ -> IOMonad.bind_res_value (reg_retrieve locals0 r2) (fun v1 -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve locals0 r3)) (fun v2 -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp) (FrontEndOps.eval_binop m0 t2 t' t1 op v1 v2))) (fun v' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_store r1 v' locals0)) (fun locals1 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v1 _ _ -> bind_ok (reg_retrieve locals0 r3) (fun x1 -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp) (FrontEndOps.eval_binop m0 t2 t' t1 op v1 x1))) (fun v' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_store r1 v' locals0)) (fun locals1 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v2 _ _ -> bind_ok (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp) (FrontEndOps.eval_binop m0 t2 t' t1 op v1 v2)) (fun x1 -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_store r1 x1 locals0)) (fun locals1 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v' _ _ -> bind_ok (reg_store r1 v' locals0) (fun x1 -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = x1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun loc _ _ -> jmeq_hackT (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ -> Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) } { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (State ({ func = func0; locals = loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs', m')) __) tr __ __)))))))) | RTLabs_syntax.St_load (ch, r1, r2, l) -> (fun _ _ -> IOMonad.bind_res_value (reg_retrieve locals0 r1) (fun vaddr -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad) (FrontEndMem.loadv ch m0 vaddr))) (fun v -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_store r2 v locals0)) (fun locals1 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v _ _ -> bind_ok (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad) (FrontEndMem.loadv ch m0 v)) (fun x1 -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_store r2 x1 locals0)) (fun locals1 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = locals1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v' _ _ -> bind_ok (reg_store r2 v' locals0) (fun x1 -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = x1; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) })) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun loc _ _ -> jmeq_hackT (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ -> Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) }) (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; Types.snd = (State ({ func = func0; locals = loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) } { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (State ({ func = func0; locals = loc; next = l; sp = sp0; retdst = dst0 }, fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs', m')) __) tr __ __))))))) | RTLabs_syntax.St_store (ch, r1, r2, l) -> (fun _ _ -> IOMonad.bind_res_value (reg_retrieve locals0 r1) (fun vaddr -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve locals0 r2)) (fun v -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore) (FrontEndMem.storev ch m0 vaddr v))) (fun m'0 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 m'0 l) })))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v _ _ -> bind_ok (reg_retrieve locals0 r2) (fun x1 -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore) (FrontEndMem.storev ch m0 v x1))) (fun m'0 -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 m'0 l) }))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v' _ _ -> bind_ok (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore) (FrontEndMem.storev ch m0 v v')) (fun x1 -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 x1 l) })) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun loc _ _ -> jmeq_hackT (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 loc l) }) (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ -> Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 loc l) }) (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 loc l) } { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (State ((adv l { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 }), fs0, loc)) (Callstate (fid0, fd0, args0, dst', fs', m')) __) tr __ __))))))) | RTLabs_syntax.St_call_id (x1, rs, or0, l) -> (fun _ _ -> IOMonad.bind_res_value (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingSymbol), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, x1)), List.Nil)))) (Globalenvs.find_symbol ge x1)) (fun b -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, x1)), List.Nil)))) (Globalenvs.find_funct_ptr ge b))) (fun fd1 -> Monad.m_bind0 (Monad.max_def Errors.res0) (Monad.m_list_map (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve locals0)) rs) (fun vs -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Callstate (x1, fd1, vs, or0, (List.Cons ((adv l { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 }), fs0)), m0)) })))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v _ _ -> bind_ok (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, x1)), List.Nil)))) (Globalenvs.find_funct_ptr ge v)) (fun x2 -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Monad.m_list_map (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve locals0)) rs) (fun vs -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Callstate (x1, x2, vs, or0, (List.Cons ((adv l { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 }), fs0)), m0)) }))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun fd' _ _ -> bind_ok (Obj.magic (Monad.m_list_map (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve locals0)) rs)) (fun x2 -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Callstate (x1, fd', x2, or0, (List.Cons ((adv l { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 }), fs0)), m0)) })) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun vs _ _ -> jmeq_hackT (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Callstate (x1, fd', vs, or0, (List.Cons ((adv l { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 }), fs0)), m0)) }) (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ -> Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = List.Nil; Types.snd = (Callstate (x1, fd', vs, or0, (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)), m0)) }) (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = List.Nil; Types.snd = (Callstate (x1, fd', vs, or0, (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)), m0)) } { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (Callstate (x1, fd', vs, or0, (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)), m0)) (Callstate (fid0, fd0, args0, dst', fs', m')) __ (fun _ -> Extralib.eq_rect_Type0_r fid0 (fun _ _ _ _ _ _ _ -> Extralib.eq_rect_Type0_r fd0 (fun _ _ _ _ _ -> Extralib.eq_rect_Type0_r args0 (fun _ _ _ _ _ -> Extralib.eq_rect_Type0_r dst' (fun _ _ _ _ _ -> Logic.eq_rect_Type0 (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)) (fun _ _ _ _ -> Extralib.eq_rect_Type0_r m' (fun _ _ _ -> Logic.streicherK (Errors.OK { Types.fst = List.Nil; Types.snd = (Callstate (fid0, fd0, args0, dst', (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)), m')) }) (Logic.streicherK { Types.fst = List.Nil; Types.snd = (Callstate (fid0, fd0, args0, dst', (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)), m')) } (Logic.streicherK (Callstate (fid0, fd0, args0, dst', (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)), m')) v))) m0 __ __ __) fs' __ __ __) or0 __ __ __ __) vs __ __ __ __) fd' __ __ __ __) x1 __ __ __ __ __ __)) tr __ __))))))) | RTLabs_syntax.St_call_ptr (x1, rs, or0, l) -> (fun _ _ -> IOMonad.bind_res_value (reg_retrieve locals0 x1) (fun fv -> Obj.magic (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.BadFunction) (Globalenvs.find_funct_id ge fv))) (fun fd1 id -> Monad.m_bind0 (Monad.max_def Errors.res0) (Monad.m_list_map (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve locals0)) rs) (fun vs -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Callstate (id, fd1, vs, or0, (List.Cons ((adv l { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 }), fs0)), m0)) })))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v _ _ -> bind_ok (Errors.opt_to_res (Errors.msg ErrorMessages.BadFunction) (Globalenvs.find_funct_id ge v)) (fun x2 -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Monad.m_list_map (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve locals0)) rs) (fun vs -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Callstate (x2.Types.snd, x2.Types.fst, vs, or0, (List.Cons ((adv l { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 }), fs0)), m0)) }))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun fd' _ _ -> bind_ok (Obj.magic (Monad.m_list_map (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve locals0)) rs)) (fun x2 -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Callstate (fd'.Types.snd, fd'.Types.fst, x2, or0, (List.Cons ((adv l { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 }), fs0)), m0)) })) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun vs _ _ -> jmeq_hackT (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Callstate (fd'.Types.snd, fd'.Types.fst, vs, or0, (List.Cons ((adv l { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 }), fs0)), m0)) }) (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ -> Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = List.Nil; Types.snd = (Callstate (fd'.Types.snd, fd'.Types.fst, vs, or0, (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)), m0)) }) (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = List.Nil; Types.snd = (Callstate (fd'.Types.snd, fd'.Types.fst, vs, or0, (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)), m0)) } { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (Callstate (fd'.Types.snd, fd'.Types.fst, vs, or0, (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)), m0)) (Callstate (fid0, fd0, args0, dst', fs', m')) __ (fun _ -> Logic.eq_rect_Type0 fd'.Types.snd (fun _ _ _ _ -> Logic.eq_rect_Type0 fd'.Types.fst (fun _ _ _ _ -> Extralib.eq_rect_Type0_r args0 (fun _ _ _ _ _ -> Extralib.eq_rect_Type0_r dst' (fun _ _ _ _ _ -> Logic.eq_rect_Type0 (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)) (fun _ _ _ _ -> Extralib.eq_rect_Type0_r m' (fun _ _ _ -> Logic.streicherK (Errors.OK { Types.fst = List.Nil; Types.snd = (Callstate (fd'.Types.snd, fd'.Types.fst, args0, dst', (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)), m')) }) (Logic.streicherK { Types.fst = List.Nil; Types.snd = (Callstate (fd'.Types.snd, fd'.Types.fst, args0, dst', (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)), m')) } (Logic.streicherK (Callstate (fd'.Types.snd, fd'.Types.fst, args0, dst', (List.Cons ({ func = func0; locals = locals0; next = l; sp = sp0; retdst = dst0 }, fs0)), m')) ((match v with | Values.Vundef -> (fun _ -> Obj.magic Errors.res_discr (Errors.Error (List.Cons ((Errors.MSG ErrorMessages.BadFunction), List.Nil))) (Errors.OK fd') __) | Values.Vint (a, b) -> (fun _ -> Obj.magic Errors.res_discr (Errors.Error (List.Cons ((Errors.MSG ErrorMessages.BadFunction), List.Nil))) (Errors.OK fd') __) | Values.Vnull -> (fun _ -> Obj.magic Errors.res_discr (Errors.Error (List.Cons ((Errors.MSG ErrorMessages.BadFunction), List.Nil))) (Errors.OK fd') __) | Values.Vptr clearme1 -> let { Pointers.pblock = b; Pointers.poff = off } = clearme1 in let { Types.fst = fd''; Types.snd = fid' } = fd' in (fun _ -> b)) __)))) m0 __ __ __) fs' __ __ __) or0 __ __ __ __) vs __ __ __ __) fd0 __ __ __) fid0 __ __ __)) tr __ __))))))) | RTLabs_syntax.St_cond (r, l1, l2) -> (fun _ _ -> IOMonad.bind_res_value (reg_retrieve locals0 r) (fun v -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Values.eval_bool_of_val v)) (fun b -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 m0 (match b with | Bool.True -> l1 | Bool.False -> l2)) }))) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v _ _ -> bind_ok (Values.eval_bool_of_val v) (fun x1 -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 m0 (match x1 with | Bool.True -> l1 | Bool.False -> l2)) })) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun b _ _ -> jmeq_hackT (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 m0 (match b with | Bool.True -> l1 | Bool.False -> l2)) }) (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ -> Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 m0 (match b with | Bool.True -> l1 | Bool.False -> l2)) }) (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; Types.snd = (build_state { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 } fs0 m0 (match b with | Bool.True -> l1 | Bool.False -> l2)) } { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (State ((adv (match b with | Bool.True -> l1 | Bool.False -> l2) { func = func0; locals = locals0; next = next0; sp = sp0; retdst = dst0 }), fs0, m0)) (Callstate (fid0, fd0, args0, dst', fs', m')) __) tr __ __)))))) | RTLabs_syntax.St_return -> (fun _ _ -> IOMonad.bind_res_value (match func0.RTLabs_syntax.f_result with | Types.None -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) Types.None) | Types.Some rt -> let { Types.fst = r; Types.snd = ty } = rt in Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (reg_retrieve locals0 r)) (fun v -> Monad.m_return0 (Monad.max_def Errors.res0) (Types.Some v)))) (fun v -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Returnstate (v, dst0, fs0, (GenMem.free m0 sp0))) })) { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } (fun v -> match func0.RTLabs_syntax.f_result with | Types.None -> (fun _ _ -> jmeq_hackT (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Returnstate (v, dst0, fs0, (GenMem.free m0 sp0))) }) (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ -> Obj.magic Errors.res_discr (Errors.OK Types.None) (Errors.OK v) __ (Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = Events.e0; Types.snd = (Returnstate (v, dst0, fs0, (GenMem.free m0 sp0))) }) (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; Types.snd = (Returnstate (v, dst0, fs0, (GenMem.free m0 sp0))) } { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (Returnstate (v, dst0, fs0, (GenMem.free m0 sp0))) (Callstate (fid0, fd0, args0, dst', fs', m')) __) tr __ __))))) | Types.Some clearme1 -> let { Types.fst = r; Types.snd = t0 } = clearme1 in (fun _ -> bind_ok (reg_retrieve locals0 r) (fun x1 -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) (Types.Some x1))) v (fun v0 _ _ _ -> jmeq_hackT (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (Returnstate (v, dst0, fs0, (GenMem.free m0 sp0))) }) (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) })) (fun _ -> Obj.magic Errors.res_discr (Errors.OK (Types.Some v0)) (Errors.OK v) __ (Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = Events.e0; Types.snd = (Returnstate (v, dst0, fs0, (GenMem.free m0 sp0))) }) (Errors.OK { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; Types.snd = (Returnstate (v, dst0, fs0, (GenMem.free m0 sp0))) } { Types.fst = tr; Types.snd = (Callstate (fid0, fd0, args0, dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (Returnstate (v, dst0, fs0, (GenMem.free m0 sp0))) (Callstate (fid0, fd0, args0, dst', fs', m')) __) tr __ __))))))))) __)) x x0 | Callstate (vf, clearme0, x, x0, x1, x2) -> (match clearme0 with | AST.Internal fn -> (fun args0 retdst0 stk m0 tr vf' fd' args' dst' fs' m' _ -> IOMonad.bind_res_value (params_store fn.RTLabs_syntax.f_params args0 (init_locals fn.RTLabs_syntax.f_locals)) (fun locals0 -> let { Types.fst = m'0; Types.snd = sp0 } = GenMem.alloc m0 (Z.z_of_nat Nat.O) (Z.z_of_nat fn.RTLabs_syntax.f_stacksize) in Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = fn; locals = locals0; next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp = sp0; retdst = retdst0 }, stk, m'0)) })) { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) } (fun loc _ -> let { Types.fst = m'0; Types.snd = b } = GenMem.alloc m0 (Z.z_of_nat Nat.O) (Z.z_of_nat fn.RTLabs_syntax.f_stacksize) in (fun _ -> jmeq_hackT (Errors.OK { Types.fst = Events.e0; Types.snd = (State ({ func = fn; locals = loc; next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp = b; retdst = retdst0 }, stk, m'0)) }) (Errors.OK { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) (fun _ -> Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = Events.e0; Types.snd = (State ({ func = fn; locals = loc; next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp = b; retdst = retdst0 }, stk, m'0)) }) (Errors.OK { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; Types.snd = (State ({ func = fn; locals = loc; next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp = b; retdst = retdst0 }, stk, m'0)) } { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (State ({ func = fn; locals = loc; next = (Types.pi1 fn.RTLabs_syntax.f_entry); sp = b; retdst = retdst0 }, stk, m'0)) (Callstate (vf', fd', args', dst', fs', m')) __) tr __ __)))))) | AST.External fn -> (fun args0 retdst0 stk m0 tr vf' fd' args' dst' fs' m' _ -> IOMonad.bindIO_value (IOMonad.err_to_io (IO.check_eventval_list args0 fn.AST.ef_sig.AST.sig_args)) (fun evargs -> Obj.magic (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (Obj.magic (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig))) (fun evres -> Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = (Events.eextcall fn.AST.ef_id evargs (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres)); Types.snd = (Returnstate ((Types.Some (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)), retdst0, stk, m0)) }))) { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) } (fun evargs _ _ -> Obj.magic IOMonad.iO_discr (IOMonad.Interact ({ IO.io_function = fn.AST.ef_id; IO.io_args = evargs; IO.io_in_typ = (AST.proj_sig_res fn.AST.ef_sig) }, (fun res -> IOMonad.bindIO (IOMonad.Value res) (fun evres -> Obj.magic (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst = (Events.eextcall fn.AST.ef_id evargs (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres)); Types.snd = (Returnstate ((Types.Some (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)), retdst0, stk, m0)) }))))) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __))) x x0 x1 x2 | Returnstate (v, r, clearme0, x) -> (match clearme0 with | List.Nil -> (fun m0 tr vf' fd' args' dst' fs' m' -> match v with | Types.None -> (fun _ -> Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil))) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __) | Types.Some clearme1 -> (match clearme1 with | Values.Vundef -> (fun _ -> Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil))) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __) | Values.Vint (clearme2, x0) -> (match clearme2 with | AST.I8 -> (fun r0 _ -> jmeq_hackT (IOMonad.Wrong (List.Cons ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil))) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) (fun _ -> Obj.magic IOMonad.iO_jmdiscr (IOMonad.Wrong (List.Cons ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil))) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __)) | AST.I16 -> (fun r0 _ -> jmeq_hackT (IOMonad.Wrong (List.Cons ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil))) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) (fun _ -> Obj.magic IOMonad.iO_jmdiscr (IOMonad.Wrong (List.Cons ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil))) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __)) | AST.I32 -> (fun r0 _ -> jmeq_hackT (IOMonad.Value { Types.fst = List.Nil; Types.snd = (Finalstate r0) }) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) (fun _ -> Obj.magic IOMonad.iO_jmdiscr (IOMonad.Value { Types.fst = List.Nil; Types.snd = (Finalstate r0) }) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = List.Nil; Types.snd = (Finalstate r0) } { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (Finalstate r0) (Callstate (vf', fd', args', dst', fs', m')) __) tr __ __))))) x0 | Values.Vnull -> (fun _ -> Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil))) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __) | Values.Vptr a -> (fun _ -> Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons ((Errors.MSG ErrorMessages.ReturnMismatch), List.Nil))) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __))) | List.Cons (f, fs0) -> (fun m0 tr vf' fd' args' dst' fs' m' _ -> IOMonad.bind_res_value (match r with | Types.None -> (match v with | Types.None -> Errors.OK f.locals | Types.Some x0 -> Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)) | Types.Some d -> (match v with | Types.None -> Errors.Error (Errors.msg ErrorMessages.ReturnMismatch) | Types.Some v' -> reg_store d v' f.locals)) (fun locals0 -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = f.func; locals = locals0; next = f.next; sp = f.sp; retdst = f.retdst }, fs0, m0)) })) { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) } (fun loc _ _ -> jmeq_hackT (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = Events.e0; Types.snd = (State ({ func = f.func; locals = loc; next = f.next; sp = f.sp; retdst = f.retdst }, fs0, m0)) }) (Obj.magic (Errors.OK { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) })) (fun _ -> Obj.magic Errors.res_jmdiscr (Errors.OK { Types.fst = Events.e0; Types.snd = (State ({ func = f.func; locals = loc; next = f.next; sp = f.sp; retdst = f.retdst }, fs0, m0)) }) (Errors.OK { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __ (fun _ -> Obj.magic Globalenvs.prod_jmdiscr { Types.fst = Events.e0; Types.snd = (State ({ func = f.func; locals = loc; next = f.next; sp = f.sp; retdst = f.retdst }, fs0, m0)) } { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) } __ (fun _ -> Logic.eq_rect_Type0 List.Nil (fun _ _ _ -> Obj.magic state_jmdiscr (State ({ func = f.func; locals = loc; next = f.next; sp = f.sp; retdst = f.retdst }, fs0, m0)) (Callstate (vf', fd', args', dst', fs', m')) __) tr __ __)))))) x | Finalstate r -> (fun tr vf' fd' args' dst' fs' m' _ -> Obj.magic IOMonad.iO_discr (IOMonad.Wrong (List.Cons ((Errors.MSG ErrorMessages.FinalState), List.Nil))) (IOMonad.Value { Types.fst = tr; Types.snd = (Callstate (vf', fd', args', dst', fs', m')) }) __)) t fid fd args dst fs m __