diff options
Diffstat (limited to 'src/lem_interp/sail_impl_base.lem')
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 339 |
1 files changed, 272 insertions, 67 deletions
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index c0ec8548..59e86ece 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -106,6 +106,8 @@ type register_value = <| type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *) (*MSB first everywhere*) +type instruction_field_value = list bit + type byte = Byte of list bit (* of length 8 *) (*MSB first everywhere*) type address_lifted = Address_lifted of list byte_lifted (* of length 8 for 64bit machines*) * maybe integer @@ -131,22 +133,66 @@ type address = Address of list byte (* of length 8 *) * integer type opcode = Opcode of list byte (* of length 4 *) (** typeclass instantiations *) - -instance (EnumerationType bit) - let toNat = function - | Bitc_zero -> 0 - | Bitc_one -> 1 +let ~{ocaml} bitCompare (b1:bit) (b2:bit) = + match (b1,b2) with + | (Bitc_zero, Bitc_zero) -> EQ + | (Bitc_one, Bitc_one) -> EQ + | (Bitc_zero, _) -> LT + | (_,_) -> GT end +let inline {ocaml} bitCompare = defaultCompare + +let ~{ocaml} bitLess b1 b2 = bitCompare b1 b2 = LT +let ~{ocaml} bitLessEq b1 b2 = bitCompare b1 b2 <> GT +let ~{ocaml} bitGreater b1 b2 = bitCompare b1 b2 = GT +let ~{ocaml} bitGreaterEq b1 b2 = bitCompare b1 b2 <> LT + +let inline {ocaml} bitLess = defaultLess +let inline {ocaml} bitLessEq = defaultLessEq +let inline {ocaml} bitGreater = defaultGreater +let inline {ocaml} bitGreaterEq = defaultGreaterEq + +instance (Ord bit) + let compare = bitCompare + let (<) = bitLess + let (<=) = bitLessEq + let (>) = bitGreater + let (>=) = bitGreaterEq end -instance (EnumerationType bit_lifted) - let toNat = function - | Bitl_zero -> 0 - | Bitl_one -> 1 - | Bitl_undef -> 2 - | Bitl_unknown -> 3 +let ~{ocaml} bit_liftedCompare (bl1:bit_lifted) (bl2:bit_lifted) = + match (bl1,bl2) with + | (Bitl_zero, Bitl_zero) -> EQ + | (Bitl_zero,_) -> LT + | (Bitl_one, Bitl_zero) -> GT + | (Bitl_one, Bitl_one) -> EQ + | (Bitl_one, _) -> LT + | (Bitl_undef,Bitl_zero) -> GT + | (Bitl_undef,Bitl_one) -> GT + | (Bitl_undef,Bitl_undef) -> EQ + | (Bitl_undef,_) -> LT + | (Bitl_unknown,Bitl_unknown) -> EQ + | (Bitl_unknown,_) -> GT end +let inline {ocaml} bit_liftedCompare = defaultCompare + +let ~{ocaml} bit_liftedLess b1 b2 = bit_liftedCompare b1 b2 = LT +let ~{ocaml} bit_liftedLessEq b1 b2 = bit_liftedCompare b1 b2 <> GT +let ~{ocaml} bit_liftedGreater b1 b2 = bit_liftedCompare b1 b2 = GT +let ~{ocaml} bit_liftedGreaterEq b1 b2 = bit_liftedCompare b1 b2 <> LT + +let inline {ocaml} bit_liftedLess = defaultLess +let inline {ocaml} bit_liftedLessEq = defaultLessEq +let inline {ocaml} bit_liftedGreater = defaultGreater +let inline {ocaml} bit_liftedGreaterEq = defaultGreaterEq + +instance (Ord bit_lifted) + let compare = bit_liftedCompare + let (<) = bit_liftedLess + let (<=) = bit_liftedLessEq + let (>) = bit_liftedGreater + let (>=) = bit_liftedGreaterEq end let ~{ocaml} byte_liftedCompare (Byte_lifted b1) (Byte_lifted b2) = compare b1 b2 @@ -191,10 +237,6 @@ instance (Ord byte) let (>=) = byteGreaterEq end - - - - let ~{ocaml} opcodeCompare (Opcode o1) (Opcode o2) = compare o1 o2 let {ocaml} opcodeCompare = defaultCompare @@ -216,10 +258,6 @@ instance (Ord opcode) let (>) = opcodeGreater let (>=) = opcodeGreaterEq end - - - - let addressCompare (Address b1 i1) (Address b2 i2) = compare i1 i2 (* this cannot be defaultCompare for OCaml because addresses contain big ints *) @@ -562,55 +600,137 @@ 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_mem_rmw (r, w) -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w) - | IK_cond_branch -> "IK_cond_branch" - | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind) - | IK_simple -> "IK_simple" + | IK_cond_branch -> "IK_cond_branch" + | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind) + | IK_simple -> "IK_simple" end 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 +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 -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 +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 -instance (EnumerationType barrier_kind) - let toNat = function - | Barrier_Sync -> 0 +(* 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_Eieio -> 2 | Barrier_Isync -> 3 | Barrier_DMB -> 4 | Barrier_DMB_ST -> 5 @@ -629,6 +749,88 @@ instance (EnumerationType barrier_kind) | 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 ~{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 inline {ocaml} barrier_kindCompare = defaultCompare + +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 type event = @@ -696,32 +898,35 @@ end (* the address_lifted types should go away here and be replaced by address *) type with_aux 'o = 'o * maybe ((unit -> (string * string)) * ((list (reg_name * register_value)) -> list event)) -type outcome 'a = +type outcome_r 'a 'r = (* Request to read memory, value is location to read, integer is size to read, followed by registers that were used in computing that size *) - | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome 'a)) + | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> with_aux (outcome_r 'a 'r)) (* Tell the system a write is imminent, at address lifted, of size nat *) - | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome 'a)) + | Write_ea of (write_kind * address_lifted * nat) * (with_aux (outcome_r 'a 'r)) (* Request the result of store-exclusive *) - | Excl_res of (bool -> with_aux (outcome 'a)) + | Excl_res of (bool -> with_aux (outcome_r 'a 'r)) (* Request to write memory at last signalled address. Memory value should be 8 times the size given in ea signal *) - | Write_memv of memory_value * (bool -> with_aux (outcome 'a)) + | Write_memv of memory_value * (bool -> with_aux (outcome_r 'a 'r)) (* Request a memory barrier *) - | Barrier of barrier_kind * with_aux (outcome 'a) + | Barrier of barrier_kind * with_aux (outcome_r 'a 'r) (* Tell the system to dynamically recalculate dependency footprint *) - | Footprint of with_aux (outcome 'a) + | Footprint of with_aux (outcome_r 'a 'r) (* Request to read register, will track dependency when mode.track_values *) - | Read_reg of reg_name * (register_value -> with_aux (outcome 'a)) + | Read_reg of reg_name * (register_value -> with_aux (outcome_r 'a 'r)) (* Request to write register *) - | Write_reg of (reg_name * register_value) * with_aux (outcome 'a) + | Write_reg of (reg_name * register_value) * with_aux (outcome_r 'a 'r) | Escape of maybe string (*Result of a failed assert with possible error message to report*) | Fail of maybe string - | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome 'a) + (* Early return with value of type 'r *) + | Return of 'r + | Internal of (maybe string * maybe (unit -> string)) * with_aux (outcome_r 'a 'r) | Done of 'a | Error of string +type outcome 'a = outcome_r 'a unit type outcome_s 'a = with_aux (outcome 'a) (* first string : output of instruction_stack_to_string second string: output of local_variables_to_string *) |