path: root/README

# 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;

- 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

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 a substantial IBM POWER ISA specification
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 Robert Norton Wright or 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).

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

***************************************************************************
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: -ocaml
The resulting output of these commands may well be untype checkable 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
manual.tex      Source of manual

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)