CSetBoundsRoundDown

Makefile

@@ -318,7 +318,7 @@ c_emulator/cheri_riscv_rvfi_%: generated_definitions/c/riscv_rvfi_model_%.c $(SA
 	$(CC) -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(SAIL_RISCV_DIR)/c_emulator/riscv_sim.c $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
 
 latex: $(SAIL_SRCS) Makefile
-	$(SAIL) -latex -latex_prefix sailRISCV -o sail_latex_riscv $(SAIL_SRCS) properties/props.sail
+	$(SAIL) -latex -latex_prefix sailRISCV -o sail_latex_riscv $(SAIL_SRCS) properties/proplib.sail properties/props.sail properties/props_setboundsrounddown.sail
 
 generated_definitions/isabelle/$(ARCH)/ROOT: handwritten_support/ROOT
 	mkdir -p generated_definitions/isabelle/$(ARCH)

archdoc/app-isaquick-riscv.tex

@@ -51,6 +51,8 @@ \chapter{Instruction encoding summary}
 
 		\rvcheriisaquick{CSetBoundsExact}
 
+		\rvcheriisaquick{CSetBoundsRoundDown}
+
 		\rvcheriisaquick{CSetBoundsImm}
 
 		\rvcheriisaquick{CSetHigh}

archdoc/chap-changes.tex

@@ -44,5 +44,6 @@ \chapter{Version history}
     \item[\ghissue{71}, \ghpr{87}] \rvcheriasminsnref{CUnseal} now no longer requires exact equality between sealed input otype and authority address.
       Instead, it merely requires that the otype of the sealed input is within bounds to yield a tagged result.
       The address of a sealing-root capability is now meaningful only to \rvcheriasminsnref{CSeal}.
+    \item[\ghissue{72},\ghpr{74}] Introduce \rvcheriasminsnref{CSetBoundsRoundDown} to facilitate constructing representable slices of buffers.
   \end{description}
 \end{description}

archdoc/chap-encoding-sail.tex

@@ -24,6 +24,9 @@ \chapter{Sail listings for capability encoding}
 \medskip
 \sailRISCVfnsetCapBounds
 
+\medskip
+\sailRISCVfnsetCapBoundsRoundDown
+
 \medskip
 \sailRISCVfngetRepresentableAlignmentMask
 

archdoc/chap-isaref-riscv.tex

@@ -248,6 +248,7 @@ \subsection*{Functions for manipulating capabilities}
 
 \medskip
 \sailRISCVval{setCapBounds}
+\sailRISCVval{setCapBoundsRoundDown}
 \sailRISCVval{setCapAddr}
 \sailRISCVval{incCapAddr}
 % \sailRISCVval{setCapOffset}
@@ -305,6 +306,7 @@ \section{\cherimcu{} Instructions}
 \input{insn-riscv/csetaddr}
 \input{insn-riscv/csetbounds}
 \input{insn-riscv/csetboundsexact}
+\input{insn-riscv/csetboundsrounddown}
 \input{insn-riscv/csetboundsimm}
 \input{insn-riscv/csetequalexact}
 \input{insn-riscv/csethigh}

archdoc/def-riscv-insns.tex

@@ -33,6 +33,7 @@
 \rvcherisrcsrcdestimm[name=CIncAddrImm]{1}{cd}{cs1}{imm}
 \rvcherisrcsrcdest[name=CSetBounds]{8}{cd}{cs1}{rs2}
 \rvcherisrcsrcdest[name=CSetBoundsExact]{9}{cd}{cs1}{rs2}
+\rvcherisrcsrcdest[name=CSetBoundsRoundDown]{A}{cd}{cs1}{rs2}
 \rvcherisrcsrcdestimm[name=CSetBoundsImm]{2}{cd}{cs1}{uimm}
 \rvcherisrcsrcdest[name=CSetHigh]{16}{cd}{cs1}{rs2}
 \rvcherisrcdest[name=CClearTag]{B}{cd}{cs1}

archdoc/insn-riscv/csetboundsrounddown.tex

@@ -0,0 +1,16 @@
+\clearpage
+\phantomsection
+\addcontentsline{toc}{subsection}{CSetBoundsRoundDown}
+\insnriscvlabel{csetboundsrounddown}
+\subsection*{CSetBoundsRoundDown}
+
+\subsubsection*{Format}
+
+\rvcheriasm{CSetBoundsRoundDown}
+
+\begin{center}
+\rvcheriheader
+\rvcheribitbox{CSetBoundsRoundDown}
+\end{center}
+
+\sailRISCVisarefbody{CSetBoundsRoundDown}

properties/Makefile

@@ -5,12 +5,14 @@ SRCS+=${TOP}/sail-riscv/model/riscv_xlen32.sail
 SRCS+=${TOP}/src/cheri_prelude.sail
 SRCS+=${TOP}/src/cheri_types.sail
 SRCS+=${TOP}/src/cheri_cap_common.sail
+SRCS+=proplib.sail
 SRCS+=props.sail
+SRCS+=props_setboundsrounddown.sail
 
 all: generate_smt run_smt
 
 generate_smt:
-	sail -smt ${SRCS}
+	sail ${SAIL_FLAGS} -smt ${SRCS}
 
 run_smt:
 	@failure=0; \

properties/proplib.sail

@@ -0,0 +1,32 @@
+
+
+/* Syntactic sugar */
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+val operator --> : forall ('p 'q: Bool). (bool('p), bool('q)) -> bool('p --> 'q)
+function operator --> (p, q) = not_bool(p) | q
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+val operator <--> : forall ('p 'q: Bool). (bool('p), bool('q)) -> bool('p <--> 'q)
+function operator <--> (p, q) = (p --> q) & (q --> p)
+
+/* Useful functions */
+
+/*!
+ * THIS is a helper function to compress and then decompress a Capability.
+ * The [Capability] struct can hold non-encodable values therefore some
+ * properties encode then decode a Capability to check the effect that
+ * compression / decompression has. In general the bounds, address and tag
+ * should be unaffected but the permissions and otype might change.
+ */
+function encodeDecode(c : Capability) -> Capability =  capBitsToCapability(c.tag, capToBits(c))
+
+/*!
+ * THIS is a helper to check that the given Capability is unaffected by
+ * compression / decompression.
+ */
+function capEncodable(c : Capability) -> bool = c == encodeDecode(c)

properties/props.sail

@@ -1,36 +1,3 @@
-
-
-/* Syntactic sugar */
-
-infixr 1 -->
-
-type operator -->('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
-val operator --> : forall ('p 'q: Bool). (bool('p), bool('q)) -> bool('p --> 'q)
-function operator --> (p, q) = not_bool(p) | q
-
-infix 1 <-->
-
-type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
-val operator <--> : forall ('p 'q: Bool). (bool('p), bool('q)) -> bool('p <--> 'q)
-function operator <--> (p, q) = (p --> q) & (q --> p)
-
-/* Useful functions */
-
-/*!
- * THIS is a helper function to compress and then decompress a Capability.
- * The [Capability] struct can hold non-encodable values therefore some
- * properties encode then decode a Capability to check the effect that
- * compression / decompression has. In general the bounds, address and tag
- * should be unaffected but the permissions and otype might change.
- */
-function encodeDecode(c : Capability) -> Capability =  capBitsToCapability(c.tag, capToBits(c))
-
-/*!
- * THIS is a helper to check that the given Capability is unaffected by
- * compression / decompression.
- */
-function capEncodable(c : Capability) -> bool = c == encodeDecode(c)
-
 // $property
 /*
  * THIS is not actually an invariant but is useful for characterising unusable

properties/props_setboundsrounddown.sail

@@ -0,0 +1,61 @@
+/*!
+ * THIS checks that CSetBoundsRoundDown meets its description: the result leaves
+ * the base unaltered and returns a capability with length at most the requested
+ * size.
+ */
+$property
+function prop_setboundsrounddown_brief(reqBase : CapAddrBits, reqLen : CapAddrBits) -> bool = {
+    let c = setCapBoundsRoundDown(root_cap_mem, reqBase, reqLen);
+    let (resBase, resTop) = getCapBoundsBits(c);
+    let reqTop = (0b0 @ reqBase) + (0b0 @ reqLen);
+    let saneTop = reqTop <=_u 0b1@0x00000000;
+    saneTop --> ((resBase == reqBase) & (resTop <=_u reqTop) & (0b0 @ resBase <=_u resTop))
+}
+
+/*!
+ * THIS checks that exactly representable requests give equal answers between
+ * CSetBoundsRoundDown and CSetBounds, so long as the requested length is
+ * representable with exponent 14 or below.
+ */
+$property
+function prop_setboundsrounddown_exact(reqBase : CapAddrBits, reqLen : CapAddrBits) -> bool = {
+    let cRD = setCapBoundsRoundDown(root_cap_mem, reqBase, reqLen);
+    let (exact, cSB) = setCapBounds(root_cap_mem, reqBase, reqLen);
+    let threshold14 : CapAddrBits = zero_extend(ones(cap_mantissa_width)) << 14;
+    (exact & (reqLen <=_u threshold14)) --> (cRD == cSB)
+}
+
+/*!
+ * THIS checks that the resulting capability has nonzero length unless requested
+ */
+$property
+function prop_setboundsrounddown_nonzero(reqBase : CapAddrBits, reqLen : CapAddrBits) -> bool = {
+    let c = setCapBoundsRoundDown(root_cap_mem, reqBase, reqLen);
+    let (resBase, resTop) = getCapBoundsBits(c);
+    let reqTop = (0b0 @ reqBase) + (0b0 @ reqLen);
+    let saneTop = reqTop <=_u 0b1@0x00000000;
+    saneTop --> ( (0b0 @ resBase <_u resTop)
+                | ((0b0 @ resBase == resTop) & (reqLen == zeros())))
+}
+
+/*!
+ * THIS checks that [setCapBoundsRoundDown] returns the most precise encodable
+ * bounds that satisfy the requested bounds, unless the requested length is
+ * very large (above exponent 14), in which case the result is the largest
+ * exponent 14 capability.
+ */
+$property
+function prop_setboundsrounddown_precise(reqBase1 : CapAddrBits, reqLen1 : CapAddrBits,
+        c2 : CapBits) -> bool = {
+    let c1 = setCapBoundsRoundDown(root_cap_mem, reqBase1, reqLen1);
+    let (b1, t1) = getCapBoundsBits(c1);
+    let reqTop1 = (0b0 @ reqBase1) + (0b0 @ reqLen1);
+    let saneTop1 = reqTop1 <=_u 0b1@0x00000000;
+    let (b2, t2) = getCapBoundsBits(capBitsToCapability(false, c2));
+    let validBase = b2 == reqBase1;
+    let validTop = t2 <=_u reqTop1;
+    let betterTop = t1 <_u t2;
+    let threshold14 : CapAddrBits = zero_extend(ones(cap_mantissa_width)) << 14;
+    (saneTop1 & validBase & validTop & betterTop) -->
+      ((reqLen1 >=_u threshold14) & (t1 - (0b0 @ b1) == 0b0 @ threshold14))
+}

src/cheri_cap_common.sail

@@ -488,6 +488,57 @@ function setCapBounds(cap, base, length) : (Capability, CapAddrBits, CapAddrBits
   (exact, newCap)
 }
 
+/* XXX this should go in prelude.sail but putting here for now to avoid submodule faff */
+val count_trailing_zeros : forall 'N, 'N >=0 . bits('N) -> range(0, 'N)
+function count_trailing_zeros(bv) = {
+  foreach(i from 0 to ('N - 1) by 1 in inc) {
+    if bv[i] == bitone then {
+      return i;
+    }
+  };
+  'N
+}
+
+/*!
+ * Returns cap with the address and base set to the given base (exactly) and the
+ * length set to the largest value less than or equal to given length that can
+ * be represented while preserving the alignment of the base.
+ */
+function setCapBoundsRoundDown(cap, base, length) : (Capability, CapAddrBits, CapAddrBits) -> Capability = {
+  let ext_base = 0b0 @ base;
+  /* Compute new top, note extra bit in case of overflow */
+  let top : CapLenBits = ext_base + (0b0 @ length);
+  /* Find smallest exponent that can represent required length. */
+  let e_l : range(0, 23) = 23 - count_leading_zeros(truncateLSB(length, 23));
+  /* What is the required alignment of base? */
+  let e_b = count_trailing_zeros(base);
+
+  /*
+   * We're going to return something below the "band gap" in the encoding, so
+   * find the largest exponent that's: below the band gap, less than or equal to
+   * what's required by the length (e), and less than or equal to what's
+   * required by the base (e_b).
+   */
+  let E = min(14, min(e_l, e_b));
+
+  /* Extract B for this E */
+  let B = truncate(base >> E, cap_mantissa_width);
+
+  let T = if (e_l > e_b) | (e_l > 14) then {
+    /*
+     * Base unrepresentable using chosen e_l or length over long; choose a
+     * smaller exponent, E, and make a maximum length capability for that.
+     */
+    B - 1;
+  } else {
+    /* Extract T for E as is */
+    truncate(top >> e_l, cap_mantissa_width)
+  };
+
+  /* Return the cap with new bounds and address */
+  {cap with address=base, E=to_bits(cap_E_width, E), B=B, T=T}
+}
+
 function getCapPerms(cap) : Capability -> CapPermsBits = [
   bool_to_bit(cap.perm_user0),
   bool_to_bit(cap.permit_seal),

src/cheri_insts.sail

@@ -596,6 +596,42 @@ function clause execute (CSetBoundsExact(cd, cs1, rs2)) = {
   RETIRE_SUCCESS
 }
 
+union clause ast = CSetBoundsRoundDown : (regidx, regidx, regidx)
+/*!
+ * Capability register *cd* is set to the capability in register *cs1* with its
+ * **base** field replaced with *cs1*.**address** and its **length** field
+ * replaced with a representable value no larger than the value in the integer
+ * register *rs2*.  That **length** will be nonzero if *rs2* is nonzero.
+ *
+ * ## Notes
+ *
+ *  - As with [CSetBounds], the implementation here does the bounds check on the
+ *    *requested* bounds.  This is less interesting here than there because the
+ *    results of [setCapBoundsRoundDown] are always a subset of the requested
+ *    range.
+ *
+ *  - The present implementation returns the largest representable span from the
+ *    given base (*cs1*.**address**) whose length is no more than *rs2*, except
+ *    that it will not return anything larger than the largest capability
+ *    representable with an exponent of 14.  This caveat simplifies handling of
+ *    very large capabilities, which we do not expect to be used with this
+ *    instruction in practice.  However, we may revisit this decision in future
+ *    editions; software should depend only on the result being representable
+ *    and of non-zero length (unless *rs2* was zero).
+ */
+function clause execute (CSetBoundsRoundDown(cd, cs1, rs2)) = {
+  let cs1_val = C(cs1);
+  let rs2_val = X(rs2);
+
+  let newBase = cs1_val.address;
+  let newLen = rs2_val;
+  let inBounds = inCapBounds(cs1_val, newBase, unsigned(newLen));
+  let inCap = clearTagIfSealed(cs1_val);
+  let newCap = setCapBoundsRoundDown(inCap, newBase, newLen);
+  C(cd) = clearTagIf(newCap, not(inBounds));
+  RETIRE_SUCCESS
+}
+
 union clause ast = CClearTag : (regidx, regidx)
 /*!
  * Capability register *cd* is replaced with the contents of *cs1*, with
@@ -976,6 +1012,7 @@ mapping clause encdec = CSetHigh(cd, cs1, rs2)    if (haveXcheri()) <-> 0b001011
 mapping clause encdec = CIncAddr(cd, cs1, rs2)    if (haveXcheri()) <-> 0b0010001 @ rs2 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri())
 mapping clause encdec = CSetBounds(cd, cs1, rs2)  if (haveXcheri()) <-> 0b0001000 @ rs2 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri())
 mapping clause encdec = CSetBoundsExact(cd, cs1, rs2) if (haveXcheri()) <-> 0b0001001 @ rs2 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri())
+mapping clause encdec = CSetBoundsRoundDown(cd, cs1, rs2) if (haveXcheri()) <-> 0b0001010 @ rs2 @ cs1 @ 0b000 @ cd @ 0b1011011 if (haveXcheri())
 
 mapping clause encdec = CSub(rd, cs1, cs2)        if (haveXcheri()) <-> 0b0010100 @ cs2 @ cs1 @ 0b000 @ rd @ 0b1011011 if (haveXcheri())
 
@@ -995,6 +1032,7 @@ mapping clause assembly = CSetHigh(cd, cs1, rs2)  <-> "csethigh"    ^ spc() ^ ca
 mapping clause assembly = CIncAddr(cd, cs1, rs2)   <-> "cincaddr" ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ reg_name(rs2)
 mapping clause assembly = CSetBounds(cd, cs1, rs2) <-> "csetbounds" ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ reg_name(rs2)
 mapping clause assembly = CSetBoundsExact(cd, cs1, rs2) <-> "csetboundsexact" ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ reg_name(rs2)
+mapping clause assembly = CSetBoundsRoundDown(cd, cs1, rs2) <-> "csetboundsrounddown" ^ spc() ^ cap_reg_name(cd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ reg_name(rs2)
 
 mapping clause assembly = CSub(rd, cs1, cs2)      <-> "csub"        ^ spc() ^ reg_name(rd) ^ sep() ^ cap_reg_name(cs1) ^ sep() ^ cap_reg_name(cs2)