Armv8a_lowering (p.jasmin.2026.09.0.doc.jasmin.jasmin.Jasmin.Armv8a

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 =
  ((Armv8a_decl.register,
     Arch_utils.empty,
     Arch_utils.empty,
     Arm_common.rflag,
     Arm_common.condt,
     Armv8a_instr_decl.armv8a_asm_op,
     Armv8a_extra.armv8a_extra_op)
     Arch_extra.extended_op
     Sopn.sopn
   * Expr.pexpr list)
    option

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

val le_issue_sopn : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt,
    Armv8a_instr_decl.armv8a_asm_op,
    Armv8a_extra.armv8a_extra_op)
    Arch_extra.extended_op
    Sopn.sopn ->
  Expr.pexpr list ->
  low_expr

val le_issue_extra : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt,
    Armv8a_instr_decl.armv8a_asm_op,
    Armv8a_extra.armv8a_extra_op)
    Arch_extra.extra_op_t ->
  Expr.pexpr list ->
  low_expr

val le_issue_aop : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt,
    Armv8a_instr_decl.armv8a_asm_op)
    Arch_decl.asm_op_t' ->
  Expr.pexpr list ->
  low_expr

val le_issue_opts : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Armv8a_instr_decl.armv8a_mnemonic ->
  Armv8a_instr_decl.armv8a_options ->
  Expr.pexpr list ->
  low_expr

val le_issue : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Armv8a_instr_decl.armv8a_mnemonic ->
  Wsize.wsize ->
  Expr.pexpr list ->
  low_expr

val no_pre : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  low_expr ->
  (((Armv8a_decl.register,
      Arch_utils.empty,
      Arch_utils.empty,
      Arm_common.rflag,
      Arm_common.condt,
      Armv8a_instr_decl.armv8a_asm_op,
      Armv8a_extra.armv8a_extra_op)
      Arch_extra.extended_op
      Expr.instr_r
      list
    * (Armv8a_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_common.rflag,
        Arm_common.condt,
        Armv8a_instr_decl.armv8a_asm_op,
        Armv8a_extra.armv8a_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 ->
  Armv8a_instr_decl.armv8a_mnemonic ->
  Var0.Var.var list

val lflags_of_mn : 
  Lowering.fresh_vars ->
  Expr.var_info ->
  Armv8a_instr_decl.armv8a_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 ->
  Operators.sop2 ->
  Expr.pexpr ->
  Expr.pexpr ->
  (((Armv8a_instr_decl.armv8a_mnemonic * Wsize.wsize) * Expr.pexpr)
   * Expr.pexpr list)
    option

val lower_condition_pexpr : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  Expr.var_info ->
  Expr.pexpr ->
  (((Expr.lval list
     * (Armv8a_decl.register,
         Arch_utils.empty,
         Arch_utils.empty,
         Arm_common.rflag,
         Arm_common.condt,
         Armv8a_instr_decl.armv8a_asm_op,
         Armv8a_extra.armv8a_extra_op)
         Arch_extra.extended_op
         Sopn.sopn)
    * Expr.pexpr list)
   * Expr.pexpr)
    option

val lower_condition : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  Expr.var_info ->
  Expr.pexpr ->
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt,
    Armv8a_instr_decl.armv8a_asm_op,
    Armv8a_extra.armv8a_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 : 
  Armv8a_instr_decl.armv8a_mnemonic ->
  Wsize.wsize ->
  Expr.pexpr list ->
  Armv8a_instr_decl.armv8a_asm_op * Expr.pexpr list

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

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

val mov_imm_op : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Expr.pexpr ->
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt,
    Armv8a_instr_decl.armv8a_asm_op,
    Armv8a_extra.armv8a_extra_op)
    Arch_extra.extended_op
    Sopn.sopn

val uload_mn : 
  Wsize.wsize ->
  Wsize.wsize ->
  Armv8a_instr_decl.armv8a_mnemonic option

val sload_mn : 
  Wsize.wsize ->
  Wsize.wsize ->
  Armv8a_instr_decl.armv8a_mnemonic option

val sext_mn : 
  Wsize.wsize ->
  Wsize.wsize ->
  Armv8a_instr_decl.armv8a_mnemonic option

val uext_mn : 
  Wsize.wsize ->
  Wsize.wsize ->
  Armv8a_instr_decl.armv8a_mnemonic option

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

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

val check_shift_expr : Wsize.wsize -> Expr.pexpr -> Expr.pexpr option

val lower_Papp2_op : 
  Wsize.wsize ->
  Operators.sop2 ->
  Expr.pexpr ->
  Expr.pexpr ->
  ((Armv8a_instr_decl.armv8a_mnemonic * Expr.pexpr) * Expr.pexpr list) option

val large_arith_imm : 
  Wsize.wsize ->
  Armv8a_instr_decl.armv8a_mnemonic ->
  Expr.pexpr list ->
  BinNums.coq_Z option

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

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

val is_csel_arg : Expr.pexpr -> bool

val lower_Pif : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  Expr.var_info ->
  Wsize.wsize ->
  Expr.pexpr ->
  Expr.pexpr ->
  Expr.pexpr ->
  (((Armv8a_decl.register,
      Arch_utils.empty,
      Arch_utils.empty,
      Arm_common.rflag,
      Arm_common.condt,
      Armv8a_instr_decl.armv8a_asm_op,
      Armv8a_extra.armv8a_extra_op)
      Arch_extra.extended_op
      Expr.instr_r
      list
    * (Armv8a_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_common.rflag,
        Arm_common.condt,
        Armv8a_instr_decl.armv8a_asm_op,
        Armv8a_extra.armv8a_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val lower_pexpr : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  Expr.var_info ->
  Wsize.wsize ->
  Expr.pexpr ->
  (((Armv8a_decl.register,
      Arch_utils.empty,
      Arch_utils.empty,
      Arm_common.rflag,
      Arm_common.condt,
      Armv8a_instr_decl.armv8a_asm_op,
      Armv8a_extra.armv8a_extra_op)
      Arch_extra.extended_op
      Expr.instr_r
      list
    * (Armv8a_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_common.rflag,
        Arm_common.condt,
        Armv8a_instr_decl.armv8a_asm_op,
        Armv8a_extra.armv8a_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val lower_store : 
  Wsize.wsize ->
  Expr.pexpr ->
  (Armv8a_instr_decl.armv8a_asm_op * Expr.pexpr list) option

val lower_cassgn_word : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  Expr.lval ->
  Wsize.wsize ->
  Expr.pexpr ->
  ((Armv8a_decl.register,
     Arch_utils.empty,
     Arch_utils.empty,
     Arm_common.rflag,
     Arm_common.condt,
     Armv8a_instr_decl.armv8a_asm_op,
     Armv8a_extra.armv8a_extra_op)
     Arch_extra.extended_op
     Expr.instr_r
     list
   * ((Expr.lval list
       * (Armv8a_decl.register,
           Arch_utils.empty,
           Arch_utils.empty,
           Arm_common.rflag,
           Arm_common.condt,
           Armv8a_instr_decl.armv8a_asm_op,
           Armv8a_extra.armv8a_extra_op)
           Arch_extra.extended_op
           Sopn.sopn)
      * Expr.pexpr list))
    option

val lower_cassgn_bool : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  Expr.lval ->
  Expr.assgn_tag ->
  Expr.pexpr ->
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt,
    Armv8a_instr_decl.armv8a_asm_op,
    Armv8a_extra.armv8a_extra_op)
    Arch_extra.extended_op
    Expr.instr_r
    list
    option

val isLnone : Expr.lval -> bool

val lower_add_carry : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.lval list ->
  Expr.pexpr list ->
  ((Expr.lval list
    * (Armv8a_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_common.rflag,
        Arm_common.condt,
        Armv8a_instr_decl.armv8a_asm_op,
        Armv8a_extra.armv8a_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val with_shift : 
  Armv8a_instr_decl.armv8a_options ->
  Shift_kind.shift_kind ->
  Armv8a_instr_decl.armv8a_options

val lower_base_op : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.lval list ->
  Armv8a_instr_decl.armv8a_asm_op ->
  Expr.pexpr list ->
  ((Expr.lval list
    * (Armv8a_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_common.rflag,
        Arm_common.condt,
        Armv8a_instr_decl.armv8a_asm_op,
        Armv8a_extra.armv8a_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val lower_swap : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Type.atype ->
  Expr.lval list ->
  Expr.pexpr list ->
  ((Expr.lval list
    * (Armv8a_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_common.rflag,
        Arm_common.condt,
        Armv8a_instr_decl.armv8a_asm_op,
        Armv8a_extra.armv8a_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val lower_pseudo_operator : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.lval list ->
  Pseudo_operator.pseudo_operator ->
  Expr.pexpr list ->
  ((Expr.lval list
    * (Armv8a_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_common.rflag,
        Arm_common.condt,
        Armv8a_instr_decl.armv8a_asm_op,
        Armv8a_extra.armv8a_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val lower_copn : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.lval list ->
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt,
    Armv8a_instr_decl.armv8a_asm_op,
    Armv8a_extra.armv8a_extra_op)
    Arch_extra.extended_op
    Sopn.sopn ->
  Expr.pexpr list ->
  ((Expr.lval list
    * (Armv8a_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_common.rflag,
        Arm_common.condt,
        Armv8a_instr_decl.armv8a_asm_op,
        Armv8a_extra.armv8a_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val lower_i : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt,
    Armv8a_instr_decl.armv8a_asm_op,
    Armv8a_extra.armv8a_extra_op)
    Arch_extra.extended_op
    Expr.instr ->
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt,
    Armv8a_instr_decl.armv8a_asm_op,
    Armv8a_extra.armv8a_extra_op)
    Arch_extra.extended_op
    Expr.instr
    list