rename all lem support files to sail2_foo to avoid conflict with sail1 in rmem

1 files changed, 0 insertions, 294 deletions

diff --git a/src/lem_interp/sail_instr_kinds.lem b/src/lem_interp/sail_instr_kinds.lem
deleted file mode 100644
index d8a2c0c0..00000000
--- a/src/lem_interp/sail_instr_kinds.lem
+++ /dev/null
@@ -1,294 +0,0 @@
-(*========================================================================*)
-(*     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 import Pervasives_extra
-
-
-class ( EnumerationType 'a )
-  val toNat : 'a -> nat
-end
-
-
-val enumeration_typeCompare : forall 'a. EnumerationType 'a => 'a -> 'a -> ordering
-let ~{ocaml} enumeration_typeCompare e1 e2 =
-  compare (toNat e1) (toNat e2)
-let inline {ocaml} enumeration_typeCompare = defaultCompare
-
-
-default_instance forall 'a. EnumerationType 'a => (Ord 'a)
-  let compare = enumeration_typeCompare
-  let (<)  r1 r2 = (enumeration_typeCompare r1 r2) = LT
-  let (<=) r1 r2 = (enumeration_typeCompare r1 r2) <> GT
-  let (>)  r1 r2 = (enumeration_typeCompare r1 r2) = GT
-  let (>=) r1 r2 = (enumeration_typeCompare r1 r2) <> LT
-end
-
-
-(* 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) *)
-
-instance (Show read_kind)
-  let show = 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"
-  end
-end
-
-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) *)
-
-instance (Show write_kind)
-  let show = 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"
-  end
-end
-
-type barrier_kind =
-  (* Power barriers *)
-  Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync
-  (* AArch64 barriers *)
-  | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB
-  | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB
-  | Barrier_TM_COMMIT
-  (* MIPS barriers *)
-  | Barrier_MIPS_SYNC
-  (* RISC-V barriers *)
-  | Barrier_RISCV_rw_rw
-  | Barrier_RISCV_r_rw
-  | Barrier_RISCV_r_r
-  | Barrier_RISCV_rw_w
-  | Barrier_RISCV_w_w
-  | Barrier_RISCV_i
-  (* X86 *)
-  | Barrier_x86_MFENCE
-
-
-instance (Show barrier_kind)
-  let show = function
-    | Barrier_Sync -> "Barrier_Sync"
-    | Barrier_LwSync -> "Barrier_LwSync"
-    | Barrier_Eieio -> "Barrier_Eieio"
-    | Barrier_Isync -> "Barrier_Isync"
-    | Barrier_DMB -> "Barrier_DMB"
-    | Barrier_DMB_ST -> "Barrier_DMB_ST"
-    | Barrier_DMB_LD -> "Barrier_DMB_LD"
-    | Barrier_DSB -> "Barrier_DSB"
-    | Barrier_DSB_ST -> "Barrier_DSB_ST"
-    | Barrier_DSB_LD -> "Barrier_DSB_LD"
-    | 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_i     -> "Barrier_RISCV_i"
-    | Barrier_x86_MFENCE  -> "Barrier_x86_MFENCE"
-  end
-end
-
-type trans_kind =
-  (* AArch64 *)
-  | Transaction_start | Transaction_commit | Transaction_abort
-
-instance (Show trans_kind)
-  let show = function
-  | Transaction_start  -> "Transaction_start"
-  | Transaction_commit -> "Transaction_commit"
-  | Transaction_abort  -> "Transaction_abort"
-  end
-end
-
-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 (* 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
-
-
-instance (Show instruction_kind)
-  let show = function
-    | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind)
-    | IK_mem_read read_kind   -> "IK_mem_read " ^ (show read_kind)
-    | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind)
-    | IK_mem_rmw (r, w)       -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w)
-    | IK_branch               -> "IK_branch"
-    | IK_trans trans_kind     -> "IK_trans " ^ (show trans_kind)
-    | IK_simple               -> "IK_simple"
-  end
-end
-
-
-let read_is_exclusive = 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
-end
-
-
-
-instance (EnumerationType read_kind)
-  let toNat = 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
-  end
-end
-
-instance (EnumerationType write_kind)
-  let toNat = 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
-  end
-end
-
-instance (EnumerationType barrier_kind)
-  let toNat = function
-    | Barrier_Sync -> 0
-    | Barrier_LwSync -> 1
-    | Barrier_Eieio ->2
-    | Barrier_Isync -> 3
-    | Barrier_DMB -> 4
-    | Barrier_DMB_ST -> 5
-    | Barrier_DMB_LD -> 6
-    | Barrier_DSB -> 7
-    | Barrier_DSB_ST -> 8
-    | Barrier_DSB_LD -> 9
-    | Barrier_ISB -> 10
-    | Barrier_TM_COMMIT -> 11
-    | Barrier_MIPS_SYNC -> 12
-    | Barrier_RISCV_rw_rw -> 13
-    | Barrier_RISCV_r_rw -> 14
-    | Barrier_RISCV_r_r -> 15
-    | Barrier_RISCV_rw_w -> 16
-    | Barrier_RISCV_w_w -> 17
-    | Barrier_RISCV_i -> 18
-    | Barrier_x86_MFENCE -> 19
-  end
-end