From 2300d45d6645faae3c00a183e80547c1a6cb9165 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 29 Aug 2017 17:42:56 +0100 Subject: Make Lem export of CHERI(-256) typecheck Note: The effect annotations of the execute function differ between CHERI and MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the initial declarations of ast, decode, and execute (with the right effects for MIPS). --- src/gen_lib/sail_operators.lem | 2 ++ src/gen_lib/sail_operators_mwords.lem | 2 ++ src/gen_lib/sail_values.lem | 2 ++ 3 files changed, 6 insertions(+) (limited to 'src/gen_lib') diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index 3919d540..fbe096c9 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -34,6 +34,8 @@ let adjust_start_index (start, v) = set_vector_start (start, v) let cast_vec_bool v = bitU_to_bool (extract_only_element v) let cast_bit_vec (start, len, b) = Vector (repeat [b] len) start false +let cast_boolvec_bitvec (Vector bs start inc) = + Vector (List.map bool_to_bitU bs) start inc let pp_bitu_vector (Vector elems start inc) = let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 10a56ad5..9bc81b3e 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -96,6 +96,8 @@ let adjust_start_index (start, v) = set_bitvector_start (start, v) let cast_vec_bool v = bitU_to_bool (extract_only_bit v) let cast_bit_vec (start, len, b) = vec_to_bvec (Vector [b] start false) +let cast_boolvec_bitvec (Vector bs start inc) = + vec_to_bvec (Vector (List.map bool_to_bitU bs) start inc) let pp_bitu_vector (Vector elems start inc) = let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index eeec7440..e2cbb98a 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -11,6 +11,8 @@ type nn = natural val pow : integer -> integer -> integer let pow m n = m ** (natFromInteger n) +let pow2 n = pow 2 n + let bool_or (l, r) = (l || r) let bool_and (l, r) = (l && r) let bool_xor (l, r) = xor l r -- cgit v1.2.3 From 811bd830e2768a920d4be1473085905ac10a7627 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Sat, 2 Sep 2017 20:14:17 +0100 Subject: Remove dependency of state.lem on bitvector operations --- src/gen_lib/sail_operators.lem | 18 +++++++++++++++ src/gen_lib/sail_operators_mwords.lem | 14 ++++++++++++ src/gen_lib/state.lem | 41 +++++++---------------------------- 3 files changed, 40 insertions(+), 33 deletions(-) (limited to 'src/gen_lib') diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index fbe096c9..a760fb42 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -205,6 +205,7 @@ let modulo (l,r) = hardware_mod l r let quot = hardware_quot let power (l,r) = integerPow l r +let add_int = add let sub_int = sub let mult_int = mult @@ -452,6 +453,9 @@ let rec repeat xs n = let duplicate (bit, length) = Vector (repeat [bit] length) (length - 1) false +let replicate_bits (v, count) = + Vector (repeat (get_elems v) count) ((length v * count) - 1) false + let compare_op op (l,r) = (op l r) let lt = compare_op (<) @@ -531,3 +535,17 @@ let make_bitvector_undef length = let mask' (start, n, Vector bits _ dir) = let current_size = List.length bits in Vector (drop (current_size - (natFromInteger n)) bits) start dir + + +(* Register operations *) + +let update_reg_range i j reg_val new_val = update reg_val i j new_val +let update_reg_bit i reg_val bit = update_pos reg_val i bit +let update_reg_field_range regfield i j reg_val new_val = + let current_field_value = regfield.get_field reg_val in + let new_field_value = update current_field_value i j new_val in + regfield.set_field reg_val new_field_value +let write_reg_field_bit regfield i reg_val bit = + let current_field_value = regfield.get_field reg_val in + let new_field_value = update_pos current_field_value i bit in + regfield.set_field reg_val new_field_value diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 9bc81b3e..44ae9d7c 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -245,6 +245,7 @@ let modulo (l,r) = hardware_mod l r let quot = hardware_quot let power (l,r) = integerPow l r +let add_int = add let sub_int = sub let mult_int = mult @@ -574,3 +575,16 @@ let make_bitvector_undef length = (* TODO *) val mask : forall 'a 'b. Size 'b => (integer * integer * bitvector 'a) -> bitvector 'b let mask (start, _, Bitvector w _ dir) = (Bitvector (zeroExtend w) start dir) + +(* Register operations *) + +let update_reg_range i j reg_val new_val = bvupdate reg_val i j new_val +let update_reg_bit i reg_val bit = bvupdate_pos reg_val i bit +let update_reg_field_range regfield i j reg_val new_val = + let current_field_value = regfield.get_field reg_val in + let new_field_value = bvupdate current_field_value i j new_val in + regfield.set_field reg_val new_field_value +let write_reg_field_bit regfield i reg_val bit = + let current_field_value = regfield.get_field reg_val in + let new_field_value = bvupdate_pos current_field_value i bit in + regfield.set_field reg_val new_field_value diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem index d5866cde..914955e0 100644 --- a/src/gen_lib/state.lem +++ b/src/gen_lib/state.lem @@ -1,7 +1,6 @@ open import Pervasives_extra open import Sail_impl_base open import Sail_values -open import Sail_operators_mwords (* 'a is result type *) @@ -51,7 +50,7 @@ let inline (>>) m n = m >>= fun _ -> n val exit : forall 'regs 'e 'a. 'e -> M 'regs 'a let exit _ s = [(Right (), s)] -val early_return : forall 'regs 'r. 'r -> MR 'regs unit 'r +val early_return : forall 'regs 'a 'r. 'r -> MR 'regs 'a 'r let early_return r s = [(Right (Just r), s)] val catch_early_return : forall 'regs 'a. MR 'regs 'a 'a -> M 'regs 'a @@ -76,12 +75,11 @@ let set_reg state reg v = <| state with regstate = reg.write_to state.regstate v |> -val read_mem : forall 'regs 'a 'b. Size 'b => bool -> read_kind -> bitvector 'a -> integer -> M 'regs (bitvector 'b) +val read_mem : forall 'regs 'a 'b. Size 'b => bool -> read_kind -> integer -> integer -> M 'regs (vector bitU) let read_mem dir read_kind addr sz state = - let addr = unsigned addr in let addrs = range addr (addr+sz-1) in let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in - let value = vec_to_bvec (Sail_values.internal_mem_value dir memory_value) in + let value = Sail_values.internal_mem_value dir memory_value in let is_exclusive = match read_kind with | Sail_impl_base.Read_plain -> false | Sail_impl_base.Read_reserve -> true @@ -98,9 +96,9 @@ let read_mem dir read_kind addr sz state = (* caps are aligned at 32 bytes *) let cap_alignment = (32 : integer) -val read_tag : forall 'regs 'a. bool -> read_kind -> bitvector 'a -> M 'regs bitU +val read_tag : forall 'regs 'a. bool -> read_kind -> integer -> M 'regs bitU let read_tag dir read_kind addr state = - let addr = (unsigned addr) / cap_alignment in + let addr = addr / cap_alignment in let tag = match (Map.lookup addr state.tagstate) with | Just t -> t | Nothing -> B0 @@ -125,18 +123,17 @@ let excl_result () state = (Left true, <| state with last_exclusive_operation_was_load = false |>) in (Left false, state) :: if state.last_exclusive_operation_was_load then [success] else [] -val write_mem_ea : forall 'regs 'a. write_kind -> bitvector 'a -> integer -> M 'regs unit +val write_mem_ea : forall 'regs 'a. write_kind -> integer -> integer -> M 'regs unit let write_mem_ea write_kind addr sz state = - let addr = unsigned addr in [(Left (), <| state with write_ea = Just (write_kind,addr,sz) |>)] -val write_mem_val : forall 'regs 'b. bitvector 'b -> M 'regs bool +val write_mem_val : forall 'regs 'b. vector bitU -> M 'regs bool let write_mem_val v state = let (write_kind,addr,sz) = match state.write_ea with | Nothing -> failwith "write ea has not been announced yet" | Just write_ea -> write_ea end in let addrs = range addr (addr+sz-1) in - let v = external_mem_value (bvec_to_vec v) in + let v = external_mem_value v in let addresses_with_value = List.zip addrs v in let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem) state.memstate addresses_with_value in @@ -178,28 +175,6 @@ let update_reg reg f v state = let current_value = get_reg state reg in let new_value = f current_value v in [(Left (), set_reg state reg new_value)] -let write_reg_range reg i j v state = - let current_value = get_reg state reg in - let new_value = bvupdate current_value i j v in - [(Left (), set_reg state reg new_value)] -let write_reg_bit reg i bit state = - let current_value = get_reg state reg in - let new_value = bvupdate_pos current_value i bit in - [(Left (), set_reg state reg new_value)] -let write_reg_field reg regfield = - update_reg reg regfield.set_field -let write_reg_field_range reg regfield i j = - let upd regval v = - let current_field_value = regfield.get_field regval in - let new_field_value = bvupdate current_field_value i j v in - regfield.set_field regval new_field_value in - update_reg reg upd -let write_reg_field_bit reg regfield i = - let upd regval v = - let current_field_value = regfield.get_field regval in - let new_field_value = bvupdate_pos current_field_value i v in - regfield.set_field regval new_field_value in - update_reg reg upd val barrier : forall 'regs. barrier_kind -> M 'regs unit -- cgit v1.2.3