This is part of the implementation of the dataflow analysis framework.
See "[RFC] A dataflow analysis framework for Clang AST" on cfe-dev.
Reviewed-by: ymandel, xazax.hun
Differential Revision: https://reviews.llvm.org/D120711
#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"
/// 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:
+ ///
+ /// `S` must not be null.
+ DataflowAnalysisContext(std::unique_ptr<Solver> S)
+ : S(std::move(S)), TrueVal(createAtomicBoolValue()),
+ FalseVal(createAtomicBoolValue()) {
+ assert(this->S != nullptr);
+ }
+
+ /// Returns the SAT solver instance that is available in this context.
+ Solver &getSolver() const { return *S; }
/// Takes ownership of `Loc` and returns a reference to it.
///
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. If the given boolean values represent
+ /// the same value, the result will be the value itself.
+ BoolValue &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. If the given boolean values represent
+ /// the same value, the result will be the value itself.
+ BoolValue &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> S;
+
// Storage for the state of a program.
std::vector<std::unique_ptr<StorageLocation>> Locs;
std::vector<std::unique_ptr<Value>> Vals;
StorageLocation *ThisPointeeLoc = nullptr;
- // FIXME: Add support for boolean expressions.
AtomicBoolValue &TrueVal;
AtomicBoolValue &FalseVal;
+
+ // Indices 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
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`. 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) {
+ return DACtx->getOrCreateConjunctionValue(LHS, 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) {
+ return DACtx->getOrCreateDisjunctionValue(LHS, 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) {
+ return DACtx->getOrCreateNegationValue(Val);
+ }
+
+ /// Returns a boolean value 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 &makeImplication(BoolValue &LHS, BoolValue &RHS) {
+ return &LHS == &RHS ? getBoolLiteralValue(true) : makeOr(makeNot(LHS), RHS);
+ }
+
+ /// Returns a boolean value 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 &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.
std::pair<StructValue *, const ValueDecl *>>
MemberLocToStruct;
- // FIXME: Add flow condition constraints.
+ llvm::DenseSet<BoolValue *> FlowConditionConstraints;
};
} // namespace dataflow
add_clang_library(clangAnalysisFlowSensitive
ControlFlowContext.cpp
+ DataflowAnalysisContext.cpp
DataflowEnvironment.cpp
Transfer.cpp
TypeErasedDataflowAnalysis.cpp
--- /dev/null
+//===-- 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>
+#include <utility>
+
+namespace clang {
+namespace dataflow {
+
+static std::pair<BoolValue *, BoolValue *>
+makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
+ auto Res = std::make_pair(&LHS, &RHS);
+ if (&RHS < &LHS)
+ std::swap(Res.first, Res.second);
+ return Res;
+}
+
+BoolValue &
+DataflowAnalysisContext::getOrCreateConjunctionValue(BoolValue &LHS,
+ BoolValue &RHS) {
+ if (&LHS == &RHS)
+ return LHS;
+
+ auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+ nullptr);
+ if (Res.second)
+ Res.first->second =
+ &takeOwnership(std::make_unique<ConjunctionValue>(LHS, RHS));
+ return *Res.first->second;
+}
+
+BoolValue &
+DataflowAnalysisContext::getOrCreateDisjunctionValue(BoolValue &LHS,
+ BoolValue &RHS) {
+ if (&LHS == &RHS)
+ return LHS;
+
+ auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+ nullptr);
+ if (Res.second)
+ Res.first->second =
+ &takeOwnership(std::make_unique<DisjunctionValue>(LHS, RHS));
+ return *Res.first->second;
+}
+
+BoolValue &DataflowAnalysisContext::getOrCreateNegationValue(BoolValue &Val) {
+ auto Res = NegationVals.try_emplace(&Val, nullptr);
+ if (Res.second)
+ Res.first->second = &takeOwnership(std::make_unique<NegationValue>(Val));
+ return *Res.first->second;
+}
+
+} // namespace dataflow
+} // namespace clang
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
)
add_clang_unittest(ClangAnalysisFlowSensitiveTests
+ DataflowAnalysisContextTest.cpp
+ DataflowEnvironmentTest.cpp
MapLatticeTest.cpp
MultiVarConstantPropagationTest.cpp
SingleVarConstantPropagationTest.cpp
--- /dev/null
+//===- 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,
+ CreateAtomicBoolValueReturnsDistinctValues) {
+ auto &X = Context.createAtomicBoolValue();
+ auto &Y = Context.createAtomicBoolValue();
+ EXPECT_NE(&X, &Y);
+}
+
+TEST_F(DataflowAnalysisContextTest,
+ GetOrCreateConjunctionValueReturnsSameExprGivenSameArgs) {
+ auto &X = Context.createAtomicBoolValue();
+ auto &XAndX = Context.getOrCreateConjunctionValue(X, X);
+ EXPECT_EQ(&XAndX, &X);
+}
+
+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,
+ GetOrCreateDisjunctionValueReturnsSameExprGivenSameArgs) {
+ auto &X = Context.createAtomicBoolValue();
+ auto &XOrX = Context.getOrCreateDisjunctionValue(X, X);
+ EXPECT_EQ(&XOrX, &X);
+}
+
+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
--- /dev/null
+//===- unittests/Analysis/FlowSensitive/DataflowEnvironmentTest.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, 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
#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"
if (!CFCtx)
return CFCtx.takeError();
- DataflowAnalysisContext DACtx;
+ DataflowAnalysisContext DACtx(std::make_unique<WatchedLiteralsSolver>());
Environment Env(DACtx, *F);
auto Analysis = MakeAnalysis(Context, Env);
#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"
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);