| 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.)
|
|
Also fix a few shellcheck warnings related to printf while doing so.
|
|
Both /.gitignore and /lib/coq/.gitignore ignored some files in /lib/coq.
This commit removes /lib/coq/.gitignore and moves all ignore-statements
to /.gitignore . This should simplify the maintenance of gitignore files.
The situation with /test/mono/.gitignore is analogous.
|
|
- 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.
|
|
For example, in
let datasize = e in ...
the typechecker will generate a kid '_datasize if e has an existential
type (with one kid), and in
let 'datasize = e in ...
the typechecker will bind both 'datasize and '_datasize. If we
substitute one as part of constant propagation, this patch will make
constant propagation also substitute the other.
|
|
... and try to resolve them using constant propagation.
|
|
|
|
|
|
|
|
|
|
|
|
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 (!)
|
|
Also handle any type variables from assignments and degrade gracefully
during constant propagation when unification is not possible.
|
|
- 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)
|
|
|
|
|
|
Tweak colours of monomorphistion test output
|
|
Fix monomorphisation tests
|
|
|
|
It now pushes casts into lets and constructor applications, and so
supports the case needed for RISC-V.
|
|
|
|
Add an extra argument for Type_check.prove for the location of the prove
call (as prove __POS__) to help debug SMT related issues
|
|
|
|
Especially for return expressions, which fixes a test case
|
|
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.
|
|
(still need to sort out some string stuff, though)
|
|
|
|
|
|
(note that they're already declared in lib/arith.sail)
|
|
|
|
|
|
|
|
(also reorder the phases a little)
|
|
|
|
|
|
Doesn't remove them from function bodies because that can produce
more work for the sizeof rewriting.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(plus some adjustments for the test case)
|
|
|
