diff options
Diffstat (limited to 'src/gen_lib/sail2_state_lifting.lem')
| -rw-r--r-- | src/gen_lib/sail2_state_lifting.lem | 36 |
1 files changed, 20 insertions, 16 deletions
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem index 0e7addbb..07a6215b 100644 --- a/src/gen_lib/sail2_state_lifting.lem +++ b/src/gen_lib/sail2_state_lifting.lem @@ -8,28 +8,32 @@ open import {isabelle} `Sail2_state_monad_lemmas` (* 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 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)) - | (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_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 + | (Done a) -> returnS a + | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v)) + | (Read_tagged_mem rk a sz k) -> bindS (read_tagged_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)) + | (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_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, tag) -> + | 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_tagged_mem _ 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 tag _ -> - Just (put_mem_bytes addr sz v tag s) + | E_write_mem _ 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' -> |