sgatev created this revision.
sgatev added reviewers: ymandel, xazax.hun, gribozavr2.
Herald added subscribers: tschuett, steakhal, rnkovacs, mgorny.
sgatev requested review of this revision.
Herald added a project: clang.
This is part of the implementation of the dataflow analysis framework.
See "[RFC] A dataflow analysis framework for Clang AST" on cfe-dev.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D120711
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/lib/Analysis/FlowSensitive/CMakeLists.txt
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
@@ -18,6 +18,7 @@
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
#include "clang/Analysis/FlowSensitive/DataflowLattice.h"
#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
#include "clang/Tooling/Tooling.h"
#include "llvm/ADT/Optional.h"
#include "llvm/ADT/STLExtras.h"
@@ -68,7 +69,7 @@
ControlFlowContext::build(nullptr, Body, &AST->getASTContext()));
AnalysisT Analysis = MakeAnalysis(AST->getASTContext());
- DataflowAnalysisContext DACtx;
+ DataflowAnalysisContext DACtx(std::make_unique<WatchedLiteralsSolver>());
Environment Env(DACtx);
return runDataflowAnalysis(CFCtx, Analysis, Env);
Index: clang/unittests/Analysis/FlowSensitive/TestingSupport.h
===================================================================
--- clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -23,6 +23,7 @@
#include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
#include "clang/Analysis/FlowSensitive/DataflowAnalysis.h"
#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
#include "clang/Basic/LLVM.h"
#include "clang/Serialization/PCHContainerOperations.h"
#include "clang/Tooling/ArgumentsAdjusters.h"
@@ -104,7 +105,7 @@
if (!CFCtx)
return CFCtx.takeError();
- DataflowAnalysisContext DACtx;
+ DataflowAnalysisContext DACtx(std::make_unique<WatchedLiteralsSolver>());
Environment Env(DACtx, *F);
auto Analysis = MakeAnalysis(Context, Env);
Index: clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
===================================================================
--- /dev/null
+++ clang/unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.cpp
@@ -0,0 +1,69 @@
+//===- unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp ---===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/DataflowEnvironment.h"
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+#include <memory>
+
+namespace {
+
+using namespace clang;
+using namespace dataflow;
+
+class EnvironmentTest : public ::testing::Test {
+ DataflowAnalysisContext Context;
+
+protected:
+ EnvironmentTest()
+ : Context(std::make_unique<WatchedLiteralsSolver>()), Env(Context) {}
+
+ Environment Env;
+};
+
+TEST_F(EnvironmentTest, MakeAndReturnsSameExprGivenSameArgs) {
+ auto &X = Env.makeAtomicBoolValue();
+ auto &XAndX = Env.makeAnd(X, X);
+ EXPECT_EQ(&XAndX, &X);
+}
+
+TEST_F(EnvironmentTest, MakeOrReturnsSameExprGivenSameArgs) {
+ auto &X = Env.makeAtomicBoolValue();
+ auto &XOrX = Env.makeOr(X, X);
+ EXPECT_EQ(&XOrX, &X);
+}
+
+TEST_F(EnvironmentTest, MakeImplicationReturnsTrueGivenSameArgs) {
+ auto &X = Env.makeAtomicBoolValue();
+ auto &XEqX = Env.makeImplication(X, X);
+ EXPECT_EQ(&XEqX, &Env.getBoolLiteralValue(true));
+}
+
+TEST_F(EnvironmentTest, MakeIffReturnsTrueGivenSameArgs) {
+ auto &X = Env.makeAtomicBoolValue();
+ auto &XEqX = Env.makeIff(X, X);
+ EXPECT_EQ(&XEqX, &Env.getBoolLiteralValue(true));
+}
+
+TEST_F(EnvironmentTest, FlowCondition) {
+ EXPECT_TRUE(Env.flowConditionImplies(Env.getBoolLiteralValue(true)));
+ EXPECT_FALSE(Env.flowConditionImplies(Env.getBoolLiteralValue(false)));
+
+ auto &X = Env.makeAtomicBoolValue();
+ EXPECT_FALSE(Env.flowConditionImplies(X));
+
+ Env.addToFlowCondition(X);
+ EXPECT_TRUE(Env.flowConditionImplies(X));
+
+ auto &NotX = Env.makeNot(X);
+ EXPECT_FALSE(Env.flowConditionImplies(NotX));
+}
+
+} // namespace
Index: clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
===================================================================
--- /dev/null
+++ clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -0,0 +1,72 @@
+//===- unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp ---===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+#include <memory>
+
+namespace {
+
+using namespace clang;
+using namespace dataflow;
+
+class DataflowAnalysisContextTest : public ::testing::Test {
+protected:
+ DataflowAnalysisContextTest()
+ : Context(std::make_unique<WatchedLiteralsSolver>()) {}
+
+ DataflowAnalysisContext Context;
+};
+
+TEST_F(DataflowAnalysisContextTest,
+ GetOrCreateConjunctionValueReturnsSameExprOnSubsequentCalls) {
+ auto &X = Context.createAtomicBoolValue();
+ auto &Y = Context.createAtomicBoolValue();
+ auto &XAndY1 = Context.getOrCreateConjunctionValue(X, Y);
+ auto &XAndY2 = Context.getOrCreateConjunctionValue(X, Y);
+ EXPECT_EQ(&XAndY1, &XAndY2);
+
+ auto &YAndX = Context.getOrCreateConjunctionValue(Y, X);
+ EXPECT_EQ(&XAndY1, &YAndX);
+
+ auto &Z = Context.createAtomicBoolValue();
+ auto &XAndZ = Context.getOrCreateConjunctionValue(X, Z);
+ EXPECT_NE(&XAndY1, &XAndZ);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+ GetOrCreateDisjunctionValueReturnsSameExprOnSubsequentCalls) {
+ auto &X = Context.createAtomicBoolValue();
+ auto &Y = Context.createAtomicBoolValue();
+ auto &XOrY1 = Context.getOrCreateDisjunctionValue(X, Y);
+ auto &XOrY2 = Context.getOrCreateDisjunctionValue(X, Y);
+ EXPECT_EQ(&XOrY1, &XOrY2);
+
+ auto &YOrX = Context.getOrCreateDisjunctionValue(Y, X);
+ EXPECT_EQ(&XOrY1, &YOrX);
+
+ auto &Z = Context.createAtomicBoolValue();
+ auto &XOrZ = Context.getOrCreateDisjunctionValue(X, Z);
+ EXPECT_NE(&XOrY1, &XOrZ);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+ GetOrCreateNegationValueReturnsSameExprOnSubsequentCalls) {
+ auto &X = Context.createAtomicBoolValue();
+ auto &NotX1 = Context.getOrCreateNegationValue(X);
+ auto &NotX2 = Context.getOrCreateNegationValue(X);
+ EXPECT_EQ(&NotX1, &NotX2);
+
+ auto &Y = Context.createAtomicBoolValue();
+ auto &NotY = Context.getOrCreateNegationValue(Y);
+ EXPECT_NE(&NotX1, &NotY);
+}
+
+} // namespace
Index: clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
===================================================================
--- clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
+++ clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
@@ -4,6 +4,8 @@
)
add_clang_unittest(ClangAnalysisFlowSensitiveTests
+ DataflowAnalysisContextTest.cpp
+ DataflowEnvironmentTest.cpp
MapLatticeTest.cpp
MultiVarConstantPropagationTest.cpp
SingleVarConstantPropagationTest.cpp
Index: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -453,5 +453,24 @@
return skip(*const_cast<StorageLocation *>(&Loc), SP);
}
+void Environment::addToFlowCondition(BoolValue &Val) {
+ FlowConditionConstraints.insert(&Val);
+}
+
+bool Environment::flowConditionImplies(BoolValue &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::DenseSet<BoolValue *> Constraints = {
+ &makeNot(Val), &getBoolLiteralValue(true),
+ &makeNot(getBoolLiteralValue(false))};
+ Constraints.insert(FlowConditionConstraints.begin(),
+ FlowConditionConstraints.end());
+ return DACtx->getSolver().solve(std::move(Constraints)) ==
+ Solver::Result::Unsatisfiable;
+}
+
} // namespace dataflow
} // namespace clang
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- /dev/null
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -0,0 +1,71 @@
+//===-- DataflowAnalysisContext.cpp -----------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+// This file defines a DataflowAnalysisContext class that owns objects that
+// encompass the state of a program and stores context that is used during
+// dataflow analysis.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include <cassert>
+#include <memory>
+
+namespace clang {
+namespace dataflow {
+
+ConjunctionValue &
+DataflowAnalysisContext::getOrCreateConjunctionValue(BoolValue &LHS,
+ BoolValue &RHS) {
+ auto It = ConjunctionVals.find({&LHS, &RHS});
+ if (It != ConjunctionVals.end())
+ return *It->getSecond();
+
+ It = ConjunctionVals.find({&RHS, &LHS});
+ if (It != ConjunctionVals.end())
+ return *It->getSecond();
+
+ auto Res = ConjunctionVals.try_emplace(
+ {&LHS, &RHS},
+ &takeOwnership(std::make_unique<ConjunctionValue>(LHS, RHS)));
+ assert(Res.second);
+ return *Res.first->getSecond();
+}
+
+DisjunctionValue &
+DataflowAnalysisContext::getOrCreateDisjunctionValue(BoolValue &LHS,
+ BoolValue &RHS) {
+ auto It = DisjunctionVals.find({&LHS, &RHS});
+ if (It != DisjunctionVals.end())
+ return *It->getSecond();
+
+ It = DisjunctionVals.find({&RHS, &LHS});
+ if (It != DisjunctionVals.end())
+ return *It->getSecond();
+
+ auto Res = DisjunctionVals.try_emplace(
+ {&LHS, &RHS},
+ &takeOwnership(std::make_unique<DisjunctionValue>(LHS, RHS)));
+ assert(Res.second);
+ return *Res.first->getSecond();
+}
+
+BoolValue &DataflowAnalysisContext::getOrCreateNegationValue(BoolValue &Val) {
+ auto It = NegationVals.find(&Val);
+ if (It != NegationVals.end())
+ return *It->getSecond();
+
+ auto Res = NegationVals.try_emplace(
+ &Val, &takeOwnership(std::make_unique<NegationValue>(Val)));
+ assert(Res.second);
+ return *Res.first->getSecond();
+}
+
+} // namespace dataflow
+} // namespace clang
Index: clang/lib/Analysis/FlowSensitive/CMakeLists.txt
===================================================================
--- clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -1,5 +1,6 @@
add_clang_library(clangAnalysisFlowSensitive
ControlFlowContext.cpp
+ DataflowAnalysisContext.cpp
DataflowEnvironment.cpp
Transfer.cpp
TypeErasedDataflowAnalysis.cpp
Index: clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -235,6 +235,45 @@
return DACtx->getBoolLiteralValue(Value);
}
+ /// Returns an atomic boolean value.
+ BoolValue &makeAtomicBoolValue() { return DACtx->createAtomicBoolValue(); }
+
+ /// Returns a boolean value that represents the conjunction of `LHS` and
+ /// `RHS`.
+ BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS) {
+ return &LHS == &RHS ? LHS : DACtx->getOrCreateConjunctionValue(LHS, RHS);
+ }
+
+ /// Returns a boolean value that represents the disjunction of `LHS` and
+ /// `RHS`.
+ BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS) {
+ return &LHS == &RHS ? LHS : DACtx->getOrCreateDisjunctionValue(LHS, RHS);
+ }
+
+ /// Returns a boolean value that represents the negation of `Val`.
+ BoolValue &makeNot(BoolValue &Val) {
+ return DACtx->getOrCreateNegationValue(Val);
+ }
+
+ /// Returns a boolean value represents `LHS` => `RHS`.
+ BoolValue &makeImplication(BoolValue &LHS, BoolValue &RHS) {
+ return &LHS == &RHS ? getBoolLiteralValue(true) : makeOr(makeNot(LHS), RHS);
+ }
+
+ /// Returns a boolean value represents `LHS` <=> `RHS`.
+ BoolValue &makeIff(BoolValue &LHS, BoolValue &RHS) {
+ return &LHS == &RHS
+ ? getBoolLiteralValue(true)
+ : makeAnd(makeImplication(LHS, RHS), makeImplication(RHS, LHS));
+ }
+
+ /// Adds `Val` to the set of clauses that constitute the flow condition.
+ void addToFlowCondition(BoolValue &Val);
+
+ /// Returns true if and only if the clauses that constitute the flow condition
+ /// imply that `Val` is true.
+ bool flowConditionImplies(BoolValue &Val);
+
private:
/// Creates a value appropriate for `Type`, if `Type` is supported, otherwise
/// return null.
@@ -272,7 +311,7 @@
std::pair<StructValue *, const ValueDecl *>>
MemberLocToStruct;
- // FIXME: Add flow condition constraints.
+ llvm::DenseSet<BoolValue *> FlowConditionConstraints;
};
} // namespace dataflow
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -17,6 +17,7 @@
#include "clang/AST/Decl.h"
#include "clang/AST/Expr.h"
+#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/DenseMap.h"
@@ -33,9 +34,19 @@
/// is used during dataflow analysis.
class DataflowAnalysisContext {
public:
- DataflowAnalysisContext()
- : TrueVal(takeOwnership(std::make_unique<AtomicBoolValue>())),
- FalseVal(takeOwnership(std::make_unique<AtomicBoolValue>())) {}
+ /// Constructs a dataflow analysis context.
+ ///
+ /// Requirements:
+ ///
+ /// `Slvr` must not be null.
+ DataflowAnalysisContext(std::unique_ptr<Solver> Slvr)
+ : Slvr(std::move(Slvr)), TrueVal(createAtomicBoolValue()),
+ FalseVal(createAtomicBoolValue()) {
+ assert(this->Slvr != nullptr);
+ }
+
+ /// Returns the SAT solver instance that is available in this context.
+ Solver &getSolver() const { return *Slvr; }
/// Takes ownership of `Loc` and returns a reference to it.
///
@@ -119,7 +130,28 @@
return Value ? TrueVal : FalseVal;
}
+ /// Creates an atomic boolean value.
+ AtomicBoolValue &createAtomicBoolValue() {
+ return takeOwnership(std::make_unique<AtomicBoolValue>());
+ }
+
+ /// 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.
+ ConjunctionValue &getOrCreateConjunctionValue(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.
+ DisjunctionValue &getOrCreateDisjunctionValue(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 &getOrCreateNegationValue(BoolValue &Val);
+
private:
+ std::unique_ptr<Solver> Slvr;
+
// Storage for the state of a program.
std::vector<std::unique_ptr<StorageLocation>> Locs;
std::vector<std::unique_ptr<Value>> Vals;
@@ -134,9 +166,15 @@
StorageLocation *ThisPointeeLoc = nullptr;
- // FIXME: Add support for boolean expressions.
AtomicBoolValue &TrueVal;
AtomicBoolValue &FalseVal;
+
+ // Caches that are used to avoid recreating the same composite boolean values.
+ llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
+ ConjunctionVals;
+ llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
+ DisjunctionVals;
+ llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
};
} // namespace dataflow
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
