source: driver/extracted/rTLabs_semantics.ml @ 3106

Last change on this file since 3106 was 3059, checked in by sacerdot, 7 years ago

New extraction

File size: 85.0 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21open ErrorMessages
22
23open Option
24
25open Setoids
26
27open Monad
28
29open Jmeq
30
31open Russell
32
33open Positive
34
35open PreIdentifiers
36
37open Errors
38
39open Extra_bool
40
41open Coqlib
42
43open Values
44
45open FrontEndVal
46
47open Hide
48
49open ByteValues
50
51open Division
52
53open Z
54
55open BitVectorZ
56
57open Pointers
58
59open GenMem
60
61open FrontEndMem
62
63open Proper
64
65open PositiveMap
66
67open Deqsets
68
69open Extralib
70
71open Lists
72
73open Identifiers
74
75open Exp
76
77open Arithmetic
78
79open Vector
80
81open Div_and_mod
82
83open Util
84
85open FoldStuff
86
87open BitVector
88
89open Extranat
90
91open Integers
92
93open AST
94
95open Globalenvs
96
97open CostLabel
98
99open Events
100
101open IOMonad
102
103open IO
104
105open SmallstepExec
106
107open BitVectorTrie
108
109open Graphs
110
111open Order
112
113open Registers
114
115open FrontEndOps
116
117open RTLabs_syntax
118
119type genv = RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t
120
121type 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 **)
130let 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 **)
140let 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 **)
150let 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 **)
160let 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 **)
170let 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 **)
180let 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 **)
187let rec func xxx =
188  xxx.func
189
190(** val locals : frame -> Values.val0 Registers.register_env **)
191let rec locals xxx =
192  xxx.locals
193
194(** val next : frame -> Graphs.label **)
195let rec next xxx =
196  xxx.next
197
198(** val sp : frame -> Pointers.block **)
199let rec sp xxx =
200  xxx.sp
201
202(** val retdst : frame -> Registers.register Types.option **)
203let 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 **)
210let 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 **)
217let 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 **)
224let 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 **)
231let 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 **)
238let frame_inv_rect_Type0 hterm h1 =
239  let hcut = frame_rect_Type0 h1 hterm in hcut __
240
241(** val frame_jmdiscr : frame -> frame -> __ **)
242let 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 **)
248let adv l f =
249  { func = f.func; locals = f.locals; next = l; sp = f.sp; retdst =
250    f.retdst }
251
252type 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 **)
267let 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 **)
279let 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 **)
291let 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 **)
303let 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 **)
315let 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 **)
327let 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 **)
340let 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 **)
350let 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 **)
360let 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 **)
370let 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 **)
380let 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 -> __ **)
384let 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 **)
395let build_state f fs m n =
396  State ((adv n f), fs, m)
397
398(** val next_instruction : frame -> RTLabs_syntax.statement **)
399let 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 **)
406let 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 **)
416let 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 **)
423let 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 **)
443let 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 **)
451let 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 **)
713let 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 **)
720let 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 **)
725let make_global p =
726  Globalenvs.globalenv (fun x -> x) p
727
728(** val make_initial_state :
729    RTLabs_syntax.rTLabs_program -> state Errors.res **)
730let 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 **)
752let 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 **)
760let 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 **)
769let 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 **)
777let 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
Note: See TracBrowser for help on using the repository browser.