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"
97 std::function<llvm::StringMap<QualType>(
QualType)> CB) {
98 assert(!RecordStorageLocationCreated);
99 SyntheticFieldCallback = CB;
170 llvm::raw_ostream &OS = llvm::dbgs());
196 if (SyntheticFieldCallback) {
197 llvm::StringMap<QualType>
Result = SyntheticFieldCallback(
Type);
200 for (
const auto &Entry :
Result)
201 if (Entry.getValue()->isReferenceType())
213 struct NullableQualTypeDenseMapInfo :
private llvm::DenseMapInfo<QualType> {
219 using DenseMapInfo::getHashValue;
220 using DenseMapInfo::getTombstoneKey;
221 using DenseMapInfo::isEqual;
228 DataflowAnalysisContext(Solver &S, std::unique_ptr<Solver> &&OwnedSolver,
232 void addModeledFields(
const FieldSet &Fields);
237 addTransitiveFlowConditionConstraints(
Atom Token,
238 llvm::SetVector<const Formula *> &Out);
242 bool isSatisfiable(llvm::SetVector<const Formula *> Constraints) {
249 bool isUnsatisfiable(llvm::SetVector<const Formula *> Constraints) {
255 std::unique_ptr<Solver> OwnedSolver;
256 std::unique_ptr<Arena> A;
263 llvm::DenseMap<const ValueDecl *, StorageLocation *> DeclToLoc;
264 llvm::DenseMap<const Expr *, StorageLocation *> ExprToLoc;
272 llvm::DenseMap<QualType, PointerValue *, NullableQualTypeDenseMapInfo>
289 llvm::DenseMap<Atom, llvm::DenseSet<Atom>> FlowConditionDeps;
290 llvm::DenseMap<Atom, const Formula *> FlowConditionConstraints;
291 const Formula *Invariant =
nullptr;
293 llvm::DenseMap<const FunctionDecl *, AdornedCFG> FunctionContexts;
298 std::unique_ptr<Logger> LogOwner;
300 std::function<llvm::StringMap<QualType>(QualType)> SyntheticFieldCallback;
303 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.
DataflowAnalysisContext(std::unique_ptr< Solver > S, Options Opts=Options{ std::nullopt, nullptr})
Constructs a dataflow analysis context.
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())
DataflowAnalysisContext(Solver &S, Options Opts=Options{ std::nullopt, nullptr})
Constructs a dataflow analysis context.
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
An interface for a SAT solver that can be used by dataflow analyses.
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.