diff options
| -rw-r--r-- | Makefile | 11 | ||||
| -rw-r--r-- | doc/Makefile | 10 | ||||
| -rw-r--r-- | doc/examples/my_replicate_bits.sail | 4 | ||||
| -rw-r--r-- | doc/introduction.tex | 6 | ||||
| -rw-r--r-- | doc/manual.tex | 9 |
5 files changed, 33 insertions, 7 deletions
@@ -53,6 +53,17 @@ apply_header: headache -c etc/headache_config -h LICENCE `ls src/lem_interp/*.lem` $(MAKE) -C arm apply_header +anon_dist: + $(MAKE) clean + headache -c etc/headache_config -h etc/anon_header `ls mips/*.sail` + headache -c etc/headache_config -h etc/anon_header `ls cheri/*.sail` + headache -c etc/headache_config -h etc/anon_header `ls src/Makefile*` + headache -c etc/headache_config -h etc/anon_header `ls src/*.ml*` + headache -c etc/headache_config -h etc/anon_header `ls src/lem_interp/*.ml` + headache -c etc/headache_config -h etc/anon_header `ls src/lem_interp/*.lem` + headache -c etc/headache_config -h etc/anon_header `ls arm/*.sail` + tar cvzf sail.tar.gz . + clean: for subdir in src arm ; do\ $(MAKE) -C "$$subdir" clean;\ diff --git a/doc/Makefile b/doc/Makefile index b5a74dd6..ae542571 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -65,11 +65,15 @@ code_myreplicatebits.tex: examples/my_replicate_bits.sail grammar.tex: ../language/sail.ott ott -pp_grammar -tex_wrap false -tex_suppress_category I -tex_suppress_category D -tex_suppress_ntr terminals -tex_suppress_ntr formula -tex_suppress_ntr judgement -tex_suppress_ntr user_syntax -tex_suppress_ntr dec_comm -sort false -generate_aux_rules false -picky_multiple_parses true -i ../language/sail.ott -o grammar.tex +LATEXARG=manual.tex manual.pdf: grammar.tex introduction.tex usage.tex types.tex code_riscv.tex riscv.tex manual.tex manual.bib tutorial.tex code_myreplicatebits.tex - pdflatex manual.tex + pdflatex ${LATEXARG} bibtex manual - pdflatex manual.tex - pdflatex manual.tex + pdflatex ${LATEXARG} + pdflatex ${LATEXARG} + +anon_man: LATEXARG='\def\ANON{}\input{manual.tex}' +anon_man: manual.pdf clean: -rm manual.pdf diff --git a/doc/examples/my_replicate_bits.sail b/doc/examples/my_replicate_bits.sail index c9972cd6..8c3c9458 100644 --- a/doc/examples/my_replicate_bits.sail +++ b/doc/examples/my_replicate_bits.sail @@ -17,10 +17,14 @@ val operator >> = { val "or_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) +val zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) + overload operator | = {or_vec} val my_replicate_bits : forall 'n 'm, 'm >= 1 & 'n >= 1. (int('n), bits('m)) -> bits('n * 'm) +val zeros = "zeros" : forall 'n. atom('n) -> bits('n) + function my_replicate_bits(n, xs) = { ys = zeros(n * length(xs)); foreach (i from 1 to n) { diff --git a/doc/introduction.tex b/doc/introduction.tex index 5969f34f..9e268de5 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -114,12 +114,12 @@ except vector, float, and load-multiple instructions, without exceptions; for ARMv8 this is for the A64 fragment. The ARMv8 (hand) model is hand-written based on the ARMv8-A -specification document~\cite{armarmv8,FGP16}, principally by Flur. +specification document~\cite{armarmv8,FGP16}, principally by \anonymise{Flur}. The Power model is based on an automatic extraction of pseudocode and decoding data from an XML export of the Framemaker document source of the IBM Power manual~\cite{Power2.06,micro2015}, with manual patching -as necessary, principally by Kerneis and Gray. +as necessary, principally by \anonymise{Kerneis and Gray}. The ARMv8 (ASL) model is based on an automatic translation of ARM's machine-readable public v8.3 ASL specification\footnote{ARM v8-A @@ -135,7 +135,7 @@ which in turn drew on MIPS4000 and MIPS32~\cite{MIPS4000,MIPS32-I}. % The CHERI model is based on that and the CHERI ISA reference manual version~5~\cite{UCAM-CL-TR-891}. These two are both principally by -Norton-Wright; they cover all basic user and kernel mode MIPS features +\anonymise{Norton-Wright}; they cover all basic user and kernel mode MIPS features sufficient to boot FreeBSD, including a TLB, exceptions and a basic UART for console interaction. ISA extensions such as floating point are not covered. The CHERI model supports either 256-bit capabilities diff --git a/doc/manual.tex b/doc/manual.tex index 3b75b26a..d28719a4 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -64,9 +64,15 @@ \title{The Sail instruction-set semantics specification language} +\ifdefined\ANON +\author{Anonymous} +\newcommand\anonymise[1]{\emph{redacted}} +\else \author{Alasdair Armstrong \and Thomas Bauereiss \and Brian Campbell \and Shaked Flur \and Kathryn E. Gray \and Robert Norton-Wright \and Christopher Pulte \and Peter Sewell} +\newcommand\anonymise[1]{#1} +\fi \maketitle @@ -80,7 +86,8 @@ \include{tutorial} -\include{types} +% Remove for now since incomplete +%\include{types} \bibliographystyle{unsrt} \bibliography{manual} |