clang::dataflow::Formula Class Reference

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

Public Types
enum	Kind : unsigned {   AtomRef , Literal , Not , And ,   Or , Implies , Equal }
using	AtomNames = llvm::DenseMap<Atom, std::string>

Public Member Functions
Kind	kind () const
Atom	getAtom () const
bool	literal () const
bool	isLiteral (bool b) const
ArrayRef< const Formula * >	operands () const
void	print (llvm::raw_ostream &OS, const AtomNames *=nullptr) const
	Produces a stable human-readable representation of this formula.

Static Public Member Functions
static const Formula &	create (llvm::BumpPtrAllocator &Alloc, Kind K, ArrayRef< const Formula * > Operands, unsigned Value=0)
	Allocates Formulas using Arena rather than calling this function directly.
static unsigned	numOperands (Kind K)
	Count of operands (sub-formulas) associated with Formulas of kind K.

Detailed Description

Definition at line 49 of file Formula.h.

Member Typedef Documentation

AtomNames

using clang::dataflow::Formula::AtomNames = llvm::DenseMap<Atom, std::string>

Definition at line 87 of file Formula.h.

Member Enumeration Documentation

Kind

enum clang::dataflow::Formula::Kind : unsigned

Enumerator
AtomRef	A reference to an atomic boolean variable. We name these e.g. "V3", where 3 == atom identity == Value.
Literal	Constant true or false.
Not
And	True if its only operand is false.
Or	True if LHS and RHS are both true.
Implies	True if either LHS or RHS is true.
Equal	True if LHS is false or RHS is true.

Definition at line 51 of file Formula.h.

Member Function Documentation

create()

const Formula & clang::dataflow::Formula::create ( llvm::BumpPtrAllocator & Alloc, Kind K, ArrayRef< const Formula * > Operands, unsigned Value = 0 )

static

Allocates Formulas using Arena rather than calling this function directly.

Definition at line 19 of file Formula.cpp.

References numOperands(), and clang::Result.

Referenced by clang::dataflow::Arena::makeAnd(), clang::dataflow::Arena::makeAtomRef(), clang::dataflow::Arena::makeEquals(), clang::dataflow::Arena::makeImplies(), clang::dataflow::Arena::makeNot(), and clang::dataflow::Arena::makeOr().

getAtom()

Atom clang::dataflow::Formula::getAtom ( ) const

inline

Definition at line 68 of file Formula.h.

References AtomRef, and kind().

Referenced by clang::dataflow::buildCNF(), clang::dataflow::AtomicBoolValue::getAtom(), clang::dataflow::TopBoolValue::getAtom(), clang::dataflow::getReferencedAtoms(), print(), clang::dataflow::serializeFormula(), and clang::dataflow::substitute().

isLiteral()

bool clang::dataflow::Formula::isLiteral ( bool b ) const

inline

Definition at line 78 of file Formula.h.

References b, kind(), and Literal.

Referenced by clang::dataflow::DataflowAnalysisContext::flowConditionAllows(), clang::dataflow::DataflowAnalysisContext::flowConditionImplies(), and clang::dataflow::simplifyConstraints().

kind()

Kind clang::dataflow::Formula::kind ( ) const

inline

Definition at line 66 of file Formula.h.

Referenced by clang::dataflow::buildCNF(), getAtom(), clang::dataflow::getReferencedAtoms(), isLiteral(), literal(), clang::dataflow::Arena::makeAnd(), clang::dataflow::Arena::makeBoolValue(), clang::dataflow::Arena::makeEquals(), clang::dataflow::Arena::makeImplies(), clang::dataflow::Arena::makeNot(), clang::dataflow::Arena::makeOr(), operands(), print(), clang::dataflow::serializeFormula(), clang::dataflow::simplifyConstraints(), and clang::dataflow::substitute().

literal()

bool clang::dataflow::Formula::literal ( ) const

inline

Definition at line 73 of file Formula.h.

References kind(), and Literal.

Referenced by clang::dataflow::buildCNF(), clang::dataflow::Arena::makeAnd(), clang::dataflow::Arena::makeEquals(), clang::dataflow::Arena::makeImplies(), clang::dataflow::Arena::makeNot(), clang::dataflow::Arena::makeOr(), print(), and clang::dataflow::serializeFormula().

numOperands()

unsigned clang::dataflow::Formula::numOperands ( Kind K )

inlinestatic

Count of operands (sub-formulas) associated with Formulas of kind K.

Definition at line 99 of file Formula.h.

References And, AtomRef, Equal, Implies, Literal, Not, and Or.

Referenced by create(), operands(), print(), and clang::dataflow::serializeFormula().

operands()

ArrayRef< const Formula * > clang::dataflow::Formula::operands ( ) const

inline

Definition at line 82 of file Formula.h.

References kind(), and numOperands().

Referenced by clang::dataflow::buildCNF(), clang::dataflow::getReferencedAtoms(), clang::dataflow::Arena::makeNot(), print(), clang::dataflow::serializeFormula(), clang::dataflow::simplifyConstraints(), and clang::dataflow::substitute().

print()

void clang::dataflow::Formula::print	(	llvm::raw_ostream &	OS,
		const AtomNames *	Names = nullptr ) const

Produces a stable human-readable representation of this formula.

For example: (V3 | !(V1 & V2)) If AtomNames is provided, these override the default V0, V1... names.

Definition at line 57 of file Formula.cpp.

References AtomRef, getAtom(), kind(), Literal, literal(), numOperands(), operands(), and clang::dataflow::sigil().

Referenced by clang::dataflow::operator<<().

---

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

• include/clang/Analysis/FlowSensitive/Formula.h
• lib/Analysis/FlowSensitive/Formula.cpp