From f36a9ca1de995bfecfb3c42f111a8ab020f88858 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 10 May 2017 11:56:41 +0100
Subject: Add stubs for TAGw

Tagged memory seems to be currently missing in the Lem shallow embedding of
(CHERI-)MIPS.
---
 mips/mips_extras_embed.lem            | 4 ++++
 mips/mips_extras_embed_sequential.lem | 4 ++++
 2 files changed, 8 insertions(+)

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
 
-- 
cgit v1.2.3