This patch contains a variety of fixes needed to build the libraries in the
`what4` repo with GHC 9.6:
* GHC 9.6 bundles `mtl-2.3.*`, which no longer re-exports `Control.Monad`,
`Control.Monad.IO.Class`, and similar modules from `mtl`-related modules.
To accommodate this, various imports have been made more explicit.
* `MonadTrans t` now has a quantified `forall m. Monad m => Monad (t m)`
superclass in `mtl-2.3.*`. As a result, the `MonadTrans (PartialT sym)`
instance must now have an `IsExpr (SymExpr sym)` instance context in order
for it to typecheck, as this is the same instance context that `PartialT`'s
`Monad` instance has.
This is technically a breaking change, so I have noted it in the `what4`
changelog. That being said, this change is unlikely to affect many people
in practice, considering that the `MonadTrans` instance for `PartialT` is
usually used in tandem with the `Monad` instance.
* Various upper version bounds on `base` have been lifted to allow building
with `base-4.18`.
* The `aig` submodule has been bumped to bring in the changes from
GaloisInc/aig#15, which allows it to build with GHC 9.6.
This contains a variety of changes needed to make the libraries in the `what4`
compile warning-free with GHC 9.2:
* GHC 9.2 includes `-Woperator-whitespace-ext-conflict` as a part of `-Wall`,
which causes `Test.Verification` to warn when built with GHC 9.2. The fix is
simple: just add spaces after certain uses of the `$` character.
* GHC 9.2 includes `-Wincomplete-uni-patterns` as a part of `-Wall`, which
causes `GenWhat4Expr` to warn when built with GHC 9.2. I fixed the warnings
by introducing new `from{Bool,Int,BV8,BV16,BV32,BV64}TestExpr` functions to
extract the payloads of different `TestExpr` constructors. This is no less
partial than before, but at least this way any accidental partiality will
result in a more descriptive error message than
`Non-exhaustive patterns in ...`.
* In `base-4.16.*`, `Nat` is now a type synonym for `Natural`, and
`GHC.TypeNats` now re-exports `Natural`. This causes an import of
`Numeric.Natural` in `What4.SemiRing` (previously required to bring `Natural`
into scope) trigger an `-Wunused-imports` warning. I fixed the warning by
using explicit imports from `GHC.TypeNats` and `Numeric.Natural`.
* The `aig` and `abcBridge` submodules were bumped to bring in the changes
from GaloisInc/aig#12 and GaloisInc/abcBridge#19, respectively, which allows
them to build with `base-4.16.*`.
* The upper version bounds on `base` were raised in `what4-abc`, `what4-blt`,
and `what4-transition-system` to allow them to build with `base-4.16.*`.
This contains a variety of tweaks needed to make `what4`, `what4-abc`, and
`what4-blt` build warning-free on GHC 9.0:
* GHC's constraint solver now solves constraints in each top-level group
sooner (see
[here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0?version_id=5fcd0a50e0872efb3c38a32db140506da8310d87#the-order-of-th-splices-is-more-important)).
This affects `what4`'s `What4.Expr.App` module, as it separates top-level
groups with a Template Haskell `$(return [])` splice. The previous location
of this splice made it so that the TH-generated instances in that module
(e.g., the `TraversableFC` instance for `App`) were not available to any code
before the splice, resulting in type errors when compiled with GHC 9.0.
I implemented a fairly involved fix of moving each of the affected data
types, as well as their corresponding TH-generated instances, to the top of
the module to ensure that subsequent top-level groups have access to this
code.
* GHC 9.0 implements simplified subsumption (see
[here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0?version_id=5fcd0a50e0872efb3c38a32db140506da8310d87#simplified-subsumption)).
This affects the use of the `freshBoundTermFn` function in `what4`'s
`What4.Protocol.SMTWriter` module, as `freshBoundTermFn`'s type signature
contains a nested `forall`. Fortunately, repairing this code is as simple as
a single eta expansion.
* Raise the upper version bounds on `base` in `what4-abc` and `what4-blt` to
permit building with `base-4.15` (bundled with GHC 9.0).
* Bump the `aig` submodule commit so that it does not emit `-Wstar-is-type`
warnings when built with GHC 9.0, where `-Wall` implies `-Wstar-is-type`.
Bump the `language-sally` submodule commit to allow building with
`base-4.15` (see GaloisInc/language-sally#6).
* Update/imporove Haddock comments and bump copyright years
* Bump copyright dates in LICENSE files
* Add .cabal package lower bounds. These appear to be reasonable, but
I haven't exhaustively tested the various configurations.
* Bump copyright dates in .cabal files
* Start a basic changelog
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>
We now represent disjunctions as negated conjunctions with negated
elements. This change makes it possible to significantly simplify
the definitions of the andPred and orPred operations.
boolean formulae in What4. This datastructure automatically implements
associative-commutative-idempotent rewriting as well as recognizing
resolution opportunities (i.e. A /\ ~A = False).
gather products.
In addition, use similar machenery to represent bitwise disjunction.
This gives additional boolean lattice reductions, including absorption
and idempotency.
and generalize equality and if/then/else to work over all base types.
Bitvectors now are paricipants in two different semiring instances:
the usual arithmetic one and a bitwise one based on XOR and AND.
This allows automatic term gathering, XOR-canceling and other
similar simplifications to occur automatically.
bitvector operations in `what4`.
Solvers don't generally have primitives for these, but it is nonethess useful,
I think, to provide them as operations. A collection of useful rewrites
could probably be added (e.g., interesting interaction with concat).
This update fixes a variety of issues with solver interaction involving
the named assertion and unsat core updates. CVC4, Z3 and Yices now will
properly issue queries and return resuts.
In addition, a variety of refactorings were made to the interaction code
that should make things more uniform going forward. As part of these
refactorings, it is now possible to pass an "auxiliary output" file handle
when interacting with solvers. If provided, solver commands and responses
will be echoed into this file for debugging purposes.
instead of just a single predicate. The semantics of the query is
just the conjunction of the given predicates. However, for the purposes
of computing unsatisfiable cores, the list of given predicates
will be the atomic units that will either appear (or not) in the
generated unsat cores, for those solvers which support computing
unsat cores.
in the expression builder. That way, it can be fully elminated when
it encounters a `bvNonzero` or `bvTestBit` operation, etc.
This should remove some of the noisy patterns that otherwise arise,
especially from the LLVM translation, which uses length 1 bitvectors
as a stand-in for boolean values.
This commit mainly does two things:
* Add more robust support for the integer theory, including `div`, `mod`, `abs` and `divisible`.
* Audit the semantics of the `integerToBV` operations, and fix lingering bugs.
In the past, there were two different integer->BV operations, because we used a clamping semantics,
and it made sense to have a signed versus unsigned distinction. Now, however, we are using
a modulo `2^n` semantics, and there is only one operation. However, some places in the code were
still using the clamped semantics. These placses have now been cleaned up, and everywhere should
be using the modular arithmetic view.
In addition, I've reduced the need to use the expensive BV->Integer and Integer->BV coersions somewhat
by noticing when we round trip through those coercions more often and translating the result into
statements of modular arithmetic instead.
Along the way, I improved the abstract domain definitions for division and modulus.
