From 4db4b9619318970a0228954f64a61123c4961910 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 9 Oct 2018 21:47:31 +0100
Subject: Monad refactoring in Lem shallow embedding

- Merge tag reading/writing outcomes into memory value reading/writing outcomes
- Add effective address to Write_mem; this duplicates information in the
  Write_ea outcome that should come before, but it makes the effective address
  more conveniently available in events and traces, and it allows the following
  simplification in the state monad:
- Remove write_ea field from state record; the effective address is now
  expected as a parameter to the write_memS function
- Remove last_exclusive_operation_was_load field from state record; this was
  used to keep track of exclusive loads, but this was a a relatively coarse
  approximation anyway, so it might make more sense to track this in
  (architecture-specific) Sail code.  Overall, the state record now simply
  contains the fields regstate, memstate, tagstate.
---
 src/gen_lib/sail2_state_monad.lem | 93 +++++++++++++++++----------------------
 1 file changed, 40 insertions(+), 53 deletions(-)

(limited to 'src/gen_lib/sail2_state_monad.lem')

diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 30b296cc..89b29fa5 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -11,17 +11,13 @@ type tagstate = map integer bitU
 type sequential_state 'regs =
   <| regstate : 'regs;
      memstate : memstate;
-     tagstate : tagstate;
-     write_ea : maybe (write_kind * integer * integer);
-     last_exclusive_operation_was_load : bool |>
+     tagstate : tagstate |>
 
 val init_state : forall 'regs. 'regs -> sequential_state 'regs
 let init_state regs =
   <| regstate = regs;
      memstate = Map.empty;
-     tagstate = Map.empty;
-     write_ea = Nothing;
-     last_exclusive_operation_was_load = false |>
+     tagstate = Map.empty |>
 
 type ex 'e =
   | Failure of string
@@ -124,66 +120,57 @@ let read_tagS addr =
   readS (fun s -> fromMaybe B0 (Map.lookup addr s.tagstate)))
 
 (* Read bytes from memory and return in little endian order *)
-val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte) 'e
-let read_mem_bytesS read_kind addr sz =
+val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte * bitU) 'e
+let read_mem_bytesS _ addr sz =
   maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
   let sz = integerFromNat sz in
   let addrs = index_list addr (addr+sz-1) 1 in
   let read_byte s addr = Map.lookup addr s.memstate in
-  readS (fun s -> just_list (List.map (read_byte s) addrs)) >>$= (function
-    | Just mem_val ->
-       updateS (fun s ->
-         if read_is_exclusive read_kind
-         then <| s with last_exclusive_operation_was_load = true |>
-         else s) >>$
-       returnS mem_val
-    | Nothing -> failS "read_memS"
+  let read_tag s addr = Map.findWithDefault addr B0 s.tagstate in
+  readS (fun s ->
+    (just_list (List.map (read_byte s) addrs),
+     List.foldl and_bit B1 (List.map (read_tag s) addrs))) >>$=
+  (function
+    | (Just mem_val, tag) -> returnS (mem_val, tag)
+    | _ -> failS "read_memS"
   end))
 
-val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e
+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 =
-  read_mem_bytesS rk a (nat_of_int sz) >>$= (fun bytes ->
-  maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)))
+  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)))
 
 val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
-let excl_resultS () =
-  readS (fun s -> s.last_exclusive_operation_was_load) >>$= (fun excl_load ->
-  updateS (fun s -> <| s with last_exclusive_operation_was_load = false |>) >>$
-  chooseS (if excl_load then {false; true} else {false}))
-
-val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> monadS 'regs unit 'e
-let write_mem_eaS write_kind addr sz =
+let excl_resultS =
+  (* TODO: This used to be more deterministic, checking a flag in the state
+     whether an exclusive load has occurred before.  However, this does not
+     seem very precise; it might be safer to overapproximate the possible
+     behaviours by always making a nondeterministic choice. *)
+  undefined_boolS
+
+(* Write little-endian list of bytes to given address *)
+val write_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
+let write_mem_bytesS _ addr sz v t =
   maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
   let sz = integerFromNat sz in
-  updateS (fun s -> <| s with write_ea = Just (write_kind, addr, sz) |>))
-
-(* Write little-endian list of bytes to previously announced address *)
-val write_mem_bytesS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e
-let write_mem_bytesS v =
-  readS (fun s -> s.write_ea) >>$= (function
-      | Nothing -> failS "write ea has not been announced yet"
-      | Just (_, addr, sz) ->
-         let addrs = index_list addr (addr+sz-1) 1 in
-         (*let v = external_mem_value (bits_of v) in*)
-         let a_v = List.zip addrs v in
-         let write_byte mem (addr, v) = Map.insert addr v mem in
-         updateS (fun s ->
-           <| s with memstate = List.foldl write_byte s.memstate a_v |>) >>$
-         returnS true
-    end)
-
-val write_mem_valS : forall 'regs 'e 'a. Bitvector 'a => 'a -> monadS 'regs bool 'e
-let write_mem_valS v = match mem_bytes_of_bits v with
-  | Just v -> write_mem_bytesS v
-  | Nothing -> failS "write_mem_val"
+  let addrs = index_list addr (addr+sz-1) 1 in
+  (*let v = external_mem_value (bits_of v) 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
+  updateS (fun s ->
+    <| s with memstate = List.foldl write_byte s.memstate a_v;
+              tagstate = List.foldl write_tag s.tagstate addrs |>) >>$
+  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
 
-val write_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> bitU -> monadS 'regs bool 'e
-let write_tagS addr t =
-   maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
-   updateS (fun s -> <| s with tagstate = Map.insert addr t s.tagstate |>) >>$
-   returnS true)
-
 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)
 
-- 
cgit v1.2.3


From 10cb6bf0b0c37ccf7ec1bc222ed0a694fd815843 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 23 Oct 2018 11:28:39 +0100
Subject: Add helper functions in Sail Lem library

Running traces, directly accessing memory state
---
 src/gen_lib/sail2_state_monad.lem | 37 ++++++++++++++++++++-----------------
 1 file changed, 20 insertions(+), 17 deletions(-)

(limited to 'src/gen_lib/sail2_state_monad.lem')

diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 89b29fa5..84ae86d8 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -120,20 +120,21 @@ let read_tagS addr =
   readS (fun s -> fromMaybe B0 (Map.lookup addr s.tagstate)))
 
 (* Read bytes from memory and return in little endian order *)
-val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte * bitU) 'e
-let read_mem_bytesS _ addr sz =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
+val get_mem_bytes : forall 'regs. integer -> 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 read_byte s addr = Map.lookup addr s.memstate in
   let read_tag s addr = Map.findWithDefault addr B0 s.tagstate in
-  readS (fun s ->
-    (just_list (List.map (read_byte s) addrs),
-     List.foldl and_bit B1 (List.map (read_tag s) addrs))) >>$=
-  (function
-    | (Just mem_val, tag) -> returnS (mem_val, tag)
-    | _ -> failS "read_memS"
-  end))
+  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
+let read_mem_bytesS _ addr sz =
+  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
+  readS (get_mem_bytes addr sz) >>$=
+  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 =
@@ -150,18 +151,20 @@ let excl_resultS =
   undefined_boolS
 
 (* Write little-endian list of bytes to given address *)
-val write_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
-let write_mem_bytesS _ addr sz v t =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
+val put_mem_bytes : forall 'regs. integer -> 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 v = external_mem_value (bits_of v) 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
-  updateS (fun s ->
-    <| s with memstate = List.foldl write_byte s.memstate a_v;
-              tagstate = List.foldl write_tag s.tagstate addrs |>) >>$
+  <| 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
+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)
 
 val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
-- 
cgit v1.2.3


From d733aa5c7409c645807589d268c0b80055bf671d Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 20 Nov 2018 18:32:37 +0000
Subject: Use nat instead of (list bitU) for addresses in monad outcomes

Removes some friction by back-and-forth conversion when handling events
---
 src/gen_lib/sail2_state_monad.lem | 38 ++++++++++++++++++--------------------
 1 file changed, 18 insertions(+), 20 deletions(-)

(limited to 'src/gen_lib/sail2_state_monad.lem')

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)
-- 
cgit v1.2.3


From 17334803f125e3b839fdb7a780989d8eba555555 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 29 Nov 2018 17:58:15 +0000
Subject: Add separate outcome/event for tagged memory loads

Lets one distinguish in a trace whether an instruction tried to read
tagged memory or just read data without caring about the tag;  this is
useful for formulating predicates on traces.
---
 src/gen_lib/sail2_state_monad.lem | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

(limited to 'src/gen_lib/sail2_state_monad.lem')

diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 6c1cd4bd..8626052f 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -129,18 +129,28 @@ let get_mem_bytes addr sz s =
     (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. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e
-let read_mem_bytesS _ addr sz =
+val read_tagged_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e
+let read_tagged_mem_bytesS _ addr sz =
   readS (get_mem_bytes addr sz) >>$=
   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 =
+val read_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte) 'e
+let read_mem_bytesS rk addr sz =
+  read_tagged_mem_bytesS rk addr sz >>$= (fun (bytes, _) ->
+  returnS bytes)
+
+val read_tagged_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e
+let read_tagged_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) ->
+  read_tagged_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))))
 
+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 =
+  read_tagged_memS rk a sz >>$= (fun (bytes, _) ->
+  returnS bytes)
+
 val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
 let excl_resultS =
   (* TODO: This used to be more deterministic, checking a flag in the state
-- 
cgit v1.2.3


From 747999f5c9f9234d04ef9e574a415a88e2bcb52b Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 30 Nov 2018 18:28:32 +0000
Subject: Rename Undefined outcome to Choose

It is used for nondeterministic choice, so Undefined might be
misleading.
---
 src/gen_lib/sail2_state_monad.lem | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'src/gen_lib/sail2_state_monad.lem')

diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 8626052f..b2a7bb31 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -47,8 +47,8 @@ let seqS m n = bindS m (fun (_ : unit) -> n)
 let inline (>>$=) = bindS
 let inline (>>$) = seqS
 
-val chooseS : forall 'regs 'a 'e. SetType 'a => set 'a -> monadS 'regs 'a 'e
-let chooseS xs s = Set.map (fun x -> (Value x, s)) xs
+val chooseS : forall 'regs 'a 'e. SetType 'a => list 'a -> monadS 'regs 'a 'e
+let chooseS xs s = Set.fromList (List.map (fun x -> (Value x, s)) xs)
 
 val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e
 let readS f = (fun s -> returnS (f s) s)
@@ -59,8 +59,9 @@ let updateS f = (fun s -> returnS () (f s))
 val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e
 let failS msg s = {(Ex (Failure msg), s)}
 
-val undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
-let undefined_boolS () = chooseS {false; true}
+val choose_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
+let choose_boolS () = chooseS [false; true]
+let undefined_boolS = choose_boolS
 
 val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
 let exitS () = failS "exit"
-- 
cgit v1.2.3


From b4495040178bc7552acc76c14de7151583456ee6 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 3 Dec 2018 12:42:32 +0000
Subject: Make names of memory r/w events more consistent

Use E_read_memt for reading tagged memory, as in sail2_impl_base.lem,
and rename E_write_mem to E_write_memt, since it always writes a tag.
---
 src/gen_lib/sail2_state_monad.lem | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'src/gen_lib/sail2_state_monad.lem')

diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index b2a7bb31..18e57b30 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -130,26 +130,26 @@ let get_mem_bytes addr sz s =
     (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_tagged_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e
-let read_tagged_mem_bytesS _ addr sz =
+val read_memt_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e
+let read_memt_bytesS _ addr sz =
   readS (get_mem_bytes addr sz) >>$=
   maybe_failS "read_memS"
 
 val read_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte) 'e
 let read_mem_bytesS rk addr sz =
-  read_tagged_mem_bytesS rk addr sz >>$= (fun (bytes, _) ->
+  read_memt_bytesS rk addr sz >>$= (fun (bytes, _) ->
   returnS bytes)
 
-val read_tagged_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e
-let read_tagged_memS rk a sz =
+val read_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e
+let read_memtS rk a sz =
   maybe_failS "nat_of_bv" (nat_of_bv a) >>$= (fun a ->
-  read_tagged_mem_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) ->
+  read_memt_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))))
 
 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 =
-  read_tagged_memS rk a sz >>$= (fun (bytes, _) ->
+  read_memtS rk a sz >>$= (fun (bytes, _) ->
   returnS bytes)
 
 val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
-- 
cgit v1.2.3


From df0e02bc0c8259962f25d4c175fa950391695ab6 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 3 Dec 2018 16:03:24 +0000
Subject: Add Write_mem event/outcome without tag

The inter-instruction semantics is responsible for correctly handling memory
writes without tags; the lifting to the state monad handles it as writing a
value with a zero tag bit.
---
 src/gen_lib/sail2_state_monad.lem | 23 +++++++++++++++--------
 1 file changed, 15 insertions(+), 8 deletions(-)

(limited to 'src/gen_lib/sail2_state_monad.lem')

diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 18e57b30..3042700c 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -162,27 +162,34 @@ let excl_resultS =
 
 (* Write little-endian list of bytes to given address *)
 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 put_mem_bytes addr sz v tag s =
   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
+  let write_tag mem addr = Map.insert addr tag 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. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
-let write_mem_bytesS _ addr sz v t =
+val write_memt_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
+let write_memt_bytesS _ addr sz v t =
   updateS (put_mem_bytes addr sz v t) >>$
   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 =
+val write_mem_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> monadS 'regs bool 'e
+let write_mem_bytesS wk addr sz v = write_memt_bytesS wk addr sz v B0
+
+val write_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> integer -> 'b -> bitU -> monadS 'regs bool 'e
+let write_memtS 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
+    | (Just addr, Just v) -> write_memt_bytesS wk addr (nat_of_int 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 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)
 
-- 
cgit v1.2.3