Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
A bunch of changes I have been meaning to push up, cleaning up the vectoriser to deal with almost everything under
aarch64_vectors*
. Placeholder for me, as it really needs to be broken up into a series of PRs, when I get around to it.General bug fixes:
take
anddrop
list utilities.sdiv_int
worked its way into the code base, but it doesn't exist.Improved coverage testing of vectors:
_Z
array with random values to get some results out of coverage testing for vectors instructions.FPRSqrtEstimate
andUnsignedRSqrtEstimate
are now reachable, add them to the inlining config.sqrt_real
, not sure if it's accurate to hardware though.Change our primitive shift operations to line up with SMTLIB:
Changes to simplify and improve the vectoriser:
libASL/loops.ml
.IntToBits
, so that it can reason over trivial integer operations.select_vec
andupdate_vec
operations in terms of integer positional arguments until the last possible phase, to simplify reasoning.Remaining:
_Z
array with random values, rather than just the low 64-bits.sqrt_real
should be.override.asl
.