22#include "llvm/ADT/DenseSet.h"
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"
38 "dataflow-log", llvm::cl::Hidden, llvm::cl::ValueOptional,
39 llvm::cl::desc(
"Emit log of dataflow analysis. With no arg, writes textual "
40 "log to stderr. With an arg, writes HTML logs under the "
41 "specified directory (one per analyzed function)."));
54 if (Opts.ContextSensitiveOpts)
60void DataflowAnalysisContext::addModeledFields(
const FieldSet &Fields) {
61 ModeledFields.set_union(Fields);
66 llvm::DenseMap<const ValueDecl *, StorageLocation *> FieldLocs;
68 if (Field->getType()->isReferenceType())
69 FieldLocs.insert({Field,
nullptr});
72 Field->getType().getNonReferenceType())});
76 SyntheticFields.insert(
81 std::move(SyntheticFields));
89static llvm::DenseSet<llvm::StringRef>
getKeys(
const llvm::StringMap<T> &Map) {
90 return llvm::DenseSet<llvm::StringRef>(llvm::from_range, Map.keys());
100 RecordStorageLocationCreated =
true;
102 std::move(SyntheticFields));
107 if (
auto *Loc = DeclToLoc.lookup(&D))
110 DeclToLoc[&D] = &Loc;
118 if (
auto *Loc = ExprToLoc.lookup(&CanonE))
121 ExprToLoc[&CanonE] = &Loc;
127 auto CanonicalPointeeType =
129 auto Res = NullPointerVals.try_emplace(CanonicalPointeeType,
nullptr);
134 return *Res.first->second;
146 auto Res = FlowConditionConstraints.try_emplace(
Token, &Constraint);
155 FlowConditionDeps[ForkToken].insert(
Token);
164 auto &TokenDeps = FlowConditionDeps[
Token];
165 TokenDeps.insert(FirstToken);
166 TokenDeps.insert(SecondToken);
168 arena().makeOr(
arena().makeAtomRef(FirstToken),
169 arena().makeAtomRef(SecondToken)));
174 llvm::SetVector<const Formula *> Constraints) {
175 return S.solve(Constraints.getArrayRef());
188 llvm::SetVector<const Formula *> Constraints;
189 Constraints.insert(&
arena().makeAtomRef(
Token));
190 Constraints.insert(&
arena().makeNot(F));
191 addTransitiveFlowConditionConstraints(
Token, Constraints);
192 return isUnsatisfiable(std::move(Constraints));
200 llvm::SetVector<const Formula *> Constraints;
201 Constraints.insert(&
arena().makeAtomRef(
Token));
202 Constraints.insert(&F);
203 addTransitiveFlowConditionConstraints(
Token, Constraints);
204 return isSatisfiable(std::move(Constraints));
209 llvm::SetVector<const Formula *> Constraints;
210 Constraints.insert(&
arena().makeNot(
arena().makeEquals(Val1, Val2)));
211 return isUnsatisfiable(std::move(Constraints));
214llvm::DenseSet<Atom> DataflowAnalysisContext::collectDependencies(
215 llvm::DenseSet<Atom> Tokens)
const {
218 std::vector<Atom> Remaining(Tokens.begin(), Tokens.end());
219 while (!Remaining.empty()) {
220 Atom CurrentToken = Remaining.back();
221 Remaining.pop_back();
222 if (
auto DepsIt = FlowConditionDeps.find(CurrentToken);
223 DepsIt != FlowConditionDeps.end())
224 for (
Atom A : DepsIt->second)
225 if (Tokens.insert(A).second)
226 Remaining.push_back(A);
232void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
233 Atom Token, llvm::SetVector<const Formula *> &Constraints) {
234 llvm::DenseSet<Atom> AddedTokens;
235 std::vector<Atom> Remaining = {Token};
240 while (!Remaining.empty()) {
241 auto Token = Remaining.back();
242 Remaining.pop_back();
243 if (!AddedTokens.insert(Token).second)
246 auto ConstraintsIt = FlowConditionConstraints.find(Token);
247 if (ConstraintsIt == FlowConditionConstraints.end()) {
250 Constraints.insert(&
arena().makeAtomRef(Token));
254 Constraints.insert(&
arena().makeEquals(
arena().makeAtomRef(Token),
255 *ConstraintsIt->second));
258 if (
auto DepsIt = FlowConditionDeps.find(Token);
259 DepsIt != FlowConditionDeps.end())
260 for (
Atom A : DepsIt->second)
261 Remaining.push_back(A);
266 llvm::DenseSet<dataflow::Atom> &Refs) {
270 std::stack<const Formula *> WorkList;
273 while (!WorkList.empty()) {
274 const Formula *Current = WorkList.top();
276 switch (Current->
kind()) {
278 Refs.insert(Current->
getAtom());
283 WorkList.push(Current->
operands()[0]);
290 WorkList.push(Operands[0]);
291 WorkList.push(Operands[1]);
298 llvm::DenseSet<dataflow::Atom> TargetTokens)
const {
306 llvm::DenseSet<dataflow::Atom> Dependencies =
307 collectDependencies(std::move(TargetTokens));
312 const Formula *Constraints = FlowConditionConstraints.lookup(
Token);
313 if (Constraints ==
nullptr)
317 if (
auto DepsIt = FlowConditionDeps.find(
Token);
318 DepsIt != FlowConditionDeps.end())
327 FlowConditionConstraints = std::move(LC.
TokenDefs);
331 FlowConditionDeps = std::move(LC.
TokenDeps);
335 llvm::raw_ostream &OS) {
337 for (
size_t i = 0; i < Atoms.size(); ++i) {
339 if (i + 1 < Atoms.size())
346 llvm::raw_ostream &OS) {
347 llvm::SetVector<const Formula *> Constraints;
348 Constraints.insert(&
arena().makeAtomRef(
Token));
349 addTransitiveFlowConditionConstraints(
Token, Constraints);
351 OS <<
"Flow condition token: " <<
Token <<
"\n";
353 llvm::SetVector<const Formula *> OriginalConstraints = Constraints;
355 if (!Constraints.empty()) {
356 OS <<
"Constraints:\n";
357 for (
const auto *Constraint : Constraints) {
358 Constraint->print(OS);
363 OS <<
"True atoms: ";
367 OS <<
"False atoms: ";
371 OS <<
"Equivalent atoms:\n";
376 OS <<
"\nFlow condition constraints before simplification:\n";
377 for (
const auto *Constraint : OriginalConstraints) {
378 Constraint->print(OS);
389 auto It = FunctionContexts.find(F);
390 if (It != FunctionContexts.end())
397 auto Result = FunctionContexts.insert({F, std::move(*ACFG)});
398 return &
Result.first->second;
409 if (
auto EC = llvm::sys::fs::create_directories(Dir))
410 llvm::errs() <<
"Failed to create log dir: " << EC.message() <<
"\n";
414 static std::atomic<unsigned> Counter = {0};
416 [Dir(Dir.str())]()
mutable -> std::unique_ptr<llvm::raw_ostream> {
418 llvm::sys::path::append(
File,
419 std::to_string(Counter.fetch_add(1)) +
".html");
421 auto OS = std::make_unique<llvm::raw_fd_ostream>(
File, EC);
423 llvm::errs() <<
"Failed to create log " <<
File <<
": " << EC.message()
425 return std::make_unique<llvm::raw_null_ostream>();
433 Solver &S, std::unique_ptr<Solver> &&OwnedSolver, Options Opts)
434 : S(S), OwnedSolver(
std::move(OwnedSolver)), A(
std::make_unique<Arena>()),
439 if (Opts.Log ==
nullptr) {
440 if (DataflowLog.getNumOccurrences() > 0) {
441 LogOwner = makeLoggerFromCommandLine();
442 this->Opts.Log = LogOwner.get();
445 this->Opts.Log = &Logger::null();
450DataflowAnalysisContext::~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)."))
Forward-declares and imports various common LLVM datatypes that clang wants to use unqualified.
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 getNonReferenceType() const
If Type is a reference type (e.g., const int&), returns the type that the reference refers to ("const...
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.
static llvm::Expected< AdornedCFG > build(const FunctionDecl &Func)
Builds an AdornedCFG from a FunctionDecl.
Atom makeFlowConditionToken()
Creates a fresh flow condition and returns a token that identifies it.
const Formula & makeAnd(const Formula &LHS, const Formula &RHS)
Returns a formula for the conjunction of LHS and RHS.
std::enable_if_t< std::is_base_of< StorageLocation, T >::value, T & > create(Args &&...args)
Creates a T (some subclass of StorageLocation), forwarding args to the constructor,...
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.
StorageLocation & createStorageLocation(QualType Type)
Returns a new storage location appropriate for Type.
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.
RecordStorageLocation & createRecordStorageLocation(QualType Type, RecordStorageLocation::FieldToLoc FieldLocs, RecordStorageLocation::SyntheticFieldMap SyntheticFields)
Creates a RecordStorageLocation for the given type and with the given fields.
static std::unique_ptr< Logger > textual(llvm::raw_ostream &)
A logger that simply writes messages to the specified ostream in real time.
static std::unique_ptr< Logger > html(std::function< std::unique_ptr< llvm::raw_ostream >()>)
A logger that builds an HTML UI to inspect the analysis results.
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.
static void getReferencedAtoms(const Formula &F, llvm::DenseSet< dataflow::Atom > &Refs)
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.
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.
@ Invariant
The parameter is invariant: must match exactly.
@ Class
The "class" keyword introduces the elaborated-type-specifier.
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
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.