| 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.
|
|
|
|
This can be useful to reference things that aren't defined by sail.
|
|
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
|
|
|
|
|
|
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.
|
|
|
|
- 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.
|
|
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
|
|
|
|
|
|
|
|
in the sail state
|
|
|
|
c2: primop: -O: make sure to pick global or name correctly
|
|
exist as constructor or function
|
|
|
|
|
|
|
|
|
|
Accidentally broken by e1a2b0d2 because the Coq backend looks at the
wrong type to decide when a proof is needed.
|
|
Avoids generating an assert expression with an escape effect.
Mirrors existing case for `if cond { throw(...); };`.
No longer requires `-non_lexical_flow`.
|
|
Helps with Coq 8.11. Also fix BBVDIR default in test script.
|
|
|
|
- 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
|
|
|
|
|
|
|
|
Previous merge commit caused some code that was generating
register.field = value
to instead generate
temp = register
temp.field = value
register = temp
This was caused by rewriter changes affecting the ANF form, and the Jib
compilation was sensitive to small changes in the ANF form when
compiling l-expressions. Rather than applying a band-aid fix in the
rewriter this commit re-factors the ANF translation of l-expressions to
ensure that the jib compilation is more robust and able to consistently
generate the correct l-expressions without introducing additional
read-modify-write expressions in the code.
|
|
|
|
|
|
Otherwise the C emulator doesn't build.
|
