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
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
|
Sail README
Kathryn E. Gray and Peter Sewell
15 March 2017
********************************************************************
OVERVIEW
Sail is a language for describing the instruction semantics of
processors. It has been used in several papers, available from
http://www.cl.cam.ac.uk/~pes20/sail/
This repository contains the implementation of Sail, together with
related tools and some Sail specifications:
- a manual, manual.pdf
- sail, the type checker and compiler for programs in the Sail
language;
- a Sail specification of a MIPS ISA (in mips/)
- a Sail specification of a Cheri ISA (in cheri/)
- a Sail specification of part of the ARMv8 ISA (in arm/)
- a sequential Sail interpreter, which evaluates an ELF binary for an
architecture that has been specified using Sail (for ABIs included
in our ELF specification);
- machinery to interface with the PPCMEM concurrent evaluation
exploration tool; and
- a formal definition of the Sail language and type system.
- an emacs mode, including syntax highlighting
We also have a substantial IBM POWER ISA specification,
which we can send by email.
**************************************************************************
BUILDING
SAIL COMPILER
The Sail compiler requires OCaml; it is tested on version 4.02.3.
Run "make" in the top level sail directory; this will generate an executable
called sail in this directory and will compile the interpreter files.
make clean will remove this executable as well as the build files in
subdirectories.
SAIL INTERPRETER
The Sail interpreter relies on external access to two external tools:
Lem: a specification language that generates theorem prover code
for HOL4, Isabelle, and Coq, and executable OCaml code from a
specification. It is a publicly available Bitbucket repository
https://bitbucket.org/Peter_Sewell/lem
Linksem: a formal specification of ELF that includes the facility
to read in an ELF file and represent them in uniform ways. It is
a public Bitbucket repository
https://bitbucket.org/Peter_Sewell/linksem
The Sail build system expects to find these repositories in the same
directory as the sail repository by default. This can be changed with
make variables LEM, LEMLIBOCAML, and ELFDIR
To build the interpreter, first build Lem and the Lem ocaml libraries.
Then call make interpreter from either the toplevel directory or the src
directory.
The interpreter currently only evaluates binaries and requires modifications
to a file within the src/lem_interp directory to support new architectures.
There is 'bit-rotted' support for evaluating separate sail files and function
calls.
MIPS SEQUENTIAL EVALUATOR
With the sail interpreter and the linksem repository explained above,
the mips sequential interpreter can be build in the src/ subdirectory
with
make run_mips.native
This will then evaluate any statically linked mips elf file (without
syscalls). Use --help for command line options
Todo: describe interpreter commands
**************************************************************************
EMACS MODE
There is an emacs mode implementation very similar to the Tuareg mode in sail/editors
**************************************************************************
To get started, one probably wants to develop a new definition by
analogy with the existing MIPS definition, using the sail executable
just to check that it is type-correct. After building sail (as
described below), this is done by:
./sail mips/mips_prelude.sail mips/mips_wrappers.sail mips/mips_insts.sail mips/mips_epilogue.sail
Sail treats multiple file arguments as though they wre concatenated
into a single large file (although error messages will give the
appropriate file and line number). For an explanation of how the MIPS
model is divided up see mips/README.
Once sufficient instructions have been represented in a specification,
then one may also want to run executables sequentially, to debug the
specification and begin testing. For this, one would need to adapt the
sequential sail interpreter, which evaluates the specification on an
ELF file.
Building the architecture for compilation to connect to the
interpreter, one uses the sail executable:
./sail <sail files...> -lem_ast
which will generate a mips.lem file in the current directory, which
will be linked with the sail interpreter (the output is a verbose
representation of the sail AST).
To generate Lem specifications for theorem proving, one uses the sail
executable with flag:
./sail mips/mips.sail -lem
To generate OCaml output for fast sequential evaluation, one uses the
sail executable with flag:
./sail mips/mips.sail -ocaml
******************************************************************************
LICENCES
The Sail implementation, in src/, is distributed under the 2-clause
BSD licence in the headers of those files and in src/LICENCE, with the
exception of the library src/pprint, which is distributed under the
CeCILL-C free software licence in src/pprint/LICENSE.
The ARMv8 model, in arm/, is distributed under the 2-clause BSD
licence in the headers of those files.
The MIPS and CHERI models, in mips/ and cheri/, are distributed under
the 2-clause BSD licence in the headers of those files.
******************************************************************************
DIRECTORY STRUCTURE
Sail sources and binaries are to be found in the directories of
bitbucket/sail (l2 is the previous working name of sail).
Top level directories
src/ ML implementation of Sail frontend, Sail executable, subdirectories
language/ Ott definitions of source language, pdfs as well
mips/ Sail definition of a MIPS specification
cheri/ Sail definition of a Cheri specification
risc-v/ abandoned very partial attempt at RISC V specification
l3-to-l2/ abandoned but not GC-ed directory
language directory
l2_parse.ott Grammar of Sail generated by parser, superset of source language
l2.ott Grammar of Sail source
l2_typ.ott Grammar of Internal structures used for type annotations
l2_rules.ott Rules for type system
type_system.tex Source of type system LaTeX document
Relevant make commands:
make Builds pdfs for l2 and l2_parse, ml and lem files of grammars
Generated files
l2.pdf combines grammar of l2.ott l2_typ.ott and rules of l2_rules.ott
l2_parse.pdf grammar of l2_parse.ott only
l2.ml grammar of l2.ott only, used by type checker
l2_parse.ml grammar of l2_parse.ott only, used by parser and initial check
l2.lem combines grammar of l2.ott and l2_typ.ott, used by interpreter
src directory (including some generated files)
ast.ml symlink to language/l2.ml
demo.sh script for setting up a demo
finite_map.ml utility implementation
gen_lib/ source directory of libaries used by generated back ends
initial_check.ml translate l2_parse grammar to l2 grammar
initial_check_full.ml performs sames checks as above as to kind well-formedness but over l2 grammar
lem_interp/ source directory of interpreter
lexer.mll
myocamlbuild.ml
parse_ast.ml symlink to language/l2_parse.ml
parse.mly
pp.ml utility for printing
pprint/ library directory of someone else's pretty printing combinators
pre_lexer.mll First pass lexer, to identify type identifiers
pre_parser.mly First pass parser, to identify type identifiers for actual parsing
pretty_print.ml our printers; one to Sail source, one to Lem ast, one to Lem, and one to Ocaml
process_file.ml
reporting_basic.ml
rewriter.ml performs sail-to-sail transformations for various back ends
sail.ml main file
sail.native executable for Sail
sail_lib.ml treat some sail functions as a library, for idl/power generation
spec_analysis.ml analyses a fully type annotated ast, primarily used by rewriters
test/ directory of test suite
type_check.ml Main type checker
type_internal Structure of internal types, and type - type comparisons
util.ml
Relevant make commands:
make Builds Sail executable (does not remake language files automatically)
make interpreter Builds sail interpeter
make run_mips.native Builds an executable sequential interpreter for MIPS Elf binaries
make clean
lem_interp directory
instruction_extractor.lem processes a specification and identifies the ast nodes of instructions with appropriate tags to convert data types into/out of sail value type
interp.lem interpreter implementation
interp_ast.lem symlink to language/l2.lem
interp_inter_imp.lem implementation of externally visible interface
interp_interface.lem externally visible interface for memory
interp_lib.lem implementation of sail library functions
interp_utilities.lem commonly useful functions for interpreter
sail_impl_base.lem externally visible interface above interp_interface
pretty_interp.ml pretty printing for interperter forms
run_interp.ml interactive implementation for running interpreter with simple memory and registers, bitrotted
run_interp_model.ml interactive implementation for running sequential binaries
run_with_elf.ml hook run_interp_model up with elf support, main file of sequential interpreter
run_with_elf_cheri.ml as above but specific to cheri
run_with_elf_cheri128.ml
type_check.lem implementation to type check fully inferenced, annotated, ast nodes (not complete)
|
