diff options
| author | Robert Norton | 2017-07-03 15:12:17 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-07-03 15:12:35 +0100 |
| commit | e8d6977d677d9eab570b993816fa3bd946d5142d (patch) | |
| tree | 0cd2a4cbdcc401608abe0ca6dde3e67f50754e2f /cheri | |
| parent | 522e9ae14eabd09bb3e7cc2fd20a8f75df9d5870 (diff) | |
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.
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/cheri_insts.sail | 6 |
1 files 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) |