| Age | Commit message (Collapse) | Author |
|---|
|
While the backends will usually manage to find the constant size anyway,
this ensures that implicit arguments will be filled in with the constant
value too. (For example, this was affecting isla execution in one corner
case because the slice_mask primitive didn't see that the size was
constant.)
|
|
|
|
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.
|
|
- 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)
|
|
|
|
|
|
|
|
The monomorphisation analysis decides whether to split function
arguments in the callee or in callers. The code previously used a
datastructure that can hold results of either the one case or the other,
but there might be functions that are called in different contexts
leading to different decisions. This patch changes the datastructure to
support storing all instances of either case.
|
|
If we call a function where some arguments need to be rewritten, we
might need to rewrite those parameters in the caller as well.
|
|
|
|
|
|
Supporting more ASL idioms
|
|
... and try to resolve them using constant propagation.
|
|
Ask the type checker instead of looking at the expression syntax. This
also discovers implied instantiations, e.g. if we previously knew
('N in {32, 64}) and we have an assertion ('N != 32), then we know
('N == 64).
|
|
This will propagate constant assignments in chosen branches of case
expressions after applying pattern choices, e.g. the assignment to
datasize in
match size {
[bitone, _] => datasize = 64,
...
}
when pattern [bitone, _] is chosen for size.
|
|
- Handle more combinations of patterns and expressions in constant
propagation
- Remove dead code after throw() in monomorphisation
- Use correct val specs and environments when analysing and
pretty-printing function clauses
|
|
|
|
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).
|
|
|
|
|
|
In the new version of the ASL-generated Sail, some vector operators are
also overloaded for integers to match idioms of ASL (e.g. i[31:0], where
i is an integer), so check in the monomorphisation rewrites that we use
bitvector helper functions only for actual bitvectors.
|
|
|
|
When considering whether to add a cast, now also consider the updated
environment within an if branch / match clause to compare against the
outer environment. This picks up not only constraints on type variables
added by an if condition or pattern guard (e.g. "if (size == 16) ..."),
but also constraints depending on those (e.g. in "bits('width)" where
"'width == 'size * 8"). Fixes a type error observed when generating Lem
for sail-arm (in aget__Mem).
|
|
Also make the Error type private, so it's only constructed through the
functions we expose in reporting.mli
|
|
|
|
Also don't require a previously declared default vector indexing order
in vector_dec.sail.
|
|
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.
|
|
|
|
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
|
|
used in risc-v spec.
|
|
In particular, bitvector subrange updates work with this version.
|
|
- additional rewrites (signed extend of subrange@zeros, subrange assignment,
variants with casts)
- drop # from new top-level type variables (e.g., n_times_8) so that the
rewriter knows that they're safe to include in casts
- add casts in else-branches when only one possible value for a size is left
- add casts when assertions force a size to be a particular value
- don't use types to detect set constraints in analysis because we won't
know which part of the assertion should be replaced
- also use non-top-level type variables when simplifying sizes in analysis
(useful when it can from pattern matching on an ast)
- cope with repeated int('n) in a pattern match (!)
|
|
Mostly to make constraints sent to the SMT solver and Coq nicer, but
also makes it easy to remove uninformative constraints in the Coq
back-end.
|
|
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
|
|
Also add a $suppress_warnings directive that ensures that no warnings
are generated for a specific file.
|
|
can now write e.g.
forall (constant 'n : Int) rather than forall ('n: Int)
which requires 'n to be a constant integer value whenever the function
is called. I added this to the 'addrsize variable on memory
reads/writes to absolutely guarantee in the SMT generation that we
don't have to worry about the address being a variable length
bitvector.
|
|
Also handle any type variables from assignments and degrade gracefully
during constant propagation when unification is not possible.
|
|
|
|
Note that we might need to do both in future.
Also report more information when constructor refinement fails.
|
|
|
|
|
|
|
|
- handle multiple bitvector length variables
- more fine-grained unnecessary cast insertion checks
- add tuple matching support to constant propagation (for the test)
|
|
- updates for type checking changes
- handle a little more pattern matching in constant propagation
- fix bug where false positive warnings were produced
- ensure bitvectors in tuples are always monomorphised (to catch the case
where the bitvectors only appear alone with a constant size)
|
|
|
|
|
|
|
|
|
