Add CGetHigh and CSetHigh to the RISC-V instruction reference

Author: arichardson

app-isaquick-riscv.tex

@@ -47,6 +47,8 @@ \chapter{CHERI-RISC-V ISA Quick Reference}
 
 		\rvcheriisaquick{CGetAddr}
 
+		\rvcheriisaquick{CGetHigh}
+
 		\rvcheriisaquick{CGetTop}
 
 		\dcnote{CGetPCC is a Special}
@@ -78,6 +80,8 @@ \chapter{CHERI-RISC-V ISA Quick Reference}
 
 		\rvcheriisaquick{CSetBoundsImm}
 
+		\rvcheriisaquick{CSetHigh}
+
 		\rvcheriisaquick{CClearTag}
 
 		\rvcheriisaquick{CBuildCap}

chap-isaref-riscv.tex

@@ -257,6 +257,7 @@ \section{CHERI-RISC-V Instructions}
 \input{insn-riscv/cgetaddr}
 \input{insn-riscv/cgetbase}
 \input{insn-riscv/cgetflags}
+\input{insn-riscv/cgethigh}
 \input{insn-riscv/cgetlen}
 \input{insn-riscv/cgetoffset}
 \input{insn-riscv/cgetperm}
@@ -283,6 +284,7 @@ \section{CHERI-RISC-V Instructions}
 \input{insn-riscv/csetboundsimm}
 \input{insn-riscv/csetequalexact}
 \input{insn-riscv/csetflags}
+\input{insn-riscv/csethigh}
 \input{insn-riscv/csetoffset}
 \input{insn-riscv/cspecialrw}
 \input{insn-riscv/csub}

def-riscv-insns.tex

@@ -26,11 +26,7 @@
 \rvcherisrcdest[name=CGetFlags]{7}{rd}{cs1}
 \rvcherisrcdest[name=CGetAddr]{F}{rd}{cs1}
 \rvcherisrcdest[name=CGetTop]{18}{cd}{cs1}
-
-% Mark as noref and reserved until landing of
-% https://github.com/CTSRD-CHERI/sail-cheri-riscv/pull/55
-\rvcherisrcdest[name=CGetHigh,noref,tablesuffix=\rvcherireservedfootnotemark]{17}{cd}{cs1}
-\rvcherisrcsrcdest[name=CSetHigh,noref,tablesuffix=\rvcherireservedfootnotemark]{16}{cd}{cs1}{rs1}
+\rvcherisrcdest[name=CGetHigh]{17}{cd}{cs1}
 
 \rvcherisrcsrcdest[name=CSeal]{B}{cd}{cs1}{cs2}
 \rvcherisrcsrcdest[name=CUnseal]{C}{cd}{cs1}{cs2}
@@ -43,6 +39,7 @@
 \rvcherisrcsrcdest[name=CSetBounds]{8}{cd}{cs1}{rs2}
 \rvcherisrcsrcdest[name=CSetBoundsExact]{9}{cd}{cs1}{rs2}
 \rvcherisrcsrcdestimm[name=CSetBoundsImm]{2}{cd}{cs1}{uimm}
+\rvcherisrcsrcdest[name=CSetHigh]{16}{cd}{cs1}{rs1}
 \rvcherisrcdest[name=CClearTag]{B}{cd}{cs1}
 \rvcherisrcsrcdest[name=CBuildCap]{1D}{cd}{cs1}{cs2}
 \rvcherisrcsrcdest[name=CCopyType]{1E}{cd}{cs1}{cs2}

insn-riscv/cgethigh.tex

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

insn-riscv/csethigh.tex

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

sail_latex_riscv/commands.tex

@@ -5233,6 +5233,30 @@ \subsection*{Exceptions}
 
 }{\lstinputlisting[language=sail]{sail_latex_riscv/fclCGetOffsetzexecute33a689e3a631b9b905b85461d3814943.tex}}}}
 
+\newcommand{\sailRISCVfclCGetHighexecute}{\saildoclabelled{sailRISCVfclCGetHighzexecute}{\saildocfcl{Integer register \emph{rd} is set equal to the \textbf{high half} of capability
+register \emph{cs1}.
+
+The bits returned here are of the \textbf{in-memory} form of the capability, which
+may differ from microarchitectural forms in use within implementations.
+(Notably, in the sail implementation, see the distinction between \hyperref[sailRISCVzcapToBits]{\lstinline{capToBits}}
+and \hyperref[sailRISCVzcapToMemBits]{\lstinline{capToMemBits}}.)  That is, applying \hyperref[sailRISCVzCGetHigh]{\lstinline{CGetHigh}} to a capability loaded
+from address \emph{m} will yield the same result as loading the high half of the
+capability-sized granule at \emph{m} (that is, bits above \textbf{XLEN} when a
+capability is interpreted as a twice-\textbf{XLEN}-bit integer).
+
+}{\lstinputlisting[language=sail]{sail_latex_riscv/fclCGetHighzexecute33a689e3a631b9b905b85461d3814943.tex}}}}
+
+\newcommand{\sailRISCVfclCSetHighexecute}{\saildoclabelled{sailRISCVfclCSetHighzexecute}{\saildocfcl{Capability register \emph{cd} comes to hold the capability from \emph{cs1} with its
+high bits replaced with the value in the integer register \emph{rs2}.  The tag
+of \emph{cd} is cleared.
+
+\emph{rs2} holds the \textbf{in-memory} form of capability bits.  That is, this
+instruction yields the same result as writing \emph{cs1} out to memory,
+overwriting the high word with \emph{rs2}, and loading that capability-sized
+granule into \emph{cd}, although without the memory mutation side-effects.
+
+}{\lstinputlisting[language=sail]{sail_latex_riscv/fclCSetHighzexecute33a689e3a631b9b905b85461d3814943.tex}}}}
+
 \newcommand{\sailRISCVfclCGetLenexecute}{\saildoclabelled{sailRISCVfclCGetLenzexecute}{\saildocfcl{Integer register \emph{rd} is set equal to the \textbf{length} field of capability
 register \emph{cs1}.
 

sail_latex_riscv/fclCGetHighzexecute33a689e3a631b9b905b85461d3814943.tex

@@ -0,0 +1,3 @@
+let capVal : Capability = #\hyperref[sailRISCVzC]{C}#(cs1);
+#\hyperref[sailRISCVzX]{X}#(rd) = #\hyperref[sailRISCVzcapToMemBits]{capToMemBits}#(capVal)[sizeof(xlen) * 2 - 1 .. sizeof(xlen)];
+RETIRE_SUCCESS

sail_latex_riscv/fclCSetHighzexecute33a689e3a631b9b905b85461d3814943.tex

@@ -0,0 +1,6 @@
+let capVal = #\hyperref[sailRISCVzC]{C}#(cs1);
+let intVal = #\hyperref[sailRISCVzX]{X}#(rs2);
+let capLow : xlenbits = #\hyperref[sailRISCVzcapToMemBits]{capToMemBits}#(capVal)[sizeof(xlen) - 1 .. 0];
+let newCap : Capability = #\hyperref[sailRISCVzmemBitsToCapability]{memBitsToCapability}#(false, intVal @ capLow);
+#\hyperref[sailRISCVzC]{C}#(cd) = newCap;
+RETIRE_SUCCESS

sail_latex_riscv/fnzstepb001f84c8bf78b78b44b98d2b7f1f7d7.tex

@@ -27,6 +27,7 @@
           },
           /* non-error cases: */
           #\hyperref[sailRISCVzFzyRVC]{F\_RVC}#(h) => {
+            instbits = #\hyperref[sailRISCVzEXTZ]{EXTZ}#(h);
             let ast = #\hyperref[sailRISCVzdecodeCompressed]{decodeCompressed}#(h);
             if   #\hyperref[sailRISCVzgetzyconfigzyprintzyinstr]{get\_config\_print\_instr}#()
             then {
@@ -42,6 +43,7 @@
              }
           },
           #\hyperref[sailRISCVzFzyBase]{F\_Base}#(w) => {
+            instbits = #\hyperref[sailRISCVzEXTZ]{EXTZ}#(w);
             let ast = #\hyperref[sailRISCVzdecode]{decode}#(w);
             if   #\hyperref[sailRISCVzgetzyconfigzyprintzyinstr]{get\_config\_print\_instr}#()
             then {