Arm_lowering (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.Arm

val fv_NF : Lowering.fresh_vars -> Ident.Ident.ident

val fv_ZF : Lowering.fresh_vars -> Ident.Ident.ident

val fv_CF : Lowering.fresh_vars -> Ident.Ident.ident

val fv_VF : Lowering.fresh_vars -> Ident.Ident.ident

val all_fresh_vars : Lowering.fresh_vars -> Ident.Ident.ident list

val fvNF : Lowering.fresh_vars -> Var0.Var.var

val fvZF : Lowering.fresh_vars -> Var0.Var.var

val fvCF : Lowering.fresh_vars -> Var0.Var.var

val fvVF : Lowering.fresh_vars -> Var0.Var.var

val fresh_flags : Lowering.fresh_vars -> Var0.Var.var list

val fvars : Lowering.fresh_vars -> Var0.SvExtra.Sv.t

type low_expr =
  ((Arm_decl.register,
     Arch_utils.empty,
     Arch_utils.empty,
     Arm_decl.rflag,
     Arm_decl.condt,
     Arm_instr_decl.arm_op,
     Arm_extra.arm_extra_op)
     Arch_extra.extended_op
     Sopn.sopn
   * Expr.pexpr list)
    option

val le_skip : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  low_expr

val le_issue_sopn : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Sopn.sopn ->
  Expr.pexpr list ->
  low_expr

val le_issue_aop : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Arm_instr_decl.arm_op ->
  Expr.pexpr list ->
  low_expr

val le_issue_opts : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Arm_instr_decl.arm_mnemonic ->
  Arm_instr_decl.arm_options ->
  Expr.pexpr list ->
  low_expr

val le_issue : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Arm_instr_decl.arm_mnemonic ->
  Expr.pexpr list ->
  low_expr

val no_pre : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  low_expr ->
  (((Arm_decl.register,
      Arch_utils.empty,
      Arch_utils.empty,
      Arm_decl.rflag,
      Arm_decl.condt,
      Arm_instr_decl.arm_op,
      Arm_extra.arm_extra_op)
      Arch_extra.extended_op
      Expr.instr_r
      list
    * (Arm_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_decl.rflag,
        Arm_decl.condt,
        Arm_instr_decl.arm_op,
        Arm_extra.arm_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val chk_ws_reg : Wsize.wsize -> unit option

val flags_of_mn : 
  Lowering.fresh_vars ->
  Arm_instr_decl.arm_mnemonic ->
  Var0.Var.var list

val lflags_of_mn : 
  Lowering.fresh_vars ->
  Expr.var_info ->
  Arm_instr_decl.arm_mnemonic ->
  Expr.lval list

val lower_TST : Expr.pexpr -> Expr.pexpr -> Expr.pexpr list option

val lower_condition_Papp2 : 
  Lowering.fresh_vars ->
  Expr.var_info ->
  Expr.sop2 ->
  Expr.pexpr ->
  Expr.pexpr ->
  ((Arm_instr_decl.arm_mnemonic * Expr.pexpr) * Expr.pexpr list) option

val lower_condition_pexpr : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  Expr.var_info ->
  Expr.pexpr ->
  (((Expr.lval list
     * (Arm_decl.register,
         Arch_utils.empty,
         Arch_utils.empty,
         Arm_decl.rflag,
         Arm_decl.condt,
         Arm_instr_decl.arm_op,
         Arm_extra.arm_extra_op)
         Arch_extra.extended_op
         Sopn.sopn)
    * Expr.pexpr list)
   * Expr.pexpr)
    option

val lower_condition : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  Expr.var_info ->
  Expr.pexpr ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Expr.instr_r
    list
  * Expr.pexpr

val get_arg_shift : 
  Wsize.wsize ->
  Expr.pexpr list ->
  ((Expr.pexpr * Shift_kind.shift_kind) * Expr.pexpr) option

val arg_shift : 
  Arm_instr_decl.arm_mnemonic ->
  Wsize.wsize ->
  Expr.pexpr list ->
  Arm_instr_decl.arm_op * Expr.pexpr list

val lower_Pvar : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Expr.gvar ->
  low_expr

val lower_load : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Expr.pexpr ->
  low_expr

val mov_imm_op : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.pexpr ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Sopn.sopn

val lower_Papp1 : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Expr.sop1 ->
  Expr.pexpr ->
  low_expr

val is_mul : Expr.pexpr -> (Expr.pexpr * Expr.pexpr) option

val is_rsb : Wsize.wsize -> Expr.pexpr -> Expr.pexpr -> bool

val lower_Papp2_op : 
  Wsize.wsize ->
  Expr.sop2 ->
  Expr.pexpr ->
  Expr.pexpr ->
  ((Arm_instr_decl.arm_mnemonic * Expr.pexpr) * Expr.pexpr list) option

val lower_Papp2 : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Expr.sop2 ->
  Expr.pexpr ->
  Expr.pexpr ->
  low_expr

val lower_pexpr_aux : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Expr.pexpr ->
  low_expr

val sopn_set_is_conditional : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Sopn.sopn ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Sopn.sopn
    option

val lower_pexpr : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  Expr.var_info ->
  Wsize.wsize ->
  Expr.pexpr ->
  (((Arm_decl.register,
      Arch_utils.empty,
      Arch_utils.empty,
      Arm_decl.rflag,
      Arm_decl.condt,
      Arm_instr_decl.arm_op,
      Arm_extra.arm_extra_op)
      Arch_extra.extended_op
      Expr.instr_r
      list
    * (Arm_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_decl.rflag,
        Arm_decl.condt,
        Arm_instr_decl.arm_op,
        Arm_extra.arm_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val lower_store : 
  Wsize.wsize ->
  Expr.pexpr ->
  (Arm_instr_decl.arm_op * Expr.pexpr list) option

val lower_cassgn_word : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  Expr.lval ->
  Wsize.wsize ->
  Expr.pexpr ->
  ((Arm_decl.register,
     Arch_utils.empty,
     Arch_utils.empty,
     Arm_decl.rflag,
     Arm_decl.condt,
     Arm_instr_decl.arm_op,
     Arm_extra.arm_extra_op)
     Arch_extra.extended_op
     Expr.instr_r
     list
   * ((Expr.lval list
       * (Arm_decl.register,
           Arch_utils.empty,
           Arch_utils.empty,
           Arm_decl.rflag,
           Arm_decl.condt,
           Arm_instr_decl.arm_op,
           Arm_extra.arm_extra_op)
           Arch_extra.extended_op
           Sopn.sopn)
      * Expr.pexpr list))
    option

val lower_cassgn_bool : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  Expr.lval ->
  Expr.assgn_tag ->
  Expr.pexpr ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Expr.instr_r
    list
    option

val lower_add_carry : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.lval list ->
  Expr.pexpr list ->
  ((Expr.lval list
    * (Arm_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_decl.rflag,
        Arm_decl.condt,
        Arm_instr_decl.arm_op,
        Arm_extra.arm_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val lower_mulu : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.lval list ->
  Expr.pexpr list ->
  ((Expr.lval list
    * (Arm_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_decl.rflag,
        Arm_decl.condt,
        Arm_instr_decl.arm_op,
        Arm_extra.arm_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val with_shift : 
  Arm_instr_decl.arm_options ->
  Shift_kind.shift_kind ->
  Arm_instr_decl.arm_options

val lower_base_op : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.lval list ->
  Arm_instr_decl.arm_op ->
  Expr.pexpr list ->
  ((Expr.lval list
    * (Arm_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_decl.rflag,
        Arm_decl.condt,
        Arm_instr_decl.arm_op,
        Arm_extra.arm_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val lower_swap : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Type.stype ->
  Expr.lval list ->
  Expr.pexpr list ->
  ((Expr.lval list
    * (Arm_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_decl.rflag,
        Arm_decl.condt,
        Arm_instr_decl.arm_op,
        Arm_extra.arm_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val lower_pseudo_operator : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.lval list ->
  Pseudo_operator.pseudo_operator ->
  Expr.pexpr list ->
  ((Expr.lval list
    * (Arm_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_decl.rflag,
        Arm_decl.condt,
        Arm_instr_decl.arm_op,
        Arm_extra.arm_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val lower_copn : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.lval list ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Sopn.sopn ->
  Expr.pexpr list ->
  ((Expr.lval list
    * (Arm_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_decl.rflag,
        Arm_decl.condt,
        Arm_instr_decl.arm_op,
        Arm_extra.arm_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

type lowering_options = unit

val lower_i : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Expr.instr ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Expr.instr
    list