Use nat instead of (list bitU) for addresses in monad outcomes

Removes some friction by back-and-forth conversion when handling events

4 files changed, 44 insertions, 37 deletions

diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 5a6d2aef..ae1f2cd8 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -9,16 +9,17 @@ type address = list bitU
 type monad 'regval 'a 'e =
   | Done of 'a
   (* Read a number of bytes from memory, returned in little endian order,
-     together with a tag. *)
-  | Read_mem of read_kind * address * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e)
+     together with a tag.  The first nat specifies the address, the second
+     the number of bytes. *)
+  | Read_mem of read_kind * nat * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e)
   (* Tell the system a write is imminent, at the given address and with the
      given size. *)
-  | Write_ea of write_kind * address * nat * monad 'regval 'a 'e
+  | Write_ea of write_kind * nat * nat * monad 'regval 'a 'e
   (* Request the result of store-exclusive *)
   | Excl_res of (bool -> monad 'regval 'a 'e)
   (* Request to write a memory value of the given size together with a tag
      at the given address. *)
-  | Write_mem of write_kind * address * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e)
+  | Write_mem of write_kind * nat * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e)
   (* Tell the system to dynamically recalculate dependency footprint *)
   | Footprint of monad 'regval 'a 'e
   (* Request a memory barrier *)
@@ -37,9 +38,9 @@ type monad 'regval 'a 'e =
   | Exception of 'e
 
 type event 'regval =
-  | E_read_mem of read_kind * address * nat * (list memory_byte * bitU)
-  | E_write_mem of write_kind * address * nat * list memory_byte * bitU * bool
-  | E_write_ea of write_kind * address * nat
+  | E_read_mem of read_kind * nat * nat * (list memory_byte * bitU)
+  | E_write_mem of write_kind * nat * nat * list memory_byte * bitU * bool
+  | E_write_ea of write_kind * nat * nat
   | E_excl_res of bool
   | E_barrier of barrier_kind
   | E_footprint
@@ -136,7 +137,9 @@ end
 
 val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e
 let read_mem_bytes rk addr sz =
-  Read_mem rk (bits_of addr) (nat_of_int sz) return
+  bind
+    (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 * bitU) 'e
 let read_mem rk addr sz =
@@ -154,14 +157,19 @@ let excl_result () =
   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 = Write_ea wk (bits_of addr) (nat_of_int sz) (Done ())
+let write_mem_ea wk 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 -> bitU -> monad 'rv bool 'e
-let write_mem wk addr sz v tag = match mem_bytes_of_bits v with
-  | Just v -> Write_mem wk (bits_of addr) (nat_of_int sz) v tag return
-  | Nothing -> Fail "write_mem"
-end
+let write_mem wk addr sz v tag =
+  match (mem_bytes_of_bits v, nat_of_bv addr) with
+    | (Just v, Just addr) ->
+       Write_mem wk addr (nat_of_int sz) v tag return
+    | _ -> Fail "write_mem"
+  end
 
 val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
 let read_reg reg =
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index 314c562d..3cc396f2 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -28,12 +28,10 @@ let rec runTraceS ra t s =
   match t with
   | [] -> Just s
   | E_read_mem _ addr sz (v, tag) :: t' ->
-     Maybe.bind (unsigned addr) (fun addr ->
      Maybe.bind (get_mem_bytes addr sz s) (fun (v', tag') ->
-     if v' = v && tag' = tag then runTraceS ra t' s else Nothing))
+     if v' = v && tag' = tag then runTraceS ra t' s else Nothing)
   | E_write_mem _ addr sz v tag _ :: t' ->
-     Maybe.bind (unsigned addr) (fun addr ->
-     runTraceS ra t' (put_mem_bytes addr sz v tag s))
+     runTraceS ra t' (put_mem_bytes addr sz v tag s)
   | E_read_reg r v :: t' ->
      let (read_reg, _) = ra in
      Maybe.bind (read_reg r s.regstate) (fun v' ->
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 84ae86d8..6c1cd4bd 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -4,8 +4,8 @@ open import Sail2_values
 
 (* 'a is result type *)
 
-type memstate = map integer memory_byte
-type tagstate = map integer bitU
+type memstate = map nat memory_byte
+type tagstate = map nat bitU
 (* type regstate = map string (vector bitU) *)
 
 type sequential_state 'regs =
@@ -116,31 +116,30 @@ end
 
 val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e
 let read_tagS addr =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
+  maybe_failS "nat_of_bv" (nat_of_bv addr) >>$= (fun addr ->
   readS (fun s -> fromMaybe B0 (Map.lookup addr s.tagstate)))
 
 (* Read bytes from memory and return in little endian order *)
-val get_mem_bytes : forall 'regs. integer -> nat -> sequential_state 'regs -> maybe (list memory_byte * bitU)
+val get_mem_bytes : forall 'regs. nat -> nat -> sequential_state 'regs -> maybe (list memory_byte * bitU)
 let get_mem_bytes addr sz s =
-  let sz = integerFromNat sz in
-  let addrs = index_list addr (addr+sz-1) 1 in
+  let addrs = genlist (fun n -> addr + n) sz in
   let read_byte s addr = Map.lookup addr s.memstate in
   let read_tag s addr = Map.findWithDefault addr B0 s.tagstate in
   Maybe.map
     (fun mem_val -> (mem_val, List.foldl and_bit B1 (List.map (read_tag s) addrs)))
     (just_list (List.map (read_byte s) addrs))
 
-val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte * bitU) 'e
+val read_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e
 let read_mem_bytesS _ addr sz =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
   readS (get_mem_bytes addr sz) >>$=
-  maybe_failS "read_memS")
+  maybe_failS "read_memS"
 
 val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e
 let read_memS rk a sz =
+  maybe_failS "nat_of_bv" (nat_of_bv a) >>$= (fun a ->
   read_mem_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) ->
   maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val ->
-  returnS (mem_val, tag)))
+  returnS (mem_val, tag))))
 
 val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
 let excl_resultS =
@@ -151,28 +150,27 @@ let excl_resultS =
   undefined_boolS
 
 (* Write little-endian list of bytes to given address *)
-val put_mem_bytes : forall 'regs. integer -> nat -> list memory_byte -> bitU -> sequential_state 'regs -> sequential_state 'regs
+val put_mem_bytes : forall 'regs. nat -> nat -> list memory_byte -> bitU -> sequential_state 'regs -> sequential_state 'regs
 let put_mem_bytes addr sz v t s =
-  let sz = integerFromNat sz in
-  let addrs = index_list addr (addr+sz-1) 1 in
+  let addrs = genlist (fun n -> addr + n) sz in
   let a_v = List.zip addrs v in
   let write_byte mem (addr, v) = Map.insert addr v mem in
   let write_tag mem addr = Map.insert addr t mem in
   <| s with memstate = List.foldl write_byte s.memstate a_v;
             tagstate = List.foldl write_tag s.tagstate addrs |>
 
-val write_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
+val write_mem_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
 let write_mem_bytesS _ addr sz v t =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
   updateS (put_mem_bytes addr sz v t) >>$
-  returnS true)
+  returnS true
 
 val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
   write_kind -> 'a -> nat -> 'b -> bitU -> monadS 'regs bool 'e
-let write_memS wk addr sz v t = match mem_bytes_of_bits v with
-  | Just v -> write_mem_bytesS wk addr sz v t
-  | Nothing -> failS "write_mem"
-end
+let write_memS wk addr sz v t =
+  match (nat_of_bv addr, mem_bytes_of_bits v) with
+    | (Just addr, Just v) -> write_mem_bytesS wk addr sz v t
+    | _ -> failS "write_mem"
+  end
 
 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 8957f0dd..fa1e8426 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -625,6 +625,9 @@ let extz_bv n v = extz_bits n (bits_of v)
 val exts_bv : forall 'a. Bitvector 'a => integer -> 'a -> list bitU
 let exts_bv n v = exts_bits n (bits_of v)
 
+val nat_of_bv : forall 'a. Bitvector 'a => 'a -> maybe nat
+let nat_of_bv v = Maybe.map nat_of_int (unsigned v)
+
 val string_of_bv : forall 'a. Bitvector 'a => 'a -> string
 let string_of_bv v = show_bitlist (bits_of v)