Module cwe_checker_lib::analysis::fixpoint

Creating and computing generic fixpoint computations.

For general information on dataflow analysis using fixpoint algorithms see Wikipedia.

General implementation notes

A fixpoint problem is defined as a graph where:

• Each node n gets assigned a value val(n) where the set of all values forms a partially ordered set.
• Each edge e defines a rule e:value -> value how to compute the value at the end node given the value at the start node of the edge.

A fixpoint is reached if an assignment of values to all nodes of the graph is found so that for all edges e(val(start_node)) <= val(end_node) holds. Usually one wants to find the smallest fixpoint, i.e. a fixpoint such that for each node n the value val(n) is as small as possible (with respect to the partial order) but also not less than a given starting value.

As in the graph module, nodes are assumed to represent points in time, whereas edges represent state transitions or (artificial) information flow channels. In particular, only edges have transition functions and not nodes.

In the current implementation edge transition functions are also allowed to return None to indicate that no information flows through the edge. In such a case the value at the target node of the edge will not get updated. For example, an analysis can use this to indicate edges that are never taken and thus prevent dead code to affect the analysis.

How to compute the solution to a fixpoint problem

To create a fixpoint computation one needs an object implementing the Context trait. This object contains all information necessary to compute fixpoints, like the graph or how to compute transition functions, but not the actual starting values of a fixpoint computation. With it, create a Computation object and then modify the node values through the object to match the intended starting conditions of the fixpoint computation. The Computation object also contains methods to actually run the fixpoint computation after the starting values are set and methods to retrieve the results of the computation.

Structs

• Computation
  The computation struct contains an intermediate result of a fixpoint computation and provides methods for continuing the fixpoint computation or extracting the (intermediate or final) results.

Traits

• Context
  The context of a fixpoint computation.