 |
Verifying C++ with STL Containers via Predicate Abstraction
|
|
|
|
|
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
Verifying C++ with STL Containers
via Predicate Abstraction
|
|
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
Either SATABS or
CBMC .
|
|
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
|
|
|