3 files changed, 102 insertions, 20 deletions
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 991d3895..5a6d2aef 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -48,6 +48,8 @@ type event 'regval =
   | E_undefined of bool
   | E_print of string
 
+type trace 'regval = list (event 'regval)
+
 val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e
 let return a = Done a
 
@@ -218,6 +220,62 @@ let barrier bk = Barrier bk (Done ())
 val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e
 let footprint _ = Footprint (Done ())
 
+(* Event traces *)
+
+val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event 'regval -> maybe (monad 'regval 'a 'e)
+let emitEvent m e = match (e, m) with
+  | (E_read_mem rk a sz v, Read_mem rk' a' sz' k) ->
+     if rk' = rk && a' = a && sz' = sz then Just (k v) else Nothing
+  | (E_write_mem wk a sz v tag r, Write_mem wk' a' sz' v' tag' k) ->
+     if wk' = wk && a' = a && sz' = sz && v' = v && tag' = tag then Just (k r) else Nothing
+  | (E_read_reg r v, Read_reg r' k) ->
+     if r' = r then Just (k v) else Nothing
+  | (E_write_reg r v, Write_reg r' v' k) ->
+     if r' = r && v' = v then Just k else Nothing
+  | (E_write_ea wk a sz, Write_ea wk' a' sz' k) ->
+     if wk' = wk && a' = a && sz' = sz then Just k else Nothing
+  | (E_barrier bk, Barrier bk' k) ->
+     if bk' = bk then Just k else Nothing
+  | (E_print m, Print m' k) ->
+     if m' = m then Just k else Nothing
+  | (E_excl_res v, Excl_res k) -> Just (k v)
+  | (E_undefined v, Undefined k) -> Just (k v)
+  | (E_footprint, Footprint k) -> Just k
+  | _ -> Nothing
+end
+
+val runTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> maybe (monad 'regval 'a 'e)
+let rec runTrace t m = match t with
+  | [] -> Just m
+  | e :: t' -> Maybe.bind (emitEvent m e) (runTrace t')
+end
+
+val final : forall 'regval 'a 'e. monad 'regval 'a 'e -> bool
+let final = function
+  | Done _ -> true
+  | Fail _ -> true
+  | Exception _ -> true
+  | _ -> false
+end
+
+val hasTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
+let hasTrace t m = match runTrace t m with
+  | Just m -> final m
+  | Nothing -> false
+end
+
+val hasException : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
+let hasException t m = match runTrace t m with
+  | Just (Exception _) -> true
+  | _ -> false
+end
+
+val hasFailure : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
+let hasFailure t m = match runTrace t m with
+  | Just (Fail _) -> true
+  | _ -> false
+end
+
 (* Define a type synonym that also takes the register state as a type parameter,
    in order to make switching to the state monad without changing generated
    definitions easier, see also lib/hol/prompt_monad.lem. *)
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index 42e2c0f3..314c562d 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -5,10 +5,9 @@ open import Sail2_prompt
 open import Sail2_state_monad
 open import {isabelle} `Sail2_state_monad_lemmas`
 
-(* State monad wrapper around prompt monad *)
-
+(* Lifting from prompt monad to state monad *)
 val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
-let rec liftState ra s = match s with
+let rec liftState ra m = match m with
   | (Done a)                  -> returnS a
   | (Read_mem rk a sz k)      -> bindS (read_mem_bytesS rk a sz)      (fun v -> liftState ra (k v))
   | (Write_mem wk a sz v t k) -> bindS (write_mem_bytesS wk a sz v t) (fun v -> liftState ra (k v))
@@ -23,3 +22,25 @@ let rec liftState ra s = match s with
   | (Fail descr)              -> failS descr
   | (Exception e)             -> throwS e
 end
+
+val runTraceS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> trace 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
+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))
+  | 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))
+  | E_read_reg r v :: t' ->
+     let (read_reg, _) = ra in
+     Maybe.bind (read_reg r s.regstate) (fun v' ->
+     if v' = v then runTraceS ra t' s else Nothing)
+  | E_write_reg r v :: t' ->
+     let (_, write_reg) = ra in
+     Maybe.bind (write_reg r v s.regstate) (fun s' ->
+     runTraceS ra t' <| s with regstate = s' |>)
+  | _ :: t' -> runTraceS ra t' s
+end
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 =>