| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
This simplifies some of the code.
|
|
This was the final missing step for me to link two almost identical C files
generated from sail into the same library.
|
|
I was getting run-time failures when code generate from cheri128 and
cheri64 in the same process. This was caused because my compiler defaults
to -fcommon so it merged multiple variables (with conflicting types!).
When initializing the second set of letbindings, the first one was
overwritten (first variable was lbits, the other was uint64_t). Compiling
with -fno-common exposes this problem.
|
|
Without this I get the following linker error when trying to include both
64 and 128 bit sail-riscv code in the same binary:
duplicate symbol '_model_init' in:
libsail_wrapper128.a(sail_wrapper_128.c.o)
libsail_wrapper128.a(sail_wrapper_64.c.o)
duplicate symbol '_model_main' in:
libsail_wrapper128.a(sail_wrapper_128.c.o)
libsail_wrapper128.a(sail_wrapper_64.c.o)
duplicate symbol '_model_fini' in:
libsail_wrapper128.a(sail_wrapper_128.c.o)
libsail_wrapper128.a(sail_wrapper_64.c.o)
# Conflicts:
# src/jib/c_backend.ml
|
|
This allows me to compile sail-riscv64 and sail-riscv128 code in the same
static library.
|
|
See sailcov/README.md for a short description
Fix many location info bugs discovered by eyeballing output
|
|
Fixes the warning generated because in C -X where X is the minimum integer is
parsed as a positive integer which is then negated. This causes a (I
believe spurious) warning that the integer literal is too large for the type.
Also using INT64_C so we get either long or long long depending on
platform
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Will call:
void sail_branch_reached(int branch_id, char *source_file, int l1, int c1, int l2, int c2);
on each branch caused by a match or if statement in the source code
For each branch that is taken, will call:
void sail_branch_taken(int branch_id, char *source_file, int l1, int c1, int l2, int c2)
Every branch gets a unique identifier, and the functions are called with
the source file location and line/character information for the start
and end of each match case or then/else branch. sail_branch_reached is
given the location info for the whole match statement.
|
|
All the code-generator options can now be controlled via a json
configuration file
Extra fields can be added to the sail_state struct using a
codegen.extra_state key in the configuration json for the code
generator
If primitives want to modify the state they can be specified via
codegen.state_primops
To import such state, codegen.extra_headers can be used to add
user-defined headers to the generated .h file
|
