aboutsummaryrefslogtreecommitdiff
path: root/clang/lib/Analysis/FlowSensitive
diff options
context:
space:
mode:
Diffstat (limited to 'clang/lib/Analysis/FlowSensitive')
-rw-r--r--clang/lib/Analysis/FlowSensitive/Arena.cpp100
-rw-r--r--clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp9
-rw-r--r--clang/lib/Analysis/FlowSensitive/Formula.cpp17
-rw-r--r--clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp3
4 files changed, 51 insertions, 78 deletions
diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp
index 81137e8..b043a52 100644
--- a/clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -22,83 +22,63 @@ canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
return Res;
}
-template <class Key, class ComputeFunc>
-const Formula &cached(llvm::DenseMap<Key, const Formula *> &Cache, Key K,
- ComputeFunc &&Compute) {
- auto [It, Inserted] = Cache.try_emplace(std::forward<Key>(K));
+const Formula &Arena::makeAtomRef(Atom A) {
+ auto [It, Inserted] = AtomRefs.try_emplace(A);
if (Inserted)
- It->second = Compute();
+ It->second =
+ &Formula::create(Alloc, Formula::AtomRef, {}, static_cast<unsigned>(A));
return *It->second;
}
-const Formula &Arena::makeAtomRef(Atom A) {
- return cached(AtomRefs, A, [&] {
- return &Formula::create(Alloc, Formula::AtomRef, {},
- static_cast<unsigned>(A));
- });
-}
-
const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
- return cached(Ands, canonicalFormulaPair(LHS, RHS), [&] {
- if (&LHS == &RHS)
- return &LHS;
- if (LHS.kind() == Formula::Literal)
- return LHS.literal() ? &RHS : &LHS;
- if (RHS.kind() == Formula::Literal)
- return RHS.literal() ? &LHS : &RHS;
-
- return &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
- });
+ if (&LHS == &RHS)
+ return LHS;
+
+ auto [It, Inserted] =
+ Ands.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+ if (Inserted)
+ It->second = &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
+ return *It->second;
}
const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
- return cached(Ors, canonicalFormulaPair(LHS, RHS), [&] {
- if (&LHS == &RHS)
- return &LHS;
- if (LHS.kind() == Formula::Literal)
- return LHS.literal() ? &LHS : &RHS;
- if (RHS.kind() == Formula::Literal)
- return RHS.literal() ? &RHS : &LHS;
-
- return &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
- });
+ if (&LHS == &RHS)
+ return LHS;
+
+ auto [It, Inserted] =
+ Ors.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+ if (Inserted)
+ It->second = &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
+ return *It->second;
}
const Formula &Arena::makeNot(const Formula &Val) {
- return cached(Nots, &Val, [&] {
- if (Val.kind() == Formula::Not)
- return Val.operands()[0];
- if (Val.kind() == Formula::Literal)
- return &makeLiteral(!Val.literal());
-
- return &Formula::create(Alloc, Formula::Not, {&Val});
- });
+ auto [It, Inserted] = Nots.try_emplace(&Val, nullptr);
+ if (Inserted)
+ It->second = &Formula::create(Alloc, Formula::Not, {&Val});
+ return *It->second;
}
const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) {
- return cached(Implies, std::make_pair(&LHS, &RHS), [&] {
- if (&LHS == &RHS)
- return &makeLiteral(true);
- if (LHS.kind() == Formula::Literal)
- return LHS.literal() ? &RHS : &makeLiteral(true);
- if (RHS.kind() == Formula::Literal)
- return RHS.literal() ? &RHS : &makeNot(LHS);
-
- return &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
- });
+ if (&LHS == &RHS)
+ return makeLiteral(true);
+
+ auto [It, Inserted] =
+ Implies.try_emplace(std::make_pair(&LHS, &RHS), nullptr);
+ if (Inserted)
+ It->second = &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
+ return *It->second;
}
const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
- return cached(Equals, canonicalFormulaPair(LHS, RHS), [&] {
- if (&LHS == &RHS)
- return &makeLiteral(true);
- if (LHS.kind() == Formula::Literal)
- return LHS.literal() ? &RHS : &makeNot(RHS);
- if (RHS.kind() == Formula::Literal)
- return RHS.literal() ? &LHS : &makeNot(LHS);
-
- return &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
- });
+ if (&LHS == &RHS)
+ return makeLiteral(true);
+
+ auto [It, Inserted] =
+ Equals.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+ if (Inserted)
+ It->second = &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
+ return *It->second;
}
IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 28a8595..e81048c 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -141,6 +141,8 @@ DataflowAnalysisContext::joinFlowConditions(Atom FirstToken,
Solver::Result DataflowAnalysisContext::querySolver(
llvm::SetVector<const Formula *> Constraints) {
+ Constraints.insert(&arena().makeLiteral(true));
+ Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
return S->solve(Constraints.getArrayRef());
}
@@ -211,8 +213,13 @@ void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
Constraints.insert(&arena().makeAtomRef(Token));
addTransitiveFlowConditionConstraints(Token, Constraints);
+ // TODO: have formulas know about true/false directly instead
+ Atom True = arena().makeLiteral(true).getAtom();
+ Atom False = arena().makeLiteral(false).getAtom();
+ Formula::AtomNames Names = {{False, "false"}, {True, "true"}};
+
for (const auto *Constraint : Constraints) {
- Constraint->print(OS);
+ Constraint->print(OS, &Names);
OS << "\n";
}
}
diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp
index ef7d23f..6d22efc 100644
--- a/clang/lib/Analysis/FlowSensitive/Formula.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Formula.cpp
@@ -17,9 +17,8 @@
namespace clang::dataflow {
-const Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
- ArrayRef<const Formula *> Operands,
- unsigned Value) {
+Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
+ ArrayRef<const Formula *> Operands, unsigned Value) {
assert(Operands.size() == numOperands(K));
if (Value != 0) // Currently, formulas have values or operands, not both.
assert(numOperands(K) == 0);
@@ -39,7 +38,6 @@ const Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
static llvm::StringLiteral sigil(Formula::Kind K) {
switch (K) {
case Formula::AtomRef:
- case Formula::Literal:
return "";
case Formula::Not:
return "!";
@@ -64,16 +62,7 @@ void Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const {
switch (numOperands(kind())) {
case 0:
- switch (kind()) {
- case AtomRef:
- OS << getAtom();
- break;
- case Literal:
- OS << (literal() ? "true" : "false");
- break;
- default:
- llvm_unreachable("unhandled formula kind");
- }
+ OS << getAtom();
break;
case 1:
OS << sigil(kind());
diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
index 3ef3637..ab3a810 100644
--- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -322,9 +322,6 @@ CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
switch (Val->kind()) {
case Formula::AtomRef:
break;
- case Formula::Literal:
- CNF.addClause(Val->literal() ? posLit(Var) : negLit(Var));
- break;
case Formula::And: {
const Variable LHS = GetVar(Val->operands()[0]);
const Variable RHS = GetVar(Val->operands()[1]);
generated by cgit v1.1 at 2025-08-03 05:13:19 +0000