liquid-fixpoint: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain]

This package is a Haskell wrapper to the SMTLIB-based Horn-Clause/Logical Implication constraint solver used for Liquid Types.

The package includes:

  1. Types for Expressions, Predicates, Constraints, Solutions

  2. Code for solving constraints

Requirements

In addition to the .cabal dependencies you require


[Skip to ReadMe]

Properties

Versions0.1.0.0, 0.2.0.0, 0.2.1.0, 0.2.1.1, 0.2.2.0, 0.2.3.0, 0.2.3.1, 0.2.3.2, 0.3.0.0, 0.3.0.1, 0.4.0.0, 0.5.0.0, 0.5.0.1, 0.6.0.1, 0.6.0.2, 0.7.0.1, 0.7.0.2, 0.7.0.3, 0.7.0.5, 0.7.0.6, 0.7.0.7
Change logCHANGES.md
Dependenciesansi-terminal, array, ascii-progress (>=0.3), async, attoparsec, base (>=4.8.1.0 && <5), bifunctors, binary, boxes, bytestring, cereal, cmdargs, containers, deepseq, directory, dotgen, fgl, fgl-visualize, filemanip, filepath, ghc-prim, hashable, intern, liquid-fixpoint, located-base, mtl, parallel, parallel-io, parsec, pretty, process, syb, text, text-format, time, transformers, unordered-containers [details]
LicenseBSD-3-Clause
Copyright2010-17 Ranjit Jhala, University of California, San Diego.
AuthorRanjit Jhala, Niki Vazou, Eric Seidel
Maintainerjhala@cs.ucsd.edu
CategoryLanguage
Home pagehttps://github.com/ucsd-progsys/liquid-fixpoint
Source repositoryhead: git clone https://github.com/ucsd-progsys/liquid-fixpoint/
Executablesfixpoint
UploadedMon May 15 15:25:36 UTC 2017 by niki

Modules

Flags

NameDescriptionDefaultType
devel

turn on stricter error reporting for development

DisabledManual

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainers' corner

For package maintainers and hackage trustees


Readme for liquid-fixpoint-0.6.0.2

[back to package description]

Liquid Fixpoint Hackage Hackage-Deps Build Status

This package implements a Horn-Clause/Logical Implication constraint solver used for various Liquid Types. The solver uses SMTLIB2 to implement an algorithm similar to:

Requirements

In addition to the .cabal dependencies you require an SMTLIB2 compatible solver binary:

If on Windows, please make sure to place the binary and any associated DLLs somewhere in your path.

How To Build and Install

Simply do:

git clone https://github.com/ucsd-progsys/liquid-fixpoint.git
cd liquid-fixpoint
stack install

or (cabal instead of stack if you prefer.)

Using SMTLIB-based SMT Solvers

You can use one of several SMTLIB2 compliant solvers, by:

fixpoint --smtsolver=z3 path/to/file.hs

Currently, we support

* Z3
* CVC4
* MathSat

Configuration Management

It is very important that the version of Liquid Fixpoint be maintained properly.

Suppose that the current version of Liquid Haskell is A.B.C.D:

It is recommended to use the Bumper utility to manage the versioning of Liquid Fixpoint. Bumper will automatically do the correct update to the cabal file. Additionally, it will update any packages that you have the source for that depend on Liquid Fixpoint.

To update Liquid Fixpoint and Liquid Haskell, first clone Liquid Haskell and Liquid Fixpoint to a common location:

git clone https://github.com/ucsd-progsys/liquidhaskell.git
git clone https://github.com/ucsd-progsys/liquid-fixpoint.git

To increment the D component of Liquid Fixpoint:

./path/to/bumper -3 liquid-fixpoint

This will update the D component of Liquid Fixpoint. If necessary, this will update the Build-Depends of Liquid Haskell. If the Build-Depends was updated, Liquid Haskell's D component will be incremented.

To increment the C component of Liquid Fixpoint, and strip the D component:

./path/to/bumper --minor liquid-fixpoint

As before, this will update Liquid Fixpoint and, if necessary, Liquid Haskell.

To increment the B component of Liquid Fixpoint, and strip the D and C components:

./path/to/bumper --major liquid-fixpoint

As before, this will update Liquid Fixpoint and, if necessary, Liquid Haskell

SMTLIB2 Interface

There is a new SMTLIB2 interface directly from Haskell:

See tests/smt2/{Smt.hs, foo.smt2} for an example of how to use it.

Options

--higherorder allows higher order binders into the environment

--extsolver runs the deprecated external solver.

--parts Partitions an FInfo into a [FInfo] and emits a bunch of files. So:

$ fixpoint -n -p path/to/foo.fq

will now emit files:

path/to/.liquid/foo.1.fq
path/to/.liquid/foo.2.fq
. . .
path/to/.liquid/foo.k.fq

and also a dot file with the constraint dependency graph:

path/to/.liquid/foo.fq.dot

FInfo Invariants

Binders

This is the field

     , bs       :: !BindEnv         -- ^ Bind  |-> (Symbol, SortedReft)

or in the .fq files as

bind 1 x : ...
bind 2 y : ...

Environments

  bind 1 x : ...
  bind 12 x : ...

Then a single IBindEnv should only mention at most one of 1 or 12.

LHS

Each slhs of a constraint is a SortedReft.

     $k1[x1:=y1][x2:=y2]...[xn:=yn]

That is represented in the Expr type as

  | PKVar  !KVar !Subst

must appear only at the top-level that is not under any other operators, i.e. not as a sub-Expr of other expressions.

    x:int, y:int |- x + y : int

is well sorted. but

    x:int  |- x + y : int

is not, and

    x:int, y: list |- x + y : int

is not. The exact definition is formalized in Language.Fixpoint.SortCheck

RHS

Similarly each rhs of a SubC must either be a single $k[...] or an plain $k-free Expr.

Global vs. Distinct Literals

     , gLits    :: !(SEnv Sort)               -- ^ Global Constant symbols
     , dLits    :: !(SEnv Sort)       

The global literals gLits are symbols that are in scope everywhere i.e. need not be separately defined in individual environments. These include things like

Suppose you have an enumerated type like:

data Day = Sun | Mon | Tue | Wed | ... | Sat

You can model the above values in fixpoint as:

constant lit#Sun : Day
constant lit#Mon : Day
constant lit#Tue : Day
constant lit#Wed : Day

The distinct literals are a subset of the above where we want to tell the SMT solver that the values are distinct i.e. not equal to each other, for example, you can additionally specify this as:

distinct lit#Sun : Day
distinct lit#Mon : Day
distinct lit#Tue : Day
distinct lit#Wed : Day

The above two are represented programmatically by generating
suitable Symbol values (for the literals see litSymbol) and Sort values as FTC FTycon and then making an SEnv from the [(Symbol, Sort)].

Sorts

What's the difference between an FTC and an FObj?

In early versions of fixpoint, there was support for three sorts for expressions (Expr) that were sent to the SMT solver:

  1. int
  2. bool
  3. "other"

The FObj sort was introduced to represent essentially all non-int and non-bool values (e.g. tuples, lists, trees, pointers...)

However, we later realized that it is valuable to keep more precise information for Exprs and so we introduced the FTC (fixpoint type constructor), which lets us represent the above respectively as:

There is a comment that says FObj's are uninterpretted types; so probably a type the SMT solver doesn't know about? Does that then make FTC types that the SMT solver does know about (bools, ints, lists, sets, etc.)?

The SMT solver knows about bool, int and set (also bitvector and map) but all other types are currently represented as plain Int inside the SMT solver. However, we will be changing this to make use of SMT support for ADTs ...

To sum up: the FObj is there for historical reasons; it has been subsumed by FTC which is what I recomend you use. However FObj is there if you want a simple "unitype" / "any" type for terms that are not "interpreted".