Provides classes and predicates implementing a points-to analysis based on Steensgaard’s algorithm, extended to support fields.
A pointer set can be represented in one of two ways: an expression, or the combination of an expression and a label. In the former case, the expression represents the values the expression might evaluate to. In the latter case, the (expr, label) pair is called a “compound”, and it represents a field of the value with the name of the given label. The label can be either a string or another element.
The various “flow” predicates (
flowToCompound, etc.) represent
direct flow from a source set to a destination set. The various “pointer”
pointerFromCompound, etc.) indicate that one set
contains values pointing to the locations represented by the other set.
The individual flow and pointer predicates only hold tuples describing
one step of flow; they do not include transitive closures. The
pointstoinfo predicate determines the transitively implied points-to
information by collapsing pointers into equivalence classes. These
equivalence classes are called “points-to sets”.
The type of agg is s, and the expression initializing the ith member of s is child.
A call to the Unix system function socket(2).
Holds if anything points to an element, that is, is equivalent to:
The points-to set parentset, when dereferenced using the given label, gives values in the points-to set childset.
The same as children(), except that the label is an element.
This relation combines all pointer and flow relations that go to or from a compound set.
The value held in the source flows to the value held in the destination.
There is a flow from the compound (parent, label) to dest.
There is a flow from src to the compound (destParent, destLabel).
Things that are elements of points-to sets.
The ID of the parent set for the given expression. Children of the given element should be looked up with children() and childrenByElement() using this ID.
The source is a pointer to the destination.
The compound (parent, label) holds pointers to dest.
The values stored in src point to the compounds (destParent, destLabel).
A summary of the points-to information for the program, computed by collapsing the various flow and pointer relations using the Java class PointsToCalculator. This relation combines several kinds of information; the different kinds are filtered out by several relations further in the file: pointstosets, setflow, children, childrenByElement, parentSetFor.
Which elements are in which points-to sets.
The points-to set src flows to the points-to set dest. This relation is not transitively closed.
The elements that are either in the given points-to set, or which flow into it from another set. The results are restricted to sets which are interesting.