From d1a822bb1f1853de90b14c9ef46b15800cc5a1be Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Mon, 30 Jan 2017 10:08:48 +0000 Subject: Restore manual.tex, accidentally deleted Minor updates to README, still in progress --- README | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) (limited to 'README') diff --git a/README b/README index b02fce6d..fbc0fc4b 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,8 @@ 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 ****************************************************************************** @@ -176,6 +177,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 +186,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 -- cgit v1.2.3 From 0189ef186771a7f5ea40a750dc0b9922ff8adbf5 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Mon, 30 Jan 2017 10:19:44 +0000 Subject: updated readme --- README | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) (limited to 'README') diff --git a/README b/README index fbc0fc4b..8f649a81 100644 --- a/README +++ b/README @@ -202,7 +202,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 @@ -212,14 +214,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 @@ -232,11 +234,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) -- cgit v1.2.3 From d8041f29ad728320ca763ff3852508b617592b1a Mon Sep 17 00:00:00 2001 From: Peter Sewell Date: Fri, 3 Feb 2017 14:14:54 +0000 Subject: licensing --- README | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'README') diff --git a/README b/README index 8f649a81..9c968b28 100644 --- a/README +++ b/README @@ -167,6 +167,22 @@ 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 -- cgit v1.2.3