SATABS – Predicate Abstraction with SAT

Overview

We describe SATABS from the point of view of the user. To learn about the technology implemented in SATABS, read this.

We assume you have already installed SATABS and the necessary support files on your system. If not so, please follow these instructions.

While users of SATABS almost never have to be concerned about the underlying refinement abstraction algorithms, understanding the classes of properties that can be verified is crucial. Predicate abstraction is most effective when applied to control-flow dominated properties. As an example, reconsider the following program (lock-example-fixed.c):

_Bool nondet_bool();
_Bool LOCK = 0;

_Bool lock() {
  if(nondet_bool()) {
    assert(!LOCK);
    LOCK=1;
    return 1; }

  return 0;
}

void unlock() {
  assert(LOCK);
  LOCK=0;
}

int main() {
  unsigned got_lock = 0;
  int times;

  while(times > 0) {
    if(lock()) {
      got_lock++;
      /* critical section */
    }

    if(got_lock!=0) {
      unlock();
      got_lock--;
    }

    times--;
} }

The two assertions in the program model that the functions lock() and unlock() are called in the right order. Note that the value of times is chosen non-deterministically and is not bounded. The program has no run-time bound, and thus, unwinding the code with CBMC will never terminate.

Working with Claims

The two assertions will give rise to two properties. Each property is associated to a specific line of code, i.e., a property is violated when some condition can become false at the corresponding program location. SATABS will generate a list of all properties for the programs as follows:

satabs lock-example-fixed.c --show-properties

SATABS will list two properties; each property corresponds to one of the two assertions. We can use SATABS to verify both properties as follows:

satabs lock-example-fixed.c

SATABS will conclude the verification successfully, that is, both assertions hold for execution traces of any length.

By default, SATABS attempts to verify all properties at once. A single property can be verified (or refuted) by using the --property id option of SATABS, where id denotes the identifier of the property in the list obtained by calling SATABS with the --show-properties flag. Whenever a property is violated, SATABS reports a feasible path that leads to a state in which the condition that corresponds to the violated property evaluates to false.

Programs that use Libraries

SATABS cannot check programs that use functions that are only available in binary (compiled) form (this restriction is not imposed by the verification algorithms that are used by SATABS – they also work on assembly code). The reason is simply that so far no assembly language frontend is available for SATABS. At the moment, (library) functions for which no C source code is available have to be replaced by stubs. The usage of stubs and harnesses (as known from unit testing) also allows to check more complicated properties (like, for example, whether function fopen is always called before fclose). This technique is explained in detail in the SATABS tutorials.

Unit Testing with SATABS

The example presented here is obviously a toy example and can hardly be used to convince your project manager to use static verification in your next project. Even though we recommend to use formal verification and specification already in the early phases of your project, the sad truth is that in most projects verification (of any kind) is still pushed to the very end of the development cycle. Therefore, this section is dedicated to the verification of legacy code. However, the techniques presented here can also be used for unit testing.

Unit testing is used in most software development projects, and static verification with SATABS can be very well combined with this technique. Unit testing relies on a number test cases that yield the desired code coverage. Such test cases are implemented by a software testing engineer in terms of a test harness (aka test driver) and a set of function stubs. Typically, a slight modification to the test harness allows it to be used with SATABS. Replacing the explicit input values with non-deterministic inputs (as explained in here and here) guarantees that SATABS will try to achieve full path and state coverage (due to the fact that predicate abstraction implicitly detects equivalence classes). However, it is not guaranteed that SATABS terminates in all cases. Keep in mind that you must not make any assumptions about the validity of the properties if SATABS did not run to completion!