Add latex sources for the architecture document.

.gitignore

@@ -1,3 +1,4 @@
 generated_definitions
 z3_problems
 c_emulator
+sail_latex_riscv

archdoc/.gitignore

@@ -0,0 +1,2 @@
+*.pdf
+build

archdoc/LICENSE

@@ -0,0 +1,7 @@
+\noindent
+The CHERI ISA specification is licensed under the Creative Commons Attribution
+4.0 International License.  To view a copy of this license, visit:
+
+\medskip
+
+\url{http://creativecommons.org/licenses/by/4.0/}

archdoc/LICENSE-sail-cheri-riscv

@@ -0,0 +1,57 @@
+\noindent
+The CHERI-RISC-V pseudocode is derived from the Sail CHERI-RISC-V model\footnote{\url{https://github.com/CTSRD-CHERI/sail-cheri-riscv}},
+which has the following license:
+
+\begin{scriptsize}
+\begin{verbatim}
+This CHERI Sail RISC-V architecture model here, comprising all files and
+directories except for the snapshots of the Lem and Sail libraries in the
+prover_snapshots directory (which include copies of their licenses), is subject
+to the BSD two-clause licence below.
+
+Copyright (c) 2017-2021 Alasdair Armstrong, Thomas Bauereiss, Brian Campbell,
+  Jessica Clarke, Nathaniel Wesley Filardo (contributions prior to July 2020,
+  thereafter Microsoft), Alexandre Joannou, Microsoft, Prashanth Mundkur,
+  Robert Norton-Wright (contributions prior to March 2020, thereafter
+  Microsoft), Alexander Richardson, Peter Rugg, Peter Sewell
+
+All rights reserved.
+
+This software was developed by SRI International and the University of
+Cambridge Computer Laboratory (Department of Computer Science and
+Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and
+under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA
+SSITH research programme.
+
+This software was developed within the Rigorous Engineering of
+Mainstream Systems (REMS) project, partly funded by EPSRC grant
+EP/K008528/1, at the Universities of Cambridge and Edinburgh.
+
+This project has received funding from the European Research Council
+(ERC) under the European Union’s Horizon 2020 research and innovation
+programme (grant agreement 789108, ELVER).
+
+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.
+\end{verbatim}
+\end{scriptsize}

archdoc/LICENSE-sail-riscv

@@ -0,0 +1,59 @@
+\noindent
+The RISC-V pseudocode is derived from the Sail RISC-V model\footnote{\url{https://github.com/riscv/sail-riscv}},
+which has the following license:
+\begin{scriptsize}
+\begin{verbatim}
+This Sail RISC-V architecture model, comprising all files and
+directories except for the snapshots of the Lem and Sail libraries
+in the prover_snapshots directory (which include copies of their
+licences), is subject to the BSD two-clause licence below.
+
+Copyright (c) 2017-2021 Prashanth Mundkur, Rishiyur S. Nikhil and
+  Bluespec, Inc., Jon French, Brian Campbell, Robert Norton-Wright,
+  Alasdair Armstrong, Thomas Bauereiss, Shaked Flur, Christopher Pulte,
+  Peter Sewell, Alexander Richardson, Hesham Almatary,
+  Jessica Clarke, Microsoft, for contributions by Robert Norton-Wright and
+  Nathaniel Wesley Filardo, Peter Rugg,
+  Aril Computer Corp., for contributions by Scott Johnson
+
+All rights reserved.
+
+This software was developed by the above within the Rigorous
+Engineering of Mainstream Systems (REMS) project, partly funded by
+EPSRC grant EP/K008528/1, at the Universities of Cambridge and
+Edinburgh.
+
+This software was developed by SRI International and the University of
+Cambridge Computer Laboratory (Department of Computer Science and
+Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and
+under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA
+SSITH research programme.
+
+This project has received funding from the European Research Council
+(ERC) under the European Union’s Horizon 2020 research and innovation
+programme (grant agreement 789108, ELVER).
+
+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.
+\end{verbatim}
+\end{scriptsize}

archdoc/Makefile

@@ -0,0 +1,93 @@
+TARGET=cheriot-architecture.pdf
+MAIN_TEX=cheriot-architecture.tex
+SAIL_LATEX_RISCV_DIR=sail_latex_riscv
+
+SOURCES=$(wildcard *.tex insn-riscv/*.tex $(SAIL_LATEX_RISCV_DIR)/*.tex) cheri.bib LICENSE LICENSE-sail-cheri-riscv LICENSE-sail-riscv
+
+TIKZFIGURES=fig-representable-regions.pdf fig-sentry-plt.pdf fig-type-token.pdf
+FIGSOURCES=						\
+	misc/perms/perms5_clustered.pdf \
+	$(TIKZFIGURES)
+
+V?=0
+ifeq ($(V),0)
+INTERACTION=batchmode
+TEXLOGANALYSER_FLAGS=-w
+else
+INTERACTION=nonstopmode
+# Also include page numbers to make it easier to find what caused the warning
+TEXLOGANALYSER_FLAGS=-w -n
+endif
+
+LATEXMK_COMMON_FLAGS=-bibtex -pdf
+PDFLATEX_FLAGS=-file-line-error -halt-on-error -interaction=$(INTERACTION)
+
+.PHONY: all
+all: sail-latex ${TARGET}
+
+# The texloganalyser tool can be used to find all warning messages in the latex
+# logfile which is useful when using interaction=batchmode. There is also
+# a python package pydflatex that does the same thing (but with colours).
+# Howver, texloganalyser is included by default in some TeX distributions so
+# prefer that one.
+# TODO: fix the broken sail hyperrefs so we don't have to filter the out.
+${TARGET}: ${SOURCES} ${FIGSOURCES}
+	latexmk $(LATEXMK_COMMON_FLAGS) $(MAIN_TEX) $(PDFLATEX_FLAGS); ret=$$?; \
+	    if command -v texloganalyser >/dev/null 2>/dev/null; then \
+	        texloganalyser $(TEXLOGANALYSER_FLAGS) build/cheri-architecture.log; \
+	    fi; exit $$ret
+
+$(TIKZFIGURES): %.pdf: %.tex Makefile
+	latexmk $(LATEXMK_COMMON_FLAGS) $(PDFLATEX_FLAGS) $<
+
+.PHONY: figures
+figures: $(TIKZFIGURES)
+
+.PHONY: quick
+quick:
+	pdflatex $(MAIN_TEX) $(PDFLATEX_FLAGS)
+	@(echo "pdflatex only run once so build may be incomplete")
+
+# The sed commands require GNU sed
+ifeq ($(shell uname -s),Linux)
+SED?=sed
+else
+SED?=gsed
+endif
+
+# Work around `find: fts_read: Invalid argument` on macOS
+ifeq ($(shell uname -s),Darwin)
+FIND?=gfind
+else
+FIND?=find
+endif
+
+SAIL_CHERI_RISCV_DIR?=..
+sail-latex:
+	rm -rf $(SAIL_LATEX_RISCV_DIR)
+	$(MAKE) -C $(SAIL_CHERI_RISCV_DIR) latex
+	mv $(SAIL_CHERI_RISCV_DIR)/$(SAIL_LATEX_RISCV_DIR) .
+	$(FIND) $(SAIL_LATEX_RISCV_DIR) -type f -name 'fcl*zexecute*.tex' -exec $(SED) -i -e '1d; 2{/^{$$/d}; $$d; s/^  //;' {} +
+	touch $(SAIL_LATEX_RISCV_DIR)/0GENERATED_FILES_DO_NOT_EDIT
+	touch $(SAIL_LATEX_RISCV_DIR)/zGENERATED_FILES_DO_NOT_EDIT
+	$(FIND) $(SAIL_LATEX_RISCV_DIR) -type f -exec chmod -w {} +
+
+.PHONY: clean update-sail-defs sail-latex
+clean:
+	latexmk -C $(LATEXMK_COMMON_FLAGS) $(MAIN_TEX)
+	latexmk -C $(LATEXMK_COMMON_FLAGS) fig-*.tex
+	rm -f $(TARGET) $(TIKZFIGURES)
+
+cheri-sorted.bib: cheri.bib bib-sorting.conf
+	biber --tool $< --sortcase=false --strip-comments --sortdebug --isbn13 --isbn-normalise --fixinits \
+	    --output_indent=4 --output_fieldcase=lower --sortlocale=en_GB \
+	    --configfile=bib-sorting.conf --validate-config --output-file=$@
+
+
+.PHONY: check-bibliography check-bibliography-strict
+check-bibliography:
+	# For more detailed output add --debug
+	biber --tool cheri.bib
+
+check-bibliography-strict:
+	biber --tool --validate-datamodel cheri.bib | grep -v "Missing mandatory field 'editor'" | grep -v "is not an integer"

archdoc/acknowledgments.tex

@@ -0,0 +1,134 @@
+\section*{Acknowledgments}
+
+\vspace{-0.2cm}
+
+\noindent
+This document contains some elements from the CHERI ISA Specification\footnote{\url{https://github.com/CTSRD-CHERI/cheri-specification}},
+which is licensed under the Creative Commons Attribution 4.0 International License. 
+To view a copy of this license, visit:
+
+\medskip
+
+\url{http://creativecommons.org/licenses/by/4.0/}
+
+\medskip
+\noindent
+We acknowledge all the authors of that report:
+
+\medskip
+\begin{small}
+\noindent\begin{autogrid}{4}
+Robert~N.~M.~Watson \\
+Peter~G.~Neumann \\
+Jonathan~Woodruff \\
+Michael~Roe \\
+Hesham~Almatary \\
+Jonathan~Anderson \\
+John~Baldwin \\
+Graeme~Barnes \\
+David~Chisnall \\
+Jessica~Clarke \\
+Brooks~Davis \\
+Lee~Eisen \\
+Nathaniel~Wesley~Filardo \\
+Richard~Grisenthwaite \\
+Alexandre~Joannou \\
+Ben~Laurie \\
+A.~Theodore~Markettos \\
+Simon~W.~Moore \\
+Steven~J.~Murdoch \\
+Kyndylan~Nienhuis \\
+Robert~Norton \\
+Alexander~Richardson \\
+Peter~Rugg \\
+Peter~Sewell \\
+Stacey~Son \\
+Hongyan~Xia
+\end{autogrid}
+\end{small}
+
+\medskip
+\noindent
+as well as the many other contributors to the CHERI project:
+\medskip
+
+\begin{small}
+\noindent\begin{autogrid}{4}
+Sam Ainsworth \\
+Ross J. Anderson \\
+Ruben Ayrapetyan \\
+Hadrien Barral \\
+Thomas Bauereiss \\
+Stuart Biles \\
+Andrew Bivin \\
+Peter Blandford-Baker \\
+Matthias Boettcher \\
+David Brazdil \\
+Reuben Broadfoot \\
+Kevin Brodsky \\
+Ruslan Bukin \\
+Brian Campbell \\
+Gregory Chadwick \\
+Serban Constantinescu \\
+Chris Dalton \\
+Nirav Dave \\
+Dominique Devriese \\
+Mike Dodson \\
+Lawrence Esswood \\
+Jonas Fiala \\
+Wedson Filho \\
+Anthony Fox \\
+Paul J. Fox \\
+Franz Fuchs \\
+Ivan Gomes Ribeiro \\
+Paul Gotch \\
+Tom Grocutt \\
+Khilan Gudka \\
+Brett Gutstein \\
+Jong Hun Han \\
+Andy Hopper \\
+Alex Horsman \\
+Timothy Jones \\
+Asif Khan \\
+Myron King \\
+Joe Kiniry \\
+Chris Kitching \\
+Wojciech Koszek \\
+Robert Kovacsics \\
+Karthik Muthusamy \\
+Patrick Lincoln \\
+Marno van der Maas \\
+Anil Madhavapeddy \\
+Ilias Marinos \\
+Tim Marsland \\
+Ed Maste \\
+Alfredo Mazzinghi \\
+Kayvan Memarian \\
+Dejan Milojicic \\
+Andrew W. Moore \\
+Will Morland \\
+Alan Mujumdar \\
+Prashanth Mundkur \\
+Edward Napierala \\
+Philip Paeps \\
+Lucian Paul-Trifu \\
+Austin Roach \\
+Colin Rothwell \\
+John Rushby \\
+Hassen Saidi \\
+Hans Petter Selasky \\
+Andrew Scull \\
+Muhammad Shahbaz \\
+Bradley Smith \\
+Lee Smith \\
+Ian Stark \\
+Ramy Tadros \\
+Andrew Turner \\
+Richard Uhler \\
+Munraj Vadera \\
+Jacques Vidrine \\
+Hugo Vincent \\
+Philip Withnall \\
+Bjoern A. Zeeb \\
+\end{autogrid}
+\end{small}