package sail_manifest

You can search for identifiers within the package.

in-package search v0.2.0

Helper tool for compiling Sail

Install

Dune Dependency

github.com Readme BSD-2-Clause License Edit opam file Versions (4)

Authors

Maintainers

S

Sail Devs <cl-sail-dev@lists.cam.ac.uk>

Sources

sail-0.17.1.tbz

sha256=11463fe0bb4a494dab408598d37e7a065ffab348753e3134e964edb56da896a2

sha512=3ea18086992e07414d474bf3b604b6927d7dee313fb475e9bb1fdf4f7c0e10f7d4b0143c8e6670f90db335d3a8fcd507f777a9e3a98051be343e0d101fd8b9a4

README.md.html

README.md

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/.

Given a Sail definition, the tool will type-check it and generate documentation, executable emulators (in C and OCaml), theorem-prover definitions (for Isabelle, HOL4, and Coq), and definitions to integrate with our RMEM and isla-axiomatic tools for concurrency semantics. The Isla engine provides SMT-based symbolic evaluation for Sail models, and the Islaris verification tool integrates Isla output with the Iris program logic to support proof about binary code in Coq. Not all models are integrated with all tools - see the most recent papers and models for descriptions of the current state.

This repository contains the implementation of Sail, together with some Sail specifications and related tools.

A manual, manual.pdf with source (in doc/)
The Sail source code (in src/)
Generated Isabelle snapshots of some ISA models, in snapshots/isabelle
Documentation for generating Isabelle and working with the ISA specs in Isabelle in lib/isabelle/manual.pdf
Simple emacs and VSCode modes with syntax highlighting (in editors/)
A test suite for Sail (in test/)

The support library for Coq models is in a separate repository to help our package management.

Sail ISA Models

Sail is currently being used for Arm-A, Morello (CHERI-Arm), RISC-V, CHERI-RISC-V, MIPS, CHERI-MIPS, IBM Power, and x86 models, variously ranging from full definitions (able to boot an OS in the Sail-generated emulator) to core user-mode fragments:

REMS Models

Sail Armv9.3-A and Armv8.5-A ISA models, automatically generated from the Arm-internal ASL reference, as used in the Arm ARM.
Sail Armv8.3-A ISA model. This is the "public" model described in our POPL 2019 paper, now largely superseded by the above.
Sail Armv8-A ISA model, handwritten. This is a handwritten user-mode fragment.
Sail Morello (CHERI-Arm) ISA model, automatically generated from the Arm-internal ASL definition. This was the basis for our Morello security proofs.
Sail RISC-V ISA model, handwritten. This has been adopted by the RISC-V Foundation.
Sail MIPS and CHERI-MIPS ISA models, handwritten.
Sail IBM POWER ISA model, automatically generated from IBM XML documentation. This is a user-mode fragment.
Sail x86 ISA model, handwritten. This is a handwritten user-mode fragment.

The hand-written 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 tool for concurrency semantics.

External Models

Sail 32-bit RISC-V model, partially handwritten and partially generated. 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.)

Installation

See INSTALL.md for how to install Sail using opam.

Emacs Mode

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 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 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 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 directory.

This requires the TextMate Bundles plugin.

Vim

editors/vim contains support for syntax highlighting in the vim editor, in vim's usual format of an ftdetect directory to detect Sail files and a syntax directory to provide the actual syntax highlighting.

Logo

etc/logo contains the Sail logo

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.5 and Armv8.3 models are copyright Arm Ltd, and distributed under a BSD Clear licence. See https://github.com/meriac/archex, and the README file 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 work was partially supported by the UK Government Industrial Strategy Challenge Fund (ISCF) under the Digital Security by Design (DSbD) Programme, to deliver a DSbDtech enabled digital platform (grant 105694). This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 789108, ELVER). This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous Engineering for Mainstream Systems, an ARM iCASE award, and EPSRC IAA KTF funding. This work was partially supported by donations from Arm and Google. Approved for public release; distribution is unlimited. This research is sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 ("CTSRD") and FA8650-18-C-7809 ("CIFV"). The views, opinions, and/or findings contained in these articles OR presentations are those of the author(s)/presenter(s) and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.