sammccall created this revision.
Herald added subscribers: martong, xazax.hun.
Herald added a reviewer: NoQ.
Herald added a project: All.
sammccall requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
And simplify formulas containing true/false
It's unclear to me how useful this is, it does make formulas more
conveniently self-contained now (we can usefully print them without
carrying around the "true/false" labels)
(while here, simplify !!X to X, too)
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D153485
Files:
clang/include/clang/Analysis/FlowSensitive/Arena.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/Formula.h
clang/lib/Analysis/FlowSensitive/Arena.cpp
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/lib/Analysis/FlowSensitive/Formula.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
@@ -2853,14 +2853,14 @@
ASSERT_THAT(FooDecl, NotNull());
const auto *FooVal =
- dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*FooDecl));
+ dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
ASSERT_THAT(FooVal, NotNull());
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
ASSERT_THAT(BarDecl, NotNull());
const auto *BarVal =
- dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*BarDecl));
+ dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
ASSERT_THAT(BarVal, NotNull());
EXPECT_EQ(FooVal, &Env.getBoolLiteralValue(true));
@@ -3038,7 +3038,7 @@
ASSERT_THAT(FooDecl, NotNull());
const auto *FooVal =
- dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*FooDecl));
+ dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
ASSERT_THAT(FooVal, NotNull());
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
Index: clang/unittests/Analysis/FlowSensitive/TestingSupport.h
===================================================================
--- clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -418,6 +418,11 @@
return &Formula::create(A, Formula::AtomRef, {}, NextAtom++);
}
+ // Creates a reference to a literal boolean value.
+ const Formula *literal(bool B) {
+ return &Formula::create(A, Formula::Literal, {}, B);
+ }
+
// Creates a boolean conjunction value.
const Formula *conj(const Formula *LeftSubVal, const Formula *RightSubVal) {
return make(Formula::And, {LeftSubVal, RightSubVal});
Index: clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -32,6 +32,12 @@
EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
+TEST(BoolValueDebugStringTest, Literal) {
+ ConstraintContext Ctx;
+ EXPECT_EQ("true", llvm::to_string(*Ctx.literal(true)));
+ EXPECT_EQ("false", llvm::to_string(*Ctx.literal(false)));
+}
+
TEST(BoolValueDebugStringTest, Negation) {
ConstraintContext Ctx;
auto B = Ctx.neg(Ctx.atom());
@@ -95,22 +101,22 @@
TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
ConstraintContext Ctx;
- auto True = Ctx.atom();
- auto False = Ctx.atom();
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
auto Delegate = [&](llvm::raw_ostream &OS, const Formula &F) {
- if (&F == True) {
- OS << "True";
+ if (&F == X) {
+ OS << "X";
return true;
}
- if (&F == False) {
- OS << "False";
+ if (&F == Y) {
+ OS << "Y";
return true;
}
return false;
};
- auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom()));
+ auto B = Ctx.disj(Ctx.conj(Y, Ctx.atom()), Ctx.disj(X, Ctx.atom()));
- auto Expected = R"(((False & V2) | (True | V3)))";
+ auto Expected = R"(((Y & V2) | (X | V3)))";
std::string Actual;
llvm::raw_string_ostream OS(Actual);
B->print(OS, Delegate);
Index: clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
@@ -31,12 +31,6 @@
EXPECT_NE(&X, &Y);
}
-TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
- auto &X = A.makeAtomRef(A.makeAtom());
- auto &XAndX = A.makeAnd(X, X);
- EXPECT_EQ(&XAndX, &X);
-}
-
TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
auto &X = A.makeAtomRef(A.makeAtom());
auto &Y = A.makeAtomRef(A.makeAtom());
@@ -52,12 +46,6 @@
EXPECT_NE(&XAndY1, &XAndZ);
}
-TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
- auto &X = A.makeAtomRef(A.makeAtom());
- auto &XOrX = A.makeOr(X, X);
- EXPECT_EQ(&XOrX, &X);
-}
-
TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
auto &X = A.makeAtomRef(A.makeAtom());
auto &Y = A.makeAtomRef(A.makeAtom());
@@ -83,12 +71,6 @@
EXPECT_NE(&NotX1, &NotY);
}
-TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) {
- auto &X = A.makeAtomRef(A.makeAtom());
- auto &XImpliesX = A.makeImplies(X, X);
- EXPECT_EQ(&XImpliesX, &A.makeLiteral(true));
-}
-
TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
auto &X = A.makeAtomRef(A.makeAtom());
auto &Y = A.makeAtomRef(A.makeAtom());
@@ -104,12 +86,6 @@
EXPECT_NE(&XImpliesY1, &XImpliesZ);
}
-TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
- auto &X = A.makeAtomRef(A.makeAtom());
- auto &XIffX = A.makeEquals(X, X);
- EXPECT_EQ(&XIffX, &A.makeLiteral(true));
-}
-
TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
auto &X = A.makeAtomRef(A.makeAtom());
auto &Y = A.makeAtomRef(A.makeAtom());
@@ -137,5 +113,36 @@
EXPECT_EQ(&B1.formula(), &F1);
}
+TEST_F(ArenaTest, IdentitySimplification) {
+ auto &X = A.makeAtomRef(A.makeAtom());
+
+ EXPECT_EQ(&X, &A.makeAnd(X, X));
+ EXPECT_EQ(&X, &A.makeOr(X, X));
+ EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, X));
+ EXPECT_EQ(&A.makeLiteral(true), &A.makeEquals(X, X));
+ EXPECT_EQ(&X, &A.makeNot(A.makeNot(X)));
+}
+
+TEST_F(ArenaTest, LiteralSimplification) {
+ auto &X = A.makeAtomRef(A.makeAtom());
+
+ EXPECT_EQ(&X, &A.makeAnd(X, A.makeLiteral(true)));
+ EXPECT_EQ(&A.makeLiteral(false), &A.makeAnd(X, A.makeLiteral(false)));
+
+ EXPECT_EQ(&A.makeLiteral(true), &A.makeOr(X, A.makeLiteral(true)));
+ EXPECT_EQ(&X, &A.makeOr(X, A.makeLiteral(false)));
+
+ EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, A.makeLiteral(true)));
+ EXPECT_EQ(&A.makeNot(X), &A.makeImplies(X, A.makeLiteral(false)));
+ EXPECT_EQ(&X, &A.makeImplies(A.makeLiteral(true), X));
+ EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(A.makeLiteral(false), X));
+
+ EXPECT_EQ(&X, &A.makeEquals(X, A.makeLiteral(true)));
+ EXPECT_EQ(&A.makeNot(X), &A.makeEquals(X, A.makeLiteral(false)));
+
+ EXPECT_EQ(&A.makeLiteral(false), &A.makeNot(A.makeLiteral(true)));
+ EXPECT_EQ(&A.makeLiteral(true), &A.makeNot(A.makeLiteral(false)));
+}
+
} // namespace
} // namespace clang::dataflow
Index: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -240,6 +240,9 @@
switch (Val->kind()) {
case Formula::AtomRef:
break;
+ case Formula::Literal:
+ Form.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]);
Index: clang/lib/Analysis/FlowSensitive/Formula.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/Formula.cpp
+++ clang/lib/Analysis/FlowSensitive/Formula.cpp
@@ -16,8 +16,9 @@
namespace clang::dataflow {
-Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
- ArrayRef<const Formula *> Operands, unsigned Value) {
+const 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);
@@ -34,6 +35,7 @@
static llvm::StringLiteral sigil(Formula::Kind K) {
switch (K) {
case Formula::AtomRef:
+ case Formula::Literal:
return "";
case Formula::Not:
return "!";
@@ -56,7 +58,16 @@
switch (numOperands(kind())) {
case 0:
- OS << atom();
+ switch (kind()) {
+ case AtomRef:
+ OS << atom();
+ break;
+ case Literal:
+ OS << (literal() ? "true" : "false");
+ break;
+ default:
+ llvm_unreachable("unhandled formula kind");
+ }
break;
case 1:
OS << sigil(kind());
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -127,8 +127,6 @@
Solver::Result DataflowAnalysisContext::querySolver(
llvm::DenseSet<const Formula *> Constraints) {
- Constraints.insert(&arena().makeLiteral(true));
- Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
return S->solve(Constraints);
}
@@ -195,26 +193,11 @@
llvm::DenseSet<Atom> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
- // TODO: have formulas know about true/false directly instead
- auto &True = arena().makeLiteral(true);
- auto &False = arena().makeLiteral(false);
- auto Delegate = [&](llvm::raw_ostream &OS, const Formula &F) {
- if (&F == &True) {
- OS << "True";
- return true;
- }
- if (&F == &False) {
- OS << "False";
- return true;
- }
- return false;
- };
-
std::vector<std::string> Lines;
for (const auto *Constraint : Constraints) {
Lines.emplace_back();
llvm::raw_string_ostream LineOS(Lines.back());
- Constraint->print(LineOS, Delegate);
+ Constraint->print(LineOS);
}
llvm::sort(Lines);
for (const auto &Line : Lines)
Index: clang/lib/Analysis/FlowSensitive/Arena.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -19,63 +19,83 @@
return Res;
}
-const Formula &Arena::makeAtomRef(Atom A) {
- auto [It, Inserted] = AtomRefs.try_emplace(A);
+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));
if (Inserted)
- It->second =
- &Formula::create(Alloc, Formula::AtomRef, {}, static_cast<unsigned>(A));
+ It->second = Compute();
return *It->second;
}
-const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
- if (&LHS == &RHS)
- return LHS;
+const Formula &Arena::makeAtomRef(Atom A) {
+ return cached(AtomRefs, A, [&] {
+ return &Formula::create(Alloc, Formula::AtomRef, {},
+ static_cast<unsigned>(A));
+ });
+}
- 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::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});
+ });
}
const Formula &Arena::makeOr(const Formula &LHS, const Formula &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;
+ 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});
+ });
}
const Formula &Arena::makeNot(const Formula &Val) {
- auto [It, Inserted] = Nots.try_emplace(&Val, nullptr);
- if (Inserted)
- It->second = &Formula::create(Alloc, Formula::Not, {&Val});
- return *It->second;
+ 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});
+ });
}
const Formula &Arena::makeImplies(const Formula &LHS, const Formula &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;
+ 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});
+ });
}
const Formula &Arena::makeEquals(const Formula &LHS, const Formula &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;
+ 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});
+ });
}
IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
Index: clang/include/clang/Analysis/FlowSensitive/Formula.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/Formula.h
+++ clang/include/clang/Analysis/FlowSensitive/Formula.h
@@ -50,7 +50,8 @@
/// A reference to an atomic boolean variable.
/// We name these e.g. "V3", where 3 == atom identity == value().
AtomRef,
- // FIXME: add const true/false rather than modeling them as variables
+ /// Constant true or false.
+ Literal,
Not, /// True if its only operand is false
@@ -67,6 +68,11 @@
return static_cast<Atom>(Value);
}
+ bool literal() const {
+ assert(kind() == Literal);
+ return static_cast<bool>(Value);
+ }
+
ArrayRef<const Formula *> operands() const {
return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
numOperands(kind()));
@@ -77,9 +83,9 @@
void print(llvm::raw_ostream &OS,
llvm::function_ref<DelegatePrinter> = nullptr) const;
- static Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
- ArrayRef<const Formula *> Operands,
- unsigned Value = 0);
+ static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
+ ArrayRef<const Formula *> Operands,
+ unsigned Value = 0);
private:
Formula() = default;
@@ -89,6 +95,7 @@
static unsigned numOperands(Kind K) {
switch (K) {
case AtomRef:
+ case Literal:
return 0;
case Not:
return 1;
Index: clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -456,9 +456,8 @@
/// Returns a symbolic boolean value that models a boolean literal equal to
/// `Value`
- AtomicBoolValue &getBoolLiteralValue(bool Value) const {
- return cast<AtomicBoolValue>(
- arena().makeBoolValue(arena().makeLiteral(Value)));
+ BoolValue &getBoolLiteralValue(bool Value) const {
+ return arena().makeBoolValue(arena().makeLiteral(Value));
}
/// Returns an atomic boolean value.
Index: clang/include/clang/Analysis/FlowSensitive/Arena.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/Arena.h
+++ clang/include/clang/Analysis/FlowSensitive/Arena.h
@@ -19,7 +19,9 @@
/// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`.
class Arena {
public:
- Arena() : True(makeAtom()), False(makeAtom()) {}
+ Arena()
+ : True(Formula::create(Alloc, Formula::Literal, {}, 1)),
+ False(Formula::create(Alloc, Formula::Literal, {}, 0)) {}
Arena(const Arena &) = delete;
Arena &operator=(const Arena &) = delete;
@@ -106,9 +108,7 @@
const Formula &makeAtomRef(Atom A);
/// Returns a formula for a literal true/false.
- const Formula &makeLiteral(bool Value) {
- return makeAtomRef(Value ? True : False);
- }
+ const Formula &makeLiteral(bool Value) { return Value ? True : False; }
/// Returns a new atomic boolean variable, distinct from any other.
Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
@@ -140,7 +140,7 @@
llvm::DenseMap<const Formula *, BoolValue *> FormulaValues;
unsigned NextAtom = 0;
- Atom True, False;
+ const Formula &True, &False;
};
} // namespace clang::dataflow
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
