open Preamble

open ExtraMonads

open Deqsets_extra

open State

open Bind_new

open BindLists

open Blocks

open TranslateUtils

open ExtraGlobalenvs

open I8051bis

open String

open Sets

open Listb

open LabelledObjects

open BitVectorTrie

open Graphs

open I8051

open Order

open Registers

open BackEndOps

open Joint

open BEMem

open CostLabel

open Events

open IOMonad

open IO

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open Hide

open ByteValues

open Division

open Z

open BitVectorZ

open Pointers

open GenMem

open FrontEndMem

open Proper

open PositiveMap

open Deqsets

open Extralib

open Lists

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open ErrorMessages

open Option

open Setoids

open Monad

open Jmeq

open Russell

open Positive

open PreIdentifiers

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Errors

open Globalenvs

open Joint_semantics

open SemanticsUtils

open RTL

type reg_sp = { reg_sp_env : ByteValues.beval Identifiers.identifier_map;
                stackp : ByteValues.xpointer }

(** val reg_sp_rect_Type4 :
    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    'a1) -> reg_sp -> 'a1 **)
let rec reg_sp_rect_Type4 h_mk_reg_sp x_25168 =
  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25168 in
  h_mk_reg_sp reg_sp_env0 stackp0

(** val reg_sp_rect_Type5 :
    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    'a1) -> reg_sp -> 'a1 **)
let rec reg_sp_rect_Type5 h_mk_reg_sp x_25170 =
  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25170 in
  h_mk_reg_sp reg_sp_env0 stackp0

(** val reg_sp_rect_Type3 :
    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    'a1) -> reg_sp -> 'a1 **)
let rec reg_sp_rect_Type3 h_mk_reg_sp x_25172 =
  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25172 in
  h_mk_reg_sp reg_sp_env0 stackp0

(** val reg_sp_rect_Type2 :
    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    'a1) -> reg_sp -> 'a1 **)
let rec reg_sp_rect_Type2 h_mk_reg_sp x_25174 =
  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25174 in
  h_mk_reg_sp reg_sp_env0 stackp0

(** val reg_sp_rect_Type1 :
    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    'a1) -> reg_sp -> 'a1 **)
let rec reg_sp_rect_Type1 h_mk_reg_sp x_25176 =
  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25176 in
  h_mk_reg_sp reg_sp_env0 stackp0

(** val reg_sp_rect_Type0 :
    (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer ->
    'a1) -> reg_sp -> 'a1 **)
let rec reg_sp_rect_Type0 h_mk_reg_sp x_25178 =
  let { reg_sp_env = reg_sp_env0; stackp = stackp0 } = x_25178 in
  h_mk_reg_sp reg_sp_env0 stackp0

(** val reg_sp_env :
    reg_sp -> ByteValues.beval Identifiers.identifier_map **)
let rec reg_sp_env xxx =
  xxx.reg_sp_env

(** val stackp : reg_sp -> ByteValues.xpointer **)
let rec stackp xxx =
  xxx.stackp

(** val reg_sp_inv_rect_Type4 :
    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
let reg_sp_inv_rect_Type4 hterm h1 =
  let hcut = reg_sp_rect_Type4 h1 hterm in hcut __

(** val reg_sp_inv_rect_Type3 :
    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
let reg_sp_inv_rect_Type3 hterm h1 =
  let hcut = reg_sp_rect_Type3 h1 hterm in hcut __

(** val reg_sp_inv_rect_Type2 :
    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
let reg_sp_inv_rect_Type2 hterm h1 =
  let hcut = reg_sp_rect_Type2 h1 hterm in hcut __

(** val reg_sp_inv_rect_Type1 :
    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
let reg_sp_inv_rect_Type1 hterm h1 =
  let hcut = reg_sp_rect_Type1 h1 hterm in hcut __

(** val reg_sp_inv_rect_Type0 :
    reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
    ByteValues.xpointer -> __ -> 'a1) -> 'a1 **)
let reg_sp_inv_rect_Type0 hterm h1 =
  let hcut = reg_sp_rect_Type0 h1 hterm in hcut __

(** val reg_sp_discr : reg_sp -> reg_sp -> __ **)
let reg_sp_discr x y =
  Logic.eq_rect_Type2 x
    (let { reg_sp_env = a0; stackp = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val reg_sp_jmdiscr : reg_sp -> reg_sp -> __ **)
let reg_sp_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { reg_sp_env = a0; stackp = a1 } = x in
    Obj.magic (fun _ dH -> dH __ __)) y

(** val dpi1__o__reg_sp_env__o__inject :
    (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
    Types.sig0 **)
let dpi1__o__reg_sp_env__o__inject x2 =
  x2.Types.dpi1.reg_sp_env

(** val eject__o__reg_sp_env__o__inject :
    reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map
    Types.sig0 **)
let eject__o__reg_sp_env__o__inject x2 =
  (Types.pi1 x2).reg_sp_env

(** val reg_sp_env__o__inject :
    reg_sp -> ByteValues.beval Identifiers.identifier_map Types.sig0 **)
let reg_sp_env__o__inject x1 =
  x1.reg_sp_env

(** val dpi1__o__reg_sp_env :
    (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map **)
let dpi1__o__reg_sp_env x1 =
  x1.Types.dpi1.reg_sp_env

(** val eject__o__reg_sp_env :
    reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map **)
let eject__o__reg_sp_env x1 =
  (Types.pi1 x1).reg_sp_env

(** val reg_sp_store :
    PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp **)
let reg_sp_store reg v locals =
  let locals' = SemanticsUtils.reg_store reg v locals.reg_sp_env in
  { reg_sp_env = locals'; stackp = locals.stackp }

(** val reg_sp_retrieve :
    reg_sp -> Registers.register -> ByteValues.beval Errors.res **)
let reg_sp_retrieve locals =
  SemanticsUtils.reg_retrieve locals.reg_sp_env

(** val reg_sp_empty : ByteValues.xpointer -> reg_sp **)
let reg_sp_empty x =
  { reg_sp_env = (Identifiers.empty_map PreIdentifiers.RegisterTag); stackp =
    x }

type frame = { fr_ret_regs : Registers.register List.list;
               fr_pc : ByteValues.program_counter;
               fr_carry : ByteValues.bebit; fr_regs : reg_sp }

(** val frame_rect_Type4 :
    (Registers.register List.list -> ByteValues.program_counter ->
    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
let rec frame_rect_Type4 h_mk_frame x_25194 =
  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    fr_regs = fr_regs0 } = x_25194
  in
  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0

(** val frame_rect_Type5 :
    (Registers.register List.list -> ByteValues.program_counter ->
    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
let rec frame_rect_Type5 h_mk_frame x_25196 =
  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    fr_regs = fr_regs0 } = x_25196
  in
  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0

(** val frame_rect_Type3 :
    (Registers.register List.list -> ByteValues.program_counter ->
    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
let rec frame_rect_Type3 h_mk_frame x_25198 =
  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    fr_regs = fr_regs0 } = x_25198
  in
  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0

(** val frame_rect_Type2 :
    (Registers.register List.list -> ByteValues.program_counter ->
    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
let rec frame_rect_Type2 h_mk_frame x_25200 =
  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    fr_regs = fr_regs0 } = x_25200
  in
  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0

(** val frame_rect_Type1 :
    (Registers.register List.list -> ByteValues.program_counter ->
    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
let rec frame_rect_Type1 h_mk_frame x_25202 =
  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    fr_regs = fr_regs0 } = x_25202
  in
  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0

(** val frame_rect_Type0 :
    (Registers.register List.list -> ByteValues.program_counter ->
    ByteValues.bebit -> reg_sp -> 'a1) -> frame -> 'a1 **)
let rec frame_rect_Type0 h_mk_frame x_25204 =
  let { fr_ret_regs = fr_ret_regs0; fr_pc = fr_pc0; fr_carry = fr_carry0;
    fr_regs = fr_regs0 } = x_25204
  in
  h_mk_frame fr_ret_regs0 fr_pc0 fr_carry0 fr_regs0

(** val fr_ret_regs : frame -> Registers.register List.list **)
let rec fr_ret_regs xxx =
  xxx.fr_ret_regs

(** val fr_pc : frame -> ByteValues.program_counter **)
let rec fr_pc xxx =
  xxx.fr_pc

(** val fr_carry : frame -> ByteValues.bebit **)
let rec fr_carry xxx =
  xxx.fr_carry

(** val fr_regs : frame -> reg_sp **)
let rec fr_regs xxx =
  xxx.fr_regs

(** val frame_inv_rect_Type4 :
    frame -> (Registers.register List.list -> ByteValues.program_counter ->
    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
let frame_inv_rect_Type4 hterm h1 =
  let hcut = frame_rect_Type4 h1 hterm in hcut __

(** val frame_inv_rect_Type3 :
    frame -> (Registers.register List.list -> ByteValues.program_counter ->
    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
let frame_inv_rect_Type3 hterm h1 =
  let hcut = frame_rect_Type3 h1 hterm in hcut __

(** val frame_inv_rect_Type2 :
    frame -> (Registers.register List.list -> ByteValues.program_counter ->
    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
let frame_inv_rect_Type2 hterm h1 =
  let hcut = frame_rect_Type2 h1 hterm in hcut __

(** val frame_inv_rect_Type1 :
    frame -> (Registers.register List.list -> ByteValues.program_counter ->
    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
let frame_inv_rect_Type1 hterm h1 =
  let hcut = frame_rect_Type1 h1 hterm in hcut __

(** val frame_inv_rect_Type0 :
    frame -> (Registers.register List.list -> ByteValues.program_counter ->
    ByteValues.bebit -> reg_sp -> __ -> 'a1) -> 'a1 **)
let frame_inv_rect_Type0 hterm h1 =
  let hcut = frame_rect_Type0 h1 hterm in hcut __

(** val frame_discr : frame -> frame -> __ **)
let frame_discr x y =
  Logic.eq_rect_Type2 x
    (let { fr_ret_regs = a0; fr_pc = a1; fr_carry = a2; fr_regs = a3 } = x in
    Obj.magic (fun _ dH -> dH __ __ __ __)) y

(** val frame_jmdiscr : frame -> frame -> __ **)
let frame_jmdiscr x y =
  Logic.eq_rect_Type2 x
    (let { fr_ret_regs = a0; fr_pc = a1; fr_carry = a2; fr_regs = a3 } = x in
    Obj.magic (fun _ dH -> dH __ __ __ __)) y

(** val rTL_state_params : Joint_semantics.sem_state_params **)
let rTL_state_params =
  { Joint_semantics.empty_framesT = (Obj.magic List.Nil);
    Joint_semantics.empty_regsT = (Obj.magic reg_sp_empty);
    Joint_semantics.load_sp = (fun env -> Errors.OK (Obj.magic env).stackp);
    Joint_semantics.save_sp = (fun env ->
    Obj.magic (fun x -> { reg_sp_env = (Obj.magic env).reg_sp_env; stackp =
      x })) }

type rTL_state = Joint_semantics.state

(** val rtl_arg_retrieve :
    reg_sp -> Joint.psd_argument -> ByteValues.beval Errors.res **)
let rtl_arg_retrieve env = function
| Joint.Reg r -> SemanticsUtils.reg_retrieve env.reg_sp_env r
| Joint.Imm b -> Errors.OK (ByteValues.BVByte b)

(** val rtl_fetch_ra :
    rTL_state -> (rTL_state, ByteValues.program_counter) Types.prod
    Errors.res **)
let rtl_fetch_ra st =
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic
        (Errors.opt_to_res (List.Cons ((Errors.MSG
          ErrorMessages.FrameErrorOnPop), List.Nil))
          st.Joint_semantics.st_frms)) (fun frms ->
      match frms with
      | List.Nil ->
        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
          ErrorMessages.EmptyStack), List.Nil)))
      | List.Cons (hd, tl) ->
        Obj.magic (Errors.OK { Types.fst = st; Types.snd = hd.fr_pc })))

(** val rtl_init_local : Registers.register -> reg_sp -> reg_sp **)
let rtl_init_local local =
  reg_sp_store local ByteValues.BVundef

(** val rtl_setup_call_separate :
    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
    -> rTL_state -> rTL_state Errors.res **)
let rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st =
  (let { Types.fst = mem; Types.snd = b } =
     GenMem.alloc st.Joint_semantics.m (Z.z_of_nat Nat.O)
       (Z.z_of_nat stacksize)
   in
  (fun _ ->
  let sp = { Pointers.pblock = b; Pointers.poff =
    (BitVector.zero Pointers.offset_size) }
  in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic
        (Errors.mfold_left2 (fun lenv dest src ->
          Obj.magic
            (Monad.m_bind0 (Monad.max_def Errors.res0)
              (Obj.magic
                (rtl_arg_retrieve (Obj.magic st.Joint_semantics.regs) src))
              (fun v -> Obj.magic (Errors.OK (reg_sp_store dest v lenv)))))
          (Errors.OK (reg_sp_empty sp)) formal_arg_regs actual_arg_regs))
      (fun new_regs ->
      Obj.magic (Errors.OK
        (Joint_semantics.set_regs rTL_state_params new_regs
          (Joint_semantics.set_m rTL_state_params mem st))))))) __

(** val rtl_setup_call_separate_overflow :
    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
    -> rTL_state -> rTL_state Errors.res **)
let rtl_setup_call_separate_overflow stacksize formal_arg_regs actual_arg_regs st =
  match Nat.leb (Nat.S (Nat.plus stacksize st.Joint_semantics.stack_usage))
          (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S Nat.O))))))))))))))))) with
  | Bool.True ->
    rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st
  | Bool.False ->
    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.StackOverflow),
      List.Nil))

(** val rtl_setup_call_unique :
    Nat.nat -> Registers.register List.list -> Joint.psd_argument List.list
    -> rTL_state -> rTL_state Errors.res **)
let rtl_setup_call_unique stacksize formal_arg_regs actual_arg_regs st =
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
      let newsp =
        Pointers.neg_shift_pointer (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S Nat.O)))))))) (Types.pi1 sp)
          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
            (Nat.S (Nat.S (Nat.S Nat.O)))))))) stacksize)
      in
      Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic
          (Errors.mfold_left2 (fun lenv dest src ->
            Obj.magic
              (Monad.m_bind0 (Monad.max_def Errors.res0)
                (Obj.magic
                  (rtl_arg_retrieve (Obj.magic st.Joint_semantics.regs) src))
                (fun v -> Obj.magic (Errors.OK (reg_sp_store dest v lenv)))))
            (Errors.OK (reg_sp_empty newsp)) formal_arg_regs actual_arg_regs))
        (fun new_regs ->
        Obj.magic (Errors.OK
          (Joint_semantics.set_regs rTL_state_params new_regs st)))))

type rTL_state_pc = Joint_semantics.state_pc

(** val rtl_save_frame :
    Registers.register List.list -> rTL_state_pc -> __ **)
let rtl_save_frame retregs st =
  Monad.m_bind0 (Monad.max_def Errors.res0)
    (Obj.magic
      (Errors.opt_to_res (List.Cons ((Errors.MSG
        ErrorMessages.FrameErrorOnPush), List.Nil))
        st.Joint_semantics.st_no_pc.Joint_semantics.st_frms)) (fun frms ->
    let frame0 = List.Cons ({ fr_ret_regs = retregs; fr_pc =
      st.Joint_semantics.pc; fr_carry =
      st.Joint_semantics.st_no_pc.Joint_semantics.carry; fr_regs =
      (Obj.magic st.Joint_semantics.st_no_pc.Joint_semantics.regs) }, frms)
    in
    Obj.magic (Errors.OK
      (Joint_semantics.set_frms rTL_state_params (Obj.magic frame0)
        st.Joint_semantics.st_no_pc)))

(** val rtl_fetch_external_args :
    AST.external_function -> rTL_state -> Joint.psd_argument List.list ->
    Values.val0 List.list Errors.res **)
let rtl_fetch_external_args _ =
  failwith "AXIOM TO BE REALIZED"

(** val rtl_set_result :
    Values.val0 List.list -> Registers.register List.list -> rTL_state ->
    rTL_state Errors.res **)
let rtl_set_result _ =
  failwith "AXIOM TO BE REALIZED"

(** val rtl_reg_store :
    PreIdentifiers.identifier -> ByteValues.beval -> Joint_semantics.state ->
    Joint_semantics.state **)
let rtl_reg_store r v st =
  let mem = reg_sp_store r v (Obj.magic st.Joint_semantics.regs) in
  Joint_semantics.set_regs rTL_state_params (Obj.magic mem) st

(** val rtl_reg_retrieve :
    Joint_semantics.state -> Registers.register -> ByteValues.beval
    Errors.res **)
let rtl_reg_retrieve st l =
  reg_sp_retrieve (Obj.magic st.Joint_semantics.regs) l

(** val rtl_read_result :
    Registers.register List.list -> rTL_state -> ByteValues.beval List.list
    Errors.res **)
let rtl_read_result rets st =
  Obj.magic
    (Monad.m_list_map (Monad.max_def Errors.res0)
      (Obj.magic (rtl_reg_retrieve st)) rets)

(** val rtl_pop_frame_separate :
    Registers.register List.list -> rTL_state -> (rTL_state,
    ByteValues.program_counter) Types.prod Errors.res **)
let rtl_pop_frame_separate ret st =
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic
        (Errors.opt_to_res (List.Cons ((Errors.MSG
          ErrorMessages.FrameErrorOnPop), List.Nil))
          st.Joint_semantics.st_frms)) (fun frms ->
      match frms with
      | List.Nil ->
        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
          ErrorMessages.EmptyStack), List.Nil)))
      | List.Cons (hd, tl) ->
        Monad.m_bind0 (Monad.max_def Errors.res0)
          (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
          let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
          Monad.m_bind0 (Monad.max_def Errors.res0)
            (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
            let st0 =
              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
                (Joint_semantics.set_regs rTL_state_params
                  (Obj.magic hd.fr_regs)
                  (Joint_semantics.set_carry rTL_state_params hd.fr_carry
                    (Joint_semantics.set_m rTL_state_params
                      (GenMem.free st.Joint_semantics.m
                        (Types.pi1 sp).Pointers.pblock) st)))
            in
            let pc = hd.fr_pc in
            let st1 =
              Util.foldl (fun st1 reg_val ->
                rtl_reg_store reg_val.Types.fst reg_val.Types.snd st1) st0
                reg_vals
            in
            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
              Types.snd = pc }))))

(** val rtl_pop_frame_unique :
    Registers.register List.list -> rTL_state -> (rTL_state,
    ByteValues.program_counter) Types.prod Errors.res **)
let rtl_pop_frame_unique ret st =
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic
        (Errors.opt_to_res (List.Cons ((Errors.MSG
          ErrorMessages.FrameErrorOnPop), List.Nil))
          st.Joint_semantics.st_frms)) (fun frms ->
      match frms with
      | List.Nil ->
        Obj.magic (Errors.Error (List.Cons ((Errors.MSG
          ErrorMessages.EmptyStack), List.Nil)))
      | List.Cons (hd, tl) ->
        Monad.m_bind0 (Monad.max_def Errors.res0)
          (Obj.magic (rtl_read_result ret st)) (fun ret_vals ->
          let reg_vals = Util.zip_pottier hd.fr_ret_regs ret_vals in
          Monad.m_bind0 (Monad.max_def Errors.res0)
            (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
            let st0 =
              Joint_semantics.set_frms rTL_state_params (Obj.magic tl)
                (Joint_semantics.set_regs rTL_state_params
                  (Obj.magic hd.fr_regs)
                  (Joint_semantics.set_carry rTL_state_params hd.fr_carry st))
            in
            let pc = hd.fr_pc in
            let st1 =
              Util.foldl (fun st1 reg_val ->
                rtl_reg_store reg_val.Types.fst reg_val.Types.snd st1) st0
                reg_vals
            in
            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st1;
              Types.snd = pc }))))

(** val block_of_register_pair :
    Registers.register -> Registers.register -> rTL_state -> Pointers.block
    Errors.res **)
let block_of_register_pair r1 r2 st =
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (rtl_reg_retrieve st r1)) (fun v1 ->
      Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic (rtl_reg_retrieve st r2)) (fun v2 ->
        Monad.m_bind0 (Monad.max_def Errors.res0)
          (Obj.magic
            (BEMem.pointer_of_address { Types.fst = v1; Types.snd = v2 }))
          (fun ptr -> Obj.magic (Errors.OK ptr.Pointers.pblock)))))

(** val eval_rtl_seq :
    RTL.rtl_seq -> AST.ident -> rTL_state -> rTL_state Errors.res **)
let eval_rtl_seq stm curr_fn st =
  let RTL.Rtl_stack_address (dreg1, dreg2) = stm in
  Obj.magic
    (Monad.m_bind0 (Monad.max_def Errors.res0)
      (Obj.magic (Joint_semantics.sp rTL_state_params st)) (fun sp ->
      let { Types.fst = dpl; Types.snd = dph } =
        ByteValues.beval_pair_of_pointer (Types.pi1 sp)
      in
      let st0 = rtl_reg_store dreg1 dpl st in
      Monad.m_return0 (Monad.max_def Errors.res0)
        (rtl_reg_store dreg2 dph st0)))

(** val reg_res_store :
    PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
    Errors.res **)
let reg_res_store r v s =
  Errors.OK (reg_sp_store r v s)

(** val rTL_semantics_separate : SemanticsUtils.sem_graph_params **)
let rTL_semantics_separate =
  { SemanticsUtils.sgp_pars =
    (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
    SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
    rTL_state_params; Joint_semantics.acca_store_ =
    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
    (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
    (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
    (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
    (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
    (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
    (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
    (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
    (fun env p ->
    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
    Obj.magic
      (Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
        Monad.m_return0 (Monad.max_def Errors.res0)
          (reg_sp_store dest v (Obj.magic env)))));
    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
    Joint_semantics.setup_call = (Obj.magic rtl_setup_call_separate);
    Joint_semantics.fetch_external_args =
    (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
    (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
      Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
      ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
    Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
    Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
    Joint_semantics.pop_frame = (fun x x0 x1 ->
    Obj.magic rtl_pop_frame_separate) });
    SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }

(** val rTL_semantics_separate_overflow : SemanticsUtils.sem_graph_params **)
let rTL_semantics_separate_overflow =
  { SemanticsUtils.sgp_pars =
    (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
    SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
    rTL_state_params; Joint_semantics.acca_store_ =
    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
    (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
    (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
    (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
    (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
    (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
    (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
    (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
    (fun env p ->
    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
    Obj.magic
      (Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
        Monad.m_return0 (Monad.max_def Errors.res0)
          (reg_sp_store dest v (Obj.magic env)))));
    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
    Joint_semantics.setup_call =
    (Obj.magic rtl_setup_call_separate_overflow);
    Joint_semantics.fetch_external_args =
    (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
    (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
      Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
      ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
    Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
    Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
    Joint_semantics.pop_frame = (fun x x0 x1 ->
    Obj.magic rtl_pop_frame_separate) });
    SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }

(** val rTL_semantics_unique : SemanticsUtils.sem_graph_params **)
let rTL_semantics_unique =
  { SemanticsUtils.sgp_pars =
    (Joint.gp_to_p__o__stmt_pars__o__uns_pars RTL.rTL);
    SemanticsUtils.sgp_sup = (fun _ -> { Joint_semantics.st_pars =
    rTL_state_params; Joint_semantics.acca_store_ =
    (Obj.magic reg_res_store); Joint_semantics.acca_retrieve_ =
    (Obj.magic reg_sp_retrieve); Joint_semantics.acca_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.accb_store_ =
    (Obj.magic reg_res_store); Joint_semantics.accb_retrieve_ =
    (Obj.magic reg_sp_retrieve); Joint_semantics.accb_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.dpl_store_ =
    (Obj.magic reg_res_store); Joint_semantics.dpl_retrieve_ =
    (Obj.magic reg_sp_retrieve); Joint_semantics.dpl_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.dph_store_ =
    (Obj.magic reg_res_store); Joint_semantics.dph_retrieve_ =
    (Obj.magic reg_sp_retrieve); Joint_semantics.dph_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.snd_arg_retrieve_ =
    (Obj.magic rtl_arg_retrieve); Joint_semantics.pair_reg_move_ =
    (fun env p ->
    let { Types.fst = dest; Types.snd = src } = Obj.magic p in
    Obj.magic
      (Monad.m_bind0 (Monad.max_def Errors.res0)
        (Obj.magic (rtl_arg_retrieve (Obj.magic env) src)) (fun v ->
        Monad.m_return0 (Monad.max_def Errors.res0)
          (reg_sp_store dest v (Obj.magic env)))));
    Joint_semantics.save_frame = (fun x -> Obj.magic rtl_save_frame);
    Joint_semantics.setup_call = (Obj.magic rtl_setup_call_unique);
    Joint_semantics.fetch_external_args =
    (Obj.magic rtl_fetch_external_args); Joint_semantics.set_result =
    (Obj.magic rtl_set_result); Joint_semantics.call_args_for_main =
    (Obj.magic List.Nil); Joint_semantics.call_dest_for_main =
    (Obj.magic (List.Cons (Positive.One, (List.Cons ((Positive.P0
      Positive.One), (List.Cons ((Positive.P1 Positive.One), (List.Cons
      ((Positive.P0 (Positive.P0 Positive.One)), List.Nil)))))))));
    Joint_semantics.read_result = (fun x x0 -> Obj.magic rtl_read_result);
    Joint_semantics.eval_ext_seq = (fun x x0 -> Obj.magic eval_rtl_seq);
    Joint_semantics.pop_frame = (fun x x0 x1 ->
    Obj.magic rtl_pop_frame_unique) });
    SemanticsUtils.graph_pre_main_generator = RTL.rTL_premain }