replace bit vector return types in getCapX functions with equivalent integer range types. This removes quite a few uses of unsigned() in cheri intsruction pseudocode. Could potentially take things furter.

6 files changed, 94 insertions, 71 deletions

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 7d51d860..5882ec77 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -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,8 +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_base   := unsigned(getCapBase(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
@@ -624,9 +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(getCapBase(ct_val))) then
+  else if (ct_cursor <  getCapBase(ct_val)) then
     raise_c2_exception(CapEx_LengthViolation, ct)
-  else if (ct_cursor >= unsigned(getCapTop(ct_val))) then
+  else if (ct_cursor >= getCapTop(ct_val)) then
     raise_c2_exception(CapEx_LengthViolation, ct)
   else
     writeCapReg(cd, {cs_val with 
@@ -665,9 +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 (cs_cursor < unsigned(getCapBase(cs_val))) then
+  else if (cs_cursor < getCapBase(cs_val)) then
     raise_c2_exception(CapEx_LengthViolation, cs)
-  else if (cs_cursor >= unsigned(getCapTop(cs_val))) then
+  else if (cs_cursor >= getCapTop(cs_val)) then
     raise_c2_exception(CapEx_LengthViolation, cs)
   else
     raise_c2_exception(CapEx_CallTrap, cs);
@@ -712,8 +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_base:= unsigned(getCapBase(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
@@ -741,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;
     }
@@ -784,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)
@@ -841,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)
@@ -904,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)
@@ -953,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 7f413ec4..f97842a0 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -175,7 +175,7 @@ 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) =
+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
@@ -183,41 +183,41 @@ function int a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) =
       case (bitone, bitone)   -> 0
     }
 
-function bit[64] getCapBase((CapStruct) c)  = 
-    let ([|63|])  E = min(unsigned(c.E), 45) 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 - 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 = min(unsigned(c.E), 45) 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 - 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
@@ -250,14 +250,14 @@ function forall Nat 'N. option<[|0:('N + -1)|]> HighestSetBit((bit['N]) x) = {
 }}
 
 (* hw rounds up E to multiple of 4 *)
-function ([|48|]) roundUp(([|45|]) e) =
+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) =
+function [|48|] computeE ((bit[65]) rlength) =
     let msb = HighestSetBit((rlength + (rlength >> 6)) >> 19) in
     switch (msb) {
       (* above will always return <= 45 because 19 bits of zero are shifted in from right *)
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index 1ddc5764..388d9ed7 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -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 a3e08809..e1356ceb 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -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;
@@ -182,7 +167,8 @@ function forall Type 'o . 'o SignalException ((Exception) ex) =
     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() =
@@ -311,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
@@ -324,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..5df42a9f
--- /dev/null
+++ b/cheri/cheri_types.sail
@@ -0,0 +1,38 @@
+(*========================================================================*)
+(*                                                                        *)
+(*  Copyright (c) 2015-2016 Robert M. Norton                              *)
+(*  Copyright (c) 2015-2016 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|]
+
diff --git a/src/Makefile b/src/Makefile
index a199522c..9b8b727d 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -81,10 +81,10 @@ MIPS_NOTLB_SAILS:=$(MIPS_NOTLB_SAILS_PRE) $(BITBUCKET_ROOT)/sail/etc/regfp.sail
 
 CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri
 
-CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
-CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
-CHERI128_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+CHERI128_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail  $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
 elf:
 	make -C $(ELFDIR)