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”.
WARNING: This library may perform poorly on very large projects.
Consider using another library such as semmle.code.cpp.dataflow.DataFlow
instead.
Import path
import 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: |
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 |
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 | The values stored in src point to the compounds (destParent, destLabel). |
pointerValue | Holds if |
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 |
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 |