Symbolic Execution of C++ and SystemC with AADD
This page gives a brief introduction into AADD. AADD enables the symbolic execution of C++ and SystemC models. Basis for this is the use of Affine Arithmetic Decision Diagrams, short: AADD. An introduction of the underlying concept can be found here.
What can I do with AADD?
The AADDlib permits the efficient representation and tracing of uncertainties in mixed discrete/continuous computations. Examples are algorithms with real-valued computations and some control flow that depends on the results of the computations. A typical use case is symbolic execution of signal processing methods in C++. As a simple example, the following program can be executed symbolically with AADDlib (example in V2.0):
doubleS a; // Data types with S are computed symbolically.
a = doubleS(0,100); // a takes double value from range [0,100]
ifS(a > 1) // symbolic cond. and iteration statements
a = a + 2;
a = a - 2;
cout << "a is: " << endl;
cout << a;
The result of symbolic execution is a decision diagram that represent all possible results, assuming that a is from the range [0,100]: The condition at the root node is (a>1), and the leaf nodes have the ranges [-2,98] and [2,102], depending on the condition. Ranges are represented and computed by affine forms to yield scalability. Note that by considering the condition, these ranges can be further reduced significantly to [-2,-1] and [3,102]. This is done by GLPK that improves accuracy of the affine forms, while maintaining scalability.
If AADD are used in a simulator such as SystemC (TLM, AMS), this permits symbolic simulation. The result is then a sequence of AADD that represent all possible trajectories of output signals. As AADD are accurate and scale very well for systems that are mostly linear, it is particular well suited for symbolic simulation of analog/mixed-signal (AMS) systems.
Versions and installation
AADD requires some additional software packages that are "open source":
- GLPK with a copy of the GLPK solver that is used in AADD. You need it when using AADD. Support for other solvers is planned in future versions.
- For symbolic simulation, SystemC and SystemC AMS is needed. We use to demonstrate symbolic simulation of mixed-signal systems based on AADD. You don't need it if you want to play with symbolic execution of C++ only.
Version 1.0, Proof of concept implementation
The V1.0 implementation was a proof of concept implementation. It is no longer supported.
Version 2.0, Beta test version
- Re-worked OO design and memory management. The improved OO Design allows us to make type-save definitions of symbolic representations of bool, int, and float/real variables in C++ or SystemC.
- Much simplified support for C++ and SystemC. Just add a "S" after the data type of a variable or branch/iteration you want to be evaluated symbolically.
What still remains unsupported are direct returns out of control flow statements. Currently, only simple control flow statements are supported, but internals already prepare complete C++ support. Furthermore unsupported are symbolic pointer operations - approximation of a pointer by an interval makes no sense.
You can download the AADD library on https://github.com/TUK-CPS/AADD.
Installation is described in the file README; it is based on cmake.