diff options
Diffstat (limited to 'README')
| -rw-r--r-- | README | 236 |
1 files changed, 0 insertions, 236 deletions
diff --git a/README b/README deleted file mode 100644 index f5aaeeff..00000000 --- a/README +++ /dev/null @@ -1,236 +0,0 @@ -Sail README - -[Note that this describes the original Sail language, on the github master branch. The current development version, on the github sail2 branch, is somewhat different; documentation for that is in progress] - - -Kathryn E. Gray and Peter Sewell -15 March 2017 - -******************************************************************** -OVERVIEW - -Sail is a language for describing the instruction semantics of -processors. It has been used in several papers, available from -http://www.cl.cam.ac.uk/~pes20/sail/ - -This repository contains the implementation of Sail, together with -related tools and some Sail specifications: - -- a manual, manual.pdf - -- 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 - -We also have a substantial IBM POWER ISA specification, -which we can send by email. - - -************************************************************************** -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 Github repository - https://github.com/rems-project/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 Github repository - https://github.com/rems-project/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 - -************************************************************************** -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 how the MIPS -model is divided 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, one would need to adapt the -sequential sail interpreter, which evaluates the specification on an -ELF file. - -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 - -To generate OCaml output for fast sequential evaluation, one uses the -sail executable with flag: -./sail mips/mips.sail -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 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 -type_system.tex Source of type system LaTeX document - -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) - |