Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into mono-experiments

4 files changed, 46 insertions, 33 deletions

diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 3919d540..a760fb42 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
@@ -203,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
 
@@ -450,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 (<)
@@ -529,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 8f44b2b5..f10ed9f7 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
@@ -243,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
 
@@ -572,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/sail_values.lem b/src/gen_lib/sail_values.lem
index b7b87b97..4d3ddbce 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
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 879b092f..0ea65551 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