what4
Solver-agnostic symbolic values support for issuing queries
https://github.com/GaloisInc/what4
LTS Haskell 23.1: | 1.6.2 |
Stackage Nightly 2024-12-23: | 1.6.2 |
Latest on Hackage: | 1.6.2 |
what4-1.6.2@sha256:953b5b11f79a66e8f3769c52615009f79bcc63908345365dbeadb0050595d48d,10716
Module documentation for 1.6.2
- Test
- What4
- What4.BaseTypes
- What4.Concrete
- What4.Config
- What4.Expr
- What4.FloatMode
- What4.FunctionName
- What4.IndexLit
- What4.Interface
- What4.InterpretedFloatingPoint
- What4.LabeledPred
- What4.Panic
- What4.Partial
- What4.ProblemFeatures
- What4.ProgramLoc
- What4.Protocol
- What4.SFloat
- What4.SWord
- What4.SatResult
- What4.SemiRing
- What4.Serialize
- What4.Solver
- What4.SpecialFunctions
- What4.Symbol
- What4.Utils
- What4.Utils.AbstractDomains
- What4.Utils.AnnotatedMap
- What4.Utils.Arithmetic
- What4.Utils.BVDomain
- What4.Utils.Complex
- What4.Utils.Endian
- What4.Utils.Environment
- What4.Utils.FloatHelpers
- What4.Utils.HandleReader
- What4.Utils.IncrHash
- What4.Utils.LeqMap
- What4.Utils.MonadST
- What4.Utils.OnlyIntRepr
- What4.Utils.Process
- What4.Utils.ResolveBounds
- What4.Utils.Serialize
- What4.Utils.Streams
- What4.Utils.StringLiteral
- What4.Utils.Versions
- What4.Utils.Word16String
- What4.WordMap
What4
Introduction
What is What4?
What4 is a Haskell library developed at Galois that presents a generic interface to SMT solvers (Z3, Yices, etc.). Users of What4 use an embedded DSL to create fresh constants representing unknown values of various types (integer, boolean, etc.), assert various properties about those constants, and ask a locally-installed SMT solver for satisfying instances.
What4 relies heavily on advanced GHC extensions to ensure that solver
expressions are type correct. The parameterized-utils
library is used
throughout What4 as a “standard library” for dependently-typed Haskell.
Quick start
Let’s start with a quick end-to-end tutorial, demonstrating how to create a
model for a basic satisfiability problem and ask a solver for a satisfying
instance. The code for this quick start may be found in
doc/QuickStart.hs
, and you can compile and run the quickstart
by executing the following line at the command line from the
source root of this package.
$ cabal v2-run what4:quickstart
We will be using an example from the first page of Donald Knuth’s The Art Of Computer Programming, Volume 4, Fascicle 6: Satisfiability:
F(p, q, r) = (p | !q) & (q | r) & (!p | !r) & (!p | !q | r)
We will use What4 to:
- generate fresh constants for the three variables
p
,q
, andr
- construct an expression for
F
- assert that expression to our backend solver
- ask the solver for a satisfying instance.
We first enable the GADTs
extension (necessary for most
uses of What4) and pull
in a number of modules from What4 and parameterized-utils
:
{-# LANGUAGE GADTs #-}
module Main where
import Data.Foldable (forM_)
import System.IO (FilePath)
import Data.Parameterized.Nonce (newIONonceGenerator)
import Data.Parameterized.Some (Some(..))
import What4.Config (extendConfig)
import What4.Expr
( ExprBuilder, FloatModeRepr(..), newExprBuilder
, BoolExpr, GroundValue, groundEval
, EmptyExprBuilderState(..) )
import What4.Interface
( BaseTypeRepr(..), getConfiguration
, freshConstant, safeSymbol
, notPred, orPred, andPred )
import What4.Solver
(defaultLogData, z3Options, withZ3, SatResult(..))
import What4.Protocol.SMTLib2
(assume, sessionWriter, runCheckSat)
We create a trivial data type for the “builder state” (which we won’t need to use for this simple example), and create a top-level constant pointing to our backend solver, which is Z3 in this example. (To run this code, you’ll need Z3 on your path, or edit this path to point to your Z3.)
z3executable :: FilePath
z3executable = "z3"
We’re ready to start our main
function:
main :: IO ()
main = do
Some ng <- newIONonceGenerator
sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng
Most of the functions in What4.Interface
, the module for building up
solver expressions, require an explicit sym
parameter. This
parameter is a handle for a data structure that caches information for
sharing common subexpressions and other bookkeeping
purposes. What4.Expr.Builder.newExprBuilder
creates one of these,
and we will use this sym
throughout our code.
Before continuing, we will set up some global configuration for Z3. This sets up some configurable options specific to Z3 with default values.
extendConfig z3Options (getConfiguration sym)
We declare fresh constants for each of our propositional variables.
p <- freshConstant sym (safeSymbol "p") BaseBoolRepr
q <- freshConstant sym (safeSymbol "q") BaseBoolRepr
r <- freshConstant sym (safeSymbol "r") BaseBoolRepr
Next, we create expressions for their negation.
not_p <- notPred sym p
not_q <- notPred sym q
not_r <- notPred sym r
Then, we build up each clause of F
individually.
clause1 <- orPred sym p not_q
clause2 <- orPred sym q r
clause3 <- orPred sym not_p not_r
clause4 <- orPred sym not_p =<< orPred sym not_q r
Finally, we can create F
out of the conjunction of these four clauses.
f <- andPred sym clause1 =<<
andPred sym clause2 =<<
andPred sym clause3 clause4
Now we can we assert f
to the backend solver (Z3, in this example), and ask for
a satisfying instance.
-- Determine if f is satisfiable, and print the instance if one is found.
checkModel sym f [ ("p", p)
, ("q", q)
, ("r", r)
]
(The checkModel
function is not a What4 function; its definition is provided
below.)
Now, let’s add one more clause to F
which will make it unsatisfiable.
-- Now, let's add one more clause to f.
clause5 <- orPred sym p =<< orPred sym q not_r
g <- andPred sym f clause5
Now, when we ask the solver for a satisfying instance, it should report that the formulat is unsatisfiable.
checkModel sym g [ ("p", p)
, ("q", q)
, ("r", r)
]
This concludes the definition of our main
function. The definition for
checkModel
is as follows:
-- | Determine whether a predicate is satisfiable, and print out the values of a
-- set of expressions if a satisfying instance is found.
checkModel ::
ExprBuilder t st fs ->
BoolExpr t ->
[(String, BoolExpr t)] ->
IO ()
checkModel sym f es = do
-- We will use z3 to determine if f is satisfiable.
withZ3 sym z3executable defaultLogData $ \session -> do
-- Assume f is true.
assume (sessionWriter session) f
runCheckSat session $ \result ->
case result of
Sat (ge, _) -> do
putStrLn "Satisfiable, with model:"
forM_ es $ \(nm, e) -> do
v <- groundEval ge e
putStrLn $ " " ++ nm ++ " := " ++ show v
Unsat _ -> putStrLn "Unsatisfiable."
Unknown -> putStrLn "Solver failed to find a solution."
When we compile this code and run it, we should get the following output.
Satisfiable, with model:
p := False
q := False
r := True
Unsatisfiable.
Where to go next
The key modules to look at when modeling a problem with What4 are:
What4.BaseTypes
(the datatypes What4 understands)What4.Interface
(the functions What4 uses to build symbolic expressions)What4.Expr.Builder
(the implementation of the functions inWhat4.Interface
)
The key modules to look at when interacting with a solver are:
What4.Protocol.SMTLib2
(the functions to interact with a solver backend)What4.Solver
(solver-specific implementations ofWhat4.Protocol.SMTLib2
)What4.Solver.*
What4.Protocol.Online
(interface for online solver connections)What4.SatResult
andWhat4.Expr.GroundEval
(for analyzing solver output)
Additional implementation and operational documentation can be found in the implementation documentation in doc/implementation.md.
To serialize and deserialize what4 terms, see the following modules:
What4.Serialize.Printer
(to serialize what4 terms into an s-expression format)What4.Serialize.Parser
(to deserialize what4 terms)What4.Serialize.FastSExpr
(provides a faster s-expression parser than the default, intended to be used in conjunction with the higher-level parsing inWhat4.Serialize.Parser
)
Formula Construction vs Solving
In what4, building expressions and solving expressions are orthogonal concerns.
When you create an ExprBuilder
(with newExprBuilder
), you are not committing
to any particular solver or solving strategy (except insofar as the selected
floating point mode might preclude the use of certain solvers). There are two
dimensions of solver choice: solver and mode. The supported solvers are listed
in What4.Solver.*
. There are two modes:
- All solvers can be used in an “offline” mode, where a new solver process is
created for each query (e.g., via
What4.Solver.solver_adapter_check_sat
) - Many solvers also support an “online” mode, where what4 maintains a persistent
connection to the solver and can issue multiple queries to the same solver
process (via the interfaces in
What4.Protocol.Online
)
There are a number of reasons to use solvers in online mode. First, state
(i.e., previously defined terms and assumptions) can be shared between queries.
For a series of closely related queries that share context, this can be a
significant performance benefit. Solvers that support online solving provide
the SMT push
and pop
primitives for maintaining context frames that can be
discarded (to define local bindings and assumptions). The canonical use of
online solving is symbolic execution, which usually requires reflecting the
state of the program at every program point into the solver (in the form of a
path condition) and using push
and pop
to mimic the call and return
structure of programs. Second, reusing a single solver instance can save process
startup overhead in the presence of many small queries.
While it may always seem advantageous to use the online solving mode, there are advantages to offline solving. As offline solving creates a fresh solver process for each query, it enables parallel solving. Online solving necessarily serializes queries. Additionally, offline solving avoids the need for complex state management to synchronize the solver state with the state of the tool using what4. Additionally, not all solvers that support online interaction support per-goal timeouts; using offline solving trivially allows users of what4 to enforce timeouts for each solved goal.
Known working solver versions
What4 has been tested and is known to work with the following solver versions.
Nearby versions may also work; however, subtle changes in solver behavior from version to version sometimes happen and can cause unexpected results, especially for the more experimental logics that have not been standardized. If you encounter such a situation, please open a ticket, as our goal is to work correctly on as wide a collection of solvers as is reasonable.
- Z3 versions 4.8.7 through 4.8.12
- Yices 2.6.1 and 2.6.2
- CVC4 1.7 and 1.8
- CVC5 1.0.2
- Bitwuzla 0.3.0
- Boolector 3.2.1 and 3.2.2
- STP 2.3.3 (However, note https://github.com/stp/stp/issues/363, which prevents effective retrieval of model values. This should be resolved by the next release)
- dReal v4.20.04.1
Note that the integration with Z3, Yices and CVC4 has undergone significantly more testing than the other solvers.
Changes
1.6.2 (Sep 2024)
- Allow building with GHC 9.10.
1.6.1 (Sep 2024)
-
Fix a bug in which
what4
’s CVC5 adapter would fail to parse models involving structs. (#265) -
Add
What4.Expr.GroundEval.groundToSym
, which allows injectingGroundValue
s back intoSymExpr
s. (#268)
1.6 (May 2024)
-
Allow building with GHC 9.8.
-
Add more robust support for Constrained Horn Clause (CHC) solving:
- The
IsSymExprBuilder
class now has two additional methods,transformPredBV2LIA
andtransformSymFnLIA2BV
, which describe how to transform a bitvector (BV) predicate into a linear integer arithmetic (LIA) predicate and vice versa. - The
runZ3Horn
andwriteZ3HornSMT2File
functions now take an additionalBool
argument. When this argument isTrue
, Z3 will transform bitvector CHCs into linear integer arithmetic CHCs, which can sometimes help Z3 to solve CHC problems that it couldn’t in a bitvector setting.
- The
-
Add support for the
bitwuzla
SMT solver. -
Add
bvZero
andbvOne
functions, which are convenient shorthand for constructing bitvectors with the values0
and1
, respectively. -
Add
pushMuxOps
andpushMuxOpsOption
. If this option is enabled, What4 will push certainExprBuilder
operations (e.g.,zext
) down to the branches ofite
expressions. In some (but not all) circumstances, this can result in operations that are easier for SMT solvers to reason about. -
annotateTerm
no longer adds annotations to bound variable expressions, which already have annotations attached to them. This should result in slightly better performance and better pretty-printing.
1.5.1 (October 2023)
- Require building with
versions >= 6.0.2
.
1.5 (July 2023)
-
Allow building with GHC 9.6.
-
The
MonadTrans (PartialT sym)
instance now has aIsExpr (SymExpr sym)
constraint in its instance context. (This is a requirement imposed byMonadTrans
gaining a quantifiedMonad
superclass inmtl-2.3
.) -
Make
what4
simplify expressions of the form(bvult (bvadd a c) (bvadd b c))
to(bvult a b)
when it is sound to do so.
1.4 (January 2023)
-
Allow building with GHC 9.4.
-
Remove the
MonadFail
instance forVarRecorder
, as this instance is no longer straightforward to define due to upstream changes inbase-4.17.0.0
. This instance ultimately callederror
anyways, so any uses offail
at typeVarRecorder
can be replaced witherror
without any change in behavior. -
Remove a dependency on
data-binary-ieee754
, which has been deprecated. -
Deprecate
allSupported
which represents the SMT logicALL_SUPPORTED
, and addallLogic
instead which represents the SMTLib standard logicALL
. -
Add support for the cvc5 SMT solver.
-
Add a
get-abduct
feature which is compatible with cvc5. -
Add modules to support serialization and deserialization of what4 terms into an s-expression format that is a superset of SMTLib2. See the
What4.Serialize.Printer
,What4.Serialize.Parser
, andWhat4.Serialize.FastSExpr
modules. Note that these modules have names that conflict with the now deprecated what4-serialize package, from which they were copied. If you are updating to this version of what4, delete your dependency on what4-serialize. -
Add support Syntax-Guided Synthesis (SyGuS) in CVC5 (through the
runCVC5SyGuS
function) and Constrained Horn Clauses (CHC) in Z3 (through therunZ3Horn
function). -
Make
what4
smarter about simplifyingintMin x y
andintMax x y
expressions when eitherx <= y
ory <= x
can be statically determined.
1.3 (April 2022)
-
Allow building with GHC 9.2.
-
According to this discussion, the
forall
identifier will be claimed, andforall
made into a full keyword. Therefore, theforall
andexists
combinators ofWhat4.Protocol.SMTLib2.Syntax
have been renamed intoforall_
andexists_
. -
Add operations for increased control over the scope of configuration options, both in the
What4.Config
andWhat4.Expr.Builder
modules. -
Previously, the
exprCounter
,sbUserState
,sbUnaryThreshold
, andsbCacheStartSize
fields ofExprBuilder
were directly exposed; in principle this allows users to modify them, which was not intended in some cases. These have been uniformly renamed to remove thesb
prefix, and exposed asGetter
orLens
values instead, as appropriate. -
The
sbBVDomainRangeLimit
fields ofExprBuilder
was obsolete and has been removed. -
Allow building with
hashable-1.4.*
:- Add
Eq
instances for all data types withHashable
instances that were missing correspondingEq
instances. This is required sincehashable-1.4.0.0
adds anEq
superclass toHashable
. - Some
Hashable
instances now have extra constraints to match the constraints in their correspondingEq
instances. For example, theHashable
instance forSymNat
now has an extraTestEquality
constraint to match itsEq
instance.
- Add
-
Add an
unsafeSetAbstractValue
function to theIsExpr
class which allows one to manually set theAbstractValue
used in a symbolic expression. As the name suggests, this function is unsound in the general case, so use this with caution. -
Add a
What4.Utils.ResolveBounds.BV
module, which provides aresolveSymBV
function that checks if aSymBV
is concrete. If it is not concrete, it returns the lower and upper version bounds, as determined by querying an online SMT solver. -
Add
arrayCopy
,arraySet
, andarrayRangeEq
methods toIsExprBuilder
. -
Add a
getUnannotatedTerm
method toIsExprBuilder
for retrieving the original, unannotated term out of an annotated term. -
IsExprBuilder
now hasfloatSpecialFunction{,0,1,2}
andrealSpecialFunction{,0,1,2}
methods which allow the use of special values or functions such aspi
, trigonometric functions, exponentials, or logarithms. Similarly,IsInterpretedFloatExprBuilder
now hasiFloatSpecialFunction{,0,1,2}
methods. Although little solver support exists for special functions,what4
may be able to prove properties about them in limited cases.- The
realPi
,realLog
,realExp
,realSin
,realCos
,realTan
,realSinh
,realCosh
,realTanh
, andrealAtan2
methods ofIsExprBuilder
now have default implementations in terms ofrealSpecialFunction{,0,1,2}
.
- The
-
Add an
exprUninterpConstants
method toIsSymExprBuilder
which returns the set of uninterpreted constants in a symbolic expression. -
Add a
natToIntegerPure
function which behaves likenatToInteger
but without usingIO
. -
asConcrete
now supports concretizing float expressions by way of the newConcreteFloat
constructor inConcreteVal
. -
Add a
z3Tactic
configuration option toWhat4.Solver.Z3
that allows specifying a custom tactic to pass toz3
. -
safeSymbol
now replaces exclamation marks (!
) with underscores (_
) so that the generated names are legal in Verilog. -
Add
Foldable
,Traversable
, andShow
instances forLabeledPred
. -
Fix a bug in which
what4
would generate incorrect SMTLib code for array lookups and updates when using the CVC4 backend. -
Fix a bug in which
what4
would incorrectly attempt to configure Boolector 3.2.2 or later. -
Fix a bug in which strings containing
\u
or ending with\
would be escaped incorrectly.
1.2.1 (June 2021)
- Include test suite data in the Hackage tarball.
1.2 (June 2021)
This is primarily a bugfix release, but also adds support for GHC 9.x
-
Tweaks to the
SolverEvent
data type to remove partial fields. -
Fix issue #126. The shift operations of
What4.SWord
were not correctly handling cases where the shift amount has more bits than the word to be shifted. -
Fix issue #121. The ordering of inputs in generated Verilog files is now more predictable. Previously, it was determined by the order the inputs were encountered during term traversal. Now the user can provide a list of (input, name) pairs which are declared in order. Any additional inputs discovered during traversal will be added after these specified inputs.
-
Fix issue #113. The
bvSliceLE
andbvSliceBE
functions ofWhat4.SWord
did not properly handle size 0 bit-vectors and requests for 0 length slices. They now correctly fail for slice lengths longer than 0 on 0-length vectors, and correctly allow 0 length slices regardless of the length of the input. -
Fix issue #103. Some of the string operations would give incorrect results when string offsets are out-of-bounds. The SMTLib 2.6 standard specifies precise results for these cases, which we now implement.
-
Configuration parameters relative to solvers have been renamed in a more consistent and heirarchical fashion; the old configuration parameters still work but will emit deprecation warnings when used.
default_solver
–>solver.default
abc_path
–>solver.abc.path
boolector_path
–>solver.boolector.path
cvc4_path
–>solver.cvc4.path
cvc4.random-seed
–>solver.cvc4.random-seed
cvc4_timeout
–>solver.cvc4.timeout
dreal_path
–>solver.dreal.path
stp_path
–>solver.stp.path
stp.random-seed
–>solver.stp.random-seed
yices_path
–>solver.yices.path
yices_enable-mcsat
–>solver.yices.enable-mcsat
yices_enable-interactive
–>solver.yices.enable-interactive
yices_goal_timeout
–>solver.yices.goal-timeout
yices.*
–>solver.yices.*
for many yices internal optionsz3_path
–>solver.z3.path
z3_timeout
–>solver.z3.timeout
-
Added the
solver.strict_parsing
configuration parameter. This is enabled by default but could be disabled to allow running solvers in debug mode or to workaround other unexpected output from solver processes.
1.1 (February 2021)
-
Use multithread-safe storage primitive for configuration options, and clarify single-threaded use assumptions for other data structures.
-
Fix issue #63, which caused traversals to include the bodies of defined functions at call sites, which yielded confusing results.
-
Add concrete evaluation and constant folding for floating-point operations via the
libBF
library. -
Add min and max operations for integers and reals to the expression interface.
-
Remove
BaseNatType
from the set of base types. There were bugs relating to having nat types appear in structs, arrays and functions that were difficult to fix. Natural number values are still available as scalars (where they are represented by integers with nonzero assumptions) via theSymNat
type. -
Support for exporting What4 terms to Verilog syntax.
-
Various documentation fixes and improvements.
-
Test coverage improvements.
-
Switch to use the
prettyprinter
package for user-facing output.
1.0 (July 2020)
- Initial Hackage release