Merge branch 'master' of bitbucket.org:Peter_Sewell/sail

Conflicts:
	language/manual.pdf

1 files changed, 41 insertions, 12 deletions

diff --git a/README b/README
index b02fce6d..9c968b28 100644
--- a/README
+++ b/README
@@ -13,6 +13,8 @@ specification 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
@@ -52,9 +54,9 @@ 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.
+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:
@@ -65,7 +67,6 @@ 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
@@ -83,7 +84,7 @@ 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. 
+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.
@@ -102,7 +103,7 @@ The Sail interpreter relies on external access to two external tools:
     a public Bitbucket repository
     https://bitbucket.org/Peter_Sewell/linksem
 
-The Sail build system expects to find these repositories in in the same
+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
 
@@ -162,8 +163,24 @@ 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
+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.
+
 
 
 ******************************************************************************
@@ -176,6 +193,7 @@ 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
 
@@ -184,6 +202,7 @@ 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
@@ -199,7 +218,9 @@ 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
@@ -209,14 +230,14 @@ 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
+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
-run_power.native        executable for interpreting power model with simple memory
-run_tests.native        executable to run test suite
+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
@@ -229,11 +250,19 @@ make run_mips.native Builds an executable sequential interpreter for MIPS Elf bi
 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
+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)