New algorithm for bounds calculation and changes to cap encoding

archdoc/chap-isaref-riscv.tex

@@ -120,7 +120,7 @@ \section{Constant Definitions}
 \sailRISCVtype{cap\_cE\_width}
 \sailRISCVtype{cap\_max\_E}
 \sailRISCVtypecapSizze{}
-\sailRISCVtypecapMantissaWidth{}
+\sailRISCVtypecapBWidth{}
 \sailRISCVtype{cap\_perms\_width}
 \sailRISCVtype{cap\_cperms\_width}
 \sailRISCVtype{cap\_otype\_width}

properties/props.sail

@@ -31,22 +31,6 @@ function encodeDecode(c : Capability) -> Capability =  capBitsToCapability(c.tag
  */
 function capEncodable(c : Capability) -> bool = c == encodeDecode(c)
 
-// $property
-/*
- * THIS is not actually an invariant but is useful for characterising unusable
- * encodings. Ideally we'd like an encoding that ensures base is less than or
- * equal to top, but sadly this isn't true. Counterexamples are unusable
- * encodings. This can happen when a_top ends up being zero and T < B because
- * the attempted corrections can underflow a_top. There are other unusable
- * encodings too, for example those with top larger than 2**32.
- */
-function prop_base_lteq_top(b : CapBits) -> bool = {
-    let c = capBitsToCapability(false, b);
-    let (base, top) = getCapBoundsBits(c);
-    a_top = c.address >> (unsigned(c.E) + cap_mantissa_width);
-    (a_top != zeros() | (c.B <_u c.T)) --> ((0b0 @ base) <=_u top)
-}
-
 $property
 /*!
  * Check that null_cap as defined in the Sail encodes to all zeros.
@@ -81,24 +65,6 @@ function prop_decEnc(t : bool, c : CapBits) -> bool  = {
     (c == b) & (cap.tag == t)
 }
 
-// $counterexample
-/*!
- * THIS property attempts to prove that it is possible to recover T and B bits
- * from the decoded base and top. This would be important in an implementation
- * that decodes fully on load and recompresses on store. It fails when E is
- * cap_max_E because base is only 32-bits and we lose the top bit of B, but I
- * think it would hold if getCapBoundsBits returned a 33-bit base.
- */
-function prop_decEnc2(c : CapBits) -> bool  = {
-    let cap = capBitsToCapability(false, c);
-    let (base, top) = getCapBoundsBits(cap);
-    let newB = truncate(base >> unsigned(cap.E), cap_mantissa_width);
-    let newT = truncate(top >> unsigned(cap.E), cap_mantissa_width);
-    let cap2 = {cap with B=newB, T=newT};
-    let c2 = capToBits(cap2);
-    (c == c2)
-}
-
 $property
 /*!
  * THIS checks that for any capability and permissions mask [CAndPerm]
@@ -128,7 +94,7 @@ $property
 function prop_setbounds(reqBase : CapAddrBits, reqLen : CapAddrBits) -> bool = {
     let (exact, c) = setCapBounds(root_cap_mem, reqBase, reqLen);
     let encodable = capEncodable(c);
-    let (b2, t2) = getCapBoundsBits(c);
+    let (b2, l2, t2) = getCapBoundsBits(c);
     let reqTop = (0b0 @ reqBase) + (0b0 @ reqLen);
     let saneTop = reqTop <=_u 0b1@0x00000000;
     saneTop --> (
@@ -155,13 +121,13 @@ function prop_setbounds_monotonic(
         reqBase1 : CapAddrBits, reqLen1 : CapAddrBits,
         reqBase2 : CapAddrBits, reqLen2 : CapAddrBits) -> bool = {
     let (exact1, c1) = setCapBounds(root_cap_mem, reqBase1, reqLen1);
-    let (b1, t1) = getCapBoundsBits(c1);
+    let (b1, l1, t1) = getCapBoundsBits(c1);
     let reqTop1 = (0b0 @ reqBase1) + (0b0 @ reqLen1);
     let saneTop1 = reqTop1 <=_u 0b1@0x00000000;
     let reqTop2 = (0b0 @ reqBase2) + (0b0 @ reqLen2);
     let saneTop2 = reqTop2 <=_u 0b1@0x00000000;
     let (exact2, c2) = setCapBounds(c1, reqBase2, reqLen2);
-    let (b2, t2) = getCapBoundsBits(c2);
+    let (b2, l2, t2) = getCapBoundsBits(c2);
     let requestMonotonic = (b1 <=_u reqBase2) & (reqTop2 <=_u t1);
     let resultMonotonic = (b1 <=_u b2) & (t2 <=_u t1);
     (saneTop1 & saneTop2 & requestMonotonic) --> resultMonotonic
@@ -176,10 +142,10 @@ $property
 function prop_setbounds_precise(reqBase1 : CapAddrBits, reqLen1 : CapAddrBits,
         c2 : CapBits) -> bool = {
     let (exact, c1) = setCapBounds(root_cap_mem, reqBase1, reqLen1);
-    let (b1, t1) = getCapBoundsBits(c1);
+    let (b1, l1, t1) = getCapBoundsBits(c1);
     let reqTop1 = (0b0 @ reqBase1) + (0b0 @ reqLen1);
     let saneTop1 = reqTop1 <=_u 0b1@0x00000000;
-    let (b2, t2) = getCapBoundsBits(capBitsToCapability(false, c2));
+    let (b2, l2, t2) = getCapBoundsBits(capBitsToCapability(false, c2));
     let validBase = b2 <=_u reqBase1;
     let betterBase = b1 <_u b2;
     let validTop = reqTop1 <=_u t2;
@@ -211,7 +177,7 @@ function prop_repbounds_c(reqBase : CapAddrBits, reqLen : CapAddrBits, newAddr :
     let (exact, c) = setCapBounds(root_cap_mem, reqBase, reqLen);
     let reqTop = (0b0 @ reqBase) + (0b0 @ reqLen);
     let saneTop = reqTop <=_u 0b1@0x00000000;
-    let (b, t) = getCapBoundsBits(c);
+    let (b, l, t) = getCapBoundsBits(c);
     let (representable, newCap) = setCapAddr(c, newAddr);
     let inCBounds = (b <=_u newAddr) & ((0b0 @ newAddr) <=_u t);
     (saneTop & inCBounds) --> representable
@@ -226,7 +192,7 @@ function prop_repbounds(reqBase : CapAddrBits, reqLen : CapAddrBits, newAddr : C
     let (exact, c) = setCapBounds(root_cap_mem, reqBase, reqLen);
     let reqTop = (0b0 @ reqBase) + (0b0 @ reqLen);
     let saneTop = reqTop <=_u 0b1@0x00000000;
-    let (b, t) = getCapBoundsBits(c);
+    let (b, l, t) = getCapBoundsBits(c);
     let (representable, newCap) = setCapAddr(c, newAddr);
     let repTop = (0b0 @ b) + ((to_bits(33,1) << unsigned(c.E)) << 9);
     /* The representable bounds check: either E is max or address is in range */
@@ -266,4 +232,4 @@ function prop_crrl_cram_usage(reqLen : CapAddrBits) -> bool = {
     let mask = getRepresentableAlignmentMask(newLen);
     let mask2 = getRepresentableAlignmentMask(reqLen);
     ((reqLen == zeros()) | (newLen != zeros())) --> (mask == mask2)
-}
+}

qtest/qtest.ml

@@ -12,7 +12,7 @@ let gen_sailbits_geom n s =
 
 let test_cap_decode capbits =
   let cap = Cheri_cc.zcapBitsToCapability(false, capbits) in
-  let (bot, top)= Cheri_cc.zgetCapBounds(cap) in
+  let (bot, length, top)= Cheri_cc.zgetCapBounds(cap) in
   begin
     print (Cheri_cc.string_of_zbits capbits);
     print (",0x");