[clang] 2d8cd19 - Revert "Reland "[dataflow] Add dedicated representation of boolean formulas" and followups
Sam McCall via cfe-commits
cfe-commits at lists.llvm.org
Wed Jul 5 05:32:42 PDT 2023
Author: Sam McCall
Date: 2023-07-05T14:32:25+02:00
New Revision: 2d8cd1951202ce3acd8a3ffbfa1bd5c6d2e16a5d
URL: https://github.com/llvm/llvm-project/commit/2d8cd1951202ce3acd8a3ffbfa1bd5c6d2e16a5d
DIFF: https://github.com/llvm/llvm-project/commit/2d8cd1951202ce3acd8a3ffbfa1bd5c6d2e16a5d.diff
LOG: Revert "Reland "[dataflow] Add dedicated representation of boolean formulas" and followups
These changes are OK, but they break downstream stuff that needs more time to adapt :-(
This reverts commit 71579569f4399d3cf6bc618dcd449b5388d749cc.
This reverts commit 5e4ad816bf100b0325ed45ab1cfea18deb3ab3d1.
This reverts commit 1c3ac8dfa16c42a631968aadd0396cfe7f7778e0.
Added:
Modified:
clang/include/clang/Analysis/FlowSensitive/Arena.h
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
clang/include/clang/Analysis/FlowSensitive/Solver.h
clang/include/clang/Analysis/FlowSensitive/Value.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/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
clang/lib/Analysis/FlowSensitive/Transfer.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
Removed:
clang/include/clang/Analysis/FlowSensitive/Formula.h
clang/lib/Analysis/FlowSensitive/Formula.cpp
################################################################################
diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h
index 8437caefeeda8f..83b4ddeec02564 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Arena.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h
@@ -8,7 +8,6 @@
#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>
@@ -16,12 +15,12 @@
namespace clang::dataflow {
/// The Arena owns the objects that model data within an analysis.
-/// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`.
+/// For example, `Value` and `StorageLocation`.
class Arena {
public:
Arena()
- : True(Formula::create(Alloc, Formula::Literal, {}, 1)),
- False(Formula::create(Alloc, Formula::Literal, {}, 0)) {}
+ : TrueVal(create<AtomicBoolValue>()),
+ FalseVal(create<AtomicBoolValue>()) {}
Arena(const Arena &) = delete;
Arena &operator=(const Arena &) = delete;
@@ -57,25 +56,33 @@ class Arena {
.get());
}
- /// Creates a BoolValue wrapping a particular formula.
- ///
- /// Passing in the same formula will result in the same BoolValue.
- /// FIXME: Interning BoolValues but not other Values is inconsistent.
- /// Decide whether we want Value interning or not.
- BoolValue &makeBoolValue(const Formula &);
-
- /// Creates a fresh atom and wraps in in an AtomicBoolValue.
- /// FIXME: For now, identical-address AtomicBoolValue <=> identical atom.
- /// Stop relying on pointer identity and remove this guarantee.
- AtomicBoolValue &makeAtomValue() {
- return cast<AtomicBoolValue>(makeBoolValue(makeAtomRef(makeAtom())));
- }
-
- /// Creates a fresh Top boolean value.
- TopBoolValue &makeTopValue() {
- // No need for deduplicating: there's no way to create aliasing Tops.
- return create<TopBoolValue>(makeAtomRef(makeAtom()));
- }
+ /// Returns a boolean value that represents the conjunction of `LHS` and
+ /// `RHS`. Subsequent calls with the same arguments, regardless of their
+ /// order, will return the same result. If the given boolean values represent
+ /// the same value, the result will be the value itself.
+ BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS);
+
+ /// Returns a boolean value that represents the disjunction of `LHS` and
+ /// `RHS`. Subsequent calls with the same arguments, regardless of their
+ /// order, will return the same result. If the given boolean values represent
+ /// the same value, the result will be the value itself.
+ BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS);
+
+ /// Returns a boolean value that represents the negation of `Val`. Subsequent
+ /// calls with the same argument will return the same result.
+ BoolValue &makeNot(BoolValue &Val);
+
+ /// Returns a boolean value that represents `LHS => RHS`. Subsequent calls
+ /// with the same arguments, will return the same result. If the given boolean
+ /// values represent the same value, the result will be a value that
+ /// represents the true boolean literal.
+ BoolValue &makeImplies(BoolValue &LHS, BoolValue &RHS);
+
+ /// Returns a boolean value that represents `LHS <=> RHS`. Subsequent calls
+ /// with the same arguments, regardless of their order, will return the same
+ /// result. If the given boolean values represent the same value, the result
+ /// will be a value that represents the true boolean literal.
+ BoolValue &makeEquals(BoolValue &LHS, BoolValue &RHS);
/// Returns a symbolic integer value that models an integer literal equal to
/// `Value`. These literals are the same every time.
@@ -83,44 +90,21 @@ class Arena {
/// an integer literal is associated with.
IntegerValue &makeIntLiteral(llvm::APInt Value);
- // Factories for boolean formulas.
- // Formulas are interned: passing the same arguments return the same result.
- // For commutative operations like And/Or, interning ignores order.
- // Simplifications are applied: makeOr(X, X) => X, etc.
-
- /// Returns a formula for the conjunction of `LHS` and `RHS`.
- const Formula &makeAnd(const Formula &LHS, const Formula &RHS);
-
- /// Returns a formula for the disjunction of `LHS` and `RHS`.
- const Formula &makeOr(const Formula &LHS, const Formula &RHS);
-
- /// Returns a formula for the negation of `Val`.
- const Formula &makeNot(const Formula &Val);
-
- /// Returns a formula for `LHS => RHS`.
- const Formula &makeImplies(const Formula &LHS, const Formula &RHS);
-
- /// Returns a formula for `LHS <=> RHS`.
- const Formula &makeEquals(const Formula &LHS, const Formula &RHS);
-
- /// Returns a formula for the variable A.
- const Formula &makeAtomRef(Atom A);
-
- /// Returns a formula for a literal true/false.
- const Formula &makeLiteral(bool Value) { return Value ? True : False; }
-
- /// Returns a new atomic boolean variable, distinct from any other.
- Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
+ /// Returns a symbolic boolean value that models a boolean literal equal to
+ /// `Value`. These literals are the same every time.
+ AtomicBoolValue &makeLiteral(bool Value) const {
+ return Value ? TrueVal : FalseVal;
+ }
/// Creates a fresh flow condition and returns a token that identifies it. The
/// token can be used to perform various operations on the flow condition such
/// as adding constraints to it, forking it, joining it with another flow
/// condition, or checking implications.
- Atom makeFlowConditionToken() { return makeAtom(); }
+ AtomicBoolValue &makeFlowConditionToken() {
+ return create<AtomicBoolValue>();
+ }
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;
@@ -128,18 +112,18 @@ class Arena {
// Indices that are used to avoid recreating the same integer literals and
// composite boolean values.
llvm::DenseMap<llvm::APInt, IntegerValue *> IntegerLiterals;
- using FormulaPair = std::pair<const Formula *, const Formula *>;
- llvm::DenseMap<FormulaPair, const Formula *> Ands;
- llvm::DenseMap<FormulaPair, const Formula *> Ors;
- llvm::DenseMap<const Formula *, const Formula *> Nots;
- llvm::DenseMap<FormulaPair, const Formula *> Implies;
- llvm::DenseMap<FormulaPair, const Formula *> Equals;
- llvm::DenseMap<Atom, const Formula *> AtomRefs;
-
- llvm::DenseMap<const Formula *, BoolValue *> FormulaValues;
- unsigned NextAtom = 0;
-
- const Formula &True, &False;
+ llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
+ ConjunctionVals;
+ llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
+ DisjunctionVals;
+ llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
+ llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ImplicationValue *>
+ ImplicationVals;
+ llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
+ BiconditionalVals;
+
+ AtomicBoolValue &TrueVal;
+ AtomicBoolValue &FalseVal;
};
} // namespace clang::dataflow
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index 2a31a3477e8ceb..735f2b2d85021c 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -138,31 +138,33 @@ class DataflowAnalysisContext {
PointerValue &getOrCreateNullPointerValue(QualType PointeeType);
/// Adds `Constraint` to the flow condition identified by `Token`.
- void addFlowConditionConstraint(Atom Token, const Formula &Constraint);
+ void addFlowConditionConstraint(AtomicBoolValue &Token,
+ BoolValue &Constraint);
/// Creates a new flow condition with the same constraints as the flow
/// condition identified by `Token` and returns its token.
- Atom forkFlowCondition(Atom Token);
+ AtomicBoolValue &forkFlowCondition(AtomicBoolValue &Token);
/// Creates a new flow condition that represents the disjunction of the flow
/// conditions identified by `FirstToken` and `SecondToken`, and returns its
/// token.
- Atom joinFlowConditions(Atom FirstToken, Atom SecondToken);
+ AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
+ AtomicBoolValue &SecondToken);
/// Returns true if and only if the constraints of the flow condition
/// identified by `Token` imply that `Val` is true.
- bool flowConditionImplies(Atom Token, const Formula &);
+ bool flowConditionImplies(AtomicBoolValue &Token, BoolValue &Val);
/// Returns true if and only if the constraints of the flow condition
/// identified by `Token` are always true.
- bool flowConditionIsTautology(Atom Token);
+ bool flowConditionIsTautology(AtomicBoolValue &Token);
/// Returns true if `Val1` is equivalent to `Val2`.
/// Note: This function doesn't take into account constraints on `Val1` and
/// `Val2` imposed by the flow condition.
- bool equivalentFormulas(const Formula &Val1, const Formula &Val2);
+ bool equivalentBoolValues(BoolValue &Val1, BoolValue &Val2);
- LLVM_DUMP_METHOD void dumpFlowCondition(Atom Token,
+ LLVM_DUMP_METHOD void dumpFlowCondition(AtomicBoolValue &Token,
llvm::raw_ostream &OS = llvm::dbgs());
/// Returns the `ControlFlowContext` registered for `F`, if any. Otherwise,
@@ -179,7 +181,7 @@ class DataflowAnalysisContext {
/// included in `Constraints` to provide contextually-accurate results, e.g.
/// if any definitions or relationships of the values in `Constraints` have
/// been stored in flow conditions.
- Solver::Result querySolver(llvm::SetVector<const Formula *> Constraints);
+ Solver::Result querySolver(llvm::SetVector<BoolValue *> Constraints);
private:
friend class Environment;
@@ -207,12 +209,12 @@ class DataflowAnalysisContext {
/// to track tokens of flow conditions that were already visited by recursive
/// calls.
void addTransitiveFlowConditionConstraints(
- Atom Token, llvm::SetVector<const Formula *> &Constraints,
- llvm::DenseSet<Atom> &VisitedTokens);
+ AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints,
+ llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
/// Returns true if the solver is able to prove that there is no satisfying
/// assignment for `Constraints`
- bool isUnsatisfiable(llvm::SetVector<const Formula *> Constraints) {
+ bool isUnsatisfiable(llvm::SetVector<BoolValue *> Constraints) {
return querySolver(std::move(Constraints)).getStatus() ==
Solver::Result::Status::Unsatisfiable;
}
@@ -251,8 +253,9 @@ class DataflowAnalysisContext {
// Flow conditions depend on other flow conditions if they are created using
// `forkFlowCondition` or `joinFlowConditions`. The graph of flow condition
// dependencies is stored in the `FlowConditionDeps` map.
- llvm::DenseMap<Atom, llvm::DenseSet<Atom>> FlowConditionDeps;
- llvm::DenseMap<Atom, const Formula *> FlowConditionConstraints;
+ llvm::DenseMap<AtomicBoolValue *, llvm::DenseSet<AtomicBoolValue *>>
+ FlowConditionDeps;
+ llvm::DenseMap<AtomicBoolValue *, BoolValue *> FlowConditionConstraints;
llvm::DenseMap<const FunctionDecl *, ControlFlowContext> FunctionContexts;
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
index b94485c99c9bad..faeb5eb69cd838 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -456,29 +456,29 @@ class Environment {
template <typename T, typename... Args>
std::enable_if_t<std::is_base_of<Value, T>::value, T &>
create(Args &&...args) {
- return arena().create<T>(std::forward<Args>(args)...);
+ return DACtx->arena().create<T>(std::forward<Args>(args)...);
}
/// Returns a symbolic integer value that models an integer literal equal to
/// `Value`
IntegerValue &getIntLiteralValue(llvm::APInt Value) const {
- return arena().makeIntLiteral(Value);
+ return DACtx->arena().makeIntLiteral(Value);
}
/// Returns a symbolic boolean value that models a boolean literal equal to
/// `Value`
- BoolValue &getBoolLiteralValue(bool Value) const {
- return arena().makeBoolValue(arena().makeLiteral(Value));
+ AtomicBoolValue &getBoolLiteralValue(bool Value) const {
+ return DACtx->arena().makeLiteral(Value);
}
/// Returns an atomic boolean value.
BoolValue &makeAtomicBoolValue() const {
- return arena().makeAtomValue();
+ return DACtx->arena().create<AtomicBoolValue>();
}
/// Returns a unique instance of boolean Top.
BoolValue &makeTopBoolValue() const {
- return arena().makeTopValue();
+ return DACtx->arena().create<TopBoolValue>();
}
/// Returns a boolean value that represents the conjunction of `LHS` and
@@ -486,8 +486,7 @@ class Environment {
/// order, will return the same result. If the given boolean values represent
/// the same value, the result will be the value itself.
BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS) const {
- return arena().makeBoolValue(
- arena().makeAnd(LHS.formula(), RHS.formula()));
+ return DACtx->arena().makeAnd(LHS, RHS);
}
/// Returns a boolean value that represents the disjunction of `LHS` and
@@ -495,14 +494,13 @@ class Environment {
/// order, will return the same result. If the given boolean values represent
/// the same value, the result will be the value itself.
BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS) const {
- return arena().makeBoolValue(
- arena().makeOr(LHS.formula(), RHS.formula()));
+ return DACtx->arena().makeOr(LHS, RHS);
}
/// Returns a boolean value that represents the negation of `Val`. Subsequent
/// calls with the same argument will return the same result.
BoolValue &makeNot(BoolValue &Val) const {
- return arena().makeBoolValue(arena().makeNot(Val.formula()));
+ return DACtx->arena().makeNot(Val);
}
/// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with
@@ -510,8 +508,7 @@ class Environment {
/// values represent the same value, the result will be a value that
/// represents the true boolean literal.
BoolValue &makeImplication(BoolValue &LHS, BoolValue &RHS) const {
- return arena().makeBoolValue(
- arena().makeImplies(LHS.formula(), RHS.formula()));
+ return DACtx->arena().makeImplies(LHS, RHS);
}
/// Returns a boolean value represents `LHS` <=> `RHS`. Subsequent calls with
@@ -519,22 +516,17 @@ class Environment {
/// result. If the given boolean values represent the same value, the result
/// will be a value that represents the true boolean literal.
BoolValue &makeIff(BoolValue &LHS, BoolValue &RHS) const {
- return arena().makeBoolValue(
- arena().makeEquals(LHS.formula(), RHS.formula()));
+ return DACtx->arena().makeEquals(LHS, RHS);
}
/// Returns the token that identifies the flow condition of the environment.
- Atom getFlowConditionToken() const { return FlowConditionToken; }
+ AtomicBoolValue &getFlowConditionToken() const { return *FlowConditionToken; }
/// Adds `Val` to the set of clauses that constitute the flow condition.
- void addToFlowCondition(const Formula &);
- LLVM_DEPRECATED("Use Formula version instead", "")
void addToFlowCondition(BoolValue &Val);
/// Returns true if and only if the clauses that constitute the flow condition
/// imply that `Val` is true.
- bool flowConditionImplies(const Formula &) const;
- LLVM_DEPRECATED("Use Formula version instead", "")
bool flowConditionImplies(BoolValue &Val) const;
/// Returns the `DeclContext` of the block being analysed, if any. Otherwise,
@@ -555,8 +547,6 @@ class Environment {
/// Returns the `DataflowAnalysisContext` used by the environment.
DataflowAnalysisContext &getDataflowAnalysisContext() const { return *DACtx; }
- Arena &arena() const { return DACtx->arena(); }
-
LLVM_DUMP_METHOD void dump() const;
LLVM_DUMP_METHOD void dump(raw_ostream &OS) const;
@@ -627,7 +617,7 @@ class Environment {
std::pair<StructValue *, const ValueDecl *>>
MemberLocToStruct;
- Atom FlowConditionToken;
+ AtomicBoolValue *FlowConditionToken;
};
/// Returns the storage location for the implicit object of a
diff --git a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
index 6b9f3681490af1..360786b02729f2 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
@@ -19,6 +19,7 @@
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/StringRef.h"
namespace clang {
@@ -27,9 +28,52 @@ 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
deleted file mode 100644
index 1d8cb6b3a8b1e6..00000000000000
--- a/clang/include/clang/Analysis/FlowSensitive/Formula.h
+++ /dev/null
@@ -1,144 +0,0 @@
-//===- 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,
- /// Constant true or false.
- Literal,
-
- 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);
- }
-
- bool literal() const {
- assert(kind() == Literal);
- return static_cast<bool>(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 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;
-
- static unsigned numOperands(Kind K) {
- switch (K) {
- case AtomRef:
- case Literal:
- 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 079f6802f241ee..10964eab8c34cc 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Solver.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Solver.h
@@ -14,10 +14,12 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
-#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Analysis/FlowSensitive/Value.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>
@@ -47,7 +49,8 @@ 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<Atom, Assignment> Solution) {
+ static Result
+ Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) {
return Result(Status::Satisfiable, std::move(Solution));
}
@@ -65,17 +68,19 @@ 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<Atom, Assignment>> getSolution() const {
+ std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>>
+ getSolution() const {
return Solution;
}
private:
- Result(Status SATCheckStatus,
- std::optional<llvm::DenseMap<Atom, Assignment>> Solution)
+ Result(
+ enum Status SATCheckStatus,
+ std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
: SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {}
Status SATCheckStatus;
- std::optional<llvm::DenseMap<Atom, Assignment>> Solution;
+ std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution;
};
virtual ~Solver() = default;
@@ -86,11 +91,13 @@ class Solver {
/// Requirements:
///
/// All elements in `Vals` must not be null.
- virtual Result solve(llvm::ArrayRef<const Formula *> Vals) = 0;
-};
+ virtual Result solve(llvm::ArrayRef<BoolValue *> Vals) = 0;
-llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &);
-llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment);
+ LLVM_DEPRECATED("Pass ArrayRef for determinism", "")
+ virtual Result solve(llvm::DenseSet<BoolValue *> Vals) {
+ return solve(ArrayRef(std::vector<BoolValue *>(Vals.begin(), Vals.end())));
+ }
+};
} // namespace dataflow
} // namespace clang
diff --git a/clang/include/clang/Analysis/FlowSensitive/Value.h b/clang/include/clang/Analysis/FlowSensitive/Value.h
index 1d4f8008d19307..59d5fa6923aabd 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Value.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Value.h
@@ -15,11 +15,11 @@
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_VALUE_H
#include "clang/AST/Decl.h"
-#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/StringMap.h"
#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/raw_ostream.h"
#include <cassert>
#include <utility>
@@ -38,10 +38,14 @@ class Value {
Pointer,
Struct,
- // TODO: Top values should not be need to be type-specific.
+ // Synthetic boolean values are either atomic values or logical connectives.
TopBool,
AtomicBool,
- FormulaBool,
+ Conjunction,
+ Disjunction,
+ Negation,
+ Implication,
+ Biconditional,
};
explicit Value(Kind ValKind) : ValKind(ValKind) {}
@@ -91,68 +95,151 @@ bool areEquivalentValues(const Value &Val1, const Value &Val2);
/// Models a boolean.
class BoolValue : public Value {
- const Formula *F;
-
public:
- explicit BoolValue(Kind ValueKind, const Formula &F)
- : Value(ValueKind), F(&F) {}
+ explicit BoolValue(Kind ValueKind) : Value(ValueKind) {}
static bool classof(const Value *Val) {
return Val->getKind() == Kind::TopBool ||
Val->getKind() == Kind::AtomicBool ||
- Val->getKind() == Kind::FormulaBool;
+ Val->getKind() == Kind::Conjunction ||
+ Val->getKind() == Kind::Disjunction ||
+ Val->getKind() == Kind::Negation ||
+ Val->getKind() == Kind::Implication ||
+ Val->getKind() == Kind::Biconditional;
}
-
- const Formula &formula() const { return *F; }
};
-/// A TopBoolValue represents a boolean that is explicitly unconstrained.
-///
-/// This is equivalent to an AtomicBoolValue that does not appear anywhere
-/// else in a system of formula.
-/// Knowing the value is unconstrained is useful when e.g. reasoning about
-/// convergence.
+/// Models the trivially true formula, which is Top in the lattice of boolean
+/// formulas.
class TopBoolValue final : public BoolValue {
public:
- TopBoolValue(const Formula &F) : BoolValue(Kind::TopBool, F) {
- assert(F.kind() == Formula::AtomRef);
- }
+ TopBoolValue() : BoolValue(Kind::TopBool) {}
static bool classof(const Value *Val) {
return Val->getKind() == Kind::TopBool;
}
-
- Atom getAtom() const { return formula().getAtom(); }
};
/// Models an atomic boolean.
-///
-/// FIXME: Merge this class into FormulaBoolValue.
-/// When we want to specify atom identity, use Atom.
-class AtomicBoolValue final : public BoolValue {
+class AtomicBoolValue : public BoolValue {
public:
- explicit AtomicBoolValue(const Formula &F) : BoolValue(Kind::AtomicBool, F) {
- assert(F.kind() == Formula::AtomRef);
- }
+ explicit AtomicBoolValue() : BoolValue(Kind::AtomicBool) {}
static bool classof(const Value *Val) {
return Val->getKind() == Kind::AtomicBool;
}
+};
+
+/// Models a boolean conjunction.
+// FIXME: Consider representing binary and unary boolean operations similar
+// to how they are represented in the AST. This might become more pressing
+// when such operations need to be added for other data types.
+class ConjunctionValue : public BoolValue {
+public:
+ explicit ConjunctionValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
+ : BoolValue(Kind::Conjunction), LeftSubVal(LeftSubVal),
+ RightSubVal(RightSubVal) {}
+
+ static bool classof(const Value *Val) {
+ return Val->getKind() == Kind::Conjunction;
+ }
+
+ /// Returns the left sub-value of the conjunction.
+ BoolValue &getLeftSubValue() const { return LeftSubVal; }
+
+ /// Returns the right sub-value of the conjunction.
+ BoolValue &getRightSubValue() const { return RightSubVal; }
+
+private:
+ BoolValue &LeftSubVal;
+ BoolValue &RightSubVal;
+};
+
+/// Models a boolean disjunction.
+class DisjunctionValue : public BoolValue {
+public:
+ explicit DisjunctionValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
+ : BoolValue(Kind::Disjunction), LeftSubVal(LeftSubVal),
+ RightSubVal(RightSubVal) {}
+
+ static bool classof(const Value *Val) {
+ return Val->getKind() == Kind::Disjunction;
+ }
+
+ /// Returns the left sub-value of the disjunction.
+ BoolValue &getLeftSubValue() const { return LeftSubVal; }
+
+ /// Returns the right sub-value of the disjunction.
+ BoolValue &getRightSubValue() const { return RightSubVal; }
+
+private:
+ BoolValue &LeftSubVal;
+ BoolValue &RightSubVal;
+};
+
+/// Models a boolean negation.
+class NegationValue : public BoolValue {
+public:
+ explicit NegationValue(BoolValue &SubVal)
+ : BoolValue(Kind::Negation), SubVal(SubVal) {}
+
+ static bool classof(const Value *Val) {
+ return Val->getKind() == Kind::Negation;
+ }
+
+ /// Returns the sub-value of the negation.
+ BoolValue &getSubVal() const { return SubVal; }
- Atom getAtom() const { return formula().getAtom(); }
+private:
+ BoolValue &SubVal;
};
-/// Models a compound boolean formula.
-class FormulaBoolValue final : public BoolValue {
+/// Models a boolean implication.
+///
+/// Equivalent to `!LHS v RHS`.
+class ImplicationValue : public BoolValue {
public:
- explicit FormulaBoolValue(const Formula &F)
- : BoolValue(Kind::FormulaBool, F) {
- assert(F.kind() != Formula::AtomRef && "For now, use AtomicBoolValue");
+ explicit ImplicationValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
+ : BoolValue(Kind::Implication), LeftSubVal(LeftSubVal),
+ RightSubVal(RightSubVal) {}
+
+ static bool classof(const Value *Val) {
+ return Val->getKind() == Kind::Implication;
}
+ /// Returns the left sub-value of the implication.
+ BoolValue &getLeftSubValue() const { return LeftSubVal; }
+
+ /// Returns the right sub-value of the implication.
+ BoolValue &getRightSubValue() const { return RightSubVal; }
+
+private:
+ BoolValue &LeftSubVal;
+ BoolValue &RightSubVal;
+};
+
+/// Models a boolean biconditional.
+///
+/// Equivalent to `(LHS ^ RHS) v (!LHS ^ !RHS)`.
+class BiconditionalValue : public BoolValue {
+public:
+ explicit BiconditionalValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
+ : BoolValue(Kind::Biconditional), LeftSubVal(LeftSubVal),
+ RightSubVal(RightSubVal) {}
+
static bool classof(const Value *Val) {
- return Val->getKind() == Kind::FormulaBool;
+ return Val->getKind() == Kind::Biconditional;
}
+
+ /// Returns the left sub-value of the biconditional.
+ BoolValue &getLeftSubValue() const { return LeftSubVal; }
+
+ /// Returns the right sub-value of the biconditional.
+ BoolValue &getRightSubValue() const { return RightSubVal; }
+
+private:
+ BoolValue &LeftSubVal;
+ BoolValue &RightSubVal;
};
/// Models an integer.
diff --git a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
index a0cdce93c9d470..b69cc01542c550 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<const Formula *> Vals) override;
+ Result solve(llvm::ArrayRef<BoolValue *> Vals) override;
};
} // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp
index a61887a3500522..cff6c45e185422 100644
--- a/clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -7,95 +7,65 @@
//===----------------------------------------------------------------------===//
#include "clang/Analysis/FlowSensitive/Arena.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
namespace clang::dataflow {
-static std::pair<const Formula *, const Formula *>
-canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
+static std::pair<BoolValue *, BoolValue *>
+makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
auto Res = std::make_pair(&LHS, &RHS);
- if (&RHS < &LHS) // FIXME: use a deterministic order instead
+ if (&RHS < &LHS)
std::swap(Res.first, Res.second);
return Res;
}
-template <class Key, class ComputeFunc>
-const Formula &cached(llvm::DenseMap<Key, const Formula *> &Cache, Key K,
- ComputeFunc &&Compute) {
- auto [It, Inserted] = Cache.try_emplace(std::forward<Key>(K));
- if (Inserted)
- It->second = Compute();
- return *It->second;
-}
+BoolValue &Arena::makeAnd(BoolValue &LHS, BoolValue &RHS) {
+ if (&LHS == &RHS)
+ return LHS;
-const Formula &Arena::makeAtomRef(Atom A) {
- return cached(AtomRefs, A, [&] {
- return &Formula::create(Alloc, Formula::AtomRef, {},
- static_cast<unsigned>(A));
- });
+ auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+ nullptr);
+ if (Res.second)
+ Res.first->second = &create<ConjunctionValue>(LHS, RHS);
+ return *Res.first->second;
}
-const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
- return cached(Ands, canonicalFormulaPair(LHS, RHS), [&] {
- if (&LHS == &RHS)
- return &LHS;
- if (LHS.kind() == Formula::Literal)
- return LHS.literal() ? &RHS : &LHS;
- if (RHS.kind() == Formula::Literal)
- return RHS.literal() ? &LHS : &RHS;
+BoolValue &Arena::makeOr(BoolValue &LHS, BoolValue &RHS) {
+ if (&LHS == &RHS)
+ return LHS;
- return &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
- });
+ auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+ nullptr);
+ if (Res.second)
+ Res.first->second = &create<DisjunctionValue>(LHS, RHS);
+ return *Res.first->second;
}
-const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
- return cached(Ors, canonicalFormulaPair(LHS, RHS), [&] {
- if (&LHS == &RHS)
- return &LHS;
- if (LHS.kind() == Formula::Literal)
- return LHS.literal() ? &LHS : &RHS;
- if (RHS.kind() == Formula::Literal)
- return RHS.literal() ? &RHS : &LHS;
-
- return &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
- });
+BoolValue &Arena::makeNot(BoolValue &Val) {
+ auto Res = NegationVals.try_emplace(&Val, nullptr);
+ if (Res.second)
+ Res.first->second = &create<NegationValue>(Val);
+ return *Res.first->second;
}
-const Formula &Arena::makeNot(const Formula &Val) {
- return cached(Nots, &Val, [&] {
- if (Val.kind() == Formula::Not)
- return Val.operands()[0];
- if (Val.kind() == Formula::Literal)
- return &makeLiteral(!Val.literal());
+BoolValue &Arena::makeImplies(BoolValue &LHS, BoolValue &RHS) {
+ if (&LHS == &RHS)
+ return makeLiteral(true);
- return &Formula::create(Alloc, Formula::Not, {&Val});
- });
+ auto Res = ImplicationVals.try_emplace(std::make_pair(&LHS, &RHS), nullptr);
+ if (Res.second)
+ Res.first->second = &create<ImplicationValue>(LHS, RHS);
+ return *Res.first->second;
}
-const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) {
- return cached(Implies, std::make_pair(&LHS, &RHS), [&] {
- if (&LHS == &RHS)
- return &makeLiteral(true);
- if (LHS.kind() == Formula::Literal)
- return LHS.literal() ? &RHS : &makeLiteral(true);
- if (RHS.kind() == Formula::Literal)
- return RHS.literal() ? &RHS : &makeNot(LHS);
+BoolValue &Arena::makeEquals(BoolValue &LHS, BoolValue &RHS) {
+ if (&LHS == &RHS)
+ return makeLiteral(true);
- return &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
- });
-}
-
-const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
- return cached(Equals, canonicalFormulaPair(LHS, RHS), [&] {
- if (&LHS == &RHS)
- return &makeLiteral(true);
- if (LHS.kind() == Formula::Literal)
- return LHS.literal() ? &RHS : &makeNot(RHS);
- if (RHS.kind() == Formula::Literal)
- return RHS.literal() ? &LHS : &makeNot(LHS);
-
- return &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
- });
+ auto Res = BiconditionalVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
+ nullptr);
+ if (Res.second)
+ Res.first->second = &create<BiconditionalValue>(LHS, RHS);
+ return *Res.first->second;
}
IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
@@ -106,13 +76,4 @@ IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
return *It->second;
}
-BoolValue &Arena::makeBoolValue(const Formula &F) {
- auto [It, Inserted] = FormulaValues.try_emplace(&F);
- if (Inserted)
- It->second = (F.kind() == Formula::AtomRef)
- ? (BoolValue *)&create<AtomicBoolValue>(F)
- : &create<FormulaBoolValue>(F);
- return *It->second;
-}
-
} // namespace clang::dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
index 171884afe8f4bf..d59bebf6a5a127 100644
--- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -3,7 +3,6 @@ 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 2971df6f11de2b..37bcc8be958792 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -15,7 +15,6 @@
#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"
@@ -24,12 +23,9 @@
#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,
@@ -102,107 +98,108 @@ DataflowAnalysisContext::getOrCreateNullPointerValue(QualType PointeeType) {
}
void DataflowAnalysisContext::addFlowConditionConstraint(
- Atom Token, const Formula &Constraint) {
- auto Res = FlowConditionConstraints.try_emplace(Token, &Constraint);
+ AtomicBoolValue &Token, BoolValue &Constraint) {
+ auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint);
if (!Res.second) {
Res.first->second =
&arena().makeAnd(*Res.first->second, Constraint);
}
}
-Atom DataflowAnalysisContext::forkFlowCondition(Atom Token) {
- Atom ForkToken = arena().makeFlowConditionToken();
- FlowConditionDeps[ForkToken].insert(Token);
- addFlowConditionConstraint(ForkToken, arena().makeAtomRef(Token));
+AtomicBoolValue &
+DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
+ auto &ForkToken = arena().makeFlowConditionToken();
+ FlowConditionDeps[&ForkToken].insert(&Token);
+ addFlowConditionConstraint(ForkToken, Token);
return ForkToken;
}
-Atom
-DataflowAnalysisContext::joinFlowConditions(Atom FirstToken,
- Atom SecondToken) {
- Atom Token = arena().makeFlowConditionToken();
- FlowConditionDeps[Token].insert(FirstToken);
- FlowConditionDeps[Token].insert(SecondToken);
- addFlowConditionConstraint(Token,
- arena().makeOr(arena().makeAtomRef(FirstToken),
- arena().makeAtomRef(SecondToken)));
+AtomicBoolValue &
+DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
+ AtomicBoolValue &SecondToken) {
+ auto &Token = arena().makeFlowConditionToken();
+ FlowConditionDeps[&Token].insert(&FirstToken);
+ FlowConditionDeps[&Token].insert(&SecondToken);
+ addFlowConditionConstraint(
+ Token, arena().makeOr(FirstToken, SecondToken));
return Token;
}
-Solver::Result DataflowAnalysisContext::querySolver(
- llvm::SetVector<const Formula *> Constraints) {
+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());
}
-bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
- const Formula &Val) {
+bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
+ BoolValue &Val) {
// Returns true if and only if truth assignment of the flow condition implies
// that `Val` is also true. We prove whether or not this property holds by
// reducing the problem to satisfiability checking. In other words, we attempt
// to show that assuming `Val` is false makes the constraints induced by the
// flow condition unsatisfiable.
- llvm::SetVector<const Formula *> Constraints;
- Constraints.insert(&arena().makeAtomRef(Token));
+ llvm::SetVector<BoolValue *> Constraints;
+ Constraints.insert(&Token);
Constraints.insert(&arena().makeNot(Val));
- llvm::DenseSet<Atom> VisitedTokens;
+ llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
return isUnsatisfiable(std::move(Constraints));
}
-bool DataflowAnalysisContext::flowConditionIsTautology(Atom Token) {
+bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
// Returns true if and only if we cannot prove that the flow condition can
// ever be false.
- llvm::SetVector<const Formula *> Constraints;
- Constraints.insert(&arena().makeNot(arena().makeAtomRef(Token)));
- llvm::DenseSet<Atom> VisitedTokens;
+ llvm::SetVector<BoolValue *> Constraints;
+ Constraints.insert(&arena().makeNot(Token));
+ llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
return isUnsatisfiable(std::move(Constraints));
}
-bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1,
- const Formula &Val2) {
- llvm::SetVector<const Formula *> Constraints;
+bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
+ BoolValue &Val2) {
+ llvm::SetVector<BoolValue*> Constraints;
Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2)));
return isUnsatisfiable(std::move(Constraints));
}
void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
- Atom Token, llvm::SetVector<const Formula *> &Constraints,
- llvm::DenseSet<Atom> &VisitedTokens) {
- auto Res = VisitedTokens.insert(Token);
+ AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints,
+ llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
+ auto Res = VisitedTokens.insert(&Token);
if (!Res.second)
return;
- auto ConstraintsIt = FlowConditionConstraints.find(Token);
+ auto ConstraintsIt = FlowConditionConstraints.find(&Token);
if (ConstraintsIt == FlowConditionConstraints.end()) {
- Constraints.insert(&arena().makeAtomRef(Token));
+ Constraints.insert(&Token);
} else {
// Bind flow condition token via `iff` to its set of constraints:
// FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
- Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token),
- *ConstraintsIt->second));
+ Constraints.insert(&arena().makeEquals(Token, *ConstraintsIt->second));
}
- auto DepsIt = FlowConditionDeps.find(Token);
+ auto DepsIt = FlowConditionDeps.find(&Token);
if (DepsIt != FlowConditionDeps.end()) {
- for (Atom DepToken : DepsIt->second) {
- addTransitiveFlowConditionConstraints(DepToken, Constraints,
+ for (AtomicBoolValue *DepToken : DepsIt->second) {
+ addTransitiveFlowConditionConstraints(*DepToken, Constraints,
VisitedTokens);
}
}
}
-void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
+void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
llvm::raw_ostream &OS) {
- llvm::SetVector<const Formula *> Constraints;
- Constraints.insert(&arena().makeAtomRef(Token));
- llvm::DenseSet<Atom> VisitedTokens;
+ llvm::SetVector<BoolValue *> Constraints;
+ Constraints.insert(&Token);
+ llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
- for (const auto *Constraint : Constraints) {
- Constraint->print(OS);
- OS << "\n";
- }
+ llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {
+ {&arena().makeLiteral(false), "False"},
+ {&arena().makeLiteral(true), "True"}};
+ OS << debugString(Constraints.getArrayRef(), AtomNames);
}
const ControlFlowContext *
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
index 11bb7da97d52f4..4a11c09a44f63b 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -107,16 +107,15 @@ static Value *mergeDistinctValues(QualType Type, Value &Val1,
// if (o.has_value())
// x = o.value();
// ```
- auto &Expr1 = cast<BoolValue>(Val1).formula();
- auto &Expr2 = cast<BoolValue>(Val2).formula();
- auto &A = MergedEnv.arena();
- auto &MergedVal = A.makeAtomRef(A.makeAtom());
- MergedEnv.addToFlowCondition(
- A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()),
- A.makeEquals(MergedVal, Expr1)),
- A.makeAnd(A.makeAtomRef(Env2.getFlowConditionToken()),
- A.makeEquals(MergedVal, Expr2))));
- return &A.makeBoolValue(MergedVal);
+ auto *Expr1 = cast<BoolValue>(&Val1);
+ auto *Expr2 = cast<BoolValue>(&Val2);
+ auto &MergedVal = MergedEnv.makeAtomicBoolValue();
+ MergedEnv.addToFlowCondition(MergedEnv.makeOr(
+ MergedEnv.makeAnd(Env1.getFlowConditionToken(),
+ MergedEnv.makeIff(MergedVal, *Expr1)),
+ MergedEnv.makeAnd(Env2.getFlowConditionToken(),
+ MergedEnv.makeIff(MergedVal, *Expr2))));
+ return &MergedVal;
}
// FIXME: Consider destroying `MergedValue` immediately if `ValueModel::merge`
@@ -270,11 +269,11 @@ void Environment::initFieldsGlobalsAndFuncs(const FunctionDecl *FuncDecl) {
Environment::Environment(DataflowAnalysisContext &DACtx)
: DACtx(&DACtx),
- FlowConditionToken(DACtx.arena().makeFlowConditionToken()) {}
+ FlowConditionToken(&DACtx.arena().makeFlowConditionToken()) {}
Environment Environment::fork() const {
Environment Copy(*this);
- Copy.FlowConditionToken = DACtx->forkFlowCondition(FlowConditionToken);
+ Copy.FlowConditionToken = &DACtx->forkFlowCondition(*FlowConditionToken);
return Copy;
}
@@ -588,8 +587,8 @@ Environment Environment::join(const Environment &EnvA, const Environment &EnvB,
// FIXME: update join to detect backedges and simplify the flow condition
// accordingly.
- JoinedEnv.FlowConditionToken = EnvA.DACtx->joinFlowConditions(
- EnvA.FlowConditionToken, EnvB.FlowConditionToken);
+ JoinedEnv.FlowConditionToken = &EnvA.DACtx->joinFlowConditions(
+ *EnvA.FlowConditionToken, *EnvB.FlowConditionToken);
for (auto &Entry : EnvA.LocToVal) {
const StorageLocation *Loc = Entry.first;
@@ -820,7 +819,7 @@ Value *Environment::createValueUnlessSelfReferential(
// with integers, and so distinguishing them serves no purpose, but could
// prevent convergence.
CreatedValuesCount++;
- return &arena().create<IntegerValue>();
+ return &DACtx->arena().create<IntegerValue>();
}
if (Type->isReferenceType() || Type->isPointerType()) {
@@ -838,9 +837,9 @@ Value *Environment::createValueUnlessSelfReferential(
}
if (Type->isReferenceType())
- return &arena().create<ReferenceValue>(PointeeLoc);
+ return &DACtx->arena().create<ReferenceValue>(PointeeLoc);
else
- return &arena().create<PointerValue>(PointeeLoc);
+ return &DACtx->arena().create<PointerValue>(PointeeLoc);
}
if (Type->isRecordType()) {
@@ -860,7 +859,7 @@ Value *Environment::createValueUnlessSelfReferential(
Visited.erase(FieldType.getCanonicalType());
}
- return &arena().create<StructValue>(std::move(FieldValues));
+ return &DACtx->arena().create<StructValue>(std::move(FieldValues));
}
return nullptr;
@@ -885,18 +884,12 @@ const StorageLocation &Environment::skip(const StorageLocation &Loc,
return skip(*const_cast<StorageLocation *>(&Loc), SP);
}
-void Environment::addToFlowCondition(const Formula &Val) {
- DACtx->addFlowConditionConstraint(FlowConditionToken, Val);
-}
void Environment::addToFlowCondition(BoolValue &Val) {
- addToFlowCondition(Val.formula());
+ DACtx->addFlowConditionConstraint(*FlowConditionToken, Val);
}
-bool Environment::flowConditionImplies(const Formula &Val) const {
- return DACtx->flowConditionImplies(FlowConditionToken, Val);
-}
bool Environment::flowConditionImplies(BoolValue &Val) const {
- return flowConditionImplies(Val.formula());
+ return DACtx->flowConditionImplies(*FlowConditionToken, Val);
}
void Environment::dump(raw_ostream &OS) const {
@@ -916,7 +909,7 @@ void Environment::dump(raw_ostream &OS) const {
}
OS << "FlowConditionToken:\n";
- DACtx->dumpFlowCondition(FlowConditionToken, OS);
+ DACtx->dumpFlowCondition(*FlowConditionToken, OS);
}
void Environment::dump() const {
diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
index f8a049adea5e5d..25225ed6266fb8 100644
--- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -16,12 +16,22 @@
#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:
@@ -36,19 +46,26 @@ llvm::StringRef debugString(Value::Kind Kind) {
return "AtomicBool";
case Value::Kind::TopBool:
return "TopBool";
- case Value::Kind::FormulaBool:
- return "FormulaBool";
+ case Value::Kind::Conjunction:
+ return "Conjunction";
+ case Value::Kind::Disjunction:
+ return "Disjunction";
+ case Value::Kind::Negation:
+ return "Negation";
+ case Value::Kind::Implication:
+ return "Implication";
+ case Value::Kind::Biconditional:
+ return "Biconditional";
}
llvm_unreachable("Unhandled value kind");
}
-llvm::raw_ostream &operator<<(llvm::raw_ostream &OS,
- Solver::Result::Assignment Assignment) {
+llvm::StringRef debugString(Solver::Result::Assignment Assignment) {
switch (Assignment) {
case Solver::Result::Assignment::AssignedFalse:
- return OS << "False";
+ return "False";
case Solver::Result::Assignment::AssignedTrue:
- return OS << "True";
+ return "True";
}
llvm_unreachable("Booleans can only be assigned true/false");
}
@@ -65,16 +82,174 @@ llvm::StringRef debugString(Solver::Result::Status Status) {
llvm_unreachable("Unhandled SAT check result status");
}
-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";
+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()));
}
- return OS;
+
+ /// 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);
}
} // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp
deleted file mode 100644
index 12f4e25097d7d8..00000000000000
--- a/clang/lib/Analysis/FlowSensitive/Formula.cpp
+++ /dev/null
@@ -1,93 +0,0 @@
-//===- 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 {
-
-const 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:
- case Formula::Literal:
- 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:
- switch (kind()) {
- case AtomRef:
- OS << getAtom();
- break;
- case Literal:
- OS << (literal() ? "true" : "false");
- break;
- default:
- llvm_unreachable("unhandled formula kind");
- }
- 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/HTMLLogger.cpp b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
index 0c4e838e667be1..14293a3043f988 100644
--- a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
+++ b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
@@ -97,7 +97,6 @@ class ModelDumper {
case Value::Kind::Integer:
case Value::Kind::TopBool:
case Value::Kind::AtomicBool:
- case Value::Kind::FormulaBool:
break;
case Value::Kind::Reference:
JOS.attributeObject(
@@ -112,6 +111,35 @@ class ModelDumper {
JOS.attributeObject("f:" + Child.first->getNameAsString(),
[&] { dump(*Child.second); });
break;
+ case Value::Kind::Disjunction: {
+ auto &VV = cast<DisjunctionValue>(V);
+ JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
+ JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
+ break;
+ }
+ case Value::Kind::Conjunction: {
+ auto &VV = cast<ConjunctionValue>(V);
+ JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
+ JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
+ break;
+ }
+ case Value::Kind::Negation: {
+ auto &VV = cast<NegationValue>(V);
+ JOS.attributeObject("not", [&] { dump(VV.getSubVal()); });
+ break;
+ }
+ case Value::Kind::Implication: {
+ auto &VV = cast<ImplicationValue>(V);
+ JOS.attributeObject("if", [&] { dump(VV.getLeftSubValue()); });
+ JOS.attributeObject("then", [&] { dump(VV.getRightSubValue()); });
+ break;
+ }
+ case Value::Kind::Biconditional: {
+ auto &VV = cast<BiconditionalValue>(V);
+ JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); });
+ JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); });
+ break;
+ }
}
for (const auto& Prop : V.properties())
@@ -121,12 +149,10 @@ class ModelDumper {
// Running the SAT solver is expensive, but knowing which booleans are
// guaranteed true/false here is valuable and hard to determine by hand.
if (auto *B = llvm::dyn_cast<BoolValue>(&V)) {
- JOS.attribute("formula", llvm::to_string(B->formula()));
- JOS.attribute(
- "truth", Env.flowConditionImplies(B->formula()) ? "true"
- : Env.flowConditionImplies(Env.arena().makeNot(B->formula()))
- ? "false"
- : "unknown");
+ JOS.attribute("truth", Env.flowConditionImplies(*B) ? "true"
+ : Env.flowConditionImplies(Env.makeNot(*B))
+ ? "false"
+ : "unknown");
}
}
void dump(const StorageLocation &L) {
diff --git a/clang/lib/Analysis/FlowSensitive/Transfer.cpp b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
index b9a2672d2e1d0f..5ad176dc1cdbe9 100644
--- a/clang/lib/Analysis/FlowSensitive/Transfer.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
@@ -62,12 +62,64 @@ static BoolValue &evaluateBooleanEquality(const Expr &LHS, const Expr &RHS,
return Env.makeAtomicBoolValue();
}
+// Functionally updates `V` such that any instances of `TopBool` are replaced
+// with fresh atomic bools. Note: This implementation assumes that `B` is a
+// tree; if `B` is a DAG, it will lose any sharing between subvalues that was
+// present in the original .
+static BoolValue &unpackValue(BoolValue &V, Environment &Env);
+
+template <typename Derived, typename M>
+BoolValue &unpackBinaryBoolValue(Environment &Env, BoolValue &B, M build) {
+ auto &V = *cast<Derived>(&B);
+ BoolValue &Left = V.getLeftSubValue();
+ BoolValue &Right = V.getRightSubValue();
+ BoolValue &ULeft = unpackValue(Left, Env);
+ BoolValue &URight = unpackValue(Right, Env);
+
+ if (&ULeft == &Left && &URight == &Right)
+ return V;
+
+ return (Env.*build)(ULeft, URight);
+}
+
static BoolValue &unpackValue(BoolValue &V, Environment &Env) {
- if (auto *Top = llvm::dyn_cast<TopBoolValue>(&V)) {
- auto &A = Env.getDataflowAnalysisContext().arena();
- return A.makeBoolValue(A.makeAtomRef(Top->getAtom()));
+ switch (V.getKind()) {
+ case Value::Kind::Integer:
+ case Value::Kind::Reference:
+ case Value::Kind::Pointer:
+ case Value::Kind::Struct:
+ llvm_unreachable("BoolValue cannot have any of these kinds.");
+
+ case Value::Kind::AtomicBool:
+ return V;
+
+ case Value::Kind::TopBool:
+ // Unpack `TopBool` into a fresh atomic bool.
+ return Env.makeAtomicBoolValue();
+
+ case Value::Kind::Negation: {
+ auto &N = *cast<NegationValue>(&V);
+ BoolValue &Sub = N.getSubVal();
+ BoolValue &USub = unpackValue(Sub, Env);
+
+ if (&USub == &Sub)
+ return V;
+ return Env.makeNot(USub);
+ }
+ case Value::Kind::Conjunction:
+ return unpackBinaryBoolValue<ConjunctionValue>(Env, V,
+ &Environment::makeAnd);
+ case Value::Kind::Disjunction:
+ return unpackBinaryBoolValue<DisjunctionValue>(Env, V,
+ &Environment::makeOr);
+ case Value::Kind::Implication:
+ return unpackBinaryBoolValue<ImplicationValue>(
+ Env, V, &Environment::makeImplication);
+ case Value::Kind::Biconditional:
+ return unpackBinaryBoolValue<BiconditionalValue>(Env, V,
+ &Environment::makeIff);
}
- return V;
+ llvm_unreachable("All reachable cases in switch return");
}
// Unpacks the value (if any) associated with `E` and updates `E` to the new
diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
index bf48a1fbda5940..db2e1d694457bf 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 CNFFormula {
+struct BooleanFormula {
/// `LargestVar` is equal to the largest positive integer that represents a
/// variable in the formula.
const Variable LargestVar;
@@ -121,12 +121,12 @@ struct CNFFormula {
/// clauses in the formula start from the element at index 1.
std::vector<ClauseID> NextWatched;
- /// Stores the variable identifier and Atom for atomic booleans in the
- /// formula.
- llvm::DenseMap<Variable, Atom> Atomics;
+ /// Stores the variable identifier and value location for atomic booleans in
+ /// the formula.
+ llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
- explicit CNFFormula(Variable LargestVar,
- llvm::DenseMap<Variable, Atom> Atomics)
+ explicit BooleanFormula(Variable LargestVar,
+ llvm::DenseMap<Variable, AtomicBoolValue *> Atomics)
: LargestVar(LargestVar), Atomics(std::move(Atomics)) {
Clauses.push_back(0);
ClauseStarts.push_back(0);
@@ -144,8 +144,8 @@ struct CNFFormula {
///
/// 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 Formula
- // and the construction in `buildCNF`.
+ // The literals are guaranteed to be distinct from properties of BoolValue
+ // and the construction in `buildBooleanFormula`.
assert(L1 != NullLit && L1 != L2 && L1 != L3 &&
(L2 != L3 || L2 == NullLit));
@@ -178,59 +178,98 @@ struct CNFFormula {
/// Converts the conjunction of `Vals` into a formula in conjunctive normal
/// form where each clause has at least one and at most three literals.
-CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
+BooleanFormula buildBooleanFormula(const llvm::ArrayRef<BoolValue *> &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-formulas in `Vals`.
+ // of sub-values in `Vals`.
- // 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;
+ // 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;
Variable NextVar = 1;
{
- std::queue<const Formula *> UnprocessedSubVals;
- for (const Formula *Val : Vals)
+ std::queue<BoolValue *> UnprocessedSubVals;
+ for (BoolValue *Val : Vals)
UnprocessedSubVals.push(Val);
while (!UnprocessedSubVals.empty()) {
Variable Var = NextVar;
- const Formula *Val = UnprocessedSubVals.front();
+ BoolValue *Val = UnprocessedSubVals.front();
UnprocessedSubVals.pop();
if (!SubValsToVar.try_emplace(Val, Var).second)
continue;
++NextVar;
- for (const Formula *F : Val->operands())
- UnprocessedSubVals.push(F);
- if (Val->kind() == Formula::AtomRef)
- Atomics[Var] = Val->getAtom();
+ // 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");
+ }
}
}
- auto GetVar = [&SubValsToVar](const Formula *Val) {
+ auto GetVar = [&SubValsToVar](const BoolValue *Val) {
auto ValIt = SubValsToVar.find(Val);
assert(ValIt != SubValsToVar.end());
return ValIt->second;
};
- CNFFormula CNF(NextVar - 1, std::move(Atomics));
+ BooleanFormula Formula(NextVar - 1, std::move(Atomics));
std::vector<bool> ProcessedSubVals(NextVar, false);
- // 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 a conjunct for each variable that represents a top-level conjunction
+ // value in `Vals`.
+ for (BoolValue *Val : Vals)
+ Formula.addClause(posLit(GetVar(Val)));
// Add conjuncts that represent the mapping between newly-created variables
- // and their corresponding sub-formulas.
- std::queue<const Formula *> UnprocessedSubVals;
- for (const Formula *Val : Vals)
+ // and their corresponding sub-values.
+ std::queue<BoolValue *> UnprocessedSubVals;
+ for (BoolValue *Val : Vals)
UnprocessedSubVals.push(Val);
while (!UnprocessedSubVals.empty()) {
- const Formula *Val = UnprocessedSubVals.front();
+ const BoolValue *Val = UnprocessedSubVals.front();
UnprocessedSubVals.pop();
const Variable Var = GetVar(Val);
@@ -238,110 +277,117 @@ CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
continue;
ProcessedSubVals[Var] = true;
- switch (Val->kind()) {
- case Formula::AtomRef:
- break;
- case Formula::Literal:
- CNF.addClause(Val->literal() ? posLit(Var) : negLit(Var));
- break;
- case Formula::And: {
- const Variable LHS = GetVar(Val->operands()[0]);
- const Variable RHS = GetVar(Val->operands()[1]);
-
- if (LHS == RHS) {
+ if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
+ const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
+ const Variable RightSubVar = GetVar(&C->getRightSubValue());
+
+ if (LeftSubVar == RightSubVar) {
// `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.
- CNF.addClause(negLit(Var), posLit(LHS));
- CNF.addClause(posLit(Var), negLit(LHS));
+ 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());
} 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.
- CNF.addClause(negLit(Var), posLit(LHS));
- CNF.addClause(negLit(Var), posLit(RHS));
- CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
+ 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());
}
- break;
- }
- case Formula::Or: {
- const Variable LHS = GetVar(Val->operands()[0]);
- const Variable RHS = GetVar(Val->operands()[1]);
+ } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
+ const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
+ const Variable RightSubVar = GetVar(&D->getRightSubValue());
- if (LHS == RHS) {
+ if (LeftSubVar == RightSubVar) {
// `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.
- CNF.addClause(negLit(Var), posLit(LHS));
- CNF.addClause(posLit(Var), negLit(LHS));
+ 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());
} 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.
- CNF.addClause(negLit(Var), posLit(LHS), posLit(RHS));
- CNF.addClause(posLit(Var), negLit(LHS));
- CNF.addClause(posLit(Var), negLit(RHS));
+ // `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());
}
- 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]);
+ } 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());
// `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.
- 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) {
+ // 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) {
// `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.
- CNF.addClause(posLit(Var));
+ Formula.addClause(posLit(Var));
// No need to visit the sub-values of `Val`.
- continue;
+ } 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());
}
- // `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 CNF;
+ return Formula;
}
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.
- CNFFormula CNF;
+ BooleanFormula Formula;
/// The search for a satisfying assignment of the variables in `Formula` will
/// proceed in levels, starting from 1 and going up to `Formula.LargestVar`
@@ -393,10 +439,9 @@ class WatchedLiteralsSolverImpl {
std::vector<Variable> ActiveVars;
public:
- explicit WatchedLiteralsSolverImpl(
- const llvm::ArrayRef<const Formula *> &Vals)
- : CNF(buildCNF(Vals)), LevelVars(CNF.LargestVar + 1),
- LevelStates(CNF.LargestVar + 1) {
+ explicit WatchedLiteralsSolverImpl(const llvm::ArrayRef<BoolValue *> &Vals)
+ : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),
+ LevelStates(Formula.LargestVar + 1) {
assert(!Vals.empty());
// Initialize the state at the root level to a decision so that in
@@ -405,10 +450,10 @@ class WatchedLiteralsSolverImpl {
LevelStates[0] = State::Decision;
// Initialize all variables as unassigned.
- VarAssignments.resize(CNF.LargestVar + 1, Assignment::Unassigned);
+ VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned);
// Initialize the active variables.
- for (Variable Var = CNF.LargestVar; Var != NullVar; --Var) {
+ for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {
if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
ActiveVars.push_back(Var);
}
@@ -429,7 +474,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 `buildCNF`.
+ // transformations performed by `buildBooleanFormula`.
assert(activeVarsAreUnassigned());
assert(activeVarsFormWatchedLiterals());
assert(unassignedVarsFormingWatchedLiteralsAreActive());
@@ -510,10 +555,12 @@ class WatchedLiteralsSolverImpl {
}
private:
- /// 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) {
+ /// 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) {
// 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.
@@ -549,24 +596,24 @@ class WatchedLiteralsSolverImpl {
const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
? negLit(Var)
: posLit(Var);
- ClauseID FalseLitWatcher = CNF.WatchedHead[FalseLit];
- CNF.WatchedHead[FalseLit] = NullClause;
+ ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit];
+ Formula.WatchedHead[FalseLit] = NullClause;
while (FalseLitWatcher != NullClause) {
- const ClauseID NextFalseLitWatcher = CNF.NextWatched[FalseLitWatcher];
+ const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher];
// Pick the first non-false literal as the new watched literal.
- const size_t FalseLitWatcherStart = CNF.ClauseStarts[FalseLitWatcher];
+ const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher];
size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
- while (isCurrentlyFalse(CNF.Clauses[NewWatchedLitIdx]))
+ while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx]))
++NewWatchedLitIdx;
- const Literal NewWatchedLit = CNF.Clauses[NewWatchedLitIdx];
+ const Literal NewWatchedLit = Formula.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.
- CNF.Clauses[NewWatchedLitIdx] = FalseLit;
- CNF.Clauses[FalseLitWatcherStart] = NewWatchedLit;
+ Formula.Clauses[NewWatchedLitIdx] = FalseLit;
+ Formula.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.
@@ -574,8 +621,8 @@ class WatchedLiteralsSolverImpl {
VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
ActiveVars.push_back(NewWatchedLitVar);
- CNF.NextWatched[FalseLitWatcher] = CNF.WatchedHead[NewWatchedLit];
- CNF.WatchedHead[NewWatchedLit] = FalseLitWatcher;
+ Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit];
+ Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher;
// Go to the next clause that watches `FalseLit`.
FalseLitWatcher = NextFalseLitWatcher;
@@ -585,15 +632,16 @@ 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 = CNF.WatchedHead[Lit]; LitWatcher != NullClause;
- LitWatcher = CNF.NextWatched[LitWatcher]) {
- llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);
+ for (ClauseID LitWatcher = Formula.WatchedHead[Lit];
+ LitWatcher != NullClause;
+ LitWatcher = Formula.NextWatched[LitWatcher]) {
+ llvm::ArrayRef<Literal> Clause = Formula.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 `buildCNF`.
+ // due to the transformations performed by `buildBooleanFormula`.
assert(Clause.front() == Lit);
if (isUnit(Clause))
@@ -617,7 +665,7 @@ class WatchedLiteralsSolverImpl {
/// Returns true if and only if `Lit` is watched by a clause in `Formula`.
bool isWatched(Literal Lit) const {
- return CNF.WatchedHead[Lit] != NullClause;
+ return Formula.WatchedHead[Lit] != NullClause;
}
/// Returns an assignment for an unassigned variable.
@@ -630,8 +678,8 @@ class WatchedLiteralsSolverImpl {
/// Returns a set of all watched literals.
llvm::DenseSet<Literal> watchedLiterals() const {
llvm::DenseSet<Literal> WatchedLiterals;
- for (Literal Lit = 2; Lit < CNF.WatchedHead.size(); Lit++) {
- if (CNF.WatchedHead[Lit] == NullClause)
+ for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {
+ if (Formula.WatchedHead[Lit] == NullClause)
continue;
WatchedLiterals.insert(Lit);
}
@@ -671,8 +719,7 @@ class WatchedLiteralsSolverImpl {
}
};
-Solver::Result
-WatchedLiteralsSolver::solve(llvm::ArrayRef<const Formula *> Vals) {
+Solver::Result WatchedLiteralsSolver::solve(llvm::ArrayRef<BoolValue *> 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 98c9cc44273cff..407abf58529a50 100644
--- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
@@ -7,7 +7,6 @@
//===----------------------------------------------------------------------===//
#include "clang/Analysis/FlowSensitive/Arena.h"
-#include "llvm/Support/ScopedPrinter.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -20,20 +19,26 @@ class ArenaTest : public ::testing::Test {
};
TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) {
- auto &X = A.makeAtomValue();
- auto &Y = A.makeAtomValue();
+ auto &X = A.create<AtomicBoolValue>();
+ auto &Y = A.create<AtomicBoolValue>();
EXPECT_NE(&X, &Y);
}
TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) {
- auto &X = A.makeTopValue();
- auto &Y = A.makeTopValue();
+ auto &X = A.create<TopBoolValue>();
+ auto &Y = A.create<TopBoolValue>();
EXPECT_NE(&X, &Y);
}
+TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &XAndX = A.makeAnd(X, X);
+ EXPECT_EQ(&XAndX, &X);
+}
+
TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
- auto &X = A.makeAtomRef(A.makeAtom());
- auto &Y = A.makeAtomRef(A.makeAtom());
+ auto &X = A.create<AtomicBoolValue>();
+ auto &Y = A.create<AtomicBoolValue>();
auto &XAndY1 = A.makeAnd(X, Y);
auto &XAndY2 = A.makeAnd(X, Y);
EXPECT_EQ(&XAndY1, &XAndY2);
@@ -41,14 +46,20 @@ TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
auto &YAndX = A.makeAnd(Y, X);
EXPECT_EQ(&XAndY1, &YAndX);
- auto &Z = A.makeAtomRef(A.makeAtom());
+ auto &Z = A.create<AtomicBoolValue>();
auto &XAndZ = A.makeAnd(X, Z);
EXPECT_NE(&XAndY1, &XAndZ);
}
+TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &XOrX = A.makeOr(X, X);
+ EXPECT_EQ(&XOrX, &X);
+}
+
TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
- auto &X = A.makeAtomRef(A.makeAtom());
- auto &Y = A.makeAtomRef(A.makeAtom());
+ auto &X = A.create<AtomicBoolValue>();
+ auto &Y = A.create<AtomicBoolValue>();
auto &XOrY1 = A.makeOr(X, Y);
auto &XOrY2 = A.makeOr(X, Y);
EXPECT_EQ(&XOrY1, &XOrY2);
@@ -56,24 +67,31 @@ TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
auto &YOrX = A.makeOr(Y, X);
EXPECT_EQ(&XOrY1, &YOrX);
- auto &Z = A.makeAtomRef(A.makeAtom());
+ auto &Z = A.create<AtomicBoolValue>();
auto &XOrZ = A.makeOr(X, Z);
EXPECT_NE(&XOrY1, &XOrZ);
}
TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
- auto &X = A.makeAtomRef(A.makeAtom());
+ auto &X = A.create<AtomicBoolValue>();
auto &NotX1 = A.makeNot(X);
auto &NotX2 = A.makeNot(X);
EXPECT_EQ(&NotX1, &NotX2);
- auto &Y = A.makeAtomRef(A.makeAtom());
+
+ auto &Y = A.create<AtomicBoolValue>();
auto &NotY = A.makeNot(Y);
EXPECT_NE(&NotX1, &NotY);
}
+TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &XImpliesX = A.makeImplies(X, X);
+ EXPECT_EQ(&XImpliesX, &A.makeLiteral(true));
+}
+
TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
- auto &X = A.makeAtomRef(A.makeAtom());
- auto &Y = A.makeAtomRef(A.makeAtom());
+ auto &X = A.create<AtomicBoolValue>();
+ auto &Y = A.create<AtomicBoolValue>();
auto &XImpliesY1 = A.makeImplies(X, Y);
auto &XImpliesY2 = A.makeImplies(X, Y);
EXPECT_EQ(&XImpliesY1, &XImpliesY2);
@@ -81,14 +99,20 @@ TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
auto &YImpliesX = A.makeImplies(Y, X);
EXPECT_NE(&XImpliesY1, &YImpliesX);
- auto &Z = A.makeAtomRef(A.makeAtom());
+ auto &Z = A.create<AtomicBoolValue>();
auto &XImpliesZ = A.makeImplies(X, Z);
EXPECT_NE(&XImpliesY1, &XImpliesZ);
}
+TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &XIffX = A.makeEquals(X, X);
+ EXPECT_EQ(&XIffX, &A.makeLiteral(true));
+}
+
TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
- auto &X = A.makeAtomRef(A.makeAtom());
- auto &Y = A.makeAtomRef(A.makeAtom());
+ auto &X = A.create<AtomicBoolValue>();
+ auto &Y = A.create<AtomicBoolValue>();
auto &XIffY1 = A.makeEquals(X, Y);
auto &XIffY2 = A.makeEquals(X, Y);
EXPECT_EQ(&XIffY1, &XIffY2);
@@ -96,53 +120,10 @@ TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
auto &YIffX = A.makeEquals(Y, X);
EXPECT_EQ(&XIffY1, &YIffX);
- auto &Z = A.makeAtomRef(A.makeAtom());
+ auto &Z = A.create<AtomicBoolValue>();
auto &XIffZ = A.makeEquals(X, Z);
EXPECT_NE(&XIffY1, &XIffZ);
}
-TEST_F(ArenaTest, Interning) {
- Atom X = A.makeAtom();
- Atom Y = A.makeAtom();
- const Formula &F1 = A.makeAnd(A.makeAtomRef(X), A.makeAtomRef(Y));
- const Formula &F2 = A.makeAnd(A.makeAtomRef(Y), A.makeAtomRef(X));
- EXPECT_EQ(&F1, &F2);
- BoolValue &B1 = A.makeBoolValue(F1);
- BoolValue &B2 = A.makeBoolValue(F2);
- EXPECT_EQ(&B1, &B2);
- EXPECT_EQ(&B1.formula(), &F1);
-}
-
-TEST_F(ArenaTest, IdentitySimplification) {
- auto &X = A.makeAtomRef(A.makeAtom());
-
- EXPECT_EQ(&X, &A.makeAnd(X, X));
- EXPECT_EQ(&X, &A.makeOr(X, X));
- EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, X));
- EXPECT_EQ(&A.makeLiteral(true), &A.makeEquals(X, X));
- EXPECT_EQ(&X, &A.makeNot(A.makeNot(X)));
-}
-
-TEST_F(ArenaTest, LiteralSimplification) {
- auto &X = A.makeAtomRef(A.makeAtom());
-
- EXPECT_EQ(&X, &A.makeAnd(X, A.makeLiteral(true)));
- EXPECT_EQ(&A.makeLiteral(false), &A.makeAnd(X, A.makeLiteral(false)));
-
- EXPECT_EQ(&A.makeLiteral(true), &A.makeOr(X, A.makeLiteral(true)));
- EXPECT_EQ(&X, &A.makeOr(X, A.makeLiteral(false)));
-
- EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, A.makeLiteral(true)));
- EXPECT_EQ(&A.makeNot(X), &A.makeImplies(X, A.makeLiteral(false)));
- EXPECT_EQ(&X, &A.makeImplies(A.makeLiteral(true), X));
- EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(A.makeLiteral(false), X));
-
- EXPECT_EQ(&X, &A.makeEquals(X, A.makeLiteral(true)));
- EXPECT_EQ(&A.makeNot(X), &A.makeEquals(X, A.makeLiteral(false)));
-
- EXPECT_EQ(&A.makeLiteral(false), &A.makeNot(A.makeLiteral(true)));
- EXPECT_EQ(&A.makeLiteral(true), &A.makeNot(A.makeLiteral(false)));
-}
-
} // namespace
} // namespace clang::dataflow
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
index f6e8b30d898e89..bb76648abdc05c 100644
--- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -28,56 +28,56 @@ class DataflowAnalysisContextTest : public ::testing::Test {
};
TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) {
- auto &X = A.makeTopValue();
- auto &Y = A.makeTopValue();
- EXPECT_FALSE(Context.equivalentFormulas(X.formula(), Y.formula()));
+ auto &X = A.create<TopBoolValue>();
+ auto &Y = A.create<TopBoolValue>();
+ EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
}
TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) {
- Atom FC = A.makeFlowConditionToken();
- auto &C = A.makeAtomRef(A.makeAtom());
+ auto &FC = A.makeFlowConditionToken();
+ auto &C = A.create<AtomicBoolValue>();
EXPECT_FALSE(Context.flowConditionImplies(FC, C));
}
TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) {
- Atom FC = A.makeFlowConditionToken();
- auto &C = A.makeAtomRef(A.makeAtom());
+ auto &FC = A.makeFlowConditionToken();
+ auto &C = A.create<AtomicBoolValue>();
Context.addFlowConditionConstraint(FC, C);
EXPECT_TRUE(Context.flowConditionImplies(FC, C));
}
TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) {
- Atom FC1 = A.makeFlowConditionToken();
- auto &C1 = A.makeAtomRef(A.makeAtom());
+ auto &FC1 = A.makeFlowConditionToken();
+ auto &C1 = A.create<AtomicBoolValue>();
Context.addFlowConditionConstraint(FC1, C1);
// Forked flow condition inherits the constraints of its parent flow
// condition.
- Atom FC2 = Context.forkFlowCondition(FC1);
+ auto &FC2 = Context.forkFlowCondition(FC1);
EXPECT_TRUE(Context.flowConditionImplies(FC2, C1));
// Adding a new constraint to the forked flow condition does not affect its
// parent flow condition.
- auto &C2 = A.makeAtomRef(A.makeAtom());
+ auto &C2 = A.create<AtomicBoolValue>();
Context.addFlowConditionConstraint(FC2, C2);
EXPECT_TRUE(Context.flowConditionImplies(FC2, C2));
EXPECT_FALSE(Context.flowConditionImplies(FC1, C2));
}
TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
- auto &C1 = A.makeAtomRef(A.makeAtom());
- auto &C2 = A.makeAtomRef(A.makeAtom());
- auto &C3 = A.makeAtomRef(A.makeAtom());
+ auto &C1 = A.create<AtomicBoolValue>();
+ auto &C2 = A.create<AtomicBoolValue>();
+ auto &C3 = A.create<AtomicBoolValue>();
- Atom FC1 = A.makeFlowConditionToken();
+ auto &FC1 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC1, C1);
Context.addFlowConditionConstraint(FC1, C3);
- Atom FC2 = A.makeFlowConditionToken();
+ auto &FC2 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC2, C2);
Context.addFlowConditionConstraint(FC2, C3);
- Atom FC3 = Context.joinFlowConditions(FC1, FC2);
+ auto &FC3 = Context.joinFlowConditions(FC1, FC2);
EXPECT_FALSE(Context.flowConditionImplies(FC3, C1));
EXPECT_FALSE(Context.flowConditionImplies(FC3, C2));
EXPECT_TRUE(Context.flowConditionImplies(FC3, C3));
@@ -85,77 +85,77 @@ TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
// Fresh flow condition with empty/no constraints is always true.
- Atom FC1 = A.makeFlowConditionToken();
+ auto &FC1 = A.makeFlowConditionToken();
EXPECT_TRUE(Context.flowConditionIsTautology(FC1));
// Literal `true` is always true.
- Atom FC2 = A.makeFlowConditionToken();
+ auto &FC2 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC2, A.makeLiteral(true));
EXPECT_TRUE(Context.flowConditionIsTautology(FC2));
// Literal `false` is never true.
- Atom FC3 = A.makeFlowConditionToken();
+ auto &FC3 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC3, A.makeLiteral(false));
EXPECT_FALSE(Context.flowConditionIsTautology(FC3));
// We can't prove that an arbitrary bool A is always true...
- auto &C1 = A.makeAtomRef(A.makeAtom());
- Atom FC4 = A.makeFlowConditionToken();
+ auto &C1 = A.create<AtomicBoolValue>();
+ auto &FC4 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC4, C1);
EXPECT_FALSE(Context.flowConditionIsTautology(FC4));
// ... but we can prove A || !A is true.
- Atom FC5 = A.makeFlowConditionToken();
+ auto &FC5 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC5, A.makeOr(C1, A.makeNot(C1)));
EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
}
TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
- auto &X = A.makeAtomRef(A.makeAtom());
- auto &Y = A.makeAtomRef(A.makeAtom());
- auto &Z = A.makeAtomRef(A.makeAtom());
+ auto &X = A.create<AtomicBoolValue>();
+ auto &Y = A.create<AtomicBoolValue>();
+ auto &Z = A.create<AtomicBoolValue>();
auto &True = A.makeLiteral(true);
auto &False = A.makeLiteral(false);
// X == X
- EXPECT_TRUE(Context.equivalentFormulas(X, X));
+ EXPECT_TRUE(Context.equivalentBoolValues(X, X));
// X != Y
- EXPECT_FALSE(Context.equivalentFormulas(X, Y));
+ EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
// !X != X
- EXPECT_FALSE(Context.equivalentFormulas(A.makeNot(X), X));
+ EXPECT_FALSE(Context.equivalentBoolValues(A.makeNot(X), X));
// !(!X) = X
- EXPECT_TRUE(Context.equivalentFormulas(A.makeNot(A.makeNot(X)), X));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeNot(A.makeNot(X)), X));
// (X || X) == X
- EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, X), X));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, X), X));
// (X || Y) != X
- EXPECT_FALSE(Context.equivalentFormulas(A.makeOr(X, Y), X));
+ EXPECT_FALSE(Context.equivalentBoolValues(A.makeOr(X, Y), X));
// (X || True) == True
- EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, True), True));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, True), True));
// (X || False) == X
- EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, False), X));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, False), X));
// (X && X) == X
- EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, X), X));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, X), X));
// (X && Y) != X
- EXPECT_FALSE(Context.equivalentFormulas(A.makeAnd(X, Y), X));
+ EXPECT_FALSE(Context.equivalentBoolValues(A.makeAnd(X, Y), X));
// (X && True) == X
- EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, True), X));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, True), X));
// (X && False) == False
- EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, False), False));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, False), False));
// (X || Y) == (Y || X)
- EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, Y), A.makeOr(Y, X)));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, Y), A.makeOr(Y, X)));
// (X && Y) == (Y && X)
- EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, Y), A.makeAnd(Y, X)));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, Y), A.makeAnd(Y, X)));
// ((X || Y) || Z) == (X || (Y || Z))
- EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(A.makeOr(X, Y), Z),
- A.makeOr(X, A.makeOr(Y, Z))));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(A.makeOr(X, Y), Z),
+ A.makeOr(X, A.makeOr(Y, Z))));
// ((X && Y) && Z) == (X && (Y && Z))
- EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(A.makeAnd(X, Y), Z),
- A.makeAnd(X, A.makeAnd(Y, Z))));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(A.makeAnd(X, Y), Z),
+ A.makeAnd(X, A.makeAnd(Y, Z))));
}
} // namespace
diff --git a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
index cf266f4c3a832d..10fcd204c9ab07 100644
--- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -8,9 +8,8 @@
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "TestingSupport.h"
-#include "clang/Analysis/FlowSensitive/Formula.h"
-#include "llvm/Support/ScopedPrinter.h"
-#include "llvm/Support/raw_ostream.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -23,92 +22,429 @@ using test::ConstraintContext;
using testing::StrEq;
TEST(BoolValueDebugStringTest, AtomicBoolean) {
+ // B0
ConstraintContext Ctx;
auto B = Ctx.atom();
- auto Expected = "V0";
- EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+ auto Expected = R"(B0)";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
-TEST(BoolValueDebugStringTest, Literal) {
+TEST(BoolValueDebugStringTest, Top) {
ConstraintContext Ctx;
- EXPECT_EQ("true", llvm::to_string(*Ctx.literal(true)));
- EXPECT_EQ("false", llvm::to_string(*Ctx.literal(false)));
+ auto B = Ctx.top();
+
+ auto Expected = R"(top)";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Negation) {
+ // !B0
ConstraintContext Ctx;
auto B = Ctx.neg(Ctx.atom());
- auto Expected = "!V0";
- EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+ auto Expected = R"((not
+ B0))";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Conjunction) {
+ // B0 ^ B1
ConstraintContext Ctx;
- auto *V0 = Ctx.atom();
- auto *V1 = Ctx.atom();
- EXPECT_EQ("(V0 & V1)", llvm::to_string(*Ctx.conj(V0, V1)));
+ auto B = Ctx.conj(Ctx.atom(), Ctx.atom());
+
+ auto Expected = R"((and
+ B0
+ B1))";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Disjunction) {
+ // B0 v B1
ConstraintContext Ctx;
- auto *V0 = Ctx.atom();
- auto *V1 = Ctx.atom();
- EXPECT_EQ("(V0 | V1)", llvm::to_string(*Ctx.disj(V0, V1)));
+ auto B = Ctx.disj(Ctx.atom(), Ctx.atom());
+
+ auto Expected = R"((or
+ B0
+ B1))";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Implication) {
+ // B0 => B1
ConstraintContext Ctx;
- auto *V0 = Ctx.atom();
- auto *V1 = Ctx.atom();
- EXPECT_EQ("(V0 => V1)", llvm::to_string(*Ctx.impl(V0, V1)));
+ auto B = Ctx.impl(Ctx.atom(), Ctx.atom());
+
+ auto Expected = R"((=>
+ B0
+ B1))";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Iff) {
+ // B0 <=> B1
ConstraintContext Ctx;
- auto *V0 = Ctx.atom();
- auto *V1 = Ctx.atom();
- EXPECT_EQ("(V0 = V1)", llvm::to_string(*Ctx.iff(V0, V1)));
+ auto B = Ctx.iff(Ctx.atom(), Ctx.atom());
+
+ auto Expected = R"((=
+ B0
+ B1))";
+ EXPECT_THAT(debugString(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Xor) {
+ // (B0 ^ !B1) V (!B0 ^ B1)
ConstraintContext Ctx;
- auto V0 = Ctx.atom();
- auto V1 = Ctx.atom();
- auto B = Ctx.disj(Ctx.conj(V0, Ctx.neg(V1)), Ctx.conj(Ctx.neg(V0), V1));
+ 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 = "((V0 & !V1) | (!V0 & V1))";
- EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+ auto Expected = R"((or
+ (and
+ B0
+ (not
+ B1))
+ (and
+ (not
+ B0)
+ B1)))";
+ EXPECT_THAT(debugString(*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 V0 = Ctx.atom();
- auto V1 = Ctx.atom();
- auto V2 = Ctx.atom();
- auto V3 = Ctx.atom();
- auto V4 = Ctx.atom();
- auto B = Ctx.conj(V0, Ctx.disj(V1, Ctx.conj(V2, Ctx.disj(V3, V4))));
+ auto True = cast<AtomicBoolValue>(Ctx.atom());
+ auto B = True;
- auto Expected = "(V0 & (V1 | (V2 & (V3 | V4))))";
- EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
+ 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));
}
TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
+ // (False && B0) v (True v B1)
+ ConstraintContext Ctx;
+ auto True = cast<AtomicBoolValue>(Ctx.atom());
+ auto False = cast<AtomicBoolValue>(Ctx.atom());
+ 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));
+}
+
+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 X = Ctx.atom();
- auto Y = Ctx.atom();
- Formula::AtomNames Names;
- Names[X->getAtom()] = "X";
- Names[Y->getAtom()] = "Y";
- auto B = Ctx.disj(Ctx.conj(Y, Ctx.atom()), Ctx.disj(X, Ctx.atom()));
+ 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.
- auto Expected = R"(((Y & V2) | (X | V3)))";
- std::string Actual;
- llvm::raw_string_ostream OS(Actual);
- B->print(OS, &Names);
- EXPECT_THAT(Actual, StrEq(Expected));
+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 ba0a77a910d7c4..9999dd3a475f1b 100644
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -9,10 +9,9 @@
#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"
@@ -24,31 +23,26 @@ 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<const Formula *> Vals) {
+Solver::Result solve(llvm::ArrayRef<BoolValue *> Vals) {
return WatchedLiteralsSolver().solve(Vals);
}
-MATCHER(unsat, "") {
- return arg.getStatus() == Solver::Result::Status::Unsatisfiable;
+void expectUnsatisfiable(Solver::Result Result) {
+ EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable);
+ EXPECT_FALSE(Result.getSolution().has_value());
}
-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);
+
+template <typename Matcher>
+void expectSatisfiable(Solver::Result Result, Matcher Solution) {
+ EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable);
+ EXPECT_THAT(Result.getSolution(), Optional(Solution));
}
TEST(SolverTest, Var) {
@@ -56,8 +50,9 @@ TEST(SolverTest, Var) {
auto X = Ctx.atom();
// X
- EXPECT_THAT(solve({X}),
- sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue))));
+ expectSatisfiable(
+ solve({X}),
+ UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue)));
}
TEST(SolverTest, NegatedVar) {
@@ -66,8 +61,9 @@ TEST(SolverTest, NegatedVar) {
auto NotX = Ctx.neg(X);
// !X
- EXPECT_THAT(solve({NotX}),
- sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse))));
+ expectSatisfiable(
+ solve({NotX}),
+ UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse)));
}
TEST(SolverTest, UnitConflict) {
@@ -76,7 +72,7 @@ TEST(SolverTest, UnitConflict) {
auto NotX = Ctx.neg(X);
// X ^ !X
- EXPECT_THAT(solve({X, NotX}), unsat());
+ expectUnsatisfiable(solve({X, NotX}));
}
TEST(SolverTest, DistinctVars) {
@@ -86,9 +82,36 @@ TEST(SolverTest, DistinctVars) {
auto NotY = Ctx.neg(Y);
// X ^ !Y
- EXPECT_THAT(solve({X, NotY}),
- sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
- Pair(Y->getAtom(), AssignedFalse))));
+ 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());
}
TEST(SolverTest, DoubleNegation) {
@@ -98,7 +121,7 @@ TEST(SolverTest, DoubleNegation) {
auto NotNotX = Ctx.neg(NotX);
// !!X ^ !X
- EXPECT_THAT(solve({NotNotX, NotX}), unsat());
+ expectUnsatisfiable(solve({NotNotX, NotX}));
}
TEST(SolverTest, NegatedDisjunction) {
@@ -109,7 +132,7 @@ TEST(SolverTest, NegatedDisjunction) {
auto NotXOrY = Ctx.neg(XOrY);
// !(X v Y) ^ (X v Y)
- EXPECT_THAT(solve({NotXOrY, XOrY}), unsat());
+ expectUnsatisfiable(solve({NotXOrY, XOrY}));
}
TEST(SolverTest, NegatedConjunction) {
@@ -120,7 +143,7 @@ TEST(SolverTest, NegatedConjunction) {
auto NotXAndY = Ctx.neg(XAndY);
// !(X ^ Y) ^ (X ^ Y)
- EXPECT_THAT(solve({NotXAndY, XAndY}), unsat());
+ expectUnsatisfiable(solve({NotXAndY, XAndY}));
}
TEST(SolverTest, DisjunctionSameVarWithNegation) {
@@ -130,7 +153,7 @@ TEST(SolverTest, DisjunctionSameVarWithNegation) {
auto XOrNotX = Ctx.disj(X, NotX);
// X v !X
- EXPECT_THAT(solve({XOrNotX}), sat(_));
+ expectSatisfiable(solve({XOrNotX}), _);
}
TEST(SolverTest, DisjunctionSameVar) {
@@ -139,7 +162,7 @@ TEST(SolverTest, DisjunctionSameVar) {
auto XOrX = Ctx.disj(X, X);
// X v X
- EXPECT_THAT(solve({XOrX}), sat(_));
+ expectSatisfiable(solve({XOrX}), _);
}
TEST(SolverTest, ConjunctionSameVarsConflict) {
@@ -149,7 +172,7 @@ TEST(SolverTest, ConjunctionSameVarsConflict) {
auto XAndNotX = Ctx.conj(X, NotX);
// X ^ !X
- EXPECT_THAT(solve({XAndNotX}), unsat());
+ expectUnsatisfiable(solve({XAndNotX}));
}
TEST(SolverTest, ConjunctionSameVar) {
@@ -158,7 +181,7 @@ TEST(SolverTest, ConjunctionSameVar) {
auto XAndX = Ctx.conj(X, X);
// X ^ X
- EXPECT_THAT(solve({XAndX}), sat(_));
+ expectSatisfiable(solve({XAndX}), _);
}
TEST(SolverTest, PureVar) {
@@ -171,9 +194,10 @@ TEST(SolverTest, PureVar) {
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (!X v Y) ^ (!X v !Y)
- EXPECT_THAT(solve({NotXOrY, NotXOrNotY}),
- sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
- Pair(Y->getAtom(), _))));
+ expectSatisfiable(
+ solve({NotXOrY, NotXOrNotY}),
+ UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
+ Pair(Y, _)));
}
TEST(SolverTest, MustAssumeVarIsFalse) {
@@ -187,9 +211,10 @@ TEST(SolverTest, MustAssumeVarIsFalse) {
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y)
- EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY}),
- sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
- Pair(Y->getAtom(), AssignedTrue))));
+ expectSatisfiable(
+ solve({XOrY, NotXOrY, NotXOrNotY}),
+ UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
+ Pair(Y, Solver::Result::Assignment::AssignedTrue)));
}
TEST(SolverTest, DeepConflict) {
@@ -204,7 +229,7 @@ TEST(SolverTest, DeepConflict) {
auto XOrNotY = Ctx.disj(X, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
- EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat());
+ expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));
}
TEST(SolverTest, IffIsEquivalentToDNF) {
@@ -218,7 +243,7 @@ TEST(SolverTest, IffIsEquivalentToDNF) {
auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF));
// !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
- EXPECT_THAT(solve({NotEquivalent}), unsat());
+ expectUnsatisfiable(solve({NotEquivalent}));
}
TEST(SolverTest, IffSameVars) {
@@ -227,7 +252,7 @@ TEST(SolverTest, IffSameVars) {
auto XEqX = Ctx.iff(X, X);
// X <=> X
- EXPECT_THAT(solve({XEqX}), sat(_));
+ expectSatisfiable(solve({XEqX}), _);
}
TEST(SolverTest, IffDistinctVars) {
@@ -237,12 +262,14 @@ TEST(SolverTest, IffDistinctVars) {
auto XEqY = Ctx.iff(X, Y);
// X <=> Y
- EXPECT_THAT(
+ expectSatisfiable(
solve({XEqY}),
- sat(AnyOf(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
- Pair(Y->getAtom(), AssignedTrue)),
- UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
- Pair(Y->getAtom(), AssignedFalse)))));
+ 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))));
}
TEST(SolverTest, IffWithUnits) {
@@ -252,9 +279,10 @@ TEST(SolverTest, IffWithUnits) {
auto XEqY = Ctx.iff(X, Y);
// (X <=> Y) ^ X ^ Y
- EXPECT_THAT(solve({XEqY, X, Y}),
- sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
- Pair(Y->getAtom(), AssignedTrue))));
+ expectSatisfiable(
+ solve({XEqY, X, Y}),
+ UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
+ Pair(Y, Solver::Result::Assignment::AssignedTrue)));
}
TEST(SolverTest, IffWithUnitsConflict) {
@@ -265,7 +293,7 @@ TEST(SolverTest, IffWithUnitsConflict) {
auto NotY = Ctx.neg(Y);
// (X <=> Y) ^ X !Y
- EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
+ expectUnsatisfiable(solve({XEqY, X, NotY}));
}
TEST(SolverTest, IffTransitiveConflict) {
@@ -278,7 +306,7 @@ TEST(SolverTest, IffTransitiveConflict) {
auto NotX = Ctx.neg(X);
// (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
- EXPECT_THAT(solve({XEqY, YEqZ, Z, NotX}), unsat());
+ expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));
}
TEST(SolverTest, DeMorgan) {
@@ -295,7 +323,7 @@ TEST(SolverTest, DeMorgan) {
auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
// A ^ B
- EXPECT_THAT(solve({A, B}), sat(_));
+ expectSatisfiable(solve({A, B}), _);
}
TEST(SolverTest, RespectsAdditionalConstraints) {
@@ -306,7 +334,7 @@ TEST(SolverTest, RespectsAdditionalConstraints) {
auto NotY = Ctx.neg(Y);
// (X <=> Y) ^ X ^ !Y
- EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
+ expectUnsatisfiable(solve({XEqY, X, NotY}));
}
TEST(SolverTest, ImplicationIsEquivalentToDNF) {
@@ -318,7 +346,7 @@ TEST(SolverTest, ImplicationIsEquivalentToDNF) {
auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF));
// !((X => Y) <=> (!X v Y))
- EXPECT_THAT(solve({NotEquivalent}), unsat());
+ expectUnsatisfiable(solve({NotEquivalent}));
}
TEST(SolverTest, ImplicationConflict) {
@@ -329,7 +357,7 @@ TEST(SolverTest, ImplicationConflict) {
auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
// X => Y ^ X ^ !Y
- EXPECT_THAT(solve({XImplY, XAndNotY}), unsat());
+ expectUnsatisfiable(solve({XImplY, XAndNotY}));
}
TEST(SolverTest, LowTimeoutResultsInTimedOut) {
diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
index 2eaa783d8ea1cf..e258eb7e75f592 100644
--- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -43,7 +43,6 @@
#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"
@@ -443,49 +442,55 @@ ValueT &getValueForDecl(ASTContext &ASTCtx, const Environment &Env,
/// Creates and owns constraints which are boolean values.
class ConstraintContext {
- unsigned NextAtom = 0;
- llvm::BumpPtrAllocator A;
-
- const Formula *make(Formula::Kind K,
- llvm::ArrayRef<const Formula *> Operands) {
- return &Formula::create(A, K, Operands);
- }
-
public:
- // Returns a reference to a fresh atomic variable.
- const Formula *atom() {
- return &Formula::create(A, Formula::AtomRef, {}, NextAtom++);
+ // Creates an atomic boolean value.
+ BoolValue *atom() {
+ Vals.push_back(std::make_unique<AtomicBoolValue>());
+ return Vals.back().get();
}
- // Returns a reference to a literal boolean value.
- const Formula *literal(bool B) {
- return &Formula::create(A, Formula::Literal, {}, B);
+ // Creates an instance of the Top boolean value.
+ BoolValue *top() {
+ Vals.push_back(std::make_unique<TopBoolValue>());
+ 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 conjunction value.
+ BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
+ Vals.push_back(
+ std::make_unique<ConjunctionValue>(*LeftSubVal, *RightSubVal));
+ 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 disjunction value.
+ BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
+ Vals.push_back(
+ std::make_unique<DisjunctionValue>(*LeftSubVal, *RightSubVal));
+ return Vals.back().get();
}
- // Creates a boolean negation.
- const Formula *neg(const Formula *Operand) {
- return make(Formula::Not, {Operand});
+ // Creates a boolean negation value.
+ BoolValue *neg(BoolValue *SubVal) {
+ Vals.push_back(std::make_unique<NegationValue>(*SubVal));
+ return Vals.back().get();
}
- // Creates a boolean implication.
- const Formula *impl(const Formula *LHS, const Formula *RHS) {
- return make(Formula::Implies, {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 biconditional.
- const Formula *iff(const Formula *LHS, const Formula *RHS) {
- return make(Formula::Equal, {LHS, RHS});
+ // Creates a boolean biconditional value.
+ BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
+ Vals.push_back(
+ std::make_unique<BiconditionalValue>(*LeftSubVal, *RightSubVal));
+ return Vals.back().get();
}
+
+private:
+ std::vector<std::unique_ptr<BoolValue>> Vals;
};
} // namespace test
diff --git a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
index 4da598745cfdd2..3f99ff5652ce28 100644
--- a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
@@ -2963,14 +2963,14 @@ TEST(TransferTest, AssignFromBoolLiteral) {
ASSERT_THAT(FooDecl, NotNull());
const auto *FooVal =
- dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
+ dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*FooDecl));
ASSERT_THAT(FooVal, NotNull());
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
ASSERT_THAT(BarDecl, NotNull());
const auto *BarVal =
- dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
+ dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*BarDecl));
ASSERT_THAT(BarVal, NotNull());
EXPECT_EQ(FooVal, &Env.getBoolLiteralValue(true));
@@ -3018,12 +3018,14 @@ TEST(TransferTest, AssignFromCompositeBoolExpression) {
ASSERT_THAT(BazDecl, NotNull());
const auto *BazVal =
- dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl));
+ dyn_cast_or_null<ConjunctionValue>(Env.getValue(*BazDecl));
ASSERT_THAT(BazVal, NotNull());
- auto &A = Env.arena();
- EXPECT_EQ(&BazVal->formula(),
- &A.makeAnd(FooVal->formula(),
- A.makeOr(BarVal->formula(), QuxVal->formula())));
+ EXPECT_EQ(&BazVal->getLeftSubValue(), FooVal);
+
+ const auto *BazRightSubValVal =
+ cast<DisjunctionValue>(&BazVal->getRightSubValue());
+ EXPECT_EQ(&BazRightSubValVal->getLeftSubValue(), BarVal);
+ EXPECT_EQ(&BazRightSubValVal->getRightSubValue(), QuxVal);
});
}
@@ -3066,12 +3068,15 @@ TEST(TransferTest, AssignFromCompositeBoolExpression) {
ASSERT_THAT(BazDecl, NotNull());
const auto *BazVal =
- dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl));
+ dyn_cast_or_null<DisjunctionValue>(Env.getValue(*BazDecl));
ASSERT_THAT(BazVal, NotNull());
- auto &A = Env.arena();
- EXPECT_EQ(&BazVal->formula(),
- &A.makeOr(A.makeAnd(FooVal->formula(), QuxVal->formula()),
- BarVal->formula()));
+
+ const auto *BazLeftSubValVal =
+ cast<ConjunctionValue>(&BazVal->getLeftSubValue());
+ EXPECT_EQ(&BazLeftSubValVal->getLeftSubValue(), FooVal);
+ EXPECT_EQ(&BazLeftSubValVal->getRightSubValue(), QuxVal);
+
+ EXPECT_EQ(&BazVal->getRightSubValue(), BarVal);
});
}
@@ -3117,14 +3122,17 @@ TEST(TransferTest, AssignFromCompositeBoolExpression) {
ASSERT_THAT(FooDecl, NotNull());
const auto *FooVal =
- dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
+ dyn_cast_or_null<ConjunctionValue>(Env.getValue(*FooDecl));
ASSERT_THAT(FooVal, NotNull());
- auto &A = Env.arena();
- EXPECT_EQ(
- &FooVal->formula(),
- &A.makeAnd(A.makeAnd(A.makeAnd(AVal->formula(), BVal->formula()),
- CVal->formula()),
- DVal->formula()));
+
+ const auto &FooLeftSubVal =
+ cast<ConjunctionValue>(FooVal->getLeftSubValue());
+ const auto &FooLeftLeftSubVal =
+ cast<ConjunctionValue>(FooLeftSubVal.getLeftSubValue());
+ EXPECT_EQ(&FooLeftLeftSubVal.getLeftSubValue(), AVal);
+ EXPECT_EQ(&FooLeftLeftSubVal.getRightSubValue(), BVal);
+ EXPECT_EQ(&FooLeftSubVal.getRightSubValue(), CVal);
+ EXPECT_EQ(&FooVal->getRightSubValue(), DVal);
});
}
}
@@ -3148,17 +3156,17 @@ TEST(TransferTest, AssignFromBoolNegation) {
ASSERT_THAT(FooDecl, NotNull());
const auto *FooVal =
- dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
+ dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*FooDecl));
ASSERT_THAT(FooVal, NotNull());
const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar");
ASSERT_THAT(BarDecl, NotNull());
const auto *BarVal =
- dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
+ dyn_cast_or_null<NegationValue>(Env.getValue(*BarDecl));
ASSERT_THAT(BarVal, NotNull());
- auto &A = Env.arena();
- EXPECT_EQ(&BarVal->formula(), &A.makeNot(FooVal->formula()));
+
+ EXPECT_EQ(&BarVal->getSubVal(), FooVal);
});
}
diff --git a/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp b/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
index 02f3adeaeda756..2b7341b0839e5f 100644
--- a/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
@@ -7,7 +7,6 @@
//===----------------------------------------------------------------------===//
#include "clang/Analysis/FlowSensitive/Value.h"
-#include "clang/Analysis/FlowSensitive/Arena.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -40,19 +39,17 @@ TEST(ValueTest, AliasedPointersEquivalent) {
}
TEST(ValueTest, TopsEquivalent) {
- Arena A;
- TopBoolValue V1(A.makeAtomRef(Atom(0)));
- TopBoolValue V2(A.makeAtomRef(Atom(1)));
+ TopBoolValue V1;
+ TopBoolValue V2;
EXPECT_TRUE(areEquivalentValues(V1, V2));
EXPECT_TRUE(areEquivalentValues(V2, V1));
}
TEST(ValueTest, EquivalentValuesWithDifferentPropsEquivalent) {
- Arena A;
- TopBoolValue Prop1(A.makeAtomRef(Atom(0)));
- TopBoolValue Prop2(A.makeAtomRef(Atom(1)));
- TopBoolValue V1(A.makeAtomRef(Atom(2)));
- TopBoolValue V2(A.makeAtomRef(Atom(3)));
+ TopBoolValue Prop1;
+ TopBoolValue Prop2;
+ TopBoolValue V1;
+ TopBoolValue V2;
V1.setProperty("foo", Prop1);
V2.setProperty("bar", Prop2);
EXPECT_TRUE(areEquivalentValues(V1, V2));
@@ -60,10 +57,9 @@ TEST(ValueTest, EquivalentValuesWithDifferentPropsEquivalent) {
}
TEST(ValueTest, DifferentKindsNotEquivalent) {
- Arena A;
auto L = ScalarStorageLocation(QualType());
ReferenceValue V1(L);
- TopBoolValue V2(A.makeAtomRef(Atom(0)));
+ TopBoolValue V2;
EXPECT_FALSE(areEquivalentValues(V1, V2));
EXPECT_FALSE(areEquivalentValues(V2, V1));
}
More information about the cfe-commits
mailing list