Merge branch 'sail2' of https://github.com/rems-project/sail into sail2

3 files changed, 404 insertions, 3 deletions

diff --git a/src/gen_lib/sail2_instr_kinds.lem b/src/gen_lib/sail2_instr_kinds.lem
new file mode 100644
index 00000000..f3cdfbc9
--- /dev/null
+++ b/src/gen_lib/sail2_instr_kinds.lem
@@ -0,0 +1,376 @@
+(*========================================================================*)
+(*     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 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 = function
+  | A64_FullShare  -> "A64_FullShare"
+  | A64_InnerShare -> "A64_InnerShare"
+  | A64_OuterShare -> "A64_OuterShare"
+  | A64_NonShare   -> "A64_NonShare"
+end
+
+instance (Show a64_barrier_domain)
+  let show = string_a64_barrier_domain
+end
+
+let string_a64_barrier_type = function
+  | A64_barrier_all -> "A64_barrier_all"
+  | A64_barrier_LD  -> "A64_barrier_LD"
+  | A64_barrier_ST  -> "A64_barrier_ST"
+end
+
+instance (Show a64_barrier_type)
+  let show = string_a64_barrier_type
+end
+
+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 (dom,typ) -> "Barrier_DMB (" ^ (show dom) ^ ", " ^ (show typ) ^ ")"
+    | Barrier_DSB (dom,typ) -> "Barrier_DSB (" ^ (show dom) ^ ", " ^ (show 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"
+  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
+
+(* 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
+
+instance (Show cache_op_kind)
+  let show = 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"
+  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    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
+
+
+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"
+    | IK_cache_op cache_kind  -> "IK_cache_op " ^ (show cache_kind)
+  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 a64_barrier_domain)
+  let toNat = function
+    | A64_FullShare  -> 0
+    | A64_InnerShare -> 1
+    | A64_OuterShare -> 2
+    | A64_NonShare   -> 3
+  end
+end
+
+instance (EnumerationType a64_barrier_type)
+  let toNat = function
+    | A64_barrier_all -> 0
+    | A64_barrier_LD  -> 1
+    | A64_barrier_ST  -> 2
+  end
+end
+
+instance (EnumerationType barrier_kind)
+  let toNat = function
+    | Barrier_Sync () -> 0
+    | Barrier_LwSync () -> 1
+    | Barrier_Eieio () -> 2
+    | Barrier_Isync () -> 3
+    | Barrier_DMB (dom,typ) -> 4  + (toNat dom) + (4 * (toNat typ)) (* 4-15 *)
+    | Barrier_DSB (dom,typ) -> 16 + (toNat dom) + (4 * (toNat 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
+  end
+end
diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index c9892e4c..15daa545 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -38,6 +38,9 @@ let sign_extend bits len = exts_bits len bits
 val zeros : integer -> list bitU
 let zeros len = repeat [B0] len
 
+val ones : integer -> list bitU
+let ones len = repeat [B1] len
+
 val vector_truncate : list bitU -> integer -> list bitU
 let vector_truncate bs len = extz_bv len bs
 
diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index f657803f..69bf0852 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -423,6 +423,26 @@ let char_of_nibble = function
   | _ -> Nothing
   end
 
+let nibble_of_char = function
+  | #'0' -> Just (B0, B0, B0, B0)
+  | #'1' -> Just (B0, B0, B0, B1)
+  | #'2' -> Just (B0, B0, B1, B0)
+  | #'3' -> Just (B0, B0, B1, B1)
+  | #'4' -> Just (B0, B1, B0, B0)
+  | #'5' -> Just (B0, B1, B0, B1)
+  | #'6' -> Just (B0, B1, B1, B0)
+  | #'7' -> Just (B0, B1, B1, B1)
+  | #'8' -> Just (B1, B0, B0, B0)
+  | #'9' -> Just (B1, B0, B0, B1)
+  | #'A' -> Just (B1, B0, B1, B0)
+  | #'B' -> Just (B1, B0, B1, B1)
+  | #'C' -> Just (B1, B1, B0, B0)
+  | #'D' -> Just (B1, B1, B0, B1)
+  | #'E' -> Just (B1, B1, B1, B0)
+  | #'F' -> Just (B1, B1, B1, B1)
+  | _ -> Nothing
+  end
+
 let rec hexstring_of_bits bs = match bs with
   | b1 :: b2 :: b3 :: b4 :: bs ->
      let n = char_of_nibble (b1, b2, b3, b4) in
@@ -436,12 +456,14 @@ let rec hexstring_of_bits bs = match bs with
   end
 declare {isabelle; hol} termination_argument hexstring_of_bits = automatic
 
-let show_bitlist bs =
+let show_bitlist_prefix c bs =
   match hexstring_of_bits bs with
-  | Just s -> toString (#'0' :: #'x' :: s)
-  | Nothing -> toString (#'0' :: #'b' :: map bitU_char bs)
+  | Just s -> toString (c :: #'x' :: s)
+  | Nothing -> toString (c :: #'b' :: map bitU_char bs)
   end
 
+let show_bitlist bs = show_bitlist_prefix #'0' bs
+
 (*** List operations *)
 
 let inline (^^) = append_list