Riscv_params (p.jasmin.2025.06.2.doc.jasmin.jasmin.Jasmin.Riscv

val riscv_mov_ofs : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.lval ->
  Expr.assgn_tag ->
  Stack_alloc_params.mov_kind ->
  Expr.pexpr ->
  Expr.pexpr ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Expr.instr_r
    option

val riscv_immediate : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  BinNums.coq_Z ->
  Riscv_extra.riscv_extended_op Expr.instr_r

val riscv_swap : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.assgn_tag ->
  Expr.var_i ->
  Expr.var_i ->
  Expr.var_i ->
  Expr.var_i ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Expr.instr_r

val riscv_saparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Stack_alloc_params.stack_alloc_params

val riscv_allocate_stack_frame : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i option ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list
    * (Riscv_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arch_utils.empty,
        Riscv_decl.condt,
        Riscv_instr_decl.riscv_op,
        Riscv_extra.riscv_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Fexpr.rexpr list)
    list

val riscv_free_stack_frame : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i option ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list
    * (Riscv_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arch_utils.empty,
        Riscv_decl.condt,
        Riscv_instr_decl.riscv_op,
        Riscv_extra.riscv_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Fexpr.rexpr list)
    list

val riscv_set_up_sp_register : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  BinNums.coq_Z ->
  Wsize.wsize ->
  Expr.var_i ->
  Expr.var_i ->
  ((Fexpr.lexpr list
    * (Riscv_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arch_utils.empty,
        Riscv_decl.condt,
        Riscv_instr_decl.riscv_op,
        Riscv_extra.riscv_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Fexpr.rexpr list)
    list

val riscv_tmp : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Ident.Ident.ident

val riscv_tmp2 : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Ident.Ident.ident

val riscv_lmove : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  (Fexpr.lexpr list * Riscv_extra.riscv_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val riscv_check_ws : Eqtype.Equality.sort -> bool

val riscv_lstore : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  BinNums.coq_Z ->
  Expr.var_i ->
  (Fexpr.lexpr list * Riscv_extra.riscv_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val riscv_lload : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  BinNums.coq_Z ->
  (Fexpr.lexpr list * Riscv_extra.riscv_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val riscv_liparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Linearization.linearization_params

val riscv_loparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  ((Riscv_decl.register,
     Arch_utils.empty,
     Arch_utils.empty,
     Arch_utils.empty,
     Riscv_decl.condt,
     Riscv_instr_decl.riscv_op,
     Riscv_extra.riscv_extra_op)
     Arch_extra.extended_op,
    Riscv_lowering.lowering_options)
    Arch_params.lowering_params

val riscv_shparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Slh_lowering.sh_params

val condt_not : Riscv_decl.condt -> Riscv_decl.condt

val assemble_cond_arg : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.instr_info ->
  Fexpr.fexpr ->
  Riscv_decl.register option Compiler_util.cexec

val assemble_cond_app2 : Expr.sop2 -> (Riscv_decl.condition_kind * bool) option

val assemble_cond : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.instr_info ->
  Fexpr.fexpr ->
  Riscv_decl.condt Compiler_util.cexec

val is_valid_address : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.reg_address ->
  bool

val riscv_agparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Asm_gen.asm_gen_params

val riscv_szparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Stack_zeroization.stack_zeroization_params

val riscv_laparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_params.lower_addressing_params

val riscv_is_move_op : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Sopn.asm_op_t ->
  bool

val riscv_params : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op,
    Riscv_lowering.lowering_options)
    Arch_params.architecture_params