1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
|
# Readme
Guide to Sail, as of Feb 25, 2016.
Note: the repository name intends to change to sail for a public release
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
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
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
l2.ott Grammar of Sail source
l2_typ.ott Grammar of Internal structures used for type annotations
l2_rules.ott Rules for type system
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
initial_check.ml translate l2_parse grammar to 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
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
sail.ml main file
sail.native executable for Sail
sail_lib.ml treat some sail functions as a library, for idl/power generation
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
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
pretty_interp.ml pretty printing for interperter forms
run_interp.ml interactive implementation for running interpreter with simple memory and registers
|
