| 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.
|
|
|
|
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 tie following type check to the mono_rewrites flag
|
|
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.
|
|
|
|
See sailcov/README.md for a short description
Fix many location info bugs discovered by eyeballing output
|
|
Currently uses the -c2 option
Now generates a sail_state struct which is passed as a pointer to all
generated functions. This contains all registers, letbindings, and the
exception state. (Letbindings must be included as they can contain
pointers to registers). This should make it possible to use sail models
in a multi-threaded program by creating multiple sail_states, provided a
suitable set of thread-safe memory builtins are provided. Currently the
sail_state cannot be passed to the memory builtins.
For foo.sail, now generate a foo.c, foo.h, and (optionally) a foo_emu.c.
foo_emu.c wraps the generated library into an emulator that behaves the
same as the one we previously generated.
The sail_assert and sail_match_failure builtins are now in a separate
file, as they must exist even when the RTS is not used.
Name mangling can be controlled via the exports and exports_mangled
fields of the configuration struct (currently not exposed outside of
OCaml). exports allows specifying a name in C for any Sail identifier
(before name mangling) and exports_mangled allows specifiying a name for
a mangled Sail identifier - this is primarily useful for generic
functions and data structures which have been specialised.
|
|
... and try to resolve them using constant propagation.
|
|
This will constant-fold letbindings such as
let LOG2_TAG_GRANULE : int(4) = 4
let TAG_GRANULE : int = (1 << LOG2_TAG_GRANULE)
which is useful for the translation to Lem if TAG_GRANULE is used in
bitvector lengths.
|
|
This check is used in the guarded pattern rewrite step, which would
previously generate some impossible matches (e.g. matching expression
"true" against pattern "false").
|
|
Add casts for function arguments using the constraints in the
environment of the function clause (not just assertions within the
function body). Also pass in the global typing environment for
comparison with the environment within the function clause (and make a
corresponding change in the Lem pretty-printer so that it uses the right
environments).
|
|
Split the variable (tuple) type into an input and output type. They are
meant to be the same, but due to the way function types are
instantiated, unification can fail in the case of existential types, as
in the added test case (when trying to generate Lem definitions from
it). The output of the loop will be checked against the expected type,
though, due to a type annotation outside the loop added by the rewrite
pass for variable updates.
|
|
... instead of a tuple assignment. This makes the rewrite independent
of the tuple assignment rewrite and allows it to be moved after the
latter (nesting vector concat lexps into tuple lexps is an idiom in ASL,
but the other way around doesn't make sense).
|
|
In particular, don't add annotations for types with existentially
quantified variables that only occur in constraints, not in the type,
e.g. {'i1 'i2, 'i1 == div('i2, 8). int('i1)}. These seem to confuse the
type checker when pulled out into the source AST.
|
|
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 be more careful to avoid pattern bindings with identifiers to avoid
parsing clashes, eg `let 'bytes := ...` which is confused with the
notation for binary literals.
|
|
|
|
|
|
... not just in type abbreviations.
Fixes an error in the RV32 build of CHERI-RISC-V.
|
|
|
|
If, for example, we have a bidirectional encoding-decoding mapping as in
sail-riscv, but want to translate only the decoder to a theorem prover,
this commit allows us to stub out the the encoder by splicing in dummy
definitions.
|
|
:fixed_registers command
|
|
accordingly
|
|
|
|
Remove P_record as it's never been implemented in
parser/typechecker/rewriter, and is not likely to be. This also means
we can get rid of some ugliness with the fpat and mfpat types. Stubs
for P_or and P_not are left as they still may get added to ASL and we
might want to support them, although there are good reasons to keep
our patterns simple.
The lem warning for while -> while0 for ocaml doesn't matter because
it's only used in lem, and the 32-bit number warning is just noise.
|
|
|
|
Fixes #53
|
|
|
|
|
|
sail definitions
Definitions can be made external on a per-backend basis, so we need to
make sure constant folding doesn't inline external functions that have
sail definitions for backends other than the ones we are currently
targetting
|
|
Do this by making sure that generic pattern literal re-writing gets
applied to top-level function clauses. This requires re-ordering the
rewrites for most backends otherwise they break, which hopefully wo
anything.
After doing this re-ordering I had to turn off casting when rewriting
bitvector patterns, otherwise insane things can happen.
|
|
- 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
|
|
|
|
A missing type annotation in rewrite_guarded_clauses caused a crash in
some cases. Also fix an effect propagation bug in
rewrite_letbind_effects.
|
|
Add a fallthrough case that fails to potentially partial pattern
matches. This also helps to preserve any guard in the final match case,
which might be needed for flow typing (see the discussion on issue #51).
TODO: Merge with the MakeExhaustive rewrite, which currently does not
support guarded patterns.
|
|
Fixes #47.
Also adjust the nexp substitution so that the error message points to a
useful location, and replace the empty environment with the initial
environment in a few functions that do type checking to ensure that the
prover is set up (which may be needed for the wf check).
|
|
|
|
|
|
Clean up ott grammar a bit
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
With the new interpreter changes computing the initial state for the
interpreter does some significant work. The existing code was
re-computing the initial state for every subexpression in the
specification (not even just the ones due to be constant-folded away).
Now we just compute the initial state once and use it for all constant
folds.
Also reduce the time taken for the simple_assignments rewrite from 20s
to under 1s for ARMv8.5, by skipping l-expressions that are already in
the simplest form.
|
