Unique Solver-Based Dataflow Engine
Built into each of our language parsing engines is a revolutionary dataflow analysis component tailored to the value-tracking and related analysis needs of the C and C++ languages. The solution incorporates an industrial-scale Satisfiability Modulo Theories (SMT) solver engine alongside the precise, detailed function structure and semantics produced by our two high-fidelity parsers to yield a full compendium of important dataflow analysis results.
Our dataflow analysis component covers the following important issues in the C and C++ languages:
- Invalid Pointer Operations: dereference and arithmetic operations on a null pointer, computing or dereferencing an invalid pointer value, e.g. buffer under- and overrun, pointer operations on unrelated pointers.
- Dangerous Arithmetic Operations: division by zero, arithmetic operations resulting in overflow or wraparound, converting a negative value to unsigned and other representation issues in conversions, bit-shifting operations that result in truncation or invalid values.
- Flow control anomalies: redundant initializations or assignments, invariant logical operations and flow-control expressions, unreachable code, infinite loops, unset variables, return value mismatches.
- Analysis of standard C library API calls, coupled with pointer alias checking.
On top of this broad scope of dataflow analysis, the dataflow engine performs some intricate modeling of code structures, covering many real-world development complexities:
- Modeling of interdependencies between variables, both for assignments and in determination of conditional expressions (control flow).
- A bi-directional approach, where, for example, later conditional tests can identify earlier suspicious variable usage.
- Accurate representation of loop iterations, including increments by other than ‘1’, multiple loop control variables, and nested loops.
- Handling of bit-fields to exactly correspond to compiler behavior, matching the true size of all types, and yielding intelligence on unions and bit-field operations.
- Binding of function calls (arguments to parameters) within translation-unit calls for precise inter-function data modeling.
Read our Technical Whitepaper on Abstract Interpretations of C Language with Bit-Vector SMT