Repository files navigation

This is thedevelopment site of the LiquidHaskell formal verification tool.

If you're a LiquidHaskelluser (or just curious), you probably want to go tothe documentation website instead.

Assuming theZ3 SMT solver is installed andavailable in yourPATH, you can run

cabal install --lib liquidhaskell liquid-prelude liquid-vector --package-env . --force-reinstallsghc -fplugin=LiquidHaskell FILE.hs

--package-env . creates a.ghc.environment* file in the current folder that makesghc find theLiquidHaskell plugin only when invoking it from there.Otherwise, global user configuration would be affected.

Note that the installation step is influenced by the dependencies that arealready installed in your system, so different results may be obtained bydifferent users.

The github repo only builds with GHC 9.12.2, which must be in yourPATH.

git clone https://github.com/ucsd-progsys/liquidhaskell.gitcd liquidhaskellgit submodule update --initcabal build liquidhaskell liquid-prelude liquid-vectorcabal exec -- ghc -fplugin=LiquidHaskell FILE.hs

If you have questions or you just need help, you can always reach out on ourslack channel,google groups mailing list,GitHub issue tracker, or by emailingRanjit Jhala,Niki Vazou.

This is an open-source project, and we love getting feedback (and patches)!

If something doesn't work as it should, please consider opening agithub issueto let us know. If possible, try to:

• Try to use a descriptive title;
• State as clearly as possible what is the problem you are facing;
• Provide a small Haskell file producing the issue;
• Write down the expected behaviour vs the actual behaviour;
• Please, let us know which liquidhaskell version you are using.

We are thrilled to get PRs! Please follow these guidelines, as doing so will increase the chances ofhaving your PR accepted:

• The main LH repolives here
• Please create pull requests against thedevelop branch.
• Please be sure to include test cases that illustrate the effect of the PR
  • e.g. show new features that that are supported or how it fixes some previous issue
• If you're making user-visible changes, please also add documentation
  • e.g.options.md,specifications.md, themain tutorial (as relevant)

Pull requests don't just have to be about code: documentation can often be improved too!

For those diving into the implementation of LiquidHaskell, here are a few tips:

When changing theliquidhaskell-boot library, sometimes we don't wantto rebuildliquidhaskell orliquid-vector when testing the changes.In these cases we can set the environment variableLIQUID_DEV_MODE=truewhen runningcabal to skip rebuilding those packages.

DANGER: Note that this can give an invalid result if the changes toliquidhaskell-boot do require rebuilding otherliquid* packages.

For documentation on thetest-driver executable itself, please refer to theREADME.md intests/ or runcabal run tests:test-driver -- --help

You can runall the tests by

$ ./scripts/test/test_plugin.sh

You can run a bunch of particular test-groups instead by

$ ./scripts/test/test_plugin.sh <test-group-name1> <test-group-name2> ...

and you can list all the possible test options with

$ ./scripts/test/test_plugin.sh --help

or get a list of just the test groups, one per line, with

$ ./scripts/test/test_plugin.sh --show-all

To pass in specific parameters, you can invoke cabal directly with

$ cabal build tests:<test-group-name> --ghc-options=-fplugin-opt=LiquidHaskell:--no-termination

For example:

$ cabal build tests:unit-neg --ghc-options=-fplugin-opt=LiquidHaskell:--no-termination

Another useful option is to change the underlying solver:

$ cabal build tests:unit-pos --ghc-options=-fplugin-opt=LiquidHaskell:--smtsolver=cvc5

You can also modify the number of used threads, depending on cores etc.

You can directly extend and run the tests by modifying the files in

tests/harness/

Tests run in parallel, unless the flag--measure-timings is specified totest_plugin.sh.

Firstly, make sure to remove previous compilation artifacts of tests before measuring performance,or GHC will skip running Liquid Haskell on modules that don't need recompilation. Unfortunately,using-fforce-recomp is not ideal (see#2565for more details). At the time of writing, previous compilation artifacts of tests can be removed with

find dist-newstyle -name"tests-*" -o -name"prover-ple-lib-*"| xargs rm -r

Whenliquidhaskell tests run, we can collect timing information with

$ ./scripts/test/test_plugin.sh --measure-timings

Measures will be collected in.dump-timings files underdist-newstyle directory. These can beconverted to json data with

cabal v2-build ghc-timingscabal v2-exec ghc-timings dist-newstyle

which will producetmp/*.json files.

Then a csv report can be generated from the json files with

cabal v2-run benchmark-timings -- tmp/*.json --phase LiquidHaskell -o summary.csv

On each line, the report will contain the the wall-clock time taken by each test.Use--phase LiquidHaskellCPU to get the CPU time instead.

Comparison charts insvg format can be generated by invoking

cabal v2-run plot-performance -- -b path_to_before_summary.csv -a path_to_after_summary.csv -s 50

This will generate two filestop.svg andbot.svg containing the top 50 speedups and slowdownsover the entire test set, both enabled by the-s option) in the current directory. Alternatively,a subset of the tests can be selected by a prefix of their names with-f <prefix>, for instance-f benchmarks.-f will generate a filefiltered.svg containing the comparisons of the selected tests.The-f and-s options can be used/omitted independently. If both are omitted, a singleperf.svgwill be produced covering the full input test set. Additionally, their effects can be combined by providing a third-coption (this will produce 2 filesfiltered-top.svg andfiltered-bot.svg instead of 3). An optional key-o can besupplied to specify an output directory for the generated files.

There is also a legacy scriptscripts/plot-performance/chart_perf.sh that can be used to generate comparison chartsin bothsvg andpng formats. It requiresgnuplot to run and assumes both files containthe same test set. The following command will produce two filesperf.svg andperf.png in the current directory.

$ scripts/plot-performance/chart_perf.sh path_to_before_summary.csv path_to_after_summary.csv

The current formatting is optimized for comparing some subsets of the full test run, typically just the benchmarks alone.If one wishes to save time or is not interested in top speedups/slowdowns, the benchmark subset can be obtained by running

$ scripts/test/test_plugin.sh \    benchmark-stitch-lh \    benchmark-bytestring \    benchmark-vector-algorithms \    benchmark-cse230 \    benchmark-esop2013 \    benchmark-icfp15-pos \    benchmark-icfp15-neg

• Profiling See the instructions inscripts/profiling-driver/ProfilingDriver.hs.
• Getting stack traces on exceptions See-xc flag in theGHC user's guide.
• Working with submodules Seeman gitsubmodules or thegit documentation site.

LH supports only one version of GHC at any given time. This is because LH depends heavily on theghc libraryand there is currently no distinction between public API's and API's internal to GHC. There are currently norelease notes for theghc library and breaking changes happen without notice and without deprecationperiods. Supporting only one GHC version saves developer time because it obviates the need for#ifdef'sthroughout the codebase, or for an compatibility layer that becomes increasingly difficult to write as weattempt to support more GHC versions. Porting to newer GHC versions takes less time, the code is easier toread and there is less code duplication.

Users of older versions of GHC can still use older versions of LH.

In order to minimize the effort in porting LH to new releases of GHC, we need a way to abstract over breakingchanges in theghc library, which might change substantially with every major GHC release. This isaccomplished by theGHC.API module. The idea is thatrather than importing multipleghc modules,LH developers must import this single module in order to write future-proof code. This is especiallyimportant for versions of the compiler greater than 9, where the module hierarchy changed substantially,and using theGHC.API makes it easier to support new versions of GHC when they are released.

importPredicateimportTyCoRep...-- This will break if 'isEqPrimPred' is (re)moved or the import hierarchy changes.foo::Type->Boolfoo= isEqPrimPred

importqualifiedLanguage.Haskell.Liquid.GHC.APIasGHC...foo::GHC.Type->Boolfoo=GHC.isEqPrimPred-- OK.

This code commentary describes the current architecture for the GHCPlugin that enables LiquidHaskellto check files as part of the normal compilation process. For the sake of this commentary, we refer tothe code provided as part of therelease/0.8.10.2 branch, commit9a2f8284c5fe5b18ed0410e842acd3329a629a6b.

The moduleGHC.Plugin is the main entrypoint for all the plugin functionalities. Whenever possible, thismodule is reusing common functionalities from theGHC.Interface, which is the original module used tointerface LH with the old executable. Generally speaking, theGHC.Interface module is considered "legacy"and it's rarely what one wants to modify. It will probably be removed at some point.

Broadly speaking, the Plugin is organised this way: In thetypechecking phase, we typecheck and desugareach module via the GHC API in order to extract the unoptimisedcore binds that are needed byLH to work correctly. This is due to a tension in the design space; from one side LH needs access to the"raw" core binds (binds where primitives types are not unboxed in the presence of a PRAGMA annotation,for example) but yet the user can specify any arbitrary optimisation settings during compilation and we donot want to betray the principle of least expectation by silently compiling the code with-O0. Practicallyspeaking, this introduces some overhead and is far from ideal, but for now it allows us to iterate quickly.This phase is also responsible for:

• Extracting the [BareSpec][]s associated to any of the dependent modules;
• Producing theLiftedSpec for the currently-compiled module;
• Storing theLiftedSpec into an interface annotation for later retrieval;
• Checking and verifying the module using LH's existing API.

The reason why we do everything in thetypechecking phase is also to allow integrations with tools likeghcide. There are a number of differences between the plugin and the operations performed as part of theGHC.Interface, which we are going to outline in the next section.

• TheGHC.Interface pre-processes the input files and calls intoconfigureGhcTargets trying tobuild a dependency graph by discovering dependencies the target files might require. Then, from thislist any file in the include directory is filtered out, as well as any module which hasa "fresh".bspec file on disk, to save time during checking. In theGHC.Plugin module thoughwe don't do this and for us, essentially, each input file is considered a target, where we exploit thefact GHC will skip recompilation if unnecessary. This also implies that while theGHC.Interface callsintoprocessTargetModule only for target files, theGHC.Plugin has a single, flat function simplycalledprocessModule that essentially does the same asGHC.Interface.processModule andGHC.Interface.processTargetModule fused together.

• While theGHC.Interface sometimes "assembles" a [BareSpec][] bymappending thecommSpec (i.e. comment spec)with theLiftedSpec fetched from disk, if any, the Plugin doesn't do this but rather piggybacks on theSpecFinder (described later) to fetch dependencies' specs.

• There is a difference in how we process LIQUID pragmas. In particular, for the executable they seems tobe accumulated "in bulk" i.e. if we are refining atarget moduleA that depends onB,B seems toinherit whichever flags we were using in thetarget moduleA. Conversely, the source plugin is "stateless"when it comes to LIQUID options, i.e. it doesn't have memory ofpast options, what it counts when compilinga moduleB is theglobal options andany option this module defines. The analogy is exactly thesame as with GHC language extensions, they have either global scope (i.e.default-extensions in thecabal manifest) or local scope (i.e.{-# LANGUAGE ... #-}).

This is all done by a specialised module called theSpecFinder. The main exported function isfindRelevantSpecs which, given a list ofModules, tries to retrieve theLiftedSpecs associated withthem. Typically this is done by looking into the interface files of the input modules, trying to deserialiseanyLiftedSpec from the interface file's annotations.

Typically the first thing you might want to do is to run a "clean"cabal build usingthe latest compiler and "check the damage". If you are lucky, everything works out of the box, otherwisecompilation might fail with an error, typically because someghc API function has been removed/moved/renamed.The way to fix it is to modify theGHC.API shim module and perform any required change, likely byconditionally compiling some code in aCPP block. For minor changes, it's usually enough to perform smallchanges, but for more tricky migrations it might be necessary to backport some GHC code, or create somepatter synonym to deal with changes in type constructors.

Currently, no. Only one version of GHC is supported and that is the onethat can be tested with./scripts/test/test_plugin.sh.

The following graph summarizes the verification process of a module by showingits specification life cycle.SeeSpecs.hsfor detailed documentation on the specification stages.There are many moving parts hidden within each graph link,but some places worth noticing here areLiquid.hs—which implements constraint generation— andSpecFinder.hs—that deals with the gathering of dependencies andLHAssumptions—.

flowchart LR  subgraph Liquid Haskell    subgraph Inputs      direction TB      LiftedDeps[        Dependencies of A        LifttedSpecs        ]      CoreBinds[CoreBinds]      Bare[BarseSpec]    end    subgraph Outputs      direction TB      T[TargetSpec] --> Constraints[Verification                                    Constraints]      L[LiftedSpec]    end    Inputs --> Outputs  end  A>DepsOfA_LHAssumptions] --> LiftedDeps  Deps>DepsOfA.hi] --> LiftedDeps  Mod(A.hs) --> CoreBinds & Bare  Constraints -->|checked by| fixpoint([liquid-fixpoint])  L ---> |if verified:           serialize| File>A.hi]

Reference:Implementing a GHC Plugin for Liquid Haskell.