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 | |
| parent | 0bfa7cb591faf5e09aca2ebe87c8c0c30044bfa1 (diff) | |
Add stubs for TAGw
Tagged memory seems to be currently missing in the Lem shallow embedding of
(CHERI-)MIPS.
| -rw-r--r-- | mips/mips_extras_embed.lem | 4 | ||||
| -rw-r--r-- | mips/mips_extras_embed_sequential.lem | 4 |
2 files changed, 8 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 diff --git a/mips/mips_extras_embed_sequential.lem b/mips/mips_extras_embed_sequential.lem index 9aeb9487..bee8e972 100644 --- a/mips/mips_extras_embed_sequential.lem +++ b/mips/mips_extras_embed_sequential.lem @@ -1,4 +1,5 @@ open import Pervasives +open import Pervasives_extra open import Sail_impl_base open import Sail_values open import State @@ -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 |