#include <andersen.h>

Inheritance diagram for andersent:

Classes
struct	constraintt
struct	indirect_callt
	A call through a function pointer. More...

Public Types
enum class	constraint_kindt { ADDRESS_OF , COPY , LOAD , STORE }
	The four inclusion-constraint shapes of The four constraint kinds. More...
typedef unsigned	node_id
	A node is an abstract memory location: one program variable or one allocation site.
Public Types inherited from value_setst
typedef std::list< expr2tc >	valuest
typedef goto_programt::const_targett	locationt

Public Member Functions
	andersent ()
Core solver
Operates purely on node ids, so it is exercised by the unit tests from synthetic constraints without needing a GOTO program.
node_id	get_node (const expr2tc &e)
	Interns `e` as a node, returning a stable id (creates one on first use).
void	add_constraint (constraint_kindt kind, node_id lhs, node_id rhs)
	Registers one constraint. Cheap; the real work happens in solve.
void	points_to_top (node_id n)
	Marks `n` as possibly pointing anywhere by adding TOP to its set.
void	solve ()
	Computes the least fixpoint of all registered constraints, populating pts.
const std::unordered_set< node_id > &	points_to (node_id n) const
	The points-to set of `n` after solve (empty if never grown).
bool	may_point_to (node_id a, node_id b) const
	True iff `a` may point to `b` (i.e. b ∈ pts[a]).
GOTO frontend
void	collect_constraints (const goto_functionst &goto_functions)
	Walks every function body and lowers pointer-relevant assignments, returns and calls to constraints via add_constraint.
Query / transparency layer
Lets whole-program consumers (GCSE, the k-induction pointer-write resolver) use Andersen wherever they used the value-set analysis. Because the analysis is flow-insensitive, the location argument `l` is accepted for API compatibility and ignored. Queries are offset-insensitive: p + i reaches what p does.
void	operator() (const goto_functionst &goto_functions)
	Runs the whole analysis: collect_constraints, then solve and resolve_indirect_calls alternately until a round adds nothing.
void	get_values (locationt locationt l, const expr2tc &expr, valuest &dest) override
	value_setst interface: values `expr` may hold, as a list of object_descriptor2t wrapping each pointee's program expression.
void	get_reference_set (locationt locationt l, const expr2tc &expr, valuest &dest) override
	The set of objects a dereference-style l-value can refer to.
bool	has_location (locationt locationt) const override
	Flow-insensitive: any location is "known" once the analysis has run.
Public Member Functions inherited from value_setst
	value_setst ()=default
virtual	~value_setst ()=default

Static Public Member Functions
static bool	is_nondet_object (const expr2tc &object)
	True iff `object` is that sentinel.

Static Public Attributes
static constexpr node_id	TOP = 0
	Reserved "may point anywhere".
static constexpr const char *	nondet_object_name = "andersen::nondet"
	The object an unconstrained pointer points at: symbolic execution resolves a dereference of one to an invalid object, so a consumer can skip it, while an empty set still means "nothing constrained this".

Protected Member Functions
const node_id *	find_node (const expr2tc &e) const
	The node interned for `e`, or nullptr if it was never seen.
void	ensure_node (node_id n)
	Grows all node-indexed vectors so `n` is a valid index.
node_id	fresh_node ()
	A node with no program expression, used to hold the intermediate value of a compound right-hand side.
bool	join (node_id dst, node_id src)
	Unions pts[src] into pts[dst]; true iff pts[dst] grew.
bool	add_copy_edge (node_id from, node_id to)
	Adds the copy edge from -> to and propagates along it immediately.
node_id	allocation (const type2tc &type, unsigned loc)
	A node pointing to the heap object allocated at `loc`.
node_id	unconstrained ()
	A node pointing to the nondet sentinel: an unconstrained value.
node_id	top_source ()
	A node whose points-to set is {TOP}.
node_id	return_node (const irep_idt &fn)
	The node standing for `fn's` return value, shared by every call site (context insensitivity).
node_id	eval_rhs (const expr2tc &rhs, unsigned location_number)
	A node whose points-to set is the value of `rhs`, introducing a fresh_node when the expression is not already a nameable object.
node_id	eval_address_of (const address_of2t &rhs, unsigned location_number)
	The parts of eval_rhs, each for one kind of expression.
std::optional< node_id >	eval_sideeffect (const sideeffect2t &rhs, unsigned location_number)
node_id	eval_realloc (node_id fresh, const expr2tc &old, unsigned location_number)
std::optional< node_id >	eval_pointer_arithmetic (const expr2tc &rhs, unsigned location_number)
node_id	eval_branch (const if2t &rhs, unsigned location_number)
node_id	eval_value (const expr2tc &rhs, unsigned location_number)
	A constant, an l-value read as a value, or an integer or aggregate that may carry addresses; TOP for anything else.
node_id	eval_integer (const expr2tc &rhs, unsigned location_number)
node_id	eval_constant_aggregate (const expr2tc &rhs, unsigned location_number)
void	handle_assign (const expr2tc &lhs, const expr2tc &rhs, unsigned location_number)
	Lowers lhs := rhs to whichever of the four constraints fits.
void	assign_node (const expr2tc &lhs, node_id src, unsigned loc)
	Adds what `src` points to into every object `lhs` may designate: both arms of a conditional, and through the pointer of a dereference.
void	assign_top (const expr2tc &lhs, unsigned loc)
	Records that the object `lhs` designates may hold any address, storing through the pointer when `lhs` is a dereference.
void	handle_other (const expr2tc &code, unsigned location_number)
	Lowers an OTHER instruction: the ones that only read are dropped, the rest may write through any pointer operand.
void	handle_function_call (const code_function_call2t &call, const goto_functionst &goto_functions, unsigned location_number)
	Binds arguments to formals and the return value to the LHS.
bool	resolve_indirect_calls (const goto_functionst &goto_functions)
	Lowers every indirect call whose target set is now known.
void	bind_call (const irep_idt &callee_name, const goto_functiont &callee, const expr2tc &ret, const std::vector< expr2tc > &arguments, unsigned location_number)
	Binds `arguments` to `callee's` formals and its return value to `ret`.
void	widen_call (const expr2tc &ret, const std::vector< expr2tc > &arguments, unsigned location_number)
	The conservative treatment of a callee this analysis cannot name: it may return anything and write anything through the pointers it is handed.
void	to_object_descriptors (node_id n, valuest &dest) const
	Translates a solved points-to set into the object_descriptor2t list shape that value_setst consumers expect.

Protected Attributes
std::vector< std::unordered_set< node_id > >	pts
	node -> its points-to set. The analysis result.
std::vector< constraintt >	constraints
	All registered constraints (see add_constraint).
std::vector< std::unordered_set< node_id > >	copy_edges
	Copy edges from -> to built during solve (dynamic edges from load/store are appended here as they are discovered).
std::unordered_map< irep_idt, node_id, irep_id_hash >	symbol_to_node
	Node tracking.
std::unordered_map< expr2tc, node_id, irep2_hash >	expr_to_node
std::vector< expr2tc >	node_to_expr
unsigned	tmp_count = 0
	Counter behind fresh_node.
bool	solved = false
	Set once solve has produced a valid fixpoint.
bool	everything_escapes = false
	Set when the program contains a statement whose effect on memory is not visible in the IR at all (inline asm: IREP2 keeps only its source string, not the operands it writes through).
std::unordered_set< irep_idt, irep_id_hash >	allocators
	Functions each call of which allocates an object of its own, so a call to one is an allocation site rather than a binding of its return value.
std::unordered_map< irep_idt, bool, irep_id_hash >	reads_varargs
	Whether each function bound so far reads its variadic arguments.
std::vector< indirect_callt >	indirect_calls

Member Typedef Documentation

◆ node_id

typedef unsigned andersent::node_id

A node is an abstract memory location: one program variable or one allocation site.

Nodes are dense integers so points-to sets can be cheap hashed-int sets (and, later, bitvectors).

Member Enumeration Documentation

◆ constraint_kindt

enum class andersent::constraint_kindt

strong

The four inclusion-constraint shapes of The four constraint kinds.

Enumerator
ADDRESS_OF	pts[lhs] ⊇ {rhs} (lhs = &rhs)
COPY	pts[lhs] ⊇ pts[rhs] (lhs = rhs)
LOAD	pts[lhs] ⊇ pts[rhs] (lhs = rhs)
STORE	pts[lhs] ⊇ pts[rhs] (lhs = rhs)

Constructor & Destructor Documentation

◆ andersent()

andersent::andersent ( )

Member Function Documentation

◆ add_constraint()

void andersent::add_constraint	(	constraint_kindt	kind,
		node_id	lhs,
		node_id	rhs )

Registers one constraint. Cheap; the real work happens in solve.

◆ add_copy_edge()

bool andersent::add_copy_edge	(	node_id	from,
		node_id	to )

protected

Adds the copy edge from -> to and propagates along it immediately.

True iff pts[to] grew.

◆ allocation()

andersent::node_id andersent::allocation	(	const type2tc &	type,
		unsigned	loc )

protected

A node pointing to the heap object allocated at loc.

◆ assign_node()

void andersent::assign_node	(	const expr2tc &	lhs,
		node_id	src,
		unsigned	loc )

protected

Adds what src points to into every object lhs may designate: both arms of a conditional, and through the pointer of a dereference.

◆ assign_top()

void andersent::assign_top	(	const expr2tc &	lhs,
		unsigned	loc )

protected

Records that the object lhs designates may hold any address, storing through the pointer when lhs is a dereference.

The escape hatch for an assignment whose source this frontend cannot model.

◆ bind_call()

void andersent::bind_call	(	const irep_idt &	callee_name,
		const goto_functiont &	callee,
		const expr2tc &	ret,
		const std::vector< expr2tc > &	arguments,
		unsigned	location_number )

protected

Binds arguments to callee's formals and its return value to ret.

◆ collect_constraints()

void andersent::collect_constraints ( const goto_functionst & goto_functions )

Walks every function body and lowers pointer-relevant assignments, returns and calls to constraints via add_constraint.

Field-, index- and context-insensitive; see the implementation for the modelling choices. Independent of solve: it only builds constraints.

Calls through a function pointer cannot be lowered here — their targets are exactly what is being computed — so they are recorded and left to resolve_indirect_calls. Use operator(), which drives both.

◆ ensure_node()

void andersent::ensure_node ( node_id n )

protected

Grows all node-indexed vectors so n is a valid index.

◆ eval_address_of()

andersent::node_id andersent::eval_address_of	(	const address_of2t &	rhs,
		unsigned	location_number )

protected

The parts of eval_rhs, each for one kind of expression.

Those that return an optional give nothing when rhs is not of their kind.

◆ eval_branch()

andersent::node_id andersent::eval_branch	(	const if2t &	rhs,
		unsigned	location_number )

protected

◆ eval_constant_aggregate()

andersent::node_id andersent::eval_constant_aggregate	(	const expr2tc &	rhs,
		unsigned	location_number )

protected

◆ eval_integer()

andersent::node_id andersent::eval_integer	(	const expr2tc &	rhs,
		unsigned	location_number )

protected

◆ eval_pointer_arithmetic()

std::optional< andersent::node_id > andersent::eval_pointer_arithmetic	(	const expr2tc &	rhs,
		unsigned	location_number )

protected

◆ eval_realloc()

andersent::node_id andersent::eval_realloc	(	node_id	fresh,
		const expr2tc &	old,
		unsigned	location_number )

protected

◆ eval_rhs()

andersent::node_id andersent::eval_rhs	(	const expr2tc &	rhs,
		unsigned	location_number )

protected

A node whose points-to set is the value of rhs, introducing a fresh_node when the expression is not already a nameable object.

It may be another object's own node, so callers only ever read it.

◆ eval_sideeffect()

std::optional< andersent::node_id > andersent::eval_sideeffect	(	const sideeffect2t &	rhs,
		unsigned	location_number )

protected

◆ eval_value()

andersent::node_id andersent::eval_value	(	const expr2tc &	rhs,
		unsigned	location_number )

protected

A constant, an l-value read as a value, or an integer or aggregate that may carry addresses; TOP for anything else.

◆ find_node()

const andersent::node_id * andersent::find_node ( const expr2tc & e ) const

protected

The node interned for e, or nullptr if it was never seen.

◆ fresh_node()

andersent::node_id andersent::fresh_node ( )

protected

A node with no program expression, used to hold the intermediate value of a compound right-hand side.

Never the target of an ADDRESS_OF, so it never appears inside a points-to set.

◆ get_node()

andersent::node_id andersent::get_node ( const expr2tc & e )

Interns e as a node, returning a stable id (creates one on first use).

Symbols are interned by identifier alone: the same variable can reach the analysis with different-but-compatible types (a symbol_type at one use, the followed struct at another), and those must share a node.

◆ get_reference_set()

void andersent::get_reference_set	(	locationt locationt	l,
		const expr2tc &	expr,
		valuest &	dest )

overridevirtual

The set of objects a dereference-style l-value can refer to.

Implements value_setst.

◆ get_values()

void andersent::get_values	(	locationt locationt	l,
		const expr2tc &	expr,
		valuest &	dest )

overridevirtual

value_setst interface: values expr may hold, as a list of object_descriptor2t wrapping each pointee's program expression.

Implements value_setst.

◆ handle_assign()

void andersent::handle_assign	(	const expr2tc &	lhs,
		const expr2tc &	rhs,
		unsigned	location_number )

protected

Lowers lhs := rhs to whichever of the four constraints fits.

◆ handle_function_call()

void andersent::handle_function_call	(	const code_function_call2t &	call,
		const goto_functionst &	goto_functions,
		unsigned	location_number )

protected

Binds arguments to formals and the return value to the LHS.

◆ handle_other()

void andersent::handle_other	(	const expr2tc &	code,
		unsigned	location_number )

protected

Lowers an OTHER instruction: the ones that only read are dropped, the rest may write through any pointer operand.

◆ has_location()

bool andersent::has_location ( locationt locationt ) const

inlineoverridevirtual

Flow-insensitive: any location is "known" once the analysis has run.

Implements value_setst.

◆ is_nondet_object()

bool andersent::is_nondet_object ( const expr2tc & object )

inlinestatic

True iff object is that sentinel.

◆ join()

bool andersent::join	(	node_id	dst,
		node_id	src )

protected

Unions pts[src] into pts[dst]; true iff pts[dst] grew.

◆ may_point_to()

bool andersent::may_point_to	(	node_id	a,
		node_id	b ) const

True iff a may point to b (i.e. b ∈ pts[a]).

◆ operator()()

void andersent::operator() ( const goto_functionst & goto_functions )

Runs the whole analysis: collect_constraints, then solve and resolve_indirect_calls alternately until a round adds nothing.

◆ points_to()

const std::unordered_set< andersent::node_id > & andersent::points_to ( node_id n ) const

The points-to set of n after solve (empty if never grown).

◆ points_to_top()

void andersent::points_to_top ( node_id n )

Marks n as possibly pointing anywhere by adding TOP to its set.

The conservative escape hatch for anything the frontend cannot model.

◆ resolve_indirect_calls()

bool andersent::resolve_indirect_calls ( const goto_functionst & goto_functions )

protected

Lowers every indirect call whose target set is now known.

True iff new constraints were added, meaning another solve round is needed.

◆ return_node()

andersent::node_id andersent::return_node ( const irep_idt & fn )

protected

The node standing for fn's return value, shared by every call site (context insensitivity).

◆ solve()

void andersent::solve ( )

Computes the least fixpoint of all registered constraints, populating pts.

Idempotent: safe to call again after adding constraints.

◆ to_object_descriptors()

void andersent::to_object_descriptors	(	node_id	n,
		valuest &	dest ) const

protected

Translates a solved points-to set into the object_descriptor2t list shape that value_setst consumers expect.

◆ top_source()

andersent::node_id andersent::top_source ( )

protected

A node whose points-to set is {TOP}.

Used as the source of a STORE to express "an unmodelled callee may write anything through this pointer".

◆ unconstrained()

andersent::node_id andersent::unconstrained ( )

protected

A node pointing to the nondet sentinel: an unconstrained value.

◆ widen_call()

void andersent::widen_call	(	const expr2tc &	ret,
		const std::vector< expr2tc > &	arguments,
		unsigned	location_number )

protected

The conservative treatment of a callee this analysis cannot name: it may return anything and write anything through the pointers it is handed.

Member Data Documentation

◆ allocators

std::unordered_set<irep_idt, irep_id_hash> andersent::allocators

protected

Functions each call of which allocates an object of its own, so a call to one is an allocation site rather than a binding of its return value.

◆ constraints

std::vector<constraintt> andersent::constraints

protected

All registered constraints (see add_constraint).

◆ copy_edges

std::vector<std::unordered_set<node_id> > andersent::copy_edges

protected

Copy edges from -> to built during solve (dynamic edges from load/store are appended here as they are discovered).

A set, because the load/store rules re-derive the same edge on every re-visit of a node and duplicates would otherwise accumulate without bound.

◆ everything_escapes

bool andersent::everything_escapes = false

protected

Set when the program contains a statement whose effect on memory is not visible in the IR at all (inline asm: IREP2 keeps only its source string, not the operands it writes through).

No per-object widening can be sound then, so every query answers TOP.

◆ expr_to_node

std::unordered_map<expr2tc, node_id, irep2_hash> andersent::expr_to_node

protected

◆ indirect_calls

std::vector<indirect_callt> andersent::indirect_calls

protected

◆ node_to_expr

std::vector<expr2tc> andersent::node_to_expr

protected

◆ nondet_object_name

const char* andersent::nondet_object_name = "andersen::nondet"

staticconstexpr

The object an unconstrained pointer points at: symbolic execution resolves a dereference of one to an invalid object, so a consumer can skip it, while an empty set still means "nothing constrained this".

It is inert, as that invalid object is: a store into it is dropped and a load from it yields another unconstrained pointer. Sound relative to symex's memory model, not to C's.

◆ pts

std::vector<std::unordered_set<node_id> > andersent::pts

protected

node -> its points-to set. The analysis result.

◆ reads_varargs

std::unordered_map<irep_idt, bool, irep_id_hash> andersent::reads_varargs

protected

Whether each function bound so far reads its variadic arguments.

◆ solved

bool andersent::solved = false

protected

Set once solve has produced a valid fixpoint.

◆ symbol_to_node

std::unordered_map<irep_idt, node_id, irep_id_hash> andersent::symbol_to_node

protected

Node tracking.

Symbols are keyed by identifier, everything else by the expression itself; see get_node.

◆ tmp_count

unsigned andersent::tmp_count = 0

protected

Counter behind fresh_node.

◆ TOP

node_id andersent::TOP = 0

staticconstexpr

Reserved "may point anywhere".

The documentation for this class was generated from the following files:

src/pointer-analysis/andersen.h
src/pointer-analysis/andersen.cpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Protected Member Functions

Protected Attributes

Member Typedef Documentation

◆ node_id

Member Enumeration Documentation

◆ constraint_kindt

Constructor & Destructor Documentation

◆ andersent()

Member Function Documentation

◆ add_constraint()

◆ add_copy_edge()

◆ allocation()

◆ assign_node()

◆ assign_top()

◆ bind_call()

◆ collect_constraints()

◆ ensure_node()

◆ eval_address_of()

◆ eval_branch()

◆ eval_constant_aggregate()

◆ eval_integer()

◆ eval_pointer_arithmetic()

◆ eval_realloc()

◆ eval_rhs()

◆ eval_sideeffect()

◆ eval_value()

◆ find_node()

◆ fresh_node()

◆ get_node()

◆ get_reference_set()

◆ get_values()

◆ handle_assign()

◆ handle_function_call()

◆ handle_other()

◆ has_location()

◆ is_nondet_object()

◆ join()

◆ may_point_to()

◆ operator()()

◆ points_to()

◆ points_to_top()

◆ resolve_indirect_calls()

◆ return_node()

◆ solve()

◆ to_object_descriptors()

◆ top_source()

◆ unconstrained()

◆ widen_call()

Member Data Documentation

◆ allocators

◆ constraints

◆ copy_edges

◆ everything_escapes

◆ expr_to_node

◆ indirect_calls

◆ node_to_expr

◆ nondet_object_name

◆ pts

◆ reads_varargs

◆ solved

◆ symbol_to_node

◆ tmp_count

◆ TOP