https://github.com/ymand updated
https://github.com/llvm/llvm-project/pull/152487
>From a39ac4fe8bdd337ca03651ca70879392b00cdfca Mon Sep 17 00:00:00 2001
From: Yitzhak Mandelbaum <yitzh...@google.com>
Date: Mon, 4 Aug 2025 18:09:28 +0000
Subject: [PATCH 1/3] [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 | 14 +-
.../clang/Analysis/FlowSensitive/Formula.h | 19 +-
.../FlowSensitive/FormulaSerialization.h | 40 ++++
.../lib/Analysis/FlowSensitive/CMakeLists.txt | 1 +
.../FlowSensitive/DataflowAnalysisContext.cpp | 23 +++
.../FlowSensitive/FormulaSerialization.cpp | 161 +++++++++++++++
.../Analysis/FlowSensitive/CMakeLists.txt | 1 +
.../DataflowAnalysisContextTest.cpp | 189 ++++++++++++++++++
.../Analysis/FlowSensitive/FormulaTest.cpp | 179 +++++++++++++++++
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..076714462bb2a 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -157,10 +157,18 @@ class Environment {
};
/// Creates an environment that uses `DACtx` to store objects that encompass
- /// the state of a program.
+ /// 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(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)
- : DACtx(&DACtx),
- FlowConditionToken(DACtx.arena().makeFlowConditionToken()) {}
+ : 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..119f93e5d73f6
--- /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 {
+
+/// Prints `F` to `OS` in a compact format, optimized for easy parsing
+/// (deserialization) rather than human use.
+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..56cbf5aba8e55
--- /dev/null
+++ b/clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp
@@ -0,0 +1,161 @@
+//===- FormulaSerialization.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/FormulaSerialization.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "clang/Analysis/FlowSensitive/Formula.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 {
+
+// Returns the leading indicator of operation formulas. `AtomRef` and `Literal`
+// are handled differently.
+static char compactSigil(Formula::Kind K) {
+ switch (K) {
+ case Formula::AtomRef:
+ case Formula::Literal:
+ // No sigil.
+ 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..07323952b3e67 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::IsEmpty;
+using ::testing::UnorderedElementsAre;
+
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,160 @@ 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..49c02a8f192f2
--- /dev/null
+++ b/clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp
@@ -0,0 +1,179 @@
+//===- 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
>From 08b0b10595561bafca91a88d8ec142d04cf89425 Mon Sep 17 00:00:00 2001
From: Yitzhak Mandelbaum <yitzh...@google.com>
Date: Sun, 10 Aug 2025 04:00:32 +0000
Subject: [PATCH 2/3] fixup! [clang][dataflow] Add support for serialization
and deserialization.
rework to use explicit serialization functions
---
.../FlowSensitive/DataflowAnalysisContext.h | 48 ++---
.../FlowSensitive/DataflowAnalysisContext.cpp | 59 ++++++
.../DataflowAnalysisContextTest.cpp | 187 +++++-------------
3 files changed, 131 insertions(+), 163 deletions(-)
diff --git
a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index 17b80f0d01100..a03bfe058061e 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -42,6 +42,18 @@ struct ContextSensitiveOptions {
unsigned Depth = 2;
};
+/// A simple representation of essential elements of the logical context used
in
+/// environments. Designed for import/export for applications requiring
+/// serialization support.
+struct SimpleLogicalContext {
+ // Global invariant that applies for all definitions in the context.
+ const Formula *Invariant;
+ // Flow-condition tokens in the context.
+ llvm::DenseMap<Atom, const Formula *> TokenDefs;
+ // Dependencies between flow-condition definitions.
+ llvm::DenseMap<Atom, llvm::DenseSet<Atom>> TokenDeps;
+};
+
/// Owns objects that encompass the state of a program and stores context that
/// is used during dataflow analysis.
class DataflowAnalysisContext {
@@ -186,29 +198,6 @@ 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
@@ -239,6 +228,14 @@ class DataflowAnalysisContext {
return {};
}
+ /// Export the logical-context portions of `AC`, limited to the given target
+ /// flow-condition tokens.
+ SimpleLogicalContext
+ exportLogicalContext(llvm::DenseSet<dataflow::Atom> TargetTokens) const;
+
+ /// Initializes this context's "logical" components with `LC`.
+ void initLogicalContext(SimpleLogicalContext LC);
+
private:
friend class Environment;
@@ -260,6 +257,11 @@ class DataflowAnalysisContext {
DataflowAnalysisContext(Solver &S, std::unique_ptr<Solver> &&OwnedSolver,
Options Opts);
+ /// Computes the transitive closure of reachable atoms from `Tokens`, through
+ /// the dependency graph.
+ llvm::DenseSet<Atom>
+ getTransitiveClosure(const llvm::DenseSet<Atom> &Tokens) const;
+
// Extends the set of modeled field declarations.
void addModeledFields(const FieldSet &Fields);
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 97914023ee79e..487f517420995 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -262,6 +262,65 @@ void
DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
}
}
+static void getReferencedAtoms(const Formula &F,
+ llvm::DenseSet<dataflow::Atom> &Refs) {
+ switch (F.kind()) {
+ case Formula::AtomRef:
+ Refs.insert(F.getAtom());
+ break;
+ case Formula::Literal:
+ break;
+ case Formula::Not:
+ getReferencedAtoms(*F.operands()[0], Refs);
+ break;
+ case Formula::And:
+ case Formula::Or:
+ case Formula::Implies:
+ case Formula::Equal:
+ ArrayRef<const Formula *> Operands = F.operands();
+ getReferencedAtoms(*Operands[0], Refs);
+ getReferencedAtoms(*Operands[1], Refs);
+ break;
+ }
+}
+
+SimpleLogicalContext DataflowAnalysisContext::exportLogicalContext(
+ llvm::DenseSet<dataflow::Atom> TargetTokens) const {
+ SimpleLogicalContext LC;
+
+ if (Invariant != nullptr) {
+ LC.Invariant = Invariant;
+ getReferencedAtoms(*Invariant, TargetTokens);
+ }
+
+ llvm::DenseSet<dataflow::Atom> ReachableTokens =
+ getTransitiveClosure(TargetTokens);
+
+ for (dataflow::Atom Token : ReachableTokens) {
+ // Only process the token if it is constrained. Unconstrained tokens don't
+ // have dependencies.
+ auto ConstraintsIt = FlowConditionConstraints.find(Token);
+ if (ConstraintsIt == FlowConditionConstraints.end())
+ continue;
+ LC.TokenDefs[Token] = ConstraintsIt->second;
+
+ if (auto DepsIt = FlowConditionDeps.find(Token);
+ DepsIt != FlowConditionDeps.end())
+ LC.TokenDeps[Token] = DepsIt->second;
+ }
+
+ return LC;
+}
+
+void DataflowAnalysisContext::initLogicalContext(SimpleLogicalContext LC) {
+ Invariant = LC.Invariant;
+ FlowConditionConstraints = std::move(LC.TokenDefs);
+ // TODO: The dependencies in `LC.TokenDeps` can be reconstructed from
+ // `LC.TokenDefs`. Give the caller the option to reconstruct, , rather than
+ // providing them directly, to save caller space (memory/disk).
+ FlowConditionDeps = std::move(LC.TokenDeps);
+}
+
static void printAtomList(const llvm::SmallVector<Atom> &Atoms,
llvm::raw_ostream &OS) {
OS << "(";
diff --git
a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
index 07323952b3e67..92b687a5a18a4 100644
--- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -80,14 +80,6 @@ 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());
@@ -134,28 +126,6 @@ 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());
@@ -204,65 +174,27 @@ 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, {});
+using ExportLogicalContextTest = DataflowAnalysisContextTest;
- // Verify that FC1 has no dependencies.
- EXPECT_EQ(Context.getFlowConditionDeps(FC1), nullptr);
+TEST_F(ExportLogicalContextTest, EmptySet) {
+ EXPECT_THAT(Context.exportLogicalContext({}).TokenDefs, IsEmpty());
}
-TEST_F(FlowConditionDepsTest, AddAndGetDeps) {
+// Only constrainted tokens are included in the output.
+TEST_F(ExportLogicalContextTest, UnconstrainedIgnored) {
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);
+ EXPECT_THAT(Context.exportLogicalContext({FC1}).TokenDefs, IsEmpty());
}
-TEST_F(FlowConditionDepsTest, AddDepsToExisting) {
+TEST_F(ExportLogicalContextTest, SingletonSet) {
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));
+ auto &C1 = A.makeAtomRef(A.makeAtom());
+ Context.addFlowConditionConstraint(FC1, C1);
+ EXPECT_THAT(Context.exportLogicalContext({FC1}).TokenDefs.keys(),
+ UnorderedElementsAre(FC1));
}
-TEST_F(GetTransitiveClosureTest, NoDependency) {
+TEST_F(ExportLogicalContextTest, NoDependency) {
Atom FC1 = A.makeFlowConditionToken();
Atom FC2 = A.makeFlowConditionToken();
Atom FC3 = A.makeFlowConditionToken();
@@ -275,89 +207,64 @@ TEST_F(GetTransitiveClosureTest, NoDependency) {
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));
+ EXPECT_THAT(Context.exportLogicalContext({FC1}).TokenDefs.keys(),
+ UnorderedElementsAre(FC1));
+ EXPECT_THAT(Context.exportLogicalContext({FC2}).TokenDefs.keys(),
+ UnorderedElementsAre(FC2));
+ EXPECT_THAT(Context.exportLogicalContext({FC3}).TokenDefs.keys(),
+ UnorderedElementsAre(FC3));
}
-TEST_F(GetTransitiveClosureTest, SimpleDependencyChain) {
+TEST_F(ExportLogicalContextTest, 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});
+ const Formula &C = A.makeAtomRef(A.makeAtom());
+ Context.addFlowConditionConstraint(FC1, C);
+ Atom FC2 = Context.forkFlowCondition(FC1);
+ Atom FC3 = Context.forkFlowCondition(FC2);
- EXPECT_THAT(Context.getTransitiveClosure({FC1}),
+ EXPECT_THAT(Context.exportLogicalContext({FC3}).TokenDefs.keys(),
UnorderedElementsAre(FC1, FC2, FC3));
}
-TEST_F(GetTransitiveClosureTest, DependencyTree) {
+TEST_F(ExportLogicalContextTest, DependencyTree) {
Atom FC1 = A.makeFlowConditionToken();
- Atom FC2 = A.makeFlowConditionToken();
+ const Formula &C = A.makeAtomRef(A.makeAtom());
+ Context.addFlowConditionConstraint(FC1, C);
+ Atom FC2 = Context.forkFlowCondition(FC1);
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.addFlowConditionConstraint(FC3, C);
+ Atom FC4 = Context.joinFlowConditions(FC2, FC3);
- Context.addFlowConditionDeps(FC2, {FC4});
- Context.addFlowConditionConstraint(FC2, A.makeAtomRef(FC4));
-
- EXPECT_THAT(Context.getTransitiveClosure({FC1}),
+ EXPECT_THAT(Context.exportLogicalContext({FC4}).TokenDefs.keys(),
UnorderedElementsAre(FC1, FC2, FC3, FC4));
}
-TEST_F(GetTransitiveClosureTest, DependencyDAG) {
+TEST_F(ExportLogicalContextTest, 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));
+ const Formula &C = A.makeAtomRef(A.makeAtom());
+ Context.addFlowConditionConstraint(FC1, C);
- Context.addFlowConditionDeps(FC3, {FC4});
- Context.addFlowConditionConstraint(FC3, A.makeAtomRef(FC4));
+ Atom FC2 = Context.forkFlowCondition(FC1);
+ Atom FC3 = Context.forkFlowCondition(FC1);
+ Atom FC4 = Context.joinFlowConditions(FC2, FC3);
- EXPECT_THAT(Context.getTransitiveClosure({FC1}),
+ EXPECT_THAT(Context.exportLogicalContext({FC4}).TokenDefs.keys(),
UnorderedElementsAre(FC1, FC2, FC3, FC4));
}
-TEST_F(GetTransitiveClosureTest, DependencyCycle) {
+TEST_F(ExportLogicalContextTest, MixedDependencies) {
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));
+ const Formula &C = A.makeAtomRef(A.makeAtom());
+ Context.addFlowConditionConstraint(FC1, C);
- EXPECT_THAT(Context.getTransitiveClosure({FC1}),
- UnorderedElementsAre(FC1, FC2, FC3));
-}
+ Atom FC2 = Context.forkFlowCondition(FC1);
+ Atom FC3 = Context.forkFlowCondition(FC2);
+ (void)FC3; // unused, and we test below that it is not included.
-TEST_F(GetTransitiveClosureTest, MixedDependencies) {
- Atom FC1 = A.makeFlowConditionToken();
- Atom FC2 = A.makeFlowConditionToken();
- Atom FC3 = A.makeFlowConditionToken();
Atom FC4 = A.makeFlowConditionToken();
+ Context.addFlowConditionConstraint(FC4, C);
- Context.addFlowConditionDeps(FC1, {FC2});
- Context.addFlowConditionConstraint(FC1, A.makeAtomRef(FC2));
-
- EXPECT_THAT(Context.getTransitiveClosure({FC1, FC3, FC4}),
- UnorderedElementsAre(FC1, FC2, FC3, FC4));
+ EXPECT_THAT(Context.exportLogicalContext({FC2, FC4}).TokenDefs.keys(),
+ UnorderedElementsAre(FC1, FC2, FC4));
}
} // namespace
>From 235ea87823b9d55f36906e626206c4a23c2759f7 Mon Sep 17 00:00:00 2001
From: Yitzhak Mandelbaum <yitzh...@google.com>
Date: Fri, 15 Aug 2025 18:47:52 +0000
Subject: [PATCH 3/3] fixup! fixup! [clang][dataflow] Add support for
serialization and deserialization.
respond to reviewer suggested changes
---
.../FlowSensitive/DataflowAnalysisContext.h | 7 +-
.../FlowSensitive/DataflowAnalysisContext.cpp | 16 ++--
.../FlowSensitive/FormulaSerialization.cpp | 77 ++++++++++---------
.../Analysis/FlowSensitive/FormulaTest.cpp | 70 ++++++++++++-----
4 files changed, 101 insertions(+), 69 deletions(-)
diff --git
a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index a03bfe058061e..613e79719e3e1 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -257,10 +257,11 @@ class DataflowAnalysisContext {
DataflowAnalysisContext(Solver &S, std::unique_ptr<Solver> &&OwnedSolver,
Options Opts);
- /// Computes the transitive closure of reachable atoms from `Tokens`, through
- /// the dependency graph.
+ /// Computes the transitive closure of dependencies of (flow-condition)
+ /// `Tokens`. That is, the set of flow-condition tokens reachable from
+ /// `Tokens` in the dependency graph.
llvm::DenseSet<Atom>
- getTransitiveClosure(const llvm::DenseSet<Atom> &Tokens) const;
+ collectDependencies(const llvm::DenseSet<Atom> &Tokens) const;
// Extends the set of modeled field declarations.
void addModeledFields(const FieldSet &Fields);
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 487f517420995..4d7c1f033799a 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -208,7 +208,7 @@ bool DataflowAnalysisContext::equivalentFormulas(const
Formula &Val1,
return isUnsatisfiable(std::move(Constraints));
}
-llvm::DenseSet<Atom> DataflowAnalysisContext::getTransitiveClosure(
+llvm::DenseSet<Atom> DataflowAnalysisContext::collectDependencies(
const llvm::DenseSet<Atom> &Tokens) const {
llvm::DenseSet<Atom> VisitedTokens;
// Use a worklist algorithm, with `Remaining` holding the worklist.
@@ -293,16 +293,16 @@ SimpleLogicalContext
DataflowAnalysisContext::exportLogicalContext(
getReferencedAtoms(*Invariant, TargetTokens);
}
- llvm::DenseSet<dataflow::Atom> ReachableTokens =
- getTransitiveClosure(TargetTokens);
+ llvm::DenseSet<dataflow::Atom> Dependencies =
+ collectDependencies(TargetTokens);
- for (dataflow::Atom Token : ReachableTokens) {
+ for (dataflow::Atom Token : Dependencies) {
// Only process the token if it is constrained. Unconstrained tokens don't
// have dependencies.
- auto ConstraintsIt = FlowConditionConstraints.find(Token);
- if (ConstraintsIt == FlowConditionConstraints.end())
+ const Formula *Constraints = FlowConditionConstraints.lookup(Token);
+ if (Constraints == nullptr)
continue;
- LC.TokenDefs[Token] = ConstraintsIt->second;
+ LC.TokenDefs[Token] = Constraints;
if (auto DepsIt = FlowConditionDeps.find(Token);
DepsIt != FlowConditionDeps.end())
@@ -316,7 +316,7 @@ void
DataflowAnalysisContext::initLogicalContext(SimpleLogicalContext LC) {
Invariant = LC.Invariant;
FlowConditionConstraints = std::move(LC.TokenDefs);
// TODO: The dependencies in `LC.TokenDeps` can be reconstructed from
- // `LC.TokenDefs`. Give the caller the option to reconstruct, , rather than
+ // `LC.TokenDefs`. Give the caller the option to reconstruct, rather than
// providing them directly, to save caller space (memory/disk).
FlowConditionDeps = std::move(LC.TokenDeps);
}
diff --git a/clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp
b/clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp
index 56cbf5aba8e55..cff1107f34291 100644
--- a/clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp
+++ b/clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp
@@ -70,6 +70,25 @@ void serializeFormula(const Formula &F, llvm::raw_ostream
&OS) {
}
}
+static llvm::Expected<const Formula *>
+parsePrefix(llvm::StringRef &Str, Arena &A,
+ llvm::DenseMap<unsigned, Atom> &AtomMap);
+
+static llvm::Expected<const Formula *>
+parseBinaryOp(llvm::StringRef &Str, Arena &A,
+ llvm::DenseMap<unsigned, Atom> &AtomMap,
+ llvm::function_ref<const Formula *(Arena &A, const Formula &L,
+ const Formula &R)>
+ Op) {
+ auto LeftOrErr = parsePrefix(Str, A, AtomMap);
+ if (!LeftOrErr)
+ return LeftOrErr.takeError();
+ auto RightOrErr = parsePrefix(Str, A, AtomMap);
+ if (!RightOrErr)
+ return RightOrErr.takeError();
+ return Op(A, **LeftOrErr, **RightOrErr);
+}
+
static llvm::Expected<const Formula *>
parsePrefix(llvm::StringRef &Str, Arena &A,
llvm::DenseMap<unsigned, Atom> &AtomMap) {
@@ -101,45 +120,29 @@ parsePrefix(llvm::StringRef &Str, Arena &A,
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);
- }
+ case '&':
+ return parseBinaryOp(Str, A, AtomMap,
+ [](Arena &A, const Formula &L, const Formula &R) {
+ return &A.makeAnd(L, R);
+ });
+ case '|':
+ return parseBinaryOp(Str, A, AtomMap,
+ [](Arena &A, const Formula &L, const Formula &R) {
+ return &A.makeOr(L, R);
+ });
+ case '>':
+ return parseBinaryOp(Str, A, AtomMap,
+ [](Arena &A, const Formula &L, const Formula &R) {
+ return &A.makeImplies(L, R);
+ });
+ case '=':
+ return parseBinaryOp(Str, A, AtomMap,
+ [](Arena &A, const Formula &L, const Formula &R) {
+ return &A.makeEquals(L, R);
+ });
default:
return llvm::createStringError(llvm::inconvertibleErrorCode(),
- "unexpected prefix character");
+ "unexpected prefix character: %c", Prefix);
}
}
diff --git a/clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp
b/clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp
index 49c02a8f192f2..99f5c11a9c0e8 100644
--- a/clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp
@@ -1,4 +1,4 @@
-//===- unittests/Analysis/FlowSensitive/FormulaTest.cpp -------===//
+//===- 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.
@@ -7,7 +7,6 @@
//===----------------------------------------------------------------------===//
#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"
@@ -20,7 +19,9 @@ namespace {
using namespace clang;
using namespace dataflow;
+using ::llvm::Failed;
using ::llvm::HasValue;
+using ::llvm::Succeeded;
using ::testing::ElementsAre;
using ::testing::IsEmpty;
@@ -95,6 +96,11 @@ class ParseFormulaTest : public ::testing::Test {
AtomMap[1] = Atom2;
}
+ // Convenience wrapper for `testParseFormula`.
+ llvm::Expected<const Formula *> testParseFormula(llvm::StringRef Str) {
+ return parseFormula(Str, A, AtomMap);
+ }
+
Arena A;
std::string Out;
llvm::raw_string_ostream OS{Out};
@@ -107,53 +113,58 @@ class ParseFormulaTest : public ::testing::Test {
};
TEST_F(ParseFormulaTest, Atom) {
- EXPECT_THAT_EXPECTED(parseFormula("V0", A, AtomMap), HasValue(&A1));
- EXPECT_THAT_EXPECTED(parseFormula("V1", A, AtomMap), HasValue(&A2));
+ EXPECT_THAT_EXPECTED(testParseFormula("V0"), HasValue(&A1));
+ EXPECT_THAT_EXPECTED(testParseFormula("V1"), HasValue(&A2));
}
TEST_F(ParseFormulaTest, LiteralTrue) {
- EXPECT_THAT_EXPECTED(parseFormula("T", A, AtomMap),
+ EXPECT_THAT_EXPECTED(testParseFormula("T"),
HasValue(&A.makeLiteral(true)));
}
TEST_F(ParseFormulaTest, LiteralFalse) {
- EXPECT_THAT_EXPECTED(parseFormula("F", A, AtomMap),
+ EXPECT_THAT_EXPECTED(testParseFormula("F"),
HasValue(&A.makeLiteral(false)));
}
TEST_F(ParseFormulaTest, Not) {
- EXPECT_THAT_EXPECTED(parseFormula("!V0", A, AtomMap),
+ EXPECT_THAT_EXPECTED(testParseFormula("!V0"),
HasValue(&A.makeNot(A1)));
}
TEST_F(ParseFormulaTest, Or) {
- EXPECT_THAT_EXPECTED(parseFormula("|V0V1", A, AtomMap),
+ EXPECT_THAT_EXPECTED(testParseFormula("|V0V1"),
HasValue(&A.makeOr(A1, A2)));
}
TEST_F(ParseFormulaTest, And) {
- EXPECT_THAT_EXPECTED(parseFormula("&V0V1", A, AtomMap),
+ EXPECT_THAT_EXPECTED(testParseFormula("&V0V1"),
HasValue(&A.makeAnd(A1, A2)));
}
+TEST_F(ParseFormulaTest, OutOfNumericOrder) {
+ EXPECT_THAT_EXPECTED(parseFormula("&V1V0", A, AtomMap),
+ HasValue(&A.makeAnd(A2, A1)));
+}
+
TEST_F(ParseFormulaTest, Implies) {
- EXPECT_THAT_EXPECTED(parseFormula(">V0V1", A, AtomMap),
+ EXPECT_THAT_EXPECTED(testParseFormula(">V0V1"),
HasValue(&A.makeImplies(A1, A2)));
}
TEST_F(ParseFormulaTest, Equal) {
- EXPECT_THAT_EXPECTED(parseFormula("=V0V1", A, AtomMap),
+ EXPECT_THAT_EXPECTED(testParseFormula("=V0V1"),
HasValue(&A.makeEquals(A1, A2)));
}
TEST_F(ParseFormulaTest, NestedBinaryUnary) {
- EXPECT_THAT_EXPECTED(parseFormula("=|V0V1V1", A, AtomMap),
+ EXPECT_THAT_EXPECTED(testParseFormula("=|V0V1V1"),
HasValue(&A.makeEquals(A.makeOr(A1, A2), A2)));
}
TEST_F(ParseFormulaTest, NestedBinaryBinary) {
EXPECT_THAT_EXPECTED(
- parseFormula("=|V0V1&V0V1", A, AtomMap),
+ testParseFormula("=|V0V1&V0V1"),
HasValue(&A.makeEquals(A.makeOr(A1, A2), A.makeAnd(A1, A2))));
}
@@ -161,19 +172,36 @@ TEST_F(ParseFormulaTest, NestedBinaryBinary) {
// map.
TEST_F(ParseFormulaTest, GeneratesAtoms) {
llvm::DenseMap<unsigned, Atom> FreshAtomMap;
- ASSERT_THAT_EXPECTED(parseFormula("=V0V1", A, FreshAtomMap),
- llvm::Succeeded());
+ ASSERT_THAT_EXPECTED(parseFormula("=V0V1", A, FreshAtomMap), 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());
+TEST_F(ParseFormulaTest, MalformedFormulaFails) {
+ // Arbitrary string.
+ EXPECT_THAT_EXPECTED(testParseFormula("Hello"), Failed());
+ // Empty string.
+ EXPECT_THAT_EXPECTED(testParseFormula(""), Failed());
+ // Malformed atom.
+ EXPECT_THAT_EXPECTED(testParseFormula("Vabc"), Failed());
+ // Irrelevant suffix.
+ EXPECT_THAT_EXPECTED(testParseFormula("V0Hello"), Failed());
+ EXPECT_THAT_EXPECTED(testParseFormula("=V0V1Hello"), Failed());
+ // Sequence without operator.
+ EXPECT_THAT_EXPECTED(testParseFormula("TF"), Failed());
+ // Bad subformula.
+ EXPECT_THAT_EXPECTED(testParseFormula("!G"), Failed());
+ // Incomplete formulas.
+ EXPECT_THAT_EXPECTED(testParseFormula("V"), Failed());
+ EXPECT_THAT_EXPECTED(testParseFormula("&"), Failed());
+ EXPECT_THAT_EXPECTED(testParseFormula("|"), Failed());
+ EXPECT_THAT_EXPECTED(testParseFormula(">"), Failed());
+ EXPECT_THAT_EXPECTED(testParseFormula("="), Failed());
+ EXPECT_THAT_EXPECTED(testParseFormula("&V0"), Failed());
+ EXPECT_THAT_EXPECTED(testParseFormula("|V0"), Failed());
+ EXPECT_THAT_EXPECTED(testParseFormula(">V0"), Failed());
+ EXPECT_THAT_EXPECTED(testParseFormula("=V0"), Failed());
}
} // namespace
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
