# 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/mips.sail) - 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.sail 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 mips/mips.sail -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