To make this work, we have to remove some phantom type parameters
from the `Yices` solver module. I don't think they were contrinbuting
in any useful way.
This makes the `What4.Expr.Builder` module somewhat easier to navigate,
and may help reduce build times slightly. To accomplish this change,
some API changes were necessary. Most notable is the change to
`definedFn`, which now takes a datatype defining the unfolding policy
instead of a user-provided callback function.
`Test.Verification`: this makes the testing changes have
very nearly no impact on the use sites.
Also remove the unnecessary `PropPropery` constructor.
These changes make is to that threads that are waiting for
solver processes exit more gracefully if they are interrupted
by another thread throwing an exception to them.
* Fix use of BVDomain.Arith.scale.
* Fix scale function and the unit test.
* Add the operation `scale` to the randomized BVDomain tests.
This operation was previously overlooked.
Co-authored-by: Rob Dockins <rdockins@galois.com>
GHC 8.4 haddock does not support comments on individual fields of an
ADT. This particular structure is internal only and lacks general
description haddocks, so simply converting these from haddock comments
to normal comments resolves this issue.
Update all `what4`-related packages to to concrete computation using the `bv-sized` library for fixed (but arbitrary) sized bitvector values.
Currently, the bitvector abstract domain computations are still being done directly on raw integers; we can revisit this in the future.
Co-authored-by: Ben Selfridge <benselfridge@000279.local>
Co-authored-by: Rob Dockins <rdockins@galois.com>
Default to using the arithmetic mode so that when we union together
a collection of consecutive singleton values, we get a precise arithmetic
interval. Add a test to the test suite to check for this property.
the intermediate computations. Also add a test that verifies that the
domain overlap test is precise; in other words, if the test indicates
that we have an overlap, then we can find a witness that constructively
proves that the two domains share a value.
This turns out to be pretty tricky, but the Cryptol functions in this
patch demonstrate that we can compute a precise overlap test for mixed
bitvector domains without resorting to brute enumeration or other
inefficent methods.
The main operation of interest is the `bitwise_round_between` method,
which finds the arithmetically next value above some starting value
that is bitwise between consistent bitbounds. This turns out to
be precisely what we need to test whether an arithmetic interval
which is nested "inside" a bitwise interval actually contains one
of the bitwise values.
It might be possible to simplify this operation, but the current
definition demonstrates it is possible using only word-level operations,
if we allow ourselves to use the `fillright` operation.
arithmetic and bitwise domains, and provide quickcheck
properties for exercising the individual operations.
These quickcheck properties have been organized into a new package
test suite.
There are now three cooperating abstract domains: one for arithmetic
operations, another for bitwise operations and a third which is
an alternate presentation of the bitwise operation domain.
Make the bit order for indexed operations (at, set, slice, etc) more
obvious and provide both Big- and Little-endian variants.
Transition uses of "fail" to "panic" instead.
