sgatev created this revision.
sgatev added reviewers: ymandel, xazax.hun, gribozavr2.
Herald added subscribers: tschuett, steakhal, rnkovacs.
Herald added a project: All.
sgatev requested review of this revision.
Herald added a project: clang.
Represent flow conditions as Token <=> Constraints biconditional clauses
in order to make joining of distinct values more efficient. For example,
joining distinct values while preserving flow condition information can
be implemented by adding the tokens of the flow conditions to the formula:
`makeOr(makeAnd(FC1, Val1), makeAnd(FC2, Val2))`.
Repository:
rG LLVM Github Monorepo
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->addFlowConditionConstraint(*FlowConditionToken,
+ *Other.FlowConditionToken);
+ DACtx->addFlowConditionDependency(*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,49 @@
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) {
+ 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) {
+ auto Res = VisitedTokens.insert(&Token);
+ if (!Res.second)
+ return;
+
+ Constraints.insert(FlowConditionFirstConjuncts[&Token]);
+ Constraints.insert(FlowConditionRemainingConjuncts[&Token].begin(),
+ FlowConditionRemainingConjuncts[&Token].end());
+
+ for (AtomicBoolValue *DepToken : FlowConditionDeps[&Token])
+ 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,29 @@
/// 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);
+
private:
+ void
+ addFlowConditionConstraints(AtomicBoolValue &Token,
+ llvm::DenseSet<BoolValue *> &Constraints,
+ llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
+
std::unique_ptr<Solver> S;
// Storage for the state of a program.
@@ -178,6 +201,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
