diff options
| author | Robert Norton | 2016-06-07 14:06:09 +0100 |
|---|---|---|
| committer | Robert Norton | 2016-06-07 14:08:57 +0100 |
| commit | 486ede4166e118af24b783d1efd0a667ada3b54a (patch) | |
| tree | 40d0bdea6802d4848e9e5cc8e92d13a3f388e02e /cheri | |
| parent | a0bd975bd9e12cc0434bce918c6cbd555c9f55b5 (diff) | |
Preserve padding in capability registers when converting to struct form -- this is required for copying data via (untagged) capabilities.
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/cheri_prelude.sail | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/cheri/cheri_prelude.sail b/cheri/cheri_prelude.sail index ac0e1b85..f9b33f35 100644 --- a/cheri/cheri_prelude.sail +++ b/cheri/cheri_prelude.sail @@ -103,6 +103,7 @@ let (vector <0, 32, inc, (CapReg)>) CapRegs = typedef CapStruct = const struct { bool tag; + bit[8] padding; bit[24] otype; bit[16] sw_perms; bool access_KR2C; @@ -128,6 +129,7 @@ typedef CapStruct = const struct { let (CapStruct) null_cap = { tag = false; + padding = 0; otype = 0; sw_perms = 0; access_KR2C = false; @@ -158,6 +160,7 @@ let have_cp2 = true function CapStruct capRegToCapStruct((CapReg) capReg) = { tag = capReg.tag; + padding = capReg[255..248]; otype = capReg.otype; sw_perms = capReg.sw_perms; access_KR2C = capReg.access_KR2C; @@ -208,7 +211,7 @@ function (bit[31]) capPermsToVec((CapStruct) cap) = function (bit[257]) capStructToBit257((CapStruct) cap) = ( [cap.tag] - : 0b00000000 (* padding *) + : cap.padding : cap.otype : capPermsToVec(cap) : [cap.sealed] |