Merge branch 'master' of bitbucket.org:Peter_Sewell/sail

Conflicts:
	language/manual.pdf

5 files changed, 135 insertions, 90 deletions

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 525ff324..5882ec77 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -1,7 +1,7 @@
 (*========================================================================*)
 (*                                                                        *)
-(*  Copyright (c) 2015-2016 Robert M. Norton                              *)
-(*  Copyright (c) 2015-2016 Kathyrn Gray                                  *)
+(*  Copyright (c) 2015-2017 Robert M. Norton                              *)
+(*  Copyright (c) 2015-2017 Kathyrn Gray                                  *)
 (*  All rights reserved.                                                  *)
 (*                                                                        *)
 (*  This software was developed by the University of Cambridge Computer   *)
@@ -83,7 +83,7 @@ function clause execute (CGetBase(rd, cb)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     let capVal = readCapReg(cb) in
-    wGPR(rd) := getCapBase(capVal);
+    wGPR(rd) := (bit[64]) (getCapBase(capVal));
   (* END_CGetBase *)
 }
 
@@ -95,7 +95,7 @@ function clause execute (CGetOffset(rd, cb)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     let capVal = readCapReg(cb) in
-    wGPR(rd) := getCapOffset(capVal);
+    wGPR(rd) := (bit[64]) (getCapOffset(capVal));
   (* END_CGetOffset *)
 }
 
@@ -108,8 +108,7 @@ function clause execute (CGetLen(rd, cb)) =
   else
     let capVal = readCapReg(cb) in
     let len65  = getCapLength(capVal) in
-    let len64  = if unsigned(len65) > MAX_U64 then
-        (bit[64]) MAX_U64 else len65[63..0] in
+    let len64  = (bit[64]) (min(MAX_U64, len65)) in
     wGPR(rd) := len64;
   (* END_CGetLen *)
 }
@@ -249,7 +248,7 @@ function clause execute(CToPtr(rd, cb, ct)) =
       wGPR(rd) := if not (cb_val.tag) then
           ((bit[64]) 0)
         else
-          (bit[64])(getCapCursor(cb_val) - unsigned(getCapBase(ct_val)))
+          (bit[64])(getCapCursor(cb_val) - getCapBase(ct_val))
     }
   (* END_CToPtr *)
 }
@@ -383,8 +382,8 @@ function clause execute (CSetBounds(cd, cb, rt)) =
   cb_val := readCapReg(cb);
   rt_val := unsigned(rGPR(rt));
   cursor := getCapCursor(cb_val);
-  base   := unsigned(getCapBase(cb_val));
-  top    := unsigned(getCapTop(cb_val));
+  base   := getCapBase(cb_val);
+  top    := getCapTop(cb_val);
   newTop := cursor + rt_val;
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
@@ -414,8 +413,8 @@ function clause execute (CSetBoundsExact(cd, cb, rt)) =
   cb_val := readCapReg(cb);
   rt_val := unsigned(rGPR(rt));
   cursor := getCapCursor(cb_val);
-  base   := unsigned(getCapBase(cb_val));
-  top    := unsigned(getCapTop(cb_val));
+  base   := getCapBase(cb_val);
+  top    := getCapTop(cb_val);
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -564,7 +563,8 @@ function clause execute (CSeal(cd, cs, ct)) =
   cs_val := readCapReg(cs);
   ct_val := readCapReg(ct);
   ct_cursor := getCapCursor(ct_val);
-  ct_top    := unsigned(getCapTop(ct_val));
+  ct_top    := getCapTop(ct_val);
+  ct_base   := getCapBase(ct_val);
   if (register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cs)) then
@@ -581,6 +581,8 @@ function clause execute (CSeal(cd, cs, ct)) =
     raise_c2_exception(CapEx_SealViolation, ct)
   else if not (ct_val.permit_seal) then
     raise_c2_exception(CapEx_PermitSealViolation, ct)
+  else if (ct_cursor < ct_base) then
+    raise_c2_exception(CapEx_LengthViolation, ct)
   else if (ct_cursor >= ct_top) then
     raise_c2_exception(CapEx_LengthViolation, ct)
   else if (ct_cursor > max_otype) then
@@ -621,7 +623,9 @@ function clause execute (CUnseal(cd, cs, ct)) =
     raise_c2_exception(CapEx_TypeViolation, ct)
   else if not (ct_val.permit_seal) then
     raise_c2_exception(CapEx_PermitSealViolation, ct)
-  else if (ct_cursor >= unsigned(getCapTop(ct_val))) then
+  else if (ct_cursor <  getCapBase(ct_val)) then
+    raise_c2_exception(CapEx_LengthViolation, ct)
+  else if (ct_cursor >= getCapTop(ct_val)) then
     raise_c2_exception(CapEx_LengthViolation, ct)
   else
     writeCapReg(cd, {cs_val with 
@@ -641,6 +645,7 @@ function clause execute (CCall(cs, cb)) =
   checkCP2usable();
   cs_val := readCapReg(cs);
   cb_val := readCapReg(cb);
+  cs_cursor := getCapCursor(cs_val);
   if (register_inaccessible(cs)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
   else if (register_inaccessible(cb)) then
@@ -659,7 +664,9 @@ function clause execute (CCall(cs, cb)) =
     raise_c2_exception(CapEx_PermitExecuteViolation, cs)
   else if (cb_val.permit_execute) then
     raise_c2_exception(CapEx_PermitExecuteViolation, cb)
-  else if (getCapCursor(cs_val) >= unsigned(getCapTop(cs_val))) then
+  else if (cs_cursor < getCapBase(cs_val)) then
+    raise_c2_exception(CapEx_LengthViolation, cs)
+  else if (cs_cursor >= getCapTop(cs_val)) then
     raise_c2_exception(CapEx_LengthViolation, cs)
   else
     raise_c2_exception(CapEx_CallTrap, cs);
@@ -704,7 +711,8 @@ function clause execute(CJALR(cd, cb, link)) =
   checkCP2usable();
   cb_val := readCapReg(cb);
   cb_ptr := getCapCursor(cb_val);
-  cb_top := unsigned(getCapTop(cb_val));
+  cb_top := getCapTop(cb_val);
+  cb_base:= getCapBase(cb_val);
   if (link & register_inaccessible(cd)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
   else if (register_inaccessible(cb)) then
@@ -717,7 +725,9 @@ function clause execute(CJALR(cd, cb, link)) =
     raise_c2_exception(CapEx_PermitExecuteViolation, cb)
   else if not (cb_val.global) then
     raise_c2_exception(CapEx_GlobalViolation, cb)
-  else if (cb_ptr + 4 > cb_top) then
+  else if (cb_ptr < cb_base) then
+    raise_c2_exception(CapEx_LengthViolation, cb)
+  else if ((cb_ptr + 4) > cb_top) then
     raise_c2_exception(CapEx_LengthViolation, cb)
   else if ((cb_ptr mod 4) != 0) then
     SignalException(AdEL)
@@ -730,7 +740,7 @@ function clause execute(CJALR(cd, cb, link)) =
             writeCapReg(cd, linkCap)
         else
             assert(false, None);
-      delayedPC := getCapOffset(cb_val);
+      delayedPC :=  (bit[64]) (getCapOffset(cb_val));
       delayedPCC := capStructToCapReg(cb_val);
       branchPending := 1;
     }
@@ -773,9 +783,9 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
       cursor := getCapCursor(cb_val);
       vAddr  := cursor + unsigned(rGPR(rt)) + (size*signed(offset));
       vAddr64:= (bit[64]) vAddr;
-      if ((vAddr + size) > unsigned(getCapTop(cb_val))) then
+      if ((vAddr + size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
-      else if (vAddr < unsigned(getCapBase(cb_val))) then
+      else if (vAddr < getCapBase(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if not (isAddressAligned(vAddr64, width)) then
         SignalExceptionBadAddr(AdEL, vAddr64)
@@ -830,9 +840,9 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
       cursor := getCapCursor(cb_val);
       vAddr  := cursor + unsigned(rGPR(rt)) + (size * signed(offset));
       vAddr64:= (bit[64]) vAddr;
-      if ((vAddr + size) > unsigned(getCapTop(cb_val))) then
+      if ((vAddr + size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
-      else if (vAddr < unsigned(getCapBase(cb_val))) then
+      else if (vAddr < getCapBase(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if not (isAddressAligned(vAddr64, width)) then
         SignalExceptionBadAddr(AdES, vAddr64)
@@ -893,9 +903,9 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
       cursor := getCapCursor(cb_val);
       vAddr  := cursor + unsigned(rGPR(rt)) + (16 * signed(offset));
       vAddr64:= (bit[64]) vAddr;
-      if ((vAddr + cap_size) > unsigned(getCapTop(cb_val))) then
+      if ((vAddr + cap_size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
-      else if (vAddr < unsigned(getCapBase(cb_val))) then
+      else if (vAddr < getCapBase(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if ((vAddr mod cap_size) != 0) then
         SignalExceptionBadAddr(AdES, vAddr64)
@@ -942,9 +952,9 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
       cursor := getCapCursor(cb_val);
       vAddr  := cursor + unsigned(rGPR(rt)) + (16*signed(offset));
       vAddr64:= (bit[64]) vAddr;
-      if ((vAddr + cap_size) > unsigned(getCapTop(cb_val))) then
+      if ((vAddr + cap_size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
-      else if (vAddr < unsigned(getCapBase(cb_val))) then
+      else if (vAddr < getCapBase(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if ((vAddr mod cap_size) != 0) then
         SignalExceptionBadAddr(AdEL, vAddr64)
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index a96949a5..f97842a0 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -1,7 +1,7 @@
 (*========================================================================*)
 (*                                                                        *)
-(*  Copyright (c) 2015-2016 Robert M. Norton                              *)
-(*  Copyright (c) 2015-2016 Kathyrn Gray                                  *)
+(*  Copyright (c) 2015-2017 Robert M. Norton                              *)
+(*  Copyright (c) 2015-2017 Kathyrn Gray                                  *)
 (*  All rights reserved.                                                  *)
 (*                                                                        *)
 (*  This software was developed by the University of Cambridge Computer   *)
@@ -105,7 +105,7 @@ function CapStruct capRegToCapStruct((CapReg) c) =
     permit_execute         = c[114];
     global                 = c[113];
     reserved               = c[112..111];
-    E                      = c[110..105];
+    E                      = c[110..105] ^ 0b110000;
     sealed                 = s;
     B                      = B;
     T                      = T;
@@ -132,7 +132,7 @@ function (bit[128]) capStructToMemBits((CapStruct) cap) =
     ( cap.uperms
     : getCapHardPerms(cap)
     : cap.reserved
-    : cap.E
+    : (cap.E ^ 0b110000) (* XXX brackets required otherwise sail interpreter error *)
     : [cap.sealed]
     : b
     : t
@@ -155,7 +155,7 @@ function (bit[31]) getCapPerms((CapStruct) cap) =
 function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) =
     { cap with
       uperms                 = perms[18..15];
-(*      perm_reserved11_14     = (cap.perm_reserved11_14 & (perms[14..11]));*)
+      (* 14..11 reserved -- ignore *)
       access_system_regs     = perms[10];
       perm_reserved9         = perms[9];
       perm_reserved8         = perms[8];
@@ -175,51 +175,49 @@ function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) =
     else
         (false, undefined)
 
-function int a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) =
-    switch (a_mid < R, bound < R) {
-      case (False, False) -> 0
-      case (False, True)  -> 1
-      case (True, False)  -> -1
-      case (True, True)   -> 0
+function [|-1:1|] a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) =
+    switch (unsigned(a_mid) < unsigned(R), unsigned(bound) < unsigned(R)) {
+      case (bitzero, bitzero) -> 0
+      case (bitzero, bitone)  -> 1
+      case (bitone, bitzero)  -> -1
+      case (bitone, bitone)   -> 0
     }
 
-function bit[64] getCapBase((CapStruct) c)  = 
-    let ([|63|])  E = unsigned(c.E) in
-    let (bool)    s = c.sealed in
+function uint64 getCapBase((CapStruct) c)  = 
+    let ([|45|])  E = min(unsigned(c.E), 45) in
     let (bit[20]) B = c.B in
     let (bit[64]) a = c.address in
-    let (bit[20]) R = B - 0x00100 in (* wraps *)
+    let (bit[20]) R = B - 0x01000 in (* wraps *)
     let (bit[20]) a_mid = a[(E + 19)..E] in
-    let (int) correction = a_top_correction(a_mid, R, B) in
+    let correction = a_top_correction(a_mid, R, B) in
     let a_top = a[63..(E+20)] in
-    let (bit[64]) base = EXTZ((a_top + correction) : B) in
-    base << E
+    let (bit[64]) base = EXTZ((a_top + correction) : B) << E in
+    unsigned(base)
 
-function bit[65] getCapTop((CapStruct) c)  = 
-    let ([|63|])  E = unsigned(c.E) in
-    let (bool)    s = c.sealed in
+function CapLen getCapTop ((CapStruct) c)  = 
+    let ([|45|])  E = min(unsigned(c.E), 45) in
     let (bit[20]) B = c.B in
     let (bit[20]) T = c.T in
     let (bit[64]) a = c.address  in
-    let (bit[20]) R = B - 0x00100 in (* wraps *)
+    let (bit[20]) R = B - 0x01000 in (* wraps *)
     let (bit[20]) a_mid = a[(E + 19)..E] in
-    let (int) correction = a_top_correction(a_mid, R, T) in
+    let correction = a_top_correction(a_mid, R, T) in
     let a_top = a[63..(E+20)] in
     let (bit[65]) top1 = EXTZ((a_top + correction) : T) in
-    top1 << E
+    (CapLen) (top1 << E)
 
-function bit[64] getCapOffset((CapStruct) c) = 
+function uint64 getCapOffset((CapStruct) c) = 
     let base = getCapBase(c) in
-    c.address - base
+    unsigned(c.address) - base
 
-function bit[65] getCapLength((CapStruct) c)  = getCapTop(c) - (0b0 : getCapBase(c))
+function CapLen getCapLength((CapStruct) c)  = getCapTop(c) - getCapBase(c)
 
-function nat getCapCursor((CapStruct) cap) = unsigned(cap.address)
+function uint64 getCapCursor((CapStruct) cap) = unsigned(cap.address)
 
 function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) =
     let oldBase    = getCapBase(c) in
     let oldTop     = getCapTop(c) in
-    let (bit[64]) newAddress = oldBase + offset in
+    let (bit[64]) newAddress =  oldBase + offset in
     let newCap     = { c with address = newAddress } in
     let newBase    = getCapBase(newCap) in
     let newTop     = getCapTop(newCap) in
@@ -251,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
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index 8cb162f8..388d9ed7 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -1,7 +1,7 @@
 (*========================================================================*)
 (*                                                                        *)
-(*  Copyright (c) 2015-2016 Robert M. Norton                              *)
-(*  Copyright (c) 2015-2016 Kathyrn Gray                                  *)
+(*  Copyright (c) 2015-2017 Robert M. Norton                              *)
+(*  Copyright (c) 2015-2017 Kathyrn Gray                                  *)
 (*  All rights reserved.                                                  *)
 (*                                                                        *)
 (*  This software was developed by the University of Cambridge Computer   *)
@@ -183,12 +183,12 @@ function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) =
 function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) =
     (true, {cap with sealed=true; otype=otype})
 
-function bit[64] getCapBase((CapStruct) c)   = c.base
-function bit[65] getCapTop((CapStruct) c)    = (0b0 : c.base) + (0b0 : c.length)
-function bit[64] getCapOffset((CapStruct) c) = c.offset
-function bit[65] getCapLength((CapStruct) c) = EXTZ(c.length)
+function uint64 getCapBase((CapStruct) c)   = unsigned(c.base)
+function CapLen getCapTop((CapStruct) c)    = unsigned(c.base) + unsigned(c.length)
+function uint64 getCapOffset((CapStruct) c) = unsigned(c.offset)
+function CapLen getCapLength((CapStruct) c) = unsigned(c.length)
 
-function nat getCapCursor((CapStruct) cap) = 
+function uint64 getCapCursor((CapStruct) cap) = 
   (unsigned(cap.base) + unsigned(cap.offset)) mod (2 ** 64)
 
 function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) = 
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index 7530c9cc..e1356ceb 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -1,7 +1,7 @@
 (*========================================================================*)
 (*                                                                        *)
-(*  Copyright (c) 2015-2016 Robert M. Norton                              *)
-(*  Copyright (c) 2015-2016 Kathyrn Gray                                  *)
+(*  Copyright (c) 2015-2017 Robert M. Norton                              *)
+(*  Copyright (c) 2015-2017 Kathyrn Gray                                  *)
 (*  All rights reserved.                                                  *)
 (*                                                                        *)
 (*  This software was developed by the University of Cambridge Computer   *)
@@ -83,21 +83,6 @@ function (CapStruct) readCapReg((regno) n) =
 function unit writeCapReg((regno) n, (CapStruct) cap) =
   CapRegs[n] := capStructToCapReg(cap)
 
-(*
-function (CapStruct) readCapReg((regno) n) =
-function (CapReg) capStructToCapReg((CapStruct) cap) =
-function (CapReg) memBitsToCapBits((bool) tag, (bit[8*cap_size_t]) b)function unit writeCapReg((regno) n, (CapStruct) cap) =
-function bit[64] getCapBase((CapStruct) c)
-function bit[65] getCapTop((CapStruct) c)
-function bit[64] getCapOffset((CapStruct) c)
-function bit[65] getCapLength((CapStruct) c)  = getCapTop(c) - (0b0 : getCapBase(c))
-function nat getCapCursor((CapStruct) cap)
-function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset)
-function (bool, CapStruct) incCapOffset((CapStruct) c, (bit[64]) delta)
-function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top)
-function CapStruct int_to_cap ((bit[64]) offset)
-*)
-
 typedef CapEx = enumerate {
   CapEx_None; 
   CapEx_LengthViolation;
@@ -171,14 +156,19 @@ register CapCauseReg CapCause
 
 function forall Type 'o . 'o SignalException ((Exception) ex) = 
   {
+    let pc  = (bit[64]) PC in (* XXX Cast forces read of register. Sail bug? *)
     let pcc = capRegToCapStruct(PCC) in
-    let (success, epcc) = setCapOffset(pcc, PC) in
-    C31        := capStructToCapReg(epcc);
+    let (success, epcc) = setCapOffset(pcc, pc) in
+    if (success) then
+        C31 := capStructToCapReg(epcc)
+    else
+        C31 := capStructToCapReg(int_to_cap(getCapBase(pcc) + pc));
     (* XXX what if not success? *)
     nextPCC    := C29; (* KCC *)
     delayedPCC := C29; (* always write delayedPCC together whether PCC so 
                           that non-capability branches don't override PCC *)
-    SignalExceptionMIPS(ex, getCapBase(capRegToCapStruct(C29)));
+    let base = (bit[64]) (getCapBase(capRegToCapStruct(C29))) in
+    SignalExceptionMIPS(ex, base);
   }
 
 function unit ERETHook() =
@@ -307,8 +297,8 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy
     cursor := getCapCursor(cap);
     vAddr  := cursor + unsigned(addr);
     size   := wordWidthBytes(width);
-    base   := unsigned(getCapBase(cap));
-    top    := unsigned(getCapTop(cap));
+    base   := getCapBase(cap);
+    top    := getCapTop(cap);
     if ((vAddr + size) > top) then
       (raise_c2_exception(CapEx_LengthViolation, capno))
     else if (vAddr < (base)) then
@@ -320,8 +310,8 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy
 function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = {
   incrementCP0Count();
   let pcc = capRegToCapStruct(PCC) in
-  let base  = unsigned(getCapBase(pcc)) in
-  let top   = unsigned(getCapTop(pcc)) in
+  let base  = getCapBase(pcc) in
+  let top   = getCapTop(pcc) in
   let absPC = base + unsigned(vAddr) in
   if ((absPC mod 4)  != 0) then (* bad PC alignment *)
     (SignalExceptionBadAddr(AdEL, (bit[64]) absPC)) (* XXX absPC may be truncated *)
diff --git a/cheri/cheri_types.sail b/cheri/cheri_types.sail
new file mode 100644
index 00000000..53d05cb5
--- /dev/null
+++ b/cheri/cheri_types.sail
@@ -0,0 +1,38 @@
+(*========================================================================*)
+(*                                                                        *)
+(*  Copyright (c) 2015-2017 Robert M. Norton                              *)
+(*  Copyright (c) 2015-2017 Kathyrn Gray                                  *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(*========================================================================*)
+
+let (nat) max_otype = 0xffffff
+let have_cp2 = true
+typedef CapLen = [|0 : 2**65|]
+