Skip to content

Commit 36bd5bd

Browse files
sam-mccallsam-mccall
committed
[dataflow] use true/false literals in formulas, rather than variables
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) Differential Revision: https://reviews.llvm.org/D153485
1 parent 17649a7 commit 36bd5bd

File tree

11 files changed

+147
-98
lines changed

11 files changed

+147
-98
lines changed

‎clang/include/clang/Analysis/FlowSensitive/Arena.h‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,9 @@ namespace clang::dataflow {
2020
/// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`.
2121
class Arena {
2222
public:
23-
Arena() : True(makeAtom()), False(makeAtom()) {}
23+
Arena()
24+
: True(Formula::create(Alloc, Formula::Literal, {}, 1)),
25+
False(Formula::create(Alloc, Formula::Literal, {}, 0)) {}
2426
Arena(const Arena &) = delete;
2527
Arena &operator=(const Arena &) = delete;
2628

@@ -106,9 +108,7 @@ class Arena {
106108
const Formula &makeAtomRef(Atom A);
107109

108110
/// Returns a formula for a literal true/false.
109-
const Formula &makeLiteral(bool Value) {
110-
return makeAtomRef(Value ? True : False);
111-
}
111+
const Formula &makeLiteral(bool Value) { return Value ? True : False; }
112112

113113
// Parses a formula from its textual representation.
114114
// This may refer to atoms that were not produced by makeAtom() yet!
@@ -144,7 +144,7 @@ class Arena {
144144
llvm::DenseMap<const Formula *, BoolValue *> FormulaValues;
145145
unsigned NextAtom = 0;
146146

147-
Atom True, False;
147+
const Formula &True, &False;
148148
};
149149

150150
} // namespace clang::dataflow

‎clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -466,9 +466,8 @@ class Environment {
466466

467467
/// Returns a symbolic boolean value that models a boolean literal equal to
468468
/// `Value`
469-
AtomicBoolValue &getBoolLiteralValue(bool Value) const {
470-
return cast<AtomicBoolValue>(
471-
arena().makeBoolValue(arena().makeLiteral(Value)));
469+
BoolValue &getBoolLiteralValue(bool Value) const {
470+
return arena().makeBoolValue(arena().makeLiteral(Value));
472471
}
473472

474473
/// Returns an atomic boolean value.

‎clang/include/clang/Analysis/FlowSensitive/Formula.h‎

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,8 @@ class alignas(const Formula *) Formula {
5353
/// A reference to an atomic boolean variable.
5454
/// We name these e.g. "V3", where 3 == atom identity == Value.
5555
AtomRef,
56-
// FIXME: add const true/false rather than modeling them as variables
56+
/// Constant true or false.
57+
Literal,
5758

5859
Not, /// True if its only operand is false
5960

@@ -70,6 +71,11 @@ class alignas(const Formula *) Formula {
7071
return static_cast<Atom>(Value);
7172
}
7273

74+
bool literal() const {
75+
assert(kind() == Literal);
76+
return static_cast<bool>(Value);
77+
}
78+
7379
ArrayRef<const Formula *> operands() const {
7480
return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
7581
numOperands(kind()));
@@ -82,9 +88,9 @@ class alignas(const Formula *) Formula {
8288
void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
8389

8490
// Allocate Formulas using Arena rather than calling this function directly.
85-
static Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
86-
ArrayRef<const Formula *> Operands,
87-
unsigned Value = 0);
91+
static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
92+
ArrayRef<const Formula *> Operands,
93+
unsigned Value = 0);
8894

8995
private:
9096
Formula() = default;
@@ -94,6 +100,7 @@ class alignas(const Formula *) Formula {
94100
static unsigned numOperands(Kind K) {
95101
switch (K) {
96102
case AtomRef:
103+
case Literal:
97104
return 0;
98105
case Not:
99106
return 1;

‎clang/lib/Analysis/FlowSensitive/Arena.cpp‎

Lines changed: 60 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -22,63 +22,83 @@ canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
2222
return Res;
2323
}
2424

25-
const Formula &Arena::makeAtomRef(Atom A) {
26-
auto [It, Inserted] = AtomRefs.try_emplace(A);
25+
template <class Key, class ComputeFunc>
26+
const Formula &cached(llvm::DenseMap<Key, const Formula *> &Cache, Key K,
27+
ComputeFunc &&Compute) {
28+
auto [It, Inserted] = Cache.try_emplace(std::forward<Key>(K));
2729
if (Inserted)
28-
It->second =
29-
&Formula::create(Alloc, Formula::AtomRef, {}, static_cast<unsigned>(A));
30+
It->second = Compute();
3031
return *It->second;
3132
}
3233

33-
const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
34-
if (&LHS == &RHS)
35-
return LHS;
34+
const Formula &Arena::makeAtomRef(Atom A) {
35+
return cached(AtomRefs, A, [&] {
36+
return &Formula::create(Alloc, Formula::AtomRef, {},
37+
static_cast<unsigned>(A));
38+
});
39+
}
3640

37-
auto [It, Inserted] =
38-
Ands.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
39-
if (Inserted)
40-
It->second = &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
41-
return *It->second;
41+
const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
42+
return cached(Ands, canonicalFormulaPair(LHS, RHS), [&] {
43+
if (&LHS == &RHS)
44+
return &LHS;
45+
if (LHS.kind() == Formula::Literal)
46+
return LHS.literal() ? &RHS : &LHS;
47+
if (RHS.kind() == Formula::Literal)
48+
return RHS.literal() ? &LHS : &RHS;
49+
50+
return &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
51+
});
4252
}
4353

4454
const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
45-
if (&LHS == &RHS)
46-
return LHS;
47-
48-
auto [It, Inserted] =
49-
Ors.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
50-
if (Inserted)
51-
It->second = &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
52-
return *It->second;
55+
return cached(Ors, canonicalFormulaPair(LHS, RHS), [&] {
56+
if (&LHS == &RHS)
57+
return &LHS;
58+
if (LHS.kind() == Formula::Literal)
59+
return LHS.literal() ? &LHS : &RHS;
60+
if (RHS.kind() == Formula::Literal)
61+
return RHS.literal() ? &RHS : &LHS;
62+
63+
return &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
64+
});
5365
}
5466

5567
const Formula &Arena::makeNot(const Formula &Val) {
56-
auto [It, Inserted] = Nots.try_emplace(&Val, nullptr);
57-
if (Inserted)
58-
It->second = &Formula::create(Alloc, Formula::Not, {&Val});
59-
return *It->second;
68+
return cached(Nots, &Val, [&] {
69+
if (Val.kind() == Formula::Not)
70+
return Val.operands()[0];
71+
if (Val.kind() == Formula::Literal)
72+
return &makeLiteral(!Val.literal());
73+
74+
return &Formula::create(Alloc, Formula::Not, {&Val});
75+
});
6076
}
6177

6278
const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) {
63-
if (&LHS == &RHS)
64-
return makeLiteral(true);
65-
66-
auto [It, Inserted] =
67-
Implies.try_emplace(std::make_pair(&LHS, &RHS), nullptr);
68-
if (Inserted)
69-
It->second = &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
70-
return *It->second;
79+
return cached(Implies, std::make_pair(&LHS, &RHS), [&] {
80+
if (&LHS == &RHS)
81+
return &makeLiteral(true);
82+
if (LHS.kind() == Formula::Literal)
83+
return LHS.literal() ? &RHS : &makeLiteral(true);
84+
if (RHS.kind() == Formula::Literal)
85+
return RHS.literal() ? &RHS : &makeNot(LHS);
86+
87+
return &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
88+
});
7189
}
7290

7391
const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
74-
if (&LHS == &RHS)
75-
return makeLiteral(true);
76-
77-
auto [It, Inserted] =
78-
Equals.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
79-
if (Inserted)
80-
It->second = &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
81-
return *It->second;
92+
return cached(Equals, canonicalFormulaPair(LHS, RHS), [&] {
93+
if (&LHS == &RHS)
94+
return &makeLiteral(true);
95+
if (LHS.kind() == Formula::Literal)
96+
return LHS.literal() ? &RHS : &makeNot(RHS);
97+
if (RHS.kind() == Formula::Literal)
98+
return RHS.literal() ? &LHS : &makeNot(LHS);
99+
100+
return &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
101+
});
82102
}
83103

84104
IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {

‎clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp‎

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -141,8 +141,6 @@ DataflowAnalysisContext::joinFlowConditions(Atom FirstToken,
141141

142142
Solver::Result DataflowAnalysisContext::querySolver(
143143
llvm::SetVector<const Formula *> Constraints) {
144-
Constraints.insert(&arena().makeLiteral(true));
145-
Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
146144
return S->solve(Constraints.getArrayRef());
147145
}
148146

@@ -213,13 +211,8 @@ void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
213211
Constraints.insert(&arena().makeAtomRef(Token));
214212
addTransitiveFlowConditionConstraints(Token, Constraints);
215213

216-
// TODO: have formulas know about true/false directly instead
217-
Atom True = arena().makeLiteral(true).getAtom();
218-
Atom False = arena().makeLiteral(false).getAtom();
219-
Formula::AtomNames Names = {{False, "false"}, {True, "true"}};
220-
221214
for (const auto *Constraint : Constraints) {
222-
Constraint->print(OS, &Names);
215+
Constraint->print(OS);
223216
OS << "\n";
224217
}
225218
}

‎clang/lib/Analysis/FlowSensitive/Formula.cpp‎

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,9 @@
1717

1818
namespace clang::dataflow {
1919

20-
Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
21-
ArrayRef<const Formula *> Operands, unsigned Value) {
20+
const Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
21+
ArrayRef<const Formula *> Operands,
22+
unsigned Value) {
2223
assert(Operands.size() == numOperands(K));
2324
if (Value != 0) // Currently, formulas have values or operands, not both.
2425
assert(numOperands(K) == 0);
@@ -38,6 +39,7 @@ Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
3839
static llvm::StringLiteral sigil(Formula::Kind K) {
3940
switch (K) {
4041
case Formula::AtomRef:
42+
case Formula::Literal:
4143
return "";
4244
case Formula::Not:
4345
return "!";
@@ -62,7 +64,16 @@ void Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const {
6264

6365
switch (numOperands(kind())) {
6466
case 0:
65-
OS << getAtom();
67+
switch (kind()) {
68+
case AtomRef:
69+
OS << getAtom();
70+
break;
71+
case Literal:
72+
OS << (literal() ? "true" : "false");
73+
break;
74+
default:
75+
llvm_unreachable("unhandled formula kind");
76+
}
6677
break;
6778
case 1:
6879
OS << sigil(kind());

‎clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -322,6 +322,9 @@ CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
322322
switch (Val->kind()) {
323323
case Formula::AtomRef:
324324
break;
325+
case Formula::Literal:
326+
CNF.addClause(Val->literal() ? posLit(Var) : negLit(Var));
327+
break;
325328
case Formula::And: {
326329
const Variable LHS = GetVar(Val->operands()[0]);
327330
const Variable RHS = GetVar(Val->operands()[1]);

‎clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp‎

Lines changed: 31 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -34,12 +34,6 @@ TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) {
3434
EXPECT_NE(&X, &Y);
3535
}
3636

37-
TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
38-
auto &X = A.makeAtomRef(A.makeAtom());
39-
auto &XAndX = A.makeAnd(X, X);
40-
EXPECT_EQ(&XAndX, &X);
41-
}
42-
4337
TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
4438
auto &X = A.makeAtomRef(A.makeAtom());
4539
auto &Y = A.makeAtomRef(A.makeAtom());
@@ -55,12 +49,6 @@ TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
5549
EXPECT_NE(&XAndY1, &XAndZ);
5650
}
5751

58-
TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
59-
auto &X = A.makeAtomRef(A.makeAtom());
60-
auto &XOrX = A.makeOr(X, X);
61-
EXPECT_EQ(&XOrX, &X);
62-
}
63-
6452
TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
6553
auto &X = A.makeAtomRef(A.makeAtom());
6654
auto &Y = A.makeAtomRef(A.makeAtom());
@@ -86,12 +74,6 @@ TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
8674
EXPECT_NE(&NotX1, &NotY);
8775
}
8876

89-
TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) {
90-
auto &X = A.makeAtomRef(A.makeAtom());
91-
auto &XImpliesX = A.makeImplies(X, X);
92-
EXPECT_EQ(&XImpliesX, &A.makeLiteral(true));
93-
}
94-
9577
TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
9678
auto &X = A.makeAtomRef(A.makeAtom());
9779
auto &Y = A.makeAtomRef(A.makeAtom());
@@ -107,12 +89,6 @@ TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
10789
EXPECT_NE(&XImpliesY1, &XImpliesZ);
10890
}
10991

110-
TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
111-
auto &X = A.makeAtomRef(A.makeAtom());
112-
auto &XIffX = A.makeEquals(X, X);
113-
EXPECT_EQ(&XIffX, &A.makeLiteral(true));
114-
}
115-
11692
TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
11793
auto &X = A.makeAtomRef(A.makeAtom());
11894
auto &Y = A.makeAtomRef(A.makeAtom());
@@ -181,5 +157,36 @@ V1 V2
181157
^)"));
182158
}
183159

160+
TEST_F(ArenaTest, IdentitySimplification) {
161+
auto &X = A.makeAtomRef(A.makeAtom());
162+
163+
EXPECT_EQ(&X, &A.makeAnd(X, X));
164+
EXPECT_EQ(&X, &A.makeOr(X, X));
165+
EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, X));
166+
EXPECT_EQ(&A.makeLiteral(true), &A.makeEquals(X, X));
167+
EXPECT_EQ(&X, &A.makeNot(A.makeNot(X)));
168+
}
169+
170+
TEST_F(ArenaTest, LiteralSimplification) {
171+
auto &X = A.makeAtomRef(A.makeAtom());
172+
173+
EXPECT_EQ(&X, &A.makeAnd(X, A.makeLiteral(true)));
174+
EXPECT_EQ(&A.makeLiteral(false), &A.makeAnd(X, A.makeLiteral(false)));
175+
176+
EXPECT_EQ(&A.makeLiteral(true), &A.makeOr(X, A.makeLiteral(true)));
177+
EXPECT_EQ(&X, &A.makeOr(X, A.makeLiteral(false)));
178+
179+
EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, A.makeLiteral(true)));
180+
EXPECT_EQ(&A.makeNot(X), &A.makeImplies(X, A.makeLiteral(false)));
181+
EXPECT_EQ(&X, &A.makeImplies(A.makeLiteral(true), X));
182+
EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(A.makeLiteral(false), X));
183+
184+
EXPECT_EQ(&X, &A.makeEquals(X, A.makeLiteral(true)));
185+
EXPECT_EQ(&A.makeNot(X), &A.makeEquals(X, A.makeLiteral(false)));
186+
187+
EXPECT_EQ(&A.makeLiteral(false), &A.makeNot(A.makeLiteral(true)));
188+
EXPECT_EQ(&A.makeLiteral(true), &A.makeNot(A.makeLiteral(false)));
189+
}
190+
184191
} // namespace
185192
} // namespace clang::dataflow

0 commit comments

Comments
 (0)