1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
\documentclass[a4paper]{article}
\usepackage{etoolbox}
\usepackage[nounderscore]{syntax}
\usepackage{amsmath,amssymb}
\usepackage[svgnames]{xcolor}
\usepackage{algorithmicx}
\usepackage{algpseudocode}
\usepackage{fullpage}
\usepackage{listings}
\usepackage{tikz}
\usetikzlibrary{arrows}
\usepackage{hyperref}
\hypersetup{colorlinks=true,linkcolor=DarkRed}
\newcommand{\TODO}[1]{{\color{red}{TODO: #1}}}
\lstset{
basicstyle=\ttfamily\small,
columns=fullflexible,
breaklines=true,
postbreak=\mbox{\textcolor{red}{$\hookrightarrow$}\space},
}
\lstdefinelanguage{sail}
{ morekeywords={val,function,mapping,cast,type,forall,overload,operator,enum,union,undefined,exit,and,assert,sizeof,
scattered,register,inc,dec,if,then,else,effect,let,as,@,in,end,Type,Int,Order,match,clause,struct,
foreach,from,to,by,infix,infixl,infixr,bitfield,default,try,catch,throw,constraint},
keywordstyle={\bf\ttfamily\color{blue}},
morestring=[b]",
stringstyle={\ttfamily\color{red}},
morecomment=[l][\itshape\color{DarkGreen}]{//},
morecomment=[s][\itshape\color{DarkGreen}]{/*}{*/},
deletestring=[bd]{'},
escapechar=\#,
emphstyle={\it},
literate=
{\{|}{{$\{|$}}1
{|\}}{{$|\}$}}1
}
\lstset{language=sail}
\def\sail{\trivlist \item\relax}
\def\endsail{\endtrivlist}
\newcommand{\saildocval}[2]{
#1 #2
}
\newcommand{\saildocfcl}[2]{
#1 #2
}
\newcommand{\saildoctype}[2]{
#1 #2
}
\newcommand{\saildocfn}[2]{
#1 #2
}
\newcommand{\saildocoverload}[2]{
#1 #2
}
\renewcommand{\ll}[1]{\lstinline{#1}}
\newcommand{\riscv}{RISC-V}
%% \input{grammar}
%% \renewcommand{\ottkw}[1]{\mbox{\ttfamily\bfseries{#1}}}
%% \renewcommand{\ottsym}[1]{\mathop{\mbox{\ttfamily{#1}}}}
%% %\renewcommand{\ottgrammartabular}[1]{\begin{center}\begin{tabular}{llcllllll}#1\end{tabular}\end{center}}
%% \renewcommand{\ottgrammartabular}[1]{\medskip\par\begin{supertabular}{llcllllll}#1\end{supertabular}\medskip\par\noindent}
%% \newcommand{\ottpartialrulehead}[3]{$#1$ & & $#2$ & $\ldots$ & & \multicolumn{2}{l}{#3}}
%% \renewcommand{\ottrulehead}[3]{\multicolumn{9}{l}{$#1$\quad $#2$}}%
%% \renewcommand{\ottprodline}[6]{\multicolumn{9}{l}{\quad$#1$\quad $#2$}}%
% Pandoc 2.0 and above wrap lstinline with a dummy passthrough command for escaping purposes
\newcommand{\passthrough}[1]{#1}
\begin{document}
\input{code_riscv}
\title{The Sail instruction-set semantics specification language}
\ifdefined\ANON
\author{Anonymous}
\newcommand\anonymise[1]{\emph{redacted}}
\newcommand\anonymiseomit[1]{}
\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}
\newcommand\anonymiseomit[1]{#1}
\fi
\maketitle
\tableofcontents
\include{introduction}
\include{riscv}
\include{usage}
\include{tutorial}
\lstset{language={},escapechar=\`}
\include{internals}
% Remove for now since incomplete
%\include{types}
\bibliographystyle{unsrt}
\bibliography{manual}
\end{document}
|
