From 5e4ad816bf100b0325ed45ab1cfea18deb3ab3d1 Mon Sep 17 00:00:00 2001 From: Sam McCall Date: Wed, 21 Jun 2023 18:59:01 +0200 Subject: [PATCH] [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 --- clang/include/clang/Analysis/FlowSensitive/Arena.h | 120 ++++++++-------- .../FlowSensitive/DataflowAnalysisContext.h | 29 ++-- .../Analysis/FlowSensitive/DataflowEnvironment.h | 35 +++-- clang/include/clang/Analysis/FlowSensitive/Value.h | 157 +++++---------------- clang/lib/Analysis/FlowSensitive/Arena.cpp | 123 +++++++--------- .../FlowSensitive/DataflowAnalysisContext.cpp | 97 ++++++------- .../Analysis/FlowSensitive/DataflowEnvironment.cpp | 47 +++--- clang/lib/Analysis/FlowSensitive/DebugSupport.cpp | 12 +- clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp | 40 +----- clang/lib/Analysis/FlowSensitive/Transfer.cpp | 60 +------- .../unittests/Analysis/FlowSensitive/ArenaTest.cpp | 74 +++++----- .../FlowSensitive/DataflowAnalysisContextTest.cpp | 88 ++++++------ .../Analysis/FlowSensitive/TransferTest.cpp | 48 +++---- .../unittests/Analysis/FlowSensitive/ValueTest.cpp | 18 ++- 14 files changed, 374 insertions(+), 574 deletions(-) diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h index b6c62e76..373697d 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()), - FalseVal(create()) {} + Arena() : True(makeAtom()), False(makeAtom()) {} Arena(const Arena &) = delete; Arena &operator=(const Arena &) = delete; @@ -57,33 +55,25 @@ public: .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(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(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 @@ public: /// 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(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(); - } - - /// 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(NextAtom++); }; + Atom makeFlowConditionToken() { return makeAtom(); } private: llvm::BumpPtrAllocator Alloc; @@ -123,21 +128,18 @@ private: // Indices that are used to avoid recreating the same integer literals and // composite boolean values. llvm::DenseMap IntegerLiterals; - llvm::DenseMap, ConjunctionValue *> - ConjunctionVals; - llvm::DenseMap, DisjunctionValue *> - DisjunctionVals; - llvm::DenseMap NegationVals; - llvm::DenseMap, ImplicationValue *> - ImplicationVals; - llvm::DenseMap, BiconditionalValue *> - BiconditionalVals; - - llvm::DenseMap ValToFormula; + using FormulaPair = std::pair; + llvm::DenseMap Ands; + llvm::DenseMap Ors; + llvm::DenseMap Nots; + llvm::DenseMap Implies; + llvm::DenseMap Equals; + llvm::DenseMap AtomRefs; + + llvm::DenseMap 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 735f2b2..2a31a34 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -138,33 +138,31 @@ public: 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 @@ public: /// 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 Constraints); + Solver::Result querySolver(llvm::SetVector Constraints); private: friend class Environment; @@ -209,12 +207,12 @@ private: /// to track tokens of flow conditions that were already visited by recursive /// calls. void addTransitiveFlowConditionConstraints( - AtomicBoolValue &Token, llvm::SetVector &Constraints, - llvm::DenseSet &VisitedTokens); + Atom Token, llvm::SetVector &Constraints, + llvm::DenseSet &VisitedTokens); /// Returns true if the solver is able to prove that there is no satisfying /// assignment for `Constraints` - bool isUnsatisfiable(llvm::SetVector Constraints) { + bool isUnsatisfiable(llvm::SetVector Constraints) { return querySolver(std::move(Constraints)).getStatus() == Solver::Result::Status::Unsatisfiable; } @@ -253,9 +251,8 @@ private: // 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> - FlowConditionDeps; - llvm::DenseMap FlowConditionConstraints; + llvm::DenseMap> FlowConditionDeps; + llvm::DenseMap FlowConditionConstraints; llvm::DenseMap FunctionContexts; diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h index faeb5eb..116373d 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h @@ -456,29 +456,30 @@ public: template std::enable_if_t::value, T &> create(Args &&...args) { - return DACtx->arena().create(std::forward(args)...); + return arena().create(std::forward(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( + arena().makeBoolValue(arena().makeLiteral(Value))); } /// Returns an atomic boolean value. BoolValue &makeAtomicBoolValue() const { - return DACtx->arena().create(); + return arena().makeAtomValue(); } /// Returns a unique instance of boolean Top. BoolValue &makeTopBoolValue() const { - return DACtx->arena().create(); + return arena().makeTopValue(); } /// Returns a boolean value that represents the conjunction of `LHS` and @@ -486,7 +487,8 @@ public: /// 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 @@ public: /// 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 @@ public: /// 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 @@ public: /// 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 @@ public: /// 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 @@ private: std::pair> 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 59d5fa6..1d4f800 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 #include @@ -38,14 +38,10 @@ public: 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 e576aff..a12da2d 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 -makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) { +static std::pair +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(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(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(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(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(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(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(makeAtom())); - case Value::Kind::Conjunction: - return Formula::create( - Alloc, Formula::And, - {&getFormula(cast(B).getLeftSubValue()), - &getFormula(cast(B).getRightSubValue())}); - case Value::Kind::Disjunction: - return Formula::create( - Alloc, Formula::Or, - {&getFormula(cast(B).getLeftSubValue()), - &getFormula(cast(B).getRightSubValue())}); - case Value::Kind::Negation: - return Formula::create(Alloc, Formula::Not, - {&getFormula(cast(B).getSubVal())}); - case Value::Kind::Implication: - return Formula::create( - Alloc, Formula::Implies, - {&getFormula(cast(B).getLeftSubValue()), - &getFormula(cast(B).getRightSubValue())}); - case Value::Kind::Biconditional: - return Formula::create( - Alloc, Formula::Equal, - {&getFormula(cast(B).getLeftSubValue()), - &getFormula(cast(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(F) + : &create(F); + return *It->second; } } // namespace clang::dataflow diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp index 42cc6d4..a807ef8 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 Constraints) { +Solver::Result DataflowAnalysisContext::querySolver( + llvm::SetVector Constraints) { Constraints.insert(&arena().makeLiteral(true)); Constraints.insert(&arena().makeNot(arena().makeLiteral(false))); - std::vector 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 Constraints; - Constraints.insert(&Token); + llvm::SetVector Constraints; + Constraints.insert(&arena().makeAtomRef(Token)); Constraints.insert(&arena().makeNot(Val)); - llvm::DenseSet VisitedTokens; + llvm::DenseSet 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 Constraints; - Constraints.insert(&arena().makeNot(Token)); - llvm::DenseSet VisitedTokens; + llvm::SetVector Constraints; + Constraints.insert(&arena().makeNot(arena().makeAtomRef(Token))); + llvm::DenseSet VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); return isUnsatisfiable(std::move(Constraints)); } -bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1, - BoolValue &Val2) { - llvm::SetVector Constraints; +bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1, + const Formula &Val2) { + llvm::SetVector Constraints; Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2))); return isUnsatisfiable(std::move(Constraints)); } void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( - AtomicBoolValue &Token, llvm::SetVector &Constraints, - llvm::DenseSet &VisitedTokens) { - auto Res = VisitedTokens.insert(&Token); + Atom Token, llvm::SetVector &Constraints, + llvm::DenseSet &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 Constraints; - Constraints.insert(&Token); - llvm::DenseSet VisitedTokens; + llvm::SetVector Constraints; + Constraints.insert(&arena().makeAtomRef(Token)); + llvm::DenseSet 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 4a11c09..11bb7da 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(&Val1); - auto *Expr2 = cast(&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(Val1).formula(); + auto &Expr2 = cast(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(); + return &arena().create(); } if (Type->isReferenceType() || Type->isPointerType()) { @@ -837,9 +838,9 @@ Value *Environment::createValueUnlessSelfReferential( } if (Type->isReferenceType()) - return &DACtx->arena().create(PointeeLoc); + return &arena().create(PointeeLoc); else - return &DACtx->arena().create(PointeeLoc); + return &arena().create(PointeeLoc); } if (Type->isRecordType()) { @@ -859,7 +860,7 @@ Value *Environment::createValueUnlessSelfReferential( Visited.erase(FieldType.getCanonicalType()); } - return &DACtx->arena().create(std::move(FieldValues)); + return &arena().create(std::move(FieldValues)); } return nullptr; @@ -884,12 +885,18 @@ const StorageLocation &Environment::skip(const StorageLocation &Loc, return skip(*const_cast(&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 34e5324..f8a049a 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 14293a3..0c4e838 100644 --- a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp +++ b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp @@ -97,6 +97,7 @@ public: 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 @@ public: JOS.attributeObject("f:" + Child.first->getNameAsString(), [&] { dump(*Child.second); }); break; - case Value::Kind::Disjunction: { - auto &VV = cast(V); - JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); }); - JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); }); - break; - } - case Value::Kind::Conjunction: { - auto &VV = cast(V); - JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); }); - JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); }); - break; - } - case Value::Kind::Negation: { - auto &VV = cast(V); - JOS.attributeObject("not", [&] { dump(VV.getSubVal()); }); - break; - } - case Value::Kind::Implication: { - auto &VV = cast(V); - JOS.attributeObject("if", [&] { dump(VV.getLeftSubValue()); }); - JOS.attributeObject("then", [&] { dump(VV.getRightSubValue()); }); - break; - } - case Value::Kind::Biconditional: { - auto &VV = cast(V); - JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); }); - JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); }); - break; - } } for (const auto& Prop : V.properties()) @@ -149,10 +121,12 @@ public: // 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(&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 5ad176d..b9a2672 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 -BoolValue &unpackBinaryBoolValue(Environment &Env, BoolValue &B, M build) { - auto &V = *cast(&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(&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(Env, V, - &Environment::makeAnd); - case Value::Kind::Disjunction: - return unpackBinaryBoolValue(Env, V, - &Environment::makeOr); - case Value::Kind::Implication: - return unpackBinaryBoolValue( - Env, V, &Environment::makeImplication); - case Value::Kind::Biconditional: - return unpackBinaryBoolValue(Env, V, - &Environment::makeIff); + if (auto *Top = llvm::dyn_cast(&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 5313172..0f8552a 100644 --- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp @@ -20,26 +20,26 @@ protected: }; TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) { - auto &X = A.create(); - auto &Y = A.create(); + auto &X = A.makeAtomValue(); + auto &Y = A.makeAtomValue(); EXPECT_NE(&X, &Y); } TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) { - auto &X = A.create(); - auto &Y = A.create(); + auto &X = A.makeTopValue(); + auto &Y = A.makeTopValue(); EXPECT_NE(&X, &Y); } TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) { - auto &X = A.create(); + auto &X = A.makeAtomRef(A.makeAtom()); auto &XAndX = A.makeAnd(X, X); EXPECT_EQ(&XAndX, &X); } TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) { - auto &X = A.create(); - auto &Y = A.create(); + 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(); + auto &Z = A.makeAtomRef(A.makeAtom()); auto &XAndZ = A.makeAnd(X, Z); EXPECT_NE(&XAndY1, &XAndZ); } TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) { - auto &X = A.create(); + auto &X = A.makeAtomRef(A.makeAtom()); auto &XOrX = A.makeOr(X, X); EXPECT_EQ(&XOrX, &X); } TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) { - auto &X = A.create(); - auto &Y = A.create(); + 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(); + auto &Z = A.makeAtomRef(A.makeAtom()); auto &XOrZ = A.makeOr(X, Z); EXPECT_NE(&XOrY1, &XOrZ); } TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) { - auto &X = A.create(); + auto &X = A.makeAtomRef(A.makeAtom()); auto &NotX1 = A.makeNot(X); auto &NotX2 = A.makeNot(X); EXPECT_EQ(&NotX1, &NotX2); - - auto &Y = A.create(); + auto &Y = A.makeAtomRef(A.makeAtom()); auto &NotY = A.makeNot(Y); EXPECT_NE(&NotX1, &NotY); } TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) { - auto &X = A.create(); + 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(); - auto &Y = A.create(); + 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(); + auto &Z = A.makeAtomRef(A.makeAtom()); auto &XImpliesZ = A.makeImplies(X, Z); EXPECT_NE(&XImpliesY1, &XImpliesZ); } TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) { - auto &X = A.create(); + 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(); - auto &Y = A.create(); + 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(); + auto &Z = A.makeAtomRef(A.makeAtom()); auto &XIffZ = A.makeEquals(X, Z); EXPECT_NE(&XIffY1, &XIffZ); } -TEST_F(ArenaTest, ValueToFormula) { - auto &X = A.create(); - auto &Y = A.create(); - 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(); - auto &Y = A.create(); - 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 bb76648..f6e8b30 100644 --- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp @@ -28,56 +28,56 @@ protected: }; TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) { - auto &X = A.create(); - auto &Y = A.create(); - 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(); + 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(); + 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(); + 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(); + 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(); - auto &C2 = A.create(); - auto &C3 = A.create(); + 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(); - 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(); - auto &Y = A.create(); - auto &Z = A.create(); + 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 3f99ff5..667e42f 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(Env.getValue(*BazDecl)); + dyn_cast_or_null(Env.getValue(*BazDecl)); ASSERT_THAT(BazVal, NotNull()); - EXPECT_EQ(&BazVal->getLeftSubValue(), FooVal); - - const auto *BazRightSubValVal = - cast(&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(Env.getValue(*BazDecl)); + dyn_cast_or_null(Env.getValue(*BazDecl)); ASSERT_THAT(BazVal, NotNull()); - - const auto *BazLeftSubValVal = - cast(&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(Env.getValue(*FooDecl)); + dyn_cast_or_null(Env.getValue(*FooDecl)); ASSERT_THAT(FooVal, NotNull()); - - const auto &FooLeftSubVal = - cast(FooVal->getLeftSubValue()); - const auto &FooLeftLeftSubVal = - cast(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(Env.getValue(*BarDecl)); + dyn_cast_or_null(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 2b7341b..02f3ade 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)); } -- 2.7.4