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