Skip to content

Commit 3353f7d

Browse files
dyungdyung
committed
Revert "[dataflow] use true/false literals in formulas, rather than variables"
This reverts commit 36bd5bd. This change is causing a test failure on several build bots: - https://lab.llvm.org/buildbot/#/builders/139/builds/50255 - https://lab.llvm.org/buildbot/#/builders/216/builds/27735 - https://lab.llvm.org/buildbot/#/builders/247/builds/9334
1 parent 66e8398 commit 3353f7d

File tree

11 files changed

+98
-147
lines changed

11 files changed

+98
-147
lines changed

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

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

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

110108
/// Returns a formula for a literal true/false.
111-
const Formula &makeLiteral(bool Value) { return Value ? True : False; }
109+
const Formula &makeLiteral(bool Value) {
110+
return makeAtomRef(Value ? True : False);
111+
}
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-
const Formula &True, &False;
147+
Atom True, False;
148148
};
149149

150150
} // namespace clang::dataflow

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

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

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

473474
/// Returns an atomic boolean value.

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

Lines changed: 4 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -53,8 +53,7 @@ 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-
/// Constant true or false.
57-
Literal,
56+
// FIXME: add const true/false rather than modeling them as variables
5857

5958
Not, /// True if its only operand is false
6059

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

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

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

9589
private:
9690
Formula() = default;
@@ -100,7 +94,6 @@ class alignas(const Formula *) Formula {
10094
static unsigned numOperands(Kind K) {
10195
switch (K) {
10296
case AtomRef:
103-
case Literal:
10497
return 0;
10598
case Not:
10699
return 1;

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

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

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));
25+
const Formula &Arena::makeAtomRef(Atom A) {
26+
auto [It, Inserted] = AtomRefs.try_emplace(A);
2927
if (Inserted)
30-
It->second = Compute();
28+
It->second =
29+
&Formula::create(Alloc, Formula::AtomRef, {}, static_cast<unsigned>(A));
3130
return *It->second;
3231
}
3332

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-
}
40-
4133
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-
});
34+
if (&LHS == &RHS)
35+
return LHS;
36+
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;
5242
}
5343

5444
const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
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-
});
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;
6553
}
6654

6755
const Formula &Arena::makeNot(const Formula &Val) {
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-
});
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;
7660
}
7761

7862
const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) {
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-
});
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;
8971
}
9072

9173
const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
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-
});
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;
10282
}
10383

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

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

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -141,6 +141,8 @@ 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)));
144146
return S->solve(Constraints.getArrayRef());
145147
}
146148

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

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+
214221
for (const auto *Constraint : Constraints) {
215-
Constraint->print(OS);
222+
Constraint->print(OS, &Names);
216223
OS << "\n";
217224
}
218225
}

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

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

1818
namespace clang::dataflow {
1919

20-
const Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
21-
ArrayRef<const Formula *> Operands,
22-
unsigned Value) {
20+
Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
21+
ArrayRef<const Formula *> Operands, unsigned Value) {
2322
assert(Operands.size() == numOperands(K));
2423
if (Value != 0) // Currently, formulas have values or operands, not both.
2524
assert(numOperands(K) == 0);
@@ -39,7 +38,6 @@ const Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
3938
static llvm::StringLiteral sigil(Formula::Kind K) {
4039
switch (K) {
4140
case Formula::AtomRef:
42-
case Formula::Literal:
4341
return "";
4442
case Formula::Not:
4543
return "!";
@@ -64,16 +62,7 @@ void Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const {
6462

6563
switch (numOperands(kind())) {
6664
case 0:
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-
}
65+
OS << getAtom();
7766
break;
7867
case 1:
7968
OS << sigil(kind());

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

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -322,9 +322,6 @@ 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;
328325
case Formula::And: {
329326
const Variable LHS = GetVar(Val->operands()[0]);
330327
const Variable RHS = GetVar(Val->operands()[1]);

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

Lines changed: 24 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,12 @@ 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+
3743
TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
3844
auto &X = A.makeAtomRef(A.makeAtom());
3945
auto &Y = A.makeAtomRef(A.makeAtom());
@@ -49,6 +55,12 @@ TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
4955
EXPECT_NE(&XAndY1, &XAndZ);
5056
}
5157

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+
5264
TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
5365
auto &X = A.makeAtomRef(A.makeAtom());
5466
auto &Y = A.makeAtomRef(A.makeAtom());
@@ -74,6 +86,12 @@ TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
7486
EXPECT_NE(&NotX1, &NotY);
7587
}
7688

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+
7795
TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
7896
auto &X = A.makeAtomRef(A.makeAtom());
7997
auto &Y = A.makeAtomRef(A.makeAtom());
@@ -89,6 +107,12 @@ TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
89107
EXPECT_NE(&XImpliesY1, &XImpliesZ);
90108
}
91109

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+
92116
TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
93117
auto &X = A.makeAtomRef(A.makeAtom());
94118
auto &Y = A.makeAtomRef(A.makeAtom());
@@ -157,36 +181,5 @@ V1 V2
157181
^)"));
158182
}
159183

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-
191184
} // namespace
192185
} // namespace clang::dataflow

0 commit comments

Comments
 (0)