[clang] 5e4ad81 - [dataflow] Replace most BoolValue subclasses with references to Formula (and AtomicBoolValue => Atom and BoolValue => Formula where appropriate)
Sam McCall via cfe-commits
cfe-commits at lists.llvm.org
Wed Jul 5 04:56:12 PDT 2023
Author: Sam McCall
Date: 2023-07-05T13:54:32+02:00
New Revision: 5e4ad816bf100b0325ed45ab1cfea18deb3ab3d1
URL: https://github.com/llvm/llvm-project/commit/5e4ad816bf100b0325ed45ab1cfea18deb3ab3d1
DIFF: https://github.com/llvm/llvm-project/commit/5e4ad816bf100b0325ed45ab1cfea18deb3ab3d1.diff
LOG: [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:
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/Value.h
clang/lib/Analysis/FlowSensitive/Arena.cpp
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/unittests/Analysis/FlowSensitive/ArenaTest.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
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 b6c62e76246254..373697dc7379c5 100644
--- a/clang/include/clang/Analysis/FlowSensitive/Arena.h
+++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h
@@ -16,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;
@@ -57,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.
@@ -91,27 +81,42 @@ 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>();
- }
-
- /// Gets the boolean formula equivalent of a BoolValue.
- /// Each unique Top values is translated to an Atom.
- /// TODO: migrate to storing Formula directly in Values instead.
- const Formula &getFormula(const BoolValue &);
-
- /// Returns a new atomic boolean variable, distinct from any other.
- Atom makeAtom() { return static_cast<Atom>(NextAtom++); };
+ Atom makeFlowConditionToken() { return makeAtom(); }
private:
llvm::BumpPtrAllocator Alloc;
@@ -123,21 +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;
-
- llvm::DenseMap<const BoolValue *, const Formula *> ValToFormula;
+ 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;
- AtomicBoolValue &TrueVal;
- AtomicBoolValue &FalseVal;
+ 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/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/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp
index e576affc6a41b5..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,50 +86,13 @@ IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) {
return *It->second;
}
-const Formula &Arena::getFormula(const BoolValue &B) {
- auto It = ValToFormula.find(&B);
- if (It != ValToFormula.end())
- return *It->second;
- Formula &F = [&]() -> Formula & {
- switch (B.getKind()) {
- case Value::Kind::Integer:
- case Value::Kind::Reference:
- case Value::Kind::Pointer:
- case Value::Kind::Struct:
- llvm_unreachable("not a boolean");
- case Value::Kind::TopBool:
- case Value::Kind::AtomicBool:
- // TODO: assign atom numbers on creation rather than in getFormula(), so
- // they will be deterministic and maybe even meaningful.
- return Formula::create(Alloc, Formula::AtomRef, {},
- static_cast<unsigned>(makeAtom()));
- case Value::Kind::Conjunction:
- return Formula::create(
- Alloc, Formula::And,
- {&getFormula(cast<ConjunctionValue>(B).getLeftSubValue()),
- &getFormula(cast<ConjunctionValue>(B).getRightSubValue())});
- case Value::Kind::Disjunction:
- return Formula::create(
- Alloc, Formula::Or,
- {&getFormula(cast<DisjunctionValue>(B).getLeftSubValue()),
- &getFormula(cast<DisjunctionValue>(B).getRightSubValue())});
- case Value::Kind::Negation:
- return Formula::create(Alloc, Formula::Not,
- {&getFormula(cast<NegationValue>(B).getSubVal())});
- case Value::Kind::Implication:
- return Formula::create(
- Alloc, Formula::Implies,
- {&getFormula(cast<ImplicationValue>(B).getLeftSubValue()),
- &getFormula(cast<ImplicationValue>(B).getRightSubValue())});
- case Value::Kind::Biconditional:
- return Formula::create(
- Alloc, Formula::Equal,
- {&getFormula(cast<BiconditionalValue>(B).getLeftSubValue()),
- &getFormula(cast<BiconditionalValue>(B).getRightSubValue())});
- }
- }();
- ValToFormula.try_emplace(&B, &F);
- return F;
+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/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 42cc6d4c3d143e..a807ef8209be85 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -102,115 +102,112 @@ 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)));
- std::vector<const Formula *> Formulas;
- for (const BoolValue *Constraint : Constraints)
- Formulas.push_back(&arena().getFormula(*Constraint));
- return S->solve(Formulas);
+ 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) {
- // TODO: accumulate formulas directly instead
- 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);
// TODO: have formulas know about true/false directly instead
- Atom True = arena().getFormula(arena().makeLiteral(true)).getAtom();
- Atom False = arena().getFormula(arena().makeLiteral(false)).getAtom();
+ Atom True = arena().makeLiteral(true).getAtom();
+ Atom False = arena().makeLiteral(false).getAtom();
Formula::AtomNames Names = {{False, "false"}, {True, "true"}};
for (const auto *Constraint : Constraints) {
- arena().getFormula(*Constraint).print(OS, &Names);
+ Constraint->print(OS, &Names);
OS << "\n";
}
}
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 34e53249ba4d8b..f8a049adea5e5d 100644
--- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -36,16 +36,8 @@ 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");
}
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 5ad176dc1cdbe9..b9a2672d2e1d0f 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/unittests/Analysis/FlowSensitive/ArenaTest.cpp b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
index 53131723ff5cef..0f8552a58787cb 100644
--- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
@@ -20,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);
@@ -47,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);
@@ -68,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);
@@ -100,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);
@@ -121,30 +120,21 @@ 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, ValueToFormula) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
- auto &XIffY = A.makeEquals(X, Y);
- auto &XOrNotY = A.makeOr(X, A.makeNot(Y));
- auto &Implies = A.makeImplies(XIffY, XOrNotY);
-
- EXPECT_EQ(llvm::to_string(A.getFormula(Implies)),
- "((V0 = V1) => (V0 | !V1))");
-}
-
-TEST_F(ArenaTest, ValueToFormulaCached) {
- auto &X = A.create<AtomicBoolValue>();
- auto &Y = A.create<AtomicBoolValue>();
- auto &XIffY = A.makeEquals(X, Y);
-
- auto &Formula1 = A.getFormula(XIffY);
- auto &Formula2 = A.getFormula(XIffY);
- EXPECT_EQ(&Formula1, &Formula2);
+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
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/TransferTest.cpp b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
index 3f99ff5652ce28..667e42f7f063b7 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