Verifying C++ with STL Containers

Verifying general properties of full-featured C++ code is beyond the scope of current model checking and predicate abstraction techniques. However, just as Microsoft´ s SLAM project concentrates on verifying the usage of well-defined APIs in device drivers written in C, the restrictions the C++ Standard makes on the usage of the C++ Standard Template Library (STL) can be verified using a specialized form of counterexample-guided abstraction refinement. We propose a flexible and easily extensible predicate abstraction-based approach to the verification of STL usage.

Our method is to produce an operational model of the behavior guaranteed by the STL standard and apply predicate abstraction to a modified C++ program in which STL calls have been replaced by the operationally equivalent model. The operational model is not an implementation of the Standard Template Library, as it makes use of non-executable features such as infinite arrays - supported by the logic of our model checker, but not realizable in compiled code.

Our front-end to SATABS supports a large subset of the C++ language. We currently lack support for template specialization virtual base classes, and exceptions. We do implement template classes, single inheritance, overloading, and virtual methods.

Technical Report

STL Wrapper

• stl-lib-0.1.tar.gz
  This file contains the STL wrapper for vector and list.

  The model-checker command line may define __STL_PRECISE_VERSIONS to turn on a more precise overapproximation method for keeping track of the validity of the iterators.

  Furthermore, in order to speedup the verification no data is actually stored inside of the containers. If required, __STL_DATA can be defined to enable to the modeling of the containers's data.

Requirements

Examples

Example 1:

   1:
   2:
   3:
   4:
   5:
   6:
   7:
   8:
   9:
  10:
  11:
  12:
  13:

#include <vector>
using namespace std;

int main()
{
  vector<int>::iterator it;
  {
	vector<int> vec;
	vec.push_back(0);
	it = vec.begin();
  }
  *it = 1;
}

In this example, the lifetime of iterator it declared on line 6 is greater that the lifetime of container vec declared on line 8. Then on line 10, it is set to point to the first element of vec. The destructor of vec is automatically called on line 11 and thus, invalidates it. On the next line, it is dereferenced.
After 3 iterations, SATABS finds a concrete couterexample violating an assertion in the header file vector on line 226 which is inside of the body of the * operator.

Command:
satabs -I $STL example1.cpp

Replace $STL with the path to the directory that contains the STL header files.

Outputs:

...
Violated property:
  file /home/blancn/cprover/libs/stl/vector line 226
  dereference failure: temporary object invalidated
  !(it.v == &vec) || __CPROVER_alloc[POINTER_OBJECT(&vec)]

Example 2:

   1:
   2:
   3:
   4:
   5:
   6:
   7:
   8:
   9:
  10:
  11:

#include <vector>
using namespace std;

int main()
{
  vector<int> vec;
  vec.push_back(0);
  vector<int>::iterator it = vec.begin();
  vec.push_back(1);
  int i  = *it;
}

This example illustrates a common mistake of STL usage. On line 8, iterator it is set to point to the first element inside of container vec. Subsequently, a new value is pushed into the vector. On line 10, the iterator is dereferenced.
The insertion of a new value inside of a vector invalidates all the iterators if its content has to be reallocated.
It takes SATABS 5 iterations to find a concrete trace exposing the bug.

Command:
satabs -I $STL example2.cpp

Outputs:

Violated property:
  file example2.cpp line 10
  dereferencing of invalidated iterator
  return_value_version$1 == it.version

Example 3:

   1:
   2:
   3:
   4:
   5:
   6:
   7:
   8:
   9:
  10:
  11:

#include <list>
using namespace std;

int main()
{
  list<int> lst;
  lst.push_back(0);
  list<int>::iterator it = lst.begin();
  lst.push_back(1);
  int i  = *it;
}

This example is the same as previous one except that a list is used instead of a vector. The semantics of a STL list guarantees that all iterators remain valid after an insertion and thus, this code is correct. It takes SATABS seven iterations to verify this program.

Command:
satabs -I $STL example3.cpp

Outputs:

*** CEGAR Loop Iteration 3
Computing Predicate Abstraction for Program
Running Cadence SMV: smv -force -sift
VERIFICATION SUCCESSFUL
Time: 1.805 total, 0.612 abstractor, 0.231 model checker, 0.098 simulator, 0.863 refiner
Iterations: 3
Predicates: 16

Example 4:

   1:
   2:
   3:
   4:
   5:
   6:
   7:
   8:
   9:
  10:
  11:
  12:
  13:
  14:
  15:

#include <vector>
using namespace std;

int main(int argc, char * argv[])
{
  unsigned x;

  vector<int> vec;
  vec.reserve(x);
  vec.push_back(0);
  vector<int>::iterator it = vec.begin();
  vec.push_back(1);
  if(x > 1)
	*it = 1;
}

This example is similar to Example 2 except that the initial capacity of the vector is set dynamically on line 8, since variable x declared on line 6 is not initialized.
If x is greater or equal to two, then the program safely dereferences the iterator on line 14.
Note that in situations where control flow is involed, predicate abstraction is more precise than traditional static analysis. It takes SATABS twelve iterations to verify the correctness of this program.

Command:
satabs -I $STL example4.cpp

Outputs:

*** CEGAR Loop Iteration 12
Computing Predicate Abstraction for Program
Running Cadence SMV: smv -force -sift
VERIFICATION SUCCESSFUL
Time: 15.247 total, 2.745 abstractor, 3.127 model checker, 2.451 simulator, 6.92 refiner
Iterations: 12
Predicates: 34