Author: Yitzhak Mandelbaum Date: 2025-08-18T11:55:12-04:00 New Revision: 3ecfc0330d93a6c3a3f3d3e427390b01cb52a88d
URL: https://github.com/llvm/llvm-project/commit/3ecfc0330d93a6c3a3f3d3e427390b01cb52a88d DIFF: https://github.com/llvm/llvm-project/commit/3ecfc0330d93a6c3a3f3d3e427390b01cb52a88d.diff LOG: [clang][dataflow] Add support for serialization and deserialization. (#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. Added: clang/include/clang/Analysis/FlowSensitive/FormulaSerialization.h clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp Modified: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h clang/include/clang/Analysis/FlowSensitive/Formula.h clang/lib/Analysis/FlowSensitive/CMakeLists.txt clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp clang/unittests/Analysis/FlowSensitive/CMakeLists.txt clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp Removed: ################################################################################ diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h index 5be4a1145f40d..11042e865c4e6 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 { @@ -140,6 +152,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); @@ -207,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; @@ -228,6 +257,11 @@ class DataflowAnalysisContext { DataflowAnalysisContext(Solver &S, std::unique_ptr<Solver> &&OwnedSolver, Options Opts); + /// 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> collectDependencies(llvm::DenseSet<Atom> Tokens) const; + // Extends the set of modeled field declarations. void addModeledFields(const FieldSet &Fields); 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..06a88784a6f94 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -208,6 +208,24 @@ bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1, return isUnsatisfiable(std::move(Constraints)); } +llvm::DenseSet<Atom> DataflowAnalysisContext::collectDependencies( + llvm::DenseSet<Atom> Tokens) const { + // Use a worklist algorithm, with `Remaining` holding the worklist and + // `Tokens` tracking which atoms have already been added to the worklist. + std::vector<Atom> Remaining(Tokens.begin(), Tokens.end()); + while (!Remaining.empty()) { + Atom CurrentToken = Remaining.back(); + Remaining.pop_back(); + if (auto DepsIt = FlowConditionDeps.find(CurrentToken); + DepsIt != FlowConditionDeps.end()) + for (Atom A : DepsIt->second) + if (Tokens.insert(A).second) + Remaining.push_back(A); + } + + return Tokens; +} + void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( Atom Token, llvm::SetVector<const Formula *> &Constraints) { llvm::DenseSet<Atom> AddedTokens; @@ -224,6 +242,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: @@ -239,6 +259,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> Dependencies = + collectDependencies(std::move(TargetTokens)); + + for (dataflow::Atom Token : Dependencies) { + // Only process the token if it is constrained. Unconstrained tokens don't + // have dependencies. + const Formula *Constraints = FlowConditionConstraints.lookup(Token); + if (Constraints == nullptr) + continue; + LC.TokenDefs[Token] = Constraints; + + 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/lib/Analysis/FlowSensitive/FormulaSerialization.cpp b/clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp new file mode 100644 index 0000000000000..df15a1d6eaadb --- /dev/null +++ b/clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp @@ -0,0 +1,153 @@ +//===- 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 diff erently. +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 '&': + case '|': + case '>': + case '=': { + auto LeftOrErr = parsePrefix(Str, A, AtomMap); + if (!LeftOrErr) + return LeftOrErr.takeError(); + + auto RightOrErr = parsePrefix(Str, A, AtomMap); + if (!RightOrErr) + return RightOrErr.takeError(); + + const Formula &LHS = **LeftOrErr; + const Formula &RHS = **RightOrErr; + + switch (Prefix) { + case '&': + return &A.makeAnd(LHS, RHS); + case '|': + return &A.makeOr(LHS, RHS); + case '>': + return &A.makeImplies(LHS, RHS); + case '=': + return &A.makeEquals(LHS, RHS); + default: + llvm_unreachable("unexpected binary op"); + } + } + default: + return llvm::createStringError(llvm::inconvertibleErrorCode(), + "unexpected prefix character: %c", Prefix); + } +} + +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..92b687a5a18a4 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() @@ -171,4 +174,97 @@ TEST_F(DataflowAnalysisContextTest, EquivBoolVals) { A.makeAnd(X, A.makeAnd(Y, Z)))); } +using ExportLogicalContextTest = DataflowAnalysisContextTest; + +TEST_F(ExportLogicalContextTest, EmptySet) { + EXPECT_THAT(Context.exportLogicalContext({}).TokenDefs, IsEmpty()); +} + +// Only constrainted tokens are included in the output. +TEST_F(ExportLogicalContextTest, UnconstrainedIgnored) { + Atom FC1 = A.makeFlowConditionToken(); + EXPECT_THAT(Context.exportLogicalContext({FC1}).TokenDefs, IsEmpty()); +} + +TEST_F(ExportLogicalContextTest, SingletonSet) { + Atom FC1 = A.makeFlowConditionToken(); + auto &C1 = A.makeAtomRef(A.makeAtom()); + Context.addFlowConditionConstraint(FC1, C1); + EXPECT_THAT(Context.exportLogicalContext({FC1}).TokenDefs.keys(), + UnorderedElementsAre(FC1)); +} + +TEST_F(ExportLogicalContextTest, 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.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(ExportLogicalContextTest, SimpleDependencyChain) { + Atom FC1 = A.makeFlowConditionToken(); + const Formula &C = A.makeAtomRef(A.makeAtom()); + Context.addFlowConditionConstraint(FC1, C); + Atom FC2 = Context.forkFlowCondition(FC1); + Atom FC3 = Context.forkFlowCondition(FC2); + + EXPECT_THAT(Context.exportLogicalContext({FC3}).TokenDefs.keys(), + UnorderedElementsAre(FC1, FC2, FC3)); +} + +TEST_F(ExportLogicalContextTest, DependencyTree) { + Atom FC1 = A.makeFlowConditionToken(); + const Formula &C = A.makeAtomRef(A.makeAtom()); + Context.addFlowConditionConstraint(FC1, C); + Atom FC2 = Context.forkFlowCondition(FC1); + Atom FC3 = A.makeFlowConditionToken(); + Context.addFlowConditionConstraint(FC3, C); + Atom FC4 = Context.joinFlowConditions(FC2, FC3); + + EXPECT_THAT(Context.exportLogicalContext({FC4}).TokenDefs.keys(), + UnorderedElementsAre(FC1, FC2, FC3, FC4)); +} + +TEST_F(ExportLogicalContextTest, DependencyDAG) { + Atom FC1 = A.makeFlowConditionToken(); + const Formula &C = A.makeAtomRef(A.makeAtom()); + Context.addFlowConditionConstraint(FC1, C); + + Atom FC2 = Context.forkFlowCondition(FC1); + Atom FC3 = Context.forkFlowCondition(FC1); + Atom FC4 = Context.joinFlowConditions(FC2, FC3); + + EXPECT_THAT(Context.exportLogicalContext({FC4}).TokenDefs.keys(), + UnorderedElementsAre(FC1, FC2, FC3, FC4)); +} + +TEST_F(ExportLogicalContextTest, MixedDependencies) { + Atom FC1 = A.makeFlowConditionToken(); + const Formula &C = A.makeAtomRef(A.makeAtom()); + Context.addFlowConditionConstraint(FC1, C); + + Atom FC2 = Context.forkFlowCondition(FC1); + Atom FC3 = Context.forkFlowCondition(FC2); + (void)FC3; // unused, and we test below that it is not included. + + Atom FC4 = A.makeFlowConditionToken(); + Context.addFlowConditionConstraint(FC4, C); + + EXPECT_THAT(Context.exportLogicalContext({FC2, FC4}).TokenDefs.keys(), + UnorderedElementsAre(FC1, FC2, FC4)); +} } // namespace diff --git a/clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp b/clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp new file mode 100644 index 0000000000000..cabcd59fffedc --- /dev/null +++ b/clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp @@ -0,0 +1,201 @@ +//===- 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 "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::Failed; +using ::llvm::HasValue; +using ::llvm::Succeeded; +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; + } + + // 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}; + + 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(testParseFormula("V0"), HasValue(&A1)); + EXPECT_THAT_EXPECTED(testParseFormula("V1"), HasValue(&A2)); +} + +TEST_F(ParseFormulaTest, LiteralTrue) { + EXPECT_THAT_EXPECTED(testParseFormula("T"), HasValue(&A.makeLiteral(true))); +} + +TEST_F(ParseFormulaTest, LiteralFalse) { + EXPECT_THAT_EXPECTED(testParseFormula("F"), HasValue(&A.makeLiteral(false))); +} + +TEST_F(ParseFormulaTest, Not) { + EXPECT_THAT_EXPECTED(testParseFormula("!V0"), HasValue(&A.makeNot(A1))); +} + +TEST_F(ParseFormulaTest, Or) { + EXPECT_THAT_EXPECTED(testParseFormula("|V0V1"), HasValue(&A.makeOr(A1, A2))); +} + +TEST_F(ParseFormulaTest, And) { + EXPECT_THAT_EXPECTED(testParseFormula("&V0V1"), HasValue(&A.makeAnd(A1, A2))); +} + +TEST_F(ParseFormulaTest, OutOfNumericOrder) { + EXPECT_THAT_EXPECTED(testParseFormula("&V1V0"), HasValue(&A.makeAnd(A2, A1))); +} + +TEST_F(ParseFormulaTest, Implies) { + EXPECT_THAT_EXPECTED(testParseFormula(">V0V1"), + HasValue(&A.makeImplies(A1, A2))); +} + +TEST_F(ParseFormulaTest, Equal) { + EXPECT_THAT_EXPECTED(testParseFormula("=V0V1"), + HasValue(&A.makeEquals(A1, A2))); +} + +TEST_F(ParseFormulaTest, NestedBinaryUnary) { + EXPECT_THAT_EXPECTED(testParseFormula("=|V0V1V1"), + HasValue(&A.makeEquals(A.makeOr(A1, A2), A2))); +} + +TEST_F(ParseFormulaTest, NestedBinaryBinary) { + EXPECT_THAT_EXPECTED( + testParseFormula("=|V0V1&V0V1"), + 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), Succeeded()); + // The map contains two, unique elements. + ASSERT_EQ(FreshAtomMap.size(), 2U); + EXPECT_NE(FreshAtomMap[0], FreshAtomMap[1]); +} + +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
