23#include "llvm/ADT/SetOperations.h"
24#include "llvm/ADT/SetVector.h"
25#include "llvm/Support/CommandLine.h"
26#include "llvm/Support/Debug.h"
27#include "llvm/Support/FileSystem.h"
28#include "llvm/Support/Path.h"
29#include "llvm/Support/raw_ostream.h"
37 "dataflow-log", llvm::cl::Hidden, llvm::cl::ValueOptional,
38 llvm::cl::desc(
"Emit log of dataflow analysis. With no arg, writes textual "
39 "log to stderr. With an arg, writes HTML logs under the "
40 "specified directory (one per analyzed function)."));
59void DataflowAnalysisContext::addModeledFields(
const FieldSet &Fields) {
60 ModeledFields.set_union(Fields);
65 llvm::DenseMap<const ValueDecl *, StorageLocation *> FieldLocs;
67 if (Field->getType()->isReferenceType())
68 FieldLocs.insert({Field,
nullptr});
71 Field->getType().getNonReferenceType())});
75 SyntheticFields.insert(
80 std::move(SyntheticFields));
88static llvm::DenseSet<llvm::StringRef>
getKeys(
const llvm::StringMap<T> &Map) {
89 return llvm::DenseSet<llvm::StringRef>(Map.keys().begin(), Map.keys().end());
99 RecordStorageLocationCreated =
true;
101 std::move(SyntheticFields));
105DataflowAnalysisContext::getStableStorageLocation(
const ValueDecl &
D) {
106 if (
auto *
Loc = DeclToLoc.lookup(&
D))
108 auto &
Loc = createStorageLocation(
D.getType().getNonReferenceType());
109 DeclToLoc[&
D] = &
Loc;
114DataflowAnalysisContext::getStableStorageLocation(
const Expr &
E) {
117 if (
auto *
Loc = ExprToLoc.lookup(&CanonE))
119 auto &
Loc = createStorageLocation(CanonE.
getType());
120 ExprToLoc[&CanonE] = &
Loc;
125DataflowAnalysisContext::getOrCreateNullPointerValue(
QualType PointeeType) {
126 auto CanonicalPointeeType =
128 auto Res = NullPointerVals.try_emplace(CanonicalPointeeType,
nullptr);
130 auto &PointeeLoc = createStorageLocation(CanonicalPointeeType);
131 Res.first->second = &arena().create<
PointerValue>(PointeeLoc);
133 return *Res.first->second;
136void DataflowAnalysisContext::addInvariant(
const Formula &Constraint) {
143void DataflowAnalysisContext::addFlowConditionConstraint(
145 auto Res = FlowConditionConstraints.try_emplace(
Token, &Constraint);
148 &arena().makeAnd(*Res.first->second, Constraint);
153 Atom ForkToken = arena().makeFlowConditionToken();
154 FlowConditionDeps[ForkToken].insert(
Token);
155 addFlowConditionConstraint(ForkToken, arena().makeAtomRef(
Token));
160DataflowAnalysisContext::joinFlowConditions(
Atom FirstToken,
162 Atom Token = arena().makeFlowConditionToken();
163 FlowConditionDeps[
Token].insert(FirstToken);
164 FlowConditionDeps[
Token].insert(SecondToken);
165 addFlowConditionConstraint(
Token,
166 arena().makeOr(arena().makeAtomRef(FirstToken),
167 arena().makeAtomRef(SecondToken)));
172 llvm::SetVector<const Formula *> Constraints) {
173 return S.solve(Constraints.getArrayRef());
176bool DataflowAnalysisContext::flowConditionImplies(
Atom Token,
186 llvm::SetVector<const Formula *> Constraints;
187 Constraints.insert(&arena().makeAtomRef(
Token));
188 Constraints.insert(&arena().makeNot(F));
189 addTransitiveFlowConditionConstraints(
Token, Constraints);
190 return isUnsatisfiable(std::move(Constraints));
193bool DataflowAnalysisContext::flowConditionAllows(
Atom Token,
198 llvm::SetVector<const Formula *> Constraints;
199 Constraints.insert(&arena().makeAtomRef(
Token));
200 Constraints.insert(&F);
201 addTransitiveFlowConditionConstraints(
Token, Constraints);
202 return isSatisfiable(std::move(Constraints));
205bool DataflowAnalysisContext::equivalentFormulas(
const Formula &Val1,
207 llvm::SetVector<const Formula *> Constraints;
208 Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2)));
209 return isUnsatisfiable(std::move(Constraints));
212void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
213 Atom Token, llvm::SetVector<const Formula *> &Constraints) {
214 llvm::DenseSet<Atom> AddedTokens;
215 std::vector<Atom> Remaining = {
Token};
220 while (!Remaining.empty()) {
221 auto Token = Remaining.back();
222 Remaining.pop_back();
223 if (!AddedTokens.insert(
Token).second)
226 auto ConstraintsIt = FlowConditionConstraints.find(
Token);
227 if (ConstraintsIt == FlowConditionConstraints.end()) {
228 Constraints.insert(&arena().makeAtomRef(
Token));
232 Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token),
233 *ConstraintsIt->second));
236 if (
auto DepsIt = FlowConditionDeps.find(Token);
237 DepsIt != FlowConditionDeps.end())
238 for (Atom A : DepsIt->second)
239 Remaining.push_back(A);
244 llvm::raw_ostream &OS) {
246 for (
size_t i = 0; i < Atoms.size(); ++i) {
248 if (i + 1 < Atoms.size())
254void DataflowAnalysisContext::dumpFlowCondition(
Atom Token,
255 llvm::raw_ostream &OS) {
256 llvm::SetVector<const Formula *> Constraints;
257 Constraints.insert(&arena().makeAtomRef(
Token));
258 addTransitiveFlowConditionConstraints(
Token, Constraints);
260 OS <<
"Flow condition token: " <<
Token <<
"\n";
262 llvm::SetVector<const Formula *> OriginalConstraints = Constraints;
264 if (!Constraints.empty()) {
265 OS <<
"Constraints:\n";
266 for (
const auto *Constraint : Constraints) {
267 Constraint->print(OS);
272 OS <<
"True atoms: ";
276 OS <<
"False atoms: ";
280 OS <<
"Equivalent atoms:\n";
285 OS <<
"\nFlow condition constraints before simplification:\n";
286 for (
const auto *Constraint : OriginalConstraints) {
287 Constraint->print(OS);
298 auto It = FunctionContexts.find(F);
299 if (It != FunctionContexts.end())
303 auto ACFG = AdornedCFG::build(*F);
306 auto Result = FunctionContexts.insert({F, std::move(*ACFG)});
307 return &
Result.first->second;
315 return Logger::textual(llvm::errs());
318 if (
auto EC = llvm::sys::fs::create_directories(Dir))
319 llvm::errs() <<
"Failed to create log dir: " << EC.message() <<
"\n";
323 static std::atomic<unsigned> Counter = {0};
325 [Dir(Dir.str())]()
mutable -> std::unique_ptr<llvm::raw_ostream> {
327 llvm::sys::path::append(
File,
328 std::to_string(Counter.fetch_add(1)) +
".html");
330 auto OS = std::make_unique<llvm::raw_fd_ostream>(
File, EC);
332 llvm::errs() <<
"Failed to create log " <<
File <<
": " << EC.message()
334 return std::make_unique<llvm::raw_null_ostream>();
338 return Logger::html(std::move(StreamFactory));
341DataflowAnalysisContext::DataflowAnalysisContext(
342 Solver &S, std::unique_ptr<Solver> &&OwnedSolver, Options Opts)
343 : S(S), OwnedSolver(
std::move(OwnedSolver)), A(
std::make_unique<Arena>()),
348 if (Opts.Log ==
nullptr) {
351 this->Opts.Log = LogOwner.get();
359DataflowAnalysisContext::~DataflowAnalysisContext() =
default;
static llvm::cl::opt< std::string > DataflowLog("dataflow-log", llvm::cl::Hidden, llvm::cl::ValueOptional, llvm::cl::desc("Emit log of dataflow analysis. With no arg, writes textual " "log to stderr. With an arg, writes HTML logs under the " "specified directory (one per analyzed function)."))
Defines the clang::Expr interface and subclasses for C++ expressions.
This represents one expression.
Represents a member of a struct/union/class.
Represents a function declaration or definition.
bool doesThisDeclarationHaveABody() const
Returns whether this specific declaration of the function has a body.
FunctionDecl * getDefinition()
Get the definition for this declaration.
A (possibly-)qualified type.
bool isNull() const
Return true if this QualType doesn't point to a type yet.
QualType getCanonicalType() const
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.
llvm::StringMap< QualType > getSyntheticFields(QualType Type)
Returns the names and types of the synthetic fields for the given record type.
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.
RecordStorageLocation & createRecordStorageLocation(QualType Type, RecordStorageLocation::FieldToLoc FieldLocs, RecordStorageLocation::SyntheticFieldMap SyntheticFields)
Creates a RecordStorageLocation for the given type and with the given fields.
static Logger & null()
Returns a dummy logger that does nothing.
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
A storage location that is not subdivided further for the purposes of abstract interpretation.
Base class for elements of the local variable store and of the heap.
Atom
Identifies an atomic boolean variable such as "V1".
static void printAtomList(const llvm::SmallVector< Atom > &Atoms, llvm::raw_ostream &OS)
void simplifyConstraints(llvm::SetVector< const Formula * > &Constraints, Arena &arena, SimplifyConstraintsInfo *Info=nullptr)
Simplifies a set of constraints (implicitly connected by "and") in a way that does not change satisfi...
const Expr & ignoreCFGOmittedNodes(const Expr &E)
Skip past nodes that the CFG does not emit.
FieldSet getObjectFields(QualType Type)
Returns the set of all fields in the type.
static std::unique_ptr< Logger > makeLoggerFromCommandLine()
static llvm::DenseSet< llvm::StringRef > getKeys(const llvm::StringMap< T > &Map)
bool containsSameFields(const FieldSet &Fields, const RecordStorageLocation::FieldToLoc &FieldLocs)
Returns whether Fields and FieldLocs contain the same fields.
The JSON file list parser is used to communicate input to InstallAPI.
@ Result
The result type of a method or function.
@ Invariant
The parameter is invariant: must match exactly.
@ Class
The "class" keyword introduces the elaborated-type-specifier.
std::optional< ContextSensitiveOptions > ContextSensitiveOpts
Options for analyzing function bodies when present in the translation unit, or empty to disable conte...
Information on the way a set of constraints was simplified.
llvm::SmallVector< Atom > TrueAtoms
Atoms that the original constraints imply must be true.
llvm::SmallVector< llvm::SmallVector< Atom > > EquivalentAtoms
List of equivalence classes of atoms.
llvm::SmallVector< Atom > FalseAtoms
Atoms that the original constraints imply must be false.