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
|
The Sail ISA specification language
===================================
Overview
========
Sail is a language for describing the instruction semantics of
processors. Sail aims to provide a engineer-friendly,
vendor-pseudocode-like language for describing instruction
semantics. It is an imperative language containing some advanced
features like dependent typing for numeric types and bitvector
lengths, which are automatically checked using Z3. It has been used
for several papers, available from http://www.cl.cam.ac.uk/~pes20/sail/
This repository contains the implementation of Sail, together with
some Sail specifications and related tools.
* A manual, [manual.pdf](manual.pdf) with source (in [doc/](doc/))
* The Sail source code (in [src/](src/))
* A Sail specification of a MIPS ISA (in [mips/](mips/))
* A Sail specification of the CHERI MIPS ISA (in [cheri/](cheri/))
* A Sail specification of ARMv8.3-A generated from ARM's publically
released ASL specification (in [aarch64/](aarch64/))
* Generated Isabelle snapshots of the above ISAs in [snapshots/isabelle](snapshots/isabelle)
* Documentation for generating Isabelle and working with the ISA specs
in Isabelle in [snapshots/isabelle/Manual.pdf](snapshots/isabelle/Manual.pdf)
* A simple emacs mode with syntax highlighting (in [editors/](editors/))
* A test suite for Sail (in [test/](test/))
We also have versions of IBM POWER, a fragment of x86, and a
hand-written fragment of ARMv8-A, but these are currently not up-to-date
with the latest version of Sail, which is the (default) sail2 branch
on Github.
OPAM Installation
=================
See the following Sail [wiki
page](https://github.com/rems-project/sail/wiki/OPAMInstall) for how
to get pre-built binaries of Sail using OPAM.
Building
========
See [INSTALL.md](INSTALL.md) for full details of how to build Sail from source
with all the required dependencies.
Emacs Mode
==========
[editors/sail2-mode.el](editors/sail2-mode.el) contains an Emacs mode
for the most recent version of Sail which provides some basic syntax
highlighting. [editors/sail-mode.el](editors/sail-mode.el) contains an
emacs mode for previous versions of the language.
Licensing
=========
The Sail implementation, in src/, as well as its tests in test/ and
other supporting files in lib/ and language/, 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 generated parts of the ASL-derived ARMv8.3 model in aarch64/ are
copyright ARM Ltd. See https://github.com/meriac/archex, and the
[README file](aarch64/README) in that directory.
The hand-written 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.
The x86 model in x86/ is distributed under the 2-clause BSD licence in
the headers of those files.
The POWER model in power/ is distributed under the 2-clause BSD licence in
the headers of those files.
The RISC-V model in riscv/ model is also distributed under the
2-clause BSD licence.
|
