diff options
Diffstat (limited to 'README')
| -rw-r--r-- | README | 19 |
1 files changed, 11 insertions, 8 deletions
@@ -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 |