21#include "llvm/ADT/SetOperations.h"
22#include "llvm/ADT/SetVector.h"
23#include "llvm/Support/CommandLine.h"
24#include "llvm/Support/Debug.h"
25#include "llvm/Support/FileSystem.h"
26#include "llvm/Support/Path.h"
27#include "llvm/Support/raw_ostream.h"
35 "dataflow-log", llvm::cl::Hidden, llvm::cl::ValueOptional,
36 llvm::cl::desc(
"Emit log of dataflow analysis. With no arg, writes textual "
37 "log to stderr. With an arg, writes HTML logs under the "
38 "specified directory (one per analyzed function)."));
51 if (Opts.ContextSensitiveOpts)
57void DataflowAnalysisContext::addModeledFields(
const FieldSet &Fields) {
58 ModeledFields.set_union(Fields);
63 llvm::DenseMap<const ValueDecl *, StorageLocation *> FieldLocs;
65 if (Field->getType()->isReferenceType())
66 FieldLocs.insert({Field,
nullptr});
69 Field->getType().getNonReferenceType())});
73 SyntheticFields.insert(
78 std::move(SyntheticFields));
86static llvm::DenseSet<llvm::StringRef>
getKeys(
const llvm::StringMap<T> &Map) {
87 return llvm::DenseSet<llvm::StringRef>(llvm::from_range, Map.keys());
97 RecordStorageLocationCreated =
true;
99 std::move(SyntheticFields));
104 if (
auto *Loc = DeclToLoc.lookup(&D))
107 DeclToLoc[&D] = &Loc;
115 if (
auto *Loc = ExprToLoc.lookup(&CanonE))
118 ExprToLoc[&CanonE] = &Loc;
124 auto CanonicalPointeeType =
126 auto Res = NullPointerVals.try_emplace(CanonicalPointeeType,
nullptr);
131 return *Res.first->second;
143 auto Res = FlowConditionConstraints.try_emplace(
Token, &Constraint);
152 FlowConditionDeps[ForkToken].insert(
Token);
161 auto &TokenDeps = FlowConditionDeps[
Token];
162 TokenDeps.insert(FirstToken);
163 TokenDeps.insert(SecondToken);
165 arena().makeOr(
arena().makeAtomRef(FirstToken),
166 arena().makeAtomRef(SecondToken)));
171 llvm::SetVector<const Formula *> Constraints) {
172 return S.solve(Constraints.getArrayRef());
185 llvm::SetVector<const Formula *> Constraints;
186 Constraints.insert(&
arena().makeAtomRef(
Token));
187 Constraints.insert(&
arena().makeNot(F));
188 addTransitiveFlowConditionConstraints(
Token, Constraints);
189 return isUnsatisfiable(std::move(Constraints));
197 llvm::SetVector<const Formula *> Constraints;
198 Constraints.insert(&
arena().makeAtomRef(
Token));
199 Constraints.insert(&F);
200 addTransitiveFlowConditionConstraints(
Token, Constraints);
201 return isSatisfiable(std::move(Constraints));
206 llvm::SetVector<const Formula *> Constraints;
207 Constraints.insert(&
arena().makeNot(
arena().makeEquals(Val1, Val2)));
208 return isUnsatisfiable(std::move(Constraints));
211llvm::DenseSet<Atom> DataflowAnalysisContext::collectDependencies(
212 llvm::DenseSet<Atom> Tokens)
const {
215 std::vector<Atom> Remaining(Tokens.begin(), Tokens.end());
216 while (!Remaining.empty()) {
217 Atom CurrentToken = Remaining.back();
218 Remaining.pop_back();
219 if (
auto DepsIt = FlowConditionDeps.find(CurrentToken);
220 DepsIt != FlowConditionDeps.end())
221 for (
Atom A : DepsIt->second)
222 if (Tokens.insert(A).second)
223 Remaining.push_back(A);
229void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
230 Atom Token, llvm::SetVector<const Formula *> &Constraints) {
231 llvm::DenseSet<Atom> AddedTokens;
232 std::vector<Atom> Remaining = {Token};
237 while (!Remaining.empty()) {
238 auto Token = Remaining.back();
239 Remaining.pop_back();
240 if (!AddedTokens.insert(Token).second)
243 auto ConstraintsIt = FlowConditionConstraints.find(Token);
244 if (ConstraintsIt == FlowConditionConstraints.end()) {
247 Constraints.insert(&
arena().makeAtomRef(Token));
251 Constraints.insert(&
arena().makeEquals(
arena().makeAtomRef(Token),
252 *ConstraintsIt->second));
255 if (
auto DepsIt = FlowConditionDeps.find(Token);
256 DepsIt != FlowConditionDeps.end())
257 for (
Atom A : DepsIt->second)
258 Remaining.push_back(A);
263 llvm::DenseSet<dataflow::Atom> &Refs) {
285 llvm::DenseSet<dataflow::Atom> TargetTokens)
const {
293 llvm::DenseSet<dataflow::Atom> Dependencies =
294 collectDependencies(std::move(TargetTokens));
299 const Formula *Constraints = FlowConditionConstraints.lookup(
Token);
300 if (Constraints ==
nullptr)
304 if (
auto DepsIt = FlowConditionDeps.find(
Token);
305 DepsIt != FlowConditionDeps.end())
314 FlowConditionConstraints = std::move(LC.
TokenDefs);
318 FlowConditionDeps = std::move(LC.
TokenDeps);
322 llvm::raw_ostream &OS) {
324 for (
size_t i = 0; i < Atoms.size(); ++i) {
326 if (i + 1 < Atoms.size())
333 llvm::raw_ostream &OS) {
334 llvm::SetVector<const Formula *> Constraints;
335 Constraints.insert(&
arena().makeAtomRef(
Token));
336 addTransitiveFlowConditionConstraints(
Token, Constraints);
338 OS <<
"Flow condition token: " <<
Token <<
"\n";
340 llvm::SetVector<const Formula *> OriginalConstraints = Constraints;
342 if (!Constraints.empty()) {
343 OS <<
"Constraints:\n";
344 for (
const auto *Constraint : Constraints) {
345 Constraint->print(OS);
350 OS <<
"True atoms: ";
354 OS <<
"False atoms: ";
358 OS <<
"Equivalent atoms:\n";
363 OS <<
"\nFlow condition constraints before simplification:\n";
364 for (
const auto *Constraint : OriginalConstraints) {
365 Constraint->print(OS);
376 auto It = FunctionContexts.find(F);
377 if (It != FunctionContexts.end())
384 auto Result = FunctionContexts.insert({F, std::move(*ACFG)});
385 return &
Result.first->second;
396 if (
auto EC = llvm::sys::fs::create_directories(Dir))
397 llvm::errs() <<
"Failed to create log dir: " << EC.message() <<
"\n";
401 static std::atomic<unsigned> Counter = {0};
403 [Dir(Dir.str())]()
mutable -> std::unique_ptr<llvm::raw_ostream> {
405 llvm::sys::path::append(
File,
406 std::to_string(Counter.fetch_add(1)) +
".html");
408 auto OS = std::make_unique<llvm::raw_fd_ostream>(
File, EC);
410 llvm::errs() <<
"Failed to create log " <<
File <<
": " << EC.message()
412 return std::make_unique<llvm::raw_null_ostream>();
420 Solver &S, std::unique_ptr<Solver> &&OwnedSolver, Options Opts)
421 : S(S), OwnedSolver(
std::move(OwnedSolver)), A(
std::make_unique<Arena>()),
426 if (Opts.Log ==
nullptr) {
427 if (DataflowLog.getNumOccurrences() > 0) {
428 LogOwner = makeLoggerFromCommandLine();
429 this->Opts.Log = LogOwner.get();
432 this->Opts.Log = &Logger::null();
437DataflowAnalysisContext::~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)."))
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.