Merge branch 'sail2' into rmem_interpreter

1 files changed, 48 insertions, 18 deletions

diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index 039343e2..98a5390d 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -5,23 +5,53 @@ 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
-  | (Done a)             -> returnS a
-  | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
-  | (Read_tag t k)       -> bindS (read_tagS t)             (fun v -> liftState ra (k v))
-  | (Write_memv a k)     -> bindS (write_mem_bytesS a)      (fun v -> liftState ra (k v))
-  | (Write_tag a t k)    -> bindS (write_tagS a t)          (fun v -> liftState ra (k v))
-  | (Read_reg r k)       -> bindS (read_regvalS ra r)       (fun v -> liftState ra (k v))
-  | (Excl_res k)         -> bindS (excl_resultS ())         (fun v -> liftState ra (k v))
-  | (Undefined k)        -> bindS (undefined_boolS ())      (fun v -> liftState ra (k v))
-  | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz)    (liftState ra k)
-  | (Write_reg r v k)    -> seqS (write_regvalS ra r v)     (liftState ra k)
-  | (Footprint k)        -> liftState ra k
-  | (Barrier _ k)        -> liftState ra k
-  | (Print _ k)          -> liftState ra k (* TODO *)
-  | (Fail descr)         -> failS descr
-  | (Exception e)        -> throwS e
+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))
+  | (Read_memt rk a sz k)      -> bindS (read_memt_bytesS rk a sz)      (fun v -> liftState ra (k v))
+  | (Write_mem wk a sz v k)    -> bindS (write_mem_bytesS wk a sz v)    (fun v -> liftState ra (k v))
+  | (Write_memt wk a sz v t k) -> bindS (write_memt_bytesS wk a sz v t) (fun v -> liftState ra (k v))
+  | (Read_reg r k)             -> bindS (read_regvalS ra r)             (fun v -> liftState ra (k v))
+  | (Excl_res k)               -> bindS (excl_resultS ())               (fun v -> liftState ra (k v))
+  | (Choose _ k)               -> bindS (choose_boolS ())               (fun v -> liftState ra (k v))
+  | (Write_reg r v k)          -> seqS (write_regvalS ra r v)           (liftState ra k)
+  | (Write_ea _ _ _ k)         -> liftState ra k
+  | (Footprint k)              -> liftState ra k
+  | (Barrier _ k)              -> liftState ra k
+  | (Print _ k)                -> liftState ra k (* TODO *)
+  | (Fail descr)               -> failS descr
+  | (Exception e)              -> throwS e
+end
+
+val emitEventS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> event 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
+let emitEventS ra e s = match e with
+  | E_read_mem _ addr sz v ->
+     Maybe.bind (get_mem_bytes addr sz s) (fun (v', _) ->
+     if v' = v then Just s else Nothing)
+  | E_read_memt _ addr sz (v, tag) ->
+     Maybe.bind (get_mem_bytes addr sz s) (fun (v', tag') ->
+     if v' = v && tag' = tag then Just s else Nothing)
+  | E_write_mem _ addr sz v success ->
+     if success then Just (put_mem_bytes addr sz v B0 s) else Nothing
+  | E_write_memt _ addr sz v tag success ->
+     if success then Just (put_mem_bytes addr sz v tag s) else Nothing
+  | E_read_reg r v ->
+     let (read_reg, _) = ra in
+     Maybe.bind (read_reg r s.regstate) (fun v' ->
+     if v' = v then Just s else Nothing)
+  | E_write_reg r v ->
+     let (_, write_reg) = ra in
+     Maybe.bind (write_reg r v s.regstate) (fun rs' ->
+     Just <| s with regstate = rs' |>)
+  | _ -> Just s
 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 :: t' -> Maybe.bind (emitEventS ra e s) (runTraceS ra t')
+end
+
+declare {isabelle} termination_argument runTraceS = automatic