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
234
235
236
237
|
# Readme
Guide to Sail, as of Feb 25, 2016.
********************************************************************
OVERVIEW
This repository provides several tools relating to the Sail
specification language:
- sail, the type checker and compiler for programs in the Sail
language;
- an example Sail specification of a MIPS processor (in mips/)
- 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
There is also the beginnings of a manual, in manual.pdf. This
currently just describes the language syntax, type system, common
library, and a few tips for sail development; it doesn't yet really
explain the language. We can answer questions either by mail or some
google/skype chat.
Elsewhere we have substantial IBM POWER and ARM Sail specifications
which we can send by email.
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 why the MIPS
model is devided 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, there is the sequential
sail interpreter, which evaluates the specification on an ELF file. At
present, doing this for a new architecture will require conversation
with Kathy Gray, as the connections within the sail interpreter
implementation to the architecture being simulated have not been
factored out into external specification files.
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).
*** In progress. Does not work yet ***
To generate Lem specifications for theorem proving, one uses the sail
executable with flag:
./sail mips/mips.sail -lem
*** In progress. Does not work yet ***
To generate OCaml output for fast sequential evaluation, one uses the
sail executable with flag:
./sail mips/mips.sail -ocaml
**************************************************************************
BUILDING
SAIL COMPILER
The Sail compiler requires OCaml; it is tested on version 4.02.3.
Run "make" in the top level l2 directory; this will generate an executable
called sail in this directory.
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 private Bitbucket repository.
The Sail build system expects to find these repositories in in the same
directory as the l2 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 l2/editors
***************************************************************************
RUNNING SAIL compiler
./sail test.sail % Type check sail file, do not generate any output.
% Multiple files can be listed, the resulting specification is
% equivalent to a concatenation in order of the given files
Command-line options
-verbose pretty-print out the file
-lem_ast pretty-print a Lem AST representation of the file, for the interpreter
-lem print a Lem translated version of the specification
-ocaml print an Ocaml translated version of the specification
-skip_constraints skip constraint resolution in type-checking (*Not recommended*)
-lem_lib provide additional library to open in Lem output
-ocaml_lib provide additional library to open in Ocaml output
-v print version
-o select output filename prefix
-help Display this list of options
--help Display this list of options
Usage
./sail test.sail foo.sail -o spec -lem_ast -ocaml
Will generate the files spec.lem and spec.ml in the current directory
It is not recommended to try to read the generated Lem ast file, as it is a very verbose
representation of the AST.
IN PROGRESS COMMANDS: -lem -ocaml
The resulting output of these commands may well be untype checkable Lem or OCaml
******************************************************************************
DIRECTORY STRUCTURE
Sail sources and binaries are to be found in the directories of
bitbucket/l2 (to be renamed when we make sail public in a
bitbucket/sail respository (hopefully)
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
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
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
initial_check.ml translate l2_parse grammar to 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
process_file.ml
reporting_basic.ml
run_power.native executable for interpreting power model with simple memory
run_tests.native executable to run test suite
sail.ml main file
sail.native executable for Sail
sail_lib.ml treat some sail functions as a library, for idl/power generation
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
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
pretty_interp.ml pretty printing for interperter forms
run_interp.ml interactive implementation for running interpreter with simple memory and registers
|
