| Age | Commit message (Collapse) | Author |
|---|
|
Added library for simple integer arithmetic functions in lib/arith.sail
WIP TeX file for formatting latex output included in lib/sail.tex
Fixes for bugs in sail_lib
|
|
|
|
|
|
- Update Lem bindings and extras files
- Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's
(used for cap_size in the CHERI spec)
- Add Lem and Isabelle Makefile targets for CHERI
|
|
|
|
Add a flag to Sail that allows for an image of an elf file to be
dumped in a simple format using linksem, used as
sail -elf test.elf -o test.bin
This image file can then be used by a compiled C version of a sail
spec as with ocaml simply by
./a.out test.bin
|
|
|
|
intialising and dumping CHERI state. Somewhat working cheri sail2 model.
|
|
|
|
Fixed an issue with pattern matching on enums
Fixed an issue whereby fix_early_returns would cause memory leaks
Added optimizations for some of the builtins used in the decode
function. Optimizations are turned on with the -O flag.
|
|
to_get_slice_int in less confusing way. Add arithmetic shift right.
|
|
Also update the main aarch64 (no_vector) spec with latest asl_parser
|
|
|
|
|
|
passing tests.
|
|
|
|
|
|
|
|
This removes all type polymorphism, so we can generate optimized
bitvector code and compile to languages without parametric
polymorphism.
|
|
|
|
Fixed test cases for ocaml backend and interpreter
|
|
|
|
New testcase for bitfield syntax
Updated to work with latest lem and linksem
|
|
|
|
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.
|
|
|
|
|
|
will be reflected in short hand type syntax, inc is still the default if undeclared
So:
default order dec
register bit[32] t (* Declares t as a decreasing vector, starting at 31 on the left and decreasing to 0 *)
default order inc
register bit[32] o (* Declares o as an increasing vector, starting at 0 on the left and increasing to 31 *)
It is presently possible to change the default mid-file; this is almost certainly bad and I will turn it into an error soon.
|
|
|
|
|
|
Used by the Power XML extraction tool.
|
