Module `Jasmin.Riscv_instr_decl`

type __ = Obj.t

module E : sig ... end

val pp_name : 
  string ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.asm_arg
    list ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.pp_asm_op

val coq_RTypeInstruction : 
  Wsize.wsize ->
  Sem_type.sem_tuple Sem_type.sem_prod ->
  string ->
  string ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val coq_ITypeInstruction : 
  Arch_decl.caimm_checker_s ->
  Wsize.wsize ->
  Sem_type.sem_tuple Sem_type.sem_prod ->
  string ->
  string ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val coq_ITypeInstruction_12s : 
  Wsize.wsize ->
  Sem_type.sem_tuple Sem_type.sem_prod ->
  string ->
  string ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val coq_ITypeInstruction_5u : 
  Wsize.wsize ->
  Sem_type.sem_tuple Sem_type.sem_prod ->
  string ->
  string ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

type riscv_op =

| ADD
| ADDI
| SUB
| SLT
| SLTI
| SLTU
| SLTIU
| AND
| ANDI
| OR
| ORI
| XOR
| XORI
| SLL
| SLLI
| SRL
| SRLI
| SRA
| SRAI
| MV
| LA
| LI
| NOT
| NEG
| LOAD of Wsize.signedness * Wsize.wsize
| STORE of Wsize.wsize
| MUL
| MULH
| MULHU
| MULHSU
| DIV
| DIVU
| REM
| REMU

val riscv_op_rect : 
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  (Wsize.signedness -> Wsize.wsize -> 'a1) ->
  (Wsize.wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  riscv_op ->
  'a1

val riscv_op_rec : 
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  (Wsize.signedness -> Wsize.wsize -> 'a1) ->
  (Wsize.wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  riscv_op ->
  'a1

type is_riscv_op =

| Coq_is_ADD
| Coq_is_ADDI
| Coq_is_SUB
| Coq_is_SLT
| Coq_is_SLTI
| Coq_is_SLTU
| Coq_is_SLTIU
| Coq_is_AND
| Coq_is_ANDI
| Coq_is_OR
| Coq_is_ORI
| Coq_is_XOR
| Coq_is_XORI
| Coq_is_SLL
| Coq_is_SLLI
| Coq_is_SRL
| Coq_is_SRLI
| Coq_is_SRA
| Coq_is_SRAI
| Coq_is_MV
| Coq_is_LA
| Coq_is_LI
| Coq_is_NOT
| Coq_is_NEG
| Coq_is_LOAD of Wsize.signedness * Wsize.is_signedness * Wsize.wsize * Wsize.is_wsize
| Coq_is_STORE of Wsize.wsize * Wsize.is_wsize
| Coq_is_MUL
| Coq_is_MULH
| Coq_is_MULHU
| Coq_is_MULHSU
| Coq_is_DIV
| Coq_is_DIVU
| Coq_is_REM
| Coq_is_REMU

val is_riscv_op_rect : 
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  (Wsize.signedness ->
    Wsize.is_signedness ->
    Wsize.wsize ->
    Wsize.is_wsize ->
    'a1) ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  riscv_op ->
  is_riscv_op ->
  'a1

val is_riscv_op_rec : 
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  (Wsize.signedness ->
    Wsize.is_signedness ->
    Wsize.wsize ->
    Wsize.is_wsize ->
    'a1) ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  riscv_op ->
  is_riscv_op ->
  'a1

val riscv_op_tag : riscv_op -> BinNums.positive

val is_riscv_op_inhab : riscv_op -> is_riscv_op

val is_riscv_op_functor : riscv_op -> is_riscv_op -> is_riscv_op

type box_riscv_op_ADD =

| Box_riscv_op_ADD

type box_riscv_op_LOAD = {

coq_Box_riscv_op_LOAD_0 : Wsize.signedness;
coq_Box_riscv_op_LOAD_1 : Wsize.wsize;

}

val coq_Box_riscv_op_LOAD_0 : box_riscv_op_LOAD -> Wsize.signedness

val coq_Box_riscv_op_LOAD_1 : box_riscv_op_LOAD -> Wsize.wsize

type box_riscv_op_STORE = Wsize.wsize

val coq_Box_riscv_op_STORE_0 : box_riscv_op_STORE -> Wsize.wsize

type riscv_op_fields_t = __

val riscv_op_fields : riscv_op -> riscv_op_fields_t

val riscv_op_construct : 
  BinNums.positive ->
  riscv_op_fields_t ->
  riscv_op option

val riscv_op_induction : 
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  (Wsize.signedness ->
    Wsize.is_signedness ->
    Wsize.wsize ->
    Wsize.is_wsize ->
    'a1) ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  'a1 ->
  riscv_op ->
  is_riscv_op ->
  'a1

val riscv_op_eqb_fields : 
  (riscv_op -> riscv_op -> bool) ->
  BinNums.positive ->
  riscv_op_fields_t ->
  riscv_op_fields_t ->
  bool

val riscv_op_eqb : riscv_op -> riscv_op -> bool

val riscv_op_eqb_OK : riscv_op -> riscv_op -> Bool.reflect

val riscv_op_eqb_OK_sumbool : riscv_op -> riscv_op -> bool

val eqTC_riscv_op : riscv_op Utils0.eqTypeC

val riscv_op_eqType : Eqtype.Equality.coq_type

val riscv_add_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_ADD_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_ADD : string * riscv_op Sopn.prim_constructor

val riscv_ADDI_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_ADDI : string * riscv_op Sopn.prim_constructor

val riscv_sub_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_SUB_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_SUB : string * riscv_op Sopn.prim_constructor

val riscv_slt_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_SLT_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_SLT : string * riscv_op Sopn.prim_constructor

val riscv_SLTI_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_SLTI : string * riscv_op Sopn.prim_constructor

val riscv_sltu_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_SLTU_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_SLTU : string * riscv_op Sopn.prim_constructor

val riscv_SLTIU_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_SLTIU : string * riscv_op Sopn.prim_constructor

val riscv_and_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_AND_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_AND : string * riscv_op Sopn.prim_constructor

val riscv_ANDI_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_ANDI : string * riscv_op Sopn.prim_constructor

val riscv_or_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_OR_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_OR : string * riscv_op Sopn.prim_constructor

val riscv_ORI_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_ORI : string * riscv_op Sopn.prim_constructor

val riscv_xor_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_XOR_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_XOR : string * riscv_op Sopn.prim_constructor

val riscv_XORI_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_XORI : string * riscv_op Sopn.prim_constructor

val riscv_sll_semi : 
  Sem_type.sem_tuple ->
  Ssralg.GRing.ComRing.sort ->
  Sem_type.sem_tuple

val riscv_SLL_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_SLL : string * riscv_op Sopn.prim_constructor

val riscv_SLLI_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_SLLI : string * riscv_op Sopn.prim_constructor

val riscv_srl_semi : 
  Sem_type.sem_tuple ->
  Ssralg.GRing.ComRing.sort ->
  Sem_type.sem_tuple

val riscv_SRL_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_SRL : string * riscv_op Sopn.prim_constructor

val riscv_SRLI_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_SRLI : string * riscv_op Sopn.prim_constructor

val riscv_sra_semi : 
  Sem_type.sem_tuple ->
  Ssralg.GRing.ComRing.sort ->
  Sem_type.sem_tuple

val riscv_SRA_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_SRA : string * riscv_op Sopn.prim_constructor

val riscv_SRAI_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_SRAI : string * riscv_op Sopn.prim_constructor

val riscv_MV_semi : Sem_type.sem_tuple -> Sem_type.sem_tuple

val riscv_MV_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_MV : string * riscv_op Sopn.prim_constructor

val riscv_LA_semi : Sem_type.sem_tuple -> Sem_type.sem_tuple

val riscv_LA_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_LA : string * riscv_op Sopn.prim_constructor

val riscv_LI_semi : Sem_type.sem_tuple -> Sem_type.sem_tuple

val riscv_LI_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_LI : string * riscv_op Sopn.prim_constructor

val riscv_NOT_semi : Sem_type.sem_tuple -> Sem_type.sem_tuple

val riscv_NOT_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_NOT : string * riscv_op Sopn.prim_constructor

val riscv_NEG_semi : Sem_type.sem_tuple -> Sem_type.sem_tuple

val riscv_NEG_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_NEG : string * riscv_op Sopn.prim_constructor

val string_of_sign : Wsize.signedness -> string

val string_of_size : Wsize.wsize -> string

val pp_sign_sz : string -> Wsize.signedness -> Wsize.wsize -> unit -> string

val riscv_extend_semi : 
  Wsize.signedness ->
  Wsize.wsize ->
  Wsize.wsize ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort

val riscv_LOAD_instr : 
  Wsize.signedness ->
  Wsize.wsize ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val primS : 
  (Wsize.signedness -> Wsize.wsize -> riscv_op) ->
  riscv_op Sopn.prim_constructor

val prim_LOAD : string * riscv_op Sopn.prim_constructor

val riscv_STORE_instr : 
  Wsize.wsize ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_STORE : string * riscv_op Sopn.prim_constructor

val riscv_mul_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_MUL_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_MUL : string * riscv_op Sopn.prim_constructor

val riscv_mulh_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_MULH_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_MULH : string * riscv_op Sopn.prim_constructor

val riscv_mulhu_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_MULHU_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_MULHU : string * riscv_op Sopn.prim_constructor

val riscv_mulhsu_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_MULHSU_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_MULHSU : string * riscv_op Sopn.prim_constructor

val riscv_div_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_DIV_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_DIV : string * riscv_op Sopn.prim_constructor

val riscv_divu_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_DIVU_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_DIVU : string * riscv_op Sopn.prim_constructor

val riscv_rem_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_REM_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_REM : string * riscv_op Sopn.prim_constructor

val riscv_remu_semi : 
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple ->
  Sem_type.sem_tuple

val riscv_REMU_instr : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val prim_REMU : string * riscv_op Sopn.prim_constructor

val riscv_instr_desc : 
  riscv_op ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.instr_desc_t

val riscv_prim_string : (string * riscv_op Sopn.prim_constructor) list

val riscv_op_decl : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    riscv_op)
    Arch_decl.asm_op_decl

type riscv_prog =
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    riscv_op)
    Arch_decl.asm_prog

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/jasmin.jasmin/Jasmin/Riscv_instr_decl/index.html

Module `Jasmin.Riscv_instr_decl`

package jasmin

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/jasmin.jasmin/Jasmin/Riscv_instr_decl/index.html

Module Jasmin.Riscv_instr_decl

dune-project
Dependency

Module `Jasmin.Riscv_instr_decl`