From 7b77332c6d0f1f904adf5c6f5621dde0355f2d02 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Tue, 31 Jan 2017 12:38:06 +0000
Subject: Round up to multiple of 4 when computing E (CHERI does this to
 improve frequency).

---
 cheri/cheri_prelude_128.sail | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

(limited to 'cheri')

diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index 7d4eb77e..e6355717 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -249,20 +249,29 @@ function forall Nat 'N. option<[|0:('N + -1)|]> HighestSetBit((bit['N]) x) = {
   if break then Some(result) else None;
 }}
 
-function (bit[6]) computeE ((bit[65]) rlength) =
+(* hw rounds up E to multiple of 4 *)
+function ([|48|]) roundUp(([|45|]) e) =
+    let r = e mod 4 in
+    if (r == 0)
+    then e
+    else (e - r + 4)
+
+
+function ([|48|]) computeE ((bit[65]) rlength) =
     let msb = HighestSetBit((rlength + (rlength >> 6)) >> 19) in
     switch (msb) {
-      case (Some(b)) -> (bit[6]) b (* hw rounds up to multiple of 4 *)
+      (* above will always return <= 45 because 19 bits of zero are shifted in from right *)
+      case (Some(b)) -> {assert(b <= 45, None); roundUp (min(b,45)) }
       case None    -> 0
-    }    
+      }
 
 function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top) =
     (* {cap with base=base; length=(bit[64]) length; offset=0} *)
-    let (bit[6])  e = computeE(top - (0b0 : base)) in
+    let ([|48|])  e = computeE(top - (0b0 : base)) in
     let (bit[20]) B = base[(19+e)..e] in
     let (bit[20]) T = top[(19+e)..e] in
     let (bit[20]) T2 = T + if (top[(e - 1)..0] == 0) then 0 else 1 in
-    let newCap  = {cap with E=e; B=B; T=T2} in
+    let newCap  = {cap with E=(bit[6]) e; B=B; T=T2} in
     let newBase = getCapBase(newCap) in
     let newTop  = getCapTop(newCap) in
     let exact   = (base == newBase) & (top == newTop) in
-- 
cgit v1.2.3