$ifndef _REGFP
$define _REGFP

/* iR : input registers,
 * oR : output registers,
 * aR : registers feeding into the memory address */

/* branch instructions currently are not writing to NIA */

union regfp = {
   RFull : string,
   RSlice : (string,nat,nat),
   RSliceBit : (string,nat),
   RField : (string,string)
}

type regfps = list(regfp)

union niafp = {
  NIAFP_successor : unit,
  NIAFP_concrete_address : bits(64),
  NIAFP_indirect_address : unit
}

type niafps = list(niafp)

/* only for MIPS */
union diafp = {
  DIAFP_none : unit,
  DIAFP_concrete : bits(64),
  DIAFP_reg : regfp
}

$ifdef ARM_SPEC
enum read_kind = {
  Read_plain,
  Read_reserve,
  Read_acquire,
  Read_exclusive,
  Read_exclusive_acquire,
  Read_stream,
  Read_ifetch,
  Read_RISCV_acquire,
  Read_RISCV_strong_acquire,
  Read_RISCV_reserved,
  Read_RISCV_reserved_acquire,
  Read_RISCV_reserved_strong_acquire,
  Read_X86_locked
}
$else
enum read_kind = {
  Read_plain,
  Read_reserve,
  Read_acquire,
  Read_exclusive,
  Read_exclusive_acquire,
  Read_stream,
  Read_RISCV_acquire,
  Read_RISCV_strong_acquire,
  Read_RISCV_reserved,
  Read_RISCV_reserved_acquire,
  Read_RISCV_reserved_strong_acquire,
  Read_X86_locked
}
$endif

enum write_kind = {
  Write_plain,
  Write_conditional,
  Write_release,
  Write_exclusive,
  Write_exclusive_release,
  Write_RISCV_release,
  Write_RISCV_strong_release,
  Write_RISCV_conditional,
  Write_RISCV_conditional_release,
  Write_RISCV_conditional_strong_release,
  Write_X86_locked
}

$ifdef ARM_SPEC
enum barrier_kind = {
  Barrier_DMB_SY,
  Barrier_DMB_ST,
  Barrier_DMB_LD,
  Barrier_DMB_ISH,
  Barrier_DMB_ISHST,
  Barrier_DMB_ISHLD,
  Barrier_DMB_NSH,
  Barrier_DMB_NSHST,
  Barrier_DMB_NSHLD,
  Barrier_DMB_OSH,
  Barrier_DMB_OSHST,
  Barrier_DMB_OSHLD,
  Barrier_DSB_SY,
  Barrier_DSB_ST,
  Barrier_DSB_LD,
  Barrier_DSB_ISH,
  Barrier_DSB_ISHST,
  Barrier_DSB_ISHLD,
  Barrier_DSB_NSH,
  Barrier_DSB_NSHST,
  Barrier_DSB_NSHLD,
  Barrier_DSB_OSH,
  Barrier_DSB_OSHST,
  Barrier_DSB_OSHLD,
  Barrier_ISB
}
$else
enum a64_barrier_domain = {
  A64_FullShare,
  A64_InnerShare,
  A64_OuterShare,
  A64_NonShare
}

enum a64_barrier_type = {
  A64_barrier_all,
  A64_barrier_LD,
  A64_barrier_ST
}

union barrier_kind = {
  Barrier_Sync : unit,
  Barrier_LwSync : unit,
  Barrier_Eieio : unit,
  Barrier_Isync : unit,
  Barrier_DMB : (a64_barrier_domain, a64_barrier_type),
  Barrier_DSB : (a64_barrier_domain, a64_barrier_type),
  Barrier_ISB : unit,
  Barrier_MIPS_SYNC : unit,
  Barrier_RISCV_rw_rw : unit,
  Barrier_RISCV_r_rw : unit,
  Barrier_RISCV_r_r : unit,
  Barrier_RISCV_rw_w : unit,
  Barrier_RISCV_w_w : unit,
  Barrier_RISCV_w_rw : unit,
  Barrier_RISCV_rw_r : unit,
  Barrier_RISCV_r_w : unit,
  Barrier_RISCV_w_r : unit,
  Barrier_RISCV_tso : unit,
  Barrier_RISCV_i : unit,
  Barrier_x86_MFENCE : unit
}
$endif

enum trans_kind = {
  Transaction_start,
  Transaction_commit,
  Transaction_abort
}

/* cache maintenance instructions */
enum cache_op_kind = {
  /* AArch64 DC */
  Cache_op_D_IVAC, Cache_op_D_ISW,  Cache_op_D_CSW,  Cache_op_D_CISW,
  Cache_op_D_ZVA,  Cache_op_D_CVAC, Cache_op_D_CVAU, Cache_op_D_CIVAC,
  /* AArch64 IC */
  Cache_op_I_IALLUIS, Cache_op_I_IALLU, Cache_op_I_IVAU
}


union instruction_kind = {
  IK_barrier : barrier_kind,
  IK_mem_read : read_kind,
  IK_mem_write : write_kind,
  IK_mem_rmw : (read_kind, write_kind),
  IK_branch : unit,
  IK_trans : trans_kind,
  IK_simple : unit,
  IK_cache_op : cache_op_kind
}

val __read_mem
  = { ocaml: "Platform.read_mem", c: "platform_read_mem", _: "read_mem" }
  : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}.
  (read_kind, int('addrsize), bits('addrsize), int('n)) -> bits(8 * 'n) effect {rmem}
val __read_memt
  = { ocaml: "Platform.read_memt", c: "platform_read_memt", _: "read_memt" }
  : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}.
  (read_kind, bits('addrsize), int('n)) -> (bits(8 * 'n), bit) effect {rmemt}
val __write_mem_ea
  = { ocaml: "Platform.write_mem_ea", c: "platform_write_mem_ea", _: "write_mem_ea" }
  : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}.
  (write_kind, int('addrsize), bits('addrsize), int('n)) -> unit effect {eamem}
val __write_mem
  = { ocaml: "Platform.write_mem", c: "platform_write_mem", _: "write_mem" }
  : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}.
  (write_kind, int('addrsize), bits('addrsize), int('n), bits(8 * 'n)) -> bool effect {wmv}
val __write_memt
  = { ocaml: "Platform.write_memt", c: "platform_write_memt", _: "write_memt" }
  : forall 'n (constant 'addrsize : Int), 'n > 0 & 'addrsize in {32, 64}.
  (write_kind, bits('addrsize), int('n), bits(8 * 'n), bit) -> bool effect {wmvt}
val __write_tag
  = { ocaml: "Platform.write_tag", c: "platform_write_tag", _: "write_tag" }
  : forall (constant 'addrsize : Int), 'addrsize in {32, 64}.
  (write_kind, bits('addrsize), bit) -> bool effect {wmvt}
val __excl_res
  = { ocaml: "Platform.excl_res", c: "platform_excl_res", _: "excl_result" }
  : unit -> bool effect {exmem}
val __barrier
  = { ocaml: "Platform.barrier", c: "platform_barrier", _: "barrier" }
  : barrier_kind -> unit effect {barr}

val __branch_announce
  = { ocaml: "Platform.branch_announce", c: "platform_branch_announce", _ : "branch_announce" }
  : forall (constant 'addrsize : Int), 'addrsize in {32, 64}.
  (int('addrsize), bits('addrsize)) -> unit

val __cache_maintenance
  = { ocaml: "Platform.cache_maintenance", c: "platform_cache_maintenance", _ : "cache_maintenance" }
  : forall (constant 'addrsize : Int), 'addrsize in {32, 64}.
  (cache_op_kind, int('addrsize), bits('addrsize)) -> unit

val __instr_announce
  = { ocaml: "Platform.instr_announce", c: "platform_instr_announce", _: "instr_announce" }
  : forall 'n, 'n > 0.
  bits('n) -> unit

/*
val __write : forall 'n, 'n > 0. (write_kind, bits(64), int('n), bits(8 * 'n)) -> bool effect {eamem,wmv}
function __write (wk, addr, len, value) = {
  __write_mem_ea(wk, addr, len);
  __write_mem(wk, addr, len, value)
}
*/

$endif