- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Andersen-style (inclusion-based) points-to analysis. More...
#include <optional>#include <unordered_map>#include <unordered_set>#include <vector>#include <goto-programs/goto_functions.h>#include <irep2/irep2.h>#include <pointer-analysis/value_sets.h>Go to the source code of this file.
Classes | |
| class | andersent |
| struct | andersent::constraintt |
| struct | andersent::indirect_callt |
| A call through a function pointer. More... | |
Andersen-style (inclusion-based) points-to analysis.
A points-to analysis answers the question "which objects can this pointer refer to?". Andersen's analysis computes a single, flow-insensitive, context-insensitive, whole-program answer: for every abstract location it gives one points-to set that is valid at every program point. It ignores statement order (flow insensitivity) and merges all call sites of a function (context insensitivity). That makes it far cheaper than the flow-sensitive value-set analysis, at the price of precision.
It is sound: the real target of any pointer at run time is always contained in the computed set (assuming the constraint frontend models every assignment). It may be imprecise: the set can contain objects a pointer never actually refers to.
Every variable and every allocation site in the program is abstracted to a single node (see andersent::node_id). A heap allocation inside a loop is one node no matter how many concrete objects it creates at run time — that is the source of most of Andersen's imprecision, and it is what keeps the analysis finite and fast.
The result is a map pts : node_id -> set<node_id> where n' in pts[n] means "the pointer abstracted by `n` may hold the address of the object abstracted by `n'`".
Andersen reduces the whole program to a set of set-inclusion (subset) constraints. Every pointer-relevant assignment maps to exactly one of four shapes. Using p, q for pointer variables and &a for the address of object a:
| # | Statement | Constraint | Meaning |
|---|---|---|---|
| 1 | p = &a; | pts[p] ⊇ {a} | address-of |
| 2 | p = q; | pts[p] ⊇ pts[q] | copy |
| 3 | p = *q; | ∀o∈pts[q]. pts[p] ⊇ pts[o] | load |
| 4 | *p = q; | ∀o∈pts[p]. pts[o] ⊇ pts[q] | store |
Constraints 1 and 2 are static: they never change. Constraints 3 and 4 are dynamic: the pairs they relate depend on the points-to sets, which are still being computed — that is why andersent::solve needs a fixpoint (the classic O(n^3) dynamic transitive closure; cycle elimination such as HCD/LCD is deliberately left out).
This analysis is deliberately the coarsest, quickest one: it exists only to authorise safe GOTO rewrites, while symbolic execution provides the real precision. For that role correctness needs exactly one property: the points-to set must be a sound over-approximation — a superset of what a pointer can really hold. Every consumer is built to degrade safely when the set grows: it abstains from the optimisation (k-induction disables the inductive step; GCSE havocs more). Coarseness therefore costs optimisation opportunity, never soundness.
The real risk is the opposite — under-approximation. If the frontend fails to model some way a pointer gets a value (external call, inline asm, int->ptr cast, union type-pun, varargs), an empty set would let a consumer wrongly conclude "nothing to invalidate" and apply an unsafe rewrite.
andersent::TOP closes that hole. It is the reserved node "may point anywhere". Any assignment andersent::collect_constraints cannot classify must route its LHS to TOP (see andersent::points_to_top). The query layer then reports an unnameable (unknown) target, which every consumer already treats as "abstain / be maximally conservative". Model-less code stays sound.
One statement cannot even be routed per object: inline asm, whose operands IREP2 does not keep. It sets andersent::everything_escapes, and every query then answers TOP.
1.15.0