15#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWANALYSISCONTEXT_H
16#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWANALYSISCONTEXT_H
26#include "llvm/ADT/DenseMap.h"
27#include "llvm/ADT/DenseSet.h"
28#include "llvm/ADT/SetVector.h"
29#include "llvm/Support/Compiler.h"
109 std::function<llvm::StringMap<QualType>(
QualType)> CB) {
110 assert(!RecordStorageLocationCreated);
111 SyntheticFieldCallback = CB;
182 llvm::raw_ostream &OS = llvm::dbgs());
208 if (SyntheticFieldCallback)
209 return SyntheticFieldCallback(
Type);
216 struct NullableQualTypeDenseMapInfo :
private llvm::DenseMapInfo<QualType> {
222 using DenseMapInfo::getHashValue;
223 using DenseMapInfo::getTombstoneKey;
224 using DenseMapInfo::isEqual;
228 void addModeledFields(
const FieldSet &Fields);
233 addTransitiveFlowConditionConstraints(
Atom Token,
234 llvm::SetVector<const Formula *> &Out);
238 bool isSatisfiable(llvm::SetVector<const Formula *> Constraints) {
245 bool isUnsatisfiable(llvm::SetVector<const Formula *> Constraints) {
250 std::unique_ptr<Solver> S;
251 std::unique_ptr<Arena> A;
258 llvm::DenseMap<const ValueDecl *, StorageLocation *> DeclToLoc;
259 llvm::DenseMap<const Expr *, StorageLocation *> ExprToLoc;
267 llvm::DenseMap<QualType, PointerValue *, NullableQualTypeDenseMapInfo>
284 llvm::DenseMap<Atom, llvm::DenseSet<Atom>> FlowConditionDeps;
285 llvm::DenseMap<Atom, const Formula *> FlowConditionConstraints;
286 const Formula *Invariant =
nullptr;
288 llvm::DenseMap<const FunctionDecl *, ControlFlowContext> FunctionContexts;
293 std::unique_ptr<Logger> LogOwner;
295 std::function<llvm::StringMap<QualType>(QualType)> SyntheticFieldCallback;
298 bool RecordStorageLocationCreated =
false;
Allows QualTypes to be sorted and hence used in maps and sets.
This represents one expression.
Represents a function declaration or definition.
A (possibly-)qualified type.
static QualType getFromOpaquePtr(const void *Ptr)
Token - This structure provides full information about a lexed token.
The base class of the type hierarchy.
bool isRecordType() const
Represent the declaration of a variable (in which case it is an lvalue) a function (in which case it ...
The Arena owns the objects that model data within an analysis.
Holds CFG and other derived context that is needed to perform dataflow analysis.
Owns objects that encompass the state of a program and stores context that is used during dataflow an...
const Options & getOptions()
void setSyntheticFieldCallback(std::function< llvm::StringMap< QualType >(QualType)> CB)
Sets a callback that returns the names and types of the synthetic fields to add to a RecordStorageLoc...
Atom joinFlowConditions(Atom FirstToken, Atom SecondToken)
Creates a new flow condition that represents the disjunction of the flow conditions identified by Fir...
void addFlowConditionConstraint(Atom Token, const Formula &Constraint)
Adds Constraint to the flow condition identified by Token.
Atom forkFlowCondition(Atom Token)
Creates a new flow condition with the same constraints as the flow condition identified by Token and ...
bool equivalentFormulas(const Formula &Val1, const Formula &Val2)
Returns true if Val1 is equivalent to Val2.
StorageLocation & getStableStorageLocation(const ValueDecl &D)
Returns a stable storage location for D.
bool flowConditionImplies(Atom Token, const Formula &F)
Returns true if the constraints of the flow condition identified by Token imply that F is true.
Solver::Result querySolver(llvm::SetVector< const Formula * > Constraints)
Returns the outcome of satisfiability checking on Constraints.
bool flowConditionAllows(Atom Token, const Formula &F)
Returns true if the constraints of the flow condition identified by Token still allow F to be true.
PointerValue & getOrCreateNullPointerValue(QualType PointeeType)
Returns a pointer value that represents a null pointer.
void addInvariant(const Formula &Constraint)
Adds Constraint to current and future flow conditions in this context.
llvm::StringMap< QualType > getSyntheticFields(QualType Type)
Returns the names and types of the synthetic fields for the given record type.
~DataflowAnalysisContext()
StorageLocation & createStorageLocation(QualType Type)
Returns a new storage location appropriate for Type.
FieldSet getModeledFields(QualType Type)
Returns the fields of Type, limited to the set of fields modeled by this context.
LLVM_DUMP_METHOD void dumpFlowCondition(Atom Token, llvm::raw_ostream &OS=llvm::dbgs())
RecordStorageLocation & createRecordStorageLocation(QualType Type, RecordStorageLocation::FieldToLoc FieldLocs, RecordStorageLocation::SyntheticFieldMap SyntheticFields)
Creates a RecordStorageLocation for the given type and with the given fields.
const ControlFlowContext * getControlFlowContext(const FunctionDecl *F)
Returns the ControlFlowContext registered for F, if any.
Holds the state of the program (store and heap) at a given program point.
A logger is notified as the analysis progresses.
Models a symbolic pointer. Specifically, any value of type T*.
A storage location for a record (struct, class, or union).
llvm::DenseMap< const ValueDecl *, StorageLocation * > FieldToLoc
llvm::StringMap< StorageLocation * > SyntheticFieldMap
Base class for elements of the local variable store and of the heap.
Atom
Identifies an atomic boolean variable such as "V1".
llvm::SmallSetVector< const FieldDecl *, 4 > FieldSet
A set of FieldDecl *.
FieldSet getObjectFields(QualType Type)
Returns the set of all fields in the type.
const Expr & ignoreCFGOmittedNodes(const Expr &E)
Skip past nodes that the CFG does not emit.
bool containsSameFields(const FieldSet &Fields, const RecordStorageLocation::FieldToLoc &FieldLocs)
Returns whether Fields and FieldLocs contain the same fields.
unsigned Depth
The maximum depth to analyze.
Logger * Log
If provided, analysis details will be recorded here.
std::optional< ContextSensitiveOptions > ContextSensitiveOpts
Options for analyzing function bodies when present in the translation unit, or empty to disable conte...
Status getStatus() const
Returns the status of satisfiability checking on the queried boolean formula.
@ Unsatisfiable
Indicates that there is no satisfying assignment for a boolean formula.
@ Satisfiable
Indicates that there exists a satisfying assignment for a boolean formula.