15#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWANALYSISCONTEXT_H
16#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DATAFLOWANALYSISCONTEXT_H
27#include "llvm/ADT/DenseMap.h"
28#include "llvm/ADT/DenseSet.h"
29#include "llvm/ADT/SetVector.h"
30#include "llvm/Support/Compiler.h"
85 std::function<llvm::StringMap<QualType>(
QualType)> CB) {
86 assert(!RecordStorageLocationCreated);
87 SyntheticFieldCallback = CB;
158 llvm::raw_ostream &OS = llvm::dbgs());
184 if (SyntheticFieldCallback) {
185 llvm::StringMap<QualType>
Result = SyntheticFieldCallback(
Type);
188 for (
const auto &Entry :
Result)
189 if (Entry.getValue()->isReferenceType())
201 struct NullableQualTypeDenseMapInfo :
private llvm::DenseMapInfo<QualType> {
207 using DenseMapInfo::getHashValue;
208 using DenseMapInfo::getTombstoneKey;
209 using DenseMapInfo::isEqual;
213 void addModeledFields(
const FieldSet &Fields);
218 addTransitiveFlowConditionConstraints(
Atom Token,
219 llvm::SetVector<const Formula *> &Out);
223 bool isSatisfiable(llvm::SetVector<const Formula *> Constraints) {
230 bool isUnsatisfiable(llvm::SetVector<const Formula *> Constraints) {
235 std::unique_ptr<Solver> S;
236 std::unique_ptr<Arena> A;
243 llvm::DenseMap<const ValueDecl *, StorageLocation *> DeclToLoc;
244 llvm::DenseMap<const Expr *, StorageLocation *> ExprToLoc;
252 llvm::DenseMap<QualType, PointerValue *, NullableQualTypeDenseMapInfo>
269 llvm::DenseMap<Atom, llvm::DenseSet<Atom>> FlowConditionDeps;
270 llvm::DenseMap<Atom, const Formula *> FlowConditionConstraints;
271 const Formula *Invariant =
nullptr;
273 llvm::DenseMap<const FunctionDecl *, AdornedCFG> FunctionContexts;
278 std::unique_ptr<Logger> LogOwner;
280 std::function<llvm::StringMap<QualType>(QualType)> SyntheticFieldCallback;
283 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 ...
Holds CFG with additional information derived from it that is needed to perform dataflow analysis.
The Arena owns the objects that model data within an 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...
const AdornedCFG * getAdornedCFG(const FunctionDecl *F)
Returns the AdornedCFG registered for F, if any.
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.
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 *.
The JSON file list parser is used to communicate input to InstallAPI.
@ Result
The result type of a method or function.
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.