X86_params (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.X86

val x86_op_align : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  Wsize.wsize ->
  (Fexpr.lexpr list
   * (X86_decl.register,
       X86_decl.register_ext,
       X86_decl.xmm_register,
       X86_decl.rflag,
       X86_decl.condt,
       X86_instr_decl.x86_op,
       X86_extra.x86_extra_op)
       Arch_extra.extended_op
       Sopn.sopn)
  * Fexpr.rexpr list

val x86_immediate : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  BinNums.coq_Z ->
  X86_extra.x86_extended_op Expr.instr_r

val x86_swap : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.assgn_tag ->
  Expr.var_i ->
  Expr.var_i ->
  Expr.var_i ->
  Expr.var_i ->
  X86_extra.x86_extended_op Expr.instr_r

val x86_saparams : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt,
    X86_instr_decl.x86_op,
    X86_extra.x86_extra_op)
    Arch_extra.extended_op
    Stack_alloc_params.stack_alloc_params

val x86_allocate_stack_frame : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i option ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list * X86_extra.x86_extended_op Sopn.sopn) * Fexpr.rexpr list)
    list

val x86_free_stack_frame : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i option ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list * X86_extra.x86_extended_op Sopn.sopn) * Fexpr.rexpr list)
    list

val x86_lassign : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Fexpr.lexpr ->
  Wsize.wsize ->
  Fexpr.rexpr ->
  (Fexpr.lexpr list * X86_extra.x86_extended_op Sopn.sopn) * Fexpr.rexpr list

val x86_set_up_sp_register : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  BinNums.coq_Z ->
  Wsize.wsize ->
  Expr.var_i ->
  Expr.var_i ->
  ((Fexpr.lexpr list
    * (X86_decl.register,
        X86_decl.register_ext,
        X86_decl.xmm_register,
        X86_decl.rflag,
        X86_decl.condt,
        X86_instr_decl.x86_op,
        X86_extra.x86_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Fexpr.rexpr list)
    list

val x86_lmove : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  (Fexpr.lexpr list * X86_extra.x86_extended_op Sopn.sopn) * Fexpr.rexpr list

val x86_check_ws : Wsize.wsize -> bool

val x86_lstore : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  BinNums.coq_Z ->
  Expr.var_i ->
  (Fexpr.lexpr list * X86_extra.x86_extended_op Sopn.sopn) * Fexpr.rexpr list

val x86_lload : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  BinNums.coq_Z ->
  (Fexpr.lexpr list * X86_extra.x86_extended_op Sopn.sopn) * Fexpr.rexpr list

val x86_tmp : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Ident.Ident.ident

val x86_liparams : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt,
    X86_instr_decl.x86_op,
    X86_extra.x86_extra_op)
    Arch_extra.extended_op
    Linearization.linearization_params

val x86_loparams : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  ((X86_decl.register,
     X86_decl.register_ext,
     X86_decl.xmm_register,
     X86_decl.rflag,
     X86_decl.condt,
     X86_instr_decl.x86_op,
     X86_extra.x86_extra_op)
     Arch_extra.extended_op,
    X86_lowering.lowering_options)
    Arch_params.lowering_params

val lflags : Expr.lval list

val is_mmx_protect : Wsize.wsize -> Expr.lval list -> bool

val x86_sh_lower : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.lval list ->
  Slh_ops.slh_op ->
  Expr.pexpr list ->
  ((Expr.lval list
    * (X86_decl.register,
        X86_decl.register_ext,
        X86_decl.xmm_register,
        X86_decl.rflag,
        X86_decl.condt,
        X86_instr_decl.x86_op,
        X86_extra.x86_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Expr.pexpr list)
    option

val x86_shparams : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt,
    X86_instr_decl.x86_op,
    X86_extra.x86_extra_op)
    Arch_extra.extended_op
    Slh_lowering.sh_params

val not_condt : X86_decl.condt -> X86_decl.condt

val or_condt : 
  Expr.instr_info ->
  Fexpr.fexpr ->
  X86_decl.condt ->
  X86_decl.condt ->
  X86_decl.condt Compiler_util.cexec

val and_condt : 
  Expr.instr_info ->
  Fexpr.fexpr ->
  X86_decl.condt ->
  X86_decl.condt ->
  (Compiler_util.pp_error_loc, X86_decl.condt) Utils0.result

val of_var_e_bool : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.instr_info ->
  Expr.var_i ->
  X86_decl.rflag Compiler_util.cexec

val assemble_cond_r : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.instr_info ->
  Fexpr.fexpr ->
  X86_decl.condt Compiler_util.cexec

val assemble_cond : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.instr_info ->
  Fexpr.fexpr ->
  X86_decl.condt Compiler_util.cexec

val is_valid_address : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_decl.reg_address ->
  bool

val x86_agparams : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt,
    X86_instr_decl.x86_op,
    X86_extra.x86_extra_op)
    Asm_gen.asm_gen_params

val x86_szparams : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt,
    X86_instr_decl.x86_op,
    X86_extra.x86_extra_op)
    Arch_extra.extended_op
    Stack_zeroization.stack_zeroization_params

val x86_is_move_op : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt,
    X86_instr_decl.x86_op,
    X86_extra.x86_extra_op)
    Arch_extra.extended_op
    Sopn.asm_op_t ->
  bool

val x86_params : 
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt)
    Arch_extra.arch_toIdent ->
  (X86_decl.register,
    X86_decl.register_ext,
    X86_decl.xmm_register,
    X86_decl.rflag,
    X86_decl.condt,
    X86_instr_decl.x86_op,
    X86_extra.x86_extra_op,
    X86_lowering.lowering_options)
    Arch_params.architecture_params