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
|
# Readme
Guide to Sail, as of August 6 2014. Subject to possible change later.
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
(BASE might have to be the user homedirectory, but many connections
are using ../../ etc)
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
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
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 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 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
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
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
|
