diff options
| author | Thomas Bauereiss | 2017-05-10 11:56:41 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-05-10 11:56:41 +0100 |
| commit | f36a9ca1de995bfecfb3c42f111a8ab020f88858 (patch) | |
| tree | c144c8761d1638dd4a4ba3abce75ec3978052edb /mips/mips_extras_embed.lem | |
| parent | 0bfa7cb591faf5e09aca2ebe87c8c0c30044bfa1 (diff) | |
Add stubs for TAGw
Tagged memory seems to be currently missing in the Lem shallow embedding of
(CHERI-)MIPS.
Diffstat (limited to 'mips/mips_extras_embed.lem')
| -rw-r--r-- | mips/mips_extras_embed.lem | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/mips/mips_extras_embed.lem b/mips/mips_extras_embed.lem index 12f2ca5a..31be4db0 100644 --- a/mips/mips_extras_embed.lem +++ b/mips/mips_extras_embed.lem @@ -1,4 +1,5 @@ open import Pervasives +open import Pervasives_extra open import Sail_impl_base open import Sail_values open import Prompt @@ -35,6 +36,9 @@ let MEMval_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b t let MEMval_tag (_,_,v) = write_mem_val v >>= fun _ -> return () let MEMval_tag_conditional (_,_,v) = write_mem_val v >>= fun b -> return (if b then B1 else B0) +(* TODO *) +val TAGw : (vector bitU * vector bitU) -> M unit +let TAGw (addr, tag) = failwith "TAGw not implemented" val MEM_sync : unit -> M unit |