71 open Hints_declaration
111 type env = Values.val0 Identifiers.identifier_map
113 type genv = Cminor_syntax.internal_function AST.fundef Globalenvs.genv_t
117 | Kseq of Cminor_syntax.stmt * cont
120 (** val cont_rect_Type4 :
121 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
123 let rec cont_rect_Type4 h_Kend h_Kseq h_Kblock = function
125 | Kseq (x_23729, x_23728) ->
126 h_Kseq x_23729 x_23728 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_23728)
128 h_Kblock x_23730 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_23730)
130 (** val cont_rect_Type3 :
131 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
133 let rec cont_rect_Type3 h_Kend h_Kseq h_Kblock = function
135 | Kseq (x_23743, x_23742) ->
136 h_Kseq x_23743 x_23742 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_23742)
138 h_Kblock x_23744 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_23744)
140 (** val cont_rect_Type2 :
141 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
143 let rec cont_rect_Type2 h_Kend h_Kseq h_Kblock = function
145 | Kseq (x_23750, x_23749) ->
146 h_Kseq x_23750 x_23749 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_23749)
148 h_Kblock x_23751 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_23751)
150 (** val cont_rect_Type1 :
151 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
153 let rec cont_rect_Type1 h_Kend h_Kseq h_Kblock = function
155 | Kseq (x_23757, x_23756) ->
156 h_Kseq x_23757 x_23756 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_23756)
158 h_Kblock x_23758 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_23758)
160 (** val cont_rect_Type0 :
161 'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
163 let rec cont_rect_Type0 h_Kend h_Kseq h_Kblock = function
165 | Kseq (x_23764, x_23763) ->
166 h_Kseq x_23764 x_23763 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_23763)
168 h_Kblock x_23765 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_23765)
170 (** val cont_inv_rect_Type4 :
171 cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
172 -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
173 let cont_inv_rect_Type4 hterm h1 h2 h3 =
174 let hcut = cont_rect_Type4 h1 h2 h3 hterm in hcut __
176 (** val cont_inv_rect_Type3 :
177 cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
178 -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
179 let cont_inv_rect_Type3 hterm h1 h2 h3 =
180 let hcut = cont_rect_Type3 h1 h2 h3 hterm in hcut __
182 (** val cont_inv_rect_Type2 :
183 cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
184 -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
185 let cont_inv_rect_Type2 hterm h1 h2 h3 =
186 let hcut = cont_rect_Type2 h1 h2 h3 hterm in hcut __
188 (** val cont_inv_rect_Type1 :
189 cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
190 -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
191 let cont_inv_rect_Type1 hterm h1 h2 h3 =
192 let hcut = cont_rect_Type1 h1 h2 h3 hterm in hcut __
194 (** val cont_inv_rect_Type0 :
195 cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
196 -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
197 let cont_inv_rect_Type0 hterm h1 h2 h3 =
198 let hcut = cont_rect_Type0 h1 h2 h3 hterm in hcut __
200 (** val cont_discr : cont -> cont -> __ **)
202 Logic.eq_rect_Type2 x
204 | Kend -> Obj.magic (fun _ dH -> dH)
205 | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
206 | Kblock a0 -> Obj.magic (fun _ dH -> dH __)) y
208 (** val cont_jmdiscr : cont -> cont -> __ **)
209 let cont_jmdiscr x y =
210 Logic.eq_rect_Type2 x
212 | Kend -> Obj.magic (fun _ dH -> dH)
213 | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
214 | Kblock a0 -> Obj.magic (fun _ dH -> dH __)) y
218 | Scall of (AST.ident, AST.typ) Types.prod Types.option
219 * Cminor_syntax.internal_function * Pointers.block * env * cont *
222 (** val stack_rect_Type4 :
223 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
224 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
225 cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
226 let rec stack_rect_Type4 h_SStop h_Scall = function
228 | Scall (dest, f, x_23824, en, k, x_23820) ->
229 h_Scall dest f x_23824 en __ __ k __ x_23820
230 (stack_rect_Type4 h_SStop h_Scall x_23820)
232 (** val stack_rect_Type3 :
233 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
234 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
235 cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
236 let rec stack_rect_Type3 h_SStop h_Scall = function
238 | Scall (dest, f, x_23840, en, k, x_23836) ->
239 h_Scall dest f x_23840 en __ __ k __ x_23836
240 (stack_rect_Type3 h_SStop h_Scall x_23836)
242 (** val stack_rect_Type2 :
243 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
244 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
245 cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
246 let rec stack_rect_Type2 h_SStop h_Scall = function
248 | Scall (dest, f, x_23848, en, k, x_23844) ->
249 h_Scall dest f x_23848 en __ __ k __ x_23844
250 (stack_rect_Type2 h_SStop h_Scall x_23844)
252 (** val stack_rect_Type1 :
253 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
254 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
255 cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
256 let rec stack_rect_Type1 h_SStop h_Scall = function
258 | Scall (dest, f, x_23856, en, k, x_23852) ->
259 h_Scall dest f x_23856 en __ __ k __ x_23852
260 (stack_rect_Type1 h_SStop h_Scall x_23852)
262 (** val stack_rect_Type0 :
263 'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
264 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
265 cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
266 let rec stack_rect_Type0 h_SStop h_Scall = function
268 | Scall (dest, f, x_23864, en, k, x_23860) ->
269 h_Scall dest f x_23864 en __ __ k __ x_23860
270 (stack_rect_Type0 h_SStop h_Scall x_23860)
272 (** val stack_inv_rect_Type4 :
273 stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
274 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
275 cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
276 let stack_inv_rect_Type4 hterm h1 h2 =
277 let hcut = stack_rect_Type4 h1 h2 hterm in hcut __
279 (** val stack_inv_rect_Type3 :
280 stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
281 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
282 cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
283 let stack_inv_rect_Type3 hterm h1 h2 =
284 let hcut = stack_rect_Type3 h1 h2 hterm in hcut __
286 (** val stack_inv_rect_Type2 :
287 stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
288 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
289 cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
290 let stack_inv_rect_Type2 hterm h1 h2 =
291 let hcut = stack_rect_Type2 h1 h2 hterm in hcut __
293 (** val stack_inv_rect_Type1 :
294 stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
295 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
296 cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
297 let stack_inv_rect_Type1 hterm h1 h2 =
298 let hcut = stack_rect_Type1 h1 h2 hterm in hcut __
300 (** val stack_inv_rect_Type0 :
301 stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
302 Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
303 cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
304 let stack_inv_rect_Type0 hterm h1 h2 =
305 let hcut = stack_rect_Type0 h1 h2 hterm in hcut __
307 (** val stack_jmdiscr : stack -> stack -> __ **)
308 let stack_jmdiscr x y =
309 Logic.eq_rect_Type2 x
311 | SStop -> Obj.magic (fun _ dH -> dH)
312 | Scall (a0, a1, a2, a3, a6, a8) ->
313 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __)) y
316 | State of Cminor_syntax.internal_function * Cminor_syntax.stmt * env
317 * GenMem.mem * Pointers.block * cont * stack
318 | Callstate of AST.ident * Cminor_syntax.internal_function AST.fundef
319 * Values.val0 List.list * GenMem.mem * stack
320 | Returnstate of Values.val0 Types.option * GenMem.mem * stack
321 | Finalstate of Integers.int
323 (** val state_rect_Type4 :
324 (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
325 -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
326 (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
327 List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
328 GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
329 let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
330 | State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
331 | Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
332 | Returnstate (v, m, st) -> h_Returnstate v m st
333 | Finalstate r -> h_Finalstate r
335 (** val state_rect_Type5 :
336 (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
337 -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
338 (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
339 List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
340 GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
341 let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
342 | State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
343 | Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
344 | Returnstate (v, m, st) -> h_Returnstate v m st
345 | Finalstate r -> h_Finalstate r
347 (** val state_rect_Type3 :
348 (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
349 -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
350 (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
351 List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
352 GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
353 let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
354 | State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
355 | Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
356 | Returnstate (v, m, st) -> h_Returnstate v m st
357 | Finalstate r -> h_Finalstate r
359 (** val state_rect_Type2 :
360 (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
361 -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
362 (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
363 List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
364 GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
365 let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
366 | State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
367 | Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
368 | Returnstate (v, m, st) -> h_Returnstate v m st
369 | Finalstate r -> h_Finalstate r
371 (** val state_rect_Type1 :
372 (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
373 -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
374 (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
375 List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
376 GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
377 let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
378 | State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
379 | Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
380 | Returnstate (v, m, st) -> h_Returnstate v m st
381 | Finalstate r -> h_Finalstate r
383 (** val state_rect_Type0 :
384 (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
385 -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
386 (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
387 List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
388 GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
389 let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
390 | State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
391 | Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
392 | Returnstate (v, m, st) -> h_Returnstate v m st
393 | Finalstate r -> h_Finalstate r
395 (** val state_inv_rect_Type4 :
396 state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
397 __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
398 'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
399 Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
400 (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
401 (Integers.int -> __ -> 'a1) -> 'a1 **)
402 let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
403 let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __
405 (** val state_inv_rect_Type3 :
406 state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
407 __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
408 'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
409 Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
410 (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
411 (Integers.int -> __ -> 'a1) -> 'a1 **)
412 let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
413 let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __
415 (** val state_inv_rect_Type2 :
416 state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
417 __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
418 'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
419 Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
420 (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
421 (Integers.int -> __ -> 'a1) -> 'a1 **)
422 let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
423 let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __
425 (** val state_inv_rect_Type1 :
426 state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
427 __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
428 'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
429 Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
430 (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
431 (Integers.int -> __ -> 'a1) -> 'a1 **)
432 let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
433 let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __
435 (** val state_inv_rect_Type0 :
436 state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
437 __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
438 'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
439 Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
440 (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
441 (Integers.int -> __ -> 'a1) -> 'a1 **)
442 let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
443 let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __
445 (** val state_jmdiscr : state -> state -> __ **)
446 let state_jmdiscr x y =
447 Logic.eq_rect_Type2 x
449 | State (a0, a1, a2, a5, a6, a7, a9) ->
450 Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)
451 | Callstate (a0, a1, a2, a3, a4) ->
452 Obj.magic (fun _ dH -> dH __ __ __ __ __)
453 | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
454 | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
457 genv -> AST.typ -> Cminor_syntax.expr -> env -> Pointers.block ->
458 GenMem.mem -> (Events.trace, Values.val0) Types.prod Errors.res **)
459 let rec eval_expr ge ty0 e en sp m =
461 | Cminor_syntax.Id (x, i) ->
463 let r = Identifiers.lookup_present PreIdentifiers.SymbolTag en i in
464 Errors.OK { Types.fst = Events.e0; Types.snd = r })
465 | Cminor_syntax.Cst (x, c) ->
468 (Monad.m_bind0 (Monad.max_def Errors.res0)
470 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedConstant)
471 (FrontEndOps.eval_constant x (Globalenvs.find_symbol ge) sp c)))
473 Obj.magic (Errors.OK { Types.fst = Events.e0; Types.snd = r }))))
474 | Cminor_syntax.Op1 (ty, ty', op, e') ->
477 (Monad.m_bind2 (Monad.max_def Errors.res0)
478 (Obj.magic (eval_expr ge ty e' en sp m)) (fun tr v ->
479 Monad.m_bind0 (Monad.max_def Errors.res0)
481 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
482 (FrontEndOps.eval_unop ty ty' op v))) (fun r ->
483 Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r })))))
484 | Cminor_syntax.Op2 (ty1, ty2, ty', op, e1, e2) ->
487 (Monad.m_bind2 (Monad.max_def Errors.res0)
488 (Obj.magic (eval_expr ge ty1 e1 en sp m)) (fun tr1 v1 ->
489 Monad.m_bind2 (Monad.max_def Errors.res0)
490 (Obj.magic (eval_expr ge ty2 e2 en sp m)) (fun tr2 v2 ->
491 Monad.m_bind0 (Monad.max_def Errors.res0)
493 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
494 (FrontEndOps.eval_binop m ty1 ty2 ty' op v1 v2)))
496 Obj.magic (Errors.OK { Types.fst = (Events.eapp tr1 tr2);
497 Types.snd = r }))))))
498 | Cminor_syntax.Mem (ty, e0) ->
501 (Monad.m_bind2 (Monad.max_def Errors.res0)
502 (Obj.magic (eval_expr ge AST.ASTptr e0 en sp m)) (fun tr v ->
503 Monad.m_bind0 (Monad.max_def Errors.res0)
505 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
506 (FrontEndMem.loadv ty m v))) (fun r ->
507 Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r })))))
508 | Cminor_syntax.Cond (sz, sg, ty, e', e1, e2) ->
511 (Monad.m_bind2 (Monad.max_def Errors.res0)
512 (Obj.magic (eval_expr ge (AST.ASTint (sz, sg)) e' en sp m))
514 Monad.m_bind0 (Monad.max_def Errors.res0)
515 (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
516 Monad.m_bind2 (Monad.max_def Errors.res0)
521 | Bool.False -> e2) en sp m)) (fun tr' r ->
522 Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr');
523 Types.snd = r }))))))
524 | Cminor_syntax.Ecost (ty, l, e') ->
527 (Monad.m_bind2 (Monad.max_def Errors.res0)
528 (Obj.magic (eval_expr ge ty e' en sp m)) (fun tr r ->
529 Obj.magic (Errors.OK { Types.fst =
530 (Events.eapp (Events.echarge l) tr); Types.snd = r }))))) __
533 Nat.nat -> cont -> Cminor_syntax.internal_function -> env -> cont
534 Types.sig0 Errors.res **)
535 let rec k_exit n k f en =
537 | Kend -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadState))
538 | Kseq (x, k') -> (fun _ -> k_exit n k' f en)
542 | Nat.O -> Errors.OK k'
543 | Nat.S m -> k_exit m k' f en)) __
546 AST.intsize -> AST.bvint -> (AST.bvint, 'a1) Types.prod List.list -> 'a1
548 let rec find_case sz i cs default =
550 | List.Nil -> default
551 | List.Cons (h, t) ->
552 let { Types.fst = hi; Types.snd = a } = h in
553 (match BitVector.eq_bv (AST.bitsize_of_intsize sz) i hi with
555 | Bool.False -> find_case sz i t default)
558 PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
559 Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
560 Types.prod Types.sig0 Types.option **)
561 let rec find_label l s k f en =
563 | Cminor_syntax.St_skip -> (fun _ -> Types.None)
564 | Cminor_syntax.St_assign (x, x0, x1) -> (fun _ -> Types.None)
565 | Cminor_syntax.St_store (x, x0, x1) -> (fun _ -> Types.None)
566 | Cminor_syntax.St_call (x, x0, x1) -> (fun _ -> Types.None)
567 | Cminor_syntax.St_seq (s1, s2) ->
569 match find_label l s1 (Kseq (s2, k)) f en with
570 | Types.None -> find_label l s2 k f en
571 | Types.Some sk -> Types.Some sk)
572 | Cminor_syntax.St_ifthenelse (x, x0, x1, s1, s2) ->
574 match find_label l s1 k f en with
575 | Types.None -> find_label l s2 k f en
576 | Types.Some sk -> Types.Some sk)
577 | Cminor_syntax.St_return x -> (fun _ -> Types.None)
578 | Cminor_syntax.St_label (l', s') ->
580 match Identifiers.identifier_eq PreIdentifiers.Label l l' with
581 | Types.Inl _ -> Types.Some { Types.fst = s'; Types.snd = k }
582 | Types.Inr _ -> find_label l s' k f en)
583 | Cminor_syntax.St_goto x -> (fun _ -> Types.None)
584 | Cminor_syntax.St_cost (x, s') -> (fun _ -> find_label l s' k f en)) __
586 (** val find_label_always :
587 PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
588 Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
589 Types.prod Types.sig0 **)
590 let find_label_always l s k f en =
591 (match find_label l s k f en with
592 | Types.None -> (fun _ -> assert false (* absurd case *))
593 | Types.Some sk -> (fun _ -> sk)) __
595 (** val bind_params :
596 Values.val0 List.list -> (AST.ident, AST.typ) Types.prod List.list -> env
597 Types.sig0 Errors.res **)
598 let rec bind_params vs ids =
602 | List.Nil -> Errors.OK (Identifiers.empty_map PreIdentifiers.SymbolTag)
603 | List.Cons (x, x0) ->
604 Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters))
605 | List.Cons (v, vt) ->
608 Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)
609 | List.Cons (idh, idt) ->
610 let { Types.fst = id; Types.snd = ty } = idh in
612 (Monad.m_bind0 (Monad.max_def Errors.res0)
613 (Obj.magic (bind_params vt idt)) (fun en ->
615 (Identifiers.add PreIdentifiers.SymbolTag (Types.pi1 en)
618 (** val init_locals :
619 env -> (AST.ident, AST.typ) Types.prod List.list -> env **)
621 List.foldr (fun idty en ->
622 Identifiers.add PreIdentifiers.SymbolTag en idty.Types.fst Values.Vundef)
624 (** val trace_map_inv :
625 ('a1 -> __ -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list
626 -> (Events.trace, 'a2 List.list) Types.prod Errors.res **)
627 let rec trace_map_inv f l =
630 (fun _ -> Errors.OK { Types.fst = Events.e0; Types.snd = List.Nil })
631 | List.Cons (h, t) ->
634 (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic f h __)
636 Monad.m_bind2 (Monad.max_def Errors.res0)
637 (Obj.magic (trace_map_inv f t)) (fun tr' t' ->
638 Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr');
639 Types.snd = (List.Cons (h', t')) })))))) __
642 genv -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod)
644 let eval_step ge = function
645 | State (f, s, en, m, sp, k, st0) ->
648 | Cminor_syntax.St_skip ->
654 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
655 Events.e0; Types.snd = (Returnstate (Types.None,
656 (GenMem.free m sp), st0)) }))
660 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
661 Events.e0; Types.snd = (State (f, s', en, m, sp, k',
666 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
667 Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip,
668 en, m, sp, k', st0)) }))) __)
669 | Cminor_syntax.St_assign (x, id, e) ->
672 (Monad.m_bind2 (Monad.max_def Errors.res0)
673 (Obj.magic (eval_expr ge x e en sp m)) (fun tr v ->
675 Identifiers.update_present PreIdentifiers.SymbolTag en id v
677 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
678 Types.snd = (State (f, Cminor_syntax.St_skip, en', m, sp, k,
680 | Cminor_syntax.St_store (ty, edst, e) ->
683 (Monad.m_bind2 (Monad.max_def Errors.res0)
684 (Obj.magic (eval_expr ge AST.ASTptr edst en sp m))
686 Monad.m_bind2 (Monad.max_def Errors.res0)
687 (Obj.magic (eval_expr ge ty e en sp m)) (fun tr' v ->
688 Monad.m_bind0 (Monad.max_def Errors.res0)
690 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
691 (FrontEndMem.storev ty m vdst v))) (fun m' ->
692 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
693 (Events.eapp tr tr'); Types.snd = (State (f,
694 Cminor_syntax.St_skip, en, m', sp, k, st0)) })))))
695 | Cminor_syntax.St_call (dst, ef, args) ->
698 (Monad.m_bind2 (Monad.max_def Errors.res0)
699 (Obj.magic (eval_expr ge AST.ASTptr ef en sp m)) (fun tr vf ->
700 Monad.m_bind2 (Monad.max_def Errors.res0)
703 (Errors.msg ErrorMessages.BadFunctionValue)
704 (Globalenvs.find_funct_id ge vf))) (fun fd id ->
705 Monad.m_bind2 (Monad.max_def Errors.res0)
707 (trace_map_inv (fun e ->
708 let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
709 (fun _ -> eval_expr ge ty e0 en sp m)) args))
711 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
712 (Events.eapp tr tr'); Types.snd = (Callstate (id, fd,
713 vargs, m, (Scall (dst, f, sp, en, k, st0)))) })))))
714 | Cminor_syntax.St_seq (s1, s2) ->
717 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
718 Events.e0; Types.snd = (State (f, s1, en, m, sp, (Kseq (s2,
720 | Cminor_syntax.St_ifthenelse (x, x0, e, strue, sfalse) ->
723 (Monad.m_bind2 (Monad.max_def Errors.res0)
724 (Obj.magic (eval_expr ge (AST.ASTint (x, x0)) e en sp m))
726 Monad.m_bind0 (Monad.max_def Errors.res0)
727 (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
728 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
729 Types.snd = (State (f,
732 | Bool.False -> sfalse), en, m, sp, k, st0)) }))))
733 | Cminor_syntax.St_return eo ->
738 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
739 Events.e0; Types.snd = (Returnstate (Types.None,
740 (GenMem.free m sp), st0)) }))
742 let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
745 (Monad.m_bind2 (Monad.max_def Errors.res0)
746 (Obj.magic (eval_expr ge ty e0 en sp m)) (fun tr v ->
747 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
748 Types.snd = (Returnstate ((Types.Some v),
749 (GenMem.free m sp), st0)) }))))
750 | Cminor_syntax.St_label (l, s') ->
753 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
754 Events.e0; Types.snd = (State (f, s', en, m, sp, k, st0)) }))
755 | Cminor_syntax.St_goto l ->
757 let sk = find_label_always l f.Cminor_syntax.f_body Kend f en in
759 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
760 Events.e0; Types.snd = (State (f, sk.Types.fst, en, m, sp,
761 sk.Types.snd, st0)) }))
762 | Cminor_syntax.St_cost (l, s') ->
765 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
766 (Events.echarge l); Types.snd = (State (f, s', en, m, sp, k,
768 | Callstate (x, fd, args, m, st0) ->
772 (let { Types.fst = m'; Types.snd = sp } =
773 GenMem.alloc m (Z.z_of_nat Nat.O)
774 (Z.z_of_nat f.Cminor_syntax.f_stacksize)
777 (Monad.m_bind0 (Monad.max_def Errors.res0)
778 (Obj.magic (bind_params args f.Cminor_syntax.f_params)) (fun en ->
779 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
780 Events.e0; Types.snd = (State (f, f.Cminor_syntax.f_body,
781 (init_locals (Types.pi1 en) f.Cminor_syntax.f_vars), m', sp,
785 (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
788 (IO.check_eventval_list args fn.AST.ef_sig.AST.sig_args)))
790 Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
792 (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
795 match fn.AST.ef_sig.AST.sig_res with
796 | Types.None -> Types.None
798 Types.Some (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)
800 Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
801 (Events.eextcall fn.AST.ef_id evargs
802 (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
803 Types.snd = (Returnstate (res, m, st0)) }))))
804 | Returnstate (result, m, st0) ->
810 Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
814 Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
815 | Values.Vint (sz, r) ->
818 (fun x -> Errors.Error
819 (Errors.msg ErrorMessages.ReturnMismatch))
821 (fun x -> Errors.Error
822 (Errors.msg ErrorMessages.ReturnMismatch))
826 (Monad.m_return0 (Monad.max_def Errors.res0)
827 { Types.fst = Events.e0; Types.snd = (Finalstate r0) })))
830 Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
832 Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)))
833 | Scall (dst, f, sp, en, k, st') ->
839 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
840 Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip, en,
843 Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
847 (fun _ -> Errors.Error
848 (Errors.msg ErrorMessages.ReturnMismatch))
852 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
853 Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip,
854 (Identifiers.update_present PreIdentifiers.SymbolTag en
855 idty.Types.fst v), m, sp, k, st')) }))) __))
857 IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.BadState))
859 (** val is_final : state -> Integers.int Types.option **)
860 let is_final = function
861 | State (x, x0, x1, x4, x5, x6, x8) -> Types.None
862 | Callstate (x, x0, x1, x2, x3) -> Types.None
863 | Returnstate (x, x0, x1) -> Types.None
864 | Finalstate r -> Types.Some r
866 (** val cminor_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
868 { SmallstepExec.is_final = (fun x -> Obj.magic is_final);
869 SmallstepExec.step = (Obj.magic eval_step) }
871 (** val make_global : Cminor_syntax.cminor_program -> genv **)
873 Globalenvs.globalenv (fun x -> x) p
875 (** val make_initial_state :
876 Cminor_syntax.cminor_program -> state Errors.res **)
877 let make_initial_state p =
878 let ge = make_global p in
880 (Monad.m_bind0 (Monad.max_def Errors.res0)
881 (Obj.magic (Globalenvs.init_mem (fun x -> x) p)) (fun m ->
882 Monad.m_bind0 (Monad.max_def Errors.res0)
884 (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
885 (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
886 Monad.m_bind0 (Monad.max_def Errors.res0)
888 (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
889 (Globalenvs.find_funct_ptr ge b))) (fun f ->
890 Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m,
893 (** val cminor_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
894 let cminor_fullexec =
895 { SmallstepExec.es1 = cminor_exec; SmallstepExec.make_global =
896 (Obj.magic make_global); SmallstepExec.make_initial_state =
897 (Obj.magic make_initial_state) }
899 (** val make_noinit_global : Cminor_syntax.cminor_noinit_program -> genv **)
900 let make_noinit_global p =
901 Globalenvs.globalenv (fun x -> List.Cons ((AST.Init_space x), List.Nil)) p
903 (** val make_initial_noinit_state :
904 Cminor_syntax.cminor_noinit_program -> state Errors.res **)
905 let make_initial_noinit_state p =
906 let ge = make_noinit_global p in
908 (Monad.m_bind0 (Monad.max_def Errors.res0)
910 (Globalenvs.init_mem (fun x -> List.Cons ((AST.Init_space x),
911 List.Nil)) p)) (fun m ->
912 Monad.m_bind0 (Monad.max_def Errors.res0)
914 (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
915 (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
916 Monad.m_bind0 (Monad.max_def Errors.res0)
918 (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
919 (Globalenvs.find_funct_ptr ge b))) (fun f ->
920 Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m,
923 (** val cminor_noinit_fullexec :
924 (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
925 let cminor_noinit_fullexec =
926 { SmallstepExec.es1 = cminor_exec; SmallstepExec.make_global =
927 (Obj.magic make_noinit_global); SmallstepExec.make_initial_state =
928 (Obj.magic make_initial_noinit_state) }