[clang] fc9821a - Reland "[dataflow] Add dedicated representation of boolean formulas"
Sam McCall via cfe-commits
cfe-commits at lists.llvm.org
Fri Jul 7 02:58:47 PDT 2023
Author: Sam McCall
Date: 2023-07-07T11:58:33+02:00
New Revision: fc9821a877d4e1443603d67539e4369b3ec72890
URL: https://github.com/llvm/llvm-project/commit/fc9821a877d4e1443603d67539e4369b3ec72890
DIFF: https://github.com/llvm/llvm-project/commit/fc9821a877d4e1443603d67539e4369b3ec72890.diff
LOG: Reland "[dataflow] Add dedicated representation of boolean formulas"
This reverts commit 7a72ce98224be76d9328e65eee472381f7c8e7fe.
Test problems were due to unspecified order of function arg evaluation.
Reland "[dataflow] Replace most BoolValue subclasses with references to Formula (and AtomicBoolValue => Atom and BoolValue => Formula where appropriate)"
This properly frees the Value hierarchy from managing boolean formulas.
We still distinguish AtomicBoolValue; this type is used in client code.
However we expect to convert such uses to BoolValue (where the
distinction is not needed) or Atom (where atomic identity is intended),
and then fold AtomicBoolValue into FormulaBoolValue.
We also distinguish TopBoolValue; this has distinct rules for
widen/join/equivalence, and top-ness is not represented in Formula.
It'd be nice to find a cleaner representation (e.g. the absence of a
formula), but no immediate plans.
For now, BoolValues with the same Formula are deduplicated. This doesn't
seem desirable, as Values are mutable by their creators (properties).
We can probably drop this for FormulaBoolValue immediately (not in this
patch, to isolate changes). For AtomicBoolValue we first need to update
clients to stop using value pointers for atom identity.
The data structures around flow conditions are updated:
- flow condition tokens are Atom, rather than AtomicBoolValue*
- conditions are Formula, rather than BoolValue
Most APIs were changed directly, some with many clients had a
new version added and the existing one deprecated.
The factories for BoolValues in Environment keep their existing
signatures for now (e.g. makeOr(BoolValue, BoolValue) => BoolValue)
and are not deprecated. These have very many clients and finding the
most ergonomic API & migration path still needs some thought.
Differential Revision: https://reviews.llvm.org/D153469
Added:
clang/include/clang/Analysis/FlowSensitive/Formula.h
clang/lib/Analysis/FlowSensitive/Formula.cpp
Modified:
clang/include/clang/Analysis/FlowSensitive/Arena.h
clang/include/clang/Analysis/FlowSensitive/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:
################################################################################
diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h
index 83b4ddeec02564..373697dc7379c5 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Arena.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h
@@ -8,6 +8,7 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include <vector>
@@ -15,12 +16,10 @@
namespace clang::dataflow {
/// The Arena owns the objects that model data within an analysis.
-/// For example, `Value` and `StorageLocation`.
+/// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`.
class Arena {
public:
- Arena()
- : TrueVal(create<AtomicBoolValue>()),
- FalseVal(create<AtomicBoolValue>()) {}
+ Arena() : True(makeAtom()), False(makeAtom()) {}
Arena(const Arena &) = delete;
Arena &operator=(const Arena &) = delete;
@@ -56,33 +55,25 @@ class Arena {
.get());
}
- /// 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);
+ /// 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 symbolic integer value that models an integer literal equal to
/// `Value`. These literals are the same every time.
@@ -90,21 +81,46 @@ class Arena {
/// an integer literal is associated with.
IntegerValue &makeIntLiteral(llvm::APInt Value);
- /// 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;
+ // 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 makeAtomRef(Value ? True : False);
}
+ /// Returns a new atomic boolean variable, distinct from any other.
+ Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
+
/// 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.
- AtomicBoolValue &makeFlowConditionToken() {
- return create<AtomicBoolValue>();
- }
+ Atom makeFlowConditionToken() { return makeAtom(); }
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;
@@ -112,18 +128,18 @@ class Arena {
// Indices that are used to avoid recreating the same integer literals and
// composite boolean values.
llvm::DenseMap<llvm::APInt, IntegerValue *> IntegerLiterals;
- 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;
+ 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;
+
+ Atom True, False;
};
} // namespace clang::dataflow
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index 735f2b2d85021c..2a31a3477e8ceb 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -138,33 +138,31 @@ class DataflowAnalysisContext {
PointerValue &getOrCreateNullPointerValue(QualType PointeeType);
/// Adds `Constraint` to the flow condition identified by `Token`.
- void addFlowConditionConstraint(AtomicBoolValue &Token,
- BoolValue &Constraint);
+ void addFlowConditionConstraint(Atom Token, const Formula &Constraint);
/// Creates a new flow condition with the same constraints as the flow
/// condition identified by `Token` and returns its token.
- AtomicBoolValue &forkFlowCondition(AtomicBoolValue &Token);
+ Atom forkFlowCondition(Atom Token);
/// Creates a new flow condition that represents the disjunction of the flow
/// conditions identified by `FirstToken` and `SecondToken`, and returns its
/// token.
- AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
- AtomicBoolValue &SecondToken);
+ Atom joinFlowConditions(Atom FirstToken, Atom SecondToken);
/// Returns true if and only if the constraints of the flow condition
/// identified by `Token` imply that `Val` is true.
- bool flowConditionImplies(AtomicBoolValue &Token, BoolValue &Val);
+ bool flowConditionImplies(Atom Token, const Formula &);
/// Returns true if and only if the constraints of the flow condition
/// identified by `Token` are always true.
- bool flowConditionIsTautology(AtomicBoolValue &Token);
+ bool flowConditionIsTautology(Atom 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 equivalentBoolValues(BoolValue &Val1, BoolValue &Val2);
+ bool equivalentFormulas(const Formula &Val1, const Formula &Val2);
- LLVM_DUMP_METHOD void dumpFlowCondition(AtomicBoolValue &Token,
+ LLVM_DUMP_METHOD void dumpFlowCondition(Atom Token,
llvm::raw_ostream &OS = llvm::dbgs());
/// Returns the `ControlFlowContext` registered for `F`, if any. Otherwise,
@@ -181,7 +179,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<BoolValue *> Constraints);
+ Solver::Result querySolver(llvm::SetVector<const Formula *> Constraints);
private:
friend class Environment;
@@ -209,12 +207,12 @@ class DataflowAnalysisContext {
/// to track tokens of flow conditions that were already visited by recursive
/// calls.
void addTransitiveFlowConditionConstraints(
- AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints,
- llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
+ Atom Token, llvm::SetVector<const Formula *> &Constraints,
+ llvm::DenseSet<Atom> &VisitedTokens);
/// Returns true if the solver is able to prove that there is no satisfying
/// assignment for `Constraints`
- bool isUnsatisfiable(llvm::SetVector<BoolValue *> Constraints) {
+ bool isUnsatisfiable(llvm::SetVector<const Formula *> Constraints) {
return querySolver(std::move(Constraints)).getStatus() ==
Solver::Result::Status::Unsatisfiable;
}
@@ -253,9 +251,8 @@ 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<AtomicBoolValue *, llvm::DenseSet<AtomicBoolValue *>>
- FlowConditionDeps;
- llvm::DenseMap<AtomicBoolValue *, BoolValue *> FlowConditionConstraints;
+ llvm::DenseMap<Atom, llvm::DenseSet<Atom>> FlowConditionDeps;
+ llvm::DenseMap<Atom, const Formula *> 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 faeb5eb69cd838..116373dce15c81 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -456,29 +456,30 @@ class Environment {
template <typename T, typename... Args>
std::enable_if_t<std::is_base_of<Value, T>::value, T &>
create(Args &&...args) {
- return DACtx->arena().create<T>(std::forward<Args>(args)...);
+ return 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 DACtx->arena().makeIntLiteral(Value);
+ return arena().makeIntLiteral(Value);
}
/// Returns a symbolic boolean value that models a boolean literal equal to
/// `Value`
AtomicBoolValue &getBoolLiteralValue(bool Value) const {
- return DACtx->arena().makeLiteral(Value);
+ return cast<AtomicBoolValue>(
+ arena().makeBoolValue(arena().makeLiteral(Value)));
}
/// Returns an atomic boolean value.
BoolValue &makeAtomicBoolValue() const {
- return DACtx->arena().create<AtomicBoolValue>();
+ return arena().makeAtomValue();
}
/// Returns a unique instance of boolean Top.
BoolValue &makeTopBoolValue() const {
- return DACtx->arena().create<TopBoolValue>();
+ return arena().makeTopValue();
}
/// Returns a boolean value that represents the conjunction of `LHS` and
@@ -486,7 +487,8 @@ 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 DACtx->arena().makeAnd(LHS, RHS);
+ return arena().makeBoolValue(
+ arena().makeAnd(LHS.formula(), RHS.formula()));
}
/// Returns a boolean value that represents the disjunction of `LHS` and
@@ -494,13 +496,14 @@ 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 DACtx->arena().makeOr(LHS, RHS);
+ return arena().makeBoolValue(
+ arena().makeOr(LHS.formula(), RHS.formula()));
}
/// 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 DACtx->arena().makeNot(Val);
+ return arena().makeBoolValue(arena().makeNot(Val.formula()));
}
/// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with
@@ -508,7 +511,8 @@ 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 DACtx->arena().makeImplies(LHS, RHS);
+ return arena().makeBoolValue(
+ arena().makeImplies(LHS.formula(), RHS.formula()));
}
/// Returns a boolean value represents `LHS` <=> `RHS`. Subsequent calls with
@@ -516,17 +520,22 @@ 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 DACtx->arena().makeEquals(LHS, RHS);
+ return arena().makeBoolValue(
+ arena().makeEquals(LHS.formula(), RHS.formula()));
}
/// Returns the token that identifies the flow condition of the environment.
- AtomicBoolValue &getFlowConditionToken() const { return *FlowConditionToken; }
+ Atom 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,
@@ -547,6 +556,8 @@ 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;
@@ -617,7 +628,7 @@ class Environment {
std::pair<StructValue *, const ValueDecl *>>
MemberLocToStruct;
- AtomicBoolValue *FlowConditionToken;
+ Atom 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 360786b02729f2..6b9f3681490af1 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
@@ -19,7 +19,6 @@
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/Value.h"
-#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/StringRef.h"
namespace clang {
@@ -28,52 +27,9 @@ namespace dataflow {
/// Returns a string representation of a value kind.
llvm::StringRef debugString(Value::Kind Kind);
-/// Returns a string representation of a boolean assignment to true or false.
-llvm::StringRef debugString(Solver::Result::Assignment Assignment);
-
/// Returns a string representation of the result status of a SAT check.
llvm::StringRef debugString(Solver::Result::Status Status);
-/// Returns a string representation for the boolean value `B`.
-///
-/// Atomic booleans appearing in the boolean value `B` are assigned to labels
-/// either specified in `AtomNames` or created by default rules as B0, B1, ...
-///
-/// Requirements:
-///
-/// Names assigned to atoms should not be repeated in `AtomNames`.
-std::string debugString(
- const BoolValue &B,
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-
-/// Returns a string representation for `Constraints` - a collection of boolean
-/// formulas.
-///
-/// Atomic booleans appearing in the boolean value `Constraints` are assigned to
-/// labels either specified in `AtomNames` or created by default rules as B0,
-/// B1, ...
-///
-/// Requirements:
-///
-/// Names assigned to atoms should not be repeated in `AtomNames`.
-std::string debugString(
- const llvm::ArrayRef<BoolValue *> Constraints,
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-
-/// Returns a string representation for `Constraints` - a collection of boolean
-/// formulas and the `Result` of satisfiability checking.
-///
-/// Atomic booleans appearing in `Constraints` and `Result` are assigned to
-/// labels either specified in `AtomNames` or created by default rules as B0,
-/// B1, ...
-///
-/// Requirements:
-///
-/// Names assigned to atoms should not be repeated in `AtomNames`.
-std::string debugString(
- ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
-
} // namespace dataflow
} // namespace clang
diff --git a/clang/include/clang/Analysis/FlowSensitive/Formula.h b/clang/include/clang/Analysis/FlowSensitive/Formula.h
new file mode 100644
index 00000000000000..0c7b1ecd02b17c
--- /dev/null
+++ b/clang/include/clang/Analysis/FlowSensitive/Formula.h
@@ -0,0 +1,137 @@
+//===- Formula.h - Boolean formulas -----------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
+#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H
+
+#include "clang/Basic/LLVM.h"
+#include "llvm/ADT/ArrayRef.h"
+#include "llvm/ADT/DenseMap.h"
+#include "llvm/ADT/DenseMapInfo.h"
+#include "llvm/ADT/STLFunctionalExtras.h"
+#include "llvm/Support/Allocator.h"
+#include "llvm/Support/raw_ostream.h"
+#include <cassert>
+#include <string>
+#include <type_traits>
+
+namespace clang::dataflow {
+
+/// Identifies an atomic boolean variable such as "V1".
+///
+/// This often represents an assertion that is interesting to the analysis but
+/// cannot immediately be proven true or false. For example:
+/// - V1 may mean "the program reaches this point",
+/// - V2 may mean "the parameter was null"
+///
+/// We can use these variables in formulas to describe relationships we know
+/// to be true: "if the parameter was null, the program reaches this point".
+/// We also express hypotheses as formulas, and use a SAT solver to check
+/// whether they are consistent with the known facts.
+enum class Atom : unsigned {};
+
+/// A boolean expression such as "true" or "V1 & !V2".
+/// Expressions may refer to boolean atomic variables. These should take a
+/// consistent true/false value across the set of formulas being considered.
+///
+/// (Formulas are always expressions in terms of boolean variables rather than
+/// e.g. integers because our underlying model is SAT rather than e.g. SMT).
+///
+/// Simple formulas such as "true" and "V1" are self-contained.
+/// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or'
+/// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as
+/// trailing objects.
+/// For this reason, Formulas are Arena-allocated and over-aligned.
+class Formula;
+class alignas(const Formula *) Formula {
+public:
+ enum Kind : unsigned {
+ /// A reference to an atomic boolean variable.
+ /// We name these e.g. "V3", where 3 == atom identity == Value.
+ AtomRef,
+ // FIXME: add const true/false rather than modeling them as variables
+
+ Not, /// True if its only operand is false
+
+ // These kinds connect two operands LHS and RHS
+ And, /// True if LHS and RHS are both true
+ Or, /// True if either LHS or RHS is true
+ Implies, /// True if LHS is false or RHS is true
+ Equal, /// True if LHS and RHS have the same truth value
+ };
+ Kind kind() const { return FormulaKind; }
+
+ Atom getAtom() const {
+ assert(kind() == AtomRef);
+ return static_cast<Atom>(Value);
+ }
+
+ ArrayRef<const Formula *> operands() const {
+ return ArrayRef(reinterpret_cast<Formula *const *>(this + 1),
+ numOperands(kind()));
+ }
+
+ using AtomNames = llvm::DenseMap<Atom, std::string>;
+ // Produce a stable human-readable representation of this formula.
+ // For example: (V3 | !(V1 & V2))
+ // If AtomNames is provided, these override the default V0, V1... names.
+ void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const;
+
+ // Allocate Formulas using Arena rather than calling this function directly.
+ static Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K,
+ ArrayRef<const Formula *> Operands,
+ unsigned Value = 0);
+
+private:
+ Formula() = default;
+ Formula(const Formula &) = delete;
+ Formula &operator=(const Formula &) = delete;
+
+ static unsigned numOperands(Kind K) {
+ switch (K) {
+ case AtomRef:
+ return 0;
+ case Not:
+ return 1;
+ case And:
+ case Or:
+ case Implies:
+ case Equal:
+ return 2;
+ }
+ }
+
+ Kind FormulaKind;
+ // Some kinds of formula have scalar values, e.g. AtomRef's atom number.
+ unsigned Value;
+};
+
+// The default names of atoms are V0, V1 etc in order of creation.
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) {
+ return OS << 'V' << static_cast<unsigned>(A);
+}
+inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) {
+ F.print(OS);
+ return OS;
+}
+
+} // namespace clang::dataflow
+namespace llvm {
+template <> struct DenseMapInfo<clang::dataflow::Atom> {
+ using Atom = clang::dataflow::Atom;
+ using Underlying = std::underlying_type_t<Atom>;
+
+ static inline Atom getEmptyKey() { return Atom(Underlying(-1)); }
+ static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); }
+ static unsigned getHashValue(const Atom &Val) {
+ return DenseMapInfo<Underlying>::getHashValue(Underlying(Val));
+ }
+ static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; }
+};
+} // namespace llvm
+#endif
diff --git a/clang/include/clang/Analysis/FlowSensitive/Solver.h b/clang/include/clang/Analysis/FlowSensitive/Solver.h
index 10964eab8c34cc..079f6802f241ee 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Solver.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Solver.h
@@ -14,12 +14,10 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
-#include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Basic/LLVM.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/DenseMap.h"
-#include "llvm/ADT/DenseSet.h"
-#include "llvm/Support/Compiler.h"
#include <optional>
#include <vector>
@@ -49,8 +47,7 @@ class Solver {
/// Constructs a result indicating that the queried boolean formula is
/// satisfiable. The result will hold a solution found by the solver.
- static Result
- Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) {
+ static Result Satisfiable(llvm::DenseMap<Atom, Assignment> Solution) {
return Result(Status::Satisfiable, std::move(Solution));
}
@@ -68,19 +65,17 @@ class Solver {
/// Returns a truth assignment to boolean values that satisfies the queried
/// boolean formula if available. Otherwise, an empty optional is returned.
- std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>>
- getSolution() const {
+ std::optional<llvm::DenseMap<Atom, Assignment>> getSolution() const {
return Solution;
}
private:
- Result(
- enum Status SATCheckStatus,
- std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution)
+ Result(Status SATCheckStatus,
+ std::optional<llvm::DenseMap<Atom, Assignment>> Solution)
: SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {}
Status SATCheckStatus;
- std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution;
+ std::optional<llvm::DenseMap<Atom, Assignment>> Solution;
};
virtual ~Solver() = default;
@@ -91,14 +86,12 @@ class Solver {
/// Requirements:
///
/// All elements in `Vals` must not be null.
- virtual Result solve(llvm::ArrayRef<BoolValue *> Vals) = 0;
-
- LLVM_DEPRECATED("Pass ArrayRef for determinism", "")
- virtual Result solve(llvm::DenseSet<BoolValue *> Vals) {
- return solve(ArrayRef(std::vector<BoolValue *>(Vals.begin(), Vals.end())));
- }
+ virtual Result solve(llvm::ArrayRef<const Formula *> Vals) = 0;
};
+llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &);
+llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment);
+
} // namespace dataflow
} // namespace clang
diff --git a/clang/include/clang/Analysis/FlowSensitive/Value.h b/clang/include/clang/Analysis/FlowSensitive/Value.h
index 59d5fa6923aabd..1d4f8008d19307 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,14 +38,10 @@ class Value {
Pointer,
Struct,
- // Synthetic boolean values are either atomic values or logical connectives.
+ // TODO: Top values should not be need to be type-specific.
TopBool,
AtomicBool,
- Conjunction,
- Disjunction,
- Negation,
- Implication,
- Biconditional,
+ FormulaBool,
};
explicit Value(Kind ValKind) : ValKind(ValKind) {}
@@ -95,151 +91,68 @@ bool areEquivalentValues(const Value &Val1, const Value &Val2);
/// Models a boolean.
class BoolValue : public Value {
+ const Formula *F;
+
public:
- explicit BoolValue(Kind ValueKind) : Value(ValueKind) {}
+ explicit BoolValue(Kind ValueKind, const Formula &F)
+ : Value(ValueKind), F(&F) {}
static bool classof(const Value *Val) {
return Val->getKind() == Kind::TopBool ||
Val->getKind() == Kind::AtomicBool ||
- Val->getKind() == Kind::Conjunction ||
- Val->getKind() == Kind::Disjunction ||
- Val->getKind() == Kind::Negation ||
- Val->getKind() == Kind::Implication ||
- Val->getKind() == Kind::Biconditional;
+ Val->getKind() == Kind::FormulaBool;
}
+
+ const Formula &formula() const { return *F; }
};
-/// Models the trivially true formula, which is Top in the lattice of boolean
-/// formulas.
+/// 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.
class TopBoolValue final : public BoolValue {
public:
- TopBoolValue() : BoolValue(Kind::TopBool) {}
-
- static bool classof(const Value *Val) {
- return Val->getKind() == Kind::TopBool;
+ TopBoolValue(const Formula &F) : BoolValue(Kind::TopBool, F) {
+ assert(F.kind() == Formula::AtomRef);
}
-};
-
-/// Models an atomic boolean.
-class AtomicBoolValue : public BoolValue {
-public:
- 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;
+ return Val->getKind() == Kind::TopBool;
}
- /// 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;
+ Atom getAtom() const { return formula().getAtom(); }
};
-/// Models a boolean disjunction.
-class DisjunctionValue : public BoolValue {
+/// Models an atomic boolean.
+///
+/// FIXME: Merge this class into FormulaBoolValue.
+/// When we want to specify atom identity, use Atom.
+class AtomicBoolValue final : 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;
+ explicit AtomicBoolValue(const Formula &F) : BoolValue(Kind::AtomicBool, F) {
+ assert(F.kind() == Formula::AtomRef);
}
- /// 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;
+ return Val->getKind() == Kind::AtomicBool;
}
- /// Returns the sub-value of the negation.
- BoolValue &getSubVal() const { return SubVal; }
-
-private:
- BoolValue &SubVal;
+ Atom getAtom() const { return formula().getAtom(); }
};
-/// Models a boolean implication.
-///
-/// Equivalent to `!LHS v RHS`.
-class ImplicationValue : public BoolValue {
+/// Models a compound boolean formula.
+class FormulaBoolValue final : public BoolValue {
public:
- explicit ImplicationValue(BoolValue &LeftSubVal, BoolValue &RightSubVal)
- : BoolValue(Kind::Implication), LeftSubVal(LeftSubVal),
- RightSubVal(RightSubVal) {}
-
- static bool classof(const Value *Val) {
- return Val->getKind() == Kind::Implication;
+ explicit FormulaBoolValue(const Formula &F)
+ : BoolValue(Kind::FormulaBool, F) {
+ assert(F.kind() != Formula::AtomRef && "For now, use AtomicBoolValue");
}
- /// 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::Biconditional;
+ return Val->getKind() == Kind::FormulaBool;
}
-
- /// 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 b69cc01542c550..a0cdce93c9d470 100644
--- a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
+++ b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
@@ -14,8 +14,8 @@
#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/ArrayRef.h"
#include <limits>
@@ -46,7 +46,7 @@ class WatchedLiteralsSolver : public Solver {
explicit WatchedLiteralsSolver(std::int64_t WorkLimit)
: MaxIterations(WorkLimit) {}
- Result solve(llvm::ArrayRef<BoolValue *> Vals) override;
+ Result solve(llvm::ArrayRef<const Formula *> Vals) override;
};
} // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp
index cff6c45e185422..a12da2d9b555eb 100644
--- a/clang/lib/Analysis/FlowSensitive/Arena.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -7,65 +7,75 @@
//===----------------------------------------------------------------------===//
#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
namespace clang::dataflow {
-static std::pair<BoolValue *, BoolValue *>
-makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) {
+static std::pair<const Formula *, const Formula *>
+canonicalFormulaPair(const Formula &LHS, const Formula &RHS) {
auto Res = std::make_pair(&LHS, &RHS);
- if (&RHS < &LHS)
+ if (&RHS < &LHS) // FIXME: use a deterministic order instead
std::swap(Res.first, Res.second);
return Res;
}
-BoolValue &Arena::makeAnd(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeAtomRef(Atom A) {
+ auto [It, Inserted] = AtomRefs.try_emplace(A);
+ if (Inserted)
+ It->second =
+ &Formula::create(Alloc, Formula::AtomRef, {}, static_cast<unsigned>(A));
+ return *It->second;
+}
+
+const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) {
if (&LHS == &RHS)
return LHS;
- auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
- nullptr);
- if (Res.second)
- Res.first->second = &create<ConjunctionValue>(LHS, RHS);
- return *Res.first->second;
+ auto [It, Inserted] =
+ Ands.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+ if (Inserted)
+ It->second = &Formula::create(Alloc, Formula::And, {&LHS, &RHS});
+ return *It->second;
}
-BoolValue &Arena::makeOr(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) {
if (&LHS == &RHS)
return LHS;
- auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
- nullptr);
- if (Res.second)
- Res.first->second = &create<DisjunctionValue>(LHS, RHS);
- return *Res.first->second;
+ auto [It, Inserted] =
+ Ors.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+ if (Inserted)
+ It->second = &Formula::create(Alloc, Formula::Or, {&LHS, &RHS});
+ return *It->second;
}
-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) {
+ auto [It, Inserted] = Nots.try_emplace(&Val, nullptr);
+ if (Inserted)
+ It->second = &Formula::create(Alloc, Formula::Not, {&Val});
+ return *It->second;
}
-BoolValue &Arena::makeImplies(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) {
if (&LHS == &RHS)
return makeLiteral(true);
- 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;
+ auto [It, Inserted] =
+ Implies.try_emplace(std::make_pair(&LHS, &RHS), nullptr);
+ if (Inserted)
+ It->second = &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS});
+ return *It->second;
}
-BoolValue &Arena::makeEquals(BoolValue &LHS, BoolValue &RHS) {
+const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) {
if (&LHS == &RHS)
return makeLiteral(true);
- auto Res = BiconditionalVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS),
- nullptr);
- if (Res.second)
- Res.first->second = &create<BiconditionalValue>(LHS, RHS);
- return *Res.first->second;
+ auto [It, Inserted] =
+ Equals.try_emplace(canonicalFormulaPair(LHS, RHS), nullptr);
+ if (Inserted)
+ It->second = &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS});
+ return *It->second;
}
IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
@@ -76,4 +86,13 @@ 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 d59bebf6a5a127..171884afe8f4bf 100644
--- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -3,6 +3,7 @@ add_clang_library(clangAnalysisFlowSensitive
ControlFlowContext.cpp
DataflowAnalysisContext.cpp
DataflowEnvironment.cpp
+ Formula.cpp
HTMLLogger.cpp
Logger.cpp
RecordOps.cpp
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 37bcc8be958792..a807ef8209be85 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -15,6 +15,7 @@
#include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h"
#include "clang/AST/ExprCXX.h"
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Logger.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/SetOperations.h"
@@ -23,9 +24,12 @@
#include "llvm/Support/Debug.h"
#include "llvm/Support/FileSystem.h"
#include "llvm/Support/Path.h"
+#include "llvm/Support/raw_ostream.h"
#include <cassert>
#include <memory>
+#include <string>
#include <utility>
+#include <vector>
static llvm::cl::opt<std::string> DataflowLog(
"dataflow-log", llvm::cl::Hidden, llvm::cl::ValueOptional,
@@ -98,108 +102,114 @@ DataflowAnalysisContext::getOrCreateNullPointerValue(QualType PointeeType) {
}
void DataflowAnalysisContext::addFlowConditionConstraint(
- AtomicBoolValue &Token, BoolValue &Constraint) {
- auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint);
+ Atom Token, const Formula &Constraint) {
+ auto Res = FlowConditionConstraints.try_emplace(Token, &Constraint);
if (!Res.second) {
Res.first->second =
&arena().makeAnd(*Res.first->second, Constraint);
}
}
-AtomicBoolValue &
-DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
- auto &ForkToken = arena().makeFlowConditionToken();
- FlowConditionDeps[&ForkToken].insert(&Token);
- addFlowConditionConstraint(ForkToken, Token);
+Atom DataflowAnalysisContext::forkFlowCondition(Atom Token) {
+ Atom ForkToken = arena().makeFlowConditionToken();
+ FlowConditionDeps[ForkToken].insert(Token);
+ addFlowConditionConstraint(ForkToken, arena().makeAtomRef(Token));
return ForkToken;
}
-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));
+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)));
return Token;
}
-Solver::Result
-DataflowAnalysisContext::querySolver(llvm::SetVector<BoolValue *> Constraints) {
+Solver::Result DataflowAnalysisContext::querySolver(
+ llvm::SetVector<const Formula *> Constraints) {
Constraints.insert(&arena().makeLiteral(true));
Constraints.insert(&arena().makeNot(arena().makeLiteral(false)));
return S->solve(Constraints.getArrayRef());
}
-bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
- BoolValue &Val) {
+bool DataflowAnalysisContext::flowConditionImplies(Atom Token,
+ const Formula &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<BoolValue *> Constraints;
- Constraints.insert(&Token);
+ llvm::SetVector<const Formula *> Constraints;
+ Constraints.insert(&arena().makeAtomRef(Token));
Constraints.insert(&arena().makeNot(Val));
- llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+ llvm::DenseSet<Atom> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
return isUnsatisfiable(std::move(Constraints));
}
-bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
+bool DataflowAnalysisContext::flowConditionIsTautology(Atom Token) {
// Returns true if and only if we cannot prove that the flow condition can
// ever be false.
- llvm::SetVector<BoolValue *> Constraints;
- Constraints.insert(&arena().makeNot(Token));
- llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+ llvm::SetVector<const Formula *> Constraints;
+ Constraints.insert(&arena().makeNot(arena().makeAtomRef(Token)));
+ llvm::DenseSet<Atom> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
return isUnsatisfiable(std::move(Constraints));
}
-bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
- BoolValue &Val2) {
- llvm::SetVector<BoolValue*> Constraints;
+bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1,
+ const Formula &Val2) {
+ llvm::SetVector<const Formula *> Constraints;
Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2)));
return isUnsatisfiable(std::move(Constraints));
}
void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
- AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints,
- llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) {
- auto Res = VisitedTokens.insert(&Token);
+ Atom Token, llvm::SetVector<const Formula *> &Constraints,
+ llvm::DenseSet<Atom> &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(&Token);
+ Constraints.insert(&arena().makeAtomRef(Token));
} else {
// Bind flow condition token via `iff` to its set of constraints:
// FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
- Constraints.insert(&arena().makeEquals(Token, *ConstraintsIt->second));
+ Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token),
+ *ConstraintsIt->second));
}
- auto DepsIt = FlowConditionDeps.find(&Token);
+ auto DepsIt = FlowConditionDeps.find(Token);
if (DepsIt != FlowConditionDeps.end()) {
- for (AtomicBoolValue *DepToken : DepsIt->second) {
- addTransitiveFlowConditionConstraints(*DepToken, Constraints,
+ for (Atom DepToken : DepsIt->second) {
+ addTransitiveFlowConditionConstraints(DepToken, Constraints,
VisitedTokens);
}
}
}
-void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token,
+void DataflowAnalysisContext::dumpFlowCondition(Atom Token,
llvm::raw_ostream &OS) {
- llvm::SetVector<BoolValue *> Constraints;
- Constraints.insert(&Token);
- llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
+ llvm::SetVector<const Formula *> Constraints;
+ Constraints.insert(&arena().makeAtomRef(Token));
+ llvm::DenseSet<Atom> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {
- {&arena().makeLiteral(false), "False"},
- {&arena().makeLiteral(true), "True"}};
- OS << debugString(Constraints.getArrayRef(), AtomNames);
+ // TODO: have formulas know about true/false directly instead
+ Atom True = arena().makeLiteral(true).getAtom();
+ Atom False = arena().makeLiteral(false).getAtom();
+ Formula::AtomNames Names = {{False, "false"}, {True, "true"}};
+
+ for (const auto *Constraint : Constraints) {
+ Constraint->print(OS, &Names);
+ OS << "\n";
+ }
}
const ControlFlowContext *
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
index 4a11c09a44f63b..11bb7da97d52f4 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -107,15 +107,16 @@ static Value *mergeDistinctValues(QualType Type, Value &Val1,
// if (o.has_value())
// x = o.value();
// ```
- 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;
+ 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);
}
// FIXME: Consider destroying `MergedValue` immediately if `ValueModel::merge`
@@ -269,11 +270,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;
}
@@ -587,8 +588,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;
@@ -819,7 +820,7 @@ Value *Environment::createValueUnlessSelfReferential(
// with integers, and so distinguishing them serves no purpose, but could
// prevent convergence.
CreatedValuesCount++;
- return &DACtx->arena().create<IntegerValue>();
+ return &arena().create<IntegerValue>();
}
if (Type->isReferenceType() || Type->isPointerType()) {
@@ -837,9 +838,9 @@ Value *Environment::createValueUnlessSelfReferential(
}
if (Type->isReferenceType())
- return &DACtx->arena().create<ReferenceValue>(PointeeLoc);
+ return &arena().create<ReferenceValue>(PointeeLoc);
else
- return &DACtx->arena().create<PointerValue>(PointeeLoc);
+ return &arena().create<PointerValue>(PointeeLoc);
}
if (Type->isRecordType()) {
@@ -859,7 +860,7 @@ Value *Environment::createValueUnlessSelfReferential(
Visited.erase(FieldType.getCanonicalType());
}
- return &DACtx->arena().create<StructValue>(std::move(FieldValues));
+ return &arena().create<StructValue>(std::move(FieldValues));
}
return nullptr;
@@ -884,12 +885,18 @@ 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) {
- DACtx->addFlowConditionConstraint(*FlowConditionToken, Val);
+ addToFlowCondition(Val.formula());
}
+bool Environment::flowConditionImplies(const Formula &Val) const {
+ return DACtx->flowConditionImplies(FlowConditionToken, Val);
+}
bool Environment::flowConditionImplies(BoolValue &Val) const {
- return DACtx->flowConditionImplies(*FlowConditionToken, Val);
+ return flowConditionImplies(Val.formula());
}
void Environment::dump(raw_ostream &OS) const {
@@ -909,7 +916,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 25225ed6266fb8..f8a049adea5e5d 100644
--- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -16,22 +16,12 @@
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/Value.h"
-#include "llvm/ADT/DenseMap.h"
-#include "llvm/ADT/STLExtras.h"
#include "llvm/ADT/StringRef.h"
-#include "llvm/ADT/StringSet.h"
#include "llvm/Support/ErrorHandling.h"
-#include "llvm/Support/FormatAdapters.h"
-#include "llvm/Support/FormatCommon.h"
-#include "llvm/Support/FormatVariadic.h"
namespace clang {
namespace dataflow {
-using llvm::AlignStyle;
-using llvm::fmt_pad;
-using llvm::formatv;
-
llvm::StringRef debugString(Value::Kind Kind) {
switch (Kind) {
case Value::Kind::Integer:
@@ -46,26 +36,19 @@ llvm::StringRef debugString(Value::Kind Kind) {
return "AtomicBool";
case Value::Kind::TopBool:
return "TopBool";
- 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";
+ case Value::Kind::FormulaBool:
+ return "FormulaBool";
}
llvm_unreachable("Unhandled value kind");
}
-llvm::StringRef debugString(Solver::Result::Assignment Assignment) {
+llvm::raw_ostream &operator<<(llvm::raw_ostream &OS,
+ Solver::Result::Assignment Assignment) {
switch (Assignment) {
case Solver::Result::Assignment::AssignedFalse:
- return "False";
+ return OS << "False";
case Solver::Result::Assignment::AssignedTrue:
- return "True";
+ return OS << "True";
}
llvm_unreachable("Booleans can only be assigned true/false");
}
@@ -82,174 +65,16 @@ llvm::StringRef debugString(Solver::Result::Status Status) {
llvm_unreachable("Unhandled SAT check result status");
}
-namespace {
-
-class DebugStringGenerator {
-public:
- explicit DebugStringGenerator(
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg)
- : Counter(0), AtomNames(std::move(AtomNamesArg)) {
-#ifndef NDEBUG
- llvm::StringSet<> Names;
- for (auto &N : AtomNames) {
- assert(Names.insert(N.second).second &&
- "The same name must not assigned to
diff erent atoms");
- }
-#endif
- }
-
- /// Returns a string representation of a boolean value `B`.
- std::string debugString(const BoolValue &B, size_t Depth = 0) {
- std::string S;
- switch (B.getKind()) {
- case Value::Kind::AtomicBool: {
- S = getAtomName(&cast<AtomicBoolValue>(B));
- break;
- }
- case Value::Kind::TopBool: {
- S = "top";
- break;
- }
- case Value::Kind::Conjunction: {
- auto &C = cast<ConjunctionValue>(B);
- auto L = debugString(C.getLeftSubValue(), Depth + 1);
- auto R = debugString(C.getRightSubValue(), Depth + 1);
- S = formatv("(and\n{0}\n{1})", L, R);
- break;
- }
- case Value::Kind::Disjunction: {
- auto &D = cast<DisjunctionValue>(B);
- auto L = debugString(D.getLeftSubValue(), Depth + 1);
- auto R = debugString(D.getRightSubValue(), Depth + 1);
- S = formatv("(or\n{0}\n{1})", L, R);
- break;
- }
- case Value::Kind::Negation: {
- auto &N = cast<NegationValue>(B);
- S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1));
- break;
- }
- case Value::Kind::Implication: {
- auto &IV = cast<ImplicationValue>(B);
- auto L = debugString(IV.getLeftSubValue(), Depth + 1);
- auto R = debugString(IV.getRightSubValue(), Depth + 1);
- S = formatv("(=>\n{0}\n{1})", L, R);
- break;
- }
- case Value::Kind::Biconditional: {
- auto &BV = cast<BiconditionalValue>(B);
- auto L = debugString(BV.getLeftSubValue(), Depth + 1);
- auto R = debugString(BV.getRightSubValue(), Depth + 1);
- S = formatv("(=\n{0}\n{1})", L, R);
- break;
- }
- default:
- llvm_unreachable("Unhandled value kind");
- }
- auto Indent = Depth * 4;
- return formatv("{0}", fmt_pad(S, Indent, 0));
- }
-
- std::string debugString(const llvm::ArrayRef<BoolValue *> &Constraints) {
- std::string Result;
- for (const BoolValue *S : Constraints) {
- Result += debugString(*S);
- Result += '\n';
- }
- return Result;
- }
-
- /// Returns a string representation of a set of boolean `Constraints` and the
- /// `Result` of satisfiability checking on the `Constraints`.
- std::string debugString(ArrayRef<BoolValue *> &Constraints,
- const Solver::Result &Result) {
- auto Template = R"(
-Constraints
-------------
-{0:$[
-
-]}
-------------
-{1}.
-{2}
-)";
-
- std::vector<std::string> ConstraintsStrings;
- ConstraintsStrings.reserve(Constraints.size());
- for (auto &Constraint : Constraints) {
- ConstraintsStrings.push_back(debugString(*Constraint));
- }
-
- auto StatusString = clang::dataflow::debugString(Result.getStatus());
- auto Solution = Result.getSolution();
- auto SolutionString = Solution ? "\n" + debugString(*Solution) : "";
-
- return formatv(
- Template,
- llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()),
- StatusString, SolutionString);
- }
-
-private:
- /// Returns a string representation of a truth assignment to atom booleans.
- std::string debugString(
- const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
- &AtomAssignments) {
- size_t MaxNameLength = 0;
- for (auto &AtomName : AtomNames) {
- MaxNameLength = std::max(MaxNameLength, AtomName.second.size());
- }
-
- std::vector<std::string> Lines;
- for (auto &AtomAssignment : AtomAssignments) {
- auto Line = formatv("{0} = {1}",
- fmt_align(getAtomName(AtomAssignment.first),
- AlignStyle::Left, MaxNameLength),
- clang::dataflow::debugString(AtomAssignment.second));
- Lines.push_back(Line);
- }
- llvm::sort(Lines);
-
- return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end()));
+llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Solver::Result &R) {
+ OS << debugString(R.getStatus()) << "\n";
+ if (auto Solution = R.getSolution()) {
+ std::vector<std::pair<Atom, Solver::Result::Assignment>> Sorted = {
+ Solution->begin(), Solution->end()};
+ llvm::sort(Sorted);
+ for (const auto &Entry : Sorted)
+ OS << Entry.first << " = " << Entry.second << "\n";
}
-
- /// Returns the name assigned to `Atom`, either user-specified or created by
- /// default rules (B0, B1, ...).
- std::string getAtomName(const AtomicBoolValue *Atom) {
- auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter));
- if (Entry.second) {
- Counter++;
- }
- return Entry.first->second;
- }
-
- // Keep track of number of atoms without a user-specified name, used to assign
- // non-repeating default names to such atoms.
- size_t Counter;
-
- // Keep track of names assigned to atoms.
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames;
-};
-
-} // namespace
-
-std::string
-debugString(const BoolValue &B,
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
- return DebugStringGenerator(std::move(AtomNames)).debugString(B);
-}
-
-std::string
-debugString(llvm::ArrayRef<BoolValue *> Constraints,
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
- return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints);
-}
-
-std::string
-debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
- llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
- return DebugStringGenerator(std::move(AtomNames))
- .debugString(Constraints, Result);
+ return OS;
}
} // namespace dataflow
diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp
new file mode 100644
index 00000000000000..504ad2fb7938af
--- /dev/null
+++ b/clang/lib/Analysis/FlowSensitive/Formula.cpp
@@ -0,0 +1,82 @@
+//===- Formula.cpp ----------------------------------------------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "clang/Basic/LLVM.h"
+#include "llvm/ADT/STLExtras.h"
+#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Allocator.h"
+#include "llvm/Support/ErrorHandling.h"
+#include <cassert>
+
+namespace clang::dataflow {
+
+Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K,
+ ArrayRef<const Formula *> Operands, unsigned Value) {
+ assert(Operands.size() == numOperands(K));
+ if (Value != 0) // Currently, formulas have values or operands, not both.
+ assert(numOperands(K) == 0);
+ void *Mem = Alloc.Allocate(sizeof(Formula) +
+ Operands.size() * sizeof(Operands.front()),
+ alignof(Formula));
+ Formula *Result = new (Mem) Formula();
+ Result->FormulaKind = K;
+ Result->Value = Value;
+ // Operands are stored as `const Formula *`s after the formula itself.
+ // We don't need to construct an object as pointers are trivial types.
+ // Formula is alignas(const Formula *), so alignment is satisfied.
+ llvm::copy(Operands, reinterpret_cast<const Formula **>(Result + 1));
+ return *Result;
+}
+
+static llvm::StringLiteral sigil(Formula::Kind K) {
+ switch (K) {
+ case Formula::AtomRef:
+ return "";
+ case Formula::Not:
+ return "!";
+ case Formula::And:
+ return " & ";
+ case Formula::Or:
+ return " | ";
+ case Formula::Implies:
+ return " => ";
+ case Formula::Equal:
+ return " = ";
+ }
+ llvm_unreachable("unhandled formula kind");
+}
+
+void Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const {
+ if (Names && kind() == AtomRef)
+ if (auto It = Names->find(getAtom()); It != Names->end()) {
+ OS << It->second;
+ return;
+ }
+
+ switch (numOperands(kind())) {
+ case 0:
+ OS << getAtom();
+ break;
+ case 1:
+ OS << sigil(kind());
+ operands()[0]->print(OS, Names);
+ break;
+ case 2:
+ OS << '(';
+ operands()[0]->print(OS, Names);
+ OS << sigil(kind());
+ operands()[1]->print(OS, Names);
+ OS << ')';
+ break;
+ default:
+ llvm_unreachable("unhandled formula arity");
+ }
+}
+
+} // namespace clang::dataflow
\ No newline at end of file
diff --git a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
index 14293a3043f988..0c4e838e667be1 100644
--- a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
+++ b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp
@@ -97,6 +97,7 @@ 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(
@@ -111,35 +112,6 @@ 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())
@@ -149,10 +121,12 @@ 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("truth", Env.flowConditionImplies(*B) ? "true"
- : Env.flowConditionImplies(Env.makeNot(*B))
- ? "false"
- : "unknown");
+ 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");
}
}
void dump(const StorageLocation &L) {
diff --git a/clang/lib/Analysis/FlowSensitive/Transfer.cpp b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
index d69e0f5a5e1030..ac971f69150f1e 100644
--- a/clang/lib/Analysis/FlowSensitive/Transfer.cpp
+++ b/clang/lib/Analysis/FlowSensitive/Transfer.cpp
@@ -62,64 +62,12 @@ 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) {
- 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);
+ if (auto *Top = llvm::dyn_cast<TopBoolValue>(&V)) {
+ auto &A = Env.getDataflowAnalysisContext().arena();
+ return A.makeBoolValue(A.makeAtomRef(Top->getAtom()));
}
- llvm_unreachable("All reachable cases in switch return");
+ return V;
}
// 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 db2e1d694457bf..037886d09c4f7d 100644
--- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -17,8 +17,8 @@
#include <queue>
#include <vector>
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/DenseMap.h"
@@ -79,7 +79,7 @@ using ClauseID = uint32_t;
static constexpr ClauseID NullClause = 0;
/// A boolean formula in conjunctive normal form.
-struct BooleanFormula {
+struct CNFFormula {
/// `LargestVar` is equal to the largest positive integer that represents a
/// variable in the formula.
const Variable LargestVar;
@@ -121,12 +121,12 @@ struct BooleanFormula {
/// clauses in the formula start from the element at index 1.
std::vector<ClauseID> NextWatched;
- /// Stores the variable identifier and value location for atomic booleans in
- /// the formula.
- llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
+ /// Stores the variable identifier and Atom for atomic booleans in the
+ /// formula.
+ llvm::DenseMap<Variable, Atom> Atomics;
- explicit BooleanFormula(Variable LargestVar,
- llvm::DenseMap<Variable, AtomicBoolValue *> Atomics)
+ explicit CNFFormula(Variable LargestVar,
+ llvm::DenseMap<Variable, Atom> Atomics)
: LargestVar(LargestVar), Atomics(std::move(Atomics)) {
Clauses.push_back(0);
ClauseStarts.push_back(0);
@@ -144,8 +144,8 @@ struct BooleanFormula {
///
/// All literals in the input that are not `NullLit` must be distinct.
void addClause(Literal L1, Literal L2 = NullLit, Literal L3 = NullLit) {
- // The literals are guaranteed to be distinct from properties of BoolValue
- // and the construction in `buildBooleanFormula`.
+ // The literals are guaranteed to be distinct from properties of Formula
+ // and the construction in `buildCNF`.
assert(L1 != NullLit && L1 != L2 && L1 != L3 &&
(L2 != L3 || L2 == NullLit));
@@ -178,98 +178,59 @@ struct BooleanFormula {
/// Converts the conjunction of `Vals` into a formula in conjunctive normal
/// form where each clause has at least one and at most three literals.
-BooleanFormula buildBooleanFormula(const llvm::ArrayRef<BoolValue *> &Vals) {
+CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) {
// The general strategy of the algorithm implemented below is to map each
// of the sub-values in `Vals` to a unique variable and use these variables in
// the resulting CNF expression to avoid exponential blow up. The number of
// literals in the resulting formula is guaranteed to be linear in the number
- // of sub-values in `Vals`.
+ // of sub-formulas in `Vals`.
- // Map each sub-value in `Vals` to a unique variable.
- llvm::DenseMap<BoolValue *, Variable> SubValsToVar;
- // Store variable identifiers and value location of atomic booleans.
- llvm::DenseMap<Variable, AtomicBoolValue *> Atomics;
+ // Map each sub-formula in `Vals` to a unique variable.
+ llvm::DenseMap<const Formula *, Variable> SubValsToVar;
+ // Store variable identifiers and Atom of atomic booleans.
+ llvm::DenseMap<Variable, Atom> Atomics;
Variable NextVar = 1;
{
- std::queue<BoolValue *> UnprocessedSubVals;
- for (BoolValue *Val : Vals)
+ std::queue<const Formula *> UnprocessedSubVals;
+ for (const Formula *Val : Vals)
UnprocessedSubVals.push(Val);
while (!UnprocessedSubVals.empty()) {
Variable Var = NextVar;
- BoolValue *Val = UnprocessedSubVals.front();
+ const Formula *Val = UnprocessedSubVals.front();
UnprocessedSubVals.pop();
if (!SubValsToVar.try_emplace(Val, Var).second)
continue;
++NextVar;
- // Visit the sub-values of `Val`.
- switch (Val->getKind()) {
- case Value::Kind::Conjunction: {
- auto *C = cast<ConjunctionValue>(Val);
- UnprocessedSubVals.push(&C->getLeftSubValue());
- UnprocessedSubVals.push(&C->getRightSubValue());
- break;
- }
- case Value::Kind::Disjunction: {
- auto *D = cast<DisjunctionValue>(Val);
- UnprocessedSubVals.push(&D->getLeftSubValue());
- UnprocessedSubVals.push(&D->getRightSubValue());
- break;
- }
- case Value::Kind::Negation: {
- auto *N = cast<NegationValue>(Val);
- UnprocessedSubVals.push(&N->getSubVal());
- break;
- }
- case Value::Kind::Implication: {
- auto *I = cast<ImplicationValue>(Val);
- UnprocessedSubVals.push(&I->getLeftSubValue());
- UnprocessedSubVals.push(&I->getRightSubValue());
- break;
- }
- case Value::Kind::Biconditional: {
- auto *B = cast<BiconditionalValue>(Val);
- UnprocessedSubVals.push(&B->getLeftSubValue());
- UnprocessedSubVals.push(&B->getRightSubValue());
- break;
- }
- case Value::Kind::TopBool:
- // Nothing more to do. This `TopBool` instance has already been mapped
- // to a fresh solver variable (`NextVar`, above) and is thereafter
- // anonymous. The solver never sees `Top`.
- break;
- case Value::Kind::AtomicBool: {
- Atomics[Var] = cast<AtomicBoolValue>(Val);
- break;
- }
- default:
- llvm_unreachable("buildBooleanFormula: unhandled value kind");
- }
+ for (const Formula *F : Val->operands())
+ UnprocessedSubVals.push(F);
+ if (Val->kind() == Formula::AtomRef)
+ Atomics[Var] = Val->getAtom();
}
}
- auto GetVar = [&SubValsToVar](const BoolValue *Val) {
+ auto GetVar = [&SubValsToVar](const Formula *Val) {
auto ValIt = SubValsToVar.find(Val);
assert(ValIt != SubValsToVar.end());
return ValIt->second;
};
- BooleanFormula Formula(NextVar - 1, std::move(Atomics));
+ CNFFormula CNF(NextVar - 1, std::move(Atomics));
std::vector<bool> ProcessedSubVals(NextVar, false);
- // Add a conjunct for each variable that represents a top-level conjunction
- // value in `Vals`.
- for (BoolValue *Val : Vals)
- Formula.addClause(posLit(GetVar(Val)));
+ // Add a conjunct for each variable that represents a top-level formula in
+ // `Vals`.
+ for (const Formula *Val : Vals)
+ CNF.addClause(posLit(GetVar(Val)));
// Add conjuncts that represent the mapping between newly-created variables
- // and their corresponding sub-values.
- std::queue<BoolValue *> UnprocessedSubVals;
- for (BoolValue *Val : Vals)
+ // and their corresponding sub-formulas.
+ std::queue<const Formula *> UnprocessedSubVals;
+ for (const Formula *Val : Vals)
UnprocessedSubVals.push(Val);
while (!UnprocessedSubVals.empty()) {
- const BoolValue *Val = UnprocessedSubVals.front();
+ const Formula *Val = UnprocessedSubVals.front();
UnprocessedSubVals.pop();
const Variable Var = GetVar(Val);
@@ -277,117 +238,107 @@ BooleanFormula buildBooleanFormula(const llvm::ArrayRef<BoolValue *> &Vals) {
continue;
ProcessedSubVals[Var] = true;
- if (auto *C = dyn_cast<ConjunctionValue>(Val)) {
- const Variable LeftSubVar = GetVar(&C->getLeftSubValue());
- const Variable RightSubVar = GetVar(&C->getRightSubValue());
+ switch (Val->kind()) {
+ case Formula::AtomRef:
+ break;
+ case Formula::And: {
+ const Variable LHS = GetVar(Val->operands()[0]);
+ const Variable RHS = GetVar(Val->operands()[1]);
- if (LeftSubVar == RightSubVar) {
+ if (LHS == RHS) {
// `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is
// already in conjunctive normal form. Below we add each of the
// conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar));
-
- // Visit a sub-value of `Val` (pick any, they are identical).
- UnprocessedSubVals.push(&C->getLeftSubValue());
+ CNF.addClause(negLit(Var), posLit(LHS));
+ CNF.addClause(posLit(Var), negLit(LHS));
} else {
// `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)`
// which is already in conjunctive normal form. Below we add each of the
// conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar));
- Formula.addClause(negLit(Var), posLit(RightSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&C->getLeftSubValue());
- UnprocessedSubVals.push(&C->getRightSubValue());
+ CNF.addClause(negLit(Var), posLit(LHS));
+ CNF.addClause(negLit(Var), posLit(RHS));
+ CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
}
- } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) {
- const Variable LeftSubVar = GetVar(&D->getLeftSubValue());
- const Variable RightSubVar = GetVar(&D->getRightSubValue());
+ break;
+ }
+ case Formula::Or: {
+ const Variable LHS = GetVar(Val->operands()[0]);
+ const Variable RHS = GetVar(Val->operands()[1]);
- if (LeftSubVar == RightSubVar) {
+ if (LHS == RHS) {
// `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` which is
// already in conjunctive normal form. Below we add each of the
// conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar));
-
- // Visit a sub-value of `Val` (pick any, they are identical).
- UnprocessedSubVals.push(&D->getLeftSubValue());
+ CNF.addClause(negLit(Var), posLit(LHS));
+ CNF.addClause(posLit(Var), negLit(LHS));
} else {
- // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)`
- // which is already in conjunctive normal form. Below we add each of the
- // conjuncts of the latter expression to the result.
- Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar));
- Formula.addClause(posLit(Var), negLit(RightSubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&D->getLeftSubValue());
- UnprocessedSubVals.push(&D->getRightSubValue());
+ // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v
+ // !B)` which is already in conjunctive normal form. Below we add each
+ // of the conjuncts of the latter expression to the result.
+ CNF.addClause(negLit(Var), posLit(LHS), posLit(RHS));
+ CNF.addClause(posLit(Var), negLit(LHS));
+ CNF.addClause(posLit(Var), negLit(RHS));
}
- } else if (auto *N = dyn_cast<NegationValue>(Val)) {
- const Variable SubVar = GetVar(&N->getSubVal());
-
- // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is already in
- // conjunctive normal form. Below we add each of the conjuncts of the
- // latter expression to the result.
- Formula.addClause(negLit(Var), negLit(SubVar));
- Formula.addClause(posLit(Var), posLit(SubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&N->getSubVal());
- } else if (auto *I = dyn_cast<ImplicationValue>(Val)) {
- const Variable LeftSubVar = GetVar(&I->getLeftSubValue());
- const Variable RightSubVar = GetVar(&I->getRightSubValue());
+ break;
+ }
+ case Formula::Not: {
+ const Variable Operand = GetVar(Val->operands()[0]);
+
+ // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is
+ // already in conjunctive normal form. Below we add each of the
+ // conjuncts of the latter expression to the result.
+ CNF.addClause(negLit(Var), negLit(Operand));
+ CNF.addClause(posLit(Var), posLit(Operand));
+ break;
+ }
+ case Formula::Implies: {
+ const Variable LHS = GetVar(Val->operands()[0]);
+ const Variable RHS = GetVar(Val->operands()[1]);
// `X <=> (A => B)` is equivalent to
// `(X v A) ^ (X v !B) ^ (!X v !A v B)` which is already in
- // conjunctive normal form. Below we add each of the conjuncts of the
- // latter expression to the result.
- Formula.addClause(posLit(Var), posLit(LeftSubVar));
- Formula.addClause(posLit(Var), negLit(RightSubVar));
- Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&I->getLeftSubValue());
- UnprocessedSubVals.push(&I->getRightSubValue());
- } else if (auto *B = dyn_cast<BiconditionalValue>(Val)) {
- const Variable LeftSubVar = GetVar(&B->getLeftSubValue());
- const Variable RightSubVar = GetVar(&B->getRightSubValue());
-
- if (LeftSubVar == RightSubVar) {
+ // conjunctive normal form. Below we add each of the conjuncts of
+ // the latter expression to the result.
+ CNF.addClause(posLit(Var), posLit(LHS));
+ CNF.addClause(posLit(Var), negLit(RHS));
+ CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS));
+ break;
+ }
+ case Formula::Equal: {
+ const Variable LHS = GetVar(Val->operands()[0]);
+ const Variable RHS = GetVar(Val->operands()[1]);
+
+ if (LHS == RHS) {
// `X <=> (A <=> A)` is equvalent to `X` which is already in
// conjunctive normal form. Below we add each of the conjuncts of the
// latter expression to the result.
- Formula.addClause(posLit(Var));
+ CNF.addClause(posLit(Var));
// No need to visit the sub-values of `Val`.
- } else {
- // `X <=> (A <=> B)` is equivalent to
- // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which is
- // already in conjunctive normal form. Below we add each of the conjuncts
- // of the latter expression to the result.
- Formula.addClause(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar));
- Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar));
- Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar));
- Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar));
-
- // Visit the sub-values of `Val`.
- UnprocessedSubVals.push(&B->getLeftSubValue());
- UnprocessedSubVals.push(&B->getRightSubValue());
+ continue;
}
+ // `X <=> (A <=> B)` is equivalent to
+ // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which
+ // is already in conjunctive normal form. Below we add each of the
+ // conjuncts of the latter expression to the result.
+ CNF.addClause(posLit(Var), posLit(LHS), posLit(RHS));
+ CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS));
+ CNF.addClause(negLit(Var), posLit(LHS), negLit(RHS));
+ CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS));
+ break;
+ }
}
+ for (const Formula *Child : Val->operands())
+ UnprocessedSubVals.push(Child);
}
- return Formula;
+ return CNF;
}
class WatchedLiteralsSolverImpl {
/// A boolean formula in conjunctive normal form that the solver will attempt
/// to prove satisfiable. The formula will be modified in the process.
- BooleanFormula Formula;
+ CNFFormula CNF;
/// The search for a satisfying assignment of the variables in `Formula` will
/// proceed in levels, starting from 1 and going up to `Formula.LargestVar`
@@ -439,9 +390,10 @@ class WatchedLiteralsSolverImpl {
std::vector<Variable> ActiveVars;
public:
- explicit WatchedLiteralsSolverImpl(const llvm::ArrayRef<BoolValue *> &Vals)
- : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1),
- LevelStates(Formula.LargestVar + 1) {
+ explicit WatchedLiteralsSolverImpl(
+ const llvm::ArrayRef<const Formula *> &Vals)
+ : CNF(buildCNF(Vals)), LevelVars(CNF.LargestVar + 1),
+ LevelStates(CNF.LargestVar + 1) {
assert(!Vals.empty());
// Initialize the state at the root level to a decision so that in
@@ -450,10 +402,10 @@ class WatchedLiteralsSolverImpl {
LevelStates[0] = State::Decision;
// Initialize all variables as unassigned.
- VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned);
+ VarAssignments.resize(CNF.LargestVar + 1, Assignment::Unassigned);
// Initialize the active variables.
- for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {
+ for (Variable Var = CNF.LargestVar; Var != NullVar; --Var) {
if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
ActiveVars.push_back(Var);
}
@@ -474,7 +426,7 @@ class WatchedLiteralsSolverImpl {
// 3. Unassigned variables that form watched literals are active.
// FIXME: Consider replacing these with test cases that fail if the any
// of the invariants is broken. That might not be easy due to the
- // transformations performed by `buildBooleanFormula`.
+ // transformations performed by `buildCNF`.
assert(activeVarsAreUnassigned());
assert(activeVarsFormWatchedLiterals());
assert(unassignedVarsFormingWatchedLiteralsAreActive());
@@ -555,12 +507,10 @@ class WatchedLiteralsSolverImpl {
}
private:
- /// Returns a satisfying truth assignment to the atomic values in the boolean
- /// formula.
- llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
- buildSolution() {
- llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> Solution;
- for (auto &Atomic : Formula.Atomics) {
+ /// Returns a satisfying truth assignment to the atoms in the boolean formula.
+ llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() {
+ llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;
+ for (auto &Atomic : CNF.Atomics) {
// A variable may have a definite true/false assignment, or it may be
// unassigned indicating its truth value does not affect the result of
// the formula. Unassigned variables are assigned to true as a default.
@@ -596,24 +546,24 @@ class WatchedLiteralsSolverImpl {
const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
? negLit(Var)
: posLit(Var);
- ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit];
- Formula.WatchedHead[FalseLit] = NullClause;
+ ClauseID FalseLitWatcher = CNF.WatchedHead[FalseLit];
+ CNF.WatchedHead[FalseLit] = NullClause;
while (FalseLitWatcher != NullClause) {
- const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher];
+ const ClauseID NextFalseLitWatcher = CNF.NextWatched[FalseLitWatcher];
// Pick the first non-false literal as the new watched literal.
- const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher];
+ const size_t FalseLitWatcherStart = CNF.ClauseStarts[FalseLitWatcher];
size_t NewWatchedLitIdx = FalseLitWatcherStart + 1;
- while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx]))
+ while (isCurrentlyFalse(CNF.Clauses[NewWatchedLitIdx]))
++NewWatchedLitIdx;
- const Literal NewWatchedLit = Formula.Clauses[NewWatchedLitIdx];
+ const Literal NewWatchedLit = CNF.Clauses[NewWatchedLitIdx];
const Variable NewWatchedLitVar = var(NewWatchedLit);
// Swap the old watched literal for the new one in `FalseLitWatcher` to
// maintain the invariant that the watched literal is at the beginning of
// the clause.
- Formula.Clauses[NewWatchedLitIdx] = FalseLit;
- Formula.Clauses[FalseLitWatcherStart] = NewWatchedLit;
+ CNF.Clauses[NewWatchedLitIdx] = FalseLit;
+ CNF.Clauses[FalseLitWatcherStart] = NewWatchedLit;
// If the new watched literal isn't watched by any other clause and its
// variable isn't assigned we need to add it to the active variables.
@@ -621,8 +571,8 @@ class WatchedLiteralsSolverImpl {
VarAssignments[NewWatchedLitVar] == Assignment::Unassigned)
ActiveVars.push_back(NewWatchedLitVar);
- Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit];
- Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher;
+ CNF.NextWatched[FalseLitWatcher] = CNF.WatchedHead[NewWatchedLit];
+ CNF.WatchedHead[NewWatchedLit] = FalseLitWatcher;
// Go to the next clause that watches `FalseLit`.
FalseLitWatcher = NextFalseLitWatcher;
@@ -632,16 +582,15 @@ class WatchedLiteralsSolverImpl {
/// Returns true if and only if one of the clauses that watch `Lit` is a unit
/// clause.
bool watchedByUnitClause(Literal Lit) const {
- for (ClauseID LitWatcher = Formula.WatchedHead[Lit];
- LitWatcher != NullClause;
- LitWatcher = Formula.NextWatched[LitWatcher]) {
- llvm::ArrayRef<Literal> Clause = Formula.clauseLiterals(LitWatcher);
+ for (ClauseID LitWatcher = CNF.WatchedHead[Lit]; LitWatcher != NullClause;
+ LitWatcher = CNF.NextWatched[LitWatcher]) {
+ llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);
// Assert the invariant that the watched literal is always the first one
// in the clause.
// FIXME: Consider replacing this with a test case that fails if the
// invariant is broken by `updateWatchedLiterals`. That might not be easy
- // due to the transformations performed by `buildBooleanFormula`.
+ // due to the transformations performed by `buildCNF`.
assert(Clause.front() == Lit);
if (isUnit(Clause))
@@ -665,7 +614,7 @@ class WatchedLiteralsSolverImpl {
/// Returns true if and only if `Lit` is watched by a clause in `Formula`.
bool isWatched(Literal Lit) const {
- return Formula.WatchedHead[Lit] != NullClause;
+ return CNF.WatchedHead[Lit] != NullClause;
}
/// Returns an assignment for an unassigned variable.
@@ -678,8 +627,8 @@ class WatchedLiteralsSolverImpl {
/// Returns a set of all watched literals.
llvm::DenseSet<Literal> watchedLiterals() const {
llvm::DenseSet<Literal> WatchedLiterals;
- for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) {
- if (Formula.WatchedHead[Lit] == NullClause)
+ for (Literal Lit = 2; Lit < CNF.WatchedHead.size(); Lit++) {
+ if (CNF.WatchedHead[Lit] == NullClause)
continue;
WatchedLiterals.insert(Lit);
}
@@ -719,7 +668,8 @@ class WatchedLiteralsSolverImpl {
}
};
-Solver::Result WatchedLiteralsSolver::solve(llvm::ArrayRef<BoolValue *> Vals) {
+Solver::Result
+WatchedLiteralsSolver::solve(llvm::ArrayRef<const Formula *> Vals) {
if (Vals.empty())
return Solver::Result::Satisfiable({{}});
auto [Res, Iterations] =
diff --git a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
index 407abf58529a50..0f8552a58787cb 100644
--- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
@@ -7,6 +7,7 @@
//===----------------------------------------------------------------------===//
#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "llvm/Support/ScopedPrinter.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -19,26 +20,26 @@ class ArenaTest : public ::testing::Test {
};
TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomValue();
+ auto &Y = A.makeAtomValue();
EXPECT_NE(&X, &Y);
}
TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) {
- auto &X = A.create<TopBoolValue>();
- auto &Y = A.create<TopBoolValue>();
+ auto &X = A.makeTopValue();
+ auto &Y = A.makeTopValue();
EXPECT_NE(&X, &Y);
}
TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
- auto &X = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
auto &XAndX = A.makeAnd(X, X);
EXPECT_EQ(&XAndX, &X);
}
TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
+ auto &Y = A.makeAtomRef(A.makeAtom());
auto &XAndY1 = A.makeAnd(X, Y);
auto &XAndY2 = A.makeAnd(X, Y);
EXPECT_EQ(&XAndY1, &XAndY2);
@@ -46,20 +47,20 @@ TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
auto &YAndX = A.makeAnd(Y, X);
EXPECT_EQ(&XAndY1, &YAndX);
- auto &Z = A.create<AtomicBoolValue>();
+ auto &Z = A.makeAtomRef(A.makeAtom());
auto &XAndZ = A.makeAnd(X, Z);
EXPECT_NE(&XAndY1, &XAndZ);
}
TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
- auto &X = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
auto &XOrX = A.makeOr(X, X);
EXPECT_EQ(&XOrX, &X);
}
TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
+ auto &Y = A.makeAtomRef(A.makeAtom());
auto &XOrY1 = A.makeOr(X, Y);
auto &XOrY2 = A.makeOr(X, Y);
EXPECT_EQ(&XOrY1, &XOrY2);
@@ -67,31 +68,30 @@ TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
auto &YOrX = A.makeOr(Y, X);
EXPECT_EQ(&XOrY1, &YOrX);
- auto &Z = A.create<AtomicBoolValue>();
+ auto &Z = A.makeAtomRef(A.makeAtom());
auto &XOrZ = A.makeOr(X, Z);
EXPECT_NE(&XOrY1, &XOrZ);
}
TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
- auto &X = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
auto &NotX1 = A.makeNot(X);
auto &NotX2 = A.makeNot(X);
EXPECT_EQ(&NotX1, &NotX2);
-
- auto &Y = A.create<AtomicBoolValue>();
+ auto &Y = A.makeAtomRef(A.makeAtom());
auto &NotY = A.makeNot(Y);
EXPECT_NE(&NotX1, &NotY);
}
TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) {
- auto &X = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
auto &XImpliesX = A.makeImplies(X, X);
EXPECT_EQ(&XImpliesX, &A.makeLiteral(true));
}
TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
+ auto &Y = A.makeAtomRef(A.makeAtom());
auto &XImpliesY1 = A.makeImplies(X, Y);
auto &XImpliesY2 = A.makeImplies(X, Y);
EXPECT_EQ(&XImpliesY1, &XImpliesY2);
@@ -99,20 +99,20 @@ TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
auto &YImpliesX = A.makeImplies(Y, X);
EXPECT_NE(&XImpliesY1, &YImpliesX);
- auto &Z = A.create<AtomicBoolValue>();
+ auto &Z = A.makeAtomRef(A.makeAtom());
auto &XImpliesZ = A.makeImplies(X, Z);
EXPECT_NE(&XImpliesY1, &XImpliesZ);
}
TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
- auto &X = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
auto &XIffX = A.makeEquals(X, X);
EXPECT_EQ(&XIffX, &A.makeLiteral(true));
}
TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
+ auto &Y = A.makeAtomRef(A.makeAtom());
auto &XIffY1 = A.makeEquals(X, Y);
auto &XIffY2 = A.makeEquals(X, Y);
EXPECT_EQ(&XIffY1, &XIffY2);
@@ -120,10 +120,22 @@ TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
auto &YIffX = A.makeEquals(Y, X);
EXPECT_EQ(&XIffY1, &YIffX);
- auto &Z = A.create<AtomicBoolValue>();
+ auto &Z = A.makeAtomRef(A.makeAtom());
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);
+}
+
} // namespace
} // namespace clang::dataflow
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
index bb76648abdc05c..f6e8b30d898e89 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.create<TopBoolValue>();
- auto &Y = A.create<TopBoolValue>();
- EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
+ auto &X = A.makeTopValue();
+ auto &Y = A.makeTopValue();
+ EXPECT_FALSE(Context.equivalentFormulas(X.formula(), Y.formula()));
}
TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) {
- auto &FC = A.makeFlowConditionToken();
- auto &C = A.create<AtomicBoolValue>();
+ Atom FC = A.makeFlowConditionToken();
+ auto &C = A.makeAtomRef(A.makeAtom());
EXPECT_FALSE(Context.flowConditionImplies(FC, C));
}
TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) {
- auto &FC = A.makeFlowConditionToken();
- auto &C = A.create<AtomicBoolValue>();
+ Atom FC = A.makeFlowConditionToken();
+ auto &C = A.makeAtomRef(A.makeAtom());
Context.addFlowConditionConstraint(FC, C);
EXPECT_TRUE(Context.flowConditionImplies(FC, C));
}
TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) {
- auto &FC1 = A.makeFlowConditionToken();
- auto &C1 = A.create<AtomicBoolValue>();
+ Atom FC1 = A.makeFlowConditionToken();
+ auto &C1 = A.makeAtomRef(A.makeAtom());
Context.addFlowConditionConstraint(FC1, C1);
// Forked flow condition inherits the constraints of its parent flow
// condition.
- auto &FC2 = Context.forkFlowCondition(FC1);
+ Atom 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.create<AtomicBoolValue>();
+ auto &C2 = A.makeAtomRef(A.makeAtom());
Context.addFlowConditionConstraint(FC2, C2);
EXPECT_TRUE(Context.flowConditionImplies(FC2, C2));
EXPECT_FALSE(Context.flowConditionImplies(FC1, C2));
}
TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
- auto &C1 = A.create<AtomicBoolValue>();
- auto &C2 = A.create<AtomicBoolValue>();
- auto &C3 = A.create<AtomicBoolValue>();
+ auto &C1 = A.makeAtomRef(A.makeAtom());
+ auto &C2 = A.makeAtomRef(A.makeAtom());
+ auto &C3 = A.makeAtomRef(A.makeAtom());
- auto &FC1 = A.makeFlowConditionToken();
+ Atom FC1 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC1, C1);
Context.addFlowConditionConstraint(FC1, C3);
- auto &FC2 = A.makeFlowConditionToken();
+ Atom FC2 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC2, C2);
Context.addFlowConditionConstraint(FC2, C3);
- auto &FC3 = Context.joinFlowConditions(FC1, FC2);
+ Atom 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.
- auto &FC1 = A.makeFlowConditionToken();
+ Atom FC1 = A.makeFlowConditionToken();
EXPECT_TRUE(Context.flowConditionIsTautology(FC1));
// Literal `true` is always true.
- auto &FC2 = A.makeFlowConditionToken();
+ Atom FC2 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC2, A.makeLiteral(true));
EXPECT_TRUE(Context.flowConditionIsTautology(FC2));
// Literal `false` is never true.
- auto &FC3 = A.makeFlowConditionToken();
+ Atom 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.create<AtomicBoolValue>();
- auto &FC4 = A.makeFlowConditionToken();
+ auto &C1 = A.makeAtomRef(A.makeAtom());
+ Atom FC4 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC4, C1);
EXPECT_FALSE(Context.flowConditionIsTautology(FC4));
// ... but we can prove A || !A is true.
- auto &FC5 = A.makeFlowConditionToken();
+ Atom FC5 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC5, A.makeOr(C1, A.makeNot(C1)));
EXPECT_TRUE(Context.flowConditionIsTautology(FC5));
}
TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
- auto &Z = A.create<AtomicBoolValue>();
+ auto &X = A.makeAtomRef(A.makeAtom());
+ auto &Y = A.makeAtomRef(A.makeAtom());
+ auto &Z = A.makeAtomRef(A.makeAtom());
auto &True = A.makeLiteral(true);
auto &False = A.makeLiteral(false);
// X == X
- EXPECT_TRUE(Context.equivalentBoolValues(X, X));
+ EXPECT_TRUE(Context.equivalentFormulas(X, X));
// X != Y
- EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
+ EXPECT_FALSE(Context.equivalentFormulas(X, Y));
// !X != X
- EXPECT_FALSE(Context.equivalentBoolValues(A.makeNot(X), X));
+ EXPECT_FALSE(Context.equivalentFormulas(A.makeNot(X), X));
// !(!X) = X
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeNot(A.makeNot(X)), X));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeNot(A.makeNot(X)), X));
// (X || X) == X
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, X), X));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, X), X));
// (X || Y) != X
- EXPECT_FALSE(Context.equivalentBoolValues(A.makeOr(X, Y), X));
+ EXPECT_FALSE(Context.equivalentFormulas(A.makeOr(X, Y), X));
// (X || True) == True
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, True), True));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, True), True));
// (X || False) == X
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, False), X));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, False), X));
// (X && X) == X
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, X), X));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, X), X));
// (X && Y) != X
- EXPECT_FALSE(Context.equivalentBoolValues(A.makeAnd(X, Y), X));
+ EXPECT_FALSE(Context.equivalentFormulas(A.makeAnd(X, Y), X));
// (X && True) == X
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, True), X));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, True), X));
// (X && False) == False
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, False), False));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, False), False));
// (X || Y) == (Y || X)
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, Y), A.makeOr(Y, X)));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, Y), A.makeOr(Y, X)));
// (X && Y) == (Y && X)
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, Y), A.makeAnd(Y, X)));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, Y), A.makeAnd(Y, X)));
// ((X || Y) || Z) == (X || (Y || Z))
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(A.makeOr(X, Y), Z),
- A.makeOr(X, A.makeOr(Y, Z))));
+ EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(A.makeOr(X, Y), Z),
+ A.makeOr(X, A.makeOr(Y, Z))));
// ((X && Y) && Z) == (X && (Y && Z))
- EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(A.makeAnd(X, Y), Z),
- A.makeAnd(X, A.makeAnd(Y, Z))));
+ EXPECT_TRUE(Context.equivalentFormulas(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 10fcd204c9ab07..22bf8cadd1116f 100644
--- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -8,8 +8,9 @@
#include "clang/Analysis/FlowSensitive/DebugSupport.h"
#include "TestingSupport.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
-#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
+#include "llvm/Support/ScopedPrinter.h"
+#include "llvm/Support/raw_ostream.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -22,429 +23,88 @@ using test::ConstraintContext;
using testing::StrEq;
TEST(BoolValueDebugStringTest, AtomicBoolean) {
- // B0
ConstraintContext Ctx;
auto B = Ctx.atom();
- auto Expected = R"(B0)";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, Top) {
- ConstraintContext Ctx;
- auto B = Ctx.top();
-
- auto Expected = R"(top)";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "V0";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Negation) {
- // !B0
ConstraintContext Ctx;
auto B = Ctx.neg(Ctx.atom());
- auto Expected = R"((not
- B0))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "!V0";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, Conjunction) {
- // B0 ^ B1
ConstraintContext Ctx;
- auto B = Ctx.conj(Ctx.atom(), Ctx.atom());
-
- auto Expected = R"((and
- B0
- B1))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto *V0 = Ctx.atom();
+ auto *V1 = Ctx.atom();
+ EXPECT_EQ("(V0 & V1)", llvm::to_string(*Ctx.conj(V0, V1)));
}
TEST(BoolValueDebugStringTest, Disjunction) {
- // B0 v B1
ConstraintContext Ctx;
- auto B = Ctx.disj(Ctx.atom(), Ctx.atom());
-
- auto Expected = R"((or
- B0
- B1))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto *V0 = Ctx.atom();
+ auto *V1 = Ctx.atom();
+ EXPECT_EQ("(V0 | V1)", llvm::to_string(*Ctx.disj(V0, V1)));
}
TEST(BoolValueDebugStringTest, Implication) {
- // B0 => B1
ConstraintContext Ctx;
- auto B = Ctx.impl(Ctx.atom(), Ctx.atom());
-
- auto Expected = R"((=>
- B0
- B1))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto *V0 = Ctx.atom();
+ auto *V1 = Ctx.atom();
+ EXPECT_EQ("(V0 => V1)", llvm::to_string(*Ctx.impl(V0, V1)));
}
TEST(BoolValueDebugStringTest, Iff) {
- // B0 <=> B1
ConstraintContext Ctx;
- auto B = Ctx.iff(Ctx.atom(), Ctx.atom());
-
- auto Expected = R"((=
- B0
- B1))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto *V0 = Ctx.atom();
+ auto *V1 = Ctx.atom();
+ EXPECT_EQ("(V0 = V1)", llvm::to_string(*Ctx.iff(V0, V1)));
}
TEST(BoolValueDebugStringTest, Xor) {
- // (B0 ^ !B1) V (!B0 ^ B1)
ConstraintContext Ctx;
- auto B0 = Ctx.atom();
- auto B1 = Ctx.atom();
- auto B = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
+ auto V0 = Ctx.atom();
+ auto V1 = Ctx.atom();
+ auto B = Ctx.disj(Ctx.conj(V0, Ctx.neg(V1)), Ctx.conj(Ctx.neg(V0), V1));
- auto Expected = R"((or
- (and
- B0
- (not
- B1))
- (and
- (not
- B0)
- B1)))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
+ auto Expected = "((V0 & !V1) | (!V0 & V1))";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, NestedBoolean) {
- // B0 ^ (B1 v (B2 ^ (B3 v B4)))
- ConstraintContext Ctx;
- auto B = Ctx.conj(
- Ctx.atom(),
- Ctx.disj(Ctx.atom(),
- Ctx.conj(Ctx.atom(), Ctx.disj(Ctx.atom(), Ctx.atom()))));
-
- auto Expected = R"((and
- B0
- (or
- B1
- (and
- B2
- (or
- B3
- B4)))))";
- EXPECT_THAT(debugString(*B), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, AtomicBooleanWithName) {
- // True
ConstraintContext Ctx;
- auto True = cast<AtomicBoolValue>(Ctx.atom());
- auto B = True;
+ auto 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 Expected = R"(True)";
- EXPECT_THAT(debugString(*B, {{True, "True"}}), StrEq(Expected));
-}
-
-TEST(BoolValueDebugStringTest, ComplexBooleanWithNames) {
- // (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
- ConstraintContext Ctx;
- auto Cond = cast<AtomicBoolValue>(Ctx.atom());
- auto Then = cast<AtomicBoolValue>(Ctx.atom());
- auto Else = cast<AtomicBoolValue>(Ctx.atom());
- auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
- Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
-
- auto Expected = R"((or
- (and
- Cond
- (and
- Then
- (not
- Else)))
- (and
- (not
- Cond)
- (and
- (not
- Then)
- Else))))";
- EXPECT_THAT(debugString(*B, {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
- StrEq(Expected));
+ auto Expected = "(V0 & (V1 | (V2 & (V3 | V4))))";
+ EXPECT_THAT(llvm::to_string(*B), StrEq(Expected));
}
TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) {
- // (False && B0) v (True v B1)
- ConstraintContext Ctx;
- auto True = cast<AtomicBoolValue>(Ctx.atom());
- auto False = cast<AtomicBoolValue>(Ctx.atom());
- auto 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.
+ auto True = Ctx.atom();
+ auto False = Ctx.atom();
+ auto V2 = Ctx.atom();
+ auto V3 = Ctx.atom();
+ Formula::AtomNames Names;
+ Names[True->getAtom()] = "true";
+ Names[False->getAtom()] = "false";
+ auto B = Ctx.disj(Ctx.conj(False, V2), Ctx.disj(True, V3));
-B0 = True
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+ auto Expected = R"(((false & V2) | (true | V3)))";
+ std::string Actual;
+ llvm::raw_string_ostream OS(Actual);
+ B->print(OS, &Names);
+ EXPECT_THAT(Actual, StrEq(Expected));
}
-TEST(SATCheckDebugStringTest, 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 B0 = Ctx.atom();
- auto B1 = Ctx.atom();
- auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
- std::vector<BoolValue *> Constraints({B0, XOR});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-B0
-
-(or
- (and
- B0
- (not
- B1))
- (and
- (not
- B0)
- B1))
-------------
-Satisfiable.
-
-B0 = True
-B1 = False
-)";
- EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, ComplexBooleanWithNames) {
- // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
- ConstraintContext Ctx;
- auto Cond = cast<AtomicBoolValue>(Ctx.atom());
- auto Then = cast<AtomicBoolValue>(Ctx.atom());
- auto Else = cast<AtomicBoolValue>(Ctx.atom());
- auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
- Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
- std::vector<BoolValue *> Constraints({Cond, B});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-Cond
-
-(or
- (and
- Cond
- (and
- Then
- (not
- Else)))
- (and
- (not
- Cond)
- (and
- (not
- Then)
- Else)))
-------------
-Satisfiable.
-
-Cond = True
-Else = False
-Then = True
-)";
- EXPECT_THAT(debugString(Constraints, Result,
- {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
- StrEq(Expected));
-}
-
-TEST(SATCheckDebugStringTest, ComplexBooleanWithLongNames) {
- // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq
- ConstraintContext Ctx;
- auto IntsAreEq = cast<AtomicBoolValue>(Ctx.atom());
- auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
- auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
- auto BothZeroImpliesEQ =
- Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);
- std::vector<BoolValue *> Constraints(
- {ThisIntEqZero, Ctx.neg(IntsAreEq), BothZeroImpliesEQ});
- auto Result = CheckSAT(Constraints);
-
- auto Expected = R"(
-Constraints
-------------
-ThisIntEqZero
-
-(not
- IntsAreEq)
-
-(or
- (not
- (and
- ThisIntEqZero
- OtherIntEqZero))
- IntsAreEq)
-------------
-Satisfiable.
-
-IntsAreEq = False
-OtherIntEqZero = False
-ThisIntEqZero = True
-)";
- EXPECT_THAT(debugString(Constraints, Result,
- {{IntsAreEq, "IntsAreEq"},
- {ThisIntEqZero, "ThisIntEqZero"},
- {OtherIntEqZero, "OtherIntEqZero"}}),
- StrEq(Expected));
-}
} // namespace
diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
index 9999dd3a475f1b..ba0a77a910d7c4 100644
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -9,9 +9,10 @@
#include <utility>
#include "TestingSupport.h"
+#include "clang/Analysis/FlowSensitive/Formula.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
-#include "clang/Analysis/FlowSensitive/Value.h"
#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
+#include "llvm/ADT/ArrayRef.h"
#include "gmock/gmock.h"
#include "gtest/gtest.h"
@@ -23,26 +24,31 @@ using namespace dataflow;
using test::ConstraintContext;
using testing::_;
using testing::AnyOf;
-using testing::IsEmpty;
-using testing::Optional;
using testing::Pair;
using testing::UnorderedElementsAre;
+constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue;
+constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse;
+
// Checks if the conjunction of `Vals` is satisfiable and returns the
// corresponding result.
-Solver::Result solve(llvm::ArrayRef<BoolValue *> Vals) {
+Solver::Result solve(llvm::ArrayRef<const Formula *> Vals) {
return WatchedLiteralsSolver().solve(Vals);
}
-void expectUnsatisfiable(Solver::Result Result) {
- EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable);
- EXPECT_FALSE(Result.getSolution().has_value());
+MATCHER(unsat, "") {
+ return arg.getStatus() == Solver::Result::Status::Unsatisfiable;
}
-
-template <typename Matcher>
-void expectSatisfiable(Solver::Result Result, Matcher Solution) {
- EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable);
- EXPECT_THAT(Result.getSolution(), Optional(Solution));
+MATCHER_P(sat, SolutionMatcher,
+ "is satisfiable, where solution " +
+ (testing::DescribeMatcher<
+ llvm::DenseMap<Atom, Solver::Result::Assignment>>(
+ SolutionMatcher))) {
+ if (arg.getStatus() != Solver::Result::Status::Satisfiable)
+ return false;
+ auto Solution = *arg.getSolution();
+ return testing::ExplainMatchResult(SolutionMatcher, Solution,
+ result_listener);
}
TEST(SolverTest, Var) {
@@ -50,9 +56,8 @@ TEST(SolverTest, Var) {
auto X = Ctx.atom();
// X
- expectSatisfiable(
- solve({X}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue)));
+ EXPECT_THAT(solve({X}),
+ sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue))));
}
TEST(SolverTest, NegatedVar) {
@@ -61,9 +66,8 @@ TEST(SolverTest, NegatedVar) {
auto NotX = Ctx.neg(X);
// !X
- expectSatisfiable(
- solve({NotX}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse)));
+ EXPECT_THAT(solve({NotX}),
+ sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse))));
}
TEST(SolverTest, UnitConflict) {
@@ -72,7 +76,7 @@ TEST(SolverTest, UnitConflict) {
auto NotX = Ctx.neg(X);
// X ^ !X
- expectUnsatisfiable(solve({X, NotX}));
+ EXPECT_THAT(solve({X, NotX}), unsat());
}
TEST(SolverTest, DistinctVars) {
@@ -82,36 +86,9 @@ TEST(SolverTest, DistinctVars) {
auto NotY = Ctx.neg(Y);
// X ^ !Y
- expectSatisfiable(
- solve({X, NotY}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
- Pair(Y, Solver::Result::Assignment::AssignedFalse)));
-}
-
-TEST(SolverTest, Top) {
- ConstraintContext Ctx;
- auto X = Ctx.top();
-
- // X. Since Top is anonymous, we do not get any results in the solution.
- expectSatisfiable(solve({X}), IsEmpty());
-}
-
-TEST(SolverTest, NegatedTop) {
- ConstraintContext Ctx;
- auto X = Ctx.top();
-
- // !X
- expectSatisfiable(solve({Ctx.neg(X)}), IsEmpty());
-}
-
-TEST(SolverTest, DistinctTops) {
- ConstraintContext Ctx;
- auto X = Ctx.top();
- auto Y = Ctx.top();
- auto NotY = Ctx.neg(Y);
-
- // X ^ !Y
- expectSatisfiable(solve({X, NotY}), IsEmpty());
+ EXPECT_THAT(solve({X, NotY}),
+ sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
+ Pair(Y->getAtom(), AssignedFalse))));
}
TEST(SolverTest, DoubleNegation) {
@@ -121,7 +98,7 @@ TEST(SolverTest, DoubleNegation) {
auto NotNotX = Ctx.neg(NotX);
// !!X ^ !X
- expectUnsatisfiable(solve({NotNotX, NotX}));
+ EXPECT_THAT(solve({NotNotX, NotX}), unsat());
}
TEST(SolverTest, NegatedDisjunction) {
@@ -132,7 +109,7 @@ TEST(SolverTest, NegatedDisjunction) {
auto NotXOrY = Ctx.neg(XOrY);
// !(X v Y) ^ (X v Y)
- expectUnsatisfiable(solve({NotXOrY, XOrY}));
+ EXPECT_THAT(solve({NotXOrY, XOrY}), unsat());
}
TEST(SolverTest, NegatedConjunction) {
@@ -143,7 +120,7 @@ TEST(SolverTest, NegatedConjunction) {
auto NotXAndY = Ctx.neg(XAndY);
// !(X ^ Y) ^ (X ^ Y)
- expectUnsatisfiable(solve({NotXAndY, XAndY}));
+ EXPECT_THAT(solve({NotXAndY, XAndY}), unsat());
}
TEST(SolverTest, DisjunctionSameVarWithNegation) {
@@ -153,7 +130,7 @@ TEST(SolverTest, DisjunctionSameVarWithNegation) {
auto XOrNotX = Ctx.disj(X, NotX);
// X v !X
- expectSatisfiable(solve({XOrNotX}), _);
+ EXPECT_THAT(solve({XOrNotX}), sat(_));
}
TEST(SolverTest, DisjunctionSameVar) {
@@ -162,7 +139,7 @@ TEST(SolverTest, DisjunctionSameVar) {
auto XOrX = Ctx.disj(X, X);
// X v X
- expectSatisfiable(solve({XOrX}), _);
+ EXPECT_THAT(solve({XOrX}), sat(_));
}
TEST(SolverTest, ConjunctionSameVarsConflict) {
@@ -172,7 +149,7 @@ TEST(SolverTest, ConjunctionSameVarsConflict) {
auto XAndNotX = Ctx.conj(X, NotX);
// X ^ !X
- expectUnsatisfiable(solve({XAndNotX}));
+ EXPECT_THAT(solve({XAndNotX}), unsat());
}
TEST(SolverTest, ConjunctionSameVar) {
@@ -181,7 +158,7 @@ TEST(SolverTest, ConjunctionSameVar) {
auto XAndX = Ctx.conj(X, X);
// X ^ X
- expectSatisfiable(solve({XAndX}), _);
+ EXPECT_THAT(solve({XAndX}), sat(_));
}
TEST(SolverTest, PureVar) {
@@ -194,10 +171,9 @@ TEST(SolverTest, PureVar) {
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (!X v Y) ^ (!X v !Y)
- expectSatisfiable(
- solve({NotXOrY, NotXOrNotY}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
- Pair(Y, _)));
+ EXPECT_THAT(solve({NotXOrY, NotXOrNotY}),
+ sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
+ Pair(Y->getAtom(), _))));
}
TEST(SolverTest, MustAssumeVarIsFalse) {
@@ -211,10 +187,9 @@ TEST(SolverTest, MustAssumeVarIsFalse) {
auto NotXOrNotY = Ctx.disj(NotX, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y)
- expectSatisfiable(
- solve({XOrY, NotXOrY, NotXOrNotY}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse),
- Pair(Y, Solver::Result::Assignment::AssignedTrue)));
+ EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY}),
+ sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
+ Pair(Y->getAtom(), AssignedTrue))));
}
TEST(SolverTest, DeepConflict) {
@@ -229,7 +204,7 @@ TEST(SolverTest, DeepConflict) {
auto XOrNotY = Ctx.disj(X, NotY);
// (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y)
- expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}));
+ EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat());
}
TEST(SolverTest, IffIsEquivalentToDNF) {
@@ -243,7 +218,7 @@ TEST(SolverTest, IffIsEquivalentToDNF) {
auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF));
// !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y)))
- expectUnsatisfiable(solve({NotEquivalent}));
+ EXPECT_THAT(solve({NotEquivalent}), unsat());
}
TEST(SolverTest, IffSameVars) {
@@ -252,7 +227,7 @@ TEST(SolverTest, IffSameVars) {
auto XEqX = Ctx.iff(X, X);
// X <=> X
- expectSatisfiable(solve({XEqX}), _);
+ EXPECT_THAT(solve({XEqX}), sat(_));
}
TEST(SolverTest, IffDistinctVars) {
@@ -262,14 +237,12 @@ TEST(SolverTest, IffDistinctVars) {
auto XEqY = Ctx.iff(X, Y);
// X <=> Y
- expectSatisfiable(
+ EXPECT_THAT(
solve({XEqY}),
- AnyOf(UnorderedElementsAre(
- Pair(X, Solver::Result::Assignment::AssignedTrue),
- Pair(Y, Solver::Result::Assignment::AssignedTrue)),
- UnorderedElementsAre(
- Pair(X, Solver::Result::Assignment::AssignedFalse),
- Pair(Y, Solver::Result::Assignment::AssignedFalse))));
+ sat(AnyOf(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
+ Pair(Y->getAtom(), AssignedTrue)),
+ UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse),
+ Pair(Y->getAtom(), AssignedFalse)))));
}
TEST(SolverTest, IffWithUnits) {
@@ -279,10 +252,9 @@ TEST(SolverTest, IffWithUnits) {
auto XEqY = Ctx.iff(X, Y);
// (X <=> Y) ^ X ^ Y
- expectSatisfiable(
- solve({XEqY, X, Y}),
- UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue),
- Pair(Y, Solver::Result::Assignment::AssignedTrue)));
+ EXPECT_THAT(solve({XEqY, X, Y}),
+ sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue),
+ Pair(Y->getAtom(), AssignedTrue))));
}
TEST(SolverTest, IffWithUnitsConflict) {
@@ -293,7 +265,7 @@ TEST(SolverTest, IffWithUnitsConflict) {
auto NotY = Ctx.neg(Y);
// (X <=> Y) ^ X !Y
- expectUnsatisfiable(solve({XEqY, X, NotY}));
+ EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
}
TEST(SolverTest, IffTransitiveConflict) {
@@ -306,7 +278,7 @@ TEST(SolverTest, IffTransitiveConflict) {
auto NotX = Ctx.neg(X);
// (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X
- expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX}));
+ EXPECT_THAT(solve({XEqY, YEqZ, Z, NotX}), unsat());
}
TEST(SolverTest, DeMorgan) {
@@ -323,7 +295,7 @@ TEST(SolverTest, DeMorgan) {
auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
// A ^ B
- expectSatisfiable(solve({A, B}), _);
+ EXPECT_THAT(solve({A, B}), sat(_));
}
TEST(SolverTest, RespectsAdditionalConstraints) {
@@ -334,7 +306,7 @@ TEST(SolverTest, RespectsAdditionalConstraints) {
auto NotY = Ctx.neg(Y);
// (X <=> Y) ^ X ^ !Y
- expectUnsatisfiable(solve({XEqY, X, NotY}));
+ EXPECT_THAT(solve({XEqY, X, NotY}), unsat());
}
TEST(SolverTest, ImplicationIsEquivalentToDNF) {
@@ -346,7 +318,7 @@ TEST(SolverTest, ImplicationIsEquivalentToDNF) {
auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF));
// !((X => Y) <=> (!X v Y))
- expectUnsatisfiable(solve({NotEquivalent}));
+ EXPECT_THAT(solve({NotEquivalent}), unsat());
}
TEST(SolverTest, ImplicationConflict) {
@@ -357,7 +329,7 @@ TEST(SolverTest, ImplicationConflict) {
auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
// X => Y ^ X ^ !Y
- expectUnsatisfiable(solve({XImplY, XAndNotY}));
+ EXPECT_THAT(solve({XImplY, XAndNotY}), unsat());
}
TEST(SolverTest, LowTimeoutResultsInTimedOut) {
diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
index e258eb7e75f592..93991d87d77f20 100644
--- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
+++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h
@@ -43,6 +43,7 @@
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/StringMap.h"
#include "llvm/ADT/StringRef.h"
+#include "llvm/Support/Allocator.h"
#include "llvm/Support/Errc.h"
#include "llvm/Support/Error.h"
#include "llvm/Testing/Annotations/Annotations.h"
@@ -442,55 +443,44 @@ ValueT &getValueForDecl(ASTContext &ASTCtx, const Environment &Env,
/// Creates and owns constraints which are boolean values.
class ConstraintContext {
-public:
- // Creates an atomic boolean value.
- BoolValue *atom() {
- Vals.push_back(std::make_unique<AtomicBoolValue>());
- return Vals.back().get();
- }
+ unsigned NextAtom = 0;
+ llvm::BumpPtrAllocator A;
- // Creates an instance of the Top boolean value.
- BoolValue *top() {
- Vals.push_back(std::make_unique<TopBoolValue>());
- return Vals.back().get();
+ const Formula *make(Formula::Kind K,
+ llvm::ArrayRef<const Formula *> Operands) {
+ return &Formula::create(A, K, Operands);
}
- // Creates a boolean conjunction value.
- BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<ConjunctionValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
+public:
+ // Returns a reference to a fresh atomic variable.
+ const Formula *atom() {
+ return &Formula::create(A, Formula::AtomRef, {}, NextAtom++);
}
- // Creates a boolean disjunction value.
- BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<DisjunctionValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
+ // Creates a boolean conjunction.
+ const Formula *conj(const Formula *LHS, const Formula *RHS) {
+ return make(Formula::And, {LHS, RHS});
}
- // Creates a boolean negation value.
- BoolValue *neg(BoolValue *SubVal) {
- Vals.push_back(std::make_unique<NegationValue>(*SubVal));
- return Vals.back().get();
+ // Creates a boolean disjunction.
+ const Formula *disj(const Formula *LHS, const Formula *RHS) {
+ return make(Formula::Or, {LHS, RHS});
}
- // Creates a boolean implication value.
- BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<ImplicationValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
+ // Creates a boolean negation.
+ const Formula *neg(const Formula *Operand) {
+ return make(Formula::Not, {Operand});
}
- // Creates a boolean biconditional value.
- BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) {
- Vals.push_back(
- std::make_unique<BiconditionalValue>(*LeftSubVal, *RightSubVal));
- return Vals.back().get();
+ // Creates a boolean implication.
+ const Formula *impl(const Formula *LHS, const Formula *RHS) {
+ return make(Formula::Implies, {LHS, RHS});
}
-private:
- std::vector<std::unique_ptr<BoolValue>> Vals;
+ // Creates a boolean biconditional.
+ const Formula *iff(const Formula *LHS, const Formula *RHS) {
+ return make(Formula::Equal, {LHS, RHS});
+ }
};
} // namespace test
diff --git a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
index 83ea176034c0d7..baadea57e43751 100644
--- a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
@@ -3018,14 +3018,12 @@ TEST(TransferTest, AssignFromCompositeBoolExpression) {
ASSERT_THAT(BazDecl, NotNull());
const auto *BazVal =
- dyn_cast_or_null<ConjunctionValue>(Env.getValue(*BazDecl));
+ dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl));
ASSERT_THAT(BazVal, NotNull());
- EXPECT_EQ(&BazVal->getLeftSubValue(), FooVal);
-
- const auto *BazRightSubValVal =
- cast<DisjunctionValue>(&BazVal->getRightSubValue());
- EXPECT_EQ(&BazRightSubValVal->getLeftSubValue(), BarVal);
- EXPECT_EQ(&BazRightSubValVal->getRightSubValue(), QuxVal);
+ auto &A = Env.arena();
+ EXPECT_EQ(&BazVal->formula(),
+ &A.makeAnd(FooVal->formula(),
+ A.makeOr(BarVal->formula(), QuxVal->formula())));
});
}
@@ -3068,15 +3066,12 @@ TEST(TransferTest, AssignFromCompositeBoolExpression) {
ASSERT_THAT(BazDecl, NotNull());
const auto *BazVal =
- dyn_cast_or_null<DisjunctionValue>(Env.getValue(*BazDecl));
+ dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl));
ASSERT_THAT(BazVal, NotNull());
-
- const auto *BazLeftSubValVal =
- cast<ConjunctionValue>(&BazVal->getLeftSubValue());
- EXPECT_EQ(&BazLeftSubValVal->getLeftSubValue(), FooVal);
- EXPECT_EQ(&BazLeftSubValVal->getRightSubValue(), QuxVal);
-
- EXPECT_EQ(&BazVal->getRightSubValue(), BarVal);
+ auto &A = Env.arena();
+ EXPECT_EQ(&BazVal->formula(),
+ &A.makeOr(A.makeAnd(FooVal->formula(), QuxVal->formula()),
+ BarVal->formula()));
});
}
@@ -3122,17 +3117,14 @@ TEST(TransferTest, AssignFromCompositeBoolExpression) {
ASSERT_THAT(FooDecl, NotNull());
const auto *FooVal =
- dyn_cast_or_null<ConjunctionValue>(Env.getValue(*FooDecl));
+ dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl));
ASSERT_THAT(FooVal, NotNull());
-
- 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);
+ auto &A = Env.arena();
+ EXPECT_EQ(
+ &FooVal->formula(),
+ &A.makeAnd(A.makeAnd(A.makeAnd(AVal->formula(), BVal->formula()),
+ CVal->formula()),
+ DVal->formula()));
});
}
}
@@ -3163,10 +3155,10 @@ TEST(TransferTest, AssignFromBoolNegation) {
ASSERT_THAT(BarDecl, NotNull());
const auto *BarVal =
- dyn_cast_or_null<NegationValue>(Env.getValue(*BarDecl));
+ dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl));
ASSERT_THAT(BarVal, NotNull());
-
- EXPECT_EQ(&BarVal->getSubVal(), FooVal);
+ auto &A = Env.arena();
+ EXPECT_EQ(&BarVal->formula(), &A.makeNot(FooVal->formula()));
});
}
diff --git a/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp b/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
index 2b7341b0839e5f..02f3adeaeda756 100644
--- a/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp
@@ -7,6 +7,7 @@
//===----------------------------------------------------------------------===//
#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"
@@ -39,17 +40,19 @@ TEST(ValueTest, AliasedPointersEquivalent) {
}
TEST(ValueTest, TopsEquivalent) {
- TopBoolValue V1;
- TopBoolValue V2;
+ Arena A;
+ TopBoolValue V1(A.makeAtomRef(Atom(0)));
+ TopBoolValue V2(A.makeAtomRef(Atom(1)));
EXPECT_TRUE(areEquivalentValues(V1, V2));
EXPECT_TRUE(areEquivalentValues(V2, V1));
}
TEST(ValueTest, EquivalentValuesWithDifferentPropsEquivalent) {
- TopBoolValue Prop1;
- TopBoolValue Prop2;
- TopBoolValue V1;
- TopBoolValue V2;
+ 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)));
V1.setProperty("foo", Prop1);
V2.setProperty("bar", Prop2);
EXPECT_TRUE(areEquivalentValues(V1, V2));
@@ -57,9 +60,10 @@ TEST(ValueTest, EquivalentValuesWithDifferentPropsEquivalent) {
}
TEST(ValueTest, DifferentKindsNotEquivalent) {
+ Arena A;
auto L = ScalarStorageLocation(QualType());
ReferenceValue V1(L);
- TopBoolValue V2;
+ TopBoolValue V2(A.makeAtomRef(Atom(0)));
EXPECT_FALSE(areEquivalentValues(V1, V2));
EXPECT_FALSE(areEquivalentValues(V2, V1));
}
More information about the cfe-commits
mailing list