diff options
| -rw-r--r-- | Makefile | 15 | ||||
| -rw-r--r-- | README | 112 |
2 files changed, 79 insertions, 48 deletions
@@ -1,9 +1,10 @@ .PHONY: all sail language clean power test -all: sail interpreter language +all: sail -sail: language +sail: $(MAKE) -C src + ln -s src/sail.native sail language: $(MAKE) -C language @@ -11,14 +12,6 @@ language: interpreter: $(MAKE) -C src interpreter -test: - $(MAKE) -C src test - -power: - $(MAKE) -C src power - -test_power_interactive: - $(MAKE) -C src test_power_interactive - clean: $(MAKE) -C src clean + rm sail @@ -1,18 +1,77 @@ # Readme -Guide to Sail, as of August 6 2014. Subject to possible change later. +Guide to Sail, as of Feb 25, 2016. -Sail relies on external access to Lem, Ott, Lem libraries, and Power -binaries for some testing, as well as Ocaml 4.01.0 or later. Some -dependencies are at present hard coded paths in makefiles. Thus -Sail expects to find a directory structure as the following -External directory structure: -Sail to be found in BASE/bitbucket/l2 -Lem to be found in BASE/bitbucket/lem -idl to be found in BASE/rsem/idl +Note: the repository name intends to change to sail for a public release -(BASE might have to be the user homedirectory, but many connections -are using ../../ etc) +BUILDING + +The Sail type checker and compiler requires OCaml; it is tested +on version 4.02.3. + +Run make in the top level l2 directory; this will generate an executable +called sail in this directory. + +make clean will remove this executable as well as the build files in +subdirectories. + +The Sail interpreter relies on external access to Lem and Linksem +for building and running the interpreter. + +Lem is a public bitbucket git repository. Linksem is a private bitbucket +mercurial repsotory + +The Sail build system expects to find these repositories in in the same +directory as the l2 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. + +EMACS MODE + +There is an emacs mode implementation very similar to the Tuareg mode in l2/editors + +RUNNING SAIL compiler + +./sail test.sail % Type check sail file, do not generate any output. + % Multiple files can be listed, the resulting specification is + % equivalent to a concatenation in order of the given files + +Command-line options + -verbose pretty-print out the file + -lem_ast pretty-print a Lem AST representation of the file, for the interpreter + -lem print a Lem translated version of the specification + -ocaml print an Ocaml translated version of the specification + -skip_constraints skip constraint resolution in type-checking (*Not recommended*) + -lem_lib provide additional library to open in Lem output + -ocaml_lib provide additional library to open in Ocaml output + -v print version + -o select output filename prefix + -help Display this list of options + --help Display this list of options + + +Usage + +./sail test.sail foo.sail -o spec -lem_ast -ocaml + +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 + + +DIRECTORY STRUCTURE Sail sources and binaries are to be found in the directories of bitbucket/l2 (to be renamed when we make sail public in a @@ -21,14 +80,9 @@ bitbucket/sail respository (hopefully) Top level directories src/ ML implementation of Sail frontend, Sail executable, subdirectories language/ Ott definitions of source language, pdfs as well -l3-to-l2/ Directory for student to define l3-to-l2 translation, abandoned? - -Relevant make commands: -make Builds Sail executable -make test As above, also builds interpreter, and runs test suite -make power As above (except running) and builds executable interpreting power binary -make clean Cleans src and language - +mips/ Sail definition of a MIPS 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 @@ -75,16 +129,10 @@ util.ml Relevant make commands: make Builds Sail executable (does not remake language files automatically) -make test As above, also builds interpreter, and runs test suite -make power As above (except running) and builds executable interpreting power binary -make test_power As above, runs power binary found in idl/power/binary +make interpreter Builds sail interpeter +make run_mips.native Builds an executable sequential interpreter for MIPS Elf binaries make clean -Using sail executable -./sail.native -h % Lists command line flags -./sail.native test.sail -lem_ast % typical usage to generate a lem_ast file test.lem -./sail.native test.sail -verbose % resulting sail is not typecheckable - lem_interp directory interp.lem interpreter implementation interp_ast.lem symlink to language/l2.lem @@ -94,13 +142,3 @@ interp_lib.lem implementation of sail library functions pretty_interp.ml pretty printing for interperter forms run_interp.ml interactive implementation for running interpreter with simple memory and registers - -test directory -idempotence.sh script to test the pretty printer, but files might not pass type checking for predictable reasons -pattern.sail part of test suite, testing pattern match -power.sail extract of subset of power instructions: NOT JUST USED FOR TESTING -regbits.sail part of test suite, testing register declarations -run_power.ml framework to read memory, and run power in interpreter -run_tests.ml framework for running test suite -testN.sail various test suite files, based on past bugs -vectors.sail part of test suite, testing vector operations |