https://github.com/ymand created
https://github.com/llvm/llvm-project/pull/152487
Adds support for compact serialization of Formulas, and a corresponding parse
function. Extends Environment and AnalysisContext with necessary functions for
serializing and deserializing all formula-related parts of the environment.
>From 2ae1efef000b6e0e6b758baf4f18f4599770838f Mon Sep 17 00:00:00 2001
From: Yitzhak Mandelbaum <yitzh...@google.com>
Date: Mon, 4 Aug 2025 18:09:28 +0000
Subject: [PATCH] [clang][dataflow] Add support for serialization and
deserialization.
Adds support for compact serialization of Formulas, and a corresponding parse
function. Extends Environment and AnalysisContext with necessary functions for
serializing and deserializing all formula-related parts of the environment.
---
.../FlowSensitive/DataflowAnalysisContext.h | 32 +++
.../FlowSensitive/DataflowEnvironment.h | 15 +-
.../clang/Analysis/FlowSensitive/Formula.h | 19 +-
.../FlowSensitive/FormulaSerialization.h | 40 ++++
.../lib/Analysis/FlowSensitive/CMakeLists.txt | 1 +
.../FlowSensitive/DataflowAnalysisContext.cpp | 23 +++
.../FlowSensitive/FormulaSerialization.cpp | 158 +++++++++++++++
.../Analysis/FlowSensitive/CMakeLists.txt | 1 +
.../DataflowAnalysisContextTest.cpp | 190 ++++++++++++++++++
.../Analysis/FlowSensitive/FormulaTest.cpp | 180 +++++++++++++++++
10 files changed, 647 insertions(+), 12 deletions(-)
create mode 100644
clang/include/clang/Analysis/FlowSensitive/FormulaSerialization.h
create mode 100644 clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp
create mode 100644 clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp
diff --git
a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index 5be4a1145f40d..17b80f0d01100 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -140,6 +140,15 @@ class DataflowAnalysisContext {
/// Adds `Constraint` to the flow condition identified by `Token`.
void addFlowConditionConstraint(Atom Token, const Formula &Constraint);
+ /// Adds `Deps` to the dependencies of the flow condition identified by
+ /// `Token`. Intended for use in deserializing contexts. The formula alone
+ /// doesn't have enough information to indicate its deps.
+ void addFlowConditionDeps(Atom Token, const llvm::DenseSet<Atom> &Deps) {
+ // Avoid creating an entry for `Token` with an empty set.
+ if (!Deps.empty())
+ FlowConditionDeps[Token].insert(Deps.begin(), Deps.end());
+ }
+
/// Creates a new flow condition with the same constraints as the flow
/// condition identified by `Token` and returns its token.
Atom forkFlowCondition(Atom Token);
@@ -177,6 +186,29 @@ class DataflowAnalysisContext {
Arena &arena() { return *A; }
+ const Formula *getInvariant() const { return Invariant; }
+
+ /// Returns null if no constraints are associated with `Token`.
+ const Formula *getFlowConditionConstraints(Atom Token) const {
+ auto ConstraintsIt = FlowConditionConstraints.find(Token);
+ if (ConstraintsIt == FlowConditionConstraints.end())
+ return nullptr;
+ return ConstraintsIt->second;
+ }
+
+ /// Returns null if no deps are found.
+ const llvm::DenseSet<Atom> *getFlowConditionDeps(Atom Token) const {
+ auto DepsIt = FlowConditionDeps.find(Token);
+ if (DepsIt == FlowConditionDeps.end())
+ return nullptr;
+ return &DepsIt->second;
+ }
+
+ /// Computes the transitive closure of reachable atoms from `Tokens`, through
+ /// the dependency graph.
+ llvm::DenseSet<Atom>
+ getTransitiveClosure(const llvm::DenseSet<Atom> &Tokens) const;
+
/// Returns the outcome of satisfiability checking on `Constraints`.
///
/// Flow conditions are not incorporated, so they may need to be manually
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
index 097ff2bdfe7ad..2266eff059d76 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -157,10 +157,19 @@ class Environment {
};
/// Creates an environment that uses `DACtx` to store objects that encompass
- /// the state of a program.
- explicit Environment(DataflowAnalysisContext &DACtx)
+ /// the state of a program. `FlowConditionToken` sets the flow condition
+ /// associated with the environment. Generally, new environments should be
+ /// initialized with a fresh token, by using one of the other
+ /// constructors. This constructor is for specialized use, including
+ /// deserialization and delegation from other constructors.
+ Environment(DataflowAnalysisContext &DACtx, Atom FlowConditionToken)
: DACtx(&DACtx),
- FlowConditionToken(DACtx.arena().makeFlowConditionToken()) {}
+ FlowConditionToken(FlowConditionToken) {}
+
+ /// Creates an environment that uses `DACtx` to store objects that encompass
+ /// the state of a program. Populates a fresh atom as flow condition token.
+ explicit Environment(DataflowAnalysisContext &DACtx)
+ : Environment(DACtx, DACtx.arena().makeFlowConditionToken()) {}
/// Creates an environment that uses `DACtx` to store objects that encompass
/// the state of a program, with `S` as the statement to analyze.
diff --git a/clang/include/clang/Analysis/FlowSensitive/Formula.h
b/clang/include/clang/Analysis/FlowSensitive/Formula.h
index 0e6352403a832..3959bc98619b9 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Formula.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Formula.h
@@ -85,21 +85,17 @@ class alignas(const Formula *) Formula {
}
using AtomNames = llvm::DenseMap<Atom, std::string>;
- // Produce a stable human-readable representation of this formula.
- // For example: (V3 | !(V1 & V2))
- // If AtomNames is provided, these override the default V0, V1... names.
+ /// Produces a stable human-readable representation of this formula.
+ /// For example: (V3 | !(V1 & V2))
+ /// If AtomNames is provided, these override the default V0, V1... names.
void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
- // Allocate Formulas using Arena rather than calling this function directly.
+ /// Allocates Formulas using Arena rather than calling this function
directly.
static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
ArrayRef<const Formula *> Operands,
unsigned Value = 0);
-private:
- Formula() = default;
- Formula(const Formula &) = delete;
- Formula &operator=(const Formula &) = delete;
-
+ /// Count of operands (sub-formulas) associated with Formulas of kind `K`.
static unsigned numOperands(Kind K) {
switch (K) {
case AtomRef:
@@ -116,6 +112,11 @@ class alignas(const Formula *) Formula {
llvm_unreachable("Unhandled Formula::Kind enum");
}
+private:
+ Formula() = default;
+ Formula(const Formula &) = delete;
+ Formula &operator=(const Formula &) = delete;
+
Kind FormulaKind;
// Some kinds of formula have scalar values, e.g. AtomRef's atom number.
unsigned Value;
diff --git a/clang/include/clang/Analysis/FlowSensitive/FormulaSerialization.h
b/clang/include/clang/Analysis/FlowSensitive/FormulaSerialization.h
new file mode 100644
index 0000000000000..f72954d2110c3
--- /dev/null
+++ b/clang/include/clang/Analysis/FlowSensitive/FormulaSerialization.h
@@ -0,0 +1,40 @@
+//=== FormulaSerialization.h - Formula De/Serialization support -*- 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
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_SERIALIZATION_H
+#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_SERIALIZATION_H
+
+#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Basic/LLVM.h"
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/DenseMapInfo.h"
+#include "llvm/Support/Allocator.h"
+#include "llvm/Support/raw_ostream.h"
+#include <cassert>
+#include <string>
+
+namespace clang::dataflow {
+
+///
+void serializeFormula(const Formula& F, llvm::raw_ostream &OS);
+
+/// Parses `Str` to build a serialized Formula.
+/// @returns error on parse failure or if parsing does not fully consume `Str`.
+/// @param A used to construct the formula components.
+/// @param AtomMap maps serialized Atom identifiers (unsigned ints) to Atoms.
+/// This map is provided by the caller to enable consistency across
+/// multiple formulas in a single file.
+llvm::Expected<const Formula *>
+parseFormula(llvm::StringRef Str, Arena &A,
+ llvm::DenseMap<unsigned, Atom> &AtomMap);
+
+
+} // namespace clang::dataflow
+#endif
diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
index 0c30df8b4b194..97e09c9bce95f 100644
--- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -6,6 +6,7 @@ add_clang_library(clangAnalysisFlowSensitive
DataflowAnalysisContext.cpp
DataflowEnvironment.cpp
Formula.cpp
+ FormulaSerialization.cpp
HTMLLogger.cpp
Logger.cpp
RecordOps.cpp
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 6421ad3883d10..97914023ee79e 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -208,6 +208,27 @@ bool DataflowAnalysisContext::equivalentFormulas(const
Formula &Val1,
return isUnsatisfiable(std::move(Constraints));
}
+llvm::DenseSet<Atom> DataflowAnalysisContext::getTransitiveClosure(
+ const llvm::DenseSet<Atom> &Tokens) const {
+ llvm::DenseSet<Atom> VisitedTokens;
+ // Use a worklist algorithm, with `Remaining` holding the worklist.
+ std::vector<Atom> Remaining(Tokens.begin(), Tokens.end());
+
+ // For each token in `Remaining`, add its dependencies to the worklist.
+ while (!Remaining.empty()) {
+ auto Token = Remaining.back();
+ Remaining.pop_back();
+ if (!VisitedTokens.insert(Token).second)
+ continue;
+ if (auto DepsIt = FlowConditionDeps.find(Token);
+ DepsIt != FlowConditionDeps.end())
+ for (Atom A : DepsIt->second)
+ Remaining.push_back(A);
+ }
+
+ return VisitedTokens;
+}
+
void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
Atom Token, llvm::SetVector<const Formula *> &Constraints) {
llvm::DenseSet<Atom> AddedTokens;
@@ -224,6 +245,8 @@ void
DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
auto ConstraintsIt = FlowConditionConstraints.find(Token);
if (ConstraintsIt == FlowConditionConstraints.end()) {
+ // The flow condition is unconstrained. Just add the atom directly, which
+ // is equivalent to asserting it is true.
Constraints.insert(&arena().makeAtomRef(Token));
} else {
// Bind flow condition token via `iff` to its set of constraints:
diff --git a/clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp
b/clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp
new file mode 100644
index 0000000000000..12c92636dc7a9
--- /dev/null
+++ b/clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp
@@ -0,0 +1,158 @@
+//===- Formula.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
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Analysis/FlowSensitive/FormulaSerialization.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "clang/Basic/LLVM.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Allocator.h"
+#include "llvm/Support/Error.h"
+#include "llvm/Support/ErrorHandling.h"
+#include <cassert>
+
+namespace clang::dataflow {
+
+static char compactSigil(Formula::Kind K) {
+ switch (K) {
+ case Formula::AtomRef:
+ case Formula::Literal:
+ return '\0';
+ case Formula::Not:
+ return '!';
+ case Formula::And:
+ return '&';
+ case Formula::Or:
+ return '|';
+ case Formula::Implies:
+ return '>';
+ case Formula::Equal:
+ return '=';
+ }
+ llvm_unreachable("unhandled formula kind");
+}
+
+void serializeFormula(const Formula &F, llvm::raw_ostream &OS) {
+ switch (Formula::numOperands(F.kind())) {
+ case 0:
+ switch (F.kind()) {
+ case Formula::AtomRef:
+ OS << F.getAtom();
+ break;
+ case Formula::Literal:
+ OS << (F.literal() ? 'T' : 'F');
+ break;
+ default:
+ llvm_unreachable("unhandled formula kind");
+ }
+ break;
+ case 1:
+ OS << compactSigil(F.kind());
+ serializeFormula(*F.operands()[0], OS);
+ break;
+ case 2:
+ OS << compactSigil(F.kind());
+ serializeFormula(*F.operands()[0], OS);
+ serializeFormula(*F.operands()[1], OS);
+ break;
+ default:
+ llvm_unreachable("unhandled formula arity");
+ }
+}
+
+static llvm::Expected<const Formula *>
+parsePrefix(llvm::StringRef &Str, Arena &A,
+ llvm::DenseMap<unsigned, Atom> &AtomMap) {
+ if (Str.empty())
+ return llvm::createStringError(llvm::inconvertibleErrorCode(),
+ "unexpected end of input");
+
+ char Prefix = Str[0];
+ Str = Str.drop_front();
+
+ switch (Prefix) {
+ case 'T':
+ return &A.makeLiteral(true);
+ case 'F':
+ return &A.makeLiteral(false);
+ case 'V': {
+ unsigned AtomID;
+ if (Str.consumeInteger(10, AtomID))
+ return llvm::createStringError(llvm::inconvertibleErrorCode(),
+ "expected atom id");
+ auto [It, Inserted] = AtomMap.try_emplace(AtomID, Atom());
+ if (Inserted)
+ It->second = A.makeAtom();
+ return &A.makeAtomRef(It->second);
+ }
+ case '!': {
+ auto OperandOrErr = parsePrefix(Str, A, AtomMap);
+ if (!OperandOrErr)
+ return OperandOrErr.takeError();
+ return &A.makeNot(**OperandOrErr);
+ }
+ case '&': {
+ auto LeftOrErr = parsePrefix(Str, A, AtomMap);
+ if (!LeftOrErr)
+ return LeftOrErr.takeError();
+ auto RightOrErr = parsePrefix(Str, A, AtomMap);
+ if (!RightOrErr)
+ return RightOrErr.takeError();
+ return &A.makeAnd(**LeftOrErr, **RightOrErr);
+ }
+ case '|': {
+ auto LeftOrErr = parsePrefix(Str, A, AtomMap);
+ if (!LeftOrErr)
+ return LeftOrErr.takeError();
+ auto RightOrErr = parsePrefix(Str, A, AtomMap);
+ if (!RightOrErr)
+ return RightOrErr.takeError();
+ return &A.makeOr(**LeftOrErr, **RightOrErr);
+ }
+ case '>': {
+ auto LeftOrErr = parsePrefix(Str, A, AtomMap);
+ if (!LeftOrErr)
+ return LeftOrErr.takeError();
+ auto RightOrErr = parsePrefix(Str, A, AtomMap);
+ if (!RightOrErr)
+ return RightOrErr.takeError();
+ return &A.makeImplies(**LeftOrErr, **RightOrErr);
+ }
+ case '=': {
+ auto LeftOrErr = parsePrefix(Str, A, AtomMap);
+ if (!LeftOrErr)
+ return LeftOrErr.takeError();
+ auto RightOrErr = parsePrefix(Str, A, AtomMap);
+ if (!RightOrErr)
+ return RightOrErr.takeError();
+ return &A.makeEquals(**LeftOrErr, **RightOrErr);
+ }
+ default:
+ return llvm::createStringError(llvm::inconvertibleErrorCode(),
+ "unexpected prefix character");
+ }
+}
+
+llvm::Expected<const Formula *>
+parseFormula(llvm::StringRef Str, Arena &A,
+ llvm::DenseMap<unsigned, Atom> &AtomMap) {
+ size_t OriginalSize = Str.size();
+ llvm::Expected<const Formula *> F = parsePrefix(Str, A, AtomMap);
+ if (!F)
+ return F.takeError();
+ if (!Str.empty())
+ return llvm::createStringError(llvm::inconvertibleErrorCode(),
+ ("unexpected suffix of length: " +
+ llvm::Twine(Str.size() - OriginalSize))
+ .str());
+ return F;
+}
+
+} // namespace clang::dataflow
diff --git a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
index 4ac563143cd68..3bd4a6e21bee7 100644
--- a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
@@ -8,6 +8,7 @@ add_clang_unittest(ClangAnalysisFlowSensitiveTests
DataflowEnvironmentTest.cpp
DebugSupportTest.cpp
DeterminismTest.cpp
+ FormulaTest.cpp
LoggerTest.cpp
MapLatticeTest.cpp
MatchSwitchTest.cpp
diff --git
a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
index 4f7a72c502ccf..052d35343868b 100644
--- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -17,6 +17,9 @@ namespace {
using namespace clang;
using namespace dataflow;
+using ::testing::UnorderedElementsAre;
+using ::testing::IsEmpty;
+
class DataflowAnalysisContextTest : public ::testing::Test {
protected:
DataflowAnalysisContextTest()
@@ -77,6 +80,14 @@ TEST_F(DataflowAnalysisContextTest, AddInvariant) {
EXPECT_TRUE(Context.flowConditionImplies(FC, C));
}
+TEST_F(DataflowAnalysisContextTest, GetInvariant) {
+ auto &C = A.makeAtomRef(A.makeAtom());
+ Context.addInvariant(C);
+ const Formula *Inv = Context.getInvariant();
+ ASSERT_NE(Inv, nullptr);
+ EXPECT_TRUE(Context.equivalentFormulas(*Inv, C));
+}
+
TEST_F(DataflowAnalysisContextTest, InvariantAndFCConstraintInteract) {
Atom FC = A.makeFlowConditionToken();
auto &C = A.makeAtomRef(A.makeAtom());
@@ -123,6 +134,28 @@ TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));
}
+TEST_F(DataflowAnalysisContextTest, GetFlowConditionConstraints) {
+ auto &C1 = A.makeAtomRef(A.makeAtom());
+ auto &C2 = A.makeAtomRef(A.makeAtom());
+ auto &C3 = A.makeAtomRef(A.makeAtom());
+
+ Atom FC1 = A.makeFlowConditionToken();
+ Context.addFlowConditionConstraint(FC1, C1);
+ Context.addFlowConditionConstraint(FC1, C3);
+
+ Atom FC2 = A.makeFlowConditionToken();
+ Context.addFlowConditionConstraint(FC2, C2);
+ Context.addFlowConditionConstraint(FC2, C3);
+
+ const Formula *CS1 = Context.getFlowConditionConstraints(FC1);
+ ASSERT_NE(CS1, nullptr);
+ EXPECT_TRUE(Context.equivalentFormulas(*CS1, A.makeAnd(C1,C3)));
+
+ const Formula *CS2 = Context.getFlowConditionConstraints(FC2);
+ ASSERT_NE(CS2, nullptr);
+ EXPECT_TRUE(Context.equivalentFormulas(*CS2, A.makeAnd(C2,C3)));
+}
+
TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
auto &X = A.makeAtomRef(A.makeAtom());
auto &Y = A.makeAtomRef(A.makeAtom());
@@ -171,4 +204,161 @@ TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
A.makeAnd(X, A.makeAnd(Y, Z))));
}
+using FlowConditionDepsTest = DataflowAnalysisContextTest;
+
+TEST_F(FlowConditionDepsTest, AddEmptyDeps) {
+ Atom FC1 = A.makeFlowConditionToken();
+
+ // Add empty dependencies to FC1.
+ Context.addFlowConditionDeps(FC1, {});
+
+ // Verify that FC1 has no dependencies.
+ EXPECT_EQ(Context.getFlowConditionDeps(FC1), nullptr);
+}
+
+TEST_F(FlowConditionDepsTest, AddAndGetDeps) {
+ Atom FC1 = A.makeFlowConditionToken();
+ Atom FC2 = A.makeFlowConditionToken();
+ Atom FC3 = A.makeFlowConditionToken();
+
+ // Add dependencies: FC1 depends on FC2 and FC3.
+ Context.addFlowConditionDeps(FC1, {FC2, FC3});
+
+ // Verify that FC1 depends on FC2 and FC3.
+ const llvm::DenseSet<Atom> *Deps = Context.getFlowConditionDeps(FC1);
+ ASSERT_NE(Deps, nullptr);
+ EXPECT_THAT(*Deps, UnorderedElementsAre(FC2, FC3));
+
+ // Verify that FC2 and FC3 have no dependencies.
+ EXPECT_EQ(Context.getFlowConditionDeps(FC2), nullptr);
+ EXPECT_EQ(Context.getFlowConditionDeps(FC3), nullptr);
+}
+
+TEST_F(FlowConditionDepsTest, AddDepsToExisting) {
+ Atom FC1 = A.makeFlowConditionToken();
+ Atom FC2 = A.makeFlowConditionToken();
+ Atom FC3 = A.makeFlowConditionToken();
+
+ // Add initial dependency: FC1 depends on FC2.
+ Context.addFlowConditionDeps(FC1, {FC2});
+
+ // Add more dependencies: FC1 depends on FC2 and FC3.
+ Context.addFlowConditionDeps(FC1, {FC3});
+
+ // Verify that FC1 depends on FC2 and FC3.
+ const llvm::DenseSet<Atom> *Deps = Context.getFlowConditionDeps(FC1);
+ ASSERT_NE(Deps, nullptr);
+ EXPECT_THAT(*Deps, UnorderedElementsAre(FC2, FC3));
+}
+
+using GetTransitiveClosureTest = DataflowAnalysisContextTest;
+
+TEST_F(GetTransitiveClosureTest, EmptySet) {
+ EXPECT_THAT(Context.getTransitiveClosure({}), IsEmpty());
+}
+
+TEST_F(GetTransitiveClosureTest, SingletonSet) {
+ Atom FC1 = A.makeFlowConditionToken();
+ EXPECT_THAT(Context.getTransitiveClosure({FC1}), UnorderedElementsAre(FC1));
+}
+
+TEST_F(GetTransitiveClosureTest, NoDependency) {
+ Atom FC1 = A.makeFlowConditionToken();
+ Atom FC2 = A.makeFlowConditionToken();
+ Atom FC3 = A.makeFlowConditionToken();
+ auto &C1 = A.makeAtomRef(A.makeAtom());
+ auto &C2 = A.makeAtomRef(A.makeAtom());
+ auto &C3 = A.makeAtomRef(A.makeAtom());
+
+ Context.addFlowConditionConstraint(FC1, C1);
+ Context.addFlowConditionConstraint(FC2, C2);
+ Context.addFlowConditionConstraint(FC3, C3);
+
+ // FCs are independent.
+ EXPECT_THAT(Context.getTransitiveClosure({FC1}), UnorderedElementsAre(FC1));
+ EXPECT_THAT(Context.getTransitiveClosure({FC2}), UnorderedElementsAre(FC2));
+ EXPECT_THAT(Context.getTransitiveClosure({FC3}), UnorderedElementsAre(FC3));
+}
+
+TEST_F(GetTransitiveClosureTest, SimpleDependencyChain) {
+ Atom FC1 = A.makeFlowConditionToken();
+ Atom FC2 = A.makeFlowConditionToken();
+ Atom FC3 = A.makeFlowConditionToken();
+
+ Context.addFlowConditionConstraint(FC1, A.makeAtomRef(FC2));
+ Context.addFlowConditionDeps(FC1, {FC2});
+
+ Context.addFlowConditionConstraint(FC2, A.makeAtomRef(FC3));
+ Context.addFlowConditionDeps(FC2, {FC3});
+
+ EXPECT_THAT(Context.getTransitiveClosure({FC1}),
+ UnorderedElementsAre(FC1, FC2, FC3));
+}
+
+
+TEST_F(GetTransitiveClosureTest, DependencyTree) {
+ Atom FC1 = A.makeFlowConditionToken();
+ Atom FC2 = A.makeFlowConditionToken();
+ Atom FC3 = A.makeFlowConditionToken();
+ Atom FC4 = A.makeFlowConditionToken();
+
+ Context.addFlowConditionDeps(FC1, {FC2, FC3});
+ Context.addFlowConditionConstraint(
+ FC1, A.makeAnd(A.makeAtomRef(FC2), A.makeAtomRef(FC3)));
+
+ Context.addFlowConditionDeps(FC2, {FC4});
+ Context.addFlowConditionConstraint(FC2, A.makeAtomRef(FC4));
+
+ EXPECT_THAT(Context.getTransitiveClosure({FC1}),
+ UnorderedElementsAre(FC1, FC2, FC3, FC4));
+}
+
+TEST_F(GetTransitiveClosureTest, DependencyDAG) {
+ Atom FC1 = A.makeFlowConditionToken();
+ Atom FC2 = A.makeFlowConditionToken();
+ Atom FC3 = A.makeFlowConditionToken();
+ Atom FC4 = A.makeFlowConditionToken();
+
+ Context.addFlowConditionDeps(FC1, {FC2, FC3});
+ Context.addFlowConditionConstraint(
+ FC1, A.makeAnd(A.makeAtomRef(FC2), A.makeAtomRef(FC3)));
+
+ Context.addFlowConditionDeps(FC2, {FC4});
+ Context.addFlowConditionConstraint(FC2, A.makeAtomRef(FC4));
+
+ Context.addFlowConditionDeps(FC3, {FC4});
+ Context.addFlowConditionConstraint(FC3, A.makeAtomRef(FC4));
+
+ EXPECT_THAT(Context.getTransitiveClosure({FC1}),
+ UnorderedElementsAre(FC1, FC2, FC3, FC4));
+}
+
+TEST_F(GetTransitiveClosureTest, DependencyCycle) {
+ Atom FC1 = A.makeFlowConditionToken();
+ Atom FC2 = A.makeFlowConditionToken();
+ Atom FC3 = A.makeFlowConditionToken();
+
+ Context.addFlowConditionDeps(FC1, {FC2});
+ Context.addFlowConditionConstraint(FC1, A.makeAtomRef(FC2));
+ Context.addFlowConditionDeps(FC2, {FC3});
+ Context.addFlowConditionConstraint(FC2, A.makeAtomRef(FC3));
+ Context.addFlowConditionDeps(FC3, {FC1});
+ Context.addFlowConditionConstraint(FC3, A.makeAtomRef(FC1));
+
+ EXPECT_THAT(Context.getTransitiveClosure({FC1}),
+ UnorderedElementsAre(FC1, FC2, FC3));
+}
+
+TEST_F(GetTransitiveClosureTest, MixedDependencies) {
+ Atom FC1 = A.makeFlowConditionToken();
+ Atom FC2 = A.makeFlowConditionToken();
+ Atom FC3 = A.makeFlowConditionToken();
+ Atom FC4 = A.makeFlowConditionToken();
+
+ Context.addFlowConditionDeps(FC1, {FC2});
+ Context.addFlowConditionConstraint(FC1, A.makeAtomRef(FC2));
+
+ EXPECT_THAT(Context.getTransitiveClosure({FC1, FC3, FC4}),
+ UnorderedElementsAre(FC1, FC2, FC3, FC4));
+}
} // namespace
diff --git a/clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp
b/clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp
new file mode 100644
index 0000000000000..1d6db3cc60ade
--- /dev/null
+++ b/clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp
@@ -0,0 +1,180 @@
+//===- unittests/Analysis/FlowSensitive/FormulaTest.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/Formula.h"
+#include "TestingSupport.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "clang/Analysis/FlowSensitive/FormulaSerialization.h"
+#include "llvm/Support/raw_ostream.h"
+#include "llvm/Testing/Support/Error.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+
+namespace {
+
+using namespace clang;
+using namespace dataflow;
+
+using ::llvm::HasValue;
+using ::testing::ElementsAre;
+using ::testing::IsEmpty;
+
+class SerializeFormulaTest : public ::testing::Test {
+protected:
+ Arena A;
+ std::string Out;
+ llvm::raw_string_ostream OS{Out};
+
+ const Formula &A1 = A.makeAtomRef(A.makeAtom());
+ const Formula &A2 = A.makeAtomRef(A.makeAtom());
+};
+
+TEST_F(SerializeFormulaTest, Atom) {
+ serializeFormula(A1, OS);
+ EXPECT_EQ(Out, "V0");
+ Out = "";
+
+ serializeFormula(A2, OS);
+ EXPECT_EQ(Out, "V1");
+}
+
+TEST_F(SerializeFormulaTest, LiteralTrue) {
+ serializeFormula(A.makeLiteral(true), OS);
+ EXPECT_EQ(Out, "T");
+}
+
+TEST_F(SerializeFormulaTest, LiteralFalse) {
+ serializeFormula(A.makeLiteral(false), OS);
+ EXPECT_EQ(Out, "F");
+}
+
+TEST_F(SerializeFormulaTest, Not) {
+ serializeFormula(A.makeNot(A1), OS);
+ EXPECT_EQ(Out, "!V0");
+}
+
+TEST_F(SerializeFormulaTest, Or) {
+ serializeFormula(A.makeOr(A1,A2), OS);
+ EXPECT_EQ(Out, "|V0V1");
+}
+
+TEST_F(SerializeFormulaTest, And) {
+ serializeFormula(A.makeAnd(A1,A2), OS);
+ EXPECT_EQ(Out, "&V0V1");
+}
+
+TEST_F(SerializeFormulaTest, Implies) {
+ serializeFormula(A.makeImplies(A1,A2), OS);
+ EXPECT_EQ(Out, ">V0V1");
+}
+
+TEST_F(SerializeFormulaTest, Equal) {
+ serializeFormula(A.makeEquals(A1,A2), OS);
+ EXPECT_EQ(Out, "=V0V1");
+}
+
+TEST_F(SerializeFormulaTest, NestedBinaryUnary) {
+ serializeFormula(A.makeEquals(A.makeOr(A1,A2),A2), OS);
+ EXPECT_EQ(Out, "=|V0V1V1");
+}
+
+TEST_F(SerializeFormulaTest, NestedBinaryBinary) {
+ serializeFormula(A.makeEquals(A.makeOr(A1,A2),A.makeAnd(A1,A2)), OS);
+ EXPECT_EQ(Out, "=|V0V1&V0V1");
+}
+
+class ParseFormulaTest : public ::testing::Test {
+protected:
+ void SetUp() override {
+ AtomMap[0] = Atom1;
+ AtomMap[1] = Atom2;
+ }
+
+ Arena A;
+ std::string Out;
+ llvm::raw_string_ostream OS{Out};
+
+ Atom Atom1 = A.makeAtom();
+ Atom Atom2 = A.makeAtom();
+ const Formula &A1 = A.makeAtomRef(Atom1);
+ const Formula &A2 = A.makeAtomRef(Atom2);
+ llvm::DenseMap<unsigned, Atom> AtomMap;
+};
+
+TEST_F(ParseFormulaTest, Atom) {
+ EXPECT_THAT_EXPECTED(parseFormula( "V0", A, AtomMap), HasValue(&A1));
+ EXPECT_THAT_EXPECTED(parseFormula( "V1", A, AtomMap), HasValue(&A2));
+}
+
+TEST_F(ParseFormulaTest, LiteralTrue) {
+ EXPECT_THAT_EXPECTED(parseFormula("T", A, AtomMap),
+ HasValue(&A.makeLiteral(true)));
+}
+
+TEST_F(ParseFormulaTest, LiteralFalse) {
+ EXPECT_THAT_EXPECTED(parseFormula("F", A, AtomMap),
+ HasValue(&A.makeLiteral(false)));
+}
+
+TEST_F(ParseFormulaTest, Not) {
+ EXPECT_THAT_EXPECTED(parseFormula("!V0", A, AtomMap),
+ HasValue(&A.makeNot(A1)));
+}
+
+TEST_F(ParseFormulaTest, Or) {
+ EXPECT_THAT_EXPECTED(parseFormula("|V0V1", A, AtomMap),
+ HasValue(&A.makeOr(A1,A2)));
+}
+
+TEST_F(ParseFormulaTest, And) {
+ EXPECT_THAT_EXPECTED(parseFormula("&V0V1", A, AtomMap),
+ HasValue(&A.makeAnd(A1,A2)));
+}
+
+TEST_F(ParseFormulaTest, Implies) {
+ EXPECT_THAT_EXPECTED(parseFormula(">V0V1", A, AtomMap),
+ HasValue(&A.makeImplies(A1,A2)));
+}
+
+TEST_F(ParseFormulaTest, Equal) {
+ EXPECT_THAT_EXPECTED(parseFormula("=V0V1", A, AtomMap),
+ HasValue(&A.makeEquals(A1,A2)));
+}
+
+TEST_F(ParseFormulaTest, NestedBinaryUnary) {
+ EXPECT_THAT_EXPECTED(parseFormula("=|V0V1V1", A, AtomMap),
+ HasValue(&A.makeEquals(A.makeOr(A1,A2),A2)));
+}
+
+TEST_F(ParseFormulaTest, NestedBinaryBinary) {
+ EXPECT_THAT_EXPECTED(
+ parseFormula("=|V0V1&V0V1", A, AtomMap),
+ HasValue(&A.makeEquals(A.makeOr(A1, A2), A.makeAnd(A1, A2))));
+}
+
+// Verifies that parsing generates fresh atoms, if they are not already in the
+// map.
+TEST_F(ParseFormulaTest, GeneratesAtoms) {
+ llvm::DenseMap<unsigned, Atom> FreshAtomMap;
+ ASSERT_THAT_EXPECTED(parseFormula("=V0V1", A, FreshAtomMap),
+ llvm::Succeeded());
+ // The map contains two, unique elements.
+ ASSERT_EQ(FreshAtomMap.size(), 2U);
+ EXPECT_NE(FreshAtomMap[0], FreshAtomMap[1]);
+}
+
+TEST_F(ParseFormulaTest, BadFormulaFails) {
+ EXPECT_THAT_EXPECTED(parseFormula("Hello", A, AtomMap), llvm::Failed());
+}
+
+TEST_F(ParseFormulaTest, FormulaWithSuffixFails) {
+ EXPECT_THAT_EXPECTED(parseFormula("=V0V1Hello", A, AtomMap), llvm::Failed());
+}
+
+
+} // namespace
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
