Merge master branch into sail2 for OCaml 4.06 compatibility

1 files changed, 62 insertions, 204 deletions

diff --git a/src/lem_interp/sail_instr_kinds.lem b/src/lem_interp/sail_instr_kinds.lem
index 89ff67b2..d8a2c0c0 100644
--- a/src/lem_interp/sail_instr_kinds.lem
+++ b/src/lem_interp/sail_instr_kinds.lem
@@ -50,6 +50,27 @@
 
 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
@@ -177,10 +198,9 @@ type instruction_kind =
   | IK_mem_read  of read_kind
   | IK_mem_write of write_kind
   | IK_mem_rmw   of (read_kind * write_kind)
-  | IK_cond_branch
-  (* unconditional branches are not distinguished in the instruction_kind;
-  they just have particular nias (and will be IK_simple *)
-  (* | IK_uncond_branch *)
+  | 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
 
@@ -188,80 +208,16 @@ type instruction_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_read read_kind   -> "IK_mem_read " ^ (show read_kind)
     | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind)
-    | IK_cond_branch -> "IK_cond_branch"
-    | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind)
-    | IK_simple -> "IK_simple"
+    | 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 ~{ocaml} read_kindCompare rk1 rk2 =
-  match (rk1, rk2) with
-  | (Read_plain, Read_plain)             -> EQ
-  | (Read_plain, Read_reserve)           -> LT
-  | (Read_plain, Read_acquire)           -> LT
-  | (Read_plain, Read_exclusive)         -> LT
-  | (Read_plain, Read_exclusive_acquire) -> LT
-  | (Read_plain, Read_stream)            -> LT
-
-  | (Read_reserve, Read_plain)             -> GT
-  | (Read_reserve, Read_reserve)           -> EQ
-  | (Read_reserve, Read_acquire)           -> LT
-  | (Read_reserve, Read_exclusive)         -> LT
-  | (Read_reserve, Read_exclusive_acquire) -> LT
-  | (Read_reserve, Read_stream)            -> LT
-
-  | (Read_acquire, Read_plain)             -> GT
-  | (Read_acquire, Read_reserve)           -> GT
-  | (Read_acquire, Read_acquire)           -> EQ
-  | (Read_acquire, Read_exclusive)         -> LT
-  | (Read_acquire, Read_exclusive_acquire) -> LT
-  | (Read_acquire, Read_stream)            -> LT
-
-  | (Read_exclusive, Read_plain)             -> GT
-  | (Read_exclusive, Read_reserve)           -> GT
-  | (Read_exclusive, Read_acquire)           -> GT
-  | (Read_exclusive, Read_exclusive)         -> EQ
-  | (Read_exclusive, Read_exclusive_acquire) -> LT
-  | (Read_exclusive, Read_stream)            -> LT
-
-  | (Read_exclusive_acquire, Read_plain)             -> GT
-  | (Read_exclusive_acquire, Read_reserve)           -> GT
-  | (Read_exclusive_acquire, Read_acquire)           -> GT
-  | (Read_exclusive_acquire, Read_exclusive)         -> GT
-  | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ
-  | (Read_exclusive_acquire, Read_stream)            -> GT
-
-  | (Read_stream, Read_plain)             -> GT
-  | (Read_stream, Read_reserve)           -> GT
-  | (Read_stream, Read_acquire)           -> GT
-  | (Read_stream, Read_exclusive)         -> GT
-  | (Read_stream, Read_exclusive_acquire) -> GT
-  | (Read_stream, Read_stream)            -> EQ
-end
-let inline {ocaml} read_kindCompare = defaultCompare
-
-let ~{ocaml} read_kindLess b1 b2      = read_kindCompare b1 b2 =  LT
-let ~{ocaml} read_kindLessEq b1 b2    = read_kindCompare b1 b2 <> GT
-let ~{ocaml} read_kindGreater b1 b2   = read_kindCompare b1 b2 =  GT
-let ~{ocaml} read_kindGreaterEq b1 b2 = read_kindCompare b1 b2 <> LT
-
-let inline {ocaml} read_kindLess      = defaultLess
-let inline {ocaml} read_kindLessEq    = defaultLessEq
-let inline {ocaml} read_kindGreater   = defaultGreater
-let inline {ocaml} read_kindGreaterEq = defaultGreaterEq
-
-instance (Ord read_kind)
-  let compare = read_kindCompare
-  let (<)  = read_kindLess
-  let (<=) = read_kindLessEq
-  let (>)  = read_kindGreater
-  let (>=) = read_kindGreaterEq
-end
-
 let read_is_exclusive = function
   | Read_plain -> false
   | Read_reserve -> true
@@ -277,63 +233,46 @@ let read_is_exclusive = function
   | Read_X86_locked -> true
 end
 
-let ~{ocaml} write_kindCompare wk1 wk2 =
-  match (wk1, wk2) with
-  | (Write_plain, Write_plain)             -> EQ
-  | (Write_plain, Write_conditional)       -> LT
-  | (Write_plain, Write_release)           -> LT
-  | (Write_plain, Write_exclusive)         -> LT
-  | (Write_plain, Write_exclusive_release) -> LT
-
-  | (Write_conditional, Write_plain)             -> GT
-  | (Write_conditional, Write_conditional)       -> EQ
-  | (Write_conditional, Write_release)           -> LT
-  | (Write_conditional, Write_exclusive)         -> LT
-  | (Write_conditional, Write_exclusive_release) -> LT
-
-  | (Write_release, Write_plain)             -> GT
-  | (Write_release, Write_conditional)       -> GT
-  | (Write_release, Write_release)           -> EQ
-  | (Write_release, Write_exclusive)         -> LT
-  | (Write_release, Write_exclusive_release) -> LT
 
-  | (Write_exclusive, Write_plain)             -> GT
-  | (Write_exclusive, Write_conditional)       -> GT
-  | (Write_exclusive, Write_release)           -> GT
-  | (Write_exclusive, Write_exclusive)         -> EQ
-  | (Write_exclusive, Write_exclusive_release) -> LT
 
-  | (Write_exclusive_release, Write_plain)             -> GT
-  | (Write_exclusive_release, Write_conditional)       -> GT
-  | (Write_exclusive_release, Write_release)           -> GT
-  | (Write_exclusive_release, Write_exclusive)         -> GT
-  | (Write_exclusive_release, Write_exclusive_release) -> EQ
+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
-let inline {ocaml} write_kindCompare = defaultCompare
-
-let ~{ocaml} write_kindLess b1 b2      = write_kindCompare b1 b2 =  LT
-let ~{ocaml} write_kindLessEq b1 b2    = write_kindCompare b1 b2 <> GT
-let ~{ocaml} write_kindGreater b1 b2   = write_kindCompare b1 b2 =  GT
-let ~{ocaml} write_kindGreaterEq b1 b2 = write_kindCompare b1 b2 <> LT
-
-let inline {ocaml} write_kindLess      = defaultLess
-let inline {ocaml} write_kindLessEq    = defaultLessEq
-let inline {ocaml} write_kindGreater   = defaultGreater
-let inline {ocaml} write_kindGreaterEq = defaultGreaterEq
 
-instance (Ord write_kind)
-  let compare = write_kindCompare
-  let (<)  = write_kindLess
-  let (<=) = write_kindLessEq
-  let (>)  = write_kindGreater
-  let (>=) = write_kindGreaterEq
+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
 
-(* Barrier comparison that uses less memory in Isabelle/HOL *)
-let ~{ocaml} barrier_number = function
-    | Barrier_Sync -> (0 : natural)
+instance (EnumerationType barrier_kind)
+  let toNat = function
+    | Barrier_Sync -> 0
     | Barrier_LwSync -> 1
-    | Barrier_Eieio -> 2
+    | Barrier_Eieio ->2
     | Barrier_Isync -> 3
     | Barrier_DMB -> 4
     | Barrier_DMB_ST -> 5
@@ -352,85 +291,4 @@ let ~{ocaml} barrier_number = function
     | Barrier_RISCV_i -> 18
     | Barrier_x86_MFENCE -> 19
   end
-
-let ~{ocaml} barrier_kindCompare bk1 bk2 =
-  let n1 = barrier_number bk1 in
-  let n2 = barrier_number bk2 in
-  if n1 < n2 then LT
-  else if n1 = n2 then EQ
-  else GT
-let inline {ocaml} barrier_kindCompare = defaultCompare
-
-(*let ~{ocaml} barrier_kindCompare bk1 bk2 =
-  match (bk1, bk2) with
-  | (Barrier_Sync, Barrier_Sync) -> EQ
-  | (Barrier_Sync, _) -> LT
-  | (_, Barrier_Sync) -> GT
-
-  | (Barrier_LwSync, Barrier_LwSync) -> EQ
-  | (Barrier_LwSync, _) -> LT
-  | (_, Barrier_LwSync) -> GT
-
-  | (Barrier_Eieio, Barrier_Eieio) -> EQ
-  | (Barrier_Eieio, _) -> LT
-  | (_, Barrier_Eieio) -> GT
-
-  | (Barrier_Isync, Barrier_Isync) -> EQ
-  | (Barrier_Isync, _) -> LT
-  | (_, Barrier_Isync) -> GT
-
-  | (Barrier_DMB, Barrier_DMB) -> EQ
-  | (Barrier_DMB, _) -> LT
-  | (_, Barrier_DMB) -> GT
-
-  | (Barrier_DMB_ST, Barrier_DMB_ST) -> EQ
-  | (Barrier_DMB_ST, _) -> LT
-  | (_, Barrier_DMB_ST) -> GT
-
-  | (Barrier_DMB_LD, Barrier_DMB_LD) -> EQ
-  | (Barrier_DMB_LD, _) -> LT
-  | (_, Barrier_DMB_LD) -> GT
-
-  | (Barrier_DSB, Barrier_DSB) -> EQ
-  | (Barrier_DSB, _) -> LT
-  | (_, Barrier_DSB) -> GT
-
-  | (Barrier_DSB_ST, Barrier_DSB_ST) -> EQ
-  | (Barrier_DSB_ST, _) -> LT
-  | (_, Barrier_DSB_ST) -> GT
-
-  | (Barrier_DSB_LD, Barrier_DSB_LD) -> EQ
-  | (Barrier_DSB_LD, _) -> LT
-  | (_, Barrier_DSB_LD) -> GT
-
-  | (Barrier_ISB, Barrier_ISB) -> EQ
-  | (Barrier_ISB, _) -> LT
-  | (_, Barrier_ISB) -> GT
-
-  | (Barrier_TM_COMMIT, Barrier_TM_COMMIT) -> EQ
-  | (Barrier_TM_COMMIT, _) -> LT
-  | (_, Barrier_TM_COMMIT) -> GT
-
-  | (Barrier_MIPS_SYNC, Barrier_MIPS_SYNC) -> EQ
-  (* | (Barrier_MIPS_SYNC, _) -> LT
-  | (_, Barrier_MIPS_SYNC) -> GT *)
-
-  end*)
-
-let ~{ocaml} barrier_kindLess b1 b2      = barrier_kindCompare b1 b2 =  LT
-let ~{ocaml} barrier_kindLessEq b1 b2    = barrier_kindCompare b1 b2 <> GT
-let ~{ocaml} barrier_kindGreater b1 b2   = barrier_kindCompare b1 b2 =  GT
-let ~{ocaml} barrier_kindGreaterEq b1 b2 = barrier_kindCompare b1 b2 <> LT
-
-let inline {ocaml} barrier_kindLess      = defaultLess
-let inline {ocaml} barrier_kindLessEq    = defaultLessEq
-let inline {ocaml} barrier_kindGreater   = defaultGreater
-let inline {ocaml} barrier_kindGreaterEq = defaultGreaterEq
-
-instance (Ord barrier_kind)
-  let compare = barrier_kindCompare
-  let (<)  = barrier_kindLess
-  let (<=) = barrier_kindLessEq
-  let (>)  = barrier_kindGreater
-  let (>=) = barrier_kindGreaterEq
 end