applications.tex

\chapter{Experiences and applications}

We have successfully used \texttt{z3.rkt} in a number of applications, from
constraint-solving puzzles as illustrated in Section~\ref{sec:interactive}, to
verification and counterexample generation for functional programs. Along the
way, we have been pleasantly surprised by how well the power of Z3 and the
expressiveness of Racket combine. In this chapter we discuss the lessons we
have learnt and a few ideas we have explored.

\section{Handling quantified formulas}
\label{sec:quantified}

Z3 and other SMT solvers support lists and other recursive types. Z3 provides
only basic support for lists: \texttt{insert} (cons), \texttt{head}, and
\texttt{tail}. Further, Z3's macros are substitutions and do not support
recursion. This makes it challenging to define functions that operate over the
entirety of an arbitrary-length list.

Our first thought was to use a universal quantifier, as in
Section~\ref{sec:derived}. \Fref{fig:len-quantified} lists an example of a
function that calculates the length of an integer list.

\begin{program}
\caption{Calculating the length of a list with a quantified formula}
\label{fig:len-quantified}
\begin{minted}{scheme}
(declare-fun len ((List Int)) Int)
(assert (forall ((xs (List Int)))
  (ite (= xs nil)
       (= (len xs) 0)
       (= (len xs) (+ 1 (len (tail xs)))))))
\end{minted}
\end{program}

There is a drawback with this approach: solving quantified assertions in Z3
requires model-based quantifier instantiation (MBQI)~\cite{mbqi}. MBQI, while
powerful, can also be very slow. In our experience, it is very easy to write a
quantified formula that Z3's MBQI engine fails to solve in reasonable
time\footnote{In general, it is hard to deal with quantified formulas
containing even linear arithmetic, because there is no sound and complete
decision procedure for them~\cite{halpern91}.

Z3 has another way to solve quantified assertions, called
\textit{E-matching}~\cite{e-matching}. E-matching uses patterns based on
ground terms to instantiate quantifiers. We have not yet explored this
approach.}.

So avoiding quantified formulas altogether seems like a good idea, but how do
we do that? The easiest way is to unroll and bound the recursion to a desired
depth~\cite{sat-recursive}. One way to do this is to define macros
\texttt{len-0}, \texttt{len-1}, \texttt{len-2}, \ldots \texttt{len-N}, where
each \texttt{len-k} returns the length of the list if it is less than or equal
to \texttt{k}, and \texttt{k} otherwise (\Fref{fig:len-macros}).

\begin{program}
\caption{A series of SMT-LIB macros to calculate the length of a list}
\label{fig:len-macros}
\begin{minted}{scheme}
(define-fun len-0 ((xs (List Int)))
  0)

(define-fun len-1 ((xs (List Int)))
  (ite (= xs nil)
       0
       (+ 1 (len-0 (tail xs)))))

(define-fun len-2 ((xs (List Int)))
  (ite (= xs nil)
       0
       (+ 1 (len-1 (tail xs)))))
...
\end{minted}
\end{program}

Our system makes defining a series of macros like this very easy, as shown in
\Fref{fig:len-rkt}.

\begin{program}
\caption{\texttt{z3.rkt} code to generate a bounded recursive function to calculate the length of a list}
\label{fig:len-rkt}
\begin{minted}{scheme}
(define (make-length n)
  (smt:define-fun len ((xs (List Int))) Int
    (if (zero? n)
        0         ; len-0 always returns 0
        (ite/s (=/s xs nil/s)
               0
               (let ([sublen (make-length (sub1 n))])
                 (+/s 1 (sublen (tail/s xs)))))))
  len)
\end{minted}
\end{program}

\texttt{(make-length 5)} returns an SMT function that works for lists of up to
length 5, and returns 5 for anything bigger than that. Note how freely the
Racket \texttt{if} and \texttt{let} forms are mixed into the SMT body. These
constructs are evaluated at definition time, meaning that this definition
reduces to the series of macros defined above up to length \texttt{n}.

It is easy to define other bounded recursive functions along the same lines
that reverse lists, concatenate them, filter them on a predicate and much
more. For example, \Fref{fig:reverse-rkt} defines a function that creates
bounded recursive functions that reverse a list (using an accumulator).

\begin{program}
\caption{A bounded recursive function to reverse lists up to length \texttt{n}}
\label{fig:reverse-rkt}
\begin{minted}{scheme}
(define (make-reverse n)
  ; We're using an accumulator so create an internal function
  (define (make-reverse-internal n)
    (smt:define-fun reversen ((xs (List Int)) (accum (List Int)))
                             (List Int)
      (if (zero? n)
          accum     ; reverse-0 always returns the accumulated list

          ; Recursive step: generate function for n-1
          (let ([subreverse (make-reverse-internal (sub1 n))])
            (ite/s (=/s xs nil/s)
                   accum
                   (subreverse (tail/s xs) (insert/s (head/s xs)
                                                     accum))))))
    reversen)

  (define reverse (make-reverse-internal n))
  (lambda (xs) (reverse xs nil/s)))
\end{minted}
\end{program}

Using these building blocks we can now verify properties of recursive
functions.

\section{Verifying recursive functions}

For this section we will work with a simple but non-trivial
example:~\textit{quicksort}. A simple functional implementation of quicksort
might look like \Fref{fig:qsort}.

\begin{program}
\caption{A functional quicksort implementation}
\label{fig:qsort}
\begin{minted}{scheme}
(define (qsort lst)
  (if (null? lst)
      null
      (let*
       ([pivot (car lst)]
        [rest (cdr lst)]
        [left (qsort (filter (lambda (x) (<= x pivot)) rest))]
        [right (qsort (filter (lambda (x) (> x pivot)) rest))])
        (append left (cons pivot right)))))
\end{minted}
\end{program}

This definition is correct, but what if the programmer mistakenly types in
\texttt{<} instead of \texttt{<=}, or perhaps uses \texttt{>=} instead of
\texttt{>}? We note that (a) for a correct implementation, the length of the
output will always be the same as that of the input, and that (b) in either
buggy case, the length of the output will be different whenever a pivot is
repeated in the rest of the list. So comparing the two lengths is a good
property to verify.

Using the method discussed in Section~\ref{sec:quantified}, we can write
\texttt{make-qsort} that generates bounded recursive versions of
\texttt{qsort}. We believe that both automatic and manual methods would be
feasible (\Fref{fig:qsort-smt} is a manual translation).

\begin{program}

\caption[A bounded recursive version of quicksort]{A bounded recursive version
of quicksort (cf \Fref{fig:qsort}). \texttt{make-le} and \texttt{make-gt}
create functions to filter lists based on their relation to \texttt{pivot},
respectively \texttt{<=} and \texttt{>}. \texttt{make-append} creates
functions to append lists}

\label{fig:qsort-smt}
\begin{minted}{scheme}
(define (make-qsort n lessop-fn greaterop-fn)
  (smt:define-fun qsort ((xs (List Int))) (List Int)
    (if (zero? n)
        nil/s

        ; From here on is the usual definition of quicksort.
        (ite/s (=/s xs nil/s)
               nil/s

               (let*
                ([subqsort (make-qsort (sub1 n))]
                 [pivot (head/s xs)]
                 [rest (tail/s xs)]
                 [left
                  (subqsort ((make-le (sub1 n)) pivot rest))]
                 [right
                  (subqsort ((make-gt (sub1 n)) pivot rest))])

                 ((make-append (sub1 n)) left
                                         (insert/s pivot right))))))
  qsort)
\end{minted}
\end{program}

With \texttt{make-qsort} we can now verify the length property for all input
lists up to a certain length \texttt{n}.

\begin{program}
\caption{Verifying length for quicksort}
\begin{minted}{scheme}
(smt:with-context
 (smt:new-context)
 (define qsort (make-qsort n))
 ; adding 1 to the maximum length is enough to show inequality
 (define len (make-length (add1 n)))
 (smt:declare-fun xs () (List Int))
 ; set a bound on the length
 (smt:assert (<=/s (len xs) n))
 ; prove the length property by asserting its negation
 (smt:assert (not/s (=/s (len xs) (len (qsort xs)))))
 (smt:check-sat))
\end{minted}
\end{program}

Proving a property is done by checking that its negation is unsatisfiable. A
quicksort works \textit{correctly}\footnote{Here correctness is in the context
of the property we are considering, i.e. the length of the output.} for lists
up to length \texttt{n} iff the above code returns \texttt{'unsat}. For
quicksorts that are buggy (\texttt{'sat}), we can find a counterexample using
\texttt{(smt:eval xs)} and \texttt{(smt:eval (qsort xs))}. For $\mathtt{n}=4$
on a buggy quicksort with filters \texttt{<=} and \texttt{>=}, Z3 returned us
the counterexample with input \texttt{'(-3 -2 -1 -2)}, which as expected
contains a repeated element.

\subsection*{Summary}

In this chapter, we discussed our experiences using our interface for advanced
applications. We described methods to overcome fundamental SMT limitations,
and successfully verified or found bugs in non-trivial functional programs
with the help of these methods.

In our approach, there is nothing specific to quicksort: this can easily be
generalised to other functions that operate on lists and other data
structures. The properties to prove can be more complex, such as whether a
given sorting algorithm is stable. The only limits are computational
constraints and the user's imagination.