Module PointsTo

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 (flow, flowToCompound, etc.) represent direct flow from a source set to a destination set. The various “pointer” predicates (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”.

Import path

semmle.code.cpp.pointsto.PointsTo

Imports

Predicates

aggregateLiteralChild

The type of agg is s, and the expression initializing the ith member of s is child.

allocateDescriptorCall

A call to the Unix system function socket(2).

anythingPointsTo

Holds if anything points to an element, that is, is equivalent to: exists(PointsToExpr e | e.pointsTo() = elem)

children

The points-to set parentset, when dereferenced using the given label, gives values in the points-to set childset.

childrenByElement

The same as children(), except that the label is an element.

compoundEdge

This relation combines all pointer and flow relations that go to or from a compound set.

flow

The value held in the source flows to the value held in the destination.

flowFromCompound

There is a flow from the compound (parent, label) to dest.

flowToCompound

There is a flow from src to the compound (destParent, destLabel).

location

Things that are elements of points-to sets.

lvalue

Holds if e is evaluated just for its location. This includes expressions that are used in a reference expression (&foo), expressions that are used on the left side of an assignment, and some non-expression types such as Initializer.

parentSetFor

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.

pointer

The source is a pointer to the destination.

pointerFromCompound

The compound (parent, label) holds pointers to dest.

pointerToCompound
pointerValue

Holds if e has a pointer type.

pointstoinfo

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.

pointstosets

Which elements are in which points-to sets.

resolve

Holds if actual is the override of resolved for a value of type dynamic.

setflow

The points-to set src flows to the points-to set dest. This relation is not transitively closed.

setlocations

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.

varArgRead
virtualArg
virtualRet
virtualThis

Classes