llvmbot wrote:
<!--LLVM PR SUMMARY COMMENT--> @llvm/pr-subscribers-clang-analysis Author: Yitzhak Mandelbaum (ymand) <details> <summary>Changes</summary> 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. --- Patch is 28.28 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/152487.diff 10 Files Affected: - (modified) clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h (+32) - (modified) clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h (+12-3) - (modified) clang/include/clang/Analysis/FlowSensitive/Formula.h (+10-9) - (added) clang/include/clang/Analysis/FlowSensitive/FormulaSerialization.h (+40) - (modified) clang/lib/Analysis/FlowSensitive/CMakeLists.txt (+1) - (modified) clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp (+23) - (added) clang/lib/Analysis/FlowSensitive/FormulaSerialization.cpp (+158) - (modified) clang/unittests/Analysis/FlowSensitive/CMakeLists.txt (+1) - (modified) clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp (+190) - (added) clang/unittests/Analysis/FlowSensitive/FormulaTest.cpp (+180) ``````````diff 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... [truncated] `````````` </details> https://github.com/llvm/llvm-project/pull/152487 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
