sgatev updated this revision to Diff 424930.
sgatev added a comment.
Mark methods as const.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D124395/new/
https://reviews.llvm.org/D124395
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
Index: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -76,33 +76,14 @@
Environment &MergedEnv,
Environment::ValueModel &Model) {
// Join distinct boolean values preserving information about the constraints
- // in the respective path conditions. Note: this construction can, in
- // principle, result in exponential growth in the size of boolean values.
- // Potential optimizations may be worth considering. For example, represent
- // the flow condition of each environment using a bool atom and store, in
- // `DataflowAnalysisContext`, a mapping of bi-conditionals between flow
- // condition atoms and flow condition constraints. Something like:
- // \code
- // FC1 <=> C1 ^ C2
- // FC2 <=> C2 ^ C3 ^ C4
- // FC3 <=> (FC1 v FC2) ^ C5
- // \code
- // Then, we can track dependencies between flow conditions (e.g. above `FC3`
- // depends on `FC1` and `FC2`) and modify `flowConditionImplies` to construct
- // a formula that includes the bi-conditionals for all flow condition atoms in
- // the transitive set, before invoking the solver.
+ // in the respective path conditions.
//
// FIXME: Does not work for backedges, since the two (or more) paths will not
// have mutually exclusive conditions.
if (auto *Expr1 = dyn_cast<BoolValue>(Val1)) {
- for (BoolValue *Constraint : Env1.getFlowConditionConstraints()) {
- Expr1 = &MergedEnv.makeAnd(*Expr1, *Constraint);
- }
auto *Expr2 = cast<BoolValue>(Val2);
- for (BoolValue *Constraint : Env2.getFlowConditionConstraints()) {
- Expr2 = &MergedEnv.makeAnd(*Expr2, *Constraint);
- }
- return &MergedEnv.makeOr(*Expr1, *Expr2);
+ return &Env1.makeOr(Env1.makeAnd(Env1.getFlowConditionToken(), *Expr1),
+ Env1.makeAnd(Env2.getFlowConditionToken(), *Expr2));
}
// FIXME: Consider destroying `MergedValue` immediately if `ValueModel::merge`
@@ -156,63 +137,6 @@
}
}
-/// Returns constraints that represent the disjunction of `Constraints1` and
-/// `Constraints2`.
-///
-/// Requirements:
-///
-/// The elements of `Constraints1` and `Constraints2` must not be null.
-llvm::DenseSet<BoolValue *>
-joinConstraints(DataflowAnalysisContext *Context,
- const llvm::DenseSet<BoolValue *> &Constraints1,
- const llvm::DenseSet<BoolValue *> &Constraints2) {
- // `(X ^ Y) v (X ^ Z)` is logically equivalent to `X ^ (Y v Z)`. Therefore, to
- // avoid unnecessarily expanding the resulting set of constraints, we will add
- // all common constraints of `Constraints1` and `Constraints2` directly and
- // add a disjunction of the constraints that are not common.
-
- llvm::DenseSet<BoolValue *> JoinedConstraints;
-
- if (Constraints1.empty() || Constraints2.empty()) {
- // Disjunction of empty set and non-empty set is represented as empty set.
- return JoinedConstraints;
- }
-
- BoolValue *Val1 = nullptr;
- for (BoolValue *Constraint : Constraints1) {
- if (Constraints2.contains(Constraint)) {
- // Add common constraints directly to `JoinedConstraints`.
- JoinedConstraints.insert(Constraint);
- } else if (Val1 == nullptr) {
- Val1 = Constraint;
- } else {
- Val1 = &Context->getOrCreateConjunctionValue(*Val1, *Constraint);
- }
- }
-
- BoolValue *Val2 = nullptr;
- for (BoolValue *Constraint : Constraints2) {
- // Common constraints are added to `JoinedConstraints` above.
- if (Constraints1.contains(Constraint)) {
- continue;
- }
- if (Val2 == nullptr) {
- Val2 = Constraint;
- } else {
- Val2 = &Context->getOrCreateConjunctionValue(*Val2, *Constraint);
- }
- }
-
- // An empty set of constraints (represented as a null value) is interpreted as
- // `true` and `true v X` is logically equivalent to `true` so we need to add a
- // constraint only if both `Val1` and `Val2` are not null.
- if (Val1 != nullptr && Val2 != nullptr)
- JoinedConstraints.insert(
- &Context->getOrCreateDisjunctionValue(*Val1, *Val2));
-
- return JoinedConstraints;
-}
-
static void
getFieldsFromClassHierarchy(QualType Type, bool IgnorePrivateFields,
llvm::DenseSet<const FieldDecl *> &Fields) {
@@ -249,6 +173,26 @@
return Fields;
}
+Environment::Environment(DataflowAnalysisContext &DACtx)
+ : DACtx(&DACtx), FlowConditionToken(&DACtx.makeFlowConditionToken()) {}
+
+Environment::Environment(const Environment &Other)
+ : DACtx(Other.DACtx), DeclToLoc(Other.DeclToLoc),
+ ExprToLoc(Other.ExprToLoc), LocToVal(Other.LocToVal),
+ MemberLocToStruct(Other.MemberLocToStruct) {
+ FlowConditionToken = &DACtx->makeFlowConditionToken();
+ DACtx->addFlowConditionDependency(*FlowConditionToken,
+ *Other.FlowConditionToken);
+ DACtx->addFlowConditionConstraint(*FlowConditionToken,
+ *Other.FlowConditionToken);
+}
+
+Environment &Environment::operator=(const Environment &Other) {
+ Environment Copy(Other);
+ *this = std::move(Copy);
+ return *this;
+}
+
Environment::Environment(DataflowAnalysisContext &DACtx,
const DeclContext &DeclCtx)
: Environment(DACtx) {
@@ -333,8 +277,14 @@
Effect = LatticeJoinEffect::Changed;
// FIXME: set `Effect` as needed.
- JoinedEnv.FlowConditionConstraints = joinConstraints(
- DACtx, FlowConditionConstraints, Other.FlowConditionConstraints);
+ JoinedEnv.FlowConditionToken = &DACtx->makeFlowConditionToken();
+ DACtx->addFlowConditionDependency(*JoinedEnv.FlowConditionToken,
+ *FlowConditionToken);
+ DACtx->addFlowConditionDependency(*JoinedEnv.FlowConditionToken,
+ *Other.FlowConditionToken);
+ DACtx->addFlowConditionConstraint(
+ *JoinedEnv.FlowConditionToken,
+ makeOr(*FlowConditionToken, *Other.FlowConditionToken));
for (auto &Entry : LocToVal) {
const StorageLocation *Loc = Entry.first;
@@ -600,7 +550,7 @@
}
void Environment::addToFlowCondition(BoolValue &Val) {
- FlowConditionConstraints.insert(&Val);
+ DACtx->addFlowConditionConstraint(*FlowConditionToken, Val);
}
bool Environment::flowConditionImplies(BoolValue &Val) const {
@@ -609,11 +559,13 @@
// reducing the problem to satisfiability checking. In other words, we attempt
// to show that assuming `Val` is false makes the constraints induced by the
// flow condition unsatisfiable.
- llvm::DenseSet<BoolValue *> Constraints = {
- &makeNot(Val), &getBoolLiteralValue(true),
- &makeNot(getBoolLiteralValue(false))};
- Constraints.insert(FlowConditionConstraints.begin(),
- FlowConditionConstraints.end());
+
+ llvm::DenseSet<BoolValue *> Constraints =
+ DACtx->getFlowConditionConstraints(*FlowConditionToken);
+ Constraints.insert(&makeNot(Val));
+ Constraints.insert(&getBoolLiteralValue(true));
+ Constraints.insert(&makeNot(getBoolLiteralValue(false)));
+
return DACtx->getSolver().solve(std::move(Constraints)) ==
Solver::Result::Unsatisfiable;
}
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -64,5 +64,57 @@
return *Res.first->second;
}
+AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() {
+ AtomicBoolValue &Token = createAtomicBoolValue();
+ FlowConditionRemainingConjuncts[&Token] = {};
+ FlowConditionFirstConjuncts[&Token] = &Token;
+ return Token;
+}
+
+void DataflowAnalysisContext::addFlowConditionConstraint(
+ AtomicBoolValue &Token, BoolValue &Constraint) {
+ FlowConditionRemainingConjuncts[&Token].insert(&getOrCreateDisjunctionValue(
+ Constraint, getOrCreateNegationValue(Token)));
+ FlowConditionFirstConjuncts[&Token] =
+ &getOrCreateDisjunctionValue(*FlowConditionFirstConjuncts[&Token],
+ getOrCreateNegationValue(Constraint));
+}
+
+void DataflowAnalysisContext::addFlowConditionDependency(
+ AtomicBoolValue &Token, AtomicBoolValue &DepToken) {
+ FlowConditionDeps[&Token].insert(&DepToken);
+}
+
+llvm::DenseSet<BoolValue *>
+DataflowAnalysisContext::getFlowConditionConstraints(
+ AtomicBoolValue &Token) const {
+ llvm::DenseSet<BoolValue *> Constraints = {&Token};
+ llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+ addFlowConditionConstraints(Token, Constraints, VisitedTokens);
+ return Constraints;
+}
+
+void DataflowAnalysisContext::addFlowConditionConstraints(
+ AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
+ llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const {
+ auto Res = VisitedTokens.insert(&Token);
+ if (!Res.second)
+ return;
+
+ auto FirstConjunctIT = FlowConditionFirstConjuncts.find(&Token);
+ if (FirstConjunctIT != FlowConditionFirstConjuncts.end())
+ Constraints.insert(FirstConjunctIT->second);
+ auto RemainingConjunctsIT = FlowConditionRemainingConjuncts.find(&Token);
+ if (RemainingConjunctsIT != FlowConditionRemainingConjuncts.end())
+ Constraints.insert(RemainingConjunctsIT->second.begin(),
+ RemainingConjunctsIT->second.end());
+
+ auto DepsIT = FlowConditionDeps.find(&Token);
+ if (DepsIT != FlowConditionDeps.end()) {
+ for (AtomicBoolValue *DepToken : DepsIT->second)
+ addFlowConditionConstraints(*DepToken, Constraints, VisitedTokens);
+ }
+}
+
} // namespace dataflow
} // namespace clang
Index: clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -111,7 +111,13 @@
/// Creates an environment that uses `DACtx` to store objects that encompass
/// the state of a program.
- explicit Environment(DataflowAnalysisContext &DACtx) : DACtx(&DACtx) {}
+ explicit Environment(DataflowAnalysisContext &DACtx);
+
+ Environment(const Environment &Other);
+ Environment &operator=(const Environment &Other);
+
+ Environment(Environment &&Other) = default;
+ Environment &operator=(Environment &&Other) = default;
/// Creates an environment that uses `DACtx` to store objects that encompass
/// the state of a program.
@@ -297,9 +303,8 @@
: makeAnd(makeImplication(LHS, RHS), makeImplication(RHS, LHS));
}
- const llvm::DenseSet<BoolValue *> &getFlowConditionConstraints() const {
- return FlowConditionConstraints;
- }
+ /// Returns the token that identifies the flow condition of the environment.
+ AtomicBoolValue &getFlowConditionToken() const { return *FlowConditionToken; }
/// Adds `Val` to the set of clauses that constitute the flow condition.
void addToFlowCondition(BoolValue &Val);
@@ -345,7 +350,7 @@
std::pair<StructValue *, const ValueDecl *>>
MemberLocToStruct;
- llvm::DenseSet<BoolValue *> FlowConditionConstraints;
+ AtomicBoolValue *FlowConditionToken;
};
} // namespace dataflow
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -21,6 +21,7 @@
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/DenseSet.h"
#include <cassert>
#include <memory>
#include <type_traits>
@@ -151,7 +152,28 @@
/// calls with the same argument will return the same result.
BoolValue &getOrCreateNegationValue(BoolValue &Val);
+ /// Returns a fresh flow condition token.
+ AtomicBoolValue &makeFlowConditionToken();
+
+ /// Adds `Constraint` to the flow condition indentified by `Token`.
+ void addFlowConditionConstraint(AtomicBoolValue &Token,
+ BoolValue &Constraint);
+
+ /// Adds the flow condition identified by `DepToken` as a dependency of the
+ /// flow condition identified by `Token`.
+ void addFlowConditionDependency(AtomicBoolValue &Token,
+ AtomicBoolValue &DepToken);
+
+ /// Returns all constraints that were added to the flow condition identified
+ /// by `Token`.
+ llvm::DenseSet<BoolValue *>
+ getFlowConditionConstraints(AtomicBoolValue &Token) const;
+
private:
+ void addFlowConditionConstraints(
+ AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
+ llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const;
+
std::unique_ptr<Solver> S;
// Storage for the state of a program.
@@ -178,6 +200,24 @@
llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
DisjunctionVals;
llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
+
+ // Flow conditions are represented as `FC <=> (C1 ^ C2 ^ ...)` clauses where
+ // `FC` is a flow condition token (an atomic boolean) and `Ci`s are a set of
+ // constraints.
+ //
+ // Internally, a flow condition clause is represented as conjuncts of the form
+ // `(FC v !C1 v !C2 v ...) ^ (C1 v !FC) ^ (C2 v !FC) ^ ...`. The first conjuct
+ // is stored in the `FlowConditionFirstConjuncts` map. The set of remaining
+ // conjuncts are stored in the `FlowConditionRemainingConjuncts` map.
+ //
+ // Flow conditions can depend on other flow conditions (constraints can refer
+ // to flow condition tokens). The graph of flow condition dependencies is
+ // stored in the `FlowConditionDeps` map.
+ llvm::DenseMap<AtomicBoolValue *, llvm::DenseSet<AtomicBoolValue *>>
+ FlowConditionDeps;
+ llvm::DenseMap<AtomicBoolValue *, BoolValue *> FlowConditionFirstConjuncts;
+ llvm::DenseMap<AtomicBoolValue *, llvm::DenseSet<BoolValue *>>
+ FlowConditionRemainingConjuncts;
};
} // namespace dataflow
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
