source: extracted/rTLabs_semantics.ml @ 2636

Last change on this file since 2636 was 2636, checked in by campbell, 7 years ago

Extracted front-end.

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