The Arena owns the objects that model data within an analysis. More...

#include "clang/Analysis/FlowSensitive/Arena.h"

Public Member Functions
	Arena ()

	Arena (const Arena &)=delete

Arena &	operator= (const Arena &)=delete

template<typename T , typename... Args>
std::enable_if_t< std::is_base_of< StorageLocation, T >::value, T & >	create (Args &&...args)
	Creates a `T` (some subclass of `StorageLocation`), forwarding `args` to the constructor, and returns a reference to it.

template<typename T , typename... Args>
std::enable_if_t< std::is_base_of< Value, T >::value, T & >	create (Args &&...args)
	Creates a `T` (some subclass of `Value`), forwarding `args` to the constructor, and returns a reference to it.

BoolValue &	makeBoolValue (const Formula &)
	Creates a BoolValue wrapping a particular formula.

AtomicBoolValue &	makeAtomValue ()
	Creates a fresh atom and wraps in in an AtomicBoolValue.

TopBoolValue &	makeTopValue ()
	Creates a fresh Top boolean value.

IntegerValue &	makeIntLiteral (llvm::APInt Value)
	Returns a symbolic integer value that models an integer literal equal to `Value`.

const Formula &	makeAnd (const Formula &LHS, const Formula &RHS)
	Returns a formula for the conjunction of `LHS` and `RHS`.

const Formula &	makeOr (const Formula &LHS, const Formula &RHS)
	Returns a formula for the disjunction of `LHS` and `RHS`.

const Formula &	makeNot (const Formula &Val)
	Returns a formula for the negation of `Val`.

const Formula &	makeImplies (const Formula &LHS, const Formula &RHS)
	Returns a formula for `LHS => RHS`.

const Formula &	makeEquals (const Formula &LHS, const Formula &RHS)
	Returns a formula for `LHS <=> RHS`.

const Formula &	makeAtomRef (Atom A)
	Returns a formula for the variable A.

const Formula &	makeLiteral (bool Value)
	Returns a formula for a literal true/false.

llvm::Expected< const Formula & >	parseFormula (llvm::StringRef)

Atom	makeAtom ()
	Returns a new atomic boolean variable, distinct from any other.

Atom	makeFlowConditionToken ()
	Creates a fresh flow condition and returns a token that identifies it.

Detailed Description

The Arena owns the objects that model data within an analysis.

For example, Value, StorageLocation, Atom, and Formula.

Definition at line 21 of file Arena.h.

Constructor & Destructor Documentation

◆ Arena() [1/2]

clang::dataflow::Arena::Arena ( )

inline

Definition at line 23 of file Arena.h.

◆ Arena() [2/2]

clang::dataflow::Arena::Arena ( const Arena & )

delete

Member Function Documentation

◆ create() [1/2]

template<typename T , typename... Args>

std::enable_if_t< std::is_base_of< StorageLocation, T >::value, T & > clang::dataflow::Arena::create ( Args &&... args )

inline

Creates a T (some subclass of StorageLocation), forwarding args to the constructor, and returns a reference to it.

The Arena takes ownership of the created object. The object will be destroyed when the Arena is destroyed.

Definition at line 36 of file Arena.h.

Referenced by clang::dataflow::Environment::create().

◆ create() [2/2]

template<typename T , typename... Args>

std::enable_if_t< std::is_base_of< Value, T >::value, T & > clang::dataflow::Arena::create ( Args &&... args )

inline

Creates a T (some subclass of Value), forwarding args to the constructor, and returns a reference to it.

The Arena takes ownership of the created object. The object will be destroyed when the Arena is destroyed.

Definition at line 52 of file Arena.h.

◆ makeAnd()

const Formula & clang::dataflow::Arena::makeAnd	(	const Formula &	LHS,
		const Formula &	RHS
	)

Returns a formula for the conjunction of LHS and RHS.

Definition at line 41 of file Arena.cpp.

References clang::dataflow::Formula::And, clang::dataflow::cached(), clang::dataflow::canonicalFormulaPair(), clang::dataflow::Formula::create(), clang::if(), clang::dataflow::Formula::kind(), clang::dataflow::Formula::Literal, and clang::dataflow::Formula::literal().

Referenced by clang::dataflow::substitute().

◆ makeAtom()

Atom clang::dataflow::Arena::makeAtom ( )

inline

Returns a new atomic boolean variable, distinct from any other.

Definition at line 118 of file Arena.h.

Referenced by makeAtomValue(), makeFlowConditionToken(), and makeTopValue().

◆ makeAtomRef()

const Formula & clang::dataflow::Arena::makeAtomRef ( Atom A )

Returns a formula for the variable A.

Definition at line 34 of file Arena.cpp.

References clang::dataflow::Formula::AtomRef, clang::dataflow::cached(), and clang::dataflow::Formula::create().

Referenced by clang::dataflow::joinDistinctValues(), makeAtomValue(), makeTopValue(), and clang::dataflow::simplifyConstraints().

◆ makeAtomValue()

AtomicBoolValue & clang::dataflow::Arena::makeAtomValue ( )

inline

Creates a fresh atom and wraps in in an AtomicBoolValue.

FIXME: For now, identical-address AtomicBoolValue <=> identical atom. Stop relying on pointer identity and remove this guarantee.

Definition at line 71 of file Arena.h.

References makeAtom(), makeAtomRef(), and makeBoolValue().

Referenced by clang::dataflow::Environment::makeAtomicBoolValue().

◆ makeBoolValue()

BoolValue & clang::dataflow::Arena::makeBoolValue ( const Formula & F )

Creates a BoolValue wrapping a particular formula.

Passing in the same formula will result in the same BoolValue. FIXME: Interning BoolValues but not other Values is inconsistent. Decide whether we want Value interning or not.

Definition at line 112 of file Arena.cpp.

References clang::dataflow::Formula::AtomRef, and clang::dataflow::Formula::kind().

Referenced by clang::dataflow::Environment::getBoolLiteralValue(), clang::dataflow::Environment::makeAnd(), makeAtomValue(), clang::dataflow::Environment::makeIff(), clang::dataflow::Environment::makeImplication(), clang::dataflow::Environment::makeNot(), clang::dataflow::Environment::makeOr(), and clang::dataflow::unpackValue().

◆ makeEquals()

const Formula & clang::dataflow::Arena::makeEquals	(	const Formula &	LHS,
		const Formula &	RHS
	)

Returns a formula for LHS <=> RHS.

Definition at line 91 of file Arena.cpp.

References clang::dataflow::cached(), clang::dataflow::canonicalFormulaPair(), clang::dataflow::Formula::create(), clang::dataflow::Formula::Equal, clang::dataflow::Formula::kind(), clang::dataflow::Formula::Literal, clang::dataflow::Formula::literal(), makeLiteral(), and makeNot().

Referenced by clang::dataflow::substitute().

◆ makeFlowConditionToken()

Atom clang::dataflow::Arena::makeFlowConditionToken ( )

inline

Creates a fresh flow condition and returns a token that identifies it.

The token can be used to perform various operations on the flow condition such as adding constraints to it, forking it, joining it with another flow condition, or checking implications.

Definition at line 124 of file Arena.h.

References makeAtom().

◆ makeImplies()

const Formula & clang::dataflow::Arena::makeImplies	(	const Formula &	LHS,
		const Formula &	RHS
	)

Returns a formula for LHS => RHS.

Definition at line 78 of file Arena.cpp.

References clang::dataflow::cached(), clang::dataflow::Formula::create(), clang::dataflow::Formula::Implies, clang::dataflow::Formula::kind(), clang::dataflow::Formula::Literal, clang::dataflow::Formula::literal(), makeLiteral(), and makeNot().

Referenced by clang::dataflow::substitute().

◆ makeIntLiteral()

IntegerValue & clang::dataflow::Arena::makeIntLiteral ( llvm::APInt Value )

Returns a symbolic integer value that models an integer literal equal to Value.

These literals are the same every time. Integer literals are not typed; the type is determined by the Expr that an integer literal is associated with.

Definition at line 104 of file Arena.cpp.

Referenced by clang::dataflow::Environment::getIntLiteralValue().