From e8d6977d677d9eab570b993816fa3bd946d5142d Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 3 Jul 2017 15:12:17 +0100
Subject: Update to copytype and ccseal -- now use belt and braces approach
 when handling unsealed capabilities by clearing tag and setting cursor to -1.
 Also CCSeal got an encoding.

---
 cheri/cheri_insts.sail | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 76a76ea9..96127906 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -609,7 +609,7 @@ function clause execute (CCopyType(cd, cb, ct)) =
         writeCapReg(cd, cap);
       }
   } else
-    writeCapReg(cd, {cb_val with tag=false})
+    writeCapReg(cd, int_to_cap(-1))
   (* END_CCopyType *)
 }
 
@@ -703,7 +703,7 @@ function clause execute (CSeal(cd, cs, ct)) =
 }
 
 union ast member regregreg CCSeal
-(*function clause decode (0b010010 : 0b00010 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CCSeal(cd, cs, ct)) XXX no encoding yet *)
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) ct : 0b011111) = Some(CCSeal(cd, cs, ct))
 function clause execute (CCSeal(cd, cs, ct)) =
 {
   (* START_CCSeal *)
@@ -721,7 +721,7 @@ function clause execute (CCSeal(cd, cs, ct)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
   else if not (cs_val.tag) then
     raise_c2_exception(CapEx_TagViolation, cs)
-  else if not (ct_val.tag) then
+  else if (not (ct_val.tag)) | (getCapCursor(ct_val) == -1) then
     writeCapReg(cd, cs_val)
   else if (cs_val.sealed) then
     raise_c2_exception(CapEx_SealViolation, cs)
-- 
cgit v1.2.3