| Age | Commit message (Collapse) | Author |
|---|
|
Rather than having the caller prefix latex and refcode strings with the
category, push that down into common functions to both abstract away the
details and avoid duplication.
No functional change intended, and verified by regenerating the LaTeX
for sail-cheri-mips and sail-cheri-riscv.
|
|
|
|
Add latex tests and allow external links
|
|
Wrap saildoc LaTeX in \saildoclabelled macro
|
|
This can be useful to reference things that aren't defined by sail.
|
|
This is for a bug I encountered while moving some docs over from the ISA
spec into sail documentation comments.
|
|
Also fix a few shellcheck warnings related to printf while doing so.
|
|
This takes two arguments: the label name and the \saildocfoo macro use
itself. This allows cunning definitions of \saildoclabelled and
\saildocfoo to tease apart the various bits and reconstruct them in a
different order without having to redefine \phantomsection and \label
temporarily and hard-code knowledge of the implementation of these
documentation commands. I intend to use these in cheri-architecture in
combination with sail-cheri-riscv.
Unlike the other macros, this is considered a bit more niche, so we
include a default definition of it that expands to what was previously
hard-coded. This also makes this a non-breaking change.
|
|
Saildoc improvements
|
|
C codegen: remove an unnecessary declaration in the header file
|
|
|
|
This seems to be the current name for the overload.
|
|
|
|
|
|
|
|
Printing the text is only so helpful; the most important thing to know
is what kind of element it actually is, which is lost when extracting
the text. Instead, print the whole S-Expr.
|
|
We now parse
/*!
* Paragraph
*/
and
/*!
*Paragraph
*/
the same as
/*!
Paragraph
*/
since the first form is prettier, and similar to what Doxygen, Javadoc
and other such tools allow. This can cause mild confusion, as if the
start of a line in the final form happens to have a * then it will
unexpectedly remove it, but this is a problem shared by those tools too
and the intent is that everyone just use the first form and never need
to worry about it.
|
|
These were only parsed for val specs and scattered clauses, but many
other constructs can be meaningfully documented. Moreover, attaching the
documentation to the SD_aux rather than the FCL_aux etc inside it is
unhelpful since the latter is what the LaTeX backend sees.
Instead, push the documentation down into the non-scattered entity
within the SD_aux (i.e. the FCL_aux / Tu_aux / MCL_aux) when possible,
only leaving it on the SD_aux when they are more like a val spec. This
means that the saildoc for scattered function clauses is now emitted,
without any changes needed to the LaTeX backend.
Also support saildoc on a wider variety of non-scattered constructs, and
slightly simplify aspects of the grammar whilst here.
|
|
|
|
Improve gitignore and documentation a little
|
|
opam pin is useful in the development workflow.
About the rewording: The tests of Sail check the behavior of Sail and
not whether it is installed correctly, because the instructions above
that paragraph don’t install Sail, they just build it.
These circumstances weren’t represented appropriately by the text.
|
|
Both /.gitignore and /lib/coq/.gitignore ignored some files in /lib/coq.
This commit removes /lib/coq/.gitignore and moves all ignore-statements
to /.gitignore . This should simplify the maintenance of gitignore files.
The situation with /test/mono/.gitignore is analogous.
|
|
The "c" tests produce some *.h files that didn’t get ignored. The "coq"
tests also produce some files that weren’t ignored.
|
|
|
|
- add tests for a couple of related rewrites
- accept same range of constants for sign extension in the rewrite as for
the zero extension version (to make the test simpler)
|
|
|
|
|
|
|
|
For example, if a 129-bit capability is given as a 132-bit hex literal
and truncated, this produces a 129-bit binary literal. In isla, this will
keep all of the computation concrete because 129-bit concrete values are
supported.
|
|
Also remove omega workaround that lia doesn't need.
|
|
|
|
|
|
|
|
Can be set by C emulator to control where coverage information is
written
|
|
|
|
c2: make the global state API configurable for externally defined get/set functions
|
|
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.
|
|
|
|
functions
|
|
Useful for RISC-V with it's custom C emulator
|
|
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.
|
|
|
|
|
|
|
|
- also tie following type check to the mono_rewrites flag
|
|
|
|
|
|
|
|
Generate accessors for scalar types, array of scalars and scalars in struct in the sail state
|
|
in the sail state
|
