Wiki

Clone wiki

Boogaloo / User Manual

Overview

Web Interface vs. Installation

The easiest way to try out Boogaloo is through the web interface on comcom. Once you get hooked, get a local version of the tool from Downloads: then you can use your favorite text editor for Boogie source files, run both Boogie and Boogaloo on the same file and get the output from the tool gradually instead of all at once.

The download contains the boogaloo executable and a compatible version of the shared library libz3. Put the library somewhere so that the executable can see it (e.g. same directory, PATH).

Running Boogaloo

In this section we will demonstrate various features of Boogaloo on the Array Maximum program. The best way to follow the manual is to use comcom and try all the examples as you go.

The basics

The most basic Boogaloo invocation is:

boogaloo ArrayMax.bpl

(on comcom this corresponds to an empty parameter string).

The above command will try to find one valid execution of procedure Main and upon its termination display the values of all global entities and parameters of Main that were read or written during the execution. You can specify an alternative entry point through the --proc/-p flag. If the source file contains but a single procedure, it will be used as the entry point regardless of its name.

If you are after faults and are not interested in passing executions, use the test mode:

boogaloo test -p Max ArrayMax.bpl

This will try to find one valid failing execution of the procedure Max. If the tool does not succeed after some default number of tries, it will answer "No executions to display".

In our case testing reveals a failure when the array length is zero: the maximum of an empty array is not defined. We can fix this error by adding a precondition to Max:

requires N > 0;

How it works

To get a better idea of how to control Boogaloo through various command-line parameters, it is useful to understand a little about how it works. When Boogaloo is given a Boogie program it starts systematically enumerating all paths through that program. On some of those paths the interpreter will encounter an assumption violation and deem such executions infeasible (invalid). Along other paths it will reach an error state, resulting in a failing execution. Finally, along the rest of the paths it will follow the program through and end up in a normal state: such executions are considered passing.

Boogaloo is based on symbolic execution, so it doesn't have to enumerate all possible inputs to the program, only all paths through its control-flow graph. This is pretty cool, because if there is only a finite number of paths, Boogaloo can test such a program exhaustively. Unfortunately most programs contain unbounded loops and/or recursion, which makes for an infinite number of paths, and Boogaloo just has to give up at some point.

After reaching the end of the path, Boogaloo asks the constraint solver Z3 to solver the path constraints, i.e. to come up with concrete values that variables could have in this execution. There can be multiple (and even infinitely many) such solutions per path.

In addition Boogaloo has a concrete execution mode, where the path constraints are solved not only at the end of the program, but in some intermediate states as well. This often improves performance because computing with concrete values is faster. There is a danger, however, that if there are more constraints imposed on the symbolic value later in the execution, we will end up brute-forcing their solutions.

Currently Boogaloo can only enumerate paths in (approximately) depth-first order. This is efficient if the first path you follow is likely to be the one you want, as you don't waste time exploring many paths at once. However, the depth-first strategy sometimes gets stuck producing longer and longer paths and never reconsidering a wrong choice it made at the very beginning of the program. This is where the concrete mode also comes in handy: it changes the order of path exploration, sometimes leading to useful paths being found much faster (we will see an example below).

Using command-line options you can control which paths are explored and in what order, how constraints are solved, which executions are displayed and how. We explain the most useful options below. For a full list check out boogaloo --help.

Command-line options

Let's assume we have added the precondition requires N > 0; to Max (see above) and would like to see some executions of this procedure. To specify the number of executions you would like to see, use --out/-o:

boogaloo -p Max -o 3 ArrayMax.bpl

The result looks correct but not very exciting: all the input arrays have length 1. Why did this happen? The reason is that the interpreter first chooses the path (i.e. taking the loop only once) and then picks a solution to the path constraints (i.e. the particular array values); because of the depth-first exploration, the last choice will be reconsidered first, and because there are infinitely many solutions, the interpreter will never get to try another path. To limit the number of solutions considered per path use --per-path/-n:

boogaloo -p Max -o 3 -n 1 ArrayMax.bpl

This didn't do quite what we wanted: now we only get two executions (they correspond to the two branches of the conditional inside the loop). That's because Boogaloo's "concrete" execution mode is on by default: in fact the value of N is chosen before the path, and for each variable we are allowed only one solution. To disable the concrete mode use --concretize=False/-c=0:

boogaloo -p Max -o 3 -n 1 -c=0 ArrayMax.bpl

This seems to work pretty well. However, most of the time we are not interested in passing executions, because our goal is to find bugs. For this purpose Boogaloo lets us filter out the passing executions from the output using --passing=False/-P=0 (which is what boogaloo test basically does):

boogaloo -p Max -P=0 ArrayMax.bpl

You can control the total number of executions considered (including invalid ones) with the --exec/-e parameter. Fora example, the following invocation will only try 100 test cases instead the the default 2048, which won't be enough to find the error (with the default value of -n):

boogaloo -p Max -P=0 -e 100 ArrayMax.bpl

Usually it's good idea to do testing with concretization off. In this particular example, however, depth-first search will get us on a wrong track, considering ever longer loops and never finding the failing test case. You can check this out by running:

boogaloo test -p Max -c=0 -e 100 ArrayMax.bpl

To avoid such unpleasant behavior of depth-first search you can put a bound on the number of loop iterations. One way to do it for a particular loop is to add an assumption to your program, e.g. a precondition N <= 10. A more general way is through the --loop-max/-l parameter:

boogaloo test -p Max -c=0 -e 100 -l 5 ArrayMax.bpl

Limiting loop iterations is also useful for discovering infinite loops. Try commenting out the statement i := i + 1 inside Max and run Boogaloo with default parameters. Instead of running forever, the tool will let you know that you might be executing an infinite loop.

By default Boogaloo tries to minimize the numeric variable values (more precisely, their absolute values), because such executions look more natural to programmers. Usually minimization does not slow the execution down that much (on our examples it has an average overhead of 40%). Some programs, however, don't get along well with minimization. In those cases you can use --minimize=False/-m=0 to disable it:

boogaloo -p Max -m=0 ArrayMax.bpl

For a failing execution Boogaloo only output the values of those variables that it thinks are relevant to the failure, and sometimes this is not enough. You can use the --debug/-d flag to trigger debug output and ask Boogaloo to print pretty much everything it knows:

boogaloo test -p Max -d ArrayMax.bpl

Some of this information is implementation-specific and is there to debug the tool itself, but other stuff (like all global variables and all maps) may be useful for you.

Output directives

Being an intermediate verification language, Boogie does not have any output instructions. That's a shame, cause printing an expression value at a particular program point is the best debugging tool, short of an actual debugger. In Boogaloo you can do that using the print directive.

We implemented our directives as attributes (Boogie mechanism for providing meta-information) on assumptions and assertions. The advantage is that they are automatically ignored by Boogie. The downside is that the syntax is a bit ugly and the printed expressions are not type-checked in advance (the interpreter will throw an exception if it encounters an ill-typed expression in the directive).

To try it out add the following line somewhere in the loop body in Max:

assume {: print "i = ", i} true;

and run Boogaloo with default parameters.

The behavior of print is rather intuitive: you will always see the concrete values and only see those output events that occurred in the current execution (as opposed to all the infeasible executions which were started and then abandoned). The price to pay is that print has to wait until the end of the execution to perform the output, which is not very helpful if you are trying to debug a program that runs too long.

For that reason we introduced another directive called trace, which is similar to print, except it does the output immediately (as mentioned above, you cannot observe this on comcom; in general, comcom does not integrate very well with trace). As a result, some values will be symbolic, some output events might come from (otherwise invisible) infeasible executions, while other events might be shared by several executions which start with the same prefix.

Compiling Boogaloo

Make sure you have GHC and Cabal, which you can get as part of Haskell Platform, together with other Haskell tools. We are currently using GHC 7.6.3, but other recent versions probably work too.

Building Z3

Boogaloo uses Z3 v4.3.1 (currently, the head of the master branch) through a Haskell bindings library z3-haskell. In order to build z3-haskell you will need Z3 include files (z3.h, z3_api.h, z3_macros.h) and the static Z3 library (libz3.a). The most reliable way to obtain the letter is to build Z3 from sources.

Clone or download the source code for Z3 v4.3.1 (let's call the directory where you put it Z3DIR) and follow the instructions on the Z3 codeplex site to build it. Check that Z3DIR/build now contains libz3.a.

Windows: from libz3.a you can create a compatible libz3.dll using dlltool as follows:

cd Z3DIR\build
dlltool -l libz3.a -d ..\src\api\dll\api_dll.def -k -A

Building z3-haskell

Boogaloo uses Scott West 's fork of z3-haskell. Clone/download the source code, then from the top-level directory (where z3.cabal is located) run:

cabal install --extra-include-dirs=Z3DIR/src/api --extra-lib-dirs=Z3DIR/build

Building boogaloo

Clone/download the source code from this repository and from the top-level directory (where language-boogie.cabal is located) run:

cabal install

This will build a Boogaloo executable and store it in the default Cabal binary directory (which should normally already be on your PATH). If you would like to store the executable in another directory, add an option --bindir=another_directory.

Windows: cabal install will fail on Windows due to a magical GHC bug. You should still run it though, because it will install the required libraries. After it fails, run:

ghc -O2 Boogaloo.hs

This will generate Boogaloo.exe in the same directory.

Limitations

The following Boogie constructs are not yet fully supported:

  • Not supported by the parser/type checker:
    • Bit vectors
    • Reals
    • Maps with empty domains
    • Call-forall with a return value
    • Code expressions
  • Functions with a polymorphic result always need an explicit cast around the call: currently the result type cannot be inferred from the context
  • User-defined orders (<:) cannot be executed
  • Incomplete treatment of universal constraints: a constraint of the form forall i, ... :: C(i, ...) is ignored by the interpreter if
    • the bound variable does not appear as an argument of a map or a function: e.g. a constraint forall i: int :: 1 < i && i < x ==> x mod i != 0, which described that x is prime, will be ignored.
    • the bound variable appears in a map/function argument, but as a part of a more complex expression rather that by itself, e.g. forall i: int :: m[i - 1] == m[i + 1] .
    • the scoped formula is an existential, i.e. we do not support AE quantifier alternation. EA is okay though, so, for example, you can define that C is a constant function by saying axiom (exists c: int :: (forall x: int :: C(x) == c));

Older versions

User Manual v0.2 (February 2013)

Updated