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"
54 llvm::DenseMap<Atom, llvm::DenseSet<Atom>>
TokenDeps;
110 assert(!RecordStorageLocationCreated);
111 SyntheticFieldCallback = CB;
161 FlowConditionDeps[
Token].insert(Deps.begin(), Deps.end());
191 llvm::raw_ostream &OS = llvm::dbgs());
217 if (SyntheticFieldCallback) {
218 llvm::StringMap<QualType>
Result = SyntheticFieldCallback(
Type);
221 for (
const auto &Entry :
Result)
222 if (Entry.getValue()->isReferenceType())
242 struct NullableQualTypeDenseMapInfo :
private llvm::DenseMapInfo<QualType> {
248 using DenseMapInfo::getHashValue;
249 using DenseMapInfo::getTombstoneKey;
250 using DenseMapInfo::isEqual;
257 DataflowAnalysisContext(Solver &S, std::unique_ptr<Solver> &&OwnedSolver,
263 llvm::DenseSet<Atom> collectDependencies(llvm::DenseSet<Atom> Tokens)
const;
266 void addModeledFields(
const FieldSet &Fields);
271 addTransitiveFlowConditionConstraints(
Atom Token,
272 llvm::SetVector<const Formula *> &Out);
276 bool isSatisfiable(llvm::SetVector<const Formula *> Constraints) {
283 bool isUnsatisfiable(llvm::SetVector<const Formula *> Constraints) {
289 std::unique_ptr<Solver> OwnedSolver;
290 std::unique_ptr<Arena> A;
297 llvm::DenseMap<const ValueDecl *, StorageLocation *> DeclToLoc;
298 llvm::DenseMap<const Expr *, StorageLocation *> ExprToLoc;
306 llvm::DenseMap<QualType, PointerValue *, NullableQualTypeDenseMapInfo>
323 llvm::DenseMap<Atom, llvm::DenseSet<Atom>> FlowConditionDeps;
324 llvm::DenseMap<Atom, const Formula *> FlowConditionConstraints;
325 const Formula *Invariant =
nullptr;
327 llvm::DenseMap<const FunctionDecl *, AdornedCFG> FunctionContexts;
332 std::unique_ptr<Logger> LogOwner;
334 std::function<llvm::StringMap<QualType>(QualType)> SyntheticFieldCallback;
337 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.
void addFlowConditionDeps(Atom Token, const llvm::DenseSet< Atom > &Deps)
Adds Deps to the dependencies of the flow condition identified by Token.
SimpleLogicalContext exportLogicalContext(llvm::DenseSet< dataflow::Atom > TargetTokens) const
Export the logical-context portions of AC, limited to the given target flow-condition tokens.
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())
void initLogicalContext(SimpleLogicalContext LC)
Initializes this context's "logical" components with LC.
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.
int const char * 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...
A simple representation of essential elements of the logical context used in environments.
llvm::DenseMap< Atom, const Formula * > TokenDefs
const Formula * Invariant
llvm::DenseMap< Atom, llvm::DenseSet< Atom > > TokenDeps
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.