| Age | Commit message (Collapse) | Author |
|---|
|
|
|
since riscv is no longer in this repository, and we use the RISC-V
duopod as an example, you need to build as:
make RISCV=directory manual.pdf
if directory is not equal to ../../sail-riscv (which is where it would
be if sail and sail-riscv are checked out in the same respository
together)
|
|
|
|
Add a file nl_flow.ml which can analyse a block of Sail expressions
and insert constraints for flow-typing rules which do not follow the
lexical structure of the code (and therefore the syntax-directed
typing rules can't do any flow-typing for). A common case found in ASL
translated Sail would be something like
function decode(Rt: bits(4)) = {
if Rt == 0xF then {
throw(Error_see("instruction"));
};
let t = unsigned(Rt);
execute(t)
}
which would currently fail is execute has a 0 <= t <= 14 constraint
for a register it writes to. However if we spot this pattern and add
an assertion automatically:
let t = unsigned(Rt);
assert(t != 15);
execute(t)
Then everything works, because the assertion is in the correct place
for regular flow typing. Currently it only works for this specific
use-case, and is turned on using the -non_lexical_flow flag
|
|
|
|
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.
|
|
They weren't needed for ASL parser like I thought they would be, and
they increase the complexity of dealing with constraints throughout
Sail, so just remove them.
Also fix some compiler warnings
|
|
Should hopefully fix memory leak in RISC-V.
Also adds an optimization pass that removes copying structs and allows
some structs to simply alias each other and avoid copying their
contents. This requires knowing certain things about the lifetimes of
the structs involved, as can't free the struct if another variable is
referencing it - therefore we conservatively only apply this
optimization for variables that are lifted outside function
definitions, and should therefore never get freed until the model
exits - however this may cause issues outside ARMv8, as there may be
cases where a struct can exist within a variant type (which are not
yet subject to this lifting optimisation), that would break these
assumptions - therefore this optimisation is only enabled with the
-Oexperimental flag.
|
|
- Propagate types more accurately to improve optimization on ANF
representation.
- Add a generic optimization pass to remove redundant variables that
simply alias other variables.
- Modify Sail interactive mode, so it can compile a specification with
the :compile command, view generated intermediate representation via
the :ir <function> command, and step-through the IR with :exec <exp>
(although this is very incomplete)
- Introduce a third bitvector representation, between fast
fixed-precision bitvectors, and variable length large
bitvectors. The bitvector types are now from most efficient to least
* CT_fbits for fixed precision, 64-bit or less bitvectors
* CT_sbits for 64-bit or less, variable length bitvectors
* CT_lbits for arbitrary variable length bitvectors
- Support for generating C code using CT_sbits is currently
incomplete, it just exists in the intermediate representation right
now.
- Include ctyp in AV_C_fragment, so we don't have to recompute it
|
|
|
|
|
|
|
|
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.
|
|
This should fix the issue in cheri128
Also introduce a feature to more easily debug the C backend:
sail -dfunction Name
will pretty-print the ANF and IR representation of just the Name
function. I want to make this work for the type-checker as well, but
it's a bit hard to get that to not fire during re-writing passes right
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)
|
|
Currently not enabled by default, the flag -Xconstraint_synonyms
enables them
For generating constraints in ASL parser, we want to be able to give
names to the constraints that we attach to certain variables. It's
slightly awkward right now when constraints get long complicated
because the entire constraint always has to be typed out in full
whenever it appears, and there's no way to abstract away from that.
This adds constraint synonyms, which work much like type synonyms
except for constraints, e.g.
constraint Size('n) = 'n in {1, 2, 4, 8} | 128 <= 'n <= 256
these constraints can then be used instead of the full constraint, e.g.
val f : forall 'n, where Size('n). int('n) -> unit
Unfortunatly we need to have a keyword to 'call' the constraint
synonym otherwise the grammer stops being LR(1). This could be
resolved by parsing all constraints into Parse_ast.atyp and then
de-sugaring them into constraints, which is what happens for
n-expressions already, but that would require quite a bit of work on
the parser.
To avoid this forcing changes to any other parts of Sail, the intended
invariant is that all constraints appearing anywhere in a type-checked
AST have no constraint synonyms, so they don't have to worry about
matching on NC_app, or calling Env.expand_typquant_synonyms (which
isn't even exported for this reason).
|
|
|
|
(aimed at RISC-V)
|
|
|
|
Assigning to an uninitialized variable as the last statement in a
block is almost certainly a type, and if that occurs then the
lift_assign re-write will introduce empty blocks causing this error to
occur. Now when we see such an empty block when converting to A-normal
form we turn it into unit, and emit a warning stating that an empty
block has been found as well as the probable cause (uninitialized
variable).
|
|
Also allow options to be set via a pragma in Sail files
|
|
|
|
|
|
Interpreter used a re-write (vector concat removal) that is dependent
on the vector_string_to_bit_list rewriting pass. This fixes the
interpreter to work without either vector concat removal, or turning
bitstrings into vector literals like [bitzero, bitzero, bitone]. This
has the upside of reducing the number of steps the interpreter needs
for working with bitvectors so should improve interpreter performance.
We also now test all the C compilation tests behave the same using the
interpreter. Currently the real number tests fail due to limitations
of Lem's rational library (this must be fixed in Lem). This required
supporting configuration registers in the interpreter. As such the
interpreter was refactored to more cleanly process registers when
building an initial global state. The functions are also collected
into the global state, which removes the need to search for them in
the AST every time a function call happens. This should not only
improve performance, but also removes the need to pass an AST into the
interpretation functions.
|
|
Test the builtin functions by compiling them to C, OCaml, and OCaml
via Lem. Split up some of the longer builtin test programs to avoid
stack overflows when compiling to OCaml, as 3000+ line long blocks can
cause issues with some re-writing steps.
Also test constant-folding with builtins (this should reduce the
asserts in these files to assert true), and also test constant folding
with the C compilation.
Fix a bug whereby vectors with heap-allocated elements were not
initialized correctly.
Fix a bug caused by compiling and optimising empty vector literals.
Fix an OCaml test case that broke due to the ref type being used. Now
uses references to registers.
Fix a bug where Sail would output big integers that lem can't
parse. Checks if integer is between Int32.min_int and Int32.max_int
and if not, use integerOfString to represent the integer. Really this
should be fixed in Lem.
Make the python test runner script the default for testing builtins
and running the C compilation tests in test/run_tests.sh
Add a ocaml_build_dir option that sets a custom build directory for
OCaml. This is needed for running OCaml tests in parallel so the
builds don't clobber one another.
|
|
The new option -dcoq_debug_on takes a list of functions to output tracing
on.
|
|
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.
|
|
|
|
|
|
Fixes monomorphisation on files using mappings.
Also extended constant propagation to handle pattern matches on
bitvector expressions (because an earlier rewrite replaces the literals).
Also moved L_undef rewriting because monomorphisation can handle them
but not the replacement functions.
|
|
Uses previous stage to deal with (e.g.) guards.
New option -dcoq_warn_nonex tells you where all of the extra default
cases were added.
|
|
By default generated functions are non-static, using the -static flag makes them static which is useful for measuring coverage using generated code. Some utility helper functions will always be static, but the compiled versions of sail functions won't be unless this flag is set.
|
|
|
|
targets using this.
|
|
|
|
|
|
Fix a bug involving indentifers on the left hand side of assignment
statements not being shadowed correctly within foreach loops.
Make the different between different types of integer division
explicit in at least the C compilation for now. fdiv_int is division
rounding towards -infinity (floor). while tdiv_int is truncating
towards zero. Same for fmod_int and tmod_int.
|
|
|
|
|
|
Also add an additional -Oz3 flag that uses z3 to optimize some
additional types. This is currently very experimental and doesn't
fully work yet.
|
|
- Refactor the flow typing implementation in the type-checker. This
should fix an issue involving riscv_platform. Specifically it should
now work better when an if statement contains multiple conditions
combined with and/or, only some of which imply constraints at the
type level. This change also simplifies the implementation of flow
typing, and removes some obscure features that were hardly used -
specifically, flow typing could modify types, but this was fairly
obscure and doesn't seem to affect any of our specifications. More
testing is needed to ensure that this change hasn't inadvertantly
broken anything, but it does pass all our tests and continue to
typecheck arm, riscv and cheri.
- Also adds a option for generating faster undefined functions for
enum and variant types. Previously I tried to optimise away such
functions in the C backend, because they could be slow and cause
considerable uneccessary allocation, however this was error prone
and it turns out a much simpler solution is to simply make the
functions themselves much faster, at the cost of hard-coding certain
decisions about what undefined means for these types at compile tile
(which is fine for fast emulation). This almost doubles the
performance of the generated C code.
- Add a wrapper for right shift to avoid UB when shifting by 64 or
more places.
|
|
|
|
Useful for partial test cases (e.g., some of the typechecking tests)
Also a bonus warning for such functions in normal use
|
|
default (off by default).
|
|
1. Experiment with allowing some flow typing on mutable variables for
translating ASL in a more idiomatic way. I realise after updating some
of the test cases that this could have some problematic side effects
for lem translation, where mutable variables are translated into
monadic code. We'd need to ensure that whatever flow typing happens
for mutable variables also works for monadic code, including within
transformed loops. If this doesn't work out some of these changes may
need to be reverted.
2. Make the type inference for l-expressions a bit smarter. Splits the
type checking rules for l-expressions into a inference part and a
checking part like the other bi-directional rules. Should not be able
to type check slightly more l-expresions, such as nested vector slices
that may not have checked previously.
The l-expression rules for vector patterns should be simpler now, but
they are also more strict about bounds checking. Previously the bounds
checks were derived from the corresponding operations that would
appear on the RHS (i.e. LEXP_vector would get it's check from
vector_access). This meant that the l-expression bounds checks could
be weakend by weakening the checks on those operations. Now this is no
longer possible, there is a -no_lexp_bounds_check option which turns
of bounds checking in l-expressions. Currently this is on for the
generated ARM spec, but this should only be temporary.
3. Add a LEXP_vector_concat which mirrors P_vector_concat except in
l-expressions. Previously there was a hack that overloaded LEXP_tup
for this to translate some ASL patterns, but that was fairly
ugly. Adapt the rewriter and other parts of the code to handle
this. The rewriter for lexp tuple vector assignments is now a rewriter
for vector concat assignments.
4. Include a newly generated version of aarch64_no_vector
5. Update the Ocaml test suite to use builtins in lib/
|
|
- originally based on the Lem backend
- added externs to some of the library files and tests
- added wildcard to extern valspecs in parser
- added Type_check.get_val_spec_orig to return the valspec with the
function's original names for bound type variables
Note that most of the tests will fail currently
|
|
|
|
|
|
Turn on complex nexp rewriting for mono by default
(NB: solving is currently quite slow, will optimise)
|
|
(for monomorphisation, off for now because the analysis needs extended).
Also tighten up orig_nexp, make Lem backend replace # in type variables.
|
