| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Change internal terminology so we more clearly distinguish between a list of
definitions 'defs' and functions that take an entire abstract syntax
trees 'ast'.
|
|
This refactoring is intended to allow this type to have more than just a
list of definitions in future.
|
|
Reformats input source code using the pretty printer preserving the file
structure. Probably not useable as an ocamlformat or rustfmt like tool,
but good enough to take generated code without formatting and make it
readable.
|
|
Insert $file_start and $file_end pragmas in the AST, as well as
$include_start and $include_end pragmas so we can reconstruct the
original file structure later if needed, provided nothing like
topological sorting has been done.
Have the Lexer produce a list of comments whenever it parses a file,
which can the be attached to the nearest nodes in the abstract syntax
tree.
|
|
- rename files to get rid of prefix
- use -Q to get package name right
- add Base.v to make package imports simpler
- add opam file for coq package
|
|
Allows clients of sail as a library to define custom symbols for $ifdef
and $ifndef
Iterate vector concat assignment and tuple assignment to handle unusual
nesting cases when compiling to C. These rewrites should really be one
rewrite anyway though!
Don't add type annotations when introducing tuple patterns during
rewriting. I guess not adding them could also cause an error in some
circumstances, but if that's the case it could probably be fixed by
tweaking some rules in the type-checker.
|
|
Also don't include the toplevel files in the library, and move
load_files and descatter into process_file where they can be called
|
|
Also make the Error type private, so it's only constructed through the
functions we expose in reporting.mli
|
|
-coq_alt_modules2 <filename> provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default definitions of MR and M monads
|
|
|
|
|
|
|
|
Fix SMT mem_builtin test case
|
|
|
|
- allow disjoint_pat to be used on patterns that have just been introduced
by the rewrite without rechecking
- don't rebuild the matched expression in the generated fallthrough case
(or any wildcard fall-through) - it may be dead code and generate badly
typed Lem
- update the type environment passed to rewrites whenever type checking
is performed; stale information broke some rewrites
|
|
|
|
Also add a $suppress_warnings directive that ensures that no warnings
are generated for a specific file.
|
|
Only change that should be needed for 99.9% of uses is to change
vector('n, 'ord, bit) to bitvector('n, 'ord), and adding
$ifndef FEATURE_BITVECTOR_TYPE
type bitvector('n, dec) = vector('n, dec, bit)
$endif
for to support any Sail before this
Currently I have all C, Typechecking, and SMT tests passing, as well
as the RISC-V spec building OCaml and C completely unmodified.
|
|
|
|
Fixes #46
|
|
- Rename DeIid to Operator. It corresponds to operator <string> in the
syntax. The previous name is from when it was called deinfix in
sail1.
- Removed things that weren't actually common from
pretty_print_common.ml, e.g. printing identifiers is backend
specific. The doc_id function here was only used for a very specific
use case in pretty_print_lem, so I simplified it and renamed it to
doc_sia_id, as it is always used for a SIA.Id whatever that is.
- There is some support for anonymous records in constructors, e.g.
union Foo ('a : Type) = {
MkFoo : { field1 : 'a, field2 : int }
}
somewhat similar to the enum syntax in Rust. I'm not sure when this
was added, but there were a few odd things about it. It was
desugared in the preprocessor, rather than initial_check, and the
desugaring generated incorrect code for polymorphic anonymous
records as above.
I moved the code to initial_check, so the pre-processor now just
deals with pre-processor things and not generating types, and I
fixed the code to work with polymorphic types. This revealed some
issues in the C backend w.r.t. polymorphic structs, which is the
bulk of this commit. I also added some tests for this feature.
- OCaml backend can now generate a valid string_of function for
polymorphic structs, previously this would cause the ocaml to fail
to compile.
- Some cleanup in the Sail ott definition
- Add support for E_var in interpreter previously this would just
cause the interpreter to fail
|
|
Rather than having a separate variable for each backend X,
opt_print_X, just have a single variable opt_print_target, where
target contains a string option, such as `Some "lem"` or `Some
"ocaml"`, then we have a function target that takes that string and
invokes the appropriate backend, so the main function in sail.ml goes
from being a giant if-then-else block to a single call to
target !opt_target ast env
This allows us to implement a :compile <target> command in the
interactive toplevel
Also implement a :rewrites <target> command which performs all the
rewrites for a specific target, so rather than doing e.g.
> sail -c -O -o out $FILES
one could instead interactively do
> sail -i
:option -undefined_gen
:load $FILES
:option -O
:option -o out
:rewrites c
:compile c
:quit
for the same result.
To support this the behavior of the interactive mode has changed
slightly. It no longer performs any rewrites at all, so a :rewrites
interpreter is currently needed to interpret functions in the
interactive toplevel, nor does it automatically set any other flags,
so -undefined_gen is needed in this case, which is usually implied by
the -c flag.
|
|
When adding a constraint such as `x <= 2^n-1` to an environment
containing e.g. `n in {32, 64}` or similar, we can enumerate all
values of n and add `n == 32 & x <= 2^32-1 | n == 64 & x <= 2^64-1`
instead. The exponentials then get simplified away, which means that
we stay on the SMT solver's happy path.
This is enabled by the (experimental, name subject to change) flag
-smt_linearize, as this both allows some things to typecheck that
didn't before (see pow_32_64.sail in test/typecheck/pass), but also
may potentially cause some things that typecheck to no longer
typecheck for SMT solvers like z3 that have some support for reasoning
with power functions, or where we could simply treat the exponential
as a uninterpreted function.
Also make the -dsmt_verbose option print the smtlib2 files for the
solve functions in constraint.ml. We currently ignore the -smt_solver
option for these, because smtlib does not guarantee a standard format
for the output of get-model, so we always use z3 in this case.
Following the last commit where solve got renamed solve_unique, there
are now 3 functions for solving constraints:
* Constraint.solve_smt, which finds a solution if one exists
* Constraint.solve_all_smt, which returns all possible
solutions. Currently there's no bound, so this could loop forever if
there are infinite solutions.
* Constraint.solve_unique, which returns a unique solution if one exists
Fix a bug where $option pragmas were dropped unnecessarily.
|
|
For example, in
type xlen : Int = 64
type xlenbits = bits(xlen)
rewrite the 'xlen' in the definition of 'xlenbits' to the constant 64 in
order to simplify Lem generation. In order to facilitate this, pass
through the global typing environment to the rewriting steps (in the AST
itself, type definitions don't carry annotations with environments).
|
|
Fix monomorphisation tests
|
|
Allow a file sail.json in the same directory as the sail source file
which contains the ordering and options needed for sail files involved
in a specific ISA definition. I have an example for v8.5 in sail-arm.
The interactive Sail process running within emacs then knows about the
relationship between Sail files, so C-c C-l works for files in the ARM
spec. Also added a C-c C-x command to jump to a type error. Requires
yojson library to build interactive Sail.
|
|
Can now use C-c C-s to start an interactive Sail process, C-c C-l to
load a file, and C-c C-q to kill the sail process. Type errors are
highlighted in the emacs buffer (like with merlin for OCaml) with a
tooltip for the type-error, as well as being displayed in the
minibuffer. Need to add a C-c C-x command like merlin to jump to the
error, and figure out how to handle multiple files nicely, as well as
hooking the save function like tuareg/merlin, but this is already
enough to make working with small examples quite a bit more pleasant.
|
|
|
|
|
|
If we use the bitlist representation of bitvectors, the type argument in
type abbreviations such as "bits('n)" becomes dead, which confuses HOL;
as a workaround, expand type synonyms in this case.
|
|
|
|
We want to ensure that no_devices.sail and devices.sail have the same
effect footprint, because with a snapshot-type release in sail-arm, we
can't rebuild the spec with asl_to_sail every time we switch from
running elf binaries to booting OS's. This commit allows registers to
have arbitrary effects, so registers that are really representing
memory-mapped devices don't have to have the wmem/rmem effect.
|
|
Remove unused name schemes and DEF_kind
|
|
Work on improving the formatting and quality of error messages
When sail is invoked with sail -i, any type errors now drop the user
down to the interactive prompt, with the interactive environment being
the environment at the point the type error occurred, this means the
typechecker state can be interactively queried in the interpreter to help
diagnose type errors.
|
|
|
|
Mostly this is to change how we desugar types in order to make us more
flexible with what we can parse as a valid constraint as
type. Previously the structure of the initial check forced some
awkward limitations on what was parseable due to how the parse AST is
set up.
As part of this, I've taken the de-scattering of scattered functions
out of the initial check, and moved it to a re-writing step after
type-checking, where I think it logically belongs. This doesn't change
much right now, but opens up some more possibilities in the future:
Since scattered functions are now typechecked normally, any future
module system for Sail would be able to handle them specially, and the
Latex documentation backend can now document scattered functions
explicitly, rather than relying on hackish 'de-scattering' logic to
present documentation as the functions originally appeared.
This has one slight breaking change which is that union clauses must
appear before their uses in scattered functions, so
union ast = Foo : unit
function clause execute(Foo())
is ok, but
function clause execute(Foo())
union ast = Foo : unit
is not. Previously this worked because the de-scattering moved union
clauses upwards before type-checking, but as this now happens after
type-checking they must appear in the correct order. This doesn't
occur in ARM, RISC-V, MIPS, but did appear in Cheri and I submitted a
pull request to re-order the places where it happens.
|
|
|
|
|
|
The main changes so far are:
* Allow markdown formatting in doc comments. We parse the markdown
using Omd, which is a OCaml library for parsing markdown. The nice
thing about this library is it's pure OCaml and has no dependencies
other the the stdlib. Incidentally it was also developed at OCaml
labs. Using markdown keeps our doc-comments from becoming latex
specfic, and having an actual parser is _much_ nicer than trying to
hackily process latex in doc-comments using OCamls somewhat sub-par
regex support.
* More sane conversion latex identifiers the main approach is to
convert Sail identifiers to lowerCamelCase, replacing numbers with
words, and then add a 'category' code based on the type of
identifier, so for a function we'd have fnlowerCamelCase and for
type synonym typelowerCamelCase etc. Because this transformation is
non-injective we keep track of identifiers we've generated so we end
up with identifierA, identifierB, identifierC when there are
collisions.
* Because we parse markdown in doc comments doc comments can use Sail
identifiers directly in hyperlinks, without having to care about how
they are name-mangled down into TeX compatible things.
* Allow directives to be passed through the compiler to
backends. There are various $latex directives that modify the latex
output. Most usefully there's a
$latex newcommand name markdown
directive that uses the markdown parser to generate latex
commands. An example of why this is useful is bellow. We can also use
$latex noref id
To suppress automatically inserting links to an identifier
* Refactor the latex generator to make the overall generation process
cleaner
* Work around the fact that some operating systems consider
case-sensitive file names to be a good thing
* Fix a bug where latex generation wouldn't occur unless the directory
specified by -o didn't exist
This isn't quite all the requested features for good CHERI
documentation, but new features should be much easier to add now.
|
|
There is no Reporting_complex, so it's not clear what the basic is
intended to signify anyway.
Add a GitHub issue link to any err_unreachable errors (as they are all
bugs)
|
|
|
|
Now that Jenkins is updated to a newer version of OCaml we can finally
fix some warning with more recent versions of OCaml than 4.02.3. Also
fix a Lem test case that was failing.
|
|
Also allow options to be set via a pragma in Sail files
|
|
|
|
|
|
One day we will be free from the 4.02.3 menace, but today is not that day. :(
This should fix Sail on Jenkins
This reverts commit 86e29bcbb1597c4ef1f6cae8edbeed42f9a31414.
|
|
Changes are:
- String.capitalize -> String.capitalize_ascii
- String.uppercase -> String.uppercase_ascii
- String.lowercase -> String.lowercase_ascii
Basically just making the change that the warning message suggested.
|
|
E_internal_cast, E_sizeof_internal, E_internal_exp,
E_internal_exp_user, E_comment, and E_comment_struc were all
unused. For a lem based interpreter, we want to be able to compile it
to iUsabelle, and due to slowness inherent in Isabelle's datatype
package we want to remove unused constructors in our AST type.
Also remove the lem_ast backend - it's heavily bitrotted, and for
loading the ARM ast into the interpreter it's just not viable to use
this approach as it just doesn't scale. We really need a way to be
able to serialise and deserialise the AST efficiently in Lem.
|
