Source file sail2_instr_kinds.ml

(*Generated by Lem from sail2_instr_kinds.lem.*)
(*========================================================================*)
(*     Sail                                                               *)
(*                                                                        *)
(*  Copyright (c) 2013-2017                                               *)
(*    Kathyrn Gray                                                        *)
(*    Shaked Flur                                                         *)
(*    Stephen Kell                                                        *)
(*    Gabriel Kerneis                                                     *)
(*    Robert Norton-Wright                                                *)
(*    Christopher Pulte                                                   *)
(*    Peter Sewell                                                        *)
(*    Alasdair Armstrong                                                  *)
(*    Brian Campbell                                                      *)
(*    Thomas Bauereiss                                                    *)
(*    Anthony Fox                                                         *)
(*    Jon French                                                          *)
(*    Dominic Mulligan                                                    *)
(*    Stephen Kell                                                        *)
(*    Mark Wassell                                                        *)
(*                                                                        *)
(*  All rights reserved.                                                  *)
(*                                                                        *)
(*  This software was developed by the University of Cambridge Computer   *)
(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
(*                                                                        *)
(*  Redistribution and use in source and binary forms, with or without    *)
(*  modification, are permitted provided that the following conditions    *)
(*  are met:                                                              *)
(*  1. Redistributions of source code must retain the above copyright     *)
(*     notice, this list of conditions and the following disclaimer.      *)
(*  2. Redistributions in binary form must reproduce the above copyright  *)
(*     notice, this list of conditions and the following disclaimer in    *)
(*     the documentation and/or other materials provided with the         *)
(*     distribution.                                                      *)
(*                                                                        *)
(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
(*  SUCH DAMAGE.                                                          *)
(*========================================================================*)

open Lem_pervasives_extra


type 'a enumerationType_class= {
  toNat_method : 'a -> int
}


(*val enumeration_typeCompare : forall 'a. EnumerationType 'a => 'a -> 'a -> ordering*)


let instance_Basic_classes_Ord_var_dict dict_Sail2_instr_kinds_EnumerationType_a:'a ord_class= ({

  compare_method = compare;

  isLess_method = (fun  r1 r2-> Lem.orderingEqual(compare r1 r2) (-1));

  isLessEqual_method = (fun r1 r2-> not (Lem.orderingEqual (compare r1 r2) 1));

  isGreater_method = (fun  r1 r2-> Lem.orderingEqual(compare r1 r2) 1);

  isGreaterEqual_method = (fun r1 r2-> not (Lem.orderingEqual (compare r1 r2) (-1)))})


(* Data structures for building up instructions *)

(* careful: changes in the read/write/barrier kinds have to be
   reflected in deep_shallow_convert *)
type read_kind =
  (* common reads *)
  | Read_plain
  (* Power reads *)
  | Read_reserve
  (* AArch64 reads *)
  | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream
  (* RISC-V reads *)
  | Read_RISCV_acquire  | Read_RISCV_strong_acquire
  | Read_RISCV_reserved | Read_RISCV_reserved_acquire
  | Read_RISCV_reserved_strong_acquire
  (* x86 reads *)
  | Read_X86_locked (* the read part of a lock'd instruction (rmw) *)
  (* instruction fetch *)
  | Read_ifetch

let instance_Show_Show_Sail2_instr_kinds_read_kind_dict:(read_kind)show_class= ({

  show_method = ((function
    | Read_plain -> "Read_plain"
    | Read_reserve -> "Read_reserve"
    | Read_acquire -> "Read_acquire"
    | Read_exclusive -> "Read_exclusive"
    | Read_exclusive_acquire -> "Read_exclusive_acquire"
    | Read_stream -> "Read_stream"
    | Read_RISCV_acquire -> "Read_RISCV_acquire"
    | Read_RISCV_strong_acquire -> "Read_RISCV_strong_acquire"
    | Read_RISCV_reserved -> "Read_RISCV_reserved"
    | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire"
    | Read_RISCV_reserved_strong_acquire -> "Read_RISCV_reserved_strong_acquire"
    | Read_X86_locked -> "Read_X86_locked"
    | Read_ifetch -> "Read_ifetch"
  ))})

type write_kind =
  (* common writes *)
  | Write_plain
  (* Power writes *)
  | Write_conditional
  (* AArch64 writes *)
  | Write_release | Write_exclusive | Write_exclusive_release
  (* RISC-V *)
  | Write_RISCV_release     | Write_RISCV_strong_release
  | Write_RISCV_conditional | Write_RISCV_conditional_release
  | Write_RISCV_conditional_strong_release
  (* x86 writes *)
  | Write_X86_locked (* the write part of a lock'd instruction (rmw) *)

let instance_Show_Show_Sail2_instr_kinds_write_kind_dict:(write_kind)show_class= ({

  show_method = ((function
    | Write_plain -> "Write_plain"
    | Write_conditional -> "Write_conditional"
    | Write_release -> "Write_release"
    | Write_exclusive -> "Write_exclusive"
    | Write_exclusive_release -> "Write_exclusive_release"
    | Write_RISCV_release -> "Write_RISCV_release"
    | Write_RISCV_strong_release -> "Write_RISCV_strong_release"
    | Write_RISCV_conditional -> "Write_RISCV_conditional"
    | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release"
    | Write_RISCV_conditional_strong_release -> "Write_RISCV_conditional_strong_release"
    | Write_X86_locked -> "Write_X86_locked"
  ))})

type a64_barrier_domain =
  A64_FullShare
  | A64_InnerShare
  | A64_OuterShare
  | A64_NonShare

type a64_barrier_type =
  A64_barrier_all
  | A64_barrier_LD
  | A64_barrier_ST

type barrier_kind =
  (* Power barriers *)
  Barrier_Sync of unit | Barrier_LwSync of unit | Barrier_Eieio of unit | Barrier_Isync of unit
  (* AArch64 barriers *)
  | Barrier_DMB of (a64_barrier_domain * a64_barrier_type)
  | Barrier_DSB of (a64_barrier_domain * a64_barrier_type)
  | Barrier_ISB of unit
  | Barrier_TM_COMMIT of unit
  (* MIPS barriers *)
  | Barrier_MIPS_SYNC of unit
  (* RISC-V barriers *)
  | Barrier_RISCV_rw_rw of unit
  | Barrier_RISCV_r_rw of unit
  | Barrier_RISCV_r_r of unit
  | Barrier_RISCV_rw_w of unit
  | Barrier_RISCV_w_w of unit
  | Barrier_RISCV_w_rw of unit
  | Barrier_RISCV_rw_r of unit
  | Barrier_RISCV_r_w of unit
  | Barrier_RISCV_w_r of unit
  | Barrier_RISCV_tso of unit
  | Barrier_RISCV_i of unit
  (* X86 *)
  | Barrier_x86_MFENCE of unit

let string_a64_barrier_domain:a64_barrier_domain ->string=  ((function
  | A64_FullShare  -> "A64_FullShare"
  | A64_InnerShare -> "A64_InnerShare"
  | A64_OuterShare -> "A64_OuterShare"
  | A64_NonShare   -> "A64_NonShare"
))

let instance_Show_Show_Sail2_instr_kinds_a64_barrier_domain_dict:(a64_barrier_domain)show_class= ({

  show_method = string_a64_barrier_domain})

let string_a64_barrier_type:a64_barrier_type ->string=  ((function
  | A64_barrier_all -> "A64_barrier_all"
  | A64_barrier_LD  -> "A64_barrier_LD"
  | A64_barrier_ST  -> "A64_barrier_ST"
))

let instance_Show_Show_Sail2_instr_kinds_a64_barrier_type_dict:(a64_barrier_type)show_class= ({

  show_method = string_a64_barrier_type})

let instance_Show_Show_Sail2_instr_kinds_barrier_kind_dict:(barrier_kind)show_class= ({

  show_method = ((function
    | Barrier_Sync () -> "Barrier_Sync"
    | Barrier_LwSync () -> "Barrier_LwSync"
    | Barrier_Eieio () -> "Barrier_Eieio"
    | Barrier_Isync () -> "Barrier_Isync"
    | Barrier_DMB (dom,typ) -> "Barrier_DMB (" ^ ((string_a64_barrier_domain dom) ^ (", " ^ ((string_a64_barrier_type typ) ^ ")")))
    | Barrier_DSB (dom,typ) -> "Barrier_DSB (" ^ ((string_a64_barrier_domain dom) ^ (", " ^ ((string_a64_barrier_type typ) ^ ")")))
    | Barrier_ISB () -> "Barrier_ISB"
    | Barrier_TM_COMMIT () -> "Barrier_TM_COMMIT"
    | Barrier_MIPS_SYNC () -> "Barrier_MIPS_SYNC"
    | Barrier_RISCV_rw_rw () -> "Barrier_RISCV_rw_rw"
    | Barrier_RISCV_r_rw ()  -> "Barrier_RISCV_r_rw"
    | Barrier_RISCV_r_r ()   -> "Barrier_RISCV_r_r"
    | Barrier_RISCV_rw_w ()  -> "Barrier_RISCV_rw_w"
    | Barrier_RISCV_w_w ()   -> "Barrier_RISCV_w_w"
    | Barrier_RISCV_w_rw ()  -> "Barrier_RISCV_w_rw"
    | Barrier_RISCV_rw_r ()  -> "Barrier_RISCV_rw_r"
    | Barrier_RISCV_r_w ()   -> "Barrier_RISCV_r_w"
    | Barrier_RISCV_w_r ()   -> "Barrier_RISCV_w_r"
    | Barrier_RISCV_tso ()   -> "Barrier_RISCV_tso"
    | Barrier_RISCV_i ()     -> "Barrier_RISCV_i"
    | Barrier_x86_MFENCE ()  -> "Barrier_x86_MFENCE"
  ))})

type trans_kind =
  (* AArch64 *)
  | Transaction_start | Transaction_commit | Transaction_abort

let instance_Show_Show_Sail2_instr_kinds_trans_kind_dict:(trans_kind)show_class= ({

  show_method = ((function
  | Transaction_start  -> "Transaction_start"
  | Transaction_commit -> "Transaction_commit"
  | Transaction_abort  -> "Transaction_abort"
  ))})

(* cache maintenance instructions *)
type 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

let instance_Show_Show_Sail2_instr_kinds_cache_op_kind_dict:(cache_op_kind)show_class= ({

  show_method = ((function
  | Cache_op_D_IVAC    -> "Cache_op_D_IVAC"
  | Cache_op_D_ISW     -> "Cache_op_D_ISW"
  | Cache_op_D_CSW     -> "Cache_op_D_CSW"
  | Cache_op_D_CISW    -> "Cache_op_D_CISW"
  | Cache_op_D_ZVA     -> "Cache_op_D_ZVA"
  | Cache_op_D_CVAC    -> "Cache_op_D_CVAC"
  | Cache_op_D_CVAU    -> "Cache_op_D_CVAU"
  | Cache_op_D_CIVAC   -> "Cache_op_D_CIVAC"
  | Cache_op_I_IALLUIS -> "Cache_op_I_IALLUIS"
  | Cache_op_I_IALLU   -> "Cache_op_I_IALLU"
  | Cache_op_I_IVAU    -> "Cache_op_I_IVAU"
  ))})

type instruction_kind =
  | IK_barrier   of barrier_kind
  | IK_mem_read  of read_kind
  | IK_mem_write of write_kind
  | IK_mem_rmw   of (read_kind * write_kind)
  | IK_branch    of unit(* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address),
  indirect/computed-branch (single nia of kind NIA_indirect_address)
  and branch/jump (single nia of kind NIA_concrete_address) *)
  | IK_trans     of trans_kind
  | IK_simple    of unit
  | IK_cache_op  of cache_op_kind


let instance_Show_Show_Sail2_instr_kinds_instruction_kind_dict:(instruction_kind)show_class= ({

  show_method = ((function
    | IK_barrier barrier_kind1 -> "IK_barrier " ^ (((function
    | Barrier_Sync () -> "Barrier_Sync"
    | Barrier_LwSync () -> "Barrier_LwSync"
    | Barrier_Eieio () -> "Barrier_Eieio"
    | Barrier_Isync () -> "Barrier_Isync"
    | Barrier_DMB (dom,typ) -> "Barrier_DMB (" ^ ((string_a64_barrier_domain dom) ^ (", " ^ ((string_a64_barrier_type typ) ^ ")")))
    | Barrier_DSB (dom,typ) -> "Barrier_DSB (" ^ ((string_a64_barrier_domain dom) ^ (", " ^ ((string_a64_barrier_type typ) ^ ")")))
    | Barrier_ISB () -> "Barrier_ISB"
    | Barrier_TM_COMMIT () -> "Barrier_TM_COMMIT"
    | Barrier_MIPS_SYNC () -> "Barrier_MIPS_SYNC"
    | Barrier_RISCV_rw_rw () -> "Barrier_RISCV_rw_rw"
    | Barrier_RISCV_r_rw ()  -> "Barrier_RISCV_r_rw"
    | Barrier_RISCV_r_r ()   -> "Barrier_RISCV_r_r"
    | Barrier_RISCV_rw_w ()  -> "Barrier_RISCV_rw_w"
    | Barrier_RISCV_w_w ()   -> "Barrier_RISCV_w_w"
    | Barrier_RISCV_w_rw ()  -> "Barrier_RISCV_w_rw"
    | Barrier_RISCV_rw_r ()  -> "Barrier_RISCV_rw_r"
    | Barrier_RISCV_r_w ()   -> "Barrier_RISCV_r_w"
    | Barrier_RISCV_w_r ()   -> "Barrier_RISCV_w_r"
    | Barrier_RISCV_tso ()   -> "Barrier_RISCV_tso"
    | Barrier_RISCV_i ()     -> "Barrier_RISCV_i"
    | Barrier_x86_MFENCE ()  -> "Barrier_x86_MFENCE"
  ) barrier_kind1))
    | IK_mem_read read_kind1   -> "IK_mem_read " ^ (((function
    | Read_plain -> "Read_plain"
    | Read_reserve -> "Read_reserve"
    | Read_acquire -> "Read_acquire"
    | Read_exclusive -> "Read_exclusive"
    | Read_exclusive_acquire -> "Read_exclusive_acquire"
    | Read_stream -> "Read_stream"
    | Read_RISCV_acquire -> "Read_RISCV_acquire"
    | Read_RISCV_strong_acquire -> "Read_RISCV_strong_acquire"
    | Read_RISCV_reserved -> "Read_RISCV_reserved"
    | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire"
    | Read_RISCV_reserved_strong_acquire -> "Read_RISCV_reserved_strong_acquire"
    | Read_X86_locked -> "Read_X86_locked"
    | Read_ifetch -> "Read_ifetch"
  ) read_kind1))
    | IK_mem_write write_kind1 -> "IK_mem_write " ^ (((function
    | Write_plain -> "Write_plain"
    | Write_conditional -> "Write_conditional"
    | Write_release -> "Write_release"
    | Write_exclusive -> "Write_exclusive"
    | Write_exclusive_release -> "Write_exclusive_release"
    | Write_RISCV_release -> "Write_RISCV_release"
    | Write_RISCV_strong_release -> "Write_RISCV_strong_release"
    | Write_RISCV_conditional -> "Write_RISCV_conditional"
    | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release"
    | Write_RISCV_conditional_strong_release -> "Write_RISCV_conditional_strong_release"
    | Write_X86_locked -> "Write_X86_locked"
  ) write_kind1))
    | IK_mem_rmw (r, w)       -> "IK_mem_rmw " ^ ((((function
    | Read_plain -> "Read_plain"
    | Read_reserve -> "Read_reserve"
    | Read_acquire -> "Read_acquire"
    | Read_exclusive -> "Read_exclusive"
    | Read_exclusive_acquire -> "Read_exclusive_acquire"
    | Read_stream -> "Read_stream"
    | Read_RISCV_acquire -> "Read_RISCV_acquire"
    | Read_RISCV_strong_acquire -> "Read_RISCV_strong_acquire"
    | Read_RISCV_reserved -> "Read_RISCV_reserved"
    | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire"
    | Read_RISCV_reserved_strong_acquire -> "Read_RISCV_reserved_strong_acquire"
    | Read_X86_locked -> "Read_X86_locked"
    | Read_ifetch -> "Read_ifetch"
  ) r)) ^ (" " ^ (((function
    | Write_plain -> "Write_plain"
    | Write_conditional -> "Write_conditional"
    | Write_release -> "Write_release"
    | Write_exclusive -> "Write_exclusive"
    | Write_exclusive_release -> "Write_exclusive_release"
    | Write_RISCV_release -> "Write_RISCV_release"
    | Write_RISCV_strong_release -> "Write_RISCV_strong_release"
    | Write_RISCV_conditional -> "Write_RISCV_conditional"
    | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release"
    | Write_RISCV_conditional_strong_release -> "Write_RISCV_conditional_strong_release"
    | Write_X86_locked -> "Write_X86_locked"
  ) w))))
    | IK_branch ()            -> "IK_branch"
    | IK_trans trans_kind1     -> "IK_trans " ^ (((function
  | Transaction_start  -> "Transaction_start"
  | Transaction_commit -> "Transaction_commit"
  | Transaction_abort  -> "Transaction_abort"
  ) trans_kind1))
    | IK_simple ()            -> "IK_simple"
    | IK_cache_op cache_kind  -> "IK_cache_op " ^ (((function
  | Cache_op_D_IVAC    -> "Cache_op_D_IVAC"
  | Cache_op_D_ISW     -> "Cache_op_D_ISW"
  | Cache_op_D_CSW     -> "Cache_op_D_CSW"
  | Cache_op_D_CISW    -> "Cache_op_D_CISW"
  | Cache_op_D_ZVA     -> "Cache_op_D_ZVA"
  | Cache_op_D_CVAC    -> "Cache_op_D_CVAC"
  | Cache_op_D_CVAU    -> "Cache_op_D_CVAU"
  | Cache_op_D_CIVAC   -> "Cache_op_D_CIVAC"
  | Cache_op_I_IALLUIS -> "Cache_op_I_IALLUIS"
  | Cache_op_I_IALLU   -> "Cache_op_I_IALLU"
  | Cache_op_I_IVAU    -> "Cache_op_I_IVAU"
  ) cache_kind))
  ))})


let read_is_exclusive:read_kind ->bool=  ((function
  | Read_plain -> false
  | Read_reserve -> true
  | Read_acquire -> false
  | Read_exclusive -> true
  | Read_exclusive_acquire -> true
  | Read_stream -> false
  | Read_RISCV_acquire -> false
  | Read_RISCV_strong_acquire -> false
  | Read_RISCV_reserved -> true
  | Read_RISCV_reserved_acquire -> true
  | Read_RISCV_reserved_strong_acquire -> true
  | Read_X86_locked -> true
  | Read_ifetch -> false
))



let instance_Sail2_instr_kinds_EnumerationType_Sail2_instr_kinds_read_kind_dict:(read_kind)enumerationType_class= ({

  toNat_method = ((function
    | Read_plain -> 0
    | Read_reserve -> 1
    | Read_acquire -> 2
    | Read_exclusive -> 3
    | Read_exclusive_acquire -> 4
    | Read_stream -> 5
    | Read_RISCV_acquire -> 6
    | Read_RISCV_strong_acquire -> 7
    | Read_RISCV_reserved -> 8
    | Read_RISCV_reserved_acquire -> 9
    | Read_RISCV_reserved_strong_acquire -> 10
    | Read_X86_locked -> 11
    | Read_ifetch -> 12
  ))})

let instance_Sail2_instr_kinds_EnumerationType_Sail2_instr_kinds_write_kind_dict:(write_kind)enumerationType_class= ({

  toNat_method = ((function
    | Write_plain -> 0
    | Write_conditional -> 1
    | Write_release -> 2
    | Write_exclusive -> 3
    | Write_exclusive_release -> 4
    | Write_RISCV_release -> 5
    | Write_RISCV_strong_release -> 6
    | Write_RISCV_conditional -> 7
    | Write_RISCV_conditional_release -> 8
    | Write_RISCV_conditional_strong_release -> 9
    | Write_X86_locked -> 10
  ))})

let instance_Sail2_instr_kinds_EnumerationType_Sail2_instr_kinds_a64_barrier_domain_dict:(a64_barrier_domain)enumerationType_class= ({

  toNat_method = ((function
    | A64_FullShare  -> 0
    | A64_InnerShare -> 1
    | A64_OuterShare -> 2
    | A64_NonShare   -> 3
  ))})

let instance_Sail2_instr_kinds_EnumerationType_Sail2_instr_kinds_a64_barrier_type_dict:(a64_barrier_type)enumerationType_class= ({

  toNat_method = ((function
    | A64_barrier_all -> 0
    | A64_barrier_LD  -> 1
    | A64_barrier_ST  -> 2
  ))})

let instance_Sail2_instr_kinds_EnumerationType_Sail2_instr_kinds_barrier_kind_dict:(barrier_kind)enumerationType_class= ({

  toNat_method = ((function
    | Barrier_Sync () -> 0
    | Barrier_LwSync () -> 1
    | Barrier_Eieio () -> 2
    | Barrier_Isync () -> 3
    | Barrier_DMB (dom,typ) -> (4  + (((function
    | A64_FullShare  -> 0
    | A64_InnerShare -> 1
    | A64_OuterShare -> 2
    | A64_NonShare   -> 3
  ) dom))) + (4 * (((function
    | A64_barrier_all -> 0
    | A64_barrier_LD  -> 1
    | A64_barrier_ST  -> 2
  ) typ))) (* 4-15 *)
    | Barrier_DSB (dom,typ) -> (16 + (((function
    | A64_FullShare  -> 0
    | A64_InnerShare -> 1
    | A64_OuterShare -> 2
    | A64_NonShare   -> 3
  ) dom))) + (4 * (((function
    | A64_barrier_all -> 0
    | A64_barrier_LD  -> 1
    | A64_barrier_ST  -> 2
  ) typ))) (* 16-27 *)
    | Barrier_ISB () -> 28
    | Barrier_TM_COMMIT () -> 29
    | Barrier_MIPS_SYNC () -> 30
    | Barrier_RISCV_rw_rw () -> 31
    | Barrier_RISCV_r_rw () -> 32
    | Barrier_RISCV_r_r () -> 33
    | Barrier_RISCV_rw_w () -> 34
    | Barrier_RISCV_w_w () -> 35
    | Barrier_RISCV_w_rw () -> 36
    | Barrier_RISCV_rw_r () -> 37
    | Barrier_RISCV_r_w () -> 38
    | Barrier_RISCV_w_r () -> 39
    | Barrier_RISCV_tso () -> 40
    | Barrier_RISCV_i () -> 41
    | Barrier_x86_MFENCE () -> 42
  ))})