[clang] 2fd614e - [dataflow] Add dedicated representation of boolean formulas
Sam McCall via cfe-commits
cfe-commits at lists.llvm.org
Tue Jul 4 03:19:54 PDT 2023
Author: Sam McCall
Date: 2023-07-04T12:19:44+02:00
New Revision: 2fd614efc1bb9c27f1bc6c3096c60a7fe121e274
URL: https://github.com/llvm/llvm-project/commit/2fd614efc1bb9c27f1bc6c3096c60a7fe121e274
DIFF: https://github.com/llvm/llvm-project/commit/2fd614efc1bb9c27f1bc6c3096c60a7fe121e274.diff
LOG: [dataflow] Add dedicated representation of boolean formulas
This is the first step in untangling the two current jobs of BoolValue.
=== Desired end-state: ===
- BoolValue will model C++ booleans e.g. held in StorageLocations.
this includes describing uncertainty (e.g. "top" is a Value concern)
- Formula describes analysis-level assertions in terms of SAT atoms.
These can still be linked together: a BoolValue may have a corresponding
SAT atom which is constrained by formulas.
=== Done in this patch: ===
BoolValue is left intact, Formula is just the input type to the
SAT solver, and we build formulas as needed to invoke the solver.
=== Incidental changes to debug string printing: ===
- variables renamed from B0 etc to V0 etc
B0 collides with the names of basic blocks, which is confusing when
debugging flow conditions.
- debug printing of formulas (Formula and Atom) uses operator<<
rather than debugString(), so works with gtest.
Therefore moved out of DebugSupport.h
- Did the same to Solver::Result, and some helper changes to SolverTest,
so that we get useful messages on unit test failures
- formulas are now printed as infix expressions on one line, rather than
wrapped/indented S-exprs. My experience is that this is easier to scan
FCs for small examples, and large ones are unreadable either way.
- most of the several debugString() functions for constraints/results
are unused, so removed them rather than updating tests.
Inlined the one that was actually used into its callsite.
Differential Revision: https://reviews.llvm.org/D153366
Added:
clang/include/clang/Analysis/FlowSensitive/Formula.h
clang/lib/Analysis/FlowSensitive/Formula.cpp
Modified:
clang/include/clang/Analysis/FlowSensitive/Arena.h
clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
clang/include/clang/Analysis/FlowSensitive/Solver.h
clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
clang/lib/Analysis/FlowSensitive/Arena.cpp
clang/lib/Analysis/FlowSensitive/CMakeLists.txt
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
Removed:
################################################################################
diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h
index 83b4ddeec02564..b6c62e76246254 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Arena.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h
@@ -8,6 +8,7 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include <vector>
@@ -104,7 +105,17 @@ class Arena {
return create<AtomicBoolValue>();
}
+ /// Gets the boolean formula equivalent of a BoolValue.
+ /// Each unique Top values is translated to an Atom.
+ /// TODO: migrate to storing Formula directly in Values instead.
+ const Formula &getFormula(const BoolValue &);
+
+ /// Returns a new atomic boolean variable, distinct from any other.
+ Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
+
private:
+ llvm::BumpPtrAllocator Alloc;
+
// Storage for the state of a program.
std::vector<std::unique_ptr<StorageLocation>> Locs;
std::vector<std::unique_ptr<Value>> Vals;
@@ -122,6 +133,9 @@ class Arena {
llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
BiconditionalVals;
+ llvm::DenseMap<const BoolValue *, const Formula *> ValToFormula;
+ unsigned NextAtom = 0;
+
AtomicBoolValue &TrueVal;
AtomicBoolValue &FalseVal;
};
diff --git a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
index 360786b02729f2..6b9f3681490af1 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
@@ -19,7 +19,6 @@
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/Value.h"
-#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/StringRef.h"
namespace clang {
@@ -28,52 +27,9 @@ namespace dataflow {
/// Returns a string representation of a value kind.
llvm::StringRef debugString(Value::Kind Kind);
-/// Returns a string representation of a boolean assignment to true or false.
-llvm::StringRef debugString(Solver::Result::Assignment Assignment);
-
/// Returns a string representation of the result status of a SAT check.
llvm::StringRef debugString(Solver::Result::Status Status);
-/// Returns a string representation for the boolean value `B`.
-///
-/// Atomic booleans appearing in the boolean value `B` are assigned to labels
-/// either specified in `AtomNames` or created by default rules as B0, B1, ...
-///
-/// Requirements:
-///
-/// Names assigned to atoms should not be repeated in `AtomNames`.
-std::string debugString(
- const BoolValue &B,
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-
-/// Returns a string representation for `Constraints` - a collection of boolean
-/// formulas.
-///
-/// Atomic booleans appearing in the boolean value `Constraints` are assigned to
-/// labels either specified in `AtomNames` or created by default rules as B0,
-/// B1, ...
-///
-/// Requirements:
-///
-/// Names assigned to atoms should not be repeated in `AtomNames`.
-std::string debugString(
- const llvm::ArrayRef<BoolValue *> Constraints,
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-
-/// Returns a string representation for `Constraints` - a collection of boolean
-/// formulas and the `Result` of satisfiability checking.
-///
-/// Atomic booleans appearing in `Constraints` and `Result` are assigned to
-/// labels either specified in `AtomNames` or created by default rules as B0,
-/// B1, ...
-///
-/// Requirements:
-///
-/// Names assigned to atoms should not be repeated in `AtomNames`.
-std::string debugString(
- ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-
} // namespace dataflow
} // namespace clang
diff --git a/clang/include/clang/Analysis/FlowSensitive/Formula.h b/clang/include/clang/Analysis/FlowSensitive/Formula.h
new file mode 100644
index 00000000000000..0c7b1ecd02b17c
--- /dev/null
+++ b/clang/include/clang/Analysis/FlowSensitive/Formula.h
@@ -0,0 +1,137 @@
+//===- Formula.h - Boolean formulas -----------------------------*- 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_H
+#define LLVM_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/ADT/STLFunctionalExtras.h"
+#include "llvm/Support/Allocator.h"
+#include "llvm/Support/raw_ostream.h"
+#include <cassert>
+#include <string>
+#include <type_traits>
+
+namespace clang::dataflow {
+
+/// Identifies an atomic boolean variable such as "V1".
+///
+/// This often represents an assertion that is interesting to the analysis but
+/// cannot immediately be proven true or false. For example:
+/// - V1 may mean "the program reaches this point",
+/// - V2 may mean "the parameter was null"
+///
+/// We can use these variables in formulas to describe relationships we know
+/// to be true: "if the parameter was null, the program reaches this point".
+/// We also express hypotheses as formulas, and use a SAT solver to check
+/// whether they are consistent with the known facts.
+enum class Atom : unsigned {};
+
+/// A boolean expression such as "true" or "V1 & !V2".
+/// Expressions may refer to boolean atomic variables. These should take a
+/// consistent true/false value across the set of formulas being considered.
+///
+/// (Formulas are always expressions in terms of boolean variables rather than
+/// e.g. integers because our underlying model is SAT rather than e.g. SMT).
+///
+/// Simple formulas such as "true" and "V1" are self-contained.
+/// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or'
+/// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as
+/// trailing objects.
+/// For this reason, Formulas are Arena-allocated and over-aligned.
+class Formula;
+class alignas(const Formula *) Formula {
+public:
+ enum Kind : unsigned {
+ /// A reference to an atomic boolean variable.
+ /// We name these e.g. "V3", where 3 == atom identity == Value.
+ AtomRef,
+ // FIXME: add const true/false rather than modeling them as variables
+
+ Not, /// True if its only operand is false
+
+ // These kinds connect two operands LHS and RHS
+ And, /// True if LHS and RHS are both true
+ Or, /// True if either LHS or RHS is true
+ Implies, /// True if LHS is false or RHS is true
+ Equal, /// True if LHS and RHS have the same truth value
+ };
+ Kind kind() const { return FormulaKind; }
+
+ Atom getAtom() const {
+ assert(kind() == AtomRef);
+ return static_cast<Atom>(Value);
+ }
+
+ ArrayRef<const Formula *> operands() const {
+ return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
+ numOperands(kind()));
+ }
+
+ 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.
+ void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
+
+ // Allocate Formulas using Arena rather than calling this function directly.
+ static 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;
+
+ static unsigned numOperands(Kind K) {
+ switch (K) {
+ case AtomRef:
+ return 0;
+ case Not:
+ return 1;
+ case And:
+ case Or:
+ case Implies:
+ case Equal:
+ return 2;
+ }
+ }
+
+ Kind FormulaKind;
+ // Some kinds of formula have scalar values, e.g. AtomRef's atom number.
+ unsigned Value;
+};
+
+// The default names of atoms are V0, V1 etc in order of creation.
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) {
+ return OS << 'V' << static_cast<unsigned>(A);
+}
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) {
+ F.print(OS);
+ return OS;
+}
+
+} // namespace clang::dataflow
+namespace llvm {
+template <> struct DenseMapInfo<clang::dataflow::Atom> {
+ using Atom = clang::dataflow::Atom;
+ using Underlying = std::underlying_type_t<Atom>;
+
+ static inline Atom getEmptyKey() { return Atom(Underlying(-1)); }
+ static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); }
+ static unsigned getHashValue(const Atom &Val) {
+ return DenseMapInfo<Underlying>::getHashValue(Underlying(Val));
+ }
+ static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
+};
+} // namespace llvm
+#endif
diff --git a/clang/include/clang/Analysis/FlowSensitive/Solver.h b/clang/include/clang/Analysis/FlowSensitive/Solver.h
index 10964eab8c34cc..079f6802f241ee 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Solver.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Solver.h
@@ -14,12 +14,10 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
-#include "clang/Analysis/FlowSensitive/Value.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/DenseSet.h"
-#include "llvm/Support/Compiler.h"
#include <optional>
#include <vector>
@@ -49,8 +47,7 @@ class Solver {
/// Constructs a result indicating that the queried boolean formula is
/// satisfiable. The result will hold a solution found by the solver.
- static Result
- Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) {
+ static Result Satisfiable(llvm::DenseMap<Atom, Assignment> Solution) {
return Result(Status::Satisfiable, std::move(Solution));
}
@@ -68,19 +65,17 @@ class Solver {
/// Returns a truth assignment to boolean values that satisfies the queried
/// boolean formula if available. Otherwise, an empty optional is returned.
- std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>>
- getSolution() const {
+ std::optional<llvm::DenseMap<Atom, Assignment>> getSolution() const {
return Solution;
}
private:
- Result(
- enum Status SATCheckStatus,
- std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
+ Result(Status SATCheckStatus,
+ std::optional<llvm::DenseMap<Atom, Assignment>> Solution)
: SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {}
Status SATCheckStatus;
- std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution;
+ std::optional<llvm::DenseMap<Atom, Assignment>> Solution;
};
virtual ~Solver() = default;
@@ -91,14 +86,12 @@ class Solver {
/// Requirements:
///
/// All elements in `Vals` must not be null.
- virtual Result solve(llvm::ArrayRef<BoolValue *> Vals) = 0;
-
- LLVM_DEPRECATED("Pass ArrayRef for determinism", "")
- virtual Result solve(llvm::DenseSet<BoolValue *> Vals) {
- return solve(ArrayRef(std::vector<BoolValue *>(Vals.begin(), Vals.end())));
- }
+ virtual Result solve(llvm::ArrayRef<const Formula *> Vals) = 0;
};
+llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &);
+llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment);
+
} // namespace dataflow
} // namespace clang
diff --git a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
index b69cc01542c550..a0cdce93c9d470 100644
--- a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
+++ b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
@@ -14,8 +14,8 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/ArrayRef.h"
#include <limits>
@@ -46,7 +46,7 @@ class WatchedLiteralsSolver : public Solver {
explicit WatchedLiteralsSolver(std::int64_t WorkLimit)
: MaxIterations(WorkLimit) {}
- Result solve(llvm::ArrayRef<BoolValue *> Vals) override;
+ Result solve(llvm::ArrayRef<const Formula *> Vals) override;
};
} // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp
index cff6c45e185422..e576affc6a41b5 100644
--- a/clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -76,4 +76,50 @@ IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
return *It->second;
}
+const Formula &Arena::getFormula(const BoolValue &B) {
+ auto It = ValToFormula.find(&B);
+ if (It != ValToFormula.end())
+ return *It->second;
+ Formula &F = [&]() -> Formula & {
+ switch (B.getKind()) {
+ case Value::Kind::Integer:
+ case Value::Kind::Reference:
+ case Value::Kind::Pointer:
+ case Value::Kind::Struct:
+ llvm_unreachable("not a boolean");
+ case Value::Kind::TopBool:
+ case Value::Kind::AtomicBool:
+ // TODO: assign atom numbers on creation rather than in getFormula(), so
+ // they will be deterministic and maybe even meaningful.
+ return Formula::create(Alloc, Formula::AtomRef, {},
+ static_cast<unsigned>(makeAtom()));
+ case Value::Kind::Conjunction:
+ return Formula::create(
+ Alloc, Formula::And,
+ {&getFormula(cast<ConjunctionValue>(B).getLeftSubValue()),
+ &getFormula(cast<ConjunctionValue>(B).getRightSubValue())});
+ case Value::Kind::Disjunction:
+ return Formula::create(
+ Alloc, Formula::Or,
+ {&getFormula(cast<DisjunctionValue>(B).getLeftSubValue()),
+ &getFormula(cast<DisjunctionValue>(B).getRightSubValue())});
+ case Value::Kind::Negation:
+ return Formula::create(Alloc, Formula::Not,
+ {&getFormula(cast<NegationValue>(B).getSubVal())});
+ case Value::Kind::Implication:
+ return Formula::create(
+ Alloc, Formula::Implies,
+ {&getFormula(cast<ImplicationValue>(B).getLeftSubValue()),
+ &getFormula(cast<ImplicationValue>(B).getRightSubValue())});
+ case Value::Kind::Biconditional:
+ return Formula::create(
+ Alloc, Formula::Equal,
+ {&getFormula(cast<BiconditionalValue>(B).getLeftSubValue()),
+ &getFormula(cast<BiconditionalValue>(B).getRightSubValue())});
+ }
+ }();
+ ValToFormula.try_emplace(&B, &F);
+ return F;
+}
+
} // namespace clang::dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
index d59bebf6a5a127..171884afe8f4bf 100644
--- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -3,6 +3,7 @@ add_clang_library(clangAnalysisFlowSensitive
ControlFlowContext.cpp
DataflowAnalysisContext.cpp
DataflowEnvironment.cpp
+ Formula.cpp
HTMLLogger.cpp
Logger.cpp
RecordOps.cpp
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 37bcc8be958792..42cc6d4c3d143e 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -15,6 +15,7 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/AST/ExprCXX.h"
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Logger.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/SetOperations.h"
@@ -23,9 +24,12 @@
#include "llvm/Support/Debug.h"
#include "llvm/Support/FileSystem.h"
#include "llvm/Support/Path.h"
+#include "llvm/Support/raw_ostream.h"
#include <cassert>
#include <memory>
+#include <string>
#include <utility>
+#include <vector>
static llvm::cl::opt<std::string> DataflowLog(
"dataflow-log", llvm::cl::Hidden, llvm::cl::ValueOptional,
@@ -129,7 +133,10 @@ Solver::Result
DataflowAnalysisContext::querySolver(llvm::SetVector<BoolValue *> Constraints) {
Constraints.insert(&arena().makeLiteral(true));
Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
- return S->solve(Constraints.getArrayRef());
+ std::vector<const Formula *> Formulas;
+ for (const BoolValue *Constraint : Constraints)
+ Formulas.push_back(&arena().getFormula(*Constraint));
+ return S->solve(Formulas);
}
bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
@@ -191,15 +198,21 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
llvm::raw_ostream &OS) {
+ // TODO: accumulate formulas directly instead
llvm::SetVector<BoolValue *> Constraints;
Constraints.insert(&Token);
llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {
- {&arena().makeLiteral(false), "False"},
- {&arena().makeLiteral(true), "True"}};
- OS << debugString(Constraints.getArrayRef(), AtomNames);
+ // TODO: have formulas know about true/false directly instead
+ Atom True = arena().getFormula(arena().makeLiteral(true)).getAtom();
+ Atom False = arena().getFormula(arena().makeLiteral(false)).getAtom();
+ Formula::AtomNames Names = {{False, "false"}, {True, "true"}};
+
+ for (const auto *Constraint : Constraints) {
+ arena().getFormula(*Constraint).print(OS, &Names);
+ OS << "\n";
+ }
}
const ControlFlowContext *
diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
index 25225ed6266fb8..34e53249ba4d8b 100644
--- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -16,22 +16,12 @@
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/Value.h"
-#include "llvm/ADT/DenseMap.h"
-#include "llvm/ADT/STLExtras.h"
#include "llvm/ADT/StringRef.h"
-#include "llvm/ADT/StringSet.h"
#include "llvm/Support/ErrorHandling.h"
-#include "llvm/Support/FormatAdapters.h"
-#include "llvm/Support/FormatCommon.h"
-#include "llvm/Support/FormatVariadic.h"
namespace clang {
namespace dataflow {
-using llvm::AlignStyle;
-using llvm::fmt_pad;
-using llvm::formatv;
-
llvm::StringRef debugString(Value::Kind Kind) {
switch (Kind) {
case Value::Kind::Integer:
@@ -60,12 +50,13 @@ llvm::StringRef debugString(Value::Kind Kind) {
llvm_unreachable("Unhandled value kind");
}
-llvm::StringRef debugString(Solver::Result::Assignment Assignment) {
+llvm::raw_ostream &operator<<(llvm::raw_ostream &OS,
+ Solver::Result::Assignment Assignment) {
switch (Assignment) {
case Solver::Result::Assignment::AssignedFalse:
- return "False";
+ return OS << "False";
case Solver::Result::Assignment::AssignedTrue:
- return "True";
+ return OS << "True";
}
llvm_unreachable("Booleans can only be assigned true/false");
}
@@ -82,174 +73,16 @@ llvm::StringRef debugString(Solver::Result::Status Status) {
llvm_unreachable("Unhandled SAT check result status");
}
-namespace {
-
-class DebugStringGenerator {
-public:
- explicit DebugStringGenerator(
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg)
- : Counter(0), AtomNames(std::move(AtomNamesArg)) {
-#ifndef NDEBUG
- llvm::StringSet<> Names;
- for (auto &N : AtomNames) {
- assert(Names.insert(N.second).second &&
- "The same name must not assigned to
diff erent atoms");
- }
-#endif
- }
-
- /// Returns a string representation of a boolean value `B`.
- std::string debugString(const BoolValue &B, size_t Depth = 0) {
- std::string S;
- switch (B.getKind()) {
- case Value::Kind::AtomicBool: {
- S = getAtomName(&cast<AtomicBoolValue>(B));
- break;
- }
- case Value::Kind::TopBool: {
- S = "top";
- break;
- }
- case Value::Kind::Conjunction: {
- auto &C = cast<ConjunctionValue>(B);
- auto L = debugString(C.getLeftSubValue(), Depth + 1);
- auto R = debugString(C.getRightSubValue(), Depth + 1);
- S = formatv("(and\n{0}\n{1})", L, R);
- break;
- }
- case Value::Kind::Disjunction: {
- auto &D = cast<DisjunctionValue>(B);
- auto L = debugString(D.getLeftSubValue(), Depth + 1);
- auto R = debugString(D.getRightSubValue(), Depth + 1);
- S = formatv("(or\n{0}\n{1})", L, R);
- break;
- }
- case Value::Kind::Negation: {
- auto &N = cast<NegationValue>(B);
- S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1));
- break;
- }
- case Value::Kind::Implication: {
- auto &IV = cast<ImplicationValue>(B);
- auto L = debugString(IV.getLeftSubValue(), Depth + 1);
- auto R = debugString(IV.getRightSubValue(), Depth + 1);
- S = formatv("(=>\n{0}\n{1})", L, R);
- break;
- }
- case Value::Kind::Biconditional: {
- auto &BV = cast<BiconditionalValue>(B);
- auto L = debugString(BV.getLeftSubValue(), Depth + 1);
- auto R = debugString(BV.getRightSubValue(), Depth + 1);
- S = formatv("(=\n{0}\n{1})", L, R);
- break;
- }
- default:
- llvm_unreachable("Unhandled value kind");
- }
- auto Indent = Depth * 4;
- return formatv("{0}", fmt_pad(S, Indent, 0));
- }
-
- std::string debugString(const llvm::ArrayRef<BoolValue *> &Constraints) {
- std::string Result;
- for (const BoolValue *S : Constraints) {
- Result += debugString(*S);
- Result += '\n';
- }
- return Result;
- }
-
- /// Returns a string representation of a set of boolean `Constraints` and the
- /// `Result` of satisfiability checking on the `Constraints`.
- std::string debugString(ArrayRef<BoolValue *> &Constraints,
- const Solver::Result &Result) {
- auto Template = R"(
-Constraints
-------------
-{0:$[
-
-]}
-------------
-{1}.
-{2}
-)";
-
- std::vector<std::string> ConstraintsStrings;
- ConstraintsStrings.reserve(Constraints.size());
- for (auto &Constraint : Constraints) {
- ConstraintsStrings.push_back(debugString(*Constraint));
- }
-
- auto StatusString = clang::dataflow::debugString(Result.getStatus());
- auto Solution = Result.getSolution();
- auto SolutionString = Solution ? "\n" + debugString(*Solution) : "";
-
- return formatv(
- Template,
- llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()),
- StatusString, SolutionString);
- }
-
-private:
- /// Returns a string representation of a truth assignment to atom booleans.
- std::string debugString(
- const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
- &AtomAssignments) {
- size_t MaxNameLength = 0;
- for (auto &AtomName : AtomNames) {
- MaxNameLength = std::max(MaxNameLength, AtomName.second.size());
- }
-
- std::vector<std::string> Lines;
- for (auto &AtomAssignment : AtomAssignments) {
- auto Line = formatv("{0} = {1}",
- fmt_align(getAtomName(AtomAssignment.first),
- AlignStyle::Left, MaxNameLength),
- clang::dataflow::debugString(AtomAssignment.second));
- Lines.push_back(Line);
- }
- llvm::sort(Lines);
-
- return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end()));
+llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Solver::Result &R) {
+ OS << debugString(R.getStatus()) << "\n";
+ if (auto Solution = R.getSolution()) {
+ std::vector<std::pair<Atom, Solver::Result::Assignment>> Sorted = {
+ Solution->begin(), Solution->end()};
+ llvm::sort(Sorted);
+ for (const auto &Entry : Sorted)
+ OS << Entry.first << " = " << Entry.second << "\n";
}
-
- /// Returns the name assigned to `Atom`, either user-specified or created by
- /// default rules (B0, B1, ...).
- std::string getAtomName(const AtomicBoolValue *Atom) {
- auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter));
- if (Entry.second) {
- Counter++;
- }
- return Entry.first->second;
- }
-
- // Keep track of number of atoms without a user-specified name, used to assign
- // non-repeating default names to such atoms.
- size_t Counter;
-
- // Keep track of names assigned to atoms.
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames;
-};
-
-} // namespace
-
-std::string
-debugString(const BoolValue &B,
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
- return DebugStringGenerator(std::move(AtomNames)).debugString(B);
-}
-
-std::string
-debugString(llvm::ArrayRef<BoolValue *> Constraints,
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
- return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints);
-}
-
-std::string
-debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
- return DebugStringGenerator(std::move(AtomNames))
- .debugString(Constraints, Result);
+ return OS;
}
} // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp
new file mode 100644
index 00000000000000..504ad2fb7938af
--- /dev/null
+++ b/clang/lib/Analysis/FlowSensitive/Formula.cpp
@@ -0,0 +1,82 @@
+//===- 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/Basic/LLVM.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Allocator.h"
+#include "llvm/Support/ErrorHandling.h"
+#include <cassert>
+
+namespace clang::dataflow {
+
+Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
+ ArrayRef<const Formula *> Operands, unsigned Value) {
+ assert(Operands.size() == numOperands(K));
+ if (Value != 0) // Currently, formulas have values or operands, not both.
+ assert(numOperands(K) == 0);
+ void *Mem = Alloc.Allocate(sizeof(Formula) +
+ Operands.size() * sizeof(Operands.front()),
+ alignof(Formula));
+ Formula *Result = new (Mem) Formula();
+ Result->FormulaKind = K;
+ Result->Value = Value;
+ // Operands are stored as `const Formula *`s after the formula itself.
+ // We don't need to construct an object as pointers are trivial types.
+ // Formula is alignas(const Formula *), so alignment is satisfied.
+ llvm::copy(Operands, reinterpret_cast<const Formula **>(Result + 1));
+ return *Result;
+}
+
+static llvm::StringLiteral sigil(Formula::Kind K) {
+ switch (K) {
+ case Formula::AtomRef:
+ return "";
+ 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 Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const {
+ if (Names && kind() == AtomRef)
+ if (auto It = Names->find(getAtom()); It != Names->end()) {
+ OS << It->second;
+ return;
+ }
+
+ switch (numOperands(kind())) {
+ case 0:
+ OS << getAtom();
+ break;
+ case 1:
+ OS << sigil(kind());
+ operands()[0]->print(OS, Names);
+ break;
+ case 2:
+ OS << '(';
+ operands()[0]->print(OS, Names);
+ OS << sigil(kind());
+ operands()[1]->print(OS, Names);
+ OS << ')';
+ break;
+ default:
+ llvm_unreachable("unhandled formula arity");
+ }
+}
+
+} // namespace clang::dataflow
\ No newline at end of file
diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
index db2e1d694457bf..037886d09c4f7d 100644
--- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -17,8 +17,8 @@
#include <queue>
#include <vector>
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/DenseMap.h"
@@ -79,7 +79,7 @@ using ClauseID = uint32_t;
static constexpr ClauseID NullClause = 0;
/// A boolean formula in conjunctive normal form.
-struct BooleanFormula {
+struct CNFFormula {
/// `LargestVar` is equal to the largest positive integer that represents a
/// variable in the formula.
const Variable LargestVar;
@@ -121,12 +121,12 @@ struct BooleanFormula {
/// clauses in the formula start from the element at index 1.
std::vector<ClauseID> NextWatched;
- /// Stores the variable identifier and value location for atomic booleans in
- /// the formula.
- llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
+ /// Stores the variable identifier and Atom for atomic booleans in the
+ /// formula.
+ llvm::DenseMap<Variable, Atom> Atomics;
- explicit BooleanFormula(Variable LargestVar,
- llvm::DenseMap<Variable, AtomicBoolValue *> Atomics)
+ explicit CNFFormula(Variable LargestVar,
+ llvm::DenseMap<Variable, Atom> Atomics)
: LargestVar(LargestVar), Atomics(std::move(Atomics)) {
Clauses.push_back(0);
ClauseStarts.push_back(0);
@@ -144,8 +144,8 @@ struct BooleanFormula {
///
/// All literals in the input that are not `NullLit` must be distinct.
void addClause(Literal L1, Literal L2 = NullLit, Literal L3 = NullLit) {
- // The literals are guaranteed to be distinct from properties of BoolValue
- // and the construction in `buildBooleanFormula`.
+ // The literals are guaranteed to be distinct from properties of Formula
+ // and the construction in `buildCNF`.
assert(L1 != NullLit && L1 != L2 && L1 != L3 &&
(L2 != L3 || L2 == NullLit));
@@ -178,98 +178,59 @@ struct BooleanFormula {
/// Converts the conjunction of `Vals` into a formula in conjunctive normal
/// form where each clause has at least one and at most three literals.
-BooleanFormula buildBooleanFormula(const llvm::ArrayRef<BoolValue *> &Vals) {
+CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
// The general strategy of the algorithm implemented below is to map each
// of the sub-values in `Vals` to a unique variable and use these variables in
// the resulting CNF expression to avoid exponential blow up. The number of
// literals in the resulting formula is guaranteed to be linear in the number
- // of sub-values in `Vals`.
+ // of sub-formulas in `Vals`.
- // Map each sub-value in `Vals` to a unique variable.
- llvm::DenseMap<BoolValue *, Variable> SubValsToVar;
- // Store variable identifiers and value location of atomic booleans.
- llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
+ // Map each sub-formula in `Vals` to a unique variable.
+ llvm::DenseMap<const Formula *, Variable> SubValsToVar;
+ // Store variable identifiers and Atom of atomic booleans.
+ llvm::DenseMap<Variable, Atom> Atomics;
Variable NextVar = 1;
{
- std::queue<BoolValue *> UnprocessedSubVals;
- for (BoolValue *Val : Vals)
+ std::queue<const Formula *> UnprocessedSubVals;
+ for (const Formula *Val : Vals)
UnprocessedSubVals.push(Val);
while (!UnprocessedSubVals.empty()) {
Variable Var = NextVar;
- BoolValue *Val = UnprocessedSubVals.front();
+ const Formula *Val = UnprocessedSubVals.front();
UnprocessedSubVals.pop();
if (!SubValsToVar.try_emplace(Val, Var).second)
continue;
++NextVar;
- // Visit the sub-values of `Val`.
- switch (Val->getKind()) {
- case Value::Kind::Conjunction: {
- auto *C = cast<ConjunctionValue>(Val);
- UnprocessedSubVals.push(&C->getLeftSubValue());
- UnprocessedSubVals.push(&C->getRightSubValue());
- break;
- }
- case Value::Kind::Disjunction: {
- auto *D = cast<DisjunctionValue>(Val);
- UnprocessedSubVals.push(&D->getLeftSubValue());
- UnprocessedSubVals.push(&D->getRightSubValue());
- break;
- }
- case Value::Kind::Negation: {
- auto *N = cast<NegationValue>(Val);
- UnprocessedSubVals.push(&N->getSubVal());
- break;
- }
- case Value::Kind::Implication: {
- auto *I = cast<ImplicationValue>(Val);
- UnprocessedSubVals.push(&I->getLeftSubValue());
- UnprocessedSubVals.push(&I->getRightSubValue());
- break;
- }
- case Value::Kind::Biconditional: {
- auto *B = cast<BiconditionalValue>(Val);
- UnprocessedSubVals.push(&B->getLeftSubValue());
- UnprocessedSubVals.push(&B->getRightSubValue());
- break;
- }
- case Value::Kind::TopBool:
- // Nothing more to do. This `TopBool` instance has already been mapped
- // to a fresh solver variable (`NextVar`, above) and is thereafter
- // anonymous. The solver never sees `Top`.
- break;
- case Value::Kind::AtomicBool: {
- Atomics[Var] = cast<AtomicBoolValue>(Val);
- break;
- }
- default:
- llvm_unreachable("buildBooleanFormula: unhandled value kind");
- }
+ for (const Formula *F : Val->operands())
+ UnprocessedSubVals.push(F);
+ if (Val->kind() == Formula::AtomRef)
+ Atomics[Var] = Val->getAtom();
}
}
- auto GetVar = [&SubValsToVar](const BoolValue *Val) {
+ auto GetVar = [&SubValsToVar](const Formula *Val) {
auto ValIt = SubValsToVar.find(Val);
assert(ValIt != SubValsToVar.end());
return ValIt->second;
};
- BooleanFormula Formula(NextVar - 1, std::move(Atomics));
+ CNFFormula CNF(NextVar - 1, std::move(Atomics));
std::vector<bool> ProcessedSubVals(NextVar, false);
- // Add a conjunct for each variable that represents a top-level conjunction
- // value in `Vals`.
- for (BoolValue *Val : Vals)
- Formula.addClause(posLit(GetVar(Val)));
+ // Add a conjunct for each variable that represents a top-level formula in
+ // `Vals`.
+ for (const Formula *Val : Vals)
+ CNF.addClause(posLit(GetVar(Val)));
// Add conjuncts that represent the mapping between newly-created variables
- // and their corresponding sub-values.
- std::queue<BoolValue *> UnprocessedSubVals;
- for (BoolValue *Val : Vals)
+ // and their corresponding sub-formulas.
+ std::queue<const Formula *> UnprocessedSubVals;
+ for (const Formula *Val : Vals)
UnprocessedSubVals.push(Val);
while (!UnprocessedSubVals.empty()) {
- const BoolValue *Val = UnprocessedSubVals.front();
+ const Formula *Val = UnprocessedSubVals.front();
UnprocessedSubVals.pop();
const Variable Var = GetVar(Val);
@@ -277,117 +238,107 @@ BooleanFormula buildBooleanFormula(const llvm::ArrayRef<BoolValue *> &Vals) {
continue;
ProcessedSubVals[Var] = true;
- if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
- const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
- const Variable RightSubVar = GetVar(&C->getRightSubValue());
+ switch (Val->kind()) {
+ case Formula::AtomRef:
+ break;
+ case Formula::And: {
+ const Variable LHS = GetVar(Val->operands()[0]);
+ const Variable RHS = GetVar(Val->operands()[1]);
- if (LeftSubVar == RightSubVar) {
+ if (LHS == RHS) {
// `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is
// already in conjunctive normal form. Below we add each of the
// conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar));
-
- // Visit a sub-value of `Val` (pick any, they are identical).
- UnprocessedSubVals.push(&C->getLeftSubValue());
+ CNF.addClause(negLit(Var), posLit(LHS));
+ CNF.addClause(posLit(Var), negLit(LHS));
} else {
// `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)`
// which is already in conjunctive normal form. Below we add each of the
// conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar));
- Formula.addClause(negLit(Var), posLit(RightSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&C->getLeftSubValue());
- UnprocessedSubVals.push(&C->getRightSubValue());
+ CNF.addClause(negLit(Var), posLit(LHS));
+ CNF.addClause(negLit(Var), posLit(RHS));
+ CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
}
- } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
- const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
- const Variable RightSubVar = GetVar(&D->getRightSubValue());
+ break;
+ }
+ case Formula::Or: {
+ const Variable LHS = GetVar(Val->operands()[0]);
+ const Variable RHS = GetVar(Val->operands()[1]);
- if (LeftSubVar == RightSubVar) {
+ if (LHS == RHS) {
// `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` which is
// already in conjunctive normal form. Below we add each of the
// conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar));
-
- // Visit a sub-value of `Val` (pick any, they are identical).
- UnprocessedSubVals.push(&D->getLeftSubValue());
+ CNF.addClause(negLit(Var), posLit(LHS));
+ CNF.addClause(posLit(Var), negLit(LHS));
} else {
- // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)`
- // which is already in conjunctive normal form. Below we add each of the
- // conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar));
- Formula.addClause(posLit(Var), negLit(RightSubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&D->getLeftSubValue());
- UnprocessedSubVals.push(&D->getRightSubValue());
+ // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v
+ // !B)` which is already in conjunctive normal form. Below we add each
+ // of the conjuncts of the latter expression to the result.
+ CNF.addClause(negLit(Var), posLit(LHS), posLit(RHS));
+ CNF.addClause(posLit(Var), negLit(LHS));
+ CNF.addClause(posLit(Var), negLit(RHS));
}
- } else if (auto *N = dyn_cast<NegationValue>(Val)) {
- const Variable SubVar = GetVar(&N->getSubVal());
-
- // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is already in
- // conjunctive normal form. Below we add each of the conjuncts of the
- // latter expression to the result.
- Formula.addClause(negLit(Var), negLit(SubVar));
- Formula.addClause(posLit(Var), posLit(SubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&N->getSubVal());
- } else if (auto *I = dyn_cast<ImplicationValue>(Val)) {
- const Variable LeftSubVar = GetVar(&I->getLeftSubValue());
- const Variable RightSubVar = GetVar(&I->getRightSubValue());
+ break;
+ }
+ case Formula::Not: {
+ const Variable Operand = GetVar(Val->operands()[0]);
+
+ // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is
+ // already in conjunctive normal form. Below we add each of the
+ // conjuncts of the latter expression to the result.
+ CNF.addClause(negLit(Var), negLit(Operand));
+ CNF.addClause(posLit(Var), posLit(Operand));
+ break;
+ }
+ case Formula::Implies: {
+ const Variable LHS = GetVar(Val->operands()[0]);
+ const Variable RHS = GetVar(Val->operands()[1]);
// `X <=> (A => B)` is equivalent to
// `(X v A) ^ (X v !B) ^ (!X v !A v B)` which is already in
- // conjunctive normal form. Below we add each of the conjuncts of the
- // latter expression to the result.
- Formula.addClause(posLit(Var), posLit(LeftSubVar));
- Formula.addClause(posLit(Var), negLit(RightSubVar));
- Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&I->getLeftSubValue());
- UnprocessedSubVals.push(&I->getRightSubValue());
- } else if (auto *B = dyn_cast<BiconditionalValue>(Val)) {
- const Variable LeftSubVar = GetVar(&B->getLeftSubValue());
- const Variable RightSubVar = GetVar(&B->getRightSubValue());
-
- if (LeftSubVar == RightSubVar) {
+ // conjunctive normal form. Below we add each of the conjuncts of
+ // the latter expression to the result.
+ CNF.addClause(posLit(Var), posLit(LHS));
+ CNF.addClause(posLit(Var), negLit(RHS));
+ CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS));
+ break;
+ }
+ case Formula::Equal: {
+ const Variable LHS = GetVar(Val->operands()[0]);
+ const Variable RHS = GetVar(Val->operands()[1]);
+
+ if (LHS == RHS) {
// `X <=> (A <=> A)` is equvalent to `X` which is already in
// conjunctive normal form. Below we add each of the conjuncts of the
// latter expression to the result.
- Formula.addClause(posLit(Var));
+ CNF.addClause(posLit(Var));
// No need to visit the sub-values of `Val`.
- } else {
- // `X <=> (A <=> B)` is equivalent to
- // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which is
- // already in conjunctive normal form. Below we add each of the conjuncts
- // of the latter expression to the result.
- Formula.addClause(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
- Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar));
- Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&B->getLeftSubValue());
- UnprocessedSubVals.push(&B->getRightSubValue());
+ continue;
}
+ // `X <=> (A <=> B)` is equivalent to
+ // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which
+ // is already in conjunctive normal form. Below we add each of the
+ // conjuncts of the latter expression to the result.
+ CNF.addClause(posLit(Var), posLit(LHS), posLit(RHS));
+ CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
+ CNF.addClause(negLit(Var), posLit(LHS), negLit(RHS));
+ CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS));
+ break;
+ }
}
+ for (const Formula *Child : Val->operands())
+ UnprocessedSubVals.push(Child);
}
- return Formula;
+ return CNF;
}
class WatchedLiteralsSolverImpl {
/// A boolean formula in conjunctive normal form that the solver will attempt
/// to prove satisfiable. The formula will be modified in the process.
- BooleanFormula Formula;
+ CNFFormula CNF;
/// The search for a satisfying assignment of the variables in `Formula` will
/// proceed in levels, starting from 1 and going up to `Formula.LargestVar`
@@ -439,9 +390,10 @@ class WatchedLiteralsSolverImpl {
std::vector<Variable> ActiveVars;
public:
- explicit WatchedLiteralsSolverImpl(const llvm::ArrayRef<BoolValue *> &Vals)
- : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),
- LevelStates(Formula.LargestVar + 1) {
+ explicit WatchedLiteralsSolverImpl(
+ const llvm::ArrayRef<const Formula *> &Vals)
+ : CNF(buildCNF(Vals)), LevelVars(CNF.LargestVar + 1),
+ LevelStates(CNF.LargestVar + 1) {
assert(!Vals.empty());
// Initialize the state at the root level to a decision so that in
@@ -450,10 +402,10 @@ class WatchedLiteralsSolverImpl {
LevelStates[0] = State::Decision;
// Initialize all variables as unassigned.
- VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned);
+ VarAssignments.resize(CNF.LargestVar + 1, Assignment::Unassigned);
// Initialize the active variables.
- for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {
+ for (Variable Var = CNF.LargestVar; Var != NullVar; --Var) {
if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
ActiveVars.push_back(Var);
}
@@ -474,7 +426,7 @@ class WatchedLiteralsSolverImpl {
// 3. Unassigned variables that form watched literals are active.
// FIXME: Consider replacing these with test cases that fail if the any
// of the invariants is broken. That might not be easy due to the
- // transformations performed by `buildBooleanFormula`.
+ // transformations performed by `buildCNF`.
assert(activeVarsAreUnassigned());
assert(activeVarsFormWatchedLiterals());
assert(unassignedVarsFormingWatchedLiteralsAreActive());
@@ -555,12 +507,10 @@ class WatchedLiteralsSolverImpl {
}
private:
- /// Returns a satisfying truth assignment to the atomic values in the boolean
- /// formula.
- llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
- buildSolution() {
- llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> Solution;
- for (auto &Atomic : Formula.Atomics) {
+ /// Returns a satisfying truth assignment to the atoms in the boolean formula.
+ llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() {
+ llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;
+ for (auto &Atomic : CNF.Atomics) {
// A variable may have a definite true/false assignment, or it may be
// unassigned indicating its truth value does not affect the result of
// the formula. Unassigned variables are assigned to true as a default.
@@ -596,24 +546,24 @@ class WatchedLiteralsSolverImpl {
const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
? negLit(Var)
: posLit(Var);
- ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit];
- Formula.WatchedHead[FalseLit] = NullClause;
+ ClauseID FalseLitWatcher = CNF.WatchedHead[FalseLit];
+ CNF.WatchedHead[FalseLit] = NullClause;
while (FalseLitWatcher != NullClause) {
- const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher];
+ const ClauseID NextFalseLitWatcher = CNF.NextWatched[FalseLitWatcher];
// Pick the first non-false literal as the new watched literal.
- const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher];
+ const size_t FalseLitWatcherStart = CNF.ClauseStarts[FalseLitWatcher];
size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
- while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx]))
+ while (isCurrentlyFalse(CNF.Clauses[NewWatchedLitIdx]))
++NewWatchedLitIdx;
- const Literal NewWatchedLit = Formula.Clauses[NewWatchedLitIdx];
+ const Literal NewWatchedLit = CNF.Clauses[NewWatchedLitIdx];
const Variable NewWatchedLitVar = var(NewWatchedLit);
// Swap the old watched literal for the new one in `FalseLitWatcher` to
// maintain the invariant that the watched literal is at the beginning of
// the clause.
- Formula.Clauses[NewWatchedLitIdx] = FalseLit;
- Formula.Clauses[FalseLitWatcherStart] = NewWatchedLit;
+ CNF.Clauses[NewWatchedLitIdx] = FalseLit;
+ CNF.Clauses[FalseLitWatcherStart] = NewWatchedLit;
// If the new watched literal isn't watched by any other clause and its
// variable isn't assigned we need to add it to the active variables.
@@ -621,8 +571,8 @@ class WatchedLiteralsSolverImpl {
VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
ActiveVars.push_back(NewWatchedLitVar);
- Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit];
- Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher;
+ CNF.NextWatched[FalseLitWatcher] = CNF.WatchedHead[NewWatchedLit];
+ CNF.WatchedHead[NewWatchedLit] = FalseLitWatcher;
// Go to the next clause that watches `FalseLit`.
FalseLitWatcher = NextFalseLitWatcher;
@@ -632,16 +582,15 @@ class WatchedLiteralsSolverImpl {
/// Returns true if and only if one of the clauses that watch `Lit` is a unit
/// clause.
bool watchedByUnitClause(Literal Lit) const {
- for (ClauseID LitWatcher = Formula.WatchedHead[Lit];
- LitWatcher != NullClause;
- LitWatcher = Formula.NextWatched[LitWatcher]) {
- llvm::ArrayRef<Literal> Clause = Formula.clauseLiterals(LitWatcher);
+ for (ClauseID LitWatcher = CNF.WatchedHead[Lit]; LitWatcher != NullClause;
+ LitWatcher = CNF.NextWatched[LitWatcher]) {
+ llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);
// Assert the invariant that the watched literal is always the first one
// in the clause.
// FIXME: Consider replacing this with a test case that fails if the
// invariant is broken by `updateWatchedLiterals`. That might not be easy
- // due to the transformations performed by `buildBooleanFormula`.
+ // due to the transformations performed by `buildCNF`.
assert(Clause.front() == Lit);
if (isUnit(Clause))
@@ -665,7 +614,7 @@ class WatchedLiteralsSolverImpl {
/// Returns true if and only if `Lit` is watched by a clause in `Formula`.
bool isWatched(Literal Lit) const {
- return Formula.WatchedHead[Lit] != NullClause;
+ return CNF.WatchedHead[Lit] != NullClause;
}
/// Returns an assignment for an unassigned variable.
@@ -678,8 +627,8 @@ class WatchedLiteralsSolverImpl {
/// Returns a set of all watched literals.
llvm::DenseSet<Literal> watchedLiterals() const {
llvm::DenseSet<Literal> WatchedLiterals;
- for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {
- if (Formula.WatchedHead[Lit] == NullClause)
+ for (Literal Lit = 2; Lit < CNF.WatchedHead.size(); Lit++) {
+ if (CNF.WatchedHead[Lit] == NullClause)
continue;
WatchedLiterals.insert(Lit);
}
@@ -719,7 +668,8 @@ class WatchedLiteralsSolverImpl {
}
};
-Solver::Result WatchedLiteralsSolver::solve(llvm::ArrayRef<BoolValue *> Vals) {
+Solver::Result
+WatchedLiteralsSolver::solve(llvm::ArrayRef<const Formula *> Vals) {
if (Vals.empty())
return Solver::Result::Satisfiable({{}});
auto [Res, Iterations] =
diff --git a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
index 407abf58529a50..53131723ff5cef 100644
--- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
@@ -7,6 +7,7 @@
//===----------------------------------------------------------------------===//
#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "llvm/Support/ScopedPrinter.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -125,5 +126,26 @@ TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
EXPECT_NE(&XIffY1, &XIffZ);
}
+TEST_F(ArenaTest, ValueToFormula) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &Y = A.create<AtomicBoolValue>();
+ auto &XIffY = A.makeEquals(X, Y);
+ auto &XOrNotY = A.makeOr(X, A.makeNot(Y));
+ auto &Implies = A.makeImplies(XIffY, XOrNotY);
+
+ EXPECT_EQ(llvm::to_string(A.getFormula(Implies)),
+ "((V0 = V1) => (V0 | !V1))");
+}
+
+TEST_F(ArenaTest, ValueToFormulaCached) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &Y = A.create<AtomicBoolValue>();
+ auto &XIffY = A.makeEquals(X, Y);
+
+ auto &Formula1 = A.getFormula(XIffY);
+ auto &Formula2 = A.getFormula(XIffY);
+ EXPECT_EQ(&Formula1, &Formula2);
+}
+
} // namespace
} // namespace clang::dataflow
diff --git a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
index 10fcd204c9ab07..8ee56ae08b98a9 100644
--- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -8,8 +8,9 @@
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "TestingSupport.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
-#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "llvm/Support/ScopedPrinter.h"
+#include "llvm/Support/raw_ostream.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -22,429 +23,88 @@ using test::ConstraintContext;
using testing::StrEq;
TEST(BoolValueDebugStringTest, AtomicBoolean) {
- // B0
ConstraintContext Ctx;
auto B = Ctx.atom();
- auto Expected = R"(B0)";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, Top) {
- ConstraintContext Ctx;
- auto B = Ctx.top();
-
- auto Expected = R"(top)";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "V0";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Negation) {
- // !B0
ConstraintContext Ctx;
auto B = Ctx.neg(Ctx.atom());
- auto Expected = R"((not
- B0))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "!V0";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Conjunction) {
- // B0 ^ B1
ConstraintContext Ctx;
auto B = Ctx.conj(Ctx.atom(), Ctx.atom());
- auto Expected = R"((and
- B0
- B1))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "(V0 & V1)";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Disjunction) {
- // B0 v B1
ConstraintContext Ctx;
auto B = Ctx.disj(Ctx.atom(), Ctx.atom());
- auto Expected = R"((or
- B0
- B1))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "(V0 | V1)";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Implication) {
- // B0 => B1
ConstraintContext Ctx;
auto B = Ctx.impl(Ctx.atom(), Ctx.atom());
- auto Expected = R"((=>
- B0
- B1))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "(V0 => V1)";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Iff) {
- // B0 <=> B1
ConstraintContext Ctx;
auto B = Ctx.iff(Ctx.atom(), Ctx.atom());
- auto Expected = R"((=
- B0
- B1))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "(V0 = V1)";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Xor) {
- // (B0 ^ !B1) V (!B0 ^ B1)
ConstraintContext Ctx;
auto B0 = Ctx.atom();
auto B1 = Ctx.atom();
auto B = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
- auto Expected = R"((or
- (and
- B0
- (not
- B1))
- (and
- (not
- B0)
- B1)))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "((V0 & !V1) | (!V0 & V1))";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, NestedBoolean) {
- // B0 ^ (B1 v (B2 ^ (B3 v B4)))
ConstraintContext Ctx;
auto B = Ctx.conj(
Ctx.atom(),
Ctx.disj(Ctx.atom(),
Ctx.conj(Ctx.atom(), Ctx.disj(Ctx.atom(), Ctx.atom()))));
- auto Expected = R"((and
- B0
- (or
- B1
- (and
- B2
- (or
- B3
- B4)))))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, AtomicBooleanWithName) {
- // True
- ConstraintContext Ctx;
- auto True = cast<AtomicBoolValue>(Ctx.atom());
- auto B = True;
-
- auto Expected = R"(True)";
- EXPECT_THAT(debugString(*B, {{True, "True"}}), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, ComplexBooleanWithNames) {
- // (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
- ConstraintContext Ctx;
- auto Cond = cast<AtomicBoolValue>(Ctx.atom());
- auto Then = cast<AtomicBoolValue>(Ctx.atom());
- auto Else = cast<AtomicBoolValue>(Ctx.atom());
- auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
- Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
-
- auto Expected = R"((or
- (and
- Cond
- (and
- Then
- (not
- Else)))
- (and
- (not
- Cond)
- (and
- (not
- Then)
- Else))))";
- EXPECT_THAT(debugString(*B, {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
- StrEq(Expected));
+ auto Expected = "(V0 & (V1 | (V2 & (V3 | V4))))";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
- // (False && B0) v (True v B1)
ConstraintContext Ctx;
- auto True = cast<AtomicBoolValue>(Ctx.atom());
- auto False = cast<AtomicBoolValue>(Ctx.atom());
+ auto True = Ctx.atom();
+ auto False = Ctx.atom();
+ Formula::AtomNames Names;
+ Names[True->getAtom()] = "true";
+ Names[False->getAtom()] = "false";
auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom()));
- auto Expected = R"((or
- (and
- False
- B0)
- (or
- True
- B1)))";
- EXPECT_THAT(debugString(*B, {{True, "True"}, {False, "False"}}),
- StrEq(Expected));
-}
-
-TEST(ConstraintSetDebugStringTest, Empty) {
- llvm::ArrayRef<BoolValue *> Constraints;
- EXPECT_THAT(debugString(Constraints), StrEq(""));
-}
-
-TEST(ConstraintSetDebugStringTest, Simple) {
- ConstraintContext Ctx;
- std::vector<BoolValue *> Constraints;
- auto X = cast<AtomicBoolValue>(Ctx.atom());
- auto Y = cast<AtomicBoolValue>(Ctx.atom());
- Constraints.push_back(Ctx.disj(X, Y));
- Constraints.push_back(Ctx.disj(X, Ctx.neg(Y)));
-
- auto Expected = R"((or
- X
- Y)
-(or
- X
- (not
- Y))
-)";
- EXPECT_THAT(debugString(Constraints, {{X, "X"}, {Y, "Y"}}),
- StrEq(Expected));
-}
-
-Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) {
- return WatchedLiteralsSolver().solve(std::move(Constraints));
-}
-
-TEST(SATCheckDebugStringTest, AtomicBoolean) {
- // B0
- ConstraintContext Ctx;
- std::vector<BoolValue *> Constraints({Ctx.atom()});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-B0
-------------
-Satisfiable.
-
-B0 = True
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, AtomicBooleanAndNegation) {
- // B0, !B0
- ConstraintContext Ctx;
- auto B0 = Ctx.atom();
- std::vector<BoolValue *> Constraints({B0, Ctx.neg(B0)});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-B0
-
-(not
- B0)
-------------
-Unsatisfiable.
-
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, MultipleAtomicBooleans) {
- // B0, B1
- ConstraintContext Ctx;
- std::vector<BoolValue *> Constraints({Ctx.atom(), Ctx.atom()});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-B0
-
-B1
-------------
-Satisfiable.
-
-B0 = True
-B1 = True
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, Implication) {
- // B0, B0 => B1
- ConstraintContext Ctx;
- auto B0 = Ctx.atom();
- auto B1 = Ctx.atom();
- auto Impl = Ctx.disj(Ctx.neg(B0), B1);
- std::vector<BoolValue *> Constraints({B0, Impl});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-B0
-
-(or
- (not
- B0)
- B1)
-------------
-Satisfiable.
-
-B0 = True
-B1 = True
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+ auto Expected = R"(((false & V2) | (true | V3)))";
+ std::string Actual;
+ llvm::raw_string_ostream OS(Actual);
+ B->print(OS, &Names);
+ EXPECT_THAT(Actual, StrEq(Expected));
}
-TEST(SATCheckDebugStringTest, Iff) {
- // B0, B0 <=> B1
- ConstraintContext Ctx;
- auto B0 = Ctx.atom();
- auto B1 = Ctx.atom();
- auto Iff = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));
- std::vector<BoolValue *> Constraints({B0, Iff});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-B0
-
-(and
- (or
- (not
- B0)
- B1)
- (or
- B0
- (not
- B1)))
-------------
-Satisfiable.
-
-B0 = True
-B1 = True
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, Xor) {
- // B0, XOR(B0, B1)
- ConstraintContext Ctx;
- auto B0 = Ctx.atom();
- auto B1 = Ctx.atom();
- auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
- std::vector<BoolValue *> Constraints({B0, XOR});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-B0
-
-(or
- (and
- B0
- (not
- B1))
- (and
- (not
- B0)
- B1))
-------------
-Satisfiable.
-
-B0 = True
-B1 = False
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, ComplexBooleanWithNames) {
- // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
- ConstraintContext Ctx;
- auto Cond = cast<AtomicBoolValue>(Ctx.atom());
- auto Then = cast<AtomicBoolValue>(Ctx.atom());
- auto Else = cast<AtomicBoolValue>(Ctx.atom());
- auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
- Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
- std::vector<BoolValue *> Constraints({Cond, B});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-Cond
-
-(or
- (and
- Cond
- (and
- Then
- (not
- Else)))
- (and
- (not
- Cond)
- (and
- (not
- Then)
- Else)))
-------------
-Satisfiable.
-
-Cond = True
-Else = False
-Then = True
-)";
- EXPECT_THAT(debugString(Constraints, Result,
- {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
- StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, ComplexBooleanWithLongNames) {
- // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq
- ConstraintContext Ctx;
- auto IntsAreEq = cast<AtomicBoolValue>(Ctx.atom());
- auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
- auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
- auto BothZeroImpliesEQ =
- Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);
- std::vector<BoolValue *> Constraints(
- {ThisIntEqZero, Ctx.neg(IntsAreEq), BothZeroImpliesEQ});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-ThisIntEqZero
-
-(not
- IntsAreEq)
-
-(or
- (not
- (and
- ThisIntEqZero
- OtherIntEqZero))
- IntsAreEq)
-------------
-Satisfiable.
-
-IntsAreEq = False
-OtherIntEqZero = False
-ThisIntEqZero = True
-)";
- EXPECT_THAT(debugString(Constraints, Result,
- {{IntsAreEq, "IntsAreEq"},
- {ThisIntEqZero, "ThisIntEqZero"},
- {OtherIntEqZero, "OtherIntEqZero"}}),
- StrEq(Expected));
-}
} // namespace
diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
index 9999dd3a475f1b..ba0a77a910d7c4 100644
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -9,9 +9,10 @@
#include <utility>
#include "TestingSupport.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "llvm/ADT/ArrayRef.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -23,26 +24,31 @@ using namespace dataflow;
using test::ConstraintContext;
using testing::_;
using testing::AnyOf;
-using testing::IsEmpty;
-using testing::Optional;
using testing::Pair;
using testing::UnorderedElementsAre;
+constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue;
+constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse;
+
// Checks if the conjunction of `Vals` is satisfiable and returns the
// corresponding result.
-Solver::Result solve(llvm::ArrayRef<BoolValue *> Vals) {
+Solver::Result solve(llvm::ArrayRef<const Formula *> Vals) {
return WatchedLiteralsSolver().solve(Vals);
}
-void expectUnsatisfiable(Solver::Result Result) {
- EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable);
- EXPECT_FALSE(Result.getSolution().has_value());
+MATCHER(unsat, "") {
+ return arg.getStatus() == Solver::Result::Status::Unsatisfiable;
}
-
-template <typename Matcher>
-void expectSatisfiable(Solver::Result Result, Matcher Solution) {
- EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable);
- EXPECT_THAT(Result.getSolution(), Optional(Solution));
+MATCHER_P(sat, SolutionMatcher,
+ "is satisfiable, where solution " +
+ (testing::DescribeMatcher<
+ llvm::DenseMap<Atom, Solver::Result::Assignment>>(
+ SolutionMatcher))) {
+ if (arg.getStatus() != Solver::Result::Status::Satisfiable)
+ return false;
+ auto Solution = *arg.getSolution();
+ return testing::ExplainMatchResult(SolutionMatcher, Solution,
+ result_listener);
}
TEST(SolverTest, Var) {
@@ -50,9 +56,8 @@ TEST(SolverTest, Var) {
auto X = Ctx.atom();
// X
- expectSatisfiable(
- solve({X}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue)));
+ EXPECT_THAT(solve({X}),
+ sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue))));
}
TEST(SolverTest, NegatedVar) {
@@ -61,9 +66,8 @@ TEST(SolverTest, NegatedVar) {
auto NotX = Ctx.neg(X);
// !X
- expectSatisfiable(
- solve({NotX}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse)));
+ EXPECT_THAT(solve({NotX}),
+ sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse))));
}
TEST(SolverTest, UnitConflict) {
@@ -72,7 +76,7 @@ TEST(SolverTest, UnitConflict) {
auto NotX = Ctx.neg(X);
// X ^ !X
- expectUnsatisfiable(solve({X, NotX}));
+ EXPECT_THAT(solve({X, NotX}), unsat());
}
TEST(SolverTest, DistinctVars) {
@@ -82,36 +86,9 @@ TEST(SolverTest, DistinctVars) {
auto NotY = Ctx.neg(Y);
// X ^ !Y
- expectSatisfiable(
- solve({X, NotY}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
- Pair(Y, Solver::Result::Assignment::AssignedFalse)));
-}
-
-TEST(SolverTest, Top) {
- ConstraintContext Ctx;
- auto X = Ctx.top();
-
- // X. Since Top is anonymous, we do not get any results in the solution.
- expectSatisfiable(solve({X}), IsEmpty());
-}
-
-TEST(SolverTest, NegatedTop) {
- ConstraintContext Ctx;
- auto X = Ctx.top();
-
- // !X
- expectSatisfiable(solve({Ctx.neg(X)}), IsEmpty());
-}
-
-TEST(SolverTest, DistinctTops) {
- ConstraintContext Ctx;
- auto X = Ctx.top();
- auto Y = Ctx.top();
- auto NotY = Ctx.neg(Y);
-
- // X ^ !Y
- expectSatisfiable(solve({X, NotY}), IsEmpty());
+ EXPECT_THAT(solve({X, NotY}),
+ sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
+ Pair(Y->getAtom(), AssignedFalse))));
}
TEST(SolverTest, DoubleNegation) {
@@ -121,7 +98,7 @@ TEST(SolverTest, DoubleNegation) {
auto NotNotX = Ctx.neg(NotX);
// !!X ^ !X
- expectUnsatisfiable(solve({NotNotX, NotX}));
+ EXPECT_THAT(solve({NotNotX, NotX}), unsat());
}
TEST(SolverTest, NegatedDisjunction) {
@@ -132,7 +109,7 @@ TEST(SolverTest, NegatedDisjunction) {
auto NotXOrY = Ctx.neg(XOrY);
// !(X v Y) ^ (X v Y)
- expectUnsatisfiable(solve({NotXOrY, XOrY}));
+ EXPECT_THAT(solve({NotXOrY, XOrY}), unsat());
}
TEST(SolverTest, NegatedConjunction) {
@@ -143,7 +120,7 @@ TEST(SolverTest, NegatedConjunction) {
auto NotXAndY = Ctx.neg(XAndY);
// !(X ^ Y) ^ (X ^ Y)
- expectUnsatisfiable(solve({NotXAndY, XAndY}));
+ EXPECT_THAT(solve({NotXAndY, XAndY}), unsat());
}
TEST(SolverTest, DisjunctionSameVarWithNegation) {
@@ -153,7 +130,7 @@ TEST(SolverTest, DisjunctionSameVarWithNegation) {
auto XOrNotX = Ctx.disj(X, NotX);
// X v !X
- expectSatisfiable(solve({XOrNotX}), _);
+ EXPECT_THAT(solve({XOrNotX}), sat(_));
}
TEST(SolverTest, DisjunctionSameVar) {
@@ -162,7 +139,7 @@ TEST(SolverTest, DisjunctionSameVar) {
auto XOrX = Ctx.disj(X, X);
// X v X
- expectSatisfiable(solve({XOrX}), _);
+ EXPECT_THAT(solve({XOrX}), sat(_));
}
TEST(SolverTest, ConjunctionSameVarsConflict) {
@@ -172,7 +149,7 @@ TEST(SolverTest, ConjunctionSameVarsConflict) {
auto XAndNotX = Ctx.conj(X, NotX);
// X ^ !X
- expectUnsatisfiable(solve({XAndNotX}));
+ EXPECT_THAT(solve({XAndNotX}), unsat());
}
TEST(SolverTest, ConjunctionSameVar) {
@@ -181,7 +158,7 @@ TEST(SolverTest, ConjunctionSameVar) {
auto XAndX = Ctx.conj(X, X);
// X ^ X
- expectSatisfiable(solve({XAndX}), _);
+ EXPECT_THAT(solve({XAndX}), sat(_));
}
TEST(SolverTest, PureVar) {
@@ -194,10 +171,9 @@ TEST(SolverTest, PureVar) {
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (!X v Y) ^ (!X v !Y)
- expectSatisfiable(
- solve({NotXOrY, NotXOrNotY}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
- Pair(Y, _)));
+ EXPECT_THAT(solve({NotXOrY, NotXOrNotY}),
+ sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
+ Pair(Y->getAtom(), _))));
}
TEST(SolverTest, MustAssumeVarIsFalse) {
@@ -211,10 +187,9 @@ TEST(SolverTest, MustAssumeVarIsFalse) {
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y)
- expectSatisfiable(
- solve({XOrY, NotXOrY, NotXOrNotY}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
- Pair(Y, Solver::Result::Assignment::AssignedTrue)));
+ EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY}),
+ sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
+ Pair(Y->getAtom(), AssignedTrue))));
}
TEST(SolverTest, DeepConflict) {
@@ -229,7 +204,7 @@ TEST(SolverTest, DeepConflict) {
auto XOrNotY = Ctx.disj(X, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
- expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));
+ EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat());
}
TEST(SolverTest, IffIsEquivalentToDNF) {
@@ -243,7 +218,7 @@ TEST(SolverTest, IffIsEquivalentToDNF) {
auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF));
// !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
- expectUnsatisfiable(solve({NotEquivalent}));
+ EXPECT_THAT(solve({NotEquivalent}), unsat());
}
TEST(SolverTest, IffSameVars) {
@@ -252,7 +227,7 @@ TEST(SolverTest, IffSameVars) {
auto XEqX = Ctx.iff(X, X);
// X <=> X
- expectSatisfiable(solve({XEqX}), _);
+ EXPECT_THAT(solve({XEqX}), sat(_));
}
TEST(SolverTest, IffDistinctVars) {
@@ -262,14 +237,12 @@ TEST(SolverTest, IffDistinctVars) {
auto XEqY = Ctx.iff(X, Y);
// X <=> Y
- expectSatisfiable(
+ EXPECT_THAT(
solve({XEqY}),
- AnyOf(UnorderedElementsAre(
- Pair(X, Solver::Result::Assignment::AssignedTrue),
- Pair(Y, Solver::Result::Assignment::AssignedTrue)),
- UnorderedElementsAre(
- Pair(X, Solver::Result::Assignment::AssignedFalse),
- Pair(Y, Solver::Result::Assignment::AssignedFalse))));
+ sat(AnyOf(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
+ Pair(Y->getAtom(), AssignedTrue)),
+ UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
+ Pair(Y->getAtom(), AssignedFalse)))));
}
TEST(SolverTest, IffWithUnits) {
@@ -279,10 +252,9 @@ TEST(SolverTest, IffWithUnits) {
auto XEqY = Ctx.iff(X, Y);
// (X <=> Y) ^ X ^ Y
- expectSatisfiable(
- solve({XEqY, X, Y}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
- Pair(Y, Solver::Result::Assignment::AssignedTrue)));
+ EXPECT_THAT(solve({XEqY, X, Y}),
+ sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
+ Pair(Y->getAtom(), AssignedTrue))));
}
TEST(SolverTest, IffWithUnitsConflict) {
@@ -293,7 +265,7 @@ TEST(SolverTest, IffWithUnitsConflict) {
auto NotY = Ctx.neg(Y);
// (X <=> Y) ^ X !Y
- expectUnsatisfiable(solve({XEqY, X, NotY}));
+ EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
}
TEST(SolverTest, IffTransitiveConflict) {
@@ -306,7 +278,7 @@ TEST(SolverTest, IffTransitiveConflict) {
auto NotX = Ctx.neg(X);
// (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
- expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));
+ EXPECT_THAT(solve({XEqY, YEqZ, Z, NotX}), unsat());
}
TEST(SolverTest, DeMorgan) {
@@ -323,7 +295,7 @@ TEST(SolverTest, DeMorgan) {
auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
// A ^ B
- expectSatisfiable(solve({A, B}), _);
+ EXPECT_THAT(solve({A, B}), sat(_));
}
TEST(SolverTest, RespectsAdditionalConstraints) {
@@ -334,7 +306,7 @@ TEST(SolverTest, RespectsAdditionalConstraints) {
auto NotY = Ctx.neg(Y);
// (X <=> Y) ^ X ^ !Y
- expectUnsatisfiable(solve({XEqY, X, NotY}));
+ EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
}
TEST(SolverTest, ImplicationIsEquivalentToDNF) {
@@ -346,7 +318,7 @@ TEST(SolverTest, ImplicationIsEquivalentToDNF) {
auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF));
// !((X => Y) <=> (!X v Y))
- expectUnsatisfiable(solve({NotEquivalent}));
+ EXPECT_THAT(solve({NotEquivalent}), unsat());
}
TEST(SolverTest, ImplicationConflict) {
@@ -357,7 +329,7 @@ TEST(SolverTest, ImplicationConflict) {
auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
// X => Y ^ X ^ !Y
- expectUnsatisfiable(solve({XImplY, XAndNotY}));
+ EXPECT_THAT(solve({XImplY, XAndNotY}), unsat());
}
TEST(SolverTest, LowTimeoutResultsInTimedOut) {
diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
index 856737d0348550..507fd5290aef52 100644
--- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -43,6 +43,7 @@
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/StringMap.h"
#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Allocator.h"
#include "llvm/Support/Errc.h"
#include "llvm/Support/Error.h"
#include "llvm/Testing/Annotations/Annotations.h"
@@ -467,55 +468,44 @@ ValueT &getValueForDecl(ASTContext &ASTCtx, const Environment &Env,
/// Creates and owns constraints which are boolean values.
class ConstraintContext {
-public:
- // Creates an atomic boolean value.
- BoolValue *atom() {
- Vals.push_back(std::make_unique<AtomicBoolValue>());
- return Vals.back().get();
- }
+ unsigned NextAtom = 0;
+ llvm::BumpPtrAllocator A;
- // Creates an instance of the Top boolean value.
- BoolValue *top() {
- Vals.push_back(std::make_unique<TopBoolValue>());
- return Vals.back().get();
+ const Formula *make(Formula::Kind K,
+ llvm::ArrayRef<const Formula *> Operands) {
+ return &Formula::create(A, K, Operands);
}
- // Creates a boolean conjunction value.
- BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<ConjunctionValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
+public:
+ // Returns a reference to a fresh atomic variable.
+ const Formula *atom() {
+ return &Formula::create(A, Formula::AtomRef, {}, NextAtom++);
}
- // Creates a boolean disjunction value.
- BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<DisjunctionValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
+ // Creates a boolean conjunction.
+ const Formula *conj(const Formula *LHS, const Formula *RHS) {
+ return make(Formula::And, {LHS, RHS});
}
- // Creates a boolean negation value.
- BoolValue *neg(BoolValue *SubVal) {
- Vals.push_back(std::make_unique<NegationValue>(*SubVal));
- return Vals.back().get();
+ // Creates a boolean disjunction.
+ const Formula *disj(const Formula *LHS, const Formula *RHS) {
+ return make(Formula::Or, {LHS, RHS});
}
- // Creates a boolean implication value.
- BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<ImplicationValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
+ // Creates a boolean negation.
+ const Formula *neg(const Formula *Operand) {
+ return make(Formula::Not, {Operand});
}
- // Creates a boolean biconditional value.
- BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<BiconditionalValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
+ // Creates a boolean implication.
+ const Formula *impl(const Formula *LHS, const Formula *RHS) {
+ return make(Formula::Implies, {LHS, RHS});
}
-private:
- std::vector<std::unique_ptr<BoolValue>> Vals;
+ // Creates a boolean biconditional.
+ const Formula *iff(const Formula *LHS, const Formula *RHS) {
+ return make(Formula::Equal, {LHS, RHS});
+ }
};
} // namespace test
More information about the cfe-commits
mailing list