diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/sail2_deep_shallow_convert.lem | 68 | ||||
| -rw-r--r-- | src/gen_lib/sail2_instr_kinds.lem | 376 | ||||
| -rw-r--r-- | src/gen_lib/sail2_operators.lem | 10 | ||||
| -rw-r--r-- | src/gen_lib/sail2_operators_bitlists.lem | 5 | ||||
| -rw-r--r-- | src/gen_lib/sail2_operators_mwords.lem | 3 | ||||
| -rw-r--r-- | src/gen_lib/sail2_prompt_monad.lem | 16 | ||||
| -rw-r--r-- | src/gen_lib/sail2_state_monad.lem | 10 | ||||
| -rw-r--r-- | src/gen_lib/sail2_values.lem | 46 |
8 files changed, 499 insertions, 35 deletions
diff --git a/src/gen_lib/sail2_deep_shallow_convert.lem b/src/gen_lib/sail2_deep_shallow_convert.lem index b963e537..2e3543b4 100644 --- a/src/gen_lib/sail2_deep_shallow_convert.lem +++ b/src/gen_lib/sail2_deep_shallow_convert.lem @@ -455,17 +455,61 @@ instance (ToFromInterpValue write_kind) end +let a64_barrier_domainToInterpValue = function + | A64_FullShare -> + V_ctor (Id_aux (Id "A64_FullShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 0) (toInterpValue ()) + | A64_InnerShare -> + V_ctor (Id_aux (Id "A64_InnerShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 1) (toInterpValue ()) + | A64_OuterShare -> + V_ctor (Id_aux (Id "A64_OuterShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 2) (toInterpValue ()) + | A64_NonShare -> + V_ctor (Id_aux (Id "A64_NonShare") Unknown) (T_id "a64_barrier_domain") (C_Enum 3) (toInterpValue ()) +end +let rec a64_barrier_domainFromInterpValue v = match v with + | V_ctor (Id_aux (Id "A64_FullShare") _) _ _ v -> A64_FullShare + | V_ctor (Id_aux (Id "A64_InnerShare") _) _ _ v -> A64_InnerShare + | V_ctor (Id_aux (Id "A64_OuterShare") _) _ _ v -> A64_OuterShare + | V_ctor (Id_aux (Id "A64_NonShare") _) _ _ v -> A64_NonShare + | V_tuple [v] -> a64_barrier_domainFromInterpValue v + | v -> failwith ("fromInterpValue a64_barrier_domain: unexpected value. " ^ + Interp.debug_print_value v) + end +instance (ToFromInterpValue a64_barrier_domain) + let toInterpValue = a64_barrier_domainToInterpValue + let fromInterpValue = a64_barrier_domainFromInterpValue +end + +let a64_barrier_typeToInterpValue = function + | A64_barrier_all -> + V_ctor (Id_aux (Id "A64_barrier_all") Unknown) (T_id "a64_barrier_type") (C_Enum 0) (toInterpValue ()) + | A64_barrier_LD -> + V_ctor (Id_aux (Id "A64_barrier_LD") Unknown) (T_id "a64_barrier_type") (C_Enum 1) (toInterpValue ()) + | A64_barrier_ST -> + V_ctor (Id_aux (Id "A64_barrier_ST") Unknown) (T_id "a64_barrier_type") (C_Enum 2) (toInterpValue ()) +end +let rec a64_barrier_typeFromInterpValue v = match v with + | V_ctor (Id_aux (Id "A64_barrier_all") _) _ _ v -> A64_barrier_all + | V_ctor (Id_aux (Id "A64_barrier_LD") _) _ _ v -> A64_barrier_LD + | V_ctor (Id_aux (Id "A64_barrier_ST") _) _ _ v -> A64_barrier_ST + | V_tuple [v] -> a64_barrier_typeFromInterpValue v + | v -> failwith ("fromInterpValue a64_barrier_type: unexpected value. " ^ + Interp.debug_print_value v) + end +instance (ToFromInterpValue a64_barrier_type) + let toInterpValue = a64_barrier_typeToInterpValue + let fromInterpValue = a64_barrier_typeFromInterpValue +end + + let barrier_kindToInterpValue = function | Barrier_Sync -> V_ctor (Id_aux (Id "Barrier_Sync") Unknown) (T_id "barrier_kind") (C_Enum 0) (toInterpValue ()) | Barrier_LwSync -> V_ctor (Id_aux (Id "Barrier_LwSync") Unknown) (T_id "barrier_kind") (C_Enum 1) (toInterpValue ()) | Barrier_Eieio -> V_ctor (Id_aux (Id "Barrier_Eieio") Unknown) (T_id "barrier_kind") (C_Enum 2) (toInterpValue ()) | Barrier_Isync -> V_ctor (Id_aux (Id "Barrier_Isync") Unknown) (T_id "barrier_kind") (C_Enum 3) (toInterpValue ()) - | Barrier_DMB -> V_ctor (Id_aux (Id "Barrier_DMB") Unknown) (T_id "barrier_kind") (C_Enum 4) (toInterpValue ()) - | Barrier_DMB_ST -> V_ctor (Id_aux (Id "Barrier_DMB_ST") Unknown) (T_id "barrier_kind") (C_Enum 5) (toInterpValue ()) - | Barrier_DMB_LD -> V_ctor (Id_aux (Id "Barrier_DMB_LD") Unknown) (T_id "barrier_kind") (C_Enum 6) (toInterpValue ()) - | Barrier_DSB -> V_ctor (Id_aux (Id "Barrier_DSB") Unknown) (T_id "barrier_kind") (C_Enum 7) (toInterpValue ()) - | Barrier_DSB_ST -> V_ctor (Id_aux (Id "Barrier_DSB_ST") Unknown) (T_id "barrier_kind") (C_Enum 8) (toInterpValue ()) - | Barrier_DSB_LD -> V_ctor (Id_aux (Id "Barrier_DSB_LD") Unknown) (T_id "barrier_kind") (C_Enum 9) (toInterpValue ()) + | Barrier_DMB (dom,typ) -> + V_ctor (Id_aux (Id "Barrier_DMB") Unknown) (T_id "barrier_kind") C_Union (toInterpValue (dom, typ)) + | Barrier_DSB (dom,typ) -> + V_ctor (Id_aux (Id "Barrier_DSB") Unknown) (T_id "barrier_kind") C_Union (toInterpValue (dom, typ)) | Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ()) | Barrier_TM_COMMIT -> V_ctor (Id_aux (Id "Barrier_TM_COMMIT") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ()) | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 12) (toInterpValue ()) @@ -482,12 +526,12 @@ let rec barrier_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "Barrier_LwSync") _) _ _ v -> Barrier_LwSync | V_ctor (Id_aux (Id "Barrier_Eieio") _) _ _ v -> Barrier_Eieio | V_ctor (Id_aux (Id "Barrier_Isync") _) _ _ v -> Barrier_Isync - | V_ctor (Id_aux (Id "Barrier_DMB") _) _ _ v -> Barrier_DMB - | V_ctor (Id_aux (Id "Barrier_DMB_ST") _) _ _ v -> Barrier_DMB_ST - | V_ctor (Id_aux (Id "Barrier_DMB_LD") _) _ _ v -> Barrier_DMB_LD - | V_ctor (Id_aux (Id "Barrier_DSB") _) _ _ v -> Barrier_DSB - | V_ctor (Id_aux (Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST - | V_ctor (Id_aux (Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD + | V_ctor (Id_aux (Id "Barrier_DMB") _) _ _ v -> + let (dom, typ) = fromInterpValue v in + Barrier_DMB (dom,typ) + | V_ctor (Id_aux (Id "Barrier_DSB") _) _ _ v -> + let (dom, typ) = fromInterpValue v in + Barrier_DSB (dom,typ) | V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB | V_ctor (Id_aux (Id "Barrier_TM_COMMIT") _) _ _ v -> Barrier_TM_COMMIT | V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") _) _ _ v -> Barrier_MIPS_SYNC 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.lem b/src/gen_lib/sail2_operators.lem index 547160d3..43a9812e 100644 --- a/src/gen_lib/sail2_operators.lem +++ b/src/gen_lib/sail2_operators.lem @@ -163,9 +163,9 @@ let arith_op_bv_no0 op sign size l r = Maybe.bind (int_of_bv sign r) (fun r' -> if r' = 0 then Nothing else Just (of_int (length l * size) (op l' r')))) -let mod_bv = arith_op_bv_no0 hardware_mod false 1 -let quot_bv = arith_op_bv_no0 hardware_quot false 1 -let quots_bv = arith_op_bv_no0 hardware_quot true 1 +let mod_bv = arith_op_bv_no0 tmod_int false 1 +let quot_bv = arith_op_bv_no0 tdiv_int false 1 +let quots_bv = arith_op_bv_no0 tdiv_int true 1 let mod_mword = Machine_word.modulo let quot_mword = Machine_word.unsignedDivide @@ -174,8 +174,8 @@ let quots_mword = Machine_word.signedDivide let arith_op_bv_int_no0 op sign size l r = arith_op_bv_no0 op sign size l (of_int (length l) r) -let quot_bv_int = arith_op_bv_int_no0 hardware_quot false 1 -let mod_bv_int = arith_op_bv_int_no0 hardware_mod false 1 +let quot_bv_int = arith_op_bv_int_no0 tdiv_int false 1 +let mod_bv_int = arith_op_bv_int_no0 tmod_int false 1 let mod_mword_int l r = Machine_word.modulo l (wordFromInteger r) let quot_mword_int l r = Machine_word.unsignedDivide l (wordFromInteger r) diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem index 8b75fa38..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 @@ -304,3 +307,5 @@ val eq_vec : list bitU -> list bitU -> bool val neq_vec : list bitU -> list bitU -> bool let eq_vec = eq_bv let neq_vec = neq_bv + +let inline count_leading_zeros v = count_leading_zero_bits v diff --git a/src/gen_lib/sail2_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem index 181fa149..c8524e16 100644 --- a/src/gen_lib/sail2_operators_mwords.lem +++ b/src/gen_lib/sail2_operators_mwords.lem @@ -329,3 +329,6 @@ val eq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val neq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool let inline eq_vec = eq_mword let inline neq_vec = neq_mword + +val count_leading_zeros : forall 'a. Size 'a => mword 'a -> integer +let count_leading_zeros v = count_leading_zeros_bv v diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem index e0ac09f6..a35165b9 100644 --- a/src/gen_lib/sail2_prompt_monad.lem +++ b/src/gen_lib/sail2_prompt_monad.lem @@ -170,8 +170,8 @@ let read_mem_bytes rk addr sz = (maybe_fail "nat_of_bv" (nat_of_bv addr)) (fun addr -> Read_mem rk addr (nat_of_int sz) return) -val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e -let read_mem rk addr sz = +val read_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b => read_kind -> 'addrsize -> 'a -> integer -> monad 'rv 'b 'e +let read_mem rk addr_sz addr sz = bind (read_mem_bytes rk addr sz) (fun bytes -> @@ -185,15 +185,15 @@ let excl_result () = let k successful = (return successful) in Excl_res k -val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e -let write_mem_ea wk addr sz = +val write_mem_ea : forall 'rv 'a 'e 'addrsize. Bitvector 'a => write_kind -> 'addrsize -> 'a -> integer -> monad 'rv unit 'e +let write_mem_ea wk addr_size addr sz = bind (maybe_fail "nat_of_bv" (nat_of_bv addr)) (fun addr -> Write_ea wk addr (nat_of_int sz) (Done ())) -val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => - write_kind -> 'a -> integer -> 'b -> monad 'rv bool 'e -let write_mem wk addr sz v = +val write_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b => + write_kind -> 'addrsize -> 'a -> integer -> 'b -> monad 'rv bool 'e +let write_mem wk addr_size addr sz v = match (mem_bytes_of_bits v, nat_of_bv addr) with | (Just v, Just addr) -> Write_mem wk addr (nat_of_int sz) v return @@ -235,7 +235,7 @@ let read_reg_bitfield reg regfield = read_reg_aux (external_reg_field_whole reg regfield) >>= fun v -> return (extract_only_element v)*) -let reg_deref = read_reg +let inline reg_deref = read_reg val write_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> 'a -> monad 'rv unit 'e let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ()) diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem index 3042700c..8ea919f9 100644 --- a/src/gen_lib/sail2_state_monad.lem +++ b/src/gen_lib/sail2_state_monad.lem @@ -147,8 +147,8 @@ let read_memtS rk a sz = maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val -> returnS (mem_val, tag)))) -val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e -let read_memS rk a sz = +val read_memS : forall 'regs 'e 'a 'b 'addrsize. Bitvector 'a, Bitvector 'b => read_kind -> 'addrsize -> 'a -> integer -> monadS 'regs 'b 'e +let read_memS rk addr_size a sz = read_memtS rk a sz >>$= (fun (bytes, _) -> returnS bytes) @@ -186,9 +186,9 @@ let write_memtS wk addr sz v t = | _ -> failS "write_mem" end -val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => - write_kind -> 'a -> integer -> 'b -> monadS 'regs bool 'e -let write_memS wk addr sz v = write_memtS wk addr sz v B0 +val write_memS : forall 'regs 'e 'a 'b 'addrsize. Bitvector 'a, Bitvector 'b => + write_kind -> 'addrsize -> 'a -> integer -> 'b -> monadS 'regs bool 'e +let write_memS wk addr_size addr sz v = write_memtS wk addr sz v B0 val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e let read_regS reg = readS (fun s -> reg.read_from s.regstate) diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem index 5e6537a8..69bf0852 100644 --- a/src/gen_lib/sail2_values.lem +++ b/src/gen_lib/sail2_values.lem @@ -104,21 +104,25 @@ let upper n = n (* Modulus operation corresponding to quot below -- result has sign of dividend. *) -let hardware_mod (a: integer) (b:integer) : integer = +let tmod_int (a: integer) (b:integer) : integer = let m = (abs a) mod (abs b) in if a < 0 then ~m else m +let hardware_mod = tmod_int + (* There are different possible answers for integer divide regarding rounding behaviour on negative operands. Positive operands always round down so derive the one we want (trucation towards zero) from that *) -let hardware_quot (a:integer) (b:integer) : integer = +let tdiv_int (a:integer) (b:integer) : integer = let q = (abs a) / (abs b) in if ((a<0) = (b<0)) then q (* same sign -- result positive *) else ~q (* different sign -- result negative *) +let hardware_quot = tdiv_int + let max_64u = (integerPow 2 64) - 1 let max_64 = (integerPow 2 63) - 1 let min_64 = 0 - (integerPow 2 63) @@ -419,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 @@ -432,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 @@ -652,6 +678,16 @@ let int_of_bit b = | _ -> failwith "int_of_bit saw unknown" end +val count_leading_zero_bits : list bitU -> integer +let rec count_leading_zero_bits v = + match v with + | B0 :: v' -> count_leading_zero_bits v' + 1 + | _ -> 0 + end + +val count_leading_zeros_bv : forall 'a. Bitvector 'a => 'a -> integer +let count_leading_zeros_bv v = count_leading_zero_bits (bits_of v) + val decimal_string_of_bv : forall 'a. Bitvector 'a => 'a -> string let decimal_string_of_bv bv = let place_values = |