| Age | Commit message (Collapse) | Author |
|---|
|
When we are building from git, we put the git version info in manifest.ml, so
we'll get the following from sail -v
Sail $last_git_tag ($branch @ $commit_sha)
If we are be built from opam we can't assume we are in a git repository as
opam downloads specific tags as tarballs, so instead we check for the precense
of SHARE_DIR which is set by our opam build script, and instead output
Sail 0.8 (sail2 @ opam)
which is the next git tag (current is 0.7.1, this must be updated by hand),
the branch name from which opam releases are generated and then opam rather
than the commit SHA.
I also removed the Makefile-non-opam file as it's bitrotted and unused
|
|
|
|
|
|
|
|
builds this defaults to git root.
|
|
files in installed location.
|
|
their respective subdirectories.
|
|
Turns out that BSD sed is not a subset of GNU sed, GNU sed doesn't
allow a space after the -i option.
|
|
For GNU sed, the extension is optional in
sed -i ...
But in BSD sed, the extension is mandatory
sed -i .bak ...
|
|
Rename l2.ott to sail.ott
|
|
|
|
Rather than just using strings to represent literals, now use value
types from sail_lib.lem to represent them. This allows for expressions
to be evaluated at compile time, which will be useful for future
optimisations involving constant folding and propagation, and allows
the intermediate bytecode to be interpreted using the same lem
builtins that the shallow embedding uses.
To get this to work I had to tweak the build process slightly to allow
ml files to import lem files from gen_lib/. Hopefully this doesn't
break anything!
|
|
|
|
|
|
Describes precisely the intermediate representation used in the C
backend in an ott grammar, and also removes several C-isms where raw C
code was inserted into the IR, so in theory this IR could be
interpreted by a small VM/interpreter or compiled to LLVM bytecode
etc. Currently the I_raw constructor for inserting C code is just used
for inserting GCC attributes, so it can safely be ignored.
Also augment and refactor the instruction type with an aux constructor
so location information can be propagated down to this level.
|
|
|
|
|
|
|
|
|
|
Also updated some of the documentation in the sail source code
|
|
|
|
|
|
Add the ast.sed script we need to build sail. Currently we just need
this to fix up the locations in the AST but it will be removed once we
can share locations between ocaml and lem.
|
|
|
|
|
|
no longer there
|
|
Requires linenoise library (opam install linenoise) for readline
support. Use 'make isail' to build sail with interactive
support. Plain 'make sail' should work as before with no additional
dependencies.
Use 'sail -i <commands>' to run sail interactively, e.g.
sail -new_parser -i test/ocaml/prelude.sail test/ocaml/trycatch/tc.sail
then try some commands for typechecking and evaluation
sail> :t main
sail> main ()
Doesn't use the lem interpreter right now, instead has a small
operational semantics in src/interpreter.ml, but this is not very
complete and will be changed/removed.
|
|
|
|
|
|
|
|
Instruction extractor code that I commented out in this commit seems
buggy anyway - it will claim that the length of all bitvectors is 64?!
|
|
Need to map sail type annotations to interpreter type annotations in lem_ast ouput. This doesn't seem too hard.
|
|
|
|
Fix until loop not being counted as sugar
|
|
|
|
as GPR
This was wrongly translated as an update of the vector of references.
|
|
|
|
Note: The effect annotations of the execute function differ between CHERI and
MIPS, so I split out a new file mips_ast_decl.sail for MIPS with just the
initial declarations of ast, decode, and execute (with the right effects for
MIPS).
|
|
|
|
- Correctly pass exponentials to Z3
- Infer types of functional record updates
- Support "def Nat"
|
|
Modified initial_check.ml so it no longer requires type_internal. It's
still needs cleaned up in a few ways. Most of the things it's trying
to do could be done nicer if we took some time to re-factor it, and
some of the things should just be handled by the main typechecker,
leaving it as a think layer between the parse_ast and the ast.
Now that's done everything can be switched to the new typechecker and
the _new suffixes were deleted from everything except the
monomorphisation pass because I don't know the status of that.
|
|
|
|
|
|
|
|
neater access to registers of single bit.
|
|
dependency on ocaml uint library by using it.
|
|
enable gprof profiling)
|
|
|
|
|
|
between them using a command line switch.
|
