Remove dependency of state.lem on bitvector operations

4 files changed, 69 insertions, 52 deletions

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
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 3d4f3083..4e6b6615 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -391,15 +391,16 @@ let doc_exp_lem, doc_let_lem =
                    underscore ^^
                    doc_id_lem id in
                  liftR ((prefix 2 1)
-                   (string "write_reg_field_range")
+                   (string "update_reg")
                    (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space^^
-                             field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
+                      parens (string "update_reg_field_range" ^/^ field_ref ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
             | _ ->
                liftR ((prefix 2 1)
-                 (string "write_reg_range")
-                 (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e)))
+                 (string "update_reg")
+                 (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+                   parens (string "update_reg_range" ^/^ expY e2 ^/^ expY e3) ^/^ expY e)))
            )
-        | LEXP_vector (le,e2) when is_bit_typ t ->
+        | LEXP_vector (le,e2) ->
            (match le with
             | LEXP_aux (LEXP_field ((LEXP_aux (_, lannot) as le),id), fannot) ->
                if is_bit_typ (typ_of_annot fannot) then
@@ -410,12 +411,14 @@ let doc_exp_lem, doc_let_lem =
                    underscore ^^
                    doc_id_lem id in
                  liftR ((prefix 2 1)
-                   (string "write_reg_field_bit")
-                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ field_ref ^/^ expY e2 ^/^ expY e)))
+                   (string "update_reg")
+                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+                     parens (string "update_reg_field_bit" ^/^ field_ref ^/^ expY e2) ^/^ expY e)))
             | _ ->
                liftR ((prefix 2 1)
-                 (string "write_reg_bit")
-                 (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e))
+                 (string "update_reg")
+                 (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+                   parens (string "update_reg_bit" ^/^ expY e2) ^/^ expY e))
            )
         (* | LEXP_field (le,id) when is_bit_typ t ->
            liftR ((prefix 2 1)
@@ -425,9 +428,11 @@ let doc_exp_lem, doc_let_lem =
           let field_ref =
             doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^
             underscore ^^
-            doc_id_lem id in
+            doc_id_lem id ^^
+            dot ^^
+            string "set_field" in
            liftR ((prefix 2 1)
-             (string "write_reg_field")
+             (string "update_reg")
              (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
                 field_ref ^/^ expY e))
         (* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info ->
@@ -801,21 +806,26 @@ let doc_exp_lem, doc_let_lem =
        if aexp_needed then parens (align bepp) else bepp
     | E_vector_update(v,e1,e2) ->
        let t = typ_of full_exp in
+       let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
+       let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
        let call =
          if is_bitvector_typ t (*&& mwords*)
-         then "bitvector_update_pos"
-         else "update_pos" in
-       let epp = separate space [string call;expY v;expY e1;expY e2] in
+         then "bitvector_update_pos" ^ ord_suffix
+         else "update_pos" ^ ord_suffix in
+       let epp = string call ^^ space ^^ parens (separate comma_sp [expY v;expY e1;expY e2]) in
        if aexp_needed then parens (align epp) else epp
     | E_vector_update_subrange(v,e1,e2,e3) ->
        let t = typ_of full_exp in
+       let (_, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
+       let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
        let call =
          if is_bitvector_typ t (*&& mwords*)
-         then "bitvector_update"
-         else "update" in
-       let epp = align (string call ^//^
-                          group (group (expY v) ^/^ group (expY e1) ^/^ group (expY e2)) ^/^
-                            group (expY e3)) in
+         then "bitvector_update" ^ ord_suffix
+         else "update" ^ ord_suffix in
+       let epp =
+         align (string call ^//^
+           parens (separate comma_sp
+             [group (expY v); group (expY e1); group (expY e2); group (expY e3)])) in
        if aexp_needed then parens (align epp) else epp
     | E_list exps ->
        brackets (separate_map semi (expN) exps)