path: root/src/lem_interp/sail_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 import Pervasives_extra

(* 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_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_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_cond_branch -> "IK_cond_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
  | 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

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
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
end

(* Barrier comparison that uses less memory in Isabelle/HOL *)
let ~{ocaml} barrier_number = function
    | Barrier_Sync -> (0 : natural)
    | 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

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