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
|
The Sail ISA specification language
===================================
Overview
========
Sail is a language for describing the instruction-set architecture
(ISA) semantics of processors. Sail aims to provide a
engineer-friendly, vendor-pseudocode-like language for describing
instruction semantics. It is essentially a first-order imperative
language, but with lightweight 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/>.
<p>
Given a Sail definition, the tool will type-check it and generate
executable emulators, in C and OCaml, theorem-prover definitions for
Isabelle, HOL4, and Coq, and definitions to integrate with our
<a href="http://www.cl.cam.ac.uk/users/pes20/rmem">RMEM</a> tool for
concurrency semantics. This is all work in progress, and some
theorem-prover definitions do not yet work for the more complex
models; see the most recent papers and the ARMv8.5-A model for
descriptions of the current state.
<p>
<img src="https://www.cl.cam.ac.uk/~pes20/sail/overview-sail.png">
<p>
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/))
* Generated Isabelle snapshots of some ISA models, 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/))
Sail ISA Models
===============
Sail is currently being used for ARM, RISC-V, MIPS, CHERI-MIPS, IBM Power, and x86 models, variously ranging from full definitions to core user-mode fragments, and either here or in separate repositories:
### REMS Models
* [Sail ARMv8.5-A ISA model, automatically generated from the ARM-internal ASL reference, as used in the ARM ARM](https://github.com/rems-project/sail-arm).
* [Sail ARMv8.3-A ISA model](https://github.com/rems-project/sail/tree/sail2/arm). This is the "public" model described in our [POPL 2019 paper](http://www.cl.cam.ac.uk/users/pes20/sail/sail-popl2019.pdf), now largely superseded by the above.
* [Sail ARMv8-A ISA model, handwritten](https://github.com/rems-project/sail/tree/sail2/arm). This is a handwritten user-mode fragment.
* [Sail RISC-V ISA model, handwritten](https://github.com/rems-project/sail-riscv).
* [Sail MIPS and CHERI-MIPS ISA models, handwritten](https://github.com/CTSRD-CHERI/sail-cheri-mips).
* [Sail IBM POWER ISA model, automatically generated from IBM XML documentation](https://github.com/rems-project/sail/tree/sail2/power). This is a user-mode fragment.
* [Sail x86 ISA model, handwritten](https://github.com/rems-project/sail/tree/sail2/x86). This is a handwritten user-mode fragment.
The hand-written ARMv8-A, IBM POWER, and x86 models are currently not in sync
with the latest version of Sail, which is the (default) sail2 branch
on Github. These and the RISC-V model are integrated with our [RMEM](http://www.cl.cam.ac.uk/users/pes20/rmem) tool for concurrency semantics.
### External Models
* [Sail 32-bit RISC-V model, partially handwritten and partially generated](https://github.com/thoughtpolice/rv32-sail). This currently implements a fragment of the machine mode (-M) specification for RV32IM. (Developed independently of the full RISC-V model for the REMS project.)
OPAM Installation
=================
See [INSTALL.md](INSTALL.md) for how
to install Sail using opam (recommended).
Building
========
See [BUILDING.md](BUILDING.md) for full details of how to build Sail from source
with all the required dependencies.
Emacs Mode
==========
[editors/sail-mode.el](editors/sail-mode.el) contains an Emacs mode
for the most recent version of Sail which provides some basic syntax
highlighting.
VSCode Mode
===========
[editors/vscode](editors/vscode) contains a Visual Studio Code mode
which provides some basic syntax highlighting. It is also available
on the VSCode Marketplace.
CLion/PyCharm Syntax highlighting
===========
[editors/vscode/sail](editors/vscode/sail) contains a Visual Studio Code
mode which provides some basic syntax highlighting. CLion/PyCharm can also
parse the [editors/vscode/sail/syntax/sail.tmLanguage.json](sail.tmLanguage.json)
file and use it to provide basic syntax highlighting.
To install open `Preferences > Editor > TextMate Bundles`. On that settings
page press the `+` icon and locate the [editors/vscode/sail](editors/vscode/sail)
directory.
This requires the [TextMate Bundles plugin](https://plugins.jetbrains.com/plugin/7221-textmate-bundles).
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.
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 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 models in separate repositories are licensed as described in each.
## Funding
This software was developed within the Rigorous Engineering of
Mainstream Systems (REMS) project, partly funded by EPSRC grant
EP/K008528/1, at the Universities of Cambridge and Edinburgh.
This software was developed by SRI International and the University of
Cambridge Computer Laboratory (Department of Computer Science and
Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV").
|
