Thomas Wies |
Damien Zufferey |
Siddharth Krishna |
Ruzica Piskac |
GRASShopper is an experimental verification tool for programs that manipulate dynamically allocated data structures. GRASShopper programs can be annotated with specifications expressed in a decidable specification logic to check functional correctness properties. The logic supports mixing of separation logic and first-order logic assertions, yielding expressive yet concise specifications.
The input language of GRASShopper is a simple procedural imperative language that supports user-defined struct types and arrays. The specification logic supports data types such as mathematical sets and maps as well as user-defined algebraic data types, predicates, and functions.
The following GRASShopper program declares a procedure
concat
that concatenates two singly-linked lists:
/* A node in a singly-linked list. */
struct Node {
var next: Node;
}
/* Predicate denoting an acyclic singly-linked list starting from 'x'. */
predicate list(x: Node) {
acc({ z: Node :: Btwn(next, x, z, null) && z != null }) &*&
Reach(next, x, null)
}
/* Concatenate two lists 'a' and 'b'.
* The result is a single list 'res'. */
procedure concat(a: Node, b: Node)
returns (res: Node)
requires list(a) &*& list(b)
ensures list(res)
{
if (a == null) {
return b;
} else {
var curr := a;
while (curr.next != null)
invariant acc(curr) **- list(a)
{
curr := curr.next;
}
curr.next := b;
return a;
}
}
Given an input program, GRASShopper checks that:
The tool provides an Emacs mode with syntax highlighting and on-the-fly checking of GRASShopper programs. Errors in the program or its specification are automatically highlighted. There is also rudimentary support for the visualization of counterexample traces.
Unlike other verification tools based on separation logic, GRASShopper does not implement a dedicated theorem prover for separation logic. Neither does it rely on user-guided proof search. Instead, the tool reduces proof obligations in separation logic to a decidable fragment of first-order logic, which we refer to as the Logic of Graph Reachability with Stratified Sets (GRASS). Reasoning in this logic is automated using conventional Satisfiability Modulo Theories solvers. This approach enables a robust combination of separation logic with other decidable first-order theories that are important in program verification. For example, GRASShopper can verify properties about data stored in heap-allocated structures (such as sortedness properties) even though there is no dedicated inbuilt support for this in the tool.
GRASShopper is implemented in OCaml and distributed under a BSD license. We have tested the tool on Linux, Mac OS, and Windows/Cygwin.
For download and installation instructions please visit the tool's GitHub repository.
This material is based in part upon work supported by the National Science Foundation under grants 1320583, 1618059 and 1815633. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.