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.

References create().

Referenced by Arena(), and operator=().

◆ Arena() [2/2]

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

delete

References Arena().

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.

References clang::cast().

Referenced by Arena(), clang::dataflow::Environment::create(), clang::dataflow::DataflowAnalysisContext::createRecordStorageLocation(), clang::dataflow::DataflowAnalysisContext::createStorageLocation(), clang::dataflow::DataflowAnalysisContext::getOrCreateNullPointerValue(), makeBoolValue(), makeIntLiteral(), and makeTopValue().

◆ 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.

References clang::cast().

◆ 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::dataflow::Formula::kind(), clang::dataflow::Formula::Literal, and clang::dataflow::Formula::literal().

Referenced by clang::dataflow::DataflowAnalysisContext::addFlowConditionConstraint(), clang::dataflow::DataflowAnalysisContext::addInvariant(), clang::dataflow::parsePrefix(), and 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(), makeTopValue(), and clang::dataflow::parsePrefix().

◆ 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(), clang::dataflow::parsePrefix(), 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 clang::cast(), 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, create(), 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::parsePrefix(), and 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().

Referenced by clang::dataflow::DataflowAnalysisContext::forkFlowCondition(), and clang::dataflow::DataflowAnalysisContext::joinFlowConditions().

◆ 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::parsePrefix(), and 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.

References create().

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

◆ makeLiteral()

const Formula & clang::dataflow::Arena::makeLiteral ( bool Value )

inline

Returns a formula for a literal true/false.

Definition at line 111 of file Arena.h.

Referenced by makeEquals(), makeImplies(), makeNot(), clang::dataflow::parsePrefix(), clang::dataflow::simplifyConstraints(), and clang::dataflow::ChromiumCheckModel::transfer().

◆ makeNot()

const Formula & clang::dataflow::Arena::makeNot ( const Formula & Val )

Returns a formula for the negation of Val.

Definition at line 67 of file Arena.cpp.

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

Referenced by makeEquals(), makeImplies(), clang::dataflow::parsePrefix(), clang::dataflow::substitute(), and clang::dataflow::widenDistinctValues().

◆ makeOr()

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

Returns a formula for the disjunction of LHS and RHS.

Definition at line 54 of file Arena.cpp.

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

Referenced by clang::dataflow::parsePrefix(), and clang::dataflow::substitute().

◆ makeTopValue()

TopBoolValue & clang::dataflow::Arena::makeTopValue ( )

inline

Creates a fresh Top boolean value.

Definition at line 76 of file Arena.h.

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

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

◆ operator=()

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

delete

References Arena(), and clang::T.

◆ parseFormula()

llvm::Expected< const Formula & > clang::dataflow::Arena::parseFormula ( llvm::StringRef In )

Definition at line 202 of file Arena.cpp.

References clang::Result.

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

include/clang/Analysis/FlowSensitive/Arena.h
lib/Analysis/FlowSensitive/Arena.cpp

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ Arena() [1/2]

◆ Arena() [2/2]

Member Function Documentation

◆ create() [1/2]

◆ create() [2/2]

◆ makeAnd()

◆ makeAtom()

◆ makeAtomRef()

◆ makeAtomValue()

◆ makeBoolValue()

◆ makeEquals()

◆ makeFlowConditionToken()

◆ makeImplies()

◆ makeIntLiteral()

◆ makeLiteral()

◆ makeNot()

◆ makeOr()

◆ makeTopValue()

◆ operator=()

◆ parseFormula()