This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.
sammccall marked an inline comment as done.
Closed by commit rG5e4ad816bf10: [dataflow] Replace most BoolValue subclasses
with references to Formula (and… (authored by sammccall).
Changed prior to commit:
https://reviews.llvm.org/D153469?vs=533405&id=537301#toc
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D153469/new/
https://reviews.llvm.org/D153469
Files:
clang/include/clang/Analysis/FlowSensitive/Arena.h
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/Value.h
clang/lib/Analysis/FlowSensitive/Arena.cpp
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
clang/lib/Analysis/FlowSensitive/Transfer.cpp
clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
@@ -7,6 +7,7 @@
//===----------------------------------------------------------------------===//
#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -39,17 +40,19 @@
}
TEST(ValueTest, TopsEquivalent) {
- TopBoolValue V1;
- TopBoolValue V2;
+ Arena A;
+ TopBoolValue V1(A.makeAtomRef(Atom(0)));
+ TopBoolValue V2(A.makeAtomRef(Atom(1)));
EXPECT_TRUE(areEquivalentValues(V1, V2));
EXPECT_TRUE(areEquivalentValues(V2, V1));
}
TEST(ValueTest, EquivalentValuesWithDifferentPropsEquivalent) {
- TopBoolValue Prop1;
- TopBoolValue Prop2;
- TopBoolValue V1;
- TopBoolValue V2;
+ Arena A;
+ TopBoolValue Prop1(A.makeAtomRef(Atom(0)));
+ TopBoolValue Prop2(A.makeAtomRef(Atom(1)));
+ TopBoolValue V1(A.makeAtomRef(Atom(2)));
+ TopBoolValue V2(A.makeAtomRef(Atom(3)));
V1.setProperty("foo", Prop1);
V2.setProperty("bar", Prop2);
EXPECT_TRUE(areEquivalentValues(V1, V2));
@@ -57,9 +60,10 @@
}
TEST(ValueTest, DifferentKindsNotEquivalent) {
+ Arena A;
auto L = ScalarStorageLocation(QualType());
ReferenceValue V1(L);
- TopBoolValue V2;
+ TopBoolValue V2(A.makeAtomRef(Atom(0)));
EXPECT_FALSE(areEquivalentValues(V1, V2));
EXPECT_FALSE(areEquivalentValues(V2, V1));
}
Index: clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
@@ -3018,14 +3018,12 @@
ASSERT_THAT(BazDecl, NotNull());
const auto *BazVal =
- dyn_cast_or_null<ConjunctionValue>(Env.getValue(*BazDecl));
+ dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl));
ASSERT_THAT(BazVal, NotNull());
- EXPECT_EQ(&BazVal->getLeftSubValue(), FooVal);
-
- const auto *BazRightSubValVal =
- cast<DisjunctionValue>(&BazVal->getRightSubValue());
- EXPECT_EQ(&BazRightSubValVal->getLeftSubValue(), BarVal);
- EXPECT_EQ(&BazRightSubValVal->getRightSubValue(), QuxVal);
+ auto &A = Env.arena();
+ EXPECT_EQ(&BazVal->formula(),
+ &A.makeAnd(FooVal->formula(),
+ A.makeOr(BarVal->formula(), QuxVal->formula())));
});
}
@@ -3068,15 +3066,12 @@
ASSERT_THAT(BazDecl, NotNull());
const auto *BazVal =
- dyn_cast_or_null<DisjunctionValue>(Env.getValue(*BazDecl));
+ dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl));
ASSERT_THAT(BazVal, NotNull());
-
- const auto *BazLeftSubValVal =
- cast<ConjunctionValue>(&BazVal->getLeftSubValue());
- EXPECT_EQ(&BazLeftSubValVal->getLeftSubValue(), FooVal);
- EXPECT_EQ(&BazLeftSubValVal->getRightSubValue(), QuxVal);
-
- EXPECT_EQ(&BazVal->getRightSubValue(), BarVal);
+ auto &A = Env.arena();
+ EXPECT_EQ(&BazVal->formula(),
+ &A.makeOr(A.makeAnd(FooVal->formula(), QuxVal->formula()),
+ BarVal->formula()));
});
}
@@ -3122,17 +3117,14 @@
ASSERT_THAT(FooDecl, NotNull());
const auto *FooVal =
- dyn_cast_or_null<ConjunctionValue>(Env.getValue(*FooDecl));
+ dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
ASSERT_THAT(FooVal, NotNull());
-
- const auto &FooLeftSubVal =
- cast<ConjunctionValue>(FooVal->getLeftSubValue());
- const auto &FooLeftLeftSubVal =
- cast<ConjunctionValue>(FooLeftSubVal.getLeftSubValue());
- EXPECT_EQ(&FooLeftLeftSubVal.getLeftSubValue(), AVal);
- EXPECT_EQ(&FooLeftLeftSubVal.getRightSubValue(), BVal);
- EXPECT_EQ(&FooLeftSubVal.getRightSubValue(), CVal);
- EXPECT_EQ(&FooVal->getRightSubValue(), DVal);
+ auto &A = Env.arena();
+ EXPECT_EQ(
+ &FooVal->formula(),
+ &A.makeAnd(A.makeAnd(A.makeAnd(AVal->formula(), BVal->formula()),
+ CVal->formula()),
+ DVal->formula()));
});
}
}
@@ -3163,10 +3155,10 @@
ASSERT_THAT(BarDecl, NotNull());
const auto *BarVal =
- dyn_cast_or_null<NegationValue>(Env.getValue(*BarDecl));
+ dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
ASSERT_THAT(BarVal, NotNull());
-
- EXPECT_EQ(&BarVal->getSubVal(), FooVal);
+ auto &A = Env.arena();
+ EXPECT_EQ(&BarVal->formula(), &A.makeNot(FooVal->formula()));
});
}
Index: clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -28,56 +28,56 @@
};
TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) {
- auto &X = A.create<TopBoolValue>();
- auto &Y = A.create<TopBoolValue>();
- EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
+ auto &X = A.makeTopValue();
+ auto &Y = A.makeTopValue();
+ EXPECT_FALSE(Context.equivalentFormulas(X.formula(), Y.formula()));
}
TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) {
- auto &FC = A.makeFlowConditionToken();
- auto &C = A.create<AtomicBoolValue>();
+ Atom FC = A.makeFlowConditionToken();
+ auto &C = A.makeAtomRef(A.makeAtom());
EXPECT_FALSE(Context.flowConditionImplies(FC, C));
}
TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) {
- auto &FC = A.makeFlowConditionToken();
- auto &C = A.create<AtomicBoolValue>();
+ Atom FC = A.makeFlowConditionToken();
+ auto &C = A.makeAtomRef(A.makeAtom());
Context.addFlowConditionConstraint(FC, C);
EXPECT_TRUE(Context.flowConditionImplies(FC, C));
}
TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) {
- auto &FC1 = A.makeFlowConditionToken();
- auto &C1 = A.create<AtomicBoolValue>();
+ Atom FC1 = A.makeFlowConditionToken();
+ auto &C1 = A.makeAtomRef(A.makeAtom());
Context.addFlowConditionConstraint(FC1, C1);
// Forked flow condition inherits the constraints of its parent flow
// condition.
- auto &FC2 = Context.forkFlowCondition(FC1);
+ Atom FC2 = Context.forkFlowCondition(FC1);
EXPECT_TRUE(Context.flowConditionImplies(FC2, C1));
// Adding a new constraint to the forked flow condition does not affect its
// parent flow condition.
- auto &C2 = A.create<AtomicBoolValue>();
+ auto &C2 = A.makeAtomRef(A.makeAtom());
Context.addFlowConditionConstraint(FC2, C2);
EXPECT_TRUE(Context.flowConditionImplies(FC2, C2));
EXPECT_FALSE(Context.flowConditionImplies(FC1, C2));
}
TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
- auto &C1 = A.create<AtomicBoolValue>();
- auto &C2 = A.create<AtomicBoolValue>();
- auto &C3 = A.create<AtomicBoolValue>();
+ auto &C1 = A.makeAtomRef(A.makeAtom());
+ auto &C2 = A.makeAtomRef(A.makeAtom());
+ auto &C3 = A.makeAtomRef(A.makeAtom());
- auto &FC1 = A.makeFlowConditionToken();
+ Atom FC1 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC1, C1);
Context.addFlowConditionConstraint(FC1, C3);
- auto &FC2 = A.makeFlowConditionToken();
+ Atom FC2 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC2, C2);
Context.addFlowConditionConstraint(FC2, C3);
- auto &FC3 = Context.joinFlowConditions(FC1, FC2);
+ Atom FC3 = Context.joinFlowConditions(FC1, FC2);
EXPECT_FALSE(Context.flowConditionImplies(FC3, C1));
EXPECT_FALSE(Context.flowConditionImplies(FC3, C2));
EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));
@@ -85,77 +85,77 @@
TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
// Fresh flow condition with empty/no constraints is always true.
- auto &FC1 = A.makeFlowConditionToken();
+ Atom FC1 = A.makeFlowConditionToken();
EXPECT_TRUE(Context.flowConditionIsTautology(FC1));
// Literal `true` is always true.
- auto &FC2 = A.makeFlowConditionToken();
+ Atom FC2 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC2, A.makeLiteral(true));
EXPECT_TRUE(Context.flowConditionIsTautology(FC2));
// Literal `false` is never true.
- auto &FC3 = A.makeFlowConditionToken();
+ Atom FC3 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC3, A.makeLiteral(false));
EXPECT_FALSE(Context.flowConditionIsTautology(FC3));
// We can't prove that an arbitrary bool A is always true...
- auto &C1 = A.create<AtomicBoolValue>();
- auto &FC4 = A.makeFlowConditionToken();
+ auto &C1 = A.makeAtomRef(A.makeAtom());
+ Atom FC4 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC4, C1);
EXPECT_FALSE(Context.flowConditionIsTautology(FC4));
// ... but we can prove A || !A is true.
- auto &FC5 = A.makeFlowConditionToken();
+ Atom FC5 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC5, A.makeOr(C1, A.makeNot(C1)));
EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
}
TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
- auto &Z = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
+ auto &Y = A.makeAtomRef(A.makeAtom());
+ auto &Z = A.makeAtomRef(A.makeAtom());
auto &True = A.makeLiteral(true);
auto &False = A.makeLiteral(false);
// X == X
- EXPECT_TRUE(Context.equivalentBoolValues(X, X));
+ EXPECT_TRUE(Context.equivalentFormulas(X, X));
// X != Y
- EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
+ EXPECT_FALSE(Context.equivalentFormulas(X, Y));
// !X != X
- EXPECT_FALSE(Context.equivalentBoolValues(A.makeNot(X), X));
+ EXPECT_FALSE(Context.equivalentFormulas(A.makeNot(X), X));
// !(!X) = X
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeNot(A.makeNot(X)), X));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeNot(A.makeNot(X)), X));
// (X || X) == X
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, X), X));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, X), X));
// (X || Y) != X
- EXPECT_FALSE(Context.equivalentBoolValues(A.makeOr(X, Y), X));
+ EXPECT_FALSE(Context.equivalentFormulas(A.makeOr(X, Y), X));
// (X || True) == True
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, True), True));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, True), True));
// (X || False) == X
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, False), X));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, False), X));
// (X && X) == X
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, X), X));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, X), X));
// (X && Y) != X
- EXPECT_FALSE(Context.equivalentBoolValues(A.makeAnd(X, Y), X));
+ EXPECT_FALSE(Context.equivalentFormulas(A.makeAnd(X, Y), X));
// (X && True) == X
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, True), X));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, True), X));
// (X && False) == False
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, False), False));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, False), False));
// (X || Y) == (Y || X)
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, Y), A.makeOr(Y, X)));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, Y), A.makeOr(Y, X)));
// (X && Y) == (Y && X)
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, Y), A.makeAnd(Y, X)));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, Y), A.makeAnd(Y, X)));
// ((X || Y) || Z) == (X || (Y || Z))
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(A.makeOr(X, Y), Z),
- A.makeOr(X, A.makeOr(Y, Z))));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(A.makeOr(X, Y), Z),
+ A.makeOr(X, A.makeOr(Y, Z))));
// ((X && Y) && Z) == (X && (Y && Z))
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(A.makeAnd(X, Y), Z),
- A.makeAnd(X, A.makeAnd(Y, Z))));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(A.makeAnd(X, Y), Z),
+ A.makeAnd(X, A.makeAnd(Y, Z))));
}
} // namespace
Index: clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
@@ -20,26 +20,26 @@
};
TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomValue();
+ auto &Y = A.makeAtomValue();
EXPECT_NE(&X, &Y);
}
TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) {
- auto &X = A.create<TopBoolValue>();
- auto &Y = A.create<TopBoolValue>();
+ auto &X = A.makeTopValue();
+ auto &Y = A.makeTopValue();
EXPECT_NE(&X, &Y);
}
TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
- auto &X = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
auto &XAndX = A.makeAnd(X, X);
EXPECT_EQ(&XAndX, &X);
}
TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
+ auto &Y = A.makeAtomRef(A.makeAtom());
auto &XAndY1 = A.makeAnd(X, Y);
auto &XAndY2 = A.makeAnd(X, Y);
EXPECT_EQ(&XAndY1, &XAndY2);
@@ -47,20 +47,20 @@
auto &YAndX = A.makeAnd(Y, X);
EXPECT_EQ(&XAndY1, &YAndX);
- auto &Z = A.create<AtomicBoolValue>();
+ auto &Z = A.makeAtomRef(A.makeAtom());
auto &XAndZ = A.makeAnd(X, Z);
EXPECT_NE(&XAndY1, &XAndZ);
}
TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
- auto &X = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
auto &XOrX = A.makeOr(X, X);
EXPECT_EQ(&XOrX, &X);
}
TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
+ auto &Y = A.makeAtomRef(A.makeAtom());
auto &XOrY1 = A.makeOr(X, Y);
auto &XOrY2 = A.makeOr(X, Y);
EXPECT_EQ(&XOrY1, &XOrY2);
@@ -68,31 +68,30 @@
auto &YOrX = A.makeOr(Y, X);
EXPECT_EQ(&XOrY1, &YOrX);
- auto &Z = A.create<AtomicBoolValue>();
+ auto &Z = A.makeAtomRef(A.makeAtom());
auto &XOrZ = A.makeOr(X, Z);
EXPECT_NE(&XOrY1, &XOrZ);
}
TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
- auto &X = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
auto &NotX1 = A.makeNot(X);
auto &NotX2 = A.makeNot(X);
EXPECT_EQ(&NotX1, &NotX2);
-
- auto &Y = A.create<AtomicBoolValue>();
+ auto &Y = A.makeAtomRef(A.makeAtom());
auto &NotY = A.makeNot(Y);
EXPECT_NE(&NotX1, &NotY);
}
TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) {
- auto &X = A.create<AtomicBoolValue>();
+ 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.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
+ auto &Y = A.makeAtomRef(A.makeAtom());
auto &XImpliesY1 = A.makeImplies(X, Y);
auto &XImpliesY2 = A.makeImplies(X, Y);
EXPECT_EQ(&XImpliesY1, &XImpliesY2);
@@ -100,20 +99,20 @@
auto &YImpliesX = A.makeImplies(Y, X);
EXPECT_NE(&XImpliesY1, &YImpliesX);
- auto &Z = A.create<AtomicBoolValue>();
+ auto &Z = A.makeAtomRef(A.makeAtom());
auto &XImpliesZ = A.makeImplies(X, Z);
EXPECT_NE(&XImpliesY1, &XImpliesZ);
}
TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
- auto &X = A.create<AtomicBoolValue>();
+ 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.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
+ auto &Y = A.makeAtomRef(A.makeAtom());
auto &XIffY1 = A.makeEquals(X, Y);
auto &XIffY2 = A.makeEquals(X, Y);
EXPECT_EQ(&XIffY1, &XIffY2);
@@ -121,30 +120,21 @@
auto &YIffX = A.makeEquals(Y, X);
EXPECT_EQ(&XIffY1, &YIffX);
- auto &Z = A.create<AtomicBoolValue>();
+ auto &Z = A.makeAtomRef(A.makeAtom());
auto &XIffZ = A.makeEquals(X, Z);
EXPECT_NE(&XIffY1, &XIffZ);
}
-TEST_F(ArenaTest, ValueToFormula) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
- auto &XIffY = A.makeEquals(X, Y);
- auto &XOrNotY = A.makeOr(X, A.makeNot(Y));
- auto &Implies = A.makeImplies(XIffY, XOrNotY);
-
- EXPECT_EQ(llvm::to_string(A.getFormula(Implies)),
- "((V0 = V1) => (V0 | !V1))");
-}
-
-TEST_F(ArenaTest, ValueToFormulaCached) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
- auto &XIffY = A.makeEquals(X, Y);
-
- auto &Formula1 = A.getFormula(XIffY);
- auto &Formula2 = A.getFormula(XIffY);
- EXPECT_EQ(&Formula1, &Formula2);
+TEST_F(ArenaTest, Interning) {
+ Atom X = A.makeAtom();
+ Atom Y = A.makeAtom();
+ const Formula &F1 = A.makeAnd(A.makeAtomRef(X), A.makeAtomRef(Y));
+ const Formula &F2 = A.makeAnd(A.makeAtomRef(Y), A.makeAtomRef(X));
+ EXPECT_EQ(&F1, &F2);
+ BoolValue &B1 = A.makeBoolValue(F1);
+ BoolValue &B2 = A.makeBoolValue(F2);
+ EXPECT_EQ(&B1, &B2);
+ EXPECT_EQ(&B1.formula(), &F1);
}
} // namespace
Index: clang/lib/Analysis/FlowSensitive/Transfer.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/Transfer.cpp
+++ clang/lib/Analysis/FlowSensitive/Transfer.cpp
@@ -62,64 +62,12 @@
return Env.makeAtomicBoolValue();
}
-// Functionally updates `V` such that any instances of `TopBool` are replaced
-// with fresh atomic bools. Note: This implementation assumes that `B` is a
-// tree; if `B` is a DAG, it will lose any sharing between subvalues that was
-// present in the original .
-static BoolValue &unpackValue(BoolValue &V, Environment &Env);
-
-template <typename Derived, typename M>
-BoolValue &unpackBinaryBoolValue(Environment &Env, BoolValue &B, M build) {
- auto &V = *cast<Derived>(&B);
- BoolValue &Left = V.getLeftSubValue();
- BoolValue &Right = V.getRightSubValue();
- BoolValue &ULeft = unpackValue(Left, Env);
- BoolValue &URight = unpackValue(Right, Env);
-
- if (&ULeft == &Left && &URight == &Right)
- return V;
-
- return (Env.*build)(ULeft, URight);
-}
-
static BoolValue &unpackValue(BoolValue &V, Environment &Env) {
- switch (V.getKind()) {
- case Value::Kind::Integer:
- case Value::Kind::Reference:
- case Value::Kind::Pointer:
- case Value::Kind::Struct:
- llvm_unreachable("BoolValue cannot have any of these kinds.");
-
- case Value::Kind::AtomicBool:
- return V;
-
- case Value::Kind::TopBool:
- // Unpack `TopBool` into a fresh atomic bool.
- return Env.makeAtomicBoolValue();
-
- case Value::Kind::Negation: {
- auto &N = *cast<NegationValue>(&V);
- BoolValue &Sub = N.getSubVal();
- BoolValue &USub = unpackValue(Sub, Env);
-
- if (&USub == &Sub)
- return V;
- return Env.makeNot(USub);
- }
- case Value::Kind::Conjunction:
- return unpackBinaryBoolValue<ConjunctionValue>(Env, V,
- &Environment::makeAnd);
- case Value::Kind::Disjunction:
- return unpackBinaryBoolValue<DisjunctionValue>(Env, V,
- &Environment::makeOr);
- case Value::Kind::Implication:
- return unpackBinaryBoolValue<ImplicationValue>(
- Env, V, &Environment::makeImplication);
- case Value::Kind::Biconditional:
- return unpackBinaryBoolValue<BiconditionalValue>(Env, V,
- &Environment::makeIff);
+ if (auto *Top = llvm::dyn_cast<TopBoolValue>(&V)) {
+ auto &A = Env.getDataflowAnalysisContext().arena();
+ return A.makeBoolValue(A.makeAtomRef(Top->getAtom()));
}
- llvm_unreachable("All reachable cases in switch return");
+ return V;
}
// Unpacks the value (if any) associated with `E` and updates `E` to the new
Index: clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
+++ clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
@@ -97,6 +97,7 @@
case Value::Kind::Integer:
case Value::Kind::TopBool:
case Value::Kind::AtomicBool:
+ case Value::Kind::FormulaBool:
break;
case Value::Kind::Reference:
JOS.attributeObject(
@@ -111,35 +112,6 @@
JOS.attributeObject("f:" + Child.first->getNameAsString(),
[&] { dump(*Child.second); });
break;
- case Value::Kind::Disjunction: {
- auto &VV = cast<DisjunctionValue>(V);
- JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
- JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
- break;
- }
- case Value::Kind::Conjunction: {
- auto &VV = cast<ConjunctionValue>(V);
- JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
- JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
- break;
- }
- case Value::Kind::Negation: {
- auto &VV = cast<NegationValue>(V);
- JOS.attributeObject("not", [&] { dump(VV.getSubVal()); });
- break;
- }
- case Value::Kind::Implication: {
- auto &VV = cast<ImplicationValue>(V);
- JOS.attributeObject("if", [&] { dump(VV.getLeftSubValue()); });
- JOS.attributeObject("then", [&] { dump(VV.getRightSubValue()); });
- break;
- }
- case Value::Kind::Biconditional: {
- auto &VV = cast<BiconditionalValue>(V);
- JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
- JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
- break;
- }
}
for (const auto& Prop : V.properties())
@@ -149,10 +121,12 @@
// Running the SAT solver is expensive, but knowing which booleans are
// guaranteed true/false here is valuable and hard to determine by hand.
if (auto *B = llvm::dyn_cast<BoolValue>(&V)) {
- JOS.attribute("truth", Env.flowConditionImplies(*B) ? "true"
- : Env.flowConditionImplies(Env.makeNot(*B))
- ? "false"
- : "unknown");
+ JOS.attribute("formula", llvm::to_string(B->formula()));
+ JOS.attribute(
+ "truth", Env.flowConditionImplies(B->formula()) ? "true"
+ : Env.flowConditionImplies(Env.arena().makeNot(B->formula()))
+ ? "false"
+ : "unknown");
}
}
void dump(const StorageLocation &L) {
Index: clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -36,16 +36,8 @@
return "AtomicBool";
case Value::Kind::TopBool:
return "TopBool";
- case Value::Kind::Conjunction:
- return "Conjunction";
- case Value::Kind::Disjunction:
- return "Disjunction";
- case Value::Kind::Negation:
- return "Negation";
- case Value::Kind::Implication:
- return "Implication";
- case Value::Kind::Biconditional:
- return "Biconditional";
+ case Value::Kind::FormulaBool:
+ return "FormulaBool";
}
llvm_unreachable("Unhandled value kind");
}
Index: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -107,15 +107,16 @@
// if (o.has_value())
// x = o.value();
// ```
- auto *Expr1 = cast<BoolValue>(&Val1);
- auto *Expr2 = cast<BoolValue>(&Val2);
- auto &MergedVal = MergedEnv.makeAtomicBoolValue();
- MergedEnv.addToFlowCondition(MergedEnv.makeOr(
- MergedEnv.makeAnd(Env1.getFlowConditionToken(),
- MergedEnv.makeIff(MergedVal, *Expr1)),
- MergedEnv.makeAnd(Env2.getFlowConditionToken(),
- MergedEnv.makeIff(MergedVal, *Expr2))));
- return &MergedVal;
+ auto &Expr1 = cast<BoolValue>(Val1).formula();
+ auto &Expr2 = cast<BoolValue>(Val2).formula();
+ auto &A = MergedEnv.arena();
+ auto &MergedVal = A.makeAtomRef(A.makeAtom());
+ MergedEnv.addToFlowCondition(
+ A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()),
+ A.makeEquals(MergedVal, Expr1)),
+ A.makeAnd(A.makeAtomRef(Env2.getFlowConditionToken()),
+ A.makeEquals(MergedVal, Expr2))));
+ return &A.makeBoolValue(MergedVal);
}
// FIXME: Consider destroying `MergedValue` immediately if `ValueModel::merge`
@@ -269,11 +270,11 @@
Environment::Environment(DataflowAnalysisContext &DACtx)
: DACtx(&DACtx),
- FlowConditionToken(&DACtx.arena().makeFlowConditionToken()) {}
+ FlowConditionToken(DACtx.arena().makeFlowConditionToken()) {}
Environment Environment::fork() const {
Environment Copy(*this);
- Copy.FlowConditionToken = &DACtx->forkFlowCondition(*FlowConditionToken);
+ Copy.FlowConditionToken = DACtx->forkFlowCondition(FlowConditionToken);
return Copy;
}
@@ -587,8 +588,8 @@
// FIXME: update join to detect backedges and simplify the flow condition
// accordingly.
- JoinedEnv.FlowConditionToken = &EnvA.DACtx->joinFlowConditions(
- *EnvA.FlowConditionToken, *EnvB.FlowConditionToken);
+ JoinedEnv.FlowConditionToken = EnvA.DACtx->joinFlowConditions(
+ EnvA.FlowConditionToken, EnvB.FlowConditionToken);
for (auto &Entry : EnvA.LocToVal) {
const StorageLocation *Loc = Entry.first;
@@ -819,7 +820,7 @@
// with integers, and so distinguishing them serves no purpose, but could
// prevent convergence.
CreatedValuesCount++;
- return &DACtx->arena().create<IntegerValue>();
+ return &arena().create<IntegerValue>();
}
if (Type->isReferenceType() || Type->isPointerType()) {
@@ -837,9 +838,9 @@
}
if (Type->isReferenceType())
- return &DACtx->arena().create<ReferenceValue>(PointeeLoc);
+ return &arena().create<ReferenceValue>(PointeeLoc);
else
- return &DACtx->arena().create<PointerValue>(PointeeLoc);
+ return &arena().create<PointerValue>(PointeeLoc);
}
if (Type->isRecordType()) {
@@ -859,7 +860,7 @@
Visited.erase(FieldType.getCanonicalType());
}
- return &DACtx->arena().create<StructValue>(std::move(FieldValues));
+ return &arena().create<StructValue>(std::move(FieldValues));
}
return nullptr;
@@ -884,12 +885,18 @@
return skip(*const_cast<StorageLocation *>(&Loc), SP);
}
+void Environment::addToFlowCondition(const Formula &Val) {
+ DACtx->addFlowConditionConstraint(FlowConditionToken, Val);
+}
void Environment::addToFlowCondition(BoolValue &Val) {
- DACtx->addFlowConditionConstraint(*FlowConditionToken, Val);
+ addToFlowCondition(Val.formula());
}
+bool Environment::flowConditionImplies(const Formula &Val) const {
+ return DACtx->flowConditionImplies(FlowConditionToken, Val);
+}
bool Environment::flowConditionImplies(BoolValue &Val) const {
- return DACtx->flowConditionImplies(*FlowConditionToken, Val);
+ return flowConditionImplies(Val.formula());
}
void Environment::dump(raw_ostream &OS) const {
@@ -909,7 +916,7 @@
}
OS << "FlowConditionToken:\n";
- DACtx->dumpFlowCondition(*FlowConditionToken, OS);
+ DACtx->dumpFlowCondition(FlowConditionToken, OS);
}
void Environment::dump() const {
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -102,115 +102,112 @@
}
void DataflowAnalysisContext::addFlowConditionConstraint(
- AtomicBoolValue &Token, BoolValue &Constraint) {
- auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint);
+ Atom Token, const Formula &Constraint) {
+ auto Res = FlowConditionConstraints.try_emplace(Token, &Constraint);
if (!Res.second) {
Res.first->second =
&arena().makeAnd(*Res.first->second, Constraint);
}
}
-AtomicBoolValue &
-DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
- auto &ForkToken = arena().makeFlowConditionToken();
- FlowConditionDeps[&ForkToken].insert(&Token);
- addFlowConditionConstraint(ForkToken, Token);
+Atom DataflowAnalysisContext::forkFlowCondition(Atom Token) {
+ Atom ForkToken = arena().makeFlowConditionToken();
+ FlowConditionDeps[ForkToken].insert(Token);
+ addFlowConditionConstraint(ForkToken, arena().makeAtomRef(Token));
return ForkToken;
}
-AtomicBoolValue &
-DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
- AtomicBoolValue &SecondToken) {
- auto &Token = arena().makeFlowConditionToken();
- FlowConditionDeps[&Token].insert(&FirstToken);
- FlowConditionDeps[&Token].insert(&SecondToken);
- addFlowConditionConstraint(
- Token, arena().makeOr(FirstToken, SecondToken));
+Atom
+DataflowAnalysisContext::joinFlowConditions(Atom FirstToken,
+ Atom SecondToken) {
+ Atom Token = arena().makeFlowConditionToken();
+ FlowConditionDeps[Token].insert(FirstToken);
+ FlowConditionDeps[Token].insert(SecondToken);
+ addFlowConditionConstraint(Token,
+ arena().makeOr(arena().makeAtomRef(FirstToken),
+ arena().makeAtomRef(SecondToken)));
return Token;
}
-Solver::Result
-DataflowAnalysisContext::querySolver(llvm::SetVector<BoolValue *> Constraints) {
+Solver::Result DataflowAnalysisContext::querySolver(
+ llvm::SetVector<const Formula *> Constraints) {
Constraints.insert(&arena().makeLiteral(true));
Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
- std::vector<const Formula *> Formulas;
- for (const BoolValue *Constraint : Constraints)
- Formulas.push_back(&arena().getFormula(*Constraint));
- return S->solve(Formulas);
+ return S->solve(Constraints.getArrayRef());
}
-bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
- BoolValue &Val) {
+bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
+ const Formula &Val) {
// Returns true if and only if truth assignment of the flow condition implies
// that `Val` is also true. We prove whether or not this property holds by
// 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::SetVector<BoolValue *> Constraints;
- Constraints.insert(&Token);
+ llvm::SetVector<const Formula *> Constraints;
+ Constraints.insert(&arena().makeAtomRef(Token));
Constraints.insert(&arena().makeNot(Val));
- llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+ llvm::DenseSet<Atom> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
return isUnsatisfiable(std::move(Constraints));
}
-bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
+bool DataflowAnalysisContext::flowConditionIsTautology(Atom Token) {
// Returns true if and only if we cannot prove that the flow condition can
// ever be false.
- llvm::SetVector<BoolValue *> Constraints;
- Constraints.insert(&arena().makeNot(Token));
- llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+ llvm::SetVector<const Formula *> Constraints;
+ Constraints.insert(&arena().makeNot(arena().makeAtomRef(Token)));
+ llvm::DenseSet<Atom> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
return isUnsatisfiable(std::move(Constraints));
}
-bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
- BoolValue &Val2) {
- llvm::SetVector<BoolValue*> Constraints;
+bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1,
+ const Formula &Val2) {
+ llvm::SetVector<const Formula *> Constraints;
Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2)));
return isUnsatisfiable(std::move(Constraints));
}
void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
- AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints,
- llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
- auto Res = VisitedTokens.insert(&Token);
+ Atom Token, llvm::SetVector<const Formula *> &Constraints,
+ llvm::DenseSet<Atom> &VisitedTokens) {
+ auto Res = VisitedTokens.insert(Token);
if (!Res.second)
return;
- auto ConstraintsIt = FlowConditionConstraints.find(&Token);
+ auto ConstraintsIt = FlowConditionConstraints.find(Token);
if (ConstraintsIt == FlowConditionConstraints.end()) {
- Constraints.insert(&Token);
+ Constraints.insert(&arena().makeAtomRef(Token));
} else {
// Bind flow condition token via `iff` to its set of constraints:
// FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
- Constraints.insert(&arena().makeEquals(Token, *ConstraintsIt->second));
+ Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token),
+ *ConstraintsIt->second));
}
- auto DepsIt = FlowConditionDeps.find(&Token);
+ auto DepsIt = FlowConditionDeps.find(Token);
if (DepsIt != FlowConditionDeps.end()) {
- for (AtomicBoolValue *DepToken : DepsIt->second) {
- addTransitiveFlowConditionConstraints(*DepToken, Constraints,
+ for (Atom DepToken : DepsIt->second) {
+ addTransitiveFlowConditionConstraints(DepToken, Constraints,
VisitedTokens);
}
}
}
-void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
+void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
llvm::raw_ostream &OS) {
- // TODO: accumulate formulas directly instead
- llvm::SetVector<BoolValue *> Constraints;
- Constraints.insert(&Token);
- llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+ llvm::SetVector<const Formula *> Constraints;
+ Constraints.insert(&arena().makeAtomRef(Token));
+ llvm::DenseSet<Atom> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
// TODO: have formulas know about true/false directly instead
- Atom True = arena().getFormula(arena().makeLiteral(true)).getAtom();
- Atom False = arena().getFormula(arena().makeLiteral(false)).getAtom();
+ Atom True = arena().makeLiteral(true).getAtom();
+ Atom False = arena().makeLiteral(false).getAtom();
Formula::AtomNames Names = {{False, "false"}, {True, "true"}};
for (const auto *Constraint : Constraints) {
- arena().getFormula(*Constraint).print(OS, &Names);
+ Constraint->print(OS, &Names);
OS << "\n";
}
}
Index: clang/lib/Analysis/FlowSensitive/Arena.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -7,65 +7,75 @@
//===----------------------------------------------------------------------===//
#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
namespace clang::dataflow {
-static std::pair<BoolValue *, BoolValue *>
-makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
+static std::pair<const Formula *, const Formula *>
+canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
auto Res = std::make_pair(&LHS, &RHS);
- if (&RHS < &LHS)
+ if (&RHS < &LHS) // FIXME: use a deterministic order instead
std::swap(Res.first, Res.second);
return Res;
}
-BoolValue &Arena::makeAnd(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeAtomRef(Atom A) {
+ auto [It, Inserted] = AtomRefs.try_emplace(A);
+ if (Inserted)
+ It->second =
+ &Formula::create(Alloc, Formula::AtomRef, {}, static_cast<unsigned>(A));
+ return *It->second;
+}
+
+const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
if (&LHS == &RHS)
return LHS;
- auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
- nullptr);
- if (Res.second)
- Res.first->second = &create<ConjunctionValue>(LHS, RHS);
- return *Res.first->second;
+ auto [It, Inserted] =
+ Ands.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+ if (Inserted)
+ It->second = &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
+ return *It->second;
}
-BoolValue &Arena::makeOr(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
if (&LHS == &RHS)
return LHS;
- auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
- nullptr);
- if (Res.second)
- Res.first->second = &create<DisjunctionValue>(LHS, RHS);
- return *Res.first->second;
+ auto [It, Inserted] =
+ Ors.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+ if (Inserted)
+ It->second = &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
+ return *It->second;
}
-BoolValue &Arena::makeNot(BoolValue &Val) {
- auto Res = NegationVals.try_emplace(&Val, nullptr);
- if (Res.second)
- Res.first->second = &create<NegationValue>(Val);
- return *Res.first->second;
+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;
}
-BoolValue &Arena::makeImplies(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) {
if (&LHS == &RHS)
return makeLiteral(true);
- auto Res = ImplicationVals.try_emplace(std::make_pair(&LHS, &RHS), nullptr);
- if (Res.second)
- Res.first->second = &create<ImplicationValue>(LHS, RHS);
- return *Res.first->second;
+ 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;
}
-BoolValue &Arena::makeEquals(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
if (&LHS == &RHS)
return makeLiteral(true);
- auto Res = BiconditionalVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
- nullptr);
- if (Res.second)
- Res.first->second = &create<BiconditionalValue>(LHS, RHS);
- return *Res.first->second;
+ 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) {
@@ -76,50 +86,13 @@
return *It->second;
}
-const Formula &Arena::getFormula(const BoolValue &B) {
- auto It = ValToFormula.find(&B);
- if (It != ValToFormula.end())
- return *It->second;
- Formula &F = [&]() -> Formula & {
- switch (B.getKind()) {
- case Value::Kind::Integer:
- case Value::Kind::Reference:
- case Value::Kind::Pointer:
- case Value::Kind::Struct:
- llvm_unreachable("not a boolean");
- case Value::Kind::TopBool:
- case Value::Kind::AtomicBool:
- // TODO: assign atom numbers on creation rather than in getFormula(), so
- // they will be deterministic and maybe even meaningful.
- return Formula::create(Alloc, Formula::AtomRef, {},
- static_cast<unsigned>(makeAtom()));
- case Value::Kind::Conjunction:
- return Formula::create(
- Alloc, Formula::And,
- {&getFormula(cast<ConjunctionValue>(B).getLeftSubValue()),
- &getFormula(cast<ConjunctionValue>(B).getRightSubValue())});
- case Value::Kind::Disjunction:
- return Formula::create(
- Alloc, Formula::Or,
- {&getFormula(cast<DisjunctionValue>(B).getLeftSubValue()),
- &getFormula(cast<DisjunctionValue>(B).getRightSubValue())});
- case Value::Kind::Negation:
- return Formula::create(Alloc, Formula::Not,
- {&getFormula(cast<NegationValue>(B).getSubVal())});
- case Value::Kind::Implication:
- return Formula::create(
- Alloc, Formula::Implies,
- {&getFormula(cast<ImplicationValue>(B).getLeftSubValue()),
- &getFormula(cast<ImplicationValue>(B).getRightSubValue())});
- case Value::Kind::Biconditional:
- return Formula::create(
- Alloc, Formula::Equal,
- {&getFormula(cast<BiconditionalValue>(B).getLeftSubValue()),
- &getFormula(cast<BiconditionalValue>(B).getRightSubValue())});
- }
- }();
- ValToFormula.try_emplace(&B, &F);
- return F;
+BoolValue &Arena::makeBoolValue(const Formula &F) {
+ auto [It, Inserted] = FormulaValues.try_emplace(&F);
+ if (Inserted)
+ It->second = (F.kind() == Formula::AtomRef)
+ ? (BoolValue *)&create<AtomicBoolValue>(F)
+ : &create<FormulaBoolValue>(F);
+ return *It->second;
}
} // namespace clang::dataflow
Index: clang/include/clang/Analysis/FlowSensitive/Value.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/Value.h
+++ clang/include/clang/Analysis/FlowSensitive/Value.h
@@ -15,11 +15,11 @@
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_VALUE_H
#include "clang/AST/Decl.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/StringMap.h"
#include "llvm/ADT/StringRef.h"
-#include "llvm/Support/raw_ostream.h"
#include <cassert>
#include <utility>
@@ -38,14 +38,10 @@
Pointer,
Struct,
- // Synthetic boolean values are either atomic values or logical connectives.
+ // TODO: Top values should not be need to be type-specific.
TopBool,
AtomicBool,
- Conjunction,
- Disjunction,
- Negation,
- Implication,
- Biconditional,
+ FormulaBool,
};
explicit Value(Kind ValKind) : ValKind(ValKind) {}
@@ -95,151 +91,68 @@
/// Models a boolean.
class BoolValue : public Value {
+ const Formula *F;
+
public:
- explicit BoolValue(Kind ValueKind) : Value(ValueKind) {}
+ explicit BoolValue(Kind ValueKind, const Formula &F)
+ : Value(ValueKind), F(&F) {}
static bool classof(const Value *Val) {
return Val->getKind() == Kind::TopBool ||
Val->getKind() == Kind::AtomicBool ||
- Val->getKind() == Kind::Conjunction ||
- Val->getKind() == Kind::Disjunction ||
- Val->getKind() == Kind::Negation ||
- Val->getKind() == Kind::Implication ||
- Val->getKind() == Kind::Biconditional;
+ Val->getKind() == Kind::FormulaBool;
}
+
+ const Formula &formula() const { return *F; }
};
-/// Models the trivially true formula, which is Top in the lattice of boolean
-/// formulas.
+/// A TopBoolValue represents a boolean that is explicitly unconstrained.
+///
+/// This is equivalent to an AtomicBoolValue that does not appear anywhere
+/// else in a system of formula.
+/// Knowing the value is unconstrained is useful when e.g. reasoning about
+/// convergence.
class TopBoolValue final : public BoolValue {
public:
- TopBoolValue() : BoolValue(Kind::TopBool) {}
-
- static bool classof(const Value *Val) {
- return Val->getKind() == Kind::TopBool;
+ TopBoolValue(const Formula &F) : BoolValue(Kind::TopBool, F) {
+ assert(F.kind() == Formula::AtomRef);
}
-};
-
-/// Models an atomic boolean.
-class AtomicBoolValue : public BoolValue {
-public:
- explicit AtomicBoolValue() : BoolValue(Kind::AtomicBool) {}
static bool classof(const Value *Val) {
- return Val->getKind() == Kind::AtomicBool;
- }
-};
-
-/// Models a boolean conjunction.
-// FIXME: Consider representing binary and unary boolean operations similar
-// to how they are represented in the AST. This might become more pressing
-// when such operations need to be added for other data types.
-class ConjunctionValue : public BoolValue {
-public:
- explicit ConjunctionValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
- : BoolValue(Kind::Conjunction), LeftSubVal(LeftSubVal),
- RightSubVal(RightSubVal) {}
-
- static bool classof(const Value *Val) {
- return Val->getKind() == Kind::Conjunction;
+ return Val->getKind() == Kind::TopBool;
}
- /// Returns the left sub-value of the conjunction.
- BoolValue &getLeftSubValue() const { return LeftSubVal; }
-
- /// Returns the right sub-value of the conjunction.
- BoolValue &getRightSubValue() const { return RightSubVal; }
-
-private:
- BoolValue &LeftSubVal;
- BoolValue &RightSubVal;
+ Atom getAtom() const { return formula().getAtom(); }
};
-/// Models a boolean disjunction.
-class DisjunctionValue : public BoolValue {
+/// Models an atomic boolean.
+///
+/// FIXME: Merge this class into FormulaBoolValue.
+/// When we want to specify atom identity, use Atom.
+class AtomicBoolValue final : public BoolValue {
public:
- explicit DisjunctionValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
- : BoolValue(Kind::Disjunction), LeftSubVal(LeftSubVal),
- RightSubVal(RightSubVal) {}
-
- static bool classof(const Value *Val) {
- return Val->getKind() == Kind::Disjunction;
+ explicit AtomicBoolValue(const Formula &F) : BoolValue(Kind::AtomicBool, F) {
+ assert(F.kind() == Formula::AtomRef);
}
- /// Returns the left sub-value of the disjunction.
- BoolValue &getLeftSubValue() const { return LeftSubVal; }
-
- /// Returns the right sub-value of the disjunction.
- BoolValue &getRightSubValue() const { return RightSubVal; }
-
-private:
- BoolValue &LeftSubVal;
- BoolValue &RightSubVal;
-};
-
-/// Models a boolean negation.
-class NegationValue : public BoolValue {
-public:
- explicit NegationValue(BoolValue &SubVal)
- : BoolValue(Kind::Negation), SubVal(SubVal) {}
-
static bool classof(const Value *Val) {
- return Val->getKind() == Kind::Negation;
+ return Val->getKind() == Kind::AtomicBool;
}
- /// Returns the sub-value of the negation.
- BoolValue &getSubVal() const { return SubVal; }
-
-private:
- BoolValue &SubVal;
+ Atom getAtom() const { return formula().getAtom(); }
};
-/// Models a boolean implication.
-///
-/// Equivalent to `!LHS v RHS`.
-class ImplicationValue : public BoolValue {
+/// Models a compound boolean formula.
+class FormulaBoolValue final : public BoolValue {
public:
- explicit ImplicationValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
- : BoolValue(Kind::Implication), LeftSubVal(LeftSubVal),
- RightSubVal(RightSubVal) {}
-
- static bool classof(const Value *Val) {
- return Val->getKind() == Kind::Implication;
+ explicit FormulaBoolValue(const Formula &F)
+ : BoolValue(Kind::FormulaBool, F) {
+ assert(F.kind() != Formula::AtomRef && "For now, use AtomicBoolValue");
}
- /// Returns the left sub-value of the implication.
- BoolValue &getLeftSubValue() const { return LeftSubVal; }
-
- /// Returns the right sub-value of the implication.
- BoolValue &getRightSubValue() const { return RightSubVal; }
-
-private:
- BoolValue &LeftSubVal;
- BoolValue &RightSubVal;
-};
-
-/// Models a boolean biconditional.
-///
-/// Equivalent to `(LHS ^ RHS) v (!LHS ^ !RHS)`.
-class BiconditionalValue : public BoolValue {
-public:
- explicit BiconditionalValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
- : BoolValue(Kind::Biconditional), LeftSubVal(LeftSubVal),
- RightSubVal(RightSubVal) {}
-
static bool classof(const Value *Val) {
- return Val->getKind() == Kind::Biconditional;
+ return Val->getKind() == Kind::FormulaBool;
}
-
- /// Returns the left sub-value of the biconditional.
- BoolValue &getLeftSubValue() const { return LeftSubVal; }
-
- /// Returns the right sub-value of the biconditional.
- BoolValue &getRightSubValue() const { return RightSubVal; }
-
-private:
- BoolValue &LeftSubVal;
- BoolValue &RightSubVal;
};
/// Models an integer.
Index: clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -456,29 +456,30 @@
template <typename T, typename... Args>
std::enable_if_t<std::is_base_of<Value, T>::value, T &>
create(Args &&...args) {
- return DACtx->arena().create<T>(std::forward<Args>(args)...);
+ return arena().create<T>(std::forward<Args>(args)...);
}
/// Returns a symbolic integer value that models an integer literal equal to
/// `Value`
IntegerValue &getIntLiteralValue(llvm::APInt Value) const {
- return DACtx->arena().makeIntLiteral(Value);
+ return arena().makeIntLiteral(Value);
}
/// Returns a symbolic boolean value that models a boolean literal equal to
/// `Value`
AtomicBoolValue &getBoolLiteralValue(bool Value) const {
- return DACtx->arena().makeLiteral(Value);
+ return cast<AtomicBoolValue>(
+ arena().makeBoolValue(arena().makeLiteral(Value)));
}
/// Returns an atomic boolean value.
BoolValue &makeAtomicBoolValue() const {
- return DACtx->arena().create<AtomicBoolValue>();
+ return arena().makeAtomValue();
}
/// Returns a unique instance of boolean Top.
BoolValue &makeTopBoolValue() const {
- return DACtx->arena().create<TopBoolValue>();
+ return arena().makeTopValue();
}
/// Returns a boolean value that represents the conjunction of `LHS` and
@@ -486,7 +487,8 @@
/// order, will return the same result. If the given boolean values represent
/// the same value, the result will be the value itself.
BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS) const {
- return DACtx->arena().makeAnd(LHS, RHS);
+ return arena().makeBoolValue(
+ arena().makeAnd(LHS.formula(), RHS.formula()));
}
/// Returns a boolean value that represents the disjunction of `LHS` and
@@ -494,13 +496,14 @@
/// order, will return the same result. If the given boolean values represent
/// the same value, the result will be the value itself.
BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS) const {
- return DACtx->arena().makeOr(LHS, RHS);
+ return arena().makeBoolValue(
+ arena().makeOr(LHS.formula(), RHS.formula()));
}
/// Returns a boolean value that represents the negation of `Val`. Subsequent
/// calls with the same argument will return the same result.
BoolValue &makeNot(BoolValue &Val) const {
- return DACtx->arena().makeNot(Val);
+ return arena().makeBoolValue(arena().makeNot(Val.formula()));
}
/// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with
@@ -508,7 +511,8 @@
/// values represent the same value, the result will be a value that
/// represents the true boolean literal.
BoolValue &makeImplication(BoolValue &LHS, BoolValue &RHS) const {
- return DACtx->arena().makeImplies(LHS, RHS);
+ return arena().makeBoolValue(
+ arena().makeImplies(LHS.formula(), RHS.formula()));
}
/// Returns a boolean value represents `LHS` <=> `RHS`. Subsequent calls with
@@ -516,17 +520,22 @@
/// result. If the given boolean values represent the same value, the result
/// will be a value that represents the true boolean literal.
BoolValue &makeIff(BoolValue &LHS, BoolValue &RHS) const {
- return DACtx->arena().makeEquals(LHS, RHS);
+ return arena().makeBoolValue(
+ arena().makeEquals(LHS.formula(), RHS.formula()));
}
/// Returns the token that identifies the flow condition of the environment.
- AtomicBoolValue &getFlowConditionToken() const { return *FlowConditionToken; }
+ Atom getFlowConditionToken() const { return FlowConditionToken; }
/// Adds `Val` to the set of clauses that constitute the flow condition.
+ void addToFlowCondition(const Formula &);
+ LLVM_DEPRECATED("Use Formula version instead", "")
void addToFlowCondition(BoolValue &Val);
/// Returns true if and only if the clauses that constitute the flow condition
/// imply that `Val` is true.
+ bool flowConditionImplies(const Formula &) const;
+ LLVM_DEPRECATED("Use Formula version instead", "")
bool flowConditionImplies(BoolValue &Val) const;
/// Returns the `DeclContext` of the block being analysed, if any. Otherwise,
@@ -547,6 +556,8 @@
/// Returns the `DataflowAnalysisContext` used by the environment.
DataflowAnalysisContext &getDataflowAnalysisContext() const { return *DACtx; }
+ Arena &arena() const { return DACtx->arena(); }
+
LLVM_DUMP_METHOD void dump() const;
LLVM_DUMP_METHOD void dump(raw_ostream &OS) const;
@@ -617,7 +628,7 @@
std::pair<StructValue *, const ValueDecl *>>
MemberLocToStruct;
- AtomicBoolValue *FlowConditionToken;
+ Atom FlowConditionToken;
};
/// Returns the storage location for the implicit object of a
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -138,33 +138,31 @@
PointerValue &getOrCreateNullPointerValue(QualType PointeeType);
/// Adds `Constraint` to the flow condition identified by `Token`.
- void addFlowConditionConstraint(AtomicBoolValue &Token,
- BoolValue &Constraint);
+ void addFlowConditionConstraint(Atom Token, const Formula &Constraint);
/// Creates a new flow condition with the same constraints as the flow
/// condition identified by `Token` and returns its token.
- AtomicBoolValue &forkFlowCondition(AtomicBoolValue &Token);
+ Atom forkFlowCondition(Atom Token);
/// Creates a new flow condition that represents the disjunction of the flow
/// conditions identified by `FirstToken` and `SecondToken`, and returns its
/// token.
- AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
- AtomicBoolValue &SecondToken);
+ Atom joinFlowConditions(Atom FirstToken, Atom SecondToken);
/// Returns true if and only if the constraints of the flow condition
/// identified by `Token` imply that `Val` is true.
- bool flowConditionImplies(AtomicBoolValue &Token, BoolValue &Val);
+ bool flowConditionImplies(Atom Token, const Formula &);
/// Returns true if and only if the constraints of the flow condition
/// identified by `Token` are always true.
- bool flowConditionIsTautology(AtomicBoolValue &Token);
+ bool flowConditionIsTautology(Atom Token);
/// Returns true if `Val1` is equivalent to `Val2`.
/// Note: This function doesn't take into account constraints on `Val1` and
/// `Val2` imposed by the flow condition.
- bool equivalentBoolValues(BoolValue &Val1, BoolValue &Val2);
+ bool equivalentFormulas(const Formula &Val1, const Formula &Val2);
- LLVM_DUMP_METHOD void dumpFlowCondition(AtomicBoolValue &Token,
+ LLVM_DUMP_METHOD void dumpFlowCondition(Atom Token,
llvm::raw_ostream &OS = llvm::dbgs());
/// Returns the `ControlFlowContext` registered for `F`, if any. Otherwise,
@@ -181,7 +179,7 @@
/// included in `Constraints` to provide contextually-accurate results, e.g.
/// if any definitions or relationships of the values in `Constraints` have
/// been stored in flow conditions.
- Solver::Result querySolver(llvm::SetVector<BoolValue *> Constraints);
+ Solver::Result querySolver(llvm::SetVector<const Formula *> Constraints);
private:
friend class Environment;
@@ -209,12 +207,12 @@
/// to track tokens of flow conditions that were already visited by recursive
/// calls.
void addTransitiveFlowConditionConstraints(
- AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints,
- llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
+ Atom Token, llvm::SetVector<const Formula *> &Constraints,
+ llvm::DenseSet<Atom> &VisitedTokens);
/// Returns true if the solver is able to prove that there is no satisfying
/// assignment for `Constraints`
- bool isUnsatisfiable(llvm::SetVector<BoolValue *> Constraints) {
+ bool isUnsatisfiable(llvm::SetVector<const Formula *> Constraints) {
return querySolver(std::move(Constraints)).getStatus() ==
Solver::Result::Status::Unsatisfiable;
}
@@ -253,9 +251,8 @@
// Flow conditions depend on other flow conditions if they are created using
// `forkFlowCondition` or `joinFlowConditions`. The graph of flow condition
// dependencies is stored in the `FlowConditionDeps` map.
- llvm::DenseMap<AtomicBoolValue *, llvm::DenseSet<AtomicBoolValue *>>
- FlowConditionDeps;
- llvm::DenseMap<AtomicBoolValue *, BoolValue *> FlowConditionConstraints;
+ llvm::DenseMap<Atom, llvm::DenseSet<Atom>> FlowConditionDeps;
+ llvm::DenseMap<Atom, const Formula *> FlowConditionConstraints;
llvm::DenseMap<const FunctionDecl *, ControlFlowContext> FunctionContexts;
Index: clang/include/clang/Analysis/FlowSensitive/Arena.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/Arena.h
+++ clang/include/clang/Analysis/FlowSensitive/Arena.h
@@ -16,12 +16,10 @@
namespace clang::dataflow {
/// The Arena owns the objects that model data within an analysis.
-/// For example, `Value` and `StorageLocation`.
+/// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`.
class Arena {
public:
- Arena()
- : TrueVal(create<AtomicBoolValue>()),
- FalseVal(create<AtomicBoolValue>()) {}
+ Arena() : True(makeAtom()), False(makeAtom()) {}
Arena(const Arena &) = delete;
Arena &operator=(const Arena &) = delete;
@@ -57,33 +55,25 @@
.get());
}
- /// Returns a boolean value that represents the conjunction of `LHS` and
- /// `RHS`. Subsequent calls with the same arguments, regardless of their
- /// order, will return the same result. If the given boolean values represent
- /// the same value, the result will be the value itself.
- BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS);
-
- /// Returns a boolean value that represents the disjunction of `LHS` and
- /// `RHS`. Subsequent calls with the same arguments, regardless of their
- /// order, will return the same result. If the given boolean values represent
- /// the same value, the result will be the value itself.
- BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS);
-
- /// Returns a boolean value that represents the negation of `Val`. Subsequent
- /// calls with the same argument will return the same result.
- BoolValue &makeNot(BoolValue &Val);
-
- /// Returns a boolean value that represents `LHS => RHS`. Subsequent calls
- /// with the same arguments, will return the same result. If the given boolean
- /// values represent the same value, the result will be a value that
- /// represents the true boolean literal.
- BoolValue &makeImplies(BoolValue &LHS, BoolValue &RHS);
-
- /// Returns a boolean value that represents `LHS <=> RHS`. Subsequent calls
- /// with the same arguments, regardless of their order, will return the same
- /// result. If the given boolean values represent the same value, the result
- /// will be a value that represents the true boolean literal.
- BoolValue &makeEquals(BoolValue &LHS, BoolValue &RHS);
+ /// Creates a BoolValue wrapping a particular formula.
+ ///
+ /// Passing in the same formula will result in the same BoolValue.
+ /// FIXME: Interning BoolValues but not other Values is inconsistent.
+ /// Decide whether we want Value interning or not.
+ BoolValue &makeBoolValue(const Formula &);
+
+ /// Creates a fresh atom and wraps in in an AtomicBoolValue.
+ /// FIXME: For now, identical-address AtomicBoolValue <=> identical atom.
+ /// Stop relying on pointer identity and remove this guarantee.
+ AtomicBoolValue &makeAtomValue() {
+ return cast<AtomicBoolValue>(makeBoolValue(makeAtomRef(makeAtom())));
+ }
+
+ /// Creates a fresh Top boolean value.
+ TopBoolValue &makeTopValue() {
+ // No need for deduplicating: there's no way to create aliasing Tops.
+ return create<TopBoolValue>(makeAtomRef(makeAtom()));
+ }
/// Returns a symbolic integer value that models an integer literal equal to
/// `Value`. These literals are the same every time.
@@ -91,27 +81,42 @@
/// an integer literal is associated with.
IntegerValue &makeIntLiteral(llvm::APInt Value);
- /// Returns a symbolic boolean value that models a boolean literal equal to
- /// `Value`. These literals are the same every time.
- AtomicBoolValue &makeLiteral(bool Value) const {
- return Value ? TrueVal : FalseVal;
+ // Factories for boolean formulas.
+ // Formulas are interned: passing the same arguments return the same result.
+ // For commutative operations like And/Or, interning ignores order.
+ // Simplifications are applied: makeOr(X, X) => X, etc.
+
+ /// Returns a formula for the conjunction of `LHS` and `RHS`.
+ const Formula &makeAnd(const Formula &LHS, const Formula &RHS);
+
+ /// Returns a formula for the disjunction of `LHS` and `RHS`.
+ const Formula &makeOr(const Formula &LHS, const Formula &RHS);
+
+ /// Returns a formula for the negation of `Val`.
+ const Formula &makeNot(const Formula &Val);
+
+ /// Returns a formula for `LHS => RHS`.
+ const Formula &makeImplies(const Formula &LHS, const Formula &RHS);
+
+ /// Returns a formula for `LHS <=> RHS`.
+ const Formula &makeEquals(const Formula &LHS, const Formula &RHS);
+
+ /// Returns a formula for the variable A.
+ const Formula &makeAtomRef(Atom A);
+
+ /// Returns a formula for a literal true/false.
+ const Formula &makeLiteral(bool Value) {
+ return makeAtomRef(Value ? True : False);
}
+ /// Returns a new atomic boolean variable, distinct from any other.
+ Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
+
/// Creates a fresh flow condition and returns a token that identifies it. The
/// token can be used to perform various operations on the flow condition such
/// as adding constraints to it, forking it, joining it with another flow
/// condition, or checking implications.
- AtomicBoolValue &makeFlowConditionToken() {
- return create<AtomicBoolValue>();
- }
-
- /// Gets the boolean formula equivalent of a BoolValue.
- /// Each unique Top values is translated to an Atom.
- /// TODO: migrate to storing Formula directly in Values instead.
- const Formula &getFormula(const BoolValue &);
-
- /// Returns a new atomic boolean variable, distinct from any other.
- Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
+ Atom makeFlowConditionToken() { return makeAtom(); }
private:
llvm::BumpPtrAllocator Alloc;
@@ -123,21 +128,18 @@
// Indices that are used to avoid recreating the same integer literals and
// composite boolean values.
llvm::DenseMap<llvm::APInt, IntegerValue *> IntegerLiterals;
- llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
- ConjunctionVals;
- llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
- DisjunctionVals;
- llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
- llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ImplicationValue *>
- ImplicationVals;
- llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
- BiconditionalVals;
-
- llvm::DenseMap<const BoolValue *, const Formula *> ValToFormula;
+ using FormulaPair = std::pair<const Formula *, const Formula *>;
+ llvm::DenseMap<FormulaPair, const Formula *> Ands;
+ llvm::DenseMap<FormulaPair, const Formula *> Ors;
+ llvm::DenseMap<const Formula *, const Formula *> Nots;
+ llvm::DenseMap<FormulaPair, const Formula *> Implies;
+ llvm::DenseMap<FormulaPair, const Formula *> Equals;
+ llvm::DenseMap<Atom, const Formula *> AtomRefs;
+
+ llvm::DenseMap<const Formula *, BoolValue *> FormulaValues;
unsigned NextAtom = 0;
- AtomicBoolValue &TrueVal;
- AtomicBoolValue &FalseVal;
+ Atom True, False;
};
} // namespace clang::dataflow
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
