Module SimpleRangeAnalysis

Simple range analysis library. Range analysis is usually done as an abstract interpretation over the lattice of range values. (A range is a pair, containing a lower and upper bound for the value.) The problem with this approach is that the lattice is very tall, which means it can take an extremely large number of iterations to find the least fixed point. This example illustrates the problem:

int count = 0;
for (; p; p = p->next) {
  count = count+1;
}

The range of ‘count’ is initially (0,0), then (0,1) on the second iteration, (0,2) on the third iteration, and so on until we eventually reach maxInt.

This library uses a crude solution to the problem described above: if the upper (or lower) bound of an expression might depend recursively on itself then we round it up (down for lower bounds) to one of a fixed set of values, such as 0, 1, 2, 256, and +Inf. This limits the height of the lattice which ensures that the analysis will terminate in a reasonable amount of time. This solution is similar to the abstract interpretation technique known as ‘widening’, but it is less precise because we are unable to inspect the bounds from the previous iteration of the fixed point computation. For example, widening might be able to deduce that the lower bound is -11 but we would approximate it to -16.

QL does not allow us to compute an aggregate over a recursive sub-expression, so we cannot compute the minimum lower bound and maximum upper bound during the recursive phase of the query. Instead, the recursive phase computes a set of lower bounds and a set of upper bounds for each expression. We compute the minimum lower bound and maximum upper bound after the recursion is finished. This is another reason why we need to limit the number of bounds per expression, because they will all be stored until the recursive phase is finished.

The ranges are represented using a pair of floating point numbers. This is simpler than using integers because floating point numbers cannot overflow and wrap. It is also convenient because we can detect overflow and negative overflow by looking for bounds that are outside the range of the type.

Import path

semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis

Imports

RangeSSA

This library is a clone of semmle.code.cpp.controlflow.SSA, with only one difference: extra phi definitions are added after guards. For example:

SimpleRangeAnalysisCached
cpp

Provides classes and predicates for working with C/C++ code.

Predicates

negative_overflow

Holds if the expression might overflow negatively. This predicate does not consider the possibility that the expression might overflow due to a conversion.

nonNanGuardedVariable

Holds if in the branch branch of a guard guard involving v, we know that v is not NaN, and therefore it is safe to make range inferences about v.

positive_overflow

Holds if the expression might overflow positively. This predicate does not consider the possibility that the expression might overflow due to a conversion.