G2 Haskell Symbolic Execution Engine

---

About

G2 performs lazy symbolic execution of Haskell programs to detect state reachability. It is capable of generating assertion failure counterexamples and solving for higher-order functions.

---

Dependencies

• GHC: https://www.haskell.org/ghc/
• Custom Haskell Standard Library: https://github.com/BillHallahan/base-4.9.1.0
• Z3 SMT Solver: https://github.com/Z3Prover/z3

---

Setup:

1. Install GHC.
2. Install Z3. Ensure Z3 is in your system's path.
3. Pull the Custom Haskell Standard Library into ~/.g2 by running bash base_setup.sh.

---

Command line:

Reachability:

cabal run G2 ./tests/Samples/Peano.hs add

LiquidHaskell:

cabal run G2LH ./tests/Liquid/Peano.hs add

Arguments:

• --n number of reduction steps to run
• --max-outputs number of inputs/results to display
• --smt Pass "z3" or "cvc5" to select a solver [Default: Z3]
• --time Set a timeout in seconds

---

Plugin:

Running G2 on code in cabal packages can be done by means of a plugin. To do this:

1. Add a cabal.project file containing:

package *
    ghc-options:      -fexpose-all-unfoldings

this instructs GHC to make the Core of every function from every package available, which is needed to symbolically execute code in dependencies.

2. Add a dependency on G2, and

ghc-options:      -fplugin=G2.Plugin -fplugin-opt=G2.Plugin:[Optionally, arguments for G2 here]

to the project's cabal file.

3. Annotate at least one function to indicate that it should be symbolically executed:

{-# ANN f SymEx #-}
f :: MyInt -> Int -> Int

{-# ANN recCall (SymExWithConfig "--n 10000") #-}
recCall :: Int -> Int

After following these steps, building the project will symbolically execute f and recCall. recCall will be executed according to the command line arguments passed in SymExWithConfig.