grisette

Symbolic evaluation as a library

https://github.com/lsrcz/grisette#readme

Version on this page:0.5.0.1@rev:2
Stackage Nightly 2024-10-31:0.8.0.0
Latest on Hackage:0.8.0.0

See all snapshots grisette appears in

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.5.0.1@sha256:8d05b1b6115cd71847ff8fbb50f7d5125ecbcd5d887994dde083f51d6192306a,12317

Module documentation for 0.5.0.1

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.5.0.1 < 0.6

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-19.33"

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 also 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 is significantly more efficient on some examples, but it does not support all of the examples.

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

Boolector from major package managers are usually outdated or inexist. We recommend that you build Boolector from source with the CaDiCaL SAT solver, which is usually more efficient on our examples. Please refer to the Boolector 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 may output the program (\x -> x+3). 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, and
    • its interpreter accepts such symbolic syntax trees, and interprete at once all represented concrete syntax trees.
  • 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-out example.

Defining the Arithmetic Language

We will synthesize single-input programs in this example. A single input program will be \x -> E, where E is an expression 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 synthesis a program, we need to define symbolic program spaces. This relies on the UnionM container provided by the library to represent multiple ASTs compactly in a single value.

To make this expression space type work with Grisette, a set of type classes should be derived. This includes Mergeable, EvaluateSym, etc. The Mergeable type classes allows to represent multiple ASTs compactly in a UnionM, while the EvaluateSym type class allows to evaluate it given a model returned by a solver to replace the symbolic holes inside to concrete values.

{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}

import Grisette
import GHC.Generics

data SExpr
  -- `SConst` represents a constant in the syntax tree.
  --
  -- `SConst 1` is the constant 1, while `SConst "c1"` is a symbolic constant,
  -- and the solver can be used to find out what the concrete value should be.
  = SConst SymInteger
  -- `SInput` is very similar to the `SConst`, but is for inputs. We separate
  -- these two mainly for clarity.
  | SInput SymInteger
  -- `SPlus` and `SMul` represent the addition and multiplication operators.
  --
  -- The children are **sets** of symbolic programs. Here `UnionM`s are such
  -- sets.
  --
  -- The solver will try to pick one concrete program from the set of programs.
  | SPlus (UnionM SExpr) (UnionM SExpr)
  | SMul (UnionM SExpr) (UnionM SExpr)
  -- `Generic` helps us derive other type class instances for `SExpr`.
  deriving stock (Generic, Show)
  -- Some type classes provided by Grisette for building symbolic evaluation
  -- tools. See the documentation for more details.
  deriving (Mergeable, EvaluateSym)
    via (Default SExpr)

-- A template haskell procedure to help the construction of `SExpr` sets.
--
-- >>> SConst 1 :: SExpr
-- SConst 1
-- >>> mrgSConst 1 :: UnionM SExpr
-- {SConst 1}
mkMergeConstructor "mrg" ''SExpr

Then we can define the program space. 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.

space :: SymInteger -> SExpr
space x = SPlus
  (mrgSInput x)
  (mrgIf "choice" (mrgSInput x) (mrgSConst "c"))

We then need to convert this program space to its logical encoding, and we do this by writing an interpreter to interpret all the expressions represented by an SExpr all at once. The interpreter looks very similar to a normal interpreter, except that the onUnion combinator is used to lift the interpreter to work on UnionM values.

interpret :: SExpr -> SymInteger
interpret (SConst x) = x
interpret (SInput x) = x
interpret (SPlus x y) = interpretU x + interpretU y
interpret (SMul x y) = interpretU x * interpretU y

-- interpet a set of programs
interpretU :: UnionM SExpr -> SymInteger
interpretU = onUnion interpret

And we can compose the interpreter with the program space to get 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 is able to find a solution, and it will return the assignments to the symbolic constants as a model.

We can then use the model to evaluate the program space, and get the synthesized program.

example :: IO ()
example = do
  Right model <- solve (precise z3) $ executableSpace 2 .== 5
  print $ evaluateSym False model (space "x")
  -- result: SPlus {SInput x} {SConst 3}
  let synthesizedProgram :: Integer -> Integer =
        evaluateSymToCon model . executableSpace
  print $ synthesizedProgram 10
  -- result: 13

For more details, please refer to the Grisette examples (WIP).

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.

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.

Unreleased

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.