133 open Hints_declaration
153 type reg_sp = { reg_sp_env : ByteValues.beval Identifiers.identifier_map;
154 stackp : ByteValues.xpointer }
156 (** val reg_sp_rect_Type4 :
157 (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
158 'a1) -> reg_sp -> 'a1 **)
159 let rec reg_sp_rect_Type4 h_mk_reg_sp x_25168 =
160 let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25168 in
161 h_mk_reg_sp reg_sp_env0 stackp0
163 (** val reg_sp_rect_Type5 :
164 (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
165 'a1) -> reg_sp -> 'a1 **)
166 let rec reg_sp_rect_Type5 h_mk_reg_sp x_25170 =
167 let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25170 in
168 h_mk_reg_sp reg_sp_env0 stackp0
170 (** val reg_sp_rect_Type3 :
171 (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
172 'a1) -> reg_sp -> 'a1 **)
173 let rec reg_sp_rect_Type3 h_mk_reg_sp x_25172 =
174 let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25172 in
175 h_mk_reg_sp reg_sp_env0 stackp0
177 (** val reg_sp_rect_Type2 :
178 (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
179 'a1) -> reg_sp -> 'a1 **)
180 let rec reg_sp_rect_Type2 h_mk_reg_sp x_25174 =
181 let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25174 in
182 h_mk_reg_sp reg_sp_env0 stackp0
184 (** val reg_sp_rect_Type1 :
185 (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
186 'a1) -> reg_sp -> 'a1 **)
187 let rec reg_sp_rect_Type1 h_mk_reg_sp x_25176 =
188 let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25176 in
189 h_mk_reg_sp reg_sp_env0 stackp0
191 (** val reg_sp_rect_Type0 :
192 (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
193 'a1) -> reg_sp -> 'a1 **)
194 let rec reg_sp_rect_Type0 h_mk_reg_sp x_25178 =
195 let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25178 in
196 h_mk_reg_sp reg_sp_env0 stackp0
199 reg_sp -> ByteValues.beval Identifiers.identifier_map **)
200 let rec reg_sp_env xxx =
203 (** val stackp : reg_sp -> ByteValues.xpointer **)
207 (** val reg_sp_inv_rect_Type4 :
208 reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
209 ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
210 let reg_sp_inv_rect_Type4 hterm h1 =
211 let hcut = reg_sp_rect_Type4 h1 hterm in hcut __
213 (** val reg_sp_inv_rect_Type3 :
214 reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
215 ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
216 let reg_sp_inv_rect_Type3 hterm h1 =
217 let hcut = reg_sp_rect_Type3 h1 hterm in hcut __
219 (** val reg_sp_inv_rect_Type2 :
220 reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
221 ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
222 let reg_sp_inv_rect_Type2 hterm h1 =
223 let hcut = reg_sp_rect_Type2 h1 hterm in hcut __
225 (** val reg_sp_inv_rect_Type1 :
226 reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
227 ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
228 let reg_sp_inv_rect_Type1 hterm h1 =
229 let hcut = reg_sp_rect_Type1 h1 hterm in hcut __
231 (** val reg_sp_inv_rect_Type0 :
232 reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
233 ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
234 let reg_sp_inv_rect_Type0 hterm h1 =
235 let hcut = reg_sp_rect_Type0 h1 hterm in hcut __
237 (** val reg_sp_discr : reg_sp -> reg_sp -> __ **)
238 let reg_sp_discr x y =
239 Logic.eq_rect_Type2 x
240 (let { reg_sp_env = a0; stackp = a1 } = x in
241 Obj.magic (fun _ dH -> dH __ __)) y
243 (** val reg_sp_jmdiscr : reg_sp -> reg_sp -> __ **)
244 let reg_sp_jmdiscr x y =
245 Logic.eq_rect_Type2 x
246 (let { reg_sp_env = a0; stackp = a1 } = x in
247 Obj.magic (fun _ dH -> dH __ __)) y
249 (** val dpi1__o__reg_sp_env__o__inject :
250 (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
252 let dpi1__o__reg_sp_env__o__inject x2 =
253 x2.Types.dpi1.reg_sp_env
255 (** val eject__o__reg_sp_env__o__inject :
256 reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map
258 let eject__o__reg_sp_env__o__inject x2 =
259 (Types.pi1 x2).reg_sp_env
261 (** val reg_sp_env__o__inject :
262 reg_sp -> ByteValues.beval Identifiers.identifier_map Types.sig0 **)
263 let reg_sp_env__o__inject x1 =
266 (** val dpi1__o__reg_sp_env :
267 (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map **)
268 let dpi1__o__reg_sp_env x1 =
269 x1.Types.dpi1.reg_sp_env
271 (** val eject__o__reg_sp_env :
272 reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map **)
273 let eject__o__reg_sp_env x1 =
274 (Types.pi1 x1).reg_sp_env
276 (** val reg_sp_store :
277 PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp **)
278 let reg_sp_store reg v locals =
279 let locals' = SemanticsUtils.reg_store reg v locals.reg_sp_env in
280 { reg_sp_env = locals'; stackp = locals.stackp }
282 (** val reg_sp_retrieve :
283 reg_sp -> Registers.register -> ByteValues.beval Errors.res **)
284 let reg_sp_retrieve locals =
285 SemanticsUtils.reg_retrieve locals.reg_sp_env
287 (** val reg_sp_empty : ByteValues.xpointer -> reg_sp **)
289 { reg_sp_env = (Identifiers.empty_map PreIdentifiers.RegisterTag); stackp =
292 type frame = { fr_ret_regs : Registers.register List.list;
293 fr_pc : ByteValues.program_counter;
294 fr_carry : ByteValues.bebit; fr_regs : reg_sp }
296 (** val frame_rect_Type4 :
297 (Registers.register List.list -> ByteValues.program_counter ->
298 ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
299 let rec frame_rect_Type4 h_mk_frame x_25194 =
300 let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
301 fr_regs = fr_regs0 } = x_25194
303 h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
305 (** val frame_rect_Type5 :
306 (Registers.register List.list -> ByteValues.program_counter ->
307 ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
308 let rec frame_rect_Type5 h_mk_frame x_25196 =
309 let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
310 fr_regs = fr_regs0 } = x_25196
312 h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
314 (** val frame_rect_Type3 :
315 (Registers.register List.list -> ByteValues.program_counter ->
316 ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
317 let rec frame_rect_Type3 h_mk_frame x_25198 =
318 let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
319 fr_regs = fr_regs0 } = x_25198
321 h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
323 (** val frame_rect_Type2 :
324 (Registers.register List.list -> ByteValues.program_counter ->
325 ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
326 let rec frame_rect_Type2 h_mk_frame x_25200 =
327 let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
328 fr_regs = fr_regs0 } = x_25200
330 h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
332 (** val frame_rect_Type1 :
333 (Registers.register List.list -> ByteValues.program_counter ->
334 ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
335 let rec frame_rect_Type1 h_mk_frame x_25202 =
336 let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
337 fr_regs = fr_regs0 } = x_25202
339 h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
341 (** val frame_rect_Type0 :
342 (Registers.register List.list -> ByteValues.program_counter ->
343 ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
344 let rec frame_rect_Type0 h_mk_frame x_25204 =
345 let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
346 fr_regs = fr_regs0 } = x_25204
348 h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0
350 (** val fr_ret_regs : frame -> Registers.register List.list **)
351 let rec fr_ret_regs xxx =
354 (** val fr_pc : frame -> ByteValues.program_counter **)
358 (** val fr_carry : frame -> ByteValues.bebit **)
359 let rec fr_carry xxx =
362 (** val fr_regs : frame -> reg_sp **)
363 let rec fr_regs xxx =
366 (** val frame_inv_rect_Type4 :
367 frame -> (Registers.register List.list -> ByteValues.program_counter ->
368 ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
369 let frame_inv_rect_Type4 hterm h1 =
370 let hcut = frame_rect_Type4 h1 hterm in hcut __
372 (** val frame_inv_rect_Type3 :
373 frame -> (Registers.register List.list -> ByteValues.program_counter ->
374 ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
375 let frame_inv_rect_Type3 hterm h1 =
376 let hcut = frame_rect_Type3 h1 hterm in hcut __
378 (** val frame_inv_rect_Type2 :
379 frame -> (Registers.register List.list -> ByteValues.program_counter ->
380 ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
381 let frame_inv_rect_Type2 hterm h1 =
382 let hcut = frame_rect_Type2 h1 hterm in hcut __
384 (** val frame_inv_rect_Type1 :
385 frame -> (Registers.register List.list -> ByteValues.program_counter ->
386 ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
387 let frame_inv_rect_Type1 hterm h1 =
388 let hcut = frame_rect_Type1 h1 hterm in hcut __
390 (** val frame_inv_rect_Type0 :
391 frame -> (Registers.register List.list -> ByteValues.program_counter ->
392 ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
393 let frame_inv_rect_Type0 hterm h1 =
394 let hcut = frame_rect_Type0 h1 hterm in hcut __
396 (** val frame_discr : frame -> frame -> __ **)
397 let frame_discr x y =
398 Logic.eq_rect_Type2 x
399 (let { fr_ret_regs = a0; fr_pc = a1; fr_carry = a2; fr_regs = a3 } = x in
400 Obj.magic (fun _ dH -> dH __ __ __ __)) y
402 (** val frame_jmdiscr : frame -> frame -> __ **)
403 let frame_jmdiscr x y =
404 Logic.eq_rect_Type2 x
405 (let { fr_ret_regs = a0; fr_pc = a1; fr_carry = a2; fr_regs = a3 } = x in
406 Obj.magic (fun _ dH -> dH __ __ __ __)) y
408 (** val rTL_state_params : Joint_semantics.sem_state_params **)
409 let rTL_state_params =
410 { Joint_semantics.empty_framesT = (Obj.magic List.Nil);
411 Joint_semantics.empty_regsT = (Obj.magic reg_sp_empty);
412 Joint_semantics.load_sp = (fun env -> Errors.OK (Obj.magic env).stackp);
413 Joint_semantics.save_sp = (fun env ->
414 Obj.magic (fun x -> { reg_sp_env = (Obj.magic env).reg_sp_env; stackp =
417 type rTL_state = Joint_semantics.state
419 (** val rtl_arg_retrieve :
420 reg_sp -> Joint.psd_argument -> ByteValues.beval Errors.res **)
421 let rtl_arg_retrieve env = function
422 | Joint.Reg r -> SemanticsUtils.reg_retrieve env.reg_sp_env r
423 | Joint.Imm b -> Errors.OK (ByteValues.BVByte b)
425 (** val rtl_fetch_ra :
426 rTL_state -> (rTL_state, ByteValues.program_counter) Types.prod
428 let rtl_fetch_ra st =
430 (Monad.m_bind0 (Monad.max_def Errors.res0)
432 (Errors.opt_to_res (List.Cons ((Errors.MSG
433 ErrorMessages.FrameErrorOnPop), List.Nil))
434 st.Joint_semantics.st_frms)) (fun frms ->
437 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
438 ErrorMessages.EmptyStack), List.Nil)))
439 | List.Cons (hd, tl) ->
440 Obj.magic (Errors.OK { Types.fst = st; Types.snd = hd.fr_pc })))
442 (** val rtl_init_local : Registers.register -> reg_sp -> reg_sp **)
443 let rtl_init_local local =
444 reg_sp_store local ByteValues.BVundef
446 (** val rtl_setup_call_separate :
447 Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
448 -> rTL_state -> rTL_state Errors.res **)
449 let rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st =
450 (let { Types.fst = mem; Types.snd = b } =
451 GenMem.alloc st.Joint_semantics.m (Z.z_of_nat Nat.O)
452 (Z.z_of_nat stacksize)
455 let sp = { Pointers.pblock = b; Pointers.poff =
456 (BitVector.zero Pointers.offset_size) }
459 (Monad.m_bind0 (Monad.max_def Errors.res0)
461 (Errors.mfold_left2 (fun lenv dest src ->
463 (Monad.m_bind0 (Monad.max_def Errors.res0)
465 (rtl_arg_retrieve (Obj.magic st.Joint_semantics.regs) src))
466 (fun v -> Obj.magic (Errors.OK (reg_sp_store dest v lenv)))))
467 (Errors.OK (reg_sp_empty sp)) formal_arg_regs actual_arg_regs))
470 (Joint_semantics.set_regs rTL_state_params new_regs
471 (Joint_semantics.set_m rTL_state_params mem st))))))) __
473 (** val rtl_setup_call_separate_overflow :
474 Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
475 -> rTL_state -> rTL_state Errors.res **)
476 let rtl_setup_call_separate_overflow stacksize formal_arg_regs actual_arg_regs st =
477 match Nat.leb (Nat.S (Nat.plus stacksize st.Joint_semantics.stack_usage))
478 (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
479 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
480 (Nat.S (Nat.S Nat.O))))))))))))))))) with
482 rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st
484 Errors.Error (List.Cons ((Errors.MSG ErrorMessages.StackOverflow),
487 (** val rtl_setup_call_unique :
488 Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
489 -> rTL_state -> rTL_state Errors.res **)
490 let rtl_setup_call_unique stacksize formal_arg_regs actual_arg_regs st =
492 (Monad.m_bind0 (Monad.max_def Errors.res0)
493 (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
495 Pointers.neg_shift_pointer (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
496 (Nat.S (Nat.S Nat.O)))))))) (Types.pi1 sp)
497 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
498 (Nat.S (Nat.S (Nat.S Nat.O)))))))) stacksize)
500 Monad.m_bind0 (Monad.max_def Errors.res0)
502 (Errors.mfold_left2 (fun lenv dest src ->
504 (Monad.m_bind0 (Monad.max_def Errors.res0)
506 (rtl_arg_retrieve (Obj.magic st.Joint_semantics.regs) src))
507 (fun v -> Obj.magic (Errors.OK (reg_sp_store dest v lenv)))))
508 (Errors.OK (reg_sp_empty newsp)) formal_arg_regs actual_arg_regs))
511 (Joint_semantics.set_regs rTL_state_params new_regs st)))))
513 type rTL_state_pc = Joint_semantics.state_pc
515 (** val rtl_save_frame :
516 Registers.register List.list -> rTL_state_pc -> __ **)
517 let rtl_save_frame retregs st =
518 Monad.m_bind0 (Monad.max_def Errors.res0)
520 (Errors.opt_to_res (List.Cons ((Errors.MSG
521 ErrorMessages.FrameErrorOnPush), List.Nil))
522 st.Joint_semantics.st_no_pc.Joint_semantics.st_frms)) (fun frms ->
523 let frame0 = List.Cons ({ fr_ret_regs = retregs; fr_pc =
524 st.Joint_semantics.pc; fr_carry =
525 st.Joint_semantics.st_no_pc.Joint_semantics.carry; fr_regs =
526 (Obj.magic st.Joint_semantics.st_no_pc.Joint_semantics.regs) }, frms)
529 (Joint_semantics.set_frms rTL_state_params (Obj.magic frame0)
530 st.Joint_semantics.st_no_pc)))
532 (** val rtl_fetch_external_args :
533 AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
534 Values.val0 List.list Errors.res **)
535 let rtl_fetch_external_args _ =
536 failwith "AXIOM TO BE REALIZED"
538 (** val rtl_set_result :
539 Values.val0 List.list -> Registers.register List.list -> rTL_state ->
540 rTL_state Errors.res **)
541 let rtl_set_result _ =
542 failwith "AXIOM TO BE REALIZED"
544 (** val rtl_reg_store :
545 PreIdentifiers.identifier -> ByteValues.beval -> Joint_semantics.state ->
546 Joint_semantics.state **)
547 let rtl_reg_store r v st =
548 let mem = reg_sp_store r v (Obj.magic st.Joint_semantics.regs) in
549 Joint_semantics.set_regs rTL_state_params (Obj.magic mem) st
551 (** val rtl_reg_retrieve :
552 Joint_semantics.state -> Registers.register -> ByteValues.beval
554 let rtl_reg_retrieve st l =
555 reg_sp_retrieve (Obj.magic st.Joint_semantics.regs) l
557 (** val rtl_read_result :
558 Registers.register List.list -> rTL_state -> ByteValues.beval List.list
560 let rtl_read_result rets st =
562 (Monad.m_list_map (Monad.max_def Errors.res0)
563 (Obj.magic (rtl_reg_retrieve st)) rets)
565 (** val rtl_pop_frame_separate :
566 Registers.register List.list -> rTL_state -> (rTL_state,
567 ByteValues.program_counter) Types.prod Errors.res **)
568 let rtl_pop_frame_separate ret st =
570 (Monad.m_bind0 (Monad.max_def Errors.res0)
572 (Errors.opt_to_res (List.Cons ((Errors.MSG
573 ErrorMessages.FrameErrorOnPop), List.Nil))
574 st.Joint_semantics.st_frms)) (fun frms ->
577 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
578 ErrorMessages.EmptyStack), List.Nil)))
579 | List.Cons (hd, tl) ->
580 Monad.m_bind0 (Monad.max_def Errors.res0)
581 (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
582 let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
583 Monad.m_bind0 (Monad.max_def Errors.res0)
584 (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
586 Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
587 (Joint_semantics.set_regs rTL_state_params
588 (Obj.magic hd.fr_regs)
589 (Joint_semantics.set_carry rTL_state_params hd.fr_carry
590 (Joint_semantics.set_m rTL_state_params
591 (GenMem.free st.Joint_semantics.m
592 (Types.pi1 sp).Pointers.pblock) st)))
596 Util.foldl (fun st1 reg_val ->
597 rtl_reg_store reg_val.Types.fst reg_val.Types.snd st1) st0
600 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
603 (** val rtl_pop_frame_unique :
604 Registers.register List.list -> rTL_state -> (rTL_state,
605 ByteValues.program_counter) Types.prod Errors.res **)
606 let rtl_pop_frame_unique ret st =
608 (Monad.m_bind0 (Monad.max_def Errors.res0)
610 (Errors.opt_to_res (List.Cons ((Errors.MSG
611 ErrorMessages.FrameErrorOnPop), List.Nil))
612 st.Joint_semantics.st_frms)) (fun frms ->
615 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
616 ErrorMessages.EmptyStack), List.Nil)))
617 | List.Cons (hd, tl) ->
618 Monad.m_bind0 (Monad.max_def Errors.res0)
619 (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
620 let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
621 Monad.m_bind0 (Monad.max_def Errors.res0)
622 (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
624 Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
625 (Joint_semantics.set_regs rTL_state_params
626 (Obj.magic hd.fr_regs)
627 (Joint_semantics.set_carry rTL_state_params hd.fr_carry st))
631 Util.foldl (fun st1 reg_val ->
632 rtl_reg_store reg_val.Types.fst reg_val.Types.snd st1) st0
635 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
638 (** val block_of_register_pair :
639 Registers.register -> Registers.register -> rTL_state -> Pointers.block
641 let block_of_register_pair r1 r2 st =
643 (Monad.m_bind0 (Monad.max_def Errors.res0)
644 (Obj.magic (rtl_reg_retrieve st r1)) (fun v1 ->
645 Monad.m_bind0 (Monad.max_def Errors.res0)
646 (Obj.magic (rtl_reg_retrieve st r2)) (fun v2 ->
647 Monad.m_bind0 (Monad.max_def Errors.res0)
649 (BEMem.pointer_of_address { Types.fst = v1; Types.snd = v2 }))
650 (fun ptr -> Obj.magic (Errors.OK ptr.Pointers.pblock)))))
652 (** val eval_rtl_seq :
653 RTL.rtl_seq -> AST.ident -> rTL_state -> rTL_state Errors.res **)
654 let eval_rtl_seq stm curr_fn st =
655 let RTL.Rtl_stack_address (dreg1, dreg2) = stm in
657 (Monad.m_bind0 (Monad.max_def Errors.res0)
658 (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
659 let { Types.fst = dpl; Types.snd = dph } =
660 ByteValues.beval_pair_of_pointer (Types.pi1 sp)
662 let st0 = rtl_reg_store dreg1 dpl st in
663 Monad.m_return0 (Monad.max_def Errors.res0)
664 (rtl_reg_store dreg2 dph st0)))
666 (** val reg_res_store :
667 PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
669 let reg_res_store r v s =
670 Errors.OK (reg_sp_store r v s)
672 (** val rTL_semantics_separate : SemanticsUtils.sem_graph_params **)
673 let rTL_semantics_separate =
674 { SemanticsUtils.sgp_pars =
675 (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
676 SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
677 rTL_state_params; Joint_semantics.acca_store_ =
678 (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
679 (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
680 (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
681 (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
682 (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
683 (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
684 (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
685 (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
686 (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
687 (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
688 (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
689 (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
690 (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
692 let { Types.fst = dest; Types.snd = src } = Obj.magic p in
694 (Monad.m_bind0 (Monad.max_def Errors.res0)
695 (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
696 Monad.m_return0 (Monad.max_def Errors.res0)
697 (reg_sp_store dest v (Obj.magic env)))));
698 Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
699 Joint_semantics.setup_call = (Obj.magic rtl_setup_call_separate);
700 Joint_semantics.fetch_external_args =
701 (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
702 (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
703 (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
704 (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
705 Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
706 ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
707 Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
708 Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
709 Joint_semantics.pop_frame = (fun x x0 x1 ->
710 Obj.magic rtl_pop_frame_separate) });
711 SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }
713 (** val rTL_semantics_separate_overflow : SemanticsUtils.sem_graph_params **)
714 let rTL_semantics_separate_overflow =
715 { SemanticsUtils.sgp_pars =
716 (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
717 SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
718 rTL_state_params; Joint_semantics.acca_store_ =
719 (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
720 (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
721 (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
722 (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
723 (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
724 (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
725 (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
726 (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
727 (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
728 (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
729 (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
730 (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
731 (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
733 let { Types.fst = dest; Types.snd = src } = Obj.magic p in
735 (Monad.m_bind0 (Monad.max_def Errors.res0)
736 (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
737 Monad.m_return0 (Monad.max_def Errors.res0)
738 (reg_sp_store dest v (Obj.magic env)))));
739 Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
740 Joint_semantics.setup_call =
741 (Obj.magic rtl_setup_call_separate_overflow);
742 Joint_semantics.fetch_external_args =
743 (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
744 (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
745 (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
746 (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
747 Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
748 ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
749 Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
750 Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
751 Joint_semantics.pop_frame = (fun x x0 x1 ->
752 Obj.magic rtl_pop_frame_separate) });
753 SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }
755 (** val rTL_semantics_unique : SemanticsUtils.sem_graph_params **)
756 let rTL_semantics_unique =
757 { SemanticsUtils.sgp_pars =
758 (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
759 SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
760 rTL_state_params; Joint_semantics.acca_store_ =
761 (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
762 (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
763 (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
764 (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
765 (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
766 (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
767 (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
768 (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
769 (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
770 (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
771 (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
772 (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
773 (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
775 let { Types.fst = dest; Types.snd = src } = Obj.magic p in
777 (Monad.m_bind0 (Monad.max_def Errors.res0)
778 (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
779 Monad.m_return0 (Monad.max_def Errors.res0)
780 (reg_sp_store dest v (Obj.magic env)))));
781 Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
782 Joint_semantics.setup_call = (Obj.magic rtl_setup_call_unique);
783 Joint_semantics.fetch_external_args =
784 (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
785 (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
786 (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
787 (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
788 Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
789 ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
790 Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
791 Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
792 Joint_semantics.pop_frame = (fun x x0 x1 ->
793 Obj.magic rtl_pop_frame_unique) });
794 SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }