source: extracted/rTLabs_semantics.ml @ 2729

Last change on this file since 2729 was 2649, checked in by sacerdot, 7 years ago

...

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