Merge branch 'sail2' into mappings

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