Make Lem export of CHERI(-256) typecheck

Note: The effect annotations of the execute function differ between CHERI and
MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the
initial declarations of ast, decode, and execute (with the right effects for
MIPS).

4 files changed, 100 insertions, 70 deletions

diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail
index 0a286070..101414f8 100644
--- a/cheri/cheri_insts.sail
+++ b/cheri/cheri_insts.sail
@@ -73,7 +73,7 @@ function clause execute (CGetType(rd, cb)) =
     let capVal = readCapReg(cb) in
     wGPR(rd) := if (capVal.sealed)
       then EXTZ(capVal.otype)
-      else -1
+      else (bitone ^^ 64)
   (* END_CGetType *)
 }
 
@@ -110,8 +110,9 @@ function clause execute (CGetLen(rd, cb)) =
   else
     let capVal = readCapReg(cb) in
     let len65  = getCapLength(capVal) in
-    let len64  = (if len65 > MAX_U64 then MAX_U64 else len65) in
-    wGPR(rd) := (bit[64]) len64;
+    wGPR(rd) := (if len65 > MAX_U64 then MAX_U64 else len65);
+    (*let (uint64) len64 = (if len65 > MAX_U64 then MAX_U64 else len65) in
+    wGPR(rd) := (bit[64]) len64;*)
   (* END_CGetLen *)
 }
 
@@ -123,7 +124,7 @@ function clause execute (CGetTag(rd, cb)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     let capVal = readCapReg(cb) in
-    wGPR(rd) := EXTZ(capVal.tag);
+    wGPR(rd) := EXTZ([capVal.tag]);
   (* END_CGetTag *)
 }
 
@@ -135,7 +136,7 @@ function clause execute (CGetSealed(rd, cb)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
   else
     let capVal = readCapReg(cb) in
-    wGPR(rd) := EXTZ(capVal.sealed);
+    wGPR(rd) := EXTZ([capVal.sealed]);
   (* END_CGetSealed *)
 }
 
@@ -150,7 +151,7 @@ function clause execute (CGetPCC(cd)) =
   else
     let pcc = (capRegToCapStruct(PCC)) in
     let (success, pcc2) = setCapOffset(pcc, PC) in
-    {assert (success, None); (* guaranteed to be in-bounds *)
+    {assert (success, ""); (* guaranteed to be in-bounds *)
     writeCapReg(cd, pcc2)};
   (* END_CGetPCC *)
 }
@@ -279,7 +280,7 @@ function clause execute(CSub(rd, cb, ct)) =
     raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
   else 
     {
-      wGPR(rd) := (bit[64])(getCapCursor(cb_val) - getCapCursor(ct_val))
+      wGPR(rd) := (bit[64])(to_svec(getCapCursor(cb_val) - getCapCursor(ct_val)))
     }
   (* END_CSub *)
 }
@@ -325,7 +326,7 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) =
           ltu     := (cursor1 < cursor2);
           lts     := (((bit[64])cursor1) <_s ((bit[64])cursor2));
         };
-      wGPR(rd) := EXTZ(switch (op) {
+      wGPR(rd) := EXTZ ((bool[1]) (switch (op) {
         case CEQ   -> [equal]
         case CNE   -> [not (equal)]
         case CLT   -> [lts]
@@ -334,7 +335,7 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) =
         case CLEU  -> [ltu | equal]
         case CEXEQ -> [cb_val == ct_val]
         case CNEXEQ -> [cb_val != ct_val]
-      })
+      }))
     }
   (* END_CPtrCmp *)
 }
@@ -574,8 +575,8 @@ function clause execute (CBuildCap(cd, cb, ct)) =
     let (representable, cd2) = setCapOffset(cd1, (bit[64]) ct_offset) in
     let cd3 = setCapPerms(cd2, ct_perms) in
     {
-      assert(exact, None);         (* base and top came from ct originally so will be exact *)
-      assert(representable, None); (* similarly offset should be representable XXX except for fastRepCheck *)
+      assert(exact, "");         (* base and top came from ct originally so will be exact *)
+      assert(representable, ""); (* similarly offset should be representable XXX except for fastRepCheck *)
       writeCapReg(cd, cd3);
     }
   (* END_CBuildCap *)
@@ -609,11 +610,11 @@ function clause execute (CCopyType(cd, cb, ct)) =
       raise_c2_exception(CapEx_LengthViolation, cb)
     else
       let (success, cap) = setCapOffset(cb_val, (bit[64]) (ct_otype - cb_base)) in {
-        assert(success, None); (* offset is in bounds so must succeed *)
+        assert(success, ""); (* offset is in bounds so must succeed *)
         writeCapReg(cd, cap);
       }
   } else
-    writeCapReg(cd, int_to_cap(-1))
+    writeCapReg(cd, int_to_cap(bitone ^^ 64))
   (* END_CCopyType *)
 }
 
@@ -624,7 +625,7 @@ function clause execute (CCheckPerm(cs, rt)) =
   (* START_CCheckPerm *)
   checkCP2usable();
   cs_val := readCapReg(cs);
-  cs_perms := EXTZ(getCapPerms(cs_val));
+  cs_perms := (bit[64]) (EXTZ(getCapPerms(cs_val)));
   rt_perms := rGPR(rt);
   if (register_inaccessible(cs)) then
     raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
@@ -725,7 +726,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)) | (getCapCursor(ct_val) == -1) then
+  else if (not (ct_val.tag)) | (getCapCursor(ct_val) == unsigned(bitone ^^ 64)) then
     writeCapReg(cd, cs_val)
   else if (cs_val.sealed) then
     raise_c2_exception(CapEx_SealViolation, cs)
@@ -939,7 +940,7 @@ function clause execute(CJALR(cd, cb, link)) =
         if (success) then
             writeCapReg(cd, linkCap)
         else
-            assert(false, None);
+            assert(false, "");
       delayedPC :=  (bit[64]) (getCapOffset(cb_val));
       delayedPCC := capStructToCapReg(cb_val);
       branchPending := 1;
@@ -982,7 +983,7 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
       size   := wordWidthBytes(width);
       cursor := getCapCursor(cb_val);
       vAddr  := cursor + unsigned(rGPR(rt)) + (size*signed(offset));
-      vAddr64:= (bit[64]) vAddr;
+      vAddr64:= (bit[64]) (to_svec(vAddr));
       if ((vAddr + size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if (vAddr < getCapBase(cb_val)) then
@@ -993,18 +994,23 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
         {
           pAddr      := (TLBTranslate(vAddr64, LoadData));
           widthBytes := wordWidthBytes(width);
-          memResult  := if (linked) then
+          (bit[64]) memResult := if (linked) then
               {
                 CP0LLBit  := 0b1;
                 CP0LLAddr := pAddr;
-                MEMr_reserve_wrapper(pAddr, widthBytes);
+                if widthBytes == 1 then extendLoad(MEMr_reserve_wrapper(pAddr, 1), signext)
+                else if widthBytes == 2 then extendLoad(MEMr_reserve_wrapper(pAddr, 2), signext)
+                else if widthBytes == 4 then extendLoad(MEMr_reserve_wrapper(pAddr, 4), signext)
+                else extendLoad(MEMr_reserve_wrapper(pAddr, 8), signext)
               }
             else
-              MEMr_wrapper(pAddr, widthBytes);
-          if (signext) then
-            wGPR(rd) := EXTS(memResult)
-          else
-            wGPR(rd) := EXTZ(memResult)
+              {
+                if widthBytes == 1 then extendLoad(MEMr_wrapper(pAddr, 1), signext)
+                else if widthBytes == 2 then extendLoad(MEMr_wrapper(pAddr, 2), signext)
+                else if widthBytes == 4 then extendLoad(MEMr_wrapper(pAddr, 4), signext)
+                else extendLoad(MEMr_wrapper(pAddr, 8), signext)
+              };
+          wGPR(rd) := memResult;
         }
     }
   (* END_CLoad *)
@@ -1039,7 +1045,7 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
       size   := wordWidthBytes(width);
       cursor := getCapCursor(cb_val);
       vAddr  := cursor + unsigned(rGPR(rt)) + (size * signed(offset));
-      vAddr64:= (bit[64]) vAddr;
+      vAddr64:= (bit[64]) (to_svec(vAddr));
       if ((vAddr + size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if (vAddr < getCapBase(cb_val)) then
@@ -1052,7 +1058,7 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
           rs_val := rGPR(rs);
           if (conditional) then
             {
-              success := if (CP0LLBit[0]) then
+              (bool) success := if (CP0LLBit[0]) then
                   switch(width)
                     {
                       case B -> MEMw_conditional_wrapper(pAddr, 1, rs_val[7..0])
@@ -1102,7 +1108,7 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) =
     {
       cursor := getCapCursor(cb_val);
       vAddr  := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset));
-      vAddr64:= (bit[64]) vAddr;
+      vAddr64:= (bit[64]) (to_svec(vAddr));
       if ((vAddr + cap_size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if (vAddr < getCapBase(cb_val)) then
@@ -1149,7 +1155,7 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
     {
       cursor := getCapCursor(cb_val);
       vAddr  := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset));
-      vAddr64:= (bit[64]) vAddr;
+      vAddr64:= (bit[64]) (to_svec(vAddr));
       if ((vAddr + cap_size) > getCapTop(cb_val)) then
         raise_c2_exception(CapEx_LengthViolation, cb)
       else if (vAddr < getCapBase(cb_val)) then
@@ -1159,17 +1165,18 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) =
       else
         {
           let (pAddr, suppressTag) = (TLBTranslateC(vAddr64, LoadData)) in
-          let (tag, mem) = (if (linked) 
-            then
-              {
-                CP0LLBit  := 0b1;
-                CP0LLAddr := pAddr;
-                MEMr_tagged_reserve(pAddr);
-              }
-            else 
-              (MEMr_tagged(pAddr)))
-          in
-          (CapRegs[cd]) := memBitsToCapBits(tag & (cb_val.permit_load_cap) & not (suppressTag), mem);
+          if (linked) then
+            {
+              CP0LLBit  := 0b1;
+              CP0LLAddr := pAddr;
+              let (tag, mem) = MEMr_tagged_reserve(pAddr) in
+              (CapRegs[cd]) := memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem);
+            }
+          else
+            {
+              let (tag, mem) = MEMr_tagged(pAddr) in
+              (CapRegs[cd]) := memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem);
+            }
         }
     }
   (* END_CLC *)
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
index 98b0a40c..f1f33a56 100644
--- a/cheri/cheri_prelude_128.sail
+++ b/cheri/cheri_prelude_128.sail
@@ -35,6 +35,14 @@
 (* 128 bit cap + tag *)
 typedef CapReg = bit[129]
 
+val cast bool -> bit effect pure cast_bool_bit
+val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec
+val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec
+function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v)
+val extern bool -> bool effect pure not
+
+typedef uint64 = range<0, (2** 64) - 1>
+
 typedef CapStruct = const struct {
   bool    tag;
   bit[4]  uperms;
@@ -85,9 +93,9 @@ def Nat cap_size_t  = 16 (* cap size in bytes *)
 let ([:cap_size_t:]) cap_size = 16
 
 function CapStruct capRegToCapStruct((CapReg) c) =
-  let (bool)    s = c[104] in
-  let (bit[20]) B = if s then c[103..96] : 0x000 else c[103..84] in
-  let (bit[20]) T = if s then c[83..76] : 0x000 else c[83..64] in
+  let (bool)    s  = c[104] in
+  let (bit[20]) Bc = if s then c[103..96] : 0x000 else c[103..84] in
+  let (bit[20]) Tc = if s then c[83..76] : 0x000 else c[83..64] in
   let (bit[24]) otype = if s then c[95..84] : c[75..64] else 0 in
   {
     tag                    = c[128];
@@ -106,8 +114,8 @@ function CapStruct capRegToCapStruct((CapReg) c) =
     reserved               = c[112..111];
     E                      = c[110..105] ^ 0b110000;
     sealed                 = s;
-    B                      = B;
-    T                      = T;
+    B                      = Bc;
+    T                      = Tc;
     otype                  = otype;
     address                = c[63..0];
   }
@@ -175,30 +183,30 @@ function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) =
         (false, cap (* was undefined but ocaml shallow embedding can't handle it *) )
 
 function [|-1:1|] a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) =
-    switch (a_mid <_u R, bound <_u R) {
-      case (bitzero, bitzero) -> 0
-      case (bitzero, bitone)  -> 1
-      case (bitone, bitzero)  -> -1
-      case (bitone, bitone)   -> 0
+    switch (a_mid < R, bound < R) {
+      case (false, false) -> 0
+      case (false, true)  -> 1
+      case (true, false)  -> -1
+      case (true, true)   -> 0
     }
 
 function uint64 getCapBase((CapStruct) c)  = 
     let ([|45|])  E = min(unsigned(c.E), 45) in
-    let (bit[20]) B = c.B in
+    let (bit[20]) Bc = c.B in
     let (bit[65]) a = EXTZ(c.address) in
-    let (bit[20]) R = B - 0x01000 in (* wraps *)
+    let (bit[20]) R = Bc - 0x01000 in (* wraps *)
     let (bit[20]) a_mid = a[(E + 19)..E] in
-    let correction = a_top_correction(a_mid, R, B) in
+    let correction = a_top_correction(a_mid, R, Bc) in
     let a_top = a >> (E+20) in
-    let (bit[64]) base = EXTZ((a_top + correction) : B) << E in
+    let (bit[64]) base = EXTZ((a_top + correction) : Bc) << E in
     unsigned(base)
 
 function CapLen getCapTop ((CapStruct) c)  = 
     let ([|45|])  E = min(unsigned(c.E), 45) in
-    let (bit[20]) B = c.B in
+    let (bit[20]) Bc = c.B in
     let (bit[20]) T = c.T in
     let (bit[65]) a = EXTZ(c.address)  in
-    let (bit[20]) R = B - 0x01000 in (* wraps *)
+    let (bit[20]) R = Bc - 0x01000 in (* wraps *)
     let (bit[20]) a_mid = a[(E + 19)..E] in
     let correction = a_top_correction(a_mid, R, T) in
     let a_top = a >> (E+20) in
@@ -283,10 +291,10 @@ function [|48|] computeE ((bit[65]) rlength) =
 function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top) =
     (* {cap with base=base; length=(bit[64]) length; offset=0} *)
     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]) Bc = 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=(bit[6]) e; B=B; T=T2} in
+    let newCap  = {cap with E=(bit[6]) e; B=Bc; 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 ee9a91ac..7cf3d69c 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -36,7 +36,10 @@
 typedef CapReg = bit[257]
 
 val cast bool -> bit effect pure cast_bool_bit
-val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_bool_vec
+val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec
+val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec
+function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v)
+val extern bool -> bool effect pure not
 
 typedef uint64 = range<0, (2** 64) - 1>
 
@@ -188,13 +191,13 @@ 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 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 bit[64] getCapBase((CapStruct) c)        = c.base
+function [|0:2**65 - 2|] getCapTop((CapStruct) c) = unsigned(c.base) + unsigned(c.length)
+function bit[64] getCapOffset((CapStruct) c)      = c.offset
+function CapLen  getCapLength((CapStruct) c)      = unsigned(c.length)
 
 function uint64 getCapCursor((CapStruct) cap) = 
-  (unsigned(cap.base) + unsigned(cap.offset)) mod (2 ** 64)
+  (unsigned(cap.base) + unsigned(cap.offset)) mod (pow2(64))
 
 function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) = 
     (true, {c with offset=offset})
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index dcb56d01..f5fcd095 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -32,6 +32,16 @@
 (*  SUCH DAMAGE.                                                          *)
 (*========================================================================*)
 
+
+scattered typedef ast = const union
+
+val ast -> unit effect {barr, eamem, escape, rmem, rmemt, rreg, undef, wmvt, wreg} execute
+scattered function unit execute
+
+val bit[32] -> option<ast> effect pure decode
+scattered function option<ast> decode
+
+
 register CapReg PCC
 register CapReg nextPCC
 register CapReg delayedPCC
@@ -74,7 +84,7 @@ let (vector <0, 32, inc, (register<CapReg>)>) CapRegs =
   C21, C22, C23, C24, C25, C26, C27, C28, C29, C30, C31
   ]
 
-let (nat) max_otype = 0xffffff
+let max_otype = MAX(24) (*0xffffff*)
 let have_cp2 = true
 
 function (CapStruct) readCapReg((regno) n) =
@@ -204,7 +214,7 @@ function bool pcc_access_system_regs () =
       (pcc.access_system_regs)
 
 function bool register_inaccessible((regno) r) = 
-  let is_sys_reg = switch(r) {
+  let (bool) is_sys_reg = switch(r) {
     case 0b11011 -> true
     case 0b11100 -> true
     case 0b11101 -> true
@@ -249,7 +259,8 @@ function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_
   MEMval_tag_conditional(addr, cap_size, tag, reverse_endianness(data));
 }
 
-function unit effect {wmem} MEMw_wrapper(addr, size, data) =
+val forall Nat 'n, 'n >= 1. (bit[64], [:'n:], bit[8 * 'n]) -> unit effect {wmvt, wreg, eamem} MEMw_wrapper
+function unit effect {wmvt, wreg, eamem} MEMw_wrapper(addr, size, data) =
   let ledata = reverse_endianness(data) in
   if (addr == 0x000000007f000000) then
   {
@@ -263,7 +274,8 @@ function unit effect {wmem} MEMw_wrapper(addr, size, data) =
     MEMval_tag(addr, size, false, ledata);
   }
 
-function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
+val forall Nat 'n, 'n >= 1. (bit[64], [:'n:], bit[8 * 'n]) -> bool effect {wmvt, eamem} MEMw_conditional_wrapper
+function bool effect {wmvt, eamem} MEMw_conditional_wrapper(addr, size, data) =
   {
     (* On cheri non-capability writes must clear the corresponding tag*)
     MEMea_conditional(addr, size);
@@ -293,7 +305,7 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy
     else if (vAddr < (base)) then
       (raise_c2_exception(CapEx_LengthViolation, capno))
     else
-      (bit[64]) vAddr; (* XXX vAddr not truncated because top <= 2^64 and size > 0 *)
+      (bit[64]) (to_vec(vAddr)); (* XXX vAddr not truncated because top <= 2^64 and size > 0 *)
   }
 
 function (bit[64]) TranslatePC ((bit[64]) vAddr) = {
@@ -311,7 +323,7 @@ function (bit[64]) TranslatePC ((bit[64]) vAddr) = {
 }
 
 function unit checkCP2usable () =
-  if not ((CP0Status.CU)[2]) then
+  if not ((norm_dec (CP0Status.CU))[2]) then
     {
       (CP0Cause.CE) := 0b10;
       (SignalException(CpU));