Skip to content

verifast/verifast

master
Switch branches/tags
Code

Latest commit

This breaking change (probably the biggest breaking change in the
history of VeriFast) is necessary to make VeriFast sound with respect to
the fact that C compilers perform optimizations that assume that the
program does not read uninitialized memory. (See e.g.
<https://www.ralfj.de/blog/2019/07/14/uninit.html> and
<https://godbolt.org/z/dYq1Gc9G4>.)

This commit introduces, for each points-to predicate with parameter
types T* and T (representing an initialized object of type T), a
corresponding "underscore predicate" with parameter types T* and
option<T> (representing a possibly-uninitialized object of type T):

The points-to predicates and corresponding underscore predicates are:

boolean -> bool_
character -> char_
u_character -> uchar_
short_integer -> short_
u_short_integer -> ushort_
integer -> int_
u_integer -> uint_
llong_integer -> llong_
u_llong_integer -> ullong_
integer_ -> integer__ (generic integer type points-to predicate)
pointer -> pointer_
float_ -> float__
double_ -> double__
long_double -> long_double_

Similarly, for each array predicate with parameter types T*, int, and
list<T>, it introduces a corresponding underscore predicate with
parameter types T*, int, and list<option<T> >:

bools -> bools_
chars -> chars_
uchars -> uchars_
shorts -> shorts_
ushorts -> ushorts_
ints -> ints_
uints -> uints_
llongs -> llongs_
ullongs -> ullongs_
integers_ -> integers__ (generic integer array predicate)
pointers -> pointers_
floats -> floats_
doubles -> doubles_
long_doubles -> long_doubles_

Writing consumes an underscore chunk and produces an initialized chunk;
reading requires an initialized chunk. Allocation produces an underscore
chunk and deallocation consumes an underscore chunk.

The syntaxes *p |-> _ and p[..N] |-> _ are now interpreted as denoting
an underscore chunk.

TODO:
- Produce/consume underscore chunk on allocation/deallocation of
  primitive-typed objects.
- Struct field underscore predicates
- Update the VeriFast Tutorial
- Improve soundness regarding struct padding
- Make VeriFast sound with respect to pointer provenance and effective
  types
7fa8116

Git stats

Files

Permalink
Failed to load latest commit information.

CI Build status DOI

VeriFast

By Bart Jacobs*, Jan Smans*, and Frank Piessens*, with contributions by Pieter Agten*, Cedric Cuypers*, Lieven Desmet*, Jan Tobias Muehlberg*, Willem Penninckx*, Pieter Philippaerts*, Amin Timany*, Thomas Van Eyck*, Gijs Vanspauwen*, Frédéric Vogels*, and external contributors

* imec-DistriNet research group, Department of Computer Science, KU Leuven - University of Leuven, Belgium

VeriFast is a research prototype of a tool for modular formal verification of correctness properties of single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic. To express rich specifications, the programmer can define inductive datatypes, primitive recursive pure functions over these datatypes, and abstract separation logic predicates. To verify these rich specifications, the programmer can write lemma functions, i.e., functions that serve only as proofs that their precondition implies their postcondition. The verifier checks that lemma functions terminate and do not have side-effects. Since neither VeriFast itself nor the underlying SMT solver need to do any significant search, verification time is predictable and low.

The VeriFast source code and binaries are released under the MIT license.

Binaries

Within an hour after each push to the master branch, binary packages become available here.

These "nightly" builds are very stable and are recommended. Still, named releases are available here. (An archive of older named releases is here.)

Simply extract the files from the archive to any location in your filesystem. All files in the archive are in a directory named verifast-COMMIT where COMMIT describes the Git commit. For example, on Linux:

tar xzf ~/Downloads/verifast-nightly.tar.gz
cd verifast-<TAB>  # Press Tab to autocomplete
bin/vfide examples/java/termination/Stack.jarsrc  # Launch the VeriFast IDE with the specified example
./test.sh  # Run the test suite (verifies all examples)

Note (macOS): To avoid GateKeeper issues, before opening the downloaded archive, remove the com.apple.quarantine attribute by running

sudo xattr -d com.apple.quarantine ~/Downloads/verifast-nightly-osx.tar.gz

Compiling

Documentation

Acknowledgements

Dependencies

We gratefully acknowledge the authors and contributors of the following software packages.

Bits that we ship in our binary packages

  • OCaml
  • OCaml-Num
  • Lablgtk
  • GTK+ and its dependencies (including GLib, Cairo, Pango, ATK, gdk-pixbuf, gettext, fontconfig, freetype, expat, libpng, zlib, Harfbuzz, and Graphite)
  • GtkSourceView
  • The excellent Z3 theorem prover by Leonardo de Moura and Nikolaj Bjorner at Microsoft Research, and co-authors

Software used at build time

  • findlib, ocamlbuild, camlp4, valac
  • Cygwin, Homebrew, Debian, Ubuntu
  • The usual infrastructure: GNU/Linux, GNU make, gcc, etc.

Infrastructure

We gratefully acknowledge the following infrastructure providers.

  • GitHub
  • Travis CI
  • AppVeyor CI

Funding

This work is supported in part by the Flemish Research Fund (FWO-Vlaanderen), by the EU FP7 projects SecureChange, STANCE, ADVENT, and VESSEDIA, by Microsoft Research Cambridge as part of the Verified Software Initiative, and by the Research Fund KU Leuven.

Mailing lists

To be notified whenever commits are pushed to this repository, join the verifast-commits Google Groups forum.

Third-Party Resources