Solving Constrained Horn Clauses Using shara

Verifying that a given program satisfies a given safety property (i.e., a property that specifies executions that should not happen) can be reduced to solving a class of logic-programming problems called Constrained Horn Clauses (CHCs). CHCs can express safety-verification problems of imperative programs, recursive programs, some concurrent programs, and functional programs.

shara is a CHC solver. It operates purely on CHC systems, and does not require them to correspond to programs in particular languages, or particular safety properties.

Determining satisfiability of a CHC system

For example, consider the following implementation of the Fibonacci function:

int fib(int n) {
  int i = 2;
  int prev = 1;
  int cur = 1;
  while (i < n) {
    cur = prev + cur;
    prev = cur;
    i++; }
  return cur;
}

Proving that fib always returns a non-zero value can be reduced to solving the following CHC system:

i = 2 /\ prev = cur = 1 => R5(prev, cur, i, n)
R5(n, i, prev, cur), i < n => R5(n, i + 1, cur, prev + cur)
R5(n, i, prev, cur), i >= n => cur != 0

where a solution is an interpretation of the relational predicate symbol R5 as a formula over variables n, i, prev, and cur such that each of the entailments given above holds. One such solution interprets R5 as prev > 0 /\ cur > 0.

shara, given such a system, reports that it has a solution.

Determining unsatisfiability of a CHC system

Not every CHC system has a solution. In particular, for program P and property Q such that P does not satisfy Q, any CHC system that corresponds to the problem of verifying that P satisfies Q will not have a solution.

For example, consider the following erroneous implementation of the Fibonacci function:

int buggy_fib(int n) {
  int i = 2;
  int prev = 0;
  int cur = 0;
  while (i < n) {
    cur = prev + cur;
    prev = cur;
    i++; }
  return cur;
}

The corresponding CHC system

i = 2 /\ prev = cur = 0 => R5(prev, cur, i, n)
R5(n, i, prev, cur), i < n => R5(n, i + 1, cur, prev + cur)
R5(n, i, prev, cur), i >= n => cur != 0

has no solution. shara, given such a system, reports that it has no solution.

Building shara

shara is implemented as an alternative version of the z3 automatic theorem prover. To build, run the following commands in package’s main directory SHARA_DIR:

$ python scripts/mk_make.py
$ cd build
$ make

When successful, the build system generates an implementation

Using shara

shara, given a CHC system S in SMT2 format, attempts to determine if S has a solution.

After building shara in directory SHARA_DIR, to determine if a CHC system in file chcs.smt2 has a solution, run the command

$ SHARA_DIR/z3 chcs.smt2

Implementation

shara is implemented as a fork of the z3 automatic theorem prover . It supports an interface identical to that supported by the interface supported by z3 4.5.

The internal behavior of z3 and shara differ only when shara is given a CHC system. The entire implementation of shara is represented by alternative implementations of a solving algorithm used within z3’s solver.

References

shara implements a novel algorithm for solving recursion-free CHCs, which is based on the observation that a novel class of recursion-free CHCs can be solved efficiently. A technical report on the algorithm implemented in shara is publicly available.

Qi Zhou and William Harris. Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions. arxiv