BSD-3-Clause licensed by Sirui Lu, Rastislav Bodík
Maintained by Sirui Lu ([email protected])
This version can be pinned in stack with:grisette-0.8.0.0@sha256:9a9c0a4d2b1bedd343012ecbc38afddaa240542c6c9105844326c566a2e54279,16721

Module documentation for 0.8.0.0

Grisette

Haskell Tests Hackage Version Hackage Dependencies

Grisette is a symbolic evaluation library for Haskell. By translating programs into constraints, Grisette can help the development of program reasoning tools, including verification and synthesis.

For a detailed description of the system, please refer to our POPL’23 paper Grisette: Symbolic Compilation as a Functional Programming Library.

Features

  • Multi-path symbolic evaluation with efficient (customizable) state merging.
  • Symbolic evaluation is purely functional. The propagated symbolic value includes the assertion / error state of the execution, yet it is just a data structure. As a result, Grisette is a library that does not modify the Haskell compiler.
  • The separation of symbolic and concrete values is enforced with static types. These types help discover opportunities for partial evaluation as well as safe use of Haskell libraries.

Design and Benefits

  • Modular purely functional design, with a focus on composability.
    • Allows for symbolic evaluation of user-defined data structures / data structures from third-party libraries.
    • Allows for symbolic evaluation of error-handling code with user-defined error types.
    • Allows for memoization (tested and benchmarked) / parallelization (not tested and benchmarked yet) of symbolic evaluation.
  • Core multi-path symbolic evaluation semantics modeled as a monad, allowing for easy integration with other monadic effects, for example:
    • error handling via ExceptT,
    • stateful computation via StateT,
    • unstructured control flow via ContT, etc.

Installation

Install Grisette

Grisette is available via Hackage. You can add it to your project with cabal, and we also provided a stack template for quickly starting a new project with Grisette.

Manually writing cabal file

Grisette is a library and is usually used as a dependency of other packages. You can add it to your project’s .cabal file:

library
  ...
  build-depends: grisette >= 0.8 < 0.9

Quick start template with stack new

You can quickly start an stack-based Grisette project with stack new:

$ stack new <projectname> github:lsrcz/grisette

You can specify the resolver version with the parameters:

$ stack new a-new-project github:lsrcz/grisette -p "resolver:lts-22.27"

For more details, please see the template file and the documentation for stack templates.

You can test your installation by running the following command:

$ stack run app

The command assumes a working Z3 available through PATH. You can install it with the instructions below.

Install SMT Solvers

To run the examples, you need to install an SMT solver and make it available through PATH. We recommend that you start with Z3, as it supports all our examples and is usually easier to install. Boolector and its successor Bitwuzla are usually significantly more efficient on bit vectors.

Install Z3

On Ubuntu, you can install Z3 with:

$ apt update && apt install z3

On macOS, with Homebrew, you can install Z3 with:

brew install z3

You may also build Z3 from source, which may be more efficient on your system. Please refer to the Z3 homepage for the build instructions.

Install Boolector/Bitwuzla

Boolector/Bitwuzla from major package managers are usually outdated or inexist. We recommend that you build them from source with the CaDiCaL SAT solver. Please refer to the Boolector homepage and Bitwuzla homepage for the build instructions.

Example

The following example uses Grisette to build a synthesizer of arithmetic programs. Given the input-output pair (2,5), the synthesizer can tell us that the program \x -> x+3 has the desired behavior. The example is adapted from this blog post by James Bornholt.

The example has three parts:

  • We define the arithmetic language. The language is symbolic:
    • its syntax tree represents a set of concrete syntax trees (i.e., representing a program space), and
    • its interpreter accepts such symbolic syntax trees (program spaces), and interpret all represented concrete syntax trees to symbolic formulas.
  • We define the candidate program space of the synthesizer by creating a particular symbolic syntax tree. The synthesizer will search the space of concrete trees for a solution.
  • We interpret the symbolic syntax tree and pass the resulting constraints to the solver. If a solution exists, the solver returns a concrete tree that agrees with the input-output example.

Defining the Arithmetic Language

We will synthesize a single-input program \x -> E in this example. Here the E is an expression type, and is defined by the following grammar.

E -> c      -- constant
   | x      -- value for input variable
   | E + E  -- addition
   | E * E  -- multiplication

The syntax defines how a concrete expression is represented. To synthesize a program, we need to define symbolic program spaces. We do this with the Union container provided by Grisette to represent choices within multiple ASTs compactly in a single value.

data SymExpr
  -- `SymConst` represents a constant in the syntax tree.
  --
  -- `SymConst 1` is the constant 1, while `SymConst "c1"` is a symbolic
  -- constant, representing a hole in the expression. The solver can be used to
  -- find out what the concrete value for a symbolic constant should be.
  = SymConst SymInteger
  -- `SymInput` is exactly the same as `SymConst`, but is for inputs. We
  -- separate them just for clarity.
  | SymInput SymInteger
  -- `SymAdd` and `SymMul` represent the addition and multiplication operators.
  --
  -- The children are **choices** from some symbolic expressions, which is
  -- represented by the `Union` monadic container.
  --
  -- The solver will try to pick one choice from them.
  | SymAdd (Union SymExpr) (Union SymExpr)
  | SymMul (Union SymExpr) (Union SymExpr)
  -- `Generic` helps us derive other type class instances for `SymExpr`.
  deriving stock (Generic, Show)
  -- Some type classes provided by Grisette for building symbolic evaluation
  -- tools. See the documentation for more details.
  deriving (Mergeable, EvalSym) via (Default SymExpr)

-- The following template haskell procedures can also derive the instances we
-- need.
-- derive ''SymExpr [''Generic, ''Show, ''Mergeable, ''EvalSym]
-- deriveAllExcept ''SymExpr [''Ord]

Some smart constructors help us build program spaces.

-- A template haskell procedure generates smart constructors for
-- `Union SymExpr`.
--
-- >>> SymConst 1 :: SymExpr
-- SymConst 1
-- >>> mrgSymConst 1 :: Union SymExpr
-- {SymConst 1}
mkMergeConstructor "mrg" ''SymExpr

Then, the following code defines a program space \x -> x + {x, c}. Some example programs in this space are \x -> x + x, \x -> x + 1, and \x -> x + 2. The solver will be used to choose the right hand side of the addition. It may choose to use the input variable x, or synthesize a constant c.

progSpace :: SymInteger -> SymExpr
progSpace x =
  SymAdd
    (mrgSymInput x)
    (mrgIf "choice" (mrgSymInput x) (mrgSymConst "c"))

We can then convert this program space to its logical encoding and reason about it. This is done simply writing an interpreter to interpret all the expressions represented by an SymExpr all at once.

The interpreter is similar to a concrete interpreter, except that the onUnion combinator is used to lift the interpreter to work on Union values (a space of expressions).

interpret :: SymExpr -> SymInteger
interpret (SymConst x) = x
interpret (SymInput x) = x
interpret (SymAdd x y) = interpretSpace x + interpretSpace y
interpret (SymMul x y) = interpretSpace x * interpretSpace y

-- interpret a program space
interpretSpace :: Union SymExpr -> SymInteger
interpretSpace = onUnion interpret

We can then compose the interpreter with the program space to make it executable.

executableSpace :: Integer -> SymInteger
executableSpace = interpret . space . toSym

Then we can do synthesis. We call the program space on the input 2, and construct the constraint that the result is equal to 5. We then call the solver with the solve function. The solver finds a solution such that the condition evaluates to true. It returns the solution as a model, which contains an assignment to the symbolic constants (holes).

We can then get the synthesized program by evaluating the program space with the model.

example :: IO ()
example = do
  Right model <- solve z3 $ executableSpace 2 .== 5
  -- result: SymPlus {SymInput x} {SymConst 3}
  print $ evalSym False model (progSpace "x")
  let synthesizedProgram :: Integer -> Integer =
        evalSymToCon model . executableSpace
  -- result: 13
  print $ synthesizedProgram 10

The complete code is at examples/basic/Main.hs. More examples are available in Grisette’s tutorials.

Documentation

  • Haddock documentation at grisette.
  • A tutorial to Grisette is in the tutorials directory. They are provided as jupyter notebooks with the IHaskell kernel.

License

The Grisette library is distributed under the terms of the BSD3 license. The LICENSE file contains the full license text.

Note

Grisette is fully compatible with GHC 9.6+, and works in most cases with GHC 8.10+.

CLC proposal #10

As the type classes provided by Grisette implements CLC proposal #10, which requires base-4.18.0.0 to work reliably, Grisette is fully compatible with GHC 9.6. You may experience instance resolution failure when using older GHCs in the client code (Grisette itself is buildable against GHC 8.10+ with some tricks).

Quantifiers

Grisette currently supports universal and existential quantifiers $\forall$ and $\exists$, but only when building with sbv >= 10.1. This also means that you need to use GHC >= 9.2.

Floating-points

Grisette currently supports boolean, uninterpreted functions, bitvector, integer, and floating point theories. However, if you want to use the floating point theory, please make sure that you have the latest libBF (>=0.6.8) and sbv installed (>=10.10.6). We’ve detected and fixed several bugs that would prevent a sound reasoning for floating points.

Unified interfaces

Since 0.7.0.0, Grisette provides a unified interface to symbolic and concrete evaluations. GHC 9.0 or earlier, without the QuickLook type inference algorithm for impredicative types, may fail to resolve some constraints. You may need to provide additional constraints in your code to help the compiler.

Citing Grisette

If you use Grisette in your research, please use the following bibtex entry:

@article{10.1145/3571209,
author = {Lu, Sirui and Bod\'{\i}k, Rastislav},
title = {Grisette: Symbolic Compilation as a Functional Programming Library},
year = {2023},
issue_date = {January 2023},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {7},
number = {POPL},
url = {https://doi.org/10.1145/3571209},
doi = {10.1145/3571209},
abstract = {The development of constraint solvers simplified automated reasoning about programs and shifted the engineering burden to implementing symbolic compilation tools that translate programs into efficiently solvable constraints. We describe Grisette, a reusable symbolic evaluation framework for implementing domain-specific symbolic compilers. Grisette evaluates all execution paths and merges their states into a normal form that avoids making guards mutually exclusive. This ordered-guards representation reduces the constraint size 5-fold and the solving time more than 2-fold. Grisette is designed entirely as a library, which sidesteps the complications of lifting the host language into the symbolic domain. Grisette is purely functional, enabling memoization of symbolic compilation as well as monadic integration with host libraries. Grisette is statically typed, which allows catching programming errors at compile time rather than delaying their detection to the constraint solver. We implemented Grisette in Haskell and evaluated it on benchmarks that stress both the symbolic evaluation and constraint solving.},
journal = {Proc. ACM Program. Lang.},
month = {jan},
articleno = {16},
numpages = {33},
keywords = {State Merging, Symbolic Compilation}
}

Changes

Changelog

All notable changes to this project will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

0.8.0.0 - 2024-08-13

Added

  • Added pretty printer for models. (#225)
  • Added support for algebraic reals (AlgReal and SymAlgReal). (#228, #229)
  • Added support for quantifiers. (#230)
  • Added SafeFdiv, SafeLogBase, DivOr, FdivOr, and LogBaseOr. (#228, #231)
  • Added bitcast from and to Bool, IntN, WordN, FP and their symbolic counterparts when appropriate. (#232)
  • Add SymFromIntegral. (#233)
  • Add operations for concrete floating point numbers. Add IEEE754-2019 fpMinimum, fpMinimumNumber, fpMaximum, and fpMaximumNumber operations. (#235)
  • Add conversion from and to floating points. (#236)
  • Add SymFiniteBits. (#237)
  • Add unified instances for all provided operations, including FP and AlgReal. (#239, #240, #243)
  • Allow the use of number literals for SomeBV. (#245)
  • Add symDistinct. (#246, #247)

Fixed

  • Fixed model parsing for floating points. (#227)
  • Allowed mkUnifiedConstructor to be used with types without modes or args. (#242)

Changed

  • [Breaking] Changed the operand order for liftPFormatPrec2 and liftPFormatList2. (#225)
  • [Breaking] Changed the term representation with a compile-time tag for its kind (AnyKind for all symbols and ConstantKind for symbols other than uninterpreted functions). This also affects the ‘ExtractSym’. A new extractSymMaybe will regard this tag if not all symbols can be casted to that tag. extractSym will always succeed, returning a set with AnyKind. (#230)
  • [Breaking] SafeDivision renamed to SafeDiv. (#231)
  • Refined the template-haskell-based derivation mechanism. (#238)
  • [Breaking] GetData is made injective by giving Identity wrapped type for concrete evaluation instead of the type itself. (#242)
  • Changed pprint for Identity to not to print the constructor. (#242)
  • Make ToSym requires the target type to be Mergeable. This enable us to merge the results for converting from Union a to Union b again. (#244)

Removed

  • Removed fpMin and fpMax, which is removed in IEEE754-2019. (#235)
  • Dropped support for post-evaluation approximation. (#241)

0.7.0.0 - 2024-07-02

Added

  • Added true and false in LogicalOp. (#211)
  • Exported the FP constructs in the Grisette module. (#209)
  • Added missing AllSyms instance for WordN, IntN, and FP. (#209)
  • Added unified interfaces. (#210, #212, #213, #214, #215, #217)
  • Added IEEEFPRoundingMode. (#219)
  • Added Show instance for SomeSym. (#219)
  • Added incoherent conversions (ToSym, ToCon) from/to Identity a and a. (#221)

Fixed

  • Fixed the printing of FP terms. (#219)

Changed

  • [Breaking] Relaxed constraints for type classes, according to https://github.com/haskell/core-libraries-committee/issues/10. One problem this causes is that the instances for Union will no longer be able to always merge the results. This is unfortunate, but should not be critical. (#213, #214, #221)
  • [Breaking] Rewritten the generic derivation mechanism. (#213, #214, #216)
  • [Breaking] Changed the type class hierarchy for operations for functors, e.g. SEq1, as described in https://github.com/haskell/core-libraries-committee/issues/10. (#216)
  • [Breaking] Renamed UnionMergeable1 to SymBranching. Renamed Union to UnionBase, and UnionM to Union. (#214, #217)
  • [Breaking] Renamed EvaluateSym to EvalSym. Renamed SubstituteSym to SubstSym. Renamed ExtractSymbolics to ExtractSym. (#217)
  • [Breaking] Renamed SEq to SymEq. Renamed SOrd to SymOrd. (#217)
  • [Breaking] Renamed GPretty to PPrint. (#217, #224)
  • [Breaking] Discourage the use of approximation with approx. precise is now the default and we do not require precise to be used everytime we call a solver. (#218)

0.6.0.0 – 2024-06-07

Added

  • Added solving procedures with solver handles. (#198)
  • Added overestimateUnionValues. (#203)
  • Added pretty printing for hashset and hashmaps. (#205)
  • Added support for refinement of solutions in CEGIS algorithm. (#206)
  • Added generation of globally unique identifier with uniqueIdentifier. (#206)
  • Added support for arbitrary precision floating point theory. (#207)

Fixed

  • withSolver now forcifully terminate the solver when exiting the scope. (#199)
  • Fixed pretty printing for monad transformers. (#205)

Changed

  • [Breaking] Equality test for SomeBV with different bit widths will now return false rather than crash. (#200)
  • [Breaking] More intuitive CEGIS interface. (#201)
  • [Breaking] Changed the low-level solver interface. (#206)
  • [Breaking] Changed the CEGIS interface. (#206)
  • Bumped the minimum supported sbv version to 8.17. (#207)

0.5.0.1 – 2024-04-18

Fixed

0.5.0.0 – 2024-04-18

Added

  • Added the creation of unparameterized bit vectors from run-time bit-widths. (#168, #177)
  • Added all the functions available for the exception transformer in transformers and mtl packages. (#171)
  • Improved the partial evaluation for bit vectors. (#176)
  • Added symRotateNegated and symShiftNegated. (#181)
  • Added mrg and sym variants for all reasonable operations from Control.Monad, Control.Applicative, Data.Foldable, Data.List, and Data.Traversable. (#182)
  • Added mrgIfPropagatedStrategy. (#184)
  • Added freshString. (#188)
  • Added localFreshIdent. (#190)
  • Added deriving for void types for builtin type classes. (#191)

Fixed

  • Fixed the merging for safe division. (#173)
  • Fixed the behavior for safe mod and rem for signed, bounded concrete types. (#173)
  • Fixed merging in mrg* operations for monad transformers to ensure that they merge the results. (#187)

Changed

  • [Breaking] Removed the UnionLike and UnionPrjOp interface, added the TryMerge and PlainUnion interface. This allows mrg* operations to be used with non-union programs. (#170)
  • [Breaking] Refined the safe operations interface using TryMerge. (#172)
  • [Breaking] Renamed safeMinus to safeSub to be more consistent. (#172)
  • [Breaking] Unifies the implementation for all symbolic non-indexed bit-vectors. The legacy types are now type and pattern synonyms. (#174, #179, #180)
  • [Breaking] Use functional dependency instead of type family for the Function class. (#178)
  • [Breaking] Added Mergeable constraints to some mrg* list operators (#182)
  • [Breaking] Refactored the mrg* constructor related template haskell code. (#185)
  • [Breaking] Dropped symbols with extra information. (#188)
  • [Breaking] The FreshIdent is removed. It is now changed to Identifier and Symbol types. (#192)
  • Changed the internal representation of the terms. (#193)
  • [Breaking] Refactored the project structures. (#194)

0.4.1.0 – 2024-01-10

Added

  • Added cegisForAll interfaces. (#165)

0.4.0.0 – 2024-01-08

Added

  • Added wrappers for state transformers. (#132)
  • Added toGuardList function. (#137)
  • Exported some previously hidden API (BVSignConversion, runFreshTFromIndex) that we found useful or forgot to export. (#138, #139)
  • Provided mrgRunFreshT to run FreshT with merging. (#140)
  • Added Grisette.Data.Class.SignConversion.SignConversion for types from Data.Int and Data.Word. (#142)
  • Added shift functions by symbolic shift amounts. (#151)
  • Added apply for uninterpreted functions. (#155)
  • Added liftFresh to lift a Fresh into MonadFresh. (#156)
  • Added a handle types for SBV solvers. This allows users to use SBV solvers without the need to wrap everything in the SBV monads. (#159)
  • Added a new generic CEGIS interface. This allows any verifier/fuzzer to be used in the CEGIS loop. (#159)

Removed

  • [Breaking] Removed the Grisette.Lib.Mtl module. (#132)
  • [Breaking] Removed SymBoolOp and SymIntegerOp. (#146)
  • [Breaking] Removed ExtractSymbolics instance for SymbolSet. (#146)

Fixed

  • Removed the quotation marks around the pretty printed results for string-like data types. (#127)
  • Fixed the SOrd instance for VerificationConditions. (#131)
  • Fixed the missing SubstituteSym instance for UnionM. (#131)
  • Fixed the symbolic generation order for Maybe. (#131)
  • Fixed the toInteger function for IntN 1. (#143)
  • Fixed the abs function for WordN. (#144)
  • Fixed the QuickCheck shrink function for WordN 1 and IntN 1. (#149)
  • Fixed the heap overflow bug for shiftL for WordN and IntN by large numbers. (#150)

Changed

  • Reorganized the files for MonadTrans. (#132)
  • [Breaking] Changed the name of Union constructors and patterns. (#133)
  • The Union patterns, when used as constructors, now merges the result. (#133)
  • Changed the symbolic identifier type from String to Data.Text.Text. (#141)
  • [Breaking] Grisette.Data.Class.BitVector.BVSignConversion is now Grisette.Data.Class.SignConversion.SignConversion. (#142)
  • [Breaking] Moved the ITEOp, LogicalOp, and SEq type classes to dedicated modules. (#146)
  • [Breaking] Moved Grisette.Data.Class.Evaluate to Grisette.Data.Class.EvaluateSym. (#146)
  • [Breaking] Moved Grisette.Data.Class.Substitute to Grisette.Data.Class.SubstituteSym. (#146)
  • [Breaking] Split the Grisette.Data.Class.SafeArith module to Grisette.Data.Class.SafeDivision and Grisette.Data.Class.SafeLinearArith. (#146)
  • [Breaking] Changed the API to MonadFresh. (#156)
  • [Breaking] Renamed multiple symbolic operators. (#158)
  • [Breaking] Changed the solver interface. (#159)
  • [Breaking] Changed the CEGIS solver interface. (#159)

0.3.1.1 – 2023-09-29

No user-facing changes.

0.3.1.0 – 2023-07-19

Added

  • Added support to Data.Text. (#95)
  • Added Arbitrary instances for bit vectors. (#97)
  • Added pretty printers for Grisette data types. (#101)
  • Added ExtractSymbolics instances for tuples longer than 2. (#103)

Fixed

  • Fixed the Read instance for bit vectors. (#99, #100)

0.3.0.0 – 2023-07-07

Added

  • Added the conversion between signed and unsigned bit vectors. (#69)
  • Added the generation of SomeSymIntN and SomeSymWordN from a single Int for bit width. (#73)
  • Added the FiniteBits instance for SomeSymIntN and SomeSymWordN. (#83)
  • Added more flexible instances for symbolic generation for Either, Maybe and list types. (#84)
  • Added an experimental GenSymConstrained type class. (#89)

Changed

  • Changed the operations for SomeIntN and SomeWordN to accepting dynamic runtime integers rather than compile-time integers. (#71)
  • Comparing the equality of SomeIntN/SomeWordN/SomeSymIntN/SomeSymWordN with different bit widths returns false rather than crash now. (#74)

Fixed

  • Fixed the compatibility issue with sbv 10+. (#66)
  • Fixed build error with newer GHC. (#70)
  • Fixed the merging for SomeSymIntN and SomeSymWordN. (#72)

0.2.0.0 - 2023-04-13

Added

  • Add term size count API. (#48, #53)
  • Add timeout to solver interface. (#49, #50)
  • Add parallel do-notation for parallel symbolic compilation. (#51)
  • Added some missing instances for symbolic values and bit vectors. (#46, #61)
  • Add missing instances for MonadFresh and FreshT. (#59)

Changed

  • New safe operator interfaces. (#56)
  • Redesigned symbolic value interface.
    • Sym Bool/Sym Integer, etc., are no longer available and are replaced with SymBool and SymInteger. (#41)
    • New symbolic bit vector interface. Added unsized bit vector. (#41)

Removed

  • Dropped merging cache for UnionM. This fixed some segmentation fault errors. (#43)

Fixed

  • Fix CEGIS when no symbolic input is present. (#52)
  • Fix overlapping ToSym and ToCon instances. (#54)
  • Fix uninterpreted function lowering. (#57, #58)
  • Fix CEGIS crash when subsequent solver calls introduces new symbolic constant. (#60)

0.1.0.0 - 2023-01-20

Added

  • Initial release for Grisette.