Source file riscv_arch_full.ml

open Arch_decl
open Riscv_decl

module type Riscv_input = sig
  val call_conv : (register, Arch_utils.empty, Arch_utils.empty, Arch_utils.empty, condt) calling_convention

end

module Riscv_core = struct
  type reg = register
  type regx = Arch_utils.empty
  type xreg = Arch_utils.empty
  type rflag =  Arch_utils.empty
  type cond = condt
  type asm_op = Riscv_instr_decl.riscv_op
  type extra_op = Riscv_extra.riscv_extra_op

  let atoI = X86_arch_full.atoI riscv_decl

  let asm_e =  Riscv_extra.riscv_extra atoI
  let aparams = Riscv_params.riscv_params atoI
  let known_implicits = []

  let alloc_stack_need_extra sz =
    not (Riscv_params_core.is_arith_small (Conv.cz_of_z sz))

  (* Division and remainder have data-dependent latency on typical
     implementations, and are explicitly excluded from the Zkt safe list of
     the RISC-V specification ("Data-Independent Execution Latency Subset");
     see the documentation in proofs/compiler/riscv_instr_decl.v.
     Every other instruction is assumed to be constant-time, as on the other
     architectures. *)
  let is_ct_asm_op (o : asm_op) =
    match o with
    | Riscv_instr_decl.DIV | DIVU | REM | REMU -> false
    | _ -> true

  (* All of the extra ops compile into CT instructions (no DIV/REM):
     SWAP into xor, add_large_imm into lui/addi/add. *)
  let is_ct_asm_extra (_o : extra_op) = true

end

module Riscv (Lowering_params : Riscv_input) : Arch_full.Core_arch
  with type reg = register
   and type regx = Arch_utils.empty
   and type xreg = Arch_utils.empty
   and type rflag = Arch_utils.empty
   and type cond = condt
   and type asm_op = Riscv_instr_decl.riscv_op
   and type extra_op = Riscv_extra.riscv_extra_op = struct
  include Riscv_core
  include Lowering_params

  let not_saved_stack = (Riscv_params.riscv_liparams atoI).lip_not_saved_stack

  let pp_asm = Pp_riscv.print_prog

  let callstyle = Arch_full.ByReg { call = Some RA; return = true }

  let sp_min_align = Wsize.U8

  let max_store_size = Wsize.U32

  let internal_call_conv = Riscv_decl.riscv_internal_call_conv
end