diff options
24 files changed, 1458 insertions, 976 deletions
diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h index 8437cae..83b4dde 100644 --- a/clang/include/clang/Analysis/FlowSensitive/Arena.h +++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h @@ -8,7 +8,6 @@ #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE__ARENA_H -#include "clang/Analysis/FlowSensitive/Formula.h" #include "clang/Analysis/FlowSensitive/StorageLocation.h" #include "clang/Analysis/FlowSensitive/Value.h" #include <vector> @@ -16,12 +15,12 @@ namespace clang::dataflow { /// The Arena owns the objects that model data within an analysis. -/// For example, `Value`, `StorageLocation`, `Atom`, and `Formula`. +/// For example, `Value` and `StorageLocation`. class Arena { public: Arena() - : True(Formula::create(Alloc, Formula::Literal, {}, 1)), - False(Formula::create(Alloc, Formula::Literal, {}, 0)) {} + : TrueVal(create<AtomicBoolValue>()), + FalseVal(create<AtomicBoolValue>()) {} Arena(const Arena &) = delete; Arena &operator=(const Arena &) = delete; @@ -57,25 +56,33 @@ public: .get()); } - /// Creates a BoolValue wrapping a particular formula. - /// - /// Passing in the same formula will result in the same BoolValue. - /// FIXME: Interning BoolValues but not other Values is inconsistent. - /// Decide whether we want Value interning or not. - BoolValue &makeBoolValue(const Formula &); - - /// Creates a fresh atom and wraps in in an AtomicBoolValue. - /// FIXME: For now, identical-address AtomicBoolValue <=> identical atom. - /// Stop relying on pointer identity and remove this guarantee. - AtomicBoolValue &makeAtomValue() { - return cast<AtomicBoolValue>(makeBoolValue(makeAtomRef(makeAtom()))); - } - - /// Creates a fresh Top boolean value. - TopBoolValue &makeTopValue() { - // No need for deduplicating: there's no way to create aliasing Tops. - return create<TopBoolValue>(makeAtomRef(makeAtom())); - } + /// Returns a boolean value that represents the conjunction of `LHS` and + /// `RHS`. Subsequent calls with the same arguments, regardless of their + /// order, will return the same result. If the given boolean values represent + /// the same value, the result will be the value itself. + BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS); + + /// Returns a boolean value that represents the disjunction of `LHS` and + /// `RHS`. Subsequent calls with the same arguments, regardless of their + /// order, will return the same result. If the given boolean values represent + /// the same value, the result will be the value itself. + BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS); + + /// Returns a boolean value that represents the negation of `Val`. Subsequent + /// calls with the same argument will return the same result. + BoolValue &makeNot(BoolValue &Val); + + /// Returns a boolean value that represents `LHS => RHS`. Subsequent calls + /// with the same arguments, will return the same result. If the given boolean + /// values represent the same value, the result will be a value that + /// represents the true boolean literal. + BoolValue &makeImplies(BoolValue &LHS, BoolValue &RHS); + + /// Returns a boolean value that represents `LHS <=> RHS`. Subsequent calls + /// with the same arguments, regardless of their order, will return the same + /// result. If the given boolean values represent the same value, the result + /// will be a value that represents the true boolean literal. + BoolValue &makeEquals(BoolValue &LHS, BoolValue &RHS); /// Returns a symbolic integer value that models an integer literal equal to /// `Value`. These literals are the same every time. @@ -83,44 +90,21 @@ public: /// an integer literal is associated with. IntegerValue &makeIntLiteral(llvm::APInt Value); - // Factories for boolean formulas. - // Formulas are interned: passing the same arguments return the same result. - // For commutative operations like And/Or, interning ignores order. - // Simplifications are applied: makeOr(X, X) => X, etc. - - /// Returns a formula for the conjunction of `LHS` and `RHS`. - const Formula &makeAnd(const Formula &LHS, const Formula &RHS); - - /// Returns a formula for the disjunction of `LHS` and `RHS`. - const Formula &makeOr(const Formula &LHS, const Formula &RHS); - - /// Returns a formula for the negation of `Val`. - const Formula &makeNot(const Formula &Val); - - /// Returns a formula for `LHS => RHS`. - const Formula &makeImplies(const Formula &LHS, const Formula &RHS); - - /// Returns a formula for `LHS <=> RHS`. - const Formula &makeEquals(const Formula &LHS, const Formula &RHS); - - /// Returns a formula for the variable A. - const Formula &makeAtomRef(Atom A); - - /// Returns a formula for a literal true/false. - const Formula &makeLiteral(bool Value) { return Value ? True : False; } - - /// Returns a new atomic boolean variable, distinct from any other. - Atom makeAtom() { return static_cast<Atom>(NextAtom++); }; + /// Returns a symbolic boolean value that models a boolean literal equal to + /// `Value`. These literals are the same every time. + AtomicBoolValue &makeLiteral(bool Value) const { + return Value ? TrueVal : FalseVal; + } /// Creates a fresh flow condition and returns a token that identifies it. The /// token can be used to perform various operations on the flow condition such /// as adding constraints to it, forking it, joining it with another flow /// condition, or checking implications. - Atom makeFlowConditionToken() { return makeAtom(); } + AtomicBoolValue &makeFlowConditionToken() { + return create<AtomicBoolValue>(); + } private: - llvm::BumpPtrAllocator Alloc; - // Storage for the state of a program. std::vector<std::unique_ptr<StorageLocation>> Locs; std::vector<std::unique_ptr<Value>> Vals; @@ -128,18 +112,18 @@ private: // Indices that are used to avoid recreating the same integer literals and // composite boolean values. llvm::DenseMap<llvm::APInt, IntegerValue *> IntegerLiterals; - using FormulaPair = std::pair<const Formula *, const Formula *>; - llvm::DenseMap<FormulaPair, const Formula *> Ands; - llvm::DenseMap<FormulaPair, const Formula *> Ors; - llvm::DenseMap<const Formula *, const Formula *> Nots; - llvm::DenseMap<FormulaPair, const Formula *> Implies; - llvm::DenseMap<FormulaPair, const Formula *> Equals; - llvm::DenseMap<Atom, const Formula *> AtomRefs; - - llvm::DenseMap<const Formula *, BoolValue *> FormulaValues; - unsigned NextAtom = 0; - - const Formula &True, &False; + llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *> + ConjunctionVals; + llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *> + DisjunctionVals; + llvm::DenseMap<BoolValue *, NegationValue *> NegationVals; + llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ImplicationValue *> + ImplicationVals; + llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *> + BiconditionalVals; + + AtomicBoolValue &TrueVal; + AtomicBoolValue &FalseVal; }; } // namespace clang::dataflow diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h index 2a31a34..735f2b2 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -138,31 +138,33 @@ public: PointerValue &getOrCreateNullPointerValue(QualType PointeeType); /// Adds `Constraint` to the flow condition identified by `Token`. - void addFlowConditionConstraint(Atom Token, const Formula &Constraint); + void addFlowConditionConstraint(AtomicBoolValue &Token, + BoolValue &Constraint); /// Creates a new flow condition with the same constraints as the flow /// condition identified by `Token` and returns its token. - Atom forkFlowCondition(Atom Token); + AtomicBoolValue &forkFlowCondition(AtomicBoolValue &Token); /// Creates a new flow condition that represents the disjunction of the flow /// conditions identified by `FirstToken` and `SecondToken`, and returns its /// token. - Atom joinFlowConditions(Atom FirstToken, Atom SecondToken); + AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken, + AtomicBoolValue &SecondToken); /// Returns true if and only if the constraints of the flow condition /// identified by `Token` imply that `Val` is true. - bool flowConditionImplies(Atom Token, const Formula &); + bool flowConditionImplies(AtomicBoolValue &Token, BoolValue &Val); /// Returns true if and only if the constraints of the flow condition /// identified by `Token` are always true. - bool flowConditionIsTautology(Atom Token); + bool flowConditionIsTautology(AtomicBoolValue &Token); /// Returns true if `Val1` is equivalent to `Val2`. /// Note: This function doesn't take into account constraints on `Val1` and /// `Val2` imposed by the flow condition. - bool equivalentFormulas(const Formula &Val1, const Formula &Val2); + bool equivalentBoolValues(BoolValue &Val1, BoolValue &Val2); - LLVM_DUMP_METHOD void dumpFlowCondition(Atom Token, + LLVM_DUMP_METHOD void dumpFlowCondition(AtomicBoolValue &Token, llvm::raw_ostream &OS = llvm::dbgs()); /// Returns the `ControlFlowContext` registered for `F`, if any. Otherwise, @@ -179,7 +181,7 @@ 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<const Formula *> Constraints); + Solver::Result querySolver(llvm::SetVector<BoolValue *> Constraints); private: friend class Environment; @@ -207,12 +209,12 @@ private: /// to track tokens of flow conditions that were already visited by recursive /// calls. void addTransitiveFlowConditionConstraints( - Atom Token, llvm::SetVector<const Formula *> &Constraints, - llvm::DenseSet<Atom> &VisitedTokens); + AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints, + llvm::DenseSet<AtomicBoolValue *> &VisitedTokens); /// Returns true if the solver is able to prove that there is no satisfying /// assignment for `Constraints` - bool isUnsatisfiable(llvm::SetVector<const Formula *> Constraints) { + bool isUnsatisfiable(llvm::SetVector<BoolValue *> Constraints) { return querySolver(std::move(Constraints)).getStatus() == Solver::Result::Status::Unsatisfiable; } @@ -251,8 +253,9 @@ 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<Atom, llvm::DenseSet<Atom>> FlowConditionDeps; - llvm::DenseMap<Atom, const Formula *> FlowConditionConstraints; + llvm::DenseMap<AtomicBoolValue *, llvm::DenseSet<AtomicBoolValue *>> + FlowConditionDeps; + llvm::DenseMap<AtomicBoolValue *, BoolValue *> FlowConditionConstraints; llvm::DenseMap<const FunctionDecl *, ControlFlowContext> FunctionContexts; diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h index b94485c..faeb5eb 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h @@ -456,29 +456,29 @@ public: template <typename T, typename... Args> std::enable_if_t<std::is_base_of<Value, T>::value, T &> create(Args &&...args) { - return arena().create<T>(std::forward<Args>(args)...); + return DACtx->arena().create<T>(std::forward<Args>(args)...); } /// Returns a symbolic integer value that models an integer literal equal to /// `Value` IntegerValue &getIntLiteralValue(llvm::APInt Value) const { - return arena().makeIntLiteral(Value); + return DACtx->arena().makeIntLiteral(Value); } /// Returns a symbolic boolean value that models a boolean literal equal to /// `Value` - BoolValue &getBoolLiteralValue(bool Value) const { - return arena().makeBoolValue(arena().makeLiteral(Value)); + AtomicBoolValue &getBoolLiteralValue(bool Value) const { + return DACtx->arena().makeLiteral(Value); } /// Returns an atomic boolean value. BoolValue &makeAtomicBoolValue() const { - return arena().makeAtomValue(); + return DACtx->arena().create<AtomicBoolValue>(); } /// Returns a unique instance of boolean Top. BoolValue &makeTopBoolValue() const { - return arena().makeTopValue(); + return DACtx->arena().create<TopBoolValue>(); } /// Returns a boolean value that represents the conjunction of `LHS` and @@ -486,8 +486,7 @@ 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 arena().makeBoolValue( - arena().makeAnd(LHS.formula(), RHS.formula())); + return DACtx->arena().makeAnd(LHS, RHS); } /// Returns a boolean value that represents the disjunction of `LHS` and @@ -495,14 +494,13 @@ 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 arena().makeBoolValue( - arena().makeOr(LHS.formula(), RHS.formula())); + return DACtx->arena().makeOr(LHS, RHS); } /// Returns a boolean value that represents the negation of `Val`. Subsequent /// calls with the same argument will return the same result. BoolValue &makeNot(BoolValue &Val) const { - return arena().makeBoolValue(arena().makeNot(Val.formula())); + return DACtx->arena().makeNot(Val); } /// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with @@ -510,8 +508,7 @@ 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 arena().makeBoolValue( - arena().makeImplies(LHS.formula(), RHS.formula())); + return DACtx->arena().makeImplies(LHS, RHS); } /// Returns a boolean value represents `LHS` <=> `RHS`. Subsequent calls with @@ -519,22 +516,17 @@ 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 arena().makeBoolValue( - arena().makeEquals(LHS.formula(), RHS.formula())); + return DACtx->arena().makeEquals(LHS, RHS); } /// Returns the token that identifies the flow condition of the environment. - Atom getFlowConditionToken() const { return FlowConditionToken; } + AtomicBoolValue &getFlowConditionToken() const { return *FlowConditionToken; } /// Adds `Val` to the set of clauses that constitute the flow condition. - void addToFlowCondition(const Formula &); - LLVM_DEPRECATED("Use Formula version instead", "") void addToFlowCondition(BoolValue &Val); /// Returns true if and only if the clauses that constitute the flow condition /// imply that `Val` is true. - bool flowConditionImplies(const Formula &) const; - LLVM_DEPRECATED("Use Formula version instead", "") bool flowConditionImplies(BoolValue &Val) const; /// Returns the `DeclContext` of the block being analysed, if any. Otherwise, @@ -555,8 +547,6 @@ 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; @@ -627,7 +617,7 @@ private: std::pair<StructValue *, const ValueDecl *>> MemberLocToStruct; - Atom FlowConditionToken; + AtomicBoolValue *FlowConditionToken; }; /// Returns the storage location for the implicit object of a diff --git a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h index 6b9f368..360786b 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h +++ b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h @@ -19,6 +19,7 @@ #include "clang/Analysis/FlowSensitive/Solver.h" #include "clang/Analysis/FlowSensitive/Value.h" +#include "llvm/ADT/DenseMap.h" #include "llvm/ADT/StringRef.h" namespace clang { @@ -27,9 +28,52 @@ namespace dataflow { /// Returns a string representation of a value kind. llvm::StringRef debugString(Value::Kind Kind); +/// Returns a string representation of a boolean assignment to true or false. +llvm::StringRef debugString(Solver::Result::Assignment Assignment); + /// Returns a string representation of the result status of a SAT check. llvm::StringRef debugString(Solver::Result::Status Status); +/// Returns a string representation for the boolean value `B`. +/// +/// Atomic booleans appearing in the boolean value `B` are assigned to labels +/// either specified in `AtomNames` or created by default rules as B0, B1, ... +/// +/// Requirements: +/// +/// Names assigned to atoms should not be repeated in `AtomNames`. +std::string debugString( + const BoolValue &B, + llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}}); + +/// Returns a string representation for `Constraints` - a collection of boolean +/// formulas. +/// +/// Atomic booleans appearing in the boolean value `Constraints` are assigned to +/// labels either specified in `AtomNames` or created by default rules as B0, +/// B1, ... +/// +/// Requirements: +/// +/// Names assigned to atoms should not be repeated in `AtomNames`. +std::string debugString( + const llvm::ArrayRef<BoolValue *> Constraints, + llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}}); + +/// Returns a string representation for `Constraints` - a collection of boolean +/// formulas and the `Result` of satisfiability checking. +/// +/// Atomic booleans appearing in `Constraints` and `Result` are assigned to +/// labels either specified in `AtomNames` or created by default rules as B0, +/// B1, ... +/// +/// Requirements: +/// +/// Names assigned to atoms should not be repeated in `AtomNames`. +std::string debugString( + ArrayRef<BoolValue *> Constraints, const Solver::Result &Result, + llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}}); + } // namespace dataflow } // namespace clang diff --git a/clang/include/clang/Analysis/FlowSensitive/Formula.h b/clang/include/clang/Analysis/FlowSensitive/Formula.h deleted file mode 100644 index 1d8cb6b..0000000 --- a/clang/include/clang/Analysis/FlowSensitive/Formula.h +++ /dev/null @@ -1,144 +0,0 @@ -//===- Formula.h - Boolean formulas -----------------------------*- C++ -*-===// -// -// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. -// See https://llvm.org/LICENSE.txt for license information. -// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception -// -//===----------------------------------------------------------------------===// - -#ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H -#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_FORMULA_H - -#include "clang/Basic/LLVM.h" -#include "llvm/ADT/ArrayRef.h" -#include "llvm/ADT/DenseMap.h" -#include "llvm/ADT/DenseMapInfo.h" -#include "llvm/ADT/STLFunctionalExtras.h" -#include "llvm/Support/Allocator.h" -#include "llvm/Support/raw_ostream.h" -#include <cassert> -#include <string> -#include <type_traits> - -namespace clang::dataflow { - -/// Identifies an atomic boolean variable such as "V1". -/// -/// This often represents an assertion that is interesting to the analysis but -/// cannot immediately be proven true or false. For example: -/// - V1 may mean "the program reaches this point", -/// - V2 may mean "the parameter was null" -/// -/// We can use these variables in formulas to describe relationships we know -/// to be true: "if the parameter was null, the program reaches this point". -/// We also express hypotheses as formulas, and use a SAT solver to check -/// whether they are consistent with the known facts. -enum class Atom : unsigned {}; - -/// A boolean expression such as "true" or "V1 & !V2". -/// Expressions may refer to boolean atomic variables. These should take a -/// consistent true/false value across the set of formulas being considered. -/// -/// (Formulas are always expressions in terms of boolean variables rather than -/// e.g. integers because our underlying model is SAT rather than e.g. SMT). -/// -/// Simple formulas such as "true" and "V1" are self-contained. -/// Compound formulas connect other formulas, e.g. "(V1 & V2) || V3" is an 'or' -/// formula, with pointers to its operands "(V1 & V2)" and "V3" stored as -/// trailing objects. -/// For this reason, Formulas are Arena-allocated and over-aligned. -class Formula; -class alignas(const Formula *) Formula { -public: - enum Kind : unsigned { - /// A reference to an atomic boolean variable. - /// We name these e.g. "V3", where 3 == atom identity == Value. - AtomRef, - /// Constant true or false. - Literal, - - Not, /// True if its only operand is false - - // These kinds connect two operands LHS and RHS - And, /// True if LHS and RHS are both true - Or, /// True if either LHS or RHS is true - Implies, /// True if LHS is false or RHS is true - Equal, /// True if LHS and RHS have the same truth value - }; - Kind kind() const { return FormulaKind; } - - Atom getAtom() const { - assert(kind() == AtomRef); - return static_cast<Atom>(Value); - } - - bool literal() const { - assert(kind() == Literal); - return static_cast<bool>(Value); - } - - ArrayRef<const Formula *> operands() const { - return ArrayRef(reinterpret_cast<Formula *const *>(this + 1), - numOperands(kind())); - } - - using AtomNames = llvm::DenseMap<Atom, std::string>; - // Produce a stable human-readable representation of this formula. - // For example: (V3 | !(V1 & V2)) - // If AtomNames is provided, these override the default V0, V1... names. - void print(llvm::raw_ostream &OS, const AtomNames * = nullptr) const; - - // Allocate Formulas using Arena rather than calling this function directly. - static const Formula &create(llvm::BumpPtrAllocator &Alloc, Kind K, - ArrayRef<const Formula *> Operands, - unsigned Value = 0); - -private: - Formula() = default; - Formula(const Formula &) = delete; - Formula &operator=(const Formula &) = delete; - - static unsigned numOperands(Kind K) { - switch (K) { - case AtomRef: - case Literal: - return 0; - case Not: - return 1; - case And: - case Or: - case Implies: - case Equal: - return 2; - } - } - - Kind FormulaKind; - // Some kinds of formula have scalar values, e.g. AtomRef's atom number. - unsigned Value; -}; - -// The default names of atoms are V0, V1 etc in order of creation. -inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, Atom A) { - return OS << 'V' << static_cast<unsigned>(A); -} -inline llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Formula &F) { - F.print(OS); - return OS; -} - -} // namespace clang::dataflow -namespace llvm { -template <> struct DenseMapInfo<clang::dataflow::Atom> { - using Atom = clang::dataflow::Atom; - using Underlying = std::underlying_type_t<Atom>; - - static inline Atom getEmptyKey() { return Atom(Underlying(-1)); } - static inline Atom getTombstoneKey() { return Atom(Underlying(-2)); } - static unsigned getHashValue(const Atom &Val) { - return DenseMapInfo<Underlying>::getHashValue(Underlying(Val)); - } - static bool isEqual(const Atom &LHS, const Atom &RHS) { return LHS == RHS; } -}; -} // namespace llvm -#endif diff --git a/clang/include/clang/Analysis/FlowSensitive/Solver.h b/clang/include/clang/Analysis/FlowSensitive/Solver.h index 079f680..10964ea 100644 --- a/clang/include/clang/Analysis/FlowSensitive/Solver.h +++ b/clang/include/clang/Analysis/FlowSensitive/Solver.h @@ -14,10 +14,12 @@ #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H -#include "clang/Analysis/FlowSensitive/Formula.h" +#include "clang/Analysis/FlowSensitive/Value.h" #include "clang/Basic/LLVM.h" #include "llvm/ADT/ArrayRef.h" #include "llvm/ADT/DenseMap.h" +#include "llvm/ADT/DenseSet.h" +#include "llvm/Support/Compiler.h" #include <optional> #include <vector> @@ -47,7 +49,8 @@ public: /// Constructs a result indicating that the queried boolean formula is /// satisfiable. The result will hold a solution found by the solver. - static Result Satisfiable(llvm::DenseMap<Atom, Assignment> Solution) { + static Result + Satisfiable(llvm::DenseMap<AtomicBoolValue *, Assignment> Solution) { return Result(Status::Satisfiable, std::move(Solution)); } @@ -65,17 +68,19 @@ public: /// Returns a truth assignment to boolean values that satisfies the queried /// boolean formula if available. Otherwise, an empty optional is returned. - std::optional<llvm::DenseMap<Atom, Assignment>> getSolution() const { + std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> + getSolution() const { return Solution; } private: - Result(Status SATCheckStatus, - std::optional<llvm::DenseMap<Atom, Assignment>> Solution) + Result( + enum Status SATCheckStatus, + std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution) : SATCheckStatus(SATCheckStatus), Solution(std::move(Solution)) {} Status SATCheckStatus; - std::optional<llvm::DenseMap<Atom, Assignment>> Solution; + std::optional<llvm::DenseMap<AtomicBoolValue *, Assignment>> Solution; }; virtual ~Solver() = default; @@ -86,11 +91,13 @@ public: /// Requirements: /// /// All elements in `Vals` must not be null. - virtual Result solve(llvm::ArrayRef<const Formula *> Vals) = 0; -}; + virtual Result solve(llvm::ArrayRef<BoolValue *> Vals) = 0; -llvm::raw_ostream &operator<<(llvm::raw_ostream &, const Solver::Result &); -llvm::raw_ostream &operator<<(llvm::raw_ostream &, Solver::Result::Assignment); + LLVM_DEPRECATED("Pass ArrayRef for determinism", "") + virtual Result solve(llvm::DenseSet<BoolValue *> Vals) { + return solve(ArrayRef(std::vector<BoolValue *>(Vals.begin(), Vals.end()))); + } +}; } // namespace dataflow } // namespace clang diff --git a/clang/include/clang/Analysis/FlowSensitive/Value.h b/clang/include/clang/Analysis/FlowSensitive/Value.h index 1d4f800..59d5fa6 100644 --- a/clang/include/clang/Analysis/FlowSensitive/Value.h +++ b/clang/include/clang/Analysis/FlowSensitive/Value.h @@ -15,11 +15,11 @@ #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_VALUE_H #include "clang/AST/Decl.h" -#include "clang/Analysis/FlowSensitive/Formula.h" #include "clang/Analysis/FlowSensitive/StorageLocation.h" #include "llvm/ADT/DenseMap.h" #include "llvm/ADT/StringMap.h" #include "llvm/ADT/StringRef.h" +#include "llvm/Support/raw_ostream.h" #include <cassert> #include <utility> @@ -38,10 +38,14 @@ public: Pointer, Struct, - // TODO: Top values should not be need to be type-specific. + // Synthetic boolean values are either atomic values or logical connectives. TopBool, AtomicBool, - FormulaBool, + Conjunction, + Disjunction, + Negation, + Implication, + Biconditional, }; explicit Value(Kind ValKind) : ValKind(ValKind) {} @@ -91,68 +95,151 @@ bool areEquivalentValues(const Value &Val1, const Value &Val2); /// Models a boolean. class BoolValue : public Value { - const Formula *F; - public: - explicit BoolValue(Kind ValueKind, const Formula &F) - : Value(ValueKind), F(&F) {} + explicit BoolValue(Kind ValueKind) : Value(ValueKind) {} static bool classof(const Value *Val) { return Val->getKind() == Kind::TopBool || Val->getKind() == Kind::AtomicBool || - Val->getKind() == Kind::FormulaBool; + Val->getKind() == Kind::Conjunction || + Val->getKind() == Kind::Disjunction || + Val->getKind() == Kind::Negation || + Val->getKind() == Kind::Implication || + Val->getKind() == Kind::Biconditional; } - - const Formula &formula() const { return *F; } }; -/// A TopBoolValue represents a boolean that is explicitly unconstrained. -/// -/// This is equivalent to an AtomicBoolValue that does not appear anywhere -/// else in a system of formula. -/// Knowing the value is unconstrained is useful when e.g. reasoning about -/// convergence. +/// Models the trivially true formula, which is Top in the lattice of boolean +/// formulas. class TopBoolValue final : public BoolValue { public: - TopBoolValue(const Formula &F) : BoolValue(Kind::TopBool, F) { - assert(F.kind() == Formula::AtomRef); - } + TopBoolValue() : BoolValue(Kind::TopBool) {} static bool classof(const Value *Val) { return Val->getKind() == Kind::TopBool; } - - Atom getAtom() const { return formula().getAtom(); } }; /// Models an atomic boolean. -/// -/// FIXME: Merge this class into FormulaBoolValue. -/// When we want to specify atom identity, use Atom. -class AtomicBoolValue final : public BoolValue { +class AtomicBoolValue : public BoolValue { public: - explicit AtomicBoolValue(const Formula &F) : BoolValue(Kind::AtomicBool, F) { - assert(F.kind() == Formula::AtomRef); - } + explicit AtomicBoolValue() : BoolValue(Kind::AtomicBool) {} static bool classof(const Value *Val) { return Val->getKind() == Kind::AtomicBool; } +}; + +/// Models a boolean conjunction. +// FIXME: Consider representing binary and unary boolean operations similar +// to how they are represented in the AST. This might become more pressing +// when such operations need to be added for other data types. +class ConjunctionValue : public BoolValue { +public: + explicit ConjunctionValue(BoolValue &LeftSubVal, BoolValue &RightSubVal) + : BoolValue(Kind::Conjunction), LeftSubVal(LeftSubVal), + RightSubVal(RightSubVal) {} + + static bool classof(const Value *Val) { + return Val->getKind() == Kind::Conjunction; + } + + /// Returns the left sub-value of the conjunction. + BoolValue &getLeftSubValue() const { return LeftSubVal; } + + /// Returns the right sub-value of the conjunction. + BoolValue &getRightSubValue() const { return RightSubVal; } + +private: + BoolValue &LeftSubVal; + BoolValue &RightSubVal; +}; + +/// Models a boolean disjunction. +class DisjunctionValue : public BoolValue { +public: + explicit DisjunctionValue(BoolValue &LeftSubVal, BoolValue &RightSubVal) + : BoolValue(Kind::Disjunction), LeftSubVal(LeftSubVal), + RightSubVal(RightSubVal) {} + + static bool classof(const Value *Val) { + return Val->getKind() == Kind::Disjunction; + } + + /// Returns the left sub-value of the disjunction. + BoolValue &getLeftSubValue() const { return LeftSubVal; } + + /// Returns the right sub-value of the disjunction. + BoolValue &getRightSubValue() const { return RightSubVal; } + +private: + BoolValue &LeftSubVal; + BoolValue &RightSubVal; +}; + +/// Models a boolean negation. +class NegationValue : public BoolValue { +public: + explicit NegationValue(BoolValue &SubVal) + : BoolValue(Kind::Negation), SubVal(SubVal) {} + + static bool classof(const Value *Val) { + return Val->getKind() == Kind::Negation; + } + + /// Returns the sub-value of the negation. + BoolValue &getSubVal() const { return SubVal; } - Atom getAtom() const { return formula().getAtom(); } +private: + BoolValue &SubVal; }; -/// Models a compound boolean formula. -class FormulaBoolValue final : public BoolValue { +/// Models a boolean implication. +/// +/// Equivalent to `!LHS v RHS`. +class ImplicationValue : public BoolValue { public: - explicit FormulaBoolValue(const Formula &F) - : BoolValue(Kind::FormulaBool, F) { - assert(F.kind() != Formula::AtomRef && "For now, use AtomicBoolValue"); + explicit ImplicationValue(BoolValue &LeftSubVal, BoolValue &RightSubVal) + : BoolValue(Kind::Implication), LeftSubVal(LeftSubVal), + RightSubVal(RightSubVal) {} + + static bool classof(const Value *Val) { + return Val->getKind() == Kind::Implication; } + /// Returns the left sub-value of the implication. + BoolValue &getLeftSubValue() const { return LeftSubVal; } + + /// Returns the right sub-value of the implication. + BoolValue &getRightSubValue() const { return RightSubVal; } + +private: + BoolValue &LeftSubVal; + BoolValue &RightSubVal; +}; + +/// Models a boolean biconditional. +/// +/// Equivalent to `(LHS ^ RHS) v (!LHS ^ !RHS)`. +class BiconditionalValue : public BoolValue { +public: + explicit BiconditionalValue(BoolValue &LeftSubVal, BoolValue &RightSubVal) + : BoolValue(Kind::Biconditional), LeftSubVal(LeftSubVal), + RightSubVal(RightSubVal) {} + static bool classof(const Value *Val) { - return Val->getKind() == Kind::FormulaBool; + return Val->getKind() == Kind::Biconditional; } + + /// Returns the left sub-value of the biconditional. + BoolValue &getLeftSubValue() const { return LeftSubVal; } + + /// Returns the right sub-value of the biconditional. + BoolValue &getRightSubValue() const { return RightSubVal; } + +private: + BoolValue &LeftSubVal; + BoolValue &RightSubVal; }; /// Models an integer. diff --git a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h index a0cdce9..b69cc01 100644 --- a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h +++ b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h @@ -14,8 +14,8 @@ #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H -#include "clang/Analysis/FlowSensitive/Formula.h" #include "clang/Analysis/FlowSensitive/Solver.h" +#include "clang/Analysis/FlowSensitive/Value.h" #include "llvm/ADT/ArrayRef.h" #include <limits> @@ -46,7 +46,7 @@ public: explicit WatchedLiteralsSolver(std::int64_t WorkLimit) : MaxIterations(WorkLimit) {} - Result solve(llvm::ArrayRef<const Formula *> Vals) override; + Result solve(llvm::ArrayRef<BoolValue *> Vals) override; }; } // namespace dataflow diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp index a61887a..cff6c45 100644 --- a/clang/lib/Analysis/FlowSensitive/Arena.cpp +++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp @@ -7,95 +7,65 @@ //===----------------------------------------------------------------------===// #include "clang/Analysis/FlowSensitive/Arena.h" -#include "clang/Analysis/FlowSensitive/Value.h" namespace clang::dataflow { -static std::pair<const Formula *, const Formula *> -canonicalFormulaPair(const Formula &LHS, const Formula &RHS) { +static std::pair<BoolValue *, BoolValue *> +makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) { auto Res = std::make_pair(&LHS, &RHS); - if (&RHS < &LHS) // FIXME: use a deterministic order instead + if (&RHS < &LHS) std::swap(Res.first, Res.second); return Res; } -template <class Key, class ComputeFunc> -const Formula &cached(llvm::DenseMap<Key, const Formula *> &Cache, Key K, - ComputeFunc &&Compute) { - auto [It, Inserted] = Cache.try_emplace(std::forward<Key>(K)); - if (Inserted) - It->second = Compute(); - return *It->second; -} +BoolValue &Arena::makeAnd(BoolValue &LHS, BoolValue &RHS) { + if (&LHS == &RHS) + return LHS; -const Formula &Arena::makeAtomRef(Atom A) { - return cached(AtomRefs, A, [&] { - return &Formula::create(Alloc, Formula::AtomRef, {}, - static_cast<unsigned>(A)); - }); + auto Res = ConjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS), + nullptr); + if (Res.second) + Res.first->second = &create<ConjunctionValue>(LHS, RHS); + return *Res.first->second; } -const Formula &Arena::makeAnd(const Formula &LHS, const Formula &RHS) { - return cached(Ands, canonicalFormulaPair(LHS, RHS), [&] { - if (&LHS == &RHS) - return &LHS; - if (LHS.kind() == Formula::Literal) - return LHS.literal() ? &RHS : &LHS; - if (RHS.kind() == Formula::Literal) - return RHS.literal() ? &LHS : &RHS; +BoolValue &Arena::makeOr(BoolValue &LHS, BoolValue &RHS) { + if (&LHS == &RHS) + return LHS; - return &Formula::create(Alloc, Formula::And, {&LHS, &RHS}); - }); + auto Res = DisjunctionVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS), + nullptr); + if (Res.second) + Res.first->second = &create<DisjunctionValue>(LHS, RHS); + return *Res.first->second; } -const Formula &Arena::makeOr(const Formula &LHS, const Formula &RHS) { - return cached(Ors, canonicalFormulaPair(LHS, RHS), [&] { - if (&LHS == &RHS) - return &LHS; - if (LHS.kind() == Formula::Literal) - return LHS.literal() ? &LHS : &RHS; - if (RHS.kind() == Formula::Literal) - return RHS.literal() ? &RHS : &LHS; - - return &Formula::create(Alloc, Formula::Or, {&LHS, &RHS}); - }); +BoolValue &Arena::makeNot(BoolValue &Val) { + auto Res = NegationVals.try_emplace(&Val, nullptr); + if (Res.second) + Res.first->second = &create<NegationValue>(Val); + return *Res.first->second; } -const Formula &Arena::makeNot(const Formula &Val) { - return cached(Nots, &Val, [&] { - if (Val.kind() == Formula::Not) - return Val.operands()[0]; - if (Val.kind() == Formula::Literal) - return &makeLiteral(!Val.literal()); +BoolValue &Arena::makeImplies(BoolValue &LHS, BoolValue &RHS) { + if (&LHS == &RHS) + return makeLiteral(true); - return &Formula::create(Alloc, Formula::Not, {&Val}); - }); + auto Res = ImplicationVals.try_emplace(std::make_pair(&LHS, &RHS), nullptr); + if (Res.second) + Res.first->second = &create<ImplicationValue>(LHS, RHS); + return *Res.first->second; } -const Formula &Arena::makeImplies(const Formula &LHS, const Formula &RHS) { - return cached(Implies, std::make_pair(&LHS, &RHS), [&] { - if (&LHS == &RHS) - return &makeLiteral(true); - if (LHS.kind() == Formula::Literal) - return LHS.literal() ? &RHS : &makeLiteral(true); - if (RHS.kind() == Formula::Literal) - return RHS.literal() ? &RHS : &makeNot(LHS); +BoolValue &Arena::makeEquals(BoolValue &LHS, BoolValue &RHS) { + if (&LHS == &RHS) + return makeLiteral(true); - return &Formula::create(Alloc, Formula::Implies, {&LHS, &RHS}); - }); -} - -const Formula &Arena::makeEquals(const Formula &LHS, const Formula &RHS) { - return cached(Equals, canonicalFormulaPair(LHS, RHS), [&] { - if (&LHS == &RHS) - return &makeLiteral(true); - if (LHS.kind() == Formula::Literal) - return LHS.literal() ? &RHS : &makeNot(RHS); - if (RHS.kind() == Formula::Literal) - return RHS.literal() ? &LHS : &makeNot(LHS); - - return &Formula::create(Alloc, Formula::Equal, {&LHS, &RHS}); - }); + auto Res = BiconditionalVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS), + nullptr); + if (Res.second) + Res.first->second = &create<BiconditionalValue>(LHS, RHS); + return *Res.first->second; } IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) { @@ -106,13 +76,4 @@ IntegerValue &Arena::makeIntLiteral(llvm::APInt Value) { return *It->second; } -BoolValue &Arena::makeBoolValue(const Formula &F) { - auto [It, Inserted] = FormulaValues.try_emplace(&F); - if (Inserted) - It->second = (F.kind() == Formula::AtomRef) - ? (BoolValue *)&create<AtomicBoolValue>(F) - : &create<FormulaBoolValue>(F); - return *It->second; -} - } // namespace clang::dataflow diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt index 171884a..d59bebf 100644 --- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt +++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt @@ -3,7 +3,6 @@ add_clang_library(clangAnalysisFlowSensitive ControlFlowContext.cpp DataflowAnalysisContext.cpp DataflowEnvironment.cpp - Formula.cpp HTMLLogger.cpp Logger.cpp RecordOps.cpp diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp index 2971df6..37bcc8b 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -15,7 +15,6 @@ #include "clang/Analysis/FlowSensitive/DataflowAnalysisContext.h" #include "clang/AST/ExprCXX.h" #include "clang/Analysis/FlowSensitive/DebugSupport.h" -#include "clang/Analysis/FlowSensitive/Formula.h" #include "clang/Analysis/FlowSensitive/Logger.h" #include "clang/Analysis/FlowSensitive/Value.h" #include "llvm/ADT/SetOperations.h" @@ -24,12 +23,9 @@ #include "llvm/Support/Debug.h" #include "llvm/Support/FileSystem.h" #include "llvm/Support/Path.h" -#include "llvm/Support/raw_ostream.h" #include <cassert> #include <memory> -#include <string> #include <utility> -#include <vector> static llvm::cl::opt<std::string> DataflowLog( "dataflow-log", llvm::cl::Hidden, llvm::cl::ValueOptional, @@ -102,107 +98,108 @@ DataflowAnalysisContext::getOrCreateNullPointerValue(QualType PointeeType) { } void DataflowAnalysisContext::addFlowConditionConstraint( - Atom Token, const Formula &Constraint) { - auto Res = FlowConditionConstraints.try_emplace(Token, &Constraint); + AtomicBoolValue &Token, BoolValue &Constraint) { + auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint); if (!Res.second) { Res.first->second = &arena().makeAnd(*Res.first->second, Constraint); } } -Atom DataflowAnalysisContext::forkFlowCondition(Atom Token) { - Atom ForkToken = arena().makeFlowConditionToken(); - FlowConditionDeps[ForkToken].insert(Token); - addFlowConditionConstraint(ForkToken, arena().makeAtomRef(Token)); +AtomicBoolValue & +DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) { + auto &ForkToken = arena().makeFlowConditionToken(); + FlowConditionDeps[&ForkToken].insert(&Token); + addFlowConditionConstraint(ForkToken, Token); return ForkToken; } -Atom -DataflowAnalysisContext::joinFlowConditions(Atom FirstToken, - Atom SecondToken) { - Atom Token = arena().makeFlowConditionToken(); - FlowConditionDeps[Token].insert(FirstToken); - FlowConditionDeps[Token].insert(SecondToken); - addFlowConditionConstraint(Token, - arena().makeOr(arena().makeAtomRef(FirstToken), - arena().makeAtomRef(SecondToken))); +AtomicBoolValue & +DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken, + AtomicBoolValue &SecondToken) { + auto &Token = arena().makeFlowConditionToken(); + FlowConditionDeps[&Token].insert(&FirstToken); + FlowConditionDeps[&Token].insert(&SecondToken); + addFlowConditionConstraint( + Token, arena().makeOr(FirstToken, SecondToken)); return Token; } -Solver::Result DataflowAnalysisContext::querySolver( - llvm::SetVector<const Formula *> Constraints) { +Solver::Result +DataflowAnalysisContext::querySolver(llvm::SetVector<BoolValue *> Constraints) { + Constraints.insert(&arena().makeLiteral(true)); + Constraints.insert(&arena().makeNot(arena().makeLiteral(false))); return S->solve(Constraints.getArrayRef()); } -bool DataflowAnalysisContext::flowConditionImplies(Atom Token, - const Formula &Val) { +bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token, + BoolValue &Val) { // Returns true if and only if truth assignment of the flow condition implies // that `Val` is also true. We prove whether or not this property holds by // reducing the problem to satisfiability checking. In other words, we attempt // to show that assuming `Val` is false makes the constraints induced by the // flow condition unsatisfiable. - llvm::SetVector<const Formula *> Constraints; - Constraints.insert(&arena().makeAtomRef(Token)); + llvm::SetVector<BoolValue *> Constraints; + Constraints.insert(&Token); Constraints.insert(&arena().makeNot(Val)); - llvm::DenseSet<Atom> VisitedTokens; + llvm::DenseSet<AtomicBoolValue *> VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); return isUnsatisfiable(std::move(Constraints)); } -bool DataflowAnalysisContext::flowConditionIsTautology(Atom Token) { +bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) { // Returns true if and only if we cannot prove that the flow condition can // ever be false. - llvm::SetVector<const Formula *> Constraints; - Constraints.insert(&arena().makeNot(arena().makeAtomRef(Token))); - llvm::DenseSet<Atom> VisitedTokens; + llvm::SetVector<BoolValue *> Constraints; + Constraints.insert(&arena().makeNot(Token)); + llvm::DenseSet<AtomicBoolValue *> VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); return isUnsatisfiable(std::move(Constraints)); } -bool DataflowAnalysisContext::equivalentFormulas(const Formula &Val1, - const Formula &Val2) { - llvm::SetVector<const Formula *> Constraints; +bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1, + BoolValue &Val2) { + llvm::SetVector<BoolValue*> Constraints; Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2))); return isUnsatisfiable(std::move(Constraints)); } void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( - Atom Token, llvm::SetVector<const Formula *> &Constraints, - llvm::DenseSet<Atom> &VisitedTokens) { - auto Res = VisitedTokens.insert(Token); + AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints, + llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) { + auto Res = VisitedTokens.insert(&Token); if (!Res.second) return; - auto ConstraintsIt = FlowConditionConstraints.find(Token); + auto ConstraintsIt = FlowConditionConstraints.find(&Token); if (ConstraintsIt == FlowConditionConstraints.end()) { - Constraints.insert(&arena().makeAtomRef(Token)); + Constraints.insert(&Token); } else { // Bind flow condition token via `iff` to its set of constraints: // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints - Constraints.insert(&arena().makeEquals(arena().makeAtomRef(Token), - *ConstraintsIt->second)); + Constraints.insert(&arena().makeEquals(Token, *ConstraintsIt->second)); } - auto DepsIt = FlowConditionDeps.find(Token); + auto DepsIt = FlowConditionDeps.find(&Token); if (DepsIt != FlowConditionDeps.end()) { - for (Atom DepToken : DepsIt->second) { - addTransitiveFlowConditionConstraints(DepToken, Constraints, + for (AtomicBoolValue *DepToken : DepsIt->second) { + addTransitiveFlowConditionConstraints(*DepToken, Constraints, VisitedTokens); } } } -void DataflowAnalysisContext::dumpFlowCondition(Atom Token, +void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token, llvm::raw_ostream &OS) { - llvm::SetVector<const Formula *> Constraints; - Constraints.insert(&arena().makeAtomRef(Token)); - llvm::DenseSet<Atom> VisitedTokens; + llvm::SetVector<BoolValue *> Constraints; + Constraints.insert(&Token); + llvm::DenseSet<AtomicBoolValue *> VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); - for (const auto *Constraint : Constraints) { - Constraint->print(OS); - OS << "\n"; - } + llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = { + {&arena().makeLiteral(false), "False"}, + {&arena().makeLiteral(true), "True"}}; + OS << debugString(Constraints.getArrayRef(), AtomNames); } const ControlFlowContext * diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp index 11bb7da..4a11c09 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp @@ -107,16 +107,15 @@ static Value *mergeDistinctValues(QualType Type, Value &Val1, // if (o.has_value()) // x = o.value(); // ``` - auto &Expr1 = cast<BoolValue>(Val1).formula(); - auto &Expr2 = cast<BoolValue>(Val2).formula(); - auto &A = MergedEnv.arena(); - auto &MergedVal = A.makeAtomRef(A.makeAtom()); - MergedEnv.addToFlowCondition( - A.makeOr(A.makeAnd(A.makeAtomRef(Env1.getFlowConditionToken()), - A.makeEquals(MergedVal, Expr1)), - A.makeAnd(A.makeAtomRef(Env2.getFlowConditionToken()), - A.makeEquals(MergedVal, Expr2)))); - return &A.makeBoolValue(MergedVal); + auto *Expr1 = cast<BoolValue>(&Val1); + auto *Expr2 = cast<BoolValue>(&Val2); + auto &MergedVal = MergedEnv.makeAtomicBoolValue(); + MergedEnv.addToFlowCondition(MergedEnv.makeOr( + MergedEnv.makeAnd(Env1.getFlowConditionToken(), + MergedEnv.makeIff(MergedVal, *Expr1)), + MergedEnv.makeAnd(Env2.getFlowConditionToken(), + MergedEnv.makeIff(MergedVal, *Expr2)))); + return &MergedVal; } // FIXME: Consider destroying `MergedValue` immediately if `ValueModel::merge` @@ -270,11 +269,11 @@ void Environment::initFieldsGlobalsAndFuncs(const FunctionDecl *FuncDecl) { Environment::Environment(DataflowAnalysisContext &DACtx) : DACtx(&DACtx), - FlowConditionToken(DACtx.arena().makeFlowConditionToken()) {} + FlowConditionToken(&DACtx.arena().makeFlowConditionToken()) {} Environment Environment::fork() const { Environment Copy(*this); - Copy.FlowConditionToken = DACtx->forkFlowCondition(FlowConditionToken); + Copy.FlowConditionToken = &DACtx->forkFlowCondition(*FlowConditionToken); return Copy; } @@ -588,8 +587,8 @@ Environment Environment::join(const Environment &EnvA, const Environment &EnvB, // FIXME: update join to detect backedges and simplify the flow condition // accordingly. - JoinedEnv.FlowConditionToken = EnvA.DACtx->joinFlowConditions( - EnvA.FlowConditionToken, EnvB.FlowConditionToken); + JoinedEnv.FlowConditionToken = &EnvA.DACtx->joinFlowConditions( + *EnvA.FlowConditionToken, *EnvB.FlowConditionToken); for (auto &Entry : EnvA.LocToVal) { const StorageLocation *Loc = Entry.first; @@ -820,7 +819,7 @@ Value *Environment::createValueUnlessSelfReferential( // with integers, and so distinguishing them serves no purpose, but could // prevent convergence. CreatedValuesCount++; - return &arena().create<IntegerValue>(); + return &DACtx->arena().create<IntegerValue>(); } if (Type->isReferenceType() || Type->isPointerType()) { @@ -838,9 +837,9 @@ Value *Environment::createValueUnlessSelfReferential( } if (Type->isReferenceType()) - return &arena().create<ReferenceValue>(PointeeLoc); + return &DACtx->arena().create<ReferenceValue>(PointeeLoc); else - return &arena().create<PointerValue>(PointeeLoc); + return &DACtx->arena().create<PointerValue>(PointeeLoc); } if (Type->isRecordType()) { @@ -860,7 +859,7 @@ Value *Environment::createValueUnlessSelfReferential( Visited.erase(FieldType.getCanonicalType()); } - return &arena().create<StructValue>(std::move(FieldValues)); + return &DACtx->arena().create<StructValue>(std::move(FieldValues)); } return nullptr; @@ -885,18 +884,12 @@ const StorageLocation &Environment::skip(const StorageLocation &Loc, return skip(*const_cast<StorageLocation *>(&Loc), SP); } -void Environment::addToFlowCondition(const Formula &Val) { - DACtx->addFlowConditionConstraint(FlowConditionToken, Val); -} void Environment::addToFlowCondition(BoolValue &Val) { - addToFlowCondition(Val.formula()); + DACtx->addFlowConditionConstraint(*FlowConditionToken, Val); } -bool Environment::flowConditionImplies(const Formula &Val) const { - return DACtx->flowConditionImplies(FlowConditionToken, Val); -} bool Environment::flowConditionImplies(BoolValue &Val) const { - return flowConditionImplies(Val.formula()); + return DACtx->flowConditionImplies(*FlowConditionToken, Val); } void Environment::dump(raw_ostream &OS) const { @@ -916,7 +909,7 @@ void Environment::dump(raw_ostream &OS) const { } OS << "FlowConditionToken:\n"; - DACtx->dumpFlowCondition(FlowConditionToken, OS); + DACtx->dumpFlowCondition(*FlowConditionToken, OS); } void Environment::dump() const { diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp index f8a049a..25225ed 100644 --- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp +++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp @@ -16,12 +16,22 @@ #include "clang/Analysis/FlowSensitive/DebugSupport.h" #include "clang/Analysis/FlowSensitive/Solver.h" #include "clang/Analysis/FlowSensitive/Value.h" +#include "llvm/ADT/DenseMap.h" +#include "llvm/ADT/STLExtras.h" #include "llvm/ADT/StringRef.h" +#include "llvm/ADT/StringSet.h" #include "llvm/Support/ErrorHandling.h" +#include "llvm/Support/FormatAdapters.h" +#include "llvm/Support/FormatCommon.h" +#include "llvm/Support/FormatVariadic.h" namespace clang { namespace dataflow { +using llvm::AlignStyle; +using llvm::fmt_pad; +using llvm::formatv; + llvm::StringRef debugString(Value::Kind Kind) { switch (Kind) { case Value::Kind::Integer: @@ -36,19 +46,26 @@ llvm::StringRef debugString(Value::Kind Kind) { return "AtomicBool"; case Value::Kind::TopBool: return "TopBool"; - case Value::Kind::FormulaBool: - return "FormulaBool"; + case Value::Kind::Conjunction: + return "Conjunction"; + case Value::Kind::Disjunction: + return "Disjunction"; + case Value::Kind::Negation: + return "Negation"; + case Value::Kind::Implication: + return "Implication"; + case Value::Kind::Biconditional: + return "Biconditional"; } llvm_unreachable("Unhandled value kind"); } -llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, - Solver::Result::Assignment Assignment) { +llvm::StringRef debugString(Solver::Result::Assignment Assignment) { switch (Assignment) { case Solver::Result::Assignment::AssignedFalse: - return OS << "False"; + return "False"; case Solver::Result::Assignment::AssignedTrue: - return OS << "True"; + return "True"; } llvm_unreachable("Booleans can only be assigned true/false"); } @@ -65,16 +82,174 @@ llvm::StringRef debugString(Solver::Result::Status Status) { llvm_unreachable("Unhandled SAT check result status"); } -llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Solver::Result &R) { - OS << debugString(R.getStatus()) << "\n"; - if (auto Solution = R.getSolution()) { - std::vector<std::pair<Atom, Solver::Result::Assignment>> Sorted = { - Solution->begin(), Solution->end()}; - llvm::sort(Sorted); - for (const auto &Entry : Sorted) - OS << Entry.first << " = " << Entry.second << "\n"; +namespace { + +class DebugStringGenerator { +public: + explicit DebugStringGenerator( + llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNamesArg) + : Counter(0), AtomNames(std::move(AtomNamesArg)) { +#ifndef NDEBUG + llvm::StringSet<> Names; + for (auto &N : AtomNames) { + assert(Names.insert(N.second).second && + "The same name must not assigned to different atoms"); + } +#endif + } + + /// Returns a string representation of a boolean value `B`. + std::string debugString(const BoolValue &B, size_t Depth = 0) { + std::string S; + switch (B.getKind()) { + case Value::Kind::AtomicBool: { + S = getAtomName(&cast<AtomicBoolValue>(B)); + break; + } + case Value::Kind::TopBool: { + S = "top"; + break; + } + case Value::Kind::Conjunction: { + auto &C = cast<ConjunctionValue>(B); + auto L = debugString(C.getLeftSubValue(), Depth + 1); + auto R = debugString(C.getRightSubValue(), Depth + 1); + S = formatv("(and\n{0}\n{1})", L, R); + break; + } + case Value::Kind::Disjunction: { + auto &D = cast<DisjunctionValue>(B); + auto L = debugString(D.getLeftSubValue(), Depth + 1); + auto R = debugString(D.getRightSubValue(), Depth + 1); + S = formatv("(or\n{0}\n{1})", L, R); + break; + } + case Value::Kind::Negation: { + auto &N = cast<NegationValue>(B); + S = formatv("(not\n{0})", debugString(N.getSubVal(), Depth + 1)); + break; + } + case Value::Kind::Implication: { + auto &IV = cast<ImplicationValue>(B); + auto L = debugString(IV.getLeftSubValue(), Depth + 1); + auto R = debugString(IV.getRightSubValue(), Depth + 1); + S = formatv("(=>\n{0}\n{1})", L, R); + break; + } + case Value::Kind::Biconditional: { + auto &BV = cast<BiconditionalValue>(B); + auto L = debugString(BV.getLeftSubValue(), Depth + 1); + auto R = debugString(BV.getRightSubValue(), Depth + 1); + S = formatv("(=\n{0}\n{1})", L, R); + break; + } + default: + llvm_unreachable("Unhandled value kind"); + } + auto Indent = Depth * 4; + return formatv("{0}", fmt_pad(S, Indent, 0)); + } + + std::string debugString(const llvm::ArrayRef<BoolValue *> &Constraints) { + std::string Result; + for (const BoolValue *S : Constraints) { + Result += debugString(*S); + Result += '\n'; + } + return Result; + } + + /// Returns a string representation of a set of boolean `Constraints` and the + /// `Result` of satisfiability checking on the `Constraints`. + std::string debugString(ArrayRef<BoolValue *> &Constraints, + const Solver::Result &Result) { + auto Template = R"( +Constraints +------------ +{0:$[ + +]} +------------ +{1}. +{2} +)"; + + std::vector<std::string> ConstraintsStrings; + ConstraintsStrings.reserve(Constraints.size()); + for (auto &Constraint : Constraints) { + ConstraintsStrings.push_back(debugString(*Constraint)); + } + + auto StatusString = clang::dataflow::debugString(Result.getStatus()); + auto Solution = Result.getSolution(); + auto SolutionString = Solution ? "\n" + debugString(*Solution) : ""; + + return formatv( + Template, + llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()), + StatusString, SolutionString); + } + +private: + /// Returns a string representation of a truth assignment to atom booleans. + std::string debugString( + const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> + &AtomAssignments) { + size_t MaxNameLength = 0; + for (auto &AtomName : AtomNames) { + MaxNameLength = std::max(MaxNameLength, AtomName.second.size()); + } + + std::vector<std::string> Lines; + for (auto &AtomAssignment : AtomAssignments) { + auto Line = formatv("{0} = {1}", + fmt_align(getAtomName(AtomAssignment.first), + AlignStyle::Left, MaxNameLength), + clang::dataflow::debugString(AtomAssignment.second)); + Lines.push_back(Line); + } + llvm::sort(Lines); + + return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end())); } - return OS; + + /// Returns the name assigned to `Atom`, either user-specified or created by + /// default rules (B0, B1, ...). + std::string getAtomName(const AtomicBoolValue *Atom) { + auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter)); + if (Entry.second) { + Counter++; + } + return Entry.first->second; + } + + // Keep track of number of atoms without a user-specified name, used to assign + // non-repeating default names to such atoms. + size_t Counter; + + // Keep track of names assigned to atoms. + llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames; +}; + +} // namespace + +std::string +debugString(const BoolValue &B, + llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { + return DebugStringGenerator(std::move(AtomNames)).debugString(B); +} + +std::string +debugString(llvm::ArrayRef<BoolValue *> Constraints, + llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { + return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints); +} + +std::string +debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result, + llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { + return DebugStringGenerator(std::move(AtomNames)) + .debugString(Constraints, Result); } } // namespace dataflow diff --git a/clang/lib/Analysis/FlowSensitive/Formula.cpp b/clang/lib/Analysis/FlowSensitive/Formula.cpp deleted file mode 100644 index 12f4e25..0000000 --- a/clang/lib/Analysis/FlowSensitive/Formula.cpp +++ /dev/null @@ -1,93 +0,0 @@ -//===- Formula.cpp ----------------------------------------------*- C++ -*-===// -// -// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. -// See https://llvm.org/LICENSE.txt for license information. -// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception -// -//===----------------------------------------------------------------------===// - -#include "clang/Analysis/FlowSensitive/Formula.h" -#include "clang/Basic/LLVM.h" -#include "llvm/ADT/STLExtras.h" -#include "llvm/ADT/StringRef.h" -#include "llvm/Support/Allocator.h" -#include "llvm/Support/ErrorHandling.h" -#include <cassert> - -namespace clang::dataflow { - -const Formula &Formula::create(llvm::BumpPtrAllocator &Alloc, Kind K, - ArrayRef<const Formula *> Operands, - unsigned Value) { - assert(Operands.size() == numOperands(K)); - if (Value != 0) // Currently, formulas have values or operands, not both. - assert(numOperands(K) == 0); - void *Mem = Alloc.Allocate(sizeof(Formula) + - Operands.size() * sizeof(Operands.front()), - alignof(Formula)); - Formula *Result = new (Mem) Formula(); - Result->FormulaKind = K; - Result->Value = Value; - // Operands are stored as `const Formula *`s after the formula itself. - // We don't need to construct an object as pointers are trivial types. - // Formula is alignas(const Formula *), so alignment is satisfied. - llvm::copy(Operands, reinterpret_cast<const Formula **>(Result + 1)); - return *Result; -} - -static llvm::StringLiteral sigil(Formula::Kind K) { - switch (K) { - case Formula::AtomRef: - case Formula::Literal: - return ""; - case Formula::Not: - return "!"; - case Formula::And: - return " & "; - case Formula::Or: - return " | "; - case Formula::Implies: - return " => "; - case Formula::Equal: - return " = "; - } - llvm_unreachable("unhandled formula kind"); -} - -void Formula::print(llvm::raw_ostream &OS, const AtomNames *Names) const { - if (Names && kind() == AtomRef) - if (auto It = Names->find(getAtom()); It != Names->end()) { - OS << It->second; - return; - } - - switch (numOperands(kind())) { - case 0: - switch (kind()) { - case AtomRef: - OS << getAtom(); - break; - case Literal: - OS << (literal() ? "true" : "false"); - break; - default: - llvm_unreachable("unhandled formula kind"); - } - break; - case 1: - OS << sigil(kind()); - operands()[0]->print(OS, Names); - break; - case 2: - OS << '('; - operands()[0]->print(OS, Names); - OS << sigil(kind()); - operands()[1]->print(OS, Names); - OS << ')'; - break; - default: - llvm_unreachable("unhandled formula arity"); - } -} - -} // namespace clang::dataflow
\ No newline at end of file diff --git a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp index 0c4e838..14293a3 100644 --- a/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp +++ b/clang/lib/Analysis/FlowSensitive/HTMLLogger.cpp @@ -97,7 +97,6 @@ public: case Value::Kind::Integer: case Value::Kind::TopBool: case Value::Kind::AtomicBool: - case Value::Kind::FormulaBool: break; case Value::Kind::Reference: JOS.attributeObject( @@ -112,6 +111,35 @@ public: JOS.attributeObject("f:" + Child.first->getNameAsString(), [&] { dump(*Child.second); }); break; + case Value::Kind::Disjunction: { + auto &VV = cast<DisjunctionValue>(V); + JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); }); + JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); }); + break; + } + case Value::Kind::Conjunction: { + auto &VV = cast<ConjunctionValue>(V); + JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); }); + JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); }); + break; + } + case Value::Kind::Negation: { + auto &VV = cast<NegationValue>(V); + JOS.attributeObject("not", [&] { dump(VV.getSubVal()); }); + break; + } + case Value::Kind::Implication: { + auto &VV = cast<ImplicationValue>(V); + JOS.attributeObject("if", [&] { dump(VV.getLeftSubValue()); }); + JOS.attributeObject("then", [&] { dump(VV.getRightSubValue()); }); + break; + } + case Value::Kind::Biconditional: { + auto &VV = cast<BiconditionalValue>(V); + JOS.attributeObject("lhs", [&] { dump(VV.getLeftSubValue()); }); + JOS.attributeObject("rhs", [&] { dump(VV.getRightSubValue()); }); + break; + } } for (const auto& Prop : V.properties()) @@ -121,12 +149,10 @@ 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<BoolValue>(&V)) { - JOS.attribute("formula", llvm::to_string(B->formula())); - JOS.attribute( - "truth", Env.flowConditionImplies(B->formula()) ? "true" - : Env.flowConditionImplies(Env.arena().makeNot(B->formula())) - ? "false" - : "unknown"); + JOS.attribute("truth", Env.flowConditionImplies(*B) ? "true" + : Env.flowConditionImplies(Env.makeNot(*B)) + ? "false" + : "unknown"); } } void dump(const StorageLocation &L) { diff --git a/clang/lib/Analysis/FlowSensitive/Transfer.cpp b/clang/lib/Analysis/FlowSensitive/Transfer.cpp index b9a2672..5ad176d 100644 --- a/clang/lib/Analysis/FlowSensitive/Transfer.cpp +++ b/clang/lib/Analysis/FlowSensitive/Transfer.cpp @@ -62,12 +62,64 @@ static BoolValue &evaluateBooleanEquality(const Expr &LHS, const Expr &RHS, return Env.makeAtomicBoolValue(); } +// Functionally updates `V` such that any instances of `TopBool` are replaced +// with fresh atomic bools. Note: This implementation assumes that `B` is a +// tree; if `B` is a DAG, it will lose any sharing between subvalues that was +// present in the original . +static BoolValue &unpackValue(BoolValue &V, Environment &Env); + +template <typename Derived, typename M> +BoolValue &unpackBinaryBoolValue(Environment &Env, BoolValue &B, M build) { + auto &V = *cast<Derived>(&B); + BoolValue &Left = V.getLeftSubValue(); + BoolValue &Right = V.getRightSubValue(); + BoolValue &ULeft = unpackValue(Left, Env); + BoolValue &URight = unpackValue(Right, Env); + + if (&ULeft == &Left && &URight == &Right) + return V; + + return (Env.*build)(ULeft, URight); +} + static BoolValue &unpackValue(BoolValue &V, Environment &Env) { - if (auto *Top = llvm::dyn_cast<TopBoolValue>(&V)) { - auto &A = Env.getDataflowAnalysisContext().arena(); - return A.makeBoolValue(A.makeAtomRef(Top->getAtom())); + switch (V.getKind()) { + case Value::Kind::Integer: + case Value::Kind::Reference: + case Value::Kind::Pointer: + case Value::Kind::Struct: + llvm_unreachable("BoolValue cannot have any of these kinds."); + + case Value::Kind::AtomicBool: + return V; + + case Value::Kind::TopBool: + // Unpack `TopBool` into a fresh atomic bool. + return Env.makeAtomicBoolValue(); + + case Value::Kind::Negation: { + auto &N = *cast<NegationValue>(&V); + BoolValue &Sub = N.getSubVal(); + BoolValue &USub = unpackValue(Sub, Env); + + if (&USub == &Sub) + return V; + return Env.makeNot(USub); + } + case Value::Kind::Conjunction: + return unpackBinaryBoolValue<ConjunctionValue>(Env, V, + &Environment::makeAnd); + case Value::Kind::Disjunction: + return unpackBinaryBoolValue<DisjunctionValue>(Env, V, + &Environment::makeOr); + case Value::Kind::Implication: + return unpackBinaryBoolValue<ImplicationValue>( + Env, V, &Environment::makeImplication); + case Value::Kind::Biconditional: + return unpackBinaryBoolValue<BiconditionalValue>(Env, V, + &Environment::makeIff); } - return V; + llvm_unreachable("All reachable cases in switch return"); } // Unpacks the value (if any) associated with `E` and updates `E` to the new diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp index bf48a1f..db2e1d6 100644 --- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp +++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp @@ -17,8 +17,8 @@ #include <queue> #include <vector> -#include "clang/Analysis/FlowSensitive/Formula.h" #include "clang/Analysis/FlowSensitive/Solver.h" +#include "clang/Analysis/FlowSensitive/Value.h" #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h" #include "llvm/ADT/ArrayRef.h" #include "llvm/ADT/DenseMap.h" @@ -79,7 +79,7 @@ using ClauseID = uint32_t; static constexpr ClauseID NullClause = 0; /// A boolean formula in conjunctive normal form. -struct CNFFormula { +struct BooleanFormula { /// `LargestVar` is equal to the largest positive integer that represents a /// variable in the formula. const Variable LargestVar; @@ -121,12 +121,12 @@ struct CNFFormula { /// clauses in the formula start from the element at index 1. std::vector<ClauseID> NextWatched; - /// Stores the variable identifier and Atom for atomic booleans in the - /// formula. - llvm::DenseMap<Variable, Atom> Atomics; + /// Stores the variable identifier and value location for atomic booleans in + /// the formula. + llvm::DenseMap<Variable, AtomicBoolValue *> Atomics; - explicit CNFFormula(Variable LargestVar, - llvm::DenseMap<Variable, Atom> Atomics) + explicit BooleanFormula(Variable LargestVar, + llvm::DenseMap<Variable, AtomicBoolValue *> Atomics) : LargestVar(LargestVar), Atomics(std::move(Atomics)) { Clauses.push_back(0); ClauseStarts.push_back(0); @@ -144,8 +144,8 @@ struct CNFFormula { /// /// All literals in the input that are not `NullLit` must be distinct. void addClause(Literal L1, Literal L2 = NullLit, Literal L3 = NullLit) { - // The literals are guaranteed to be distinct from properties of Formula - // and the construction in `buildCNF`. + // The literals are guaranteed to be distinct from properties of BoolValue + // and the construction in `buildBooleanFormula`. assert(L1 != NullLit && L1 != L2 && L1 != L3 && (L2 != L3 || L2 == NullLit)); @@ -178,59 +178,98 @@ struct CNFFormula { /// Converts the conjunction of `Vals` into a formula in conjunctive normal /// form where each clause has at least one and at most three literals. -CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) { +BooleanFormula buildBooleanFormula(const llvm::ArrayRef<BoolValue *> &Vals) { // The general strategy of the algorithm implemented below is to map each // of the sub-values in `Vals` to a unique variable and use these variables in // the resulting CNF expression to avoid exponential blow up. The number of // literals in the resulting formula is guaranteed to be linear in the number - // of sub-formulas in `Vals`. + // of sub-values in `Vals`. - // Map each sub-formula in `Vals` to a unique variable. - llvm::DenseMap<const Formula *, Variable> SubValsToVar; - // Store variable identifiers and Atom of atomic booleans. - llvm::DenseMap<Variable, Atom> Atomics; + // Map each sub-value in `Vals` to a unique variable. + llvm::DenseMap<BoolValue *, Variable> SubValsToVar; + // Store variable identifiers and value location of atomic booleans. + llvm::DenseMap<Variable, AtomicBoolValue *> Atomics; Variable NextVar = 1; { - std::queue<const Formula *> UnprocessedSubVals; - for (const Formula *Val : Vals) + std::queue<BoolValue *> UnprocessedSubVals; + for (BoolValue *Val : Vals) UnprocessedSubVals.push(Val); while (!UnprocessedSubVals.empty()) { Variable Var = NextVar; - const Formula *Val = UnprocessedSubVals.front(); + BoolValue *Val = UnprocessedSubVals.front(); UnprocessedSubVals.pop(); if (!SubValsToVar.try_emplace(Val, Var).second) continue; ++NextVar; - for (const Formula *F : Val->operands()) - UnprocessedSubVals.push(F); - if (Val->kind() == Formula::AtomRef) - Atomics[Var] = Val->getAtom(); + // Visit the sub-values of `Val`. + switch (Val->getKind()) { + case Value::Kind::Conjunction: { + auto *C = cast<ConjunctionValue>(Val); + UnprocessedSubVals.push(&C->getLeftSubValue()); + UnprocessedSubVals.push(&C->getRightSubValue()); + break; + } + case Value::Kind::Disjunction: { + auto *D = cast<DisjunctionValue>(Val); + UnprocessedSubVals.push(&D->getLeftSubValue()); + UnprocessedSubVals.push(&D->getRightSubValue()); + break; + } + case Value::Kind::Negation: { + auto *N = cast<NegationValue>(Val); + UnprocessedSubVals.push(&N->getSubVal()); + break; + } + case Value::Kind::Implication: { + auto *I = cast<ImplicationValue>(Val); + UnprocessedSubVals.push(&I->getLeftSubValue()); + UnprocessedSubVals.push(&I->getRightSubValue()); + break; + } + case Value::Kind::Biconditional: { + auto *B = cast<BiconditionalValue>(Val); + UnprocessedSubVals.push(&B->getLeftSubValue()); + UnprocessedSubVals.push(&B->getRightSubValue()); + break; + } + case Value::Kind::TopBool: + // Nothing more to do. This `TopBool` instance has already been mapped + // to a fresh solver variable (`NextVar`, above) and is thereafter + // anonymous. The solver never sees `Top`. + break; + case Value::Kind::AtomicBool: { + Atomics[Var] = cast<AtomicBoolValue>(Val); + break; + } + default: + llvm_unreachable("buildBooleanFormula: unhandled value kind"); + } } } - auto GetVar = [&SubValsToVar](const Formula *Val) { + auto GetVar = [&SubValsToVar](const BoolValue *Val) { auto ValIt = SubValsToVar.find(Val); assert(ValIt != SubValsToVar.end()); return ValIt->second; }; - CNFFormula CNF(NextVar - 1, std::move(Atomics)); + BooleanFormula Formula(NextVar - 1, std::move(Atomics)); std::vector<bool> ProcessedSubVals(NextVar, false); - // Add a conjunct for each variable that represents a top-level formula in - // `Vals`. - for (const Formula *Val : Vals) - CNF.addClause(posLit(GetVar(Val))); + // Add a conjunct for each variable that represents a top-level conjunction + // value in `Vals`. + for (BoolValue *Val : Vals) + Formula.addClause(posLit(GetVar(Val))); // Add conjuncts that represent the mapping between newly-created variables - // and their corresponding sub-formulas. - std::queue<const Formula *> UnprocessedSubVals; - for (const Formula *Val : Vals) + // and their corresponding sub-values. + std::queue<BoolValue *> UnprocessedSubVals; + for (BoolValue *Val : Vals) UnprocessedSubVals.push(Val); while (!UnprocessedSubVals.empty()) { - const Formula *Val = UnprocessedSubVals.front(); + const BoolValue *Val = UnprocessedSubVals.front(); UnprocessedSubVals.pop(); const Variable Var = GetVar(Val); @@ -238,110 +277,117 @@ CNFFormula buildCNF(const llvm::ArrayRef<const Formula *> &Vals) { continue; ProcessedSubVals[Var] = true; - switch (Val->kind()) { - case Formula::AtomRef: - break; - case Formula::Literal: - CNF.addClause(Val->literal() ? posLit(Var) : negLit(Var)); - break; - case Formula::And: { - const Variable LHS = GetVar(Val->operands()[0]); - const Variable RHS = GetVar(Val->operands()[1]); - - if (LHS == RHS) { + if (auto *C = dyn_cast<ConjunctionValue>(Val)) { + const Variable LeftSubVar = GetVar(&C->getLeftSubValue()); + const Variable RightSubVar = GetVar(&C->getRightSubValue()); + + if (LeftSubVar == RightSubVar) { // `X <=> (A ^ A)` is equivalent to `(!X v A) ^ (X v !A)` which is // already in conjunctive normal form. Below we add each of the // conjuncts of the latter expression to the result. - CNF.addClause(negLit(Var), posLit(LHS)); - CNF.addClause(posLit(Var), negLit(LHS)); + Formula.addClause(negLit(Var), posLit(LeftSubVar)); + Formula.addClause(posLit(Var), negLit(LeftSubVar)); + + // Visit a sub-value of `Val` (pick any, they are identical). + UnprocessedSubVals.push(&C->getLeftSubValue()); } else { // `X <=> (A ^ B)` is equivalent to `(!X v A) ^ (!X v B) ^ (X v !A v !B)` // which is already in conjunctive normal form. Below we add each of the // conjuncts of the latter expression to the result. - CNF.addClause(negLit(Var), posLit(LHS)); - CNF.addClause(negLit(Var), posLit(RHS)); - CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS)); + Formula.addClause(negLit(Var), posLit(LeftSubVar)); + Formula.addClause(negLit(Var), posLit(RightSubVar)); + Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar)); + + // Visit the sub-values of `Val`. + UnprocessedSubVals.push(&C->getLeftSubValue()); + UnprocessedSubVals.push(&C->getRightSubValue()); } - break; - } - case Formula::Or: { - const Variable LHS = GetVar(Val->operands()[0]); - const Variable RHS = GetVar(Val->operands()[1]); + } else if (auto *D = dyn_cast<DisjunctionValue>(Val)) { + const Variable LeftSubVar = GetVar(&D->getLeftSubValue()); + const Variable RightSubVar = GetVar(&D->getRightSubValue()); - if (LHS == RHS) { + if (LeftSubVar == RightSubVar) { // `X <=> (A v A)` is equivalent to `(!X v A) ^ (X v !A)` which is // already in conjunctive normal form. Below we add each of the // conjuncts of the latter expression to the result. - CNF.addClause(negLit(Var), posLit(LHS)); - CNF.addClause(posLit(Var), negLit(LHS)); + Formula.addClause(negLit(Var), posLit(LeftSubVar)); + Formula.addClause(posLit(Var), negLit(LeftSubVar)); + + // Visit a sub-value of `Val` (pick any, they are identical). + UnprocessedSubVals.push(&D->getLeftSubValue()); } else { - // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v - // !B)` which is already in conjunctive normal form. Below we add each - // of the conjuncts of the latter expression to the result. - CNF.addClause(negLit(Var), posLit(LHS), posLit(RHS)); - CNF.addClause(posLit(Var), negLit(LHS)); - CNF.addClause(posLit(Var), negLit(RHS)); + // `X <=> (A v B)` is equivalent to `(!X v A v B) ^ (X v !A) ^ (X v !B)` + // which is already in conjunctive normal form. Below we add each of the + // conjuncts of the latter expression to the result. + Formula.addClause(negLit(Var), posLit(LeftSubVar), posLit(RightSubVar)); + Formula.addClause(posLit(Var), negLit(LeftSubVar)); + Formula.addClause(posLit(Var), negLit(RightSubVar)); + + // Visit the sub-values of `Val`. + UnprocessedSubVals.push(&D->getLeftSubValue()); + UnprocessedSubVals.push(&D->getRightSubValue()); } - break; - } - case Formula::Not: { - const Variable Operand = GetVar(Val->operands()[0]); - - // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is - // already in conjunctive normal form. Below we add each of the - // conjuncts of the latter expression to the result. - CNF.addClause(negLit(Var), negLit(Operand)); - CNF.addClause(posLit(Var), posLit(Operand)); - break; - } - case Formula::Implies: { - const Variable LHS = GetVar(Val->operands()[0]); - const Variable RHS = GetVar(Val->operands()[1]); + } else if (auto *N = dyn_cast<NegationValue>(Val)) { + const Variable SubVar = GetVar(&N->getSubVal()); + + // `X <=> !Y` is equivalent to `(!X v !Y) ^ (X v Y)` which is already in + // conjunctive normal form. Below we add each of the conjuncts of the + // latter expression to the result. + Formula.addClause(negLit(Var), negLit(SubVar)); + Formula.addClause(posLit(Var), posLit(SubVar)); + + // Visit the sub-values of `Val`. + UnprocessedSubVals.push(&N->getSubVal()); + } else if (auto *I = dyn_cast<ImplicationValue>(Val)) { + const Variable LeftSubVar = GetVar(&I->getLeftSubValue()); + const Variable RightSubVar = GetVar(&I->getRightSubValue()); // `X <=> (A => B)` is equivalent to // `(X v A) ^ (X v !B) ^ (!X v !A v B)` which is already in - // conjunctive normal form. Below we add each of the conjuncts of - // the latter expression to the result. - CNF.addClause(posLit(Var), posLit(LHS)); - CNF.addClause(posLit(Var), negLit(RHS)); - CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS)); - break; - } - case Formula::Equal: { - const Variable LHS = GetVar(Val->operands()[0]); - const Variable RHS = GetVar(Val->operands()[1]); - - if (LHS == RHS) { + // conjunctive normal form. Below we add each of the conjuncts of the + // latter expression to the result. + Formula.addClause(posLit(Var), posLit(LeftSubVar)); + Formula.addClause(posLit(Var), negLit(RightSubVar)); + Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar)); + + // Visit the sub-values of `Val`. + UnprocessedSubVals.push(&I->getLeftSubValue()); + UnprocessedSubVals.push(&I->getRightSubValue()); + } else if (auto *B = dyn_cast<BiconditionalValue>(Val)) { + const Variable LeftSubVar = GetVar(&B->getLeftSubValue()); + const Variable RightSubVar = GetVar(&B->getRightSubValue()); + + if (LeftSubVar == RightSubVar) { // `X <=> (A <=> A)` is equvalent to `X` which is already in // conjunctive normal form. Below we add each of the conjuncts of the // latter expression to the result. - CNF.addClause(posLit(Var)); + Formula.addClause(posLit(Var)); // No need to visit the sub-values of `Val`. - continue; + } else { + // `X <=> (A <=> B)` is equivalent to + // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which is + // already in conjunctive normal form. Below we add each of the conjuncts + // of the latter expression to the result. + Formula.addClause(posLit(Var), posLit(LeftSubVar), posLit(RightSubVar)); + Formula.addClause(posLit(Var), negLit(LeftSubVar), negLit(RightSubVar)); + Formula.addClause(negLit(Var), posLit(LeftSubVar), negLit(RightSubVar)); + Formula.addClause(negLit(Var), negLit(LeftSubVar), posLit(RightSubVar)); + + // Visit the sub-values of `Val`. + UnprocessedSubVals.push(&B->getLeftSubValue()); + UnprocessedSubVals.push(&B->getRightSubValue()); } - // `X <=> (A <=> B)` is equivalent to - // `(X v A v B) ^ (X v !A v !B) ^ (!X v A v !B) ^ (!X v !A v B)` which - // is already in conjunctive normal form. Below we add each of the - // conjuncts of the latter expression to the result. - CNF.addClause(posLit(Var), posLit(LHS), posLit(RHS)); - CNF.addClause(posLit(Var), negLit(LHS), negLit(RHS)); - CNF.addClause(negLit(Var), posLit(LHS), negLit(RHS)); - CNF.addClause(negLit(Var), negLit(LHS), posLit(RHS)); - break; - } } - for (const Formula *Child : Val->operands()) - UnprocessedSubVals.push(Child); } - return CNF; + return Formula; } class WatchedLiteralsSolverImpl { /// A boolean formula in conjunctive normal form that the solver will attempt /// to prove satisfiable. The formula will be modified in the process. - CNFFormula CNF; + BooleanFormula Formula; /// The search for a satisfying assignment of the variables in `Formula` will /// proceed in levels, starting from 1 and going up to `Formula.LargestVar` @@ -393,10 +439,9 @@ class WatchedLiteralsSolverImpl { std::vector<Variable> ActiveVars; public: - explicit WatchedLiteralsSolverImpl( - const llvm::ArrayRef<const Formula *> &Vals) - : CNF(buildCNF(Vals)), LevelVars(CNF.LargestVar + 1), - LevelStates(CNF.LargestVar + 1) { + explicit WatchedLiteralsSolverImpl(const llvm::ArrayRef<BoolValue *> &Vals) + : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1), + LevelStates(Formula.LargestVar + 1) { assert(!Vals.empty()); // Initialize the state at the root level to a decision so that in @@ -405,10 +450,10 @@ public: LevelStates[0] = State::Decision; // Initialize all variables as unassigned. - VarAssignments.resize(CNF.LargestVar + 1, Assignment::Unassigned); + VarAssignments.resize(Formula.LargestVar + 1, Assignment::Unassigned); // Initialize the active variables. - for (Variable Var = CNF.LargestVar; Var != NullVar; --Var) { + for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) { if (isWatched(posLit(Var)) || isWatched(negLit(Var))) ActiveVars.push_back(Var); } @@ -429,7 +474,7 @@ public: // 3. Unassigned variables that form watched literals are active. // FIXME: Consider replacing these with test cases that fail if the any // of the invariants is broken. That might not be easy due to the - // transformations performed by `buildCNF`. + // transformations performed by `buildBooleanFormula`. assert(activeVarsAreUnassigned()); assert(activeVarsFormWatchedLiterals()); assert(unassignedVarsFormingWatchedLiteralsAreActive()); @@ -510,10 +555,12 @@ public: } private: - /// Returns a satisfying truth assignment to the atoms in the boolean formula. - llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() { - llvm::DenseMap<Atom, Solver::Result::Assignment> Solution; - for (auto &Atomic : CNF.Atomics) { + /// Returns a satisfying truth assignment to the atomic values in the boolean + /// formula. + llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> + buildSolution() { + llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> Solution; + for (auto &Atomic : Formula.Atomics) { // A variable may have a definite true/false assignment, or it may be // unassigned indicating its truth value does not affect the result of // the formula. Unassigned variables are assigned to true as a default. @@ -549,24 +596,24 @@ private: const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue ? negLit(Var) : posLit(Var); - ClauseID FalseLitWatcher = CNF.WatchedHead[FalseLit]; - CNF.WatchedHead[FalseLit] = NullClause; + ClauseID FalseLitWatcher = Formula.WatchedHead[FalseLit]; + Formula.WatchedHead[FalseLit] = NullClause; while (FalseLitWatcher != NullClause) { - const ClauseID NextFalseLitWatcher = CNF.NextWatched[FalseLitWatcher]; + const ClauseID NextFalseLitWatcher = Formula.NextWatched[FalseLitWatcher]; // Pick the first non-false literal as the new watched literal. - const size_t FalseLitWatcherStart = CNF.ClauseStarts[FalseLitWatcher]; + const size_t FalseLitWatcherStart = Formula.ClauseStarts[FalseLitWatcher]; size_t NewWatchedLitIdx = FalseLitWatcherStart + 1; - while (isCurrentlyFalse(CNF.Clauses[NewWatchedLitIdx])) + while (isCurrentlyFalse(Formula.Clauses[NewWatchedLitIdx])) ++NewWatchedLitIdx; - const Literal NewWatchedLit = CNF.Clauses[NewWatchedLitIdx]; + const Literal NewWatchedLit = Formula.Clauses[NewWatchedLitIdx]; const Variable NewWatchedLitVar = var(NewWatchedLit); // Swap the old watched literal for the new one in `FalseLitWatcher` to // maintain the invariant that the watched literal is at the beginning of // the clause. - CNF.Clauses[NewWatchedLitIdx] = FalseLit; - CNF.Clauses[FalseLitWatcherStart] = NewWatchedLit; + Formula.Clauses[NewWatchedLitIdx] = FalseLit; + Formula.Clauses[FalseLitWatcherStart] = NewWatchedLit; // If the new watched literal isn't watched by any other clause and its // variable isn't assigned we need to add it to the active variables. @@ -574,8 +621,8 @@ private: VarAssignments[NewWatchedLitVar] == Assignment::Unassigned) ActiveVars.push_back(NewWatchedLitVar); - CNF.NextWatched[FalseLitWatcher] = CNF.WatchedHead[NewWatchedLit]; - CNF.WatchedHead[NewWatchedLit] = FalseLitWatcher; + Formula.NextWatched[FalseLitWatcher] = Formula.WatchedHead[NewWatchedLit]; + Formula.WatchedHead[NewWatchedLit] = FalseLitWatcher; // Go to the next clause that watches `FalseLit`. FalseLitWatcher = NextFalseLitWatcher; @@ -585,15 +632,16 @@ private: /// Returns true if and only if one of the clauses that watch `Lit` is a unit /// clause. bool watchedByUnitClause(Literal Lit) const { - for (ClauseID LitWatcher = CNF.WatchedHead[Lit]; LitWatcher != NullClause; - LitWatcher = CNF.NextWatched[LitWatcher]) { - llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher); + for (ClauseID LitWatcher = Formula.WatchedHead[Lit]; + LitWatcher != NullClause; + LitWatcher = Formula.NextWatched[LitWatcher]) { + llvm::ArrayRef<Literal> Clause = Formula.clauseLiterals(LitWatcher); // Assert the invariant that the watched literal is always the first one // in the clause. // FIXME: Consider replacing this with a test case that fails if the // invariant is broken by `updateWatchedLiterals`. That might not be easy - // due to the transformations performed by `buildCNF`. + // due to the transformations performed by `buildBooleanFormula`. assert(Clause.front() == Lit); if (isUnit(Clause)) @@ -617,7 +665,7 @@ private: /// Returns true if and only if `Lit` is watched by a clause in `Formula`. bool isWatched(Literal Lit) const { - return CNF.WatchedHead[Lit] != NullClause; + return Formula.WatchedHead[Lit] != NullClause; } /// Returns an assignment for an unassigned variable. @@ -630,8 +678,8 @@ private: /// Returns a set of all watched literals. llvm::DenseSet<Literal> watchedLiterals() const { llvm::DenseSet<Literal> WatchedLiterals; - for (Literal Lit = 2; Lit < CNF.WatchedHead.size(); Lit++) { - if (CNF.WatchedHead[Lit] == NullClause) + for (Literal Lit = 2; Lit < Formula.WatchedHead.size(); Lit++) { + if (Formula.WatchedHead[Lit] == NullClause) continue; WatchedLiterals.insert(Lit); } @@ -671,8 +719,7 @@ private: } }; -Solver::Result -WatchedLiteralsSolver::solve(llvm::ArrayRef<const Formula *> Vals) { +Solver::Result WatchedLiteralsSolver::solve(llvm::ArrayRef<BoolValue *> Vals) { if (Vals.empty()) return Solver::Result::Satisfiable({{}}); auto [Res, Iterations] = diff --git a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp index 98c9cc4..407abf5 100644 --- a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp @@ -7,7 +7,6 @@ //===----------------------------------------------------------------------===// #include "clang/Analysis/FlowSensitive/Arena.h" -#include "llvm/Support/ScopedPrinter.h" #include "gmock/gmock.h" #include "gtest/gtest.h" @@ -20,20 +19,26 @@ protected: }; TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) { - auto &X = A.makeAtomValue(); - auto &Y = A.makeAtomValue(); + auto &X = A.create<AtomicBoolValue>(); + auto &Y = A.create<AtomicBoolValue>(); EXPECT_NE(&X, &Y); } TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) { - auto &X = A.makeTopValue(); - auto &Y = A.makeTopValue(); + auto &X = A.create<TopBoolValue>(); + auto &Y = A.create<TopBoolValue>(); EXPECT_NE(&X, &Y); } +TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) { + auto &X = A.create<AtomicBoolValue>(); + auto &XAndX = A.makeAnd(X, X); + EXPECT_EQ(&XAndX, &X); +} + TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) { - auto &X = A.makeAtomRef(A.makeAtom()); - auto &Y = A.makeAtomRef(A.makeAtom()); + auto &X = A.create<AtomicBoolValue>(); + auto &Y = A.create<AtomicBoolValue>(); auto &XAndY1 = A.makeAnd(X, Y); auto &XAndY2 = A.makeAnd(X, Y); EXPECT_EQ(&XAndY1, &XAndY2); @@ -41,14 +46,20 @@ TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) { auto &YAndX = A.makeAnd(Y, X); EXPECT_EQ(&XAndY1, &YAndX); - auto &Z = A.makeAtomRef(A.makeAtom()); + auto &Z = A.create<AtomicBoolValue>(); auto &XAndZ = A.makeAnd(X, Z); EXPECT_NE(&XAndY1, &XAndZ); } +TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) { + auto &X = A.create<AtomicBoolValue>(); + auto &XOrX = A.makeOr(X, X); + EXPECT_EQ(&XOrX, &X); +} + TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) { - auto &X = A.makeAtomRef(A.makeAtom()); - auto &Y = A.makeAtomRef(A.makeAtom()); + auto &X = A.create<AtomicBoolValue>(); + auto &Y = A.create<AtomicBoolValue>(); auto &XOrY1 = A.makeOr(X, Y); auto &XOrY2 = A.makeOr(X, Y); EXPECT_EQ(&XOrY1, &XOrY2); @@ -56,24 +67,31 @@ TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) { auto &YOrX = A.makeOr(Y, X); EXPECT_EQ(&XOrY1, &YOrX); - auto &Z = A.makeAtomRef(A.makeAtom()); + auto &Z = A.create<AtomicBoolValue>(); auto &XOrZ = A.makeOr(X, Z); EXPECT_NE(&XOrY1, &XOrZ); } TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) { - auto &X = A.makeAtomRef(A.makeAtom()); + auto &X = A.create<AtomicBoolValue>(); auto &NotX1 = A.makeNot(X); auto &NotX2 = A.makeNot(X); EXPECT_EQ(&NotX1, &NotX2); - auto &Y = A.makeAtomRef(A.makeAtom()); + + auto &Y = A.create<AtomicBoolValue>(); auto &NotY = A.makeNot(Y); EXPECT_NE(&NotX1, &NotY); } +TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) { + auto &X = A.create<AtomicBoolValue>(); + auto &XImpliesX = A.makeImplies(X, X); + EXPECT_EQ(&XImpliesX, &A.makeLiteral(true)); +} + TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) { - auto &X = A.makeAtomRef(A.makeAtom()); - auto &Y = A.makeAtomRef(A.makeAtom()); + auto &X = A.create<AtomicBoolValue>(); + auto &Y = A.create<AtomicBoolValue>(); auto &XImpliesY1 = A.makeImplies(X, Y); auto &XImpliesY2 = A.makeImplies(X, Y); EXPECT_EQ(&XImpliesY1, &XImpliesY2); @@ -81,14 +99,20 @@ TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) { auto &YImpliesX = A.makeImplies(Y, X); EXPECT_NE(&XImpliesY1, &YImpliesX); - auto &Z = A.makeAtomRef(A.makeAtom()); + auto &Z = A.create<AtomicBoolValue>(); auto &XImpliesZ = A.makeImplies(X, Z); EXPECT_NE(&XImpliesY1, &XImpliesZ); } +TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) { + auto &X = A.create<AtomicBoolValue>(); + auto &XIffX = A.makeEquals(X, X); + EXPECT_EQ(&XIffX, &A.makeLiteral(true)); +} + TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) { - auto &X = A.makeAtomRef(A.makeAtom()); - auto &Y = A.makeAtomRef(A.makeAtom()); + auto &X = A.create<AtomicBoolValue>(); + auto &Y = A.create<AtomicBoolValue>(); auto &XIffY1 = A.makeEquals(X, Y); auto &XIffY2 = A.makeEquals(X, Y); EXPECT_EQ(&XIffY1, &XIffY2); @@ -96,53 +120,10 @@ TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) { auto &YIffX = A.makeEquals(Y, X); EXPECT_EQ(&XIffY1, &YIffX); - auto &Z = A.makeAtomRef(A.makeAtom()); + auto &Z = A.create<AtomicBoolValue>(); auto &XIffZ = A.makeEquals(X, Z); EXPECT_NE(&XIffY1, &XIffZ); } -TEST_F(ArenaTest, Interning) { - Atom X = A.makeAtom(); - Atom Y = A.makeAtom(); - const Formula &F1 = A.makeAnd(A.makeAtomRef(X), A.makeAtomRef(Y)); - const Formula &F2 = A.makeAnd(A.makeAtomRef(Y), A.makeAtomRef(X)); - EXPECT_EQ(&F1, &F2); - BoolValue &B1 = A.makeBoolValue(F1); - BoolValue &B2 = A.makeBoolValue(F2); - EXPECT_EQ(&B1, &B2); - EXPECT_EQ(&B1.formula(), &F1); -} - -TEST_F(ArenaTest, IdentitySimplification) { - auto &X = A.makeAtomRef(A.makeAtom()); - - EXPECT_EQ(&X, &A.makeAnd(X, X)); - EXPECT_EQ(&X, &A.makeOr(X, X)); - EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, X)); - EXPECT_EQ(&A.makeLiteral(true), &A.makeEquals(X, X)); - EXPECT_EQ(&X, &A.makeNot(A.makeNot(X))); -} - -TEST_F(ArenaTest, LiteralSimplification) { - auto &X = A.makeAtomRef(A.makeAtom()); - - EXPECT_EQ(&X, &A.makeAnd(X, A.makeLiteral(true))); - EXPECT_EQ(&A.makeLiteral(false), &A.makeAnd(X, A.makeLiteral(false))); - - EXPECT_EQ(&A.makeLiteral(true), &A.makeOr(X, A.makeLiteral(true))); - EXPECT_EQ(&X, &A.makeOr(X, A.makeLiteral(false))); - - EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(X, A.makeLiteral(true))); - EXPECT_EQ(&A.makeNot(X), &A.makeImplies(X, A.makeLiteral(false))); - EXPECT_EQ(&X, &A.makeImplies(A.makeLiteral(true), X)); - EXPECT_EQ(&A.makeLiteral(true), &A.makeImplies(A.makeLiteral(false), X)); - - EXPECT_EQ(&X, &A.makeEquals(X, A.makeLiteral(true))); - EXPECT_EQ(&A.makeNot(X), &A.makeEquals(X, A.makeLiteral(false))); - - EXPECT_EQ(&A.makeLiteral(false), &A.makeNot(A.makeLiteral(true))); - EXPECT_EQ(&A.makeLiteral(true), &A.makeNot(A.makeLiteral(false))); -} - } // namespace } // namespace clang::dataflow diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp index f6e8b30..bb76648 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.makeTopValue(); - auto &Y = A.makeTopValue(); - EXPECT_FALSE(Context.equivalentFormulas(X.formula(), Y.formula())); + auto &X = A.create<TopBoolValue>(); + auto &Y = A.create<TopBoolValue>(); + EXPECT_FALSE(Context.equivalentBoolValues(X, Y)); } TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) { - Atom FC = A.makeFlowConditionToken(); - auto &C = A.makeAtomRef(A.makeAtom()); + auto &FC = A.makeFlowConditionToken(); + auto &C = A.create<AtomicBoolValue>(); EXPECT_FALSE(Context.flowConditionImplies(FC, C)); } TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) { - Atom FC = A.makeFlowConditionToken(); - auto &C = A.makeAtomRef(A.makeAtom()); + auto &FC = A.makeFlowConditionToken(); + auto &C = A.create<AtomicBoolValue>(); Context.addFlowConditionConstraint(FC, C); EXPECT_TRUE(Context.flowConditionImplies(FC, C)); } TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) { - Atom FC1 = A.makeFlowConditionToken(); - auto &C1 = A.makeAtomRef(A.makeAtom()); + auto &FC1 = A.makeFlowConditionToken(); + auto &C1 = A.create<AtomicBoolValue>(); Context.addFlowConditionConstraint(FC1, C1); // Forked flow condition inherits the constraints of its parent flow // condition. - Atom FC2 = Context.forkFlowCondition(FC1); + auto &FC2 = Context.forkFlowCondition(FC1); EXPECT_TRUE(Context.flowConditionImplies(FC2, C1)); // Adding a new constraint to the forked flow condition does not affect its // parent flow condition. - auto &C2 = A.makeAtomRef(A.makeAtom()); + auto &C2 = A.create<AtomicBoolValue>(); Context.addFlowConditionConstraint(FC2, C2); EXPECT_TRUE(Context.flowConditionImplies(FC2, C2)); EXPECT_FALSE(Context.flowConditionImplies(FC1, C2)); } TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) { - auto &C1 = A.makeAtomRef(A.makeAtom()); - auto &C2 = A.makeAtomRef(A.makeAtom()); - auto &C3 = A.makeAtomRef(A.makeAtom()); + auto &C1 = A.create<AtomicBoolValue>(); + auto &C2 = A.create<AtomicBoolValue>(); + auto &C3 = A.create<AtomicBoolValue>(); - Atom FC1 = A.makeFlowConditionToken(); + auto &FC1 = A.makeFlowConditionToken(); Context.addFlowConditionConstraint(FC1, C1); Context.addFlowConditionConstraint(FC1, C3); - Atom FC2 = A.makeFlowConditionToken(); + auto &FC2 = A.makeFlowConditionToken(); Context.addFlowConditionConstraint(FC2, C2); Context.addFlowConditionConstraint(FC2, C3); - Atom FC3 = Context.joinFlowConditions(FC1, FC2); + auto &FC3 = Context.joinFlowConditions(FC1, FC2); EXPECT_FALSE(Context.flowConditionImplies(FC3, C1)); EXPECT_FALSE(Context.flowConditionImplies(FC3, C2)); EXPECT_TRUE(Context.flowConditionImplies(FC3, C3)); @@ -85,77 +85,77 @@ TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) { TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) { // Fresh flow condition with empty/no constraints is always true. - Atom FC1 = A.makeFlowConditionToken(); + auto &FC1 = A.makeFlowConditionToken(); EXPECT_TRUE(Context.flowConditionIsTautology(FC1)); // Literal `true` is always true. - Atom FC2 = A.makeFlowConditionToken(); + auto &FC2 = A.makeFlowConditionToken(); Context.addFlowConditionConstraint(FC2, A.makeLiteral(true)); EXPECT_TRUE(Context.flowConditionIsTautology(FC2)); // Literal `false` is never true. - Atom FC3 = A.makeFlowConditionToken(); + auto &FC3 = A.makeFlowConditionToken(); Context.addFlowConditionConstraint(FC3, A.makeLiteral(false)); EXPECT_FALSE(Context.flowConditionIsTautology(FC3)); // We can't prove that an arbitrary bool A is always true... - auto &C1 = A.makeAtomRef(A.makeAtom()); - Atom FC4 = A.makeFlowConditionToken(); + auto &C1 = A.create<AtomicBoolValue>(); + auto &FC4 = A.makeFlowConditionToken(); Context.addFlowConditionConstraint(FC4, C1); EXPECT_FALSE(Context.flowConditionIsTautology(FC4)); // ... but we can prove A || !A is true. - Atom FC5 = A.makeFlowConditionToken(); + auto &FC5 = A.makeFlowConditionToken(); Context.addFlowConditionConstraint(FC5, A.makeOr(C1, A.makeNot(C1))); EXPECT_TRUE(Context.flowConditionIsTautology(FC5)); } TEST_F(DataflowAnalysisContextTest, EquivBoolVals) { - auto &X = A.makeAtomRef(A.makeAtom()); - auto &Y = A.makeAtomRef(A.makeAtom()); - auto &Z = A.makeAtomRef(A.makeAtom()); + auto &X = A.create<AtomicBoolValue>(); + auto &Y = A.create<AtomicBoolValue>(); + auto &Z = A.create<AtomicBoolValue>(); auto &True = A.makeLiteral(true); auto &False = A.makeLiteral(false); // X == X - EXPECT_TRUE(Context.equivalentFormulas(X, X)); + EXPECT_TRUE(Context.equivalentBoolValues(X, X)); // X != Y - EXPECT_FALSE(Context.equivalentFormulas(X, Y)); + EXPECT_FALSE(Context.equivalentBoolValues(X, Y)); // !X != X - EXPECT_FALSE(Context.equivalentFormulas(A.makeNot(X), X)); + EXPECT_FALSE(Context.equivalentBoolValues(A.makeNot(X), X)); // !(!X) = X - EXPECT_TRUE(Context.equivalentFormulas(A.makeNot(A.makeNot(X)), X)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeNot(A.makeNot(X)), X)); // (X || X) == X - EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, X), X)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, X), X)); // (X || Y) != X - EXPECT_FALSE(Context.equivalentFormulas(A.makeOr(X, Y), X)); + EXPECT_FALSE(Context.equivalentBoolValues(A.makeOr(X, Y), X)); // (X || True) == True - EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, True), True)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, True), True)); // (X || False) == X - EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, False), X)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, False), X)); // (X && X) == X - EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, X), X)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, X), X)); // (X && Y) != X - EXPECT_FALSE(Context.equivalentFormulas(A.makeAnd(X, Y), X)); + EXPECT_FALSE(Context.equivalentBoolValues(A.makeAnd(X, Y), X)); // (X && True) == X - EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, True), X)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, True), X)); // (X && False) == False - EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, False), False)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, False), False)); // (X || Y) == (Y || X) - EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(X, Y), A.makeOr(Y, X))); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, Y), A.makeOr(Y, X))); // (X && Y) == (Y && X) - EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(X, Y), A.makeAnd(Y, X))); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, Y), A.makeAnd(Y, X))); // ((X || Y) || Z) == (X || (Y || Z)) - EXPECT_TRUE(Context.equivalentFormulas(A.makeOr(A.makeOr(X, Y), Z), - A.makeOr(X, A.makeOr(Y, Z)))); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(A.makeOr(X, Y), Z), + A.makeOr(X, A.makeOr(Y, Z)))); // ((X && Y) && Z) == (X && (Y && Z)) - EXPECT_TRUE(Context.equivalentFormulas(A.makeAnd(A.makeAnd(X, Y), Z), - A.makeAnd(X, A.makeAnd(Y, Z)))); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(A.makeAnd(X, Y), Z), + A.makeAnd(X, A.makeAnd(Y, Z)))); } } // namespace diff --git a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp index cf266f4..10fcd20 100644 --- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp @@ -8,9 +8,8 @@ #include "clang/Analysis/FlowSensitive/DebugSupport.h" #include "TestingSupport.h" -#include "clang/Analysis/FlowSensitive/Formula.h" -#include "llvm/Support/ScopedPrinter.h" -#include "llvm/Support/raw_ostream.h" +#include "clang/Analysis/FlowSensitive/Value.h" +#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h" #include "gmock/gmock.h" #include "gtest/gtest.h" @@ -23,92 +22,429 @@ using test::ConstraintContext; using testing::StrEq; TEST(BoolValueDebugStringTest, AtomicBoolean) { + // B0 ConstraintContext Ctx; auto B = Ctx.atom(); - auto Expected = "V0"; - EXPECT_THAT(llvm::to_string(*B), StrEq(Expected)); + auto Expected = R"(B0)"; + EXPECT_THAT(debugString(*B), StrEq(Expected)); } -TEST(BoolValueDebugStringTest, Literal) { +TEST(BoolValueDebugStringTest, Top) { ConstraintContext Ctx; - EXPECT_EQ("true", llvm::to_string(*Ctx.literal(true))); - EXPECT_EQ("false", llvm::to_string(*Ctx.literal(false))); + auto B = Ctx.top(); + + auto Expected = R"(top)"; + EXPECT_THAT(debugString(*B), StrEq(Expected)); } TEST(BoolValueDebugStringTest, Negation) { + // !B0 ConstraintContext Ctx; auto B = Ctx.neg(Ctx.atom()); - auto Expected = "!V0"; - EXPECT_THAT(llvm::to_string(*B), StrEq(Expected)); + auto Expected = R"((not + B0))"; + EXPECT_THAT(debugString(*B), StrEq(Expected)); } TEST(BoolValueDebugStringTest, Conjunction) { + // B0 ^ B1 ConstraintContext Ctx; - auto *V0 = Ctx.atom(); - auto *V1 = Ctx.atom(); - EXPECT_EQ("(V0 & V1)", llvm::to_string(*Ctx.conj(V0, V1))); + auto B = Ctx.conj(Ctx.atom(), Ctx.atom()); + + auto Expected = R"((and + B0 + B1))"; + EXPECT_THAT(debugString(*B), StrEq(Expected)); } TEST(BoolValueDebugStringTest, Disjunction) { + // B0 v B1 ConstraintContext Ctx; - auto *V0 = Ctx.atom(); - auto *V1 = Ctx.atom(); - EXPECT_EQ("(V0 | V1)", llvm::to_string(*Ctx.disj(V0, V1))); + auto B = Ctx.disj(Ctx.atom(), Ctx.atom()); + + auto Expected = R"((or + B0 + B1))"; + EXPECT_THAT(debugString(*B), StrEq(Expected)); } TEST(BoolValueDebugStringTest, Implication) { + // B0 => B1 ConstraintContext Ctx; - auto *V0 = Ctx.atom(); - auto *V1 = Ctx.atom(); - EXPECT_EQ("(V0 => V1)", llvm::to_string(*Ctx.impl(V0, V1))); + auto B = Ctx.impl(Ctx.atom(), Ctx.atom()); + + auto Expected = R"((=> + B0 + B1))"; + EXPECT_THAT(debugString(*B), StrEq(Expected)); } TEST(BoolValueDebugStringTest, Iff) { + // B0 <=> B1 ConstraintContext Ctx; - auto *V0 = Ctx.atom(); - auto *V1 = Ctx.atom(); - EXPECT_EQ("(V0 = V1)", llvm::to_string(*Ctx.iff(V0, V1))); + auto B = Ctx.iff(Ctx.atom(), Ctx.atom()); + + auto Expected = R"((= + B0 + B1))"; + EXPECT_THAT(debugString(*B), StrEq(Expected)); } TEST(BoolValueDebugStringTest, Xor) { + // (B0 ^ !B1) V (!B0 ^ B1) ConstraintContext Ctx; - auto V0 = Ctx.atom(); - auto V1 = Ctx.atom(); - auto B = Ctx.disj(Ctx.conj(V0, Ctx.neg(V1)), Ctx.conj(Ctx.neg(V0), V1)); + auto B0 = Ctx.atom(); + auto B1 = Ctx.atom(); + auto B = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1)); - auto Expected = "((V0 & !V1) | (!V0 & V1))"; - EXPECT_THAT(llvm::to_string(*B), StrEq(Expected)); + auto Expected = R"((or + (and + B0 + (not + B1)) + (and + (not + B0) + B1)))"; + EXPECT_THAT(debugString(*B), StrEq(Expected)); } TEST(BoolValueDebugStringTest, NestedBoolean) { + // B0 ^ (B1 v (B2 ^ (B3 v B4))) + ConstraintContext Ctx; + auto B = Ctx.conj( + Ctx.atom(), + Ctx.disj(Ctx.atom(), + Ctx.conj(Ctx.atom(), Ctx.disj(Ctx.atom(), Ctx.atom())))); + + auto Expected = R"((and + B0 + (or + B1 + (and + B2 + (or + B3 + B4)))))"; + EXPECT_THAT(debugString(*B), StrEq(Expected)); +} + +TEST(BoolValueDebugStringTest, AtomicBooleanWithName) { + // True ConstraintContext Ctx; - auto V0 = Ctx.atom(); - auto V1 = Ctx.atom(); - auto V2 = Ctx.atom(); - auto V3 = Ctx.atom(); - auto V4 = Ctx.atom(); - auto B = Ctx.conj(V0, Ctx.disj(V1, Ctx.conj(V2, Ctx.disj(V3, V4)))); + auto True = cast<AtomicBoolValue>(Ctx.atom()); + auto B = True; - auto Expected = "(V0 & (V1 | (V2 & (V3 | V4))))"; - EXPECT_THAT(llvm::to_string(*B), StrEq(Expected)); + auto Expected = R"(True)"; + EXPECT_THAT(debugString(*B, {{True, "True"}}), StrEq(Expected)); +} + +TEST(BoolValueDebugStringTest, ComplexBooleanWithNames) { + // (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else) + ConstraintContext Ctx; + auto Cond = cast<AtomicBoolValue>(Ctx.atom()); + auto Then = cast<AtomicBoolValue>(Ctx.atom()); + auto Else = cast<AtomicBoolValue>(Ctx.atom()); + auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))), + Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else))); + + auto Expected = R"((or + (and + Cond + (and + Then + (not + Else))) + (and + (not + Cond) + (and + (not + Then) + Else))))"; + EXPECT_THAT(debugString(*B, {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}), + StrEq(Expected)); } TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) { + // (False && B0) v (True v B1) + ConstraintContext Ctx; + auto True = cast<AtomicBoolValue>(Ctx.atom()); + auto False = cast<AtomicBoolValue>(Ctx.atom()); + auto B = Ctx.disj(Ctx.conj(False, Ctx.atom()), Ctx.disj(True, Ctx.atom())); + + auto Expected = R"((or + (and + False + B0) + (or + True + B1)))"; + EXPECT_THAT(debugString(*B, {{True, "True"}, {False, "False"}}), + StrEq(Expected)); +} + +TEST(ConstraintSetDebugStringTest, Empty) { + llvm::ArrayRef<BoolValue *> Constraints; + EXPECT_THAT(debugString(Constraints), StrEq("")); +} + +TEST(ConstraintSetDebugStringTest, Simple) { + ConstraintContext Ctx; + std::vector<BoolValue *> Constraints; + auto X = cast<AtomicBoolValue>(Ctx.atom()); + auto Y = cast<AtomicBoolValue>(Ctx.atom()); + Constraints.push_back(Ctx.disj(X, Y)); + Constraints.push_back(Ctx.disj(X, Ctx.neg(Y))); + + auto Expected = R"((or + X + Y) +(or + X + (not + Y)) +)"; + EXPECT_THAT(debugString(Constraints, {{X, "X"}, {Y, "Y"}}), + StrEq(Expected)); +} + +Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) { + return WatchedLiteralsSolver().solve(std::move(Constraints)); +} + +TEST(SATCheckDebugStringTest, AtomicBoolean) { + // B0 + ConstraintContext Ctx; + std::vector<BoolValue *> Constraints({Ctx.atom()}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +B0 +------------ +Satisfiable. + +B0 = True +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST(SATCheckDebugStringTest, AtomicBooleanAndNegation) { + // B0, !B0 + ConstraintContext Ctx; + auto B0 = Ctx.atom(); + std::vector<BoolValue *> Constraints({B0, Ctx.neg(B0)}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +B0 + +(not + B0) +------------ +Unsatisfiable. + +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST(SATCheckDebugStringTest, MultipleAtomicBooleans) { + // B0, B1 + ConstraintContext Ctx; + std::vector<BoolValue *> Constraints({Ctx.atom(), Ctx.atom()}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +B0 + +B1 +------------ +Satisfiable. + +B0 = True +B1 = True +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST(SATCheckDebugStringTest, Implication) { + // B0, B0 => B1 + ConstraintContext Ctx; + auto B0 = Ctx.atom(); + auto B1 = Ctx.atom(); + auto Impl = Ctx.disj(Ctx.neg(B0), B1); + std::vector<BoolValue *> Constraints({B0, Impl}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +B0 + +(or + (not + B0) + B1) +------------ +Satisfiable. + +B0 = True +B1 = True +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST(SATCheckDebugStringTest, Iff) { + // B0, B0 <=> B1 + ConstraintContext Ctx; + auto B0 = Ctx.atom(); + auto B1 = Ctx.atom(); + auto Iff = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1))); + std::vector<BoolValue *> Constraints({B0, Iff}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +B0 + +(and + (or + (not + B0) + B1) + (or + B0 + (not + B1))) +------------ +Satisfiable. + +B0 = True +B1 = True +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); +} + +TEST(SATCheckDebugStringTest, Xor) { + // B0, XOR(B0, B1) ConstraintContext Ctx; - auto X = Ctx.atom(); - auto Y = Ctx.atom(); - Formula::AtomNames Names; - Names[X->getAtom()] = "X"; - Names[Y->getAtom()] = "Y"; - auto B = Ctx.disj(Ctx.conj(Y, Ctx.atom()), Ctx.disj(X, Ctx.atom())); + auto B0 = Ctx.atom(); + auto B1 = Ctx.atom(); + auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1)); + std::vector<BoolValue *> Constraints({B0, XOR}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +B0 + +(or + (and + B0 + (not + B1)) + (and + (not + B0) + B1)) +------------ +Satisfiable. - auto Expected = R"(((Y & V2) | (X | V3)))"; - std::string Actual; - llvm::raw_string_ostream OS(Actual); - B->print(OS, &Names); - EXPECT_THAT(Actual, StrEq(Expected)); +B0 = True +B1 = False +)"; + EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected)); } +TEST(SATCheckDebugStringTest, ComplexBooleanWithNames) { + // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else) + ConstraintContext Ctx; + auto Cond = cast<AtomicBoolValue>(Ctx.atom()); + auto Then = cast<AtomicBoolValue>(Ctx.atom()); + auto Else = cast<AtomicBoolValue>(Ctx.atom()); + auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))), + Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else))); + std::vector<BoolValue *> Constraints({Cond, B}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +Cond + +(or + (and + Cond + (and + Then + (not + Else))) + (and + (not + Cond) + (and + (not + Then) + Else))) +------------ +Satisfiable. + +Cond = True +Else = False +Then = True +)"; + EXPECT_THAT(debugString(Constraints, Result, + {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}), + StrEq(Expected)); +} + +TEST(SATCheckDebugStringTest, ComplexBooleanWithLongNames) { + // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq + ConstraintContext Ctx; + auto IntsAreEq = cast<AtomicBoolValue>(Ctx.atom()); + auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom()); + auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom()); + auto BothZeroImpliesEQ = + Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq); + std::vector<BoolValue *> Constraints( + {ThisIntEqZero, Ctx.neg(IntsAreEq), BothZeroImpliesEQ}); + auto Result = CheckSAT(Constraints); + + auto Expected = R"( +Constraints +------------ +ThisIntEqZero + +(not + IntsAreEq) + +(or + (not + (and + ThisIntEqZero + OtherIntEqZero)) + IntsAreEq) +------------ +Satisfiable. + +IntsAreEq = False +OtherIntEqZero = False +ThisIntEqZero = True +)"; + EXPECT_THAT(debugString(Constraints, Result, + {{IntsAreEq, "IntsAreEq"}, + {ThisIntEqZero, "ThisIntEqZero"}, + {OtherIntEqZero, "OtherIntEqZero"}}), + StrEq(Expected)); +} } // namespace diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp index ba0a77a..9999dd3a 100644 --- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp @@ -9,10 +9,9 @@ #include <utility> #include "TestingSupport.h" -#include "clang/Analysis/FlowSensitive/Formula.h" #include "clang/Analysis/FlowSensitive/Solver.h" +#include "clang/Analysis/FlowSensitive/Value.h" #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h" -#include "llvm/ADT/ArrayRef.h" #include "gmock/gmock.h" #include "gtest/gtest.h" @@ -24,31 +23,26 @@ using namespace dataflow; using test::ConstraintContext; using testing::_; using testing::AnyOf; +using testing::IsEmpty; +using testing::Optional; using testing::Pair; using testing::UnorderedElementsAre; -constexpr auto AssignedTrue = Solver::Result::Assignment::AssignedTrue; -constexpr auto AssignedFalse = Solver::Result::Assignment::AssignedFalse; - // Checks if the conjunction of `Vals` is satisfiable and returns the // corresponding result. -Solver::Result solve(llvm::ArrayRef<const Formula *> Vals) { +Solver::Result solve(llvm::ArrayRef<BoolValue *> Vals) { return WatchedLiteralsSolver().solve(Vals); } -MATCHER(unsat, "") { - return arg.getStatus() == Solver::Result::Status::Unsatisfiable; +void expectUnsatisfiable(Solver::Result Result) { + EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable); + EXPECT_FALSE(Result.getSolution().has_value()); } -MATCHER_P(sat, SolutionMatcher, - "is satisfiable, where solution " + - (testing::DescribeMatcher< - llvm::DenseMap<Atom, Solver::Result::Assignment>>( - SolutionMatcher))) { - if (arg.getStatus() != Solver::Result::Status::Satisfiable) - return false; - auto Solution = *arg.getSolution(); - return testing::ExplainMatchResult(SolutionMatcher, Solution, - result_listener); + +template <typename Matcher> +void expectSatisfiable(Solver::Result Result, Matcher Solution) { + EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable); + EXPECT_THAT(Result.getSolution(), Optional(Solution)); } TEST(SolverTest, Var) { @@ -56,8 +50,9 @@ TEST(SolverTest, Var) { auto X = Ctx.atom(); // X - EXPECT_THAT(solve({X}), - sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue)))); + expectSatisfiable( + solve({X}), + UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue))); } TEST(SolverTest, NegatedVar) { @@ -66,8 +61,9 @@ TEST(SolverTest, NegatedVar) { auto NotX = Ctx.neg(X); // !X - EXPECT_THAT(solve({NotX}), - sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse)))); + expectSatisfiable( + solve({NotX}), + UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse))); } TEST(SolverTest, UnitConflict) { @@ -76,7 +72,7 @@ TEST(SolverTest, UnitConflict) { auto NotX = Ctx.neg(X); // X ^ !X - EXPECT_THAT(solve({X, NotX}), unsat()); + expectUnsatisfiable(solve({X, NotX})); } TEST(SolverTest, DistinctVars) { @@ -86,9 +82,36 @@ TEST(SolverTest, DistinctVars) { auto NotY = Ctx.neg(Y); // X ^ !Y - EXPECT_THAT(solve({X, NotY}), - sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue), - Pair(Y->getAtom(), AssignedFalse)))); + expectSatisfiable( + solve({X, NotY}), + UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue), + Pair(Y, Solver::Result::Assignment::AssignedFalse))); +} + +TEST(SolverTest, Top) { + ConstraintContext Ctx; + auto X = Ctx.top(); + + // X. Since Top is anonymous, we do not get any results in the solution. + expectSatisfiable(solve({X}), IsEmpty()); +} + +TEST(SolverTest, NegatedTop) { + ConstraintContext Ctx; + auto X = Ctx.top(); + + // !X + expectSatisfiable(solve({Ctx.neg(X)}), IsEmpty()); +} + +TEST(SolverTest, DistinctTops) { + ConstraintContext Ctx; + auto X = Ctx.top(); + auto Y = Ctx.top(); + auto NotY = Ctx.neg(Y); + + // X ^ !Y + expectSatisfiable(solve({X, NotY}), IsEmpty()); } TEST(SolverTest, DoubleNegation) { @@ -98,7 +121,7 @@ TEST(SolverTest, DoubleNegation) { auto NotNotX = Ctx.neg(NotX); // !!X ^ !X - EXPECT_THAT(solve({NotNotX, NotX}), unsat()); + expectUnsatisfiable(solve({NotNotX, NotX})); } TEST(SolverTest, NegatedDisjunction) { @@ -109,7 +132,7 @@ TEST(SolverTest, NegatedDisjunction) { auto NotXOrY = Ctx.neg(XOrY); // !(X v Y) ^ (X v Y) - EXPECT_THAT(solve({NotXOrY, XOrY}), unsat()); + expectUnsatisfiable(solve({NotXOrY, XOrY})); } TEST(SolverTest, NegatedConjunction) { @@ -120,7 +143,7 @@ TEST(SolverTest, NegatedConjunction) { auto NotXAndY = Ctx.neg(XAndY); // !(X ^ Y) ^ (X ^ Y) - EXPECT_THAT(solve({NotXAndY, XAndY}), unsat()); + expectUnsatisfiable(solve({NotXAndY, XAndY})); } TEST(SolverTest, DisjunctionSameVarWithNegation) { @@ -130,7 +153,7 @@ TEST(SolverTest, DisjunctionSameVarWithNegation) { auto XOrNotX = Ctx.disj(X, NotX); // X v !X - EXPECT_THAT(solve({XOrNotX}), sat(_)); + expectSatisfiable(solve({XOrNotX}), _); } TEST(SolverTest, DisjunctionSameVar) { @@ -139,7 +162,7 @@ TEST(SolverTest, DisjunctionSameVar) { auto XOrX = Ctx.disj(X, X); // X v X - EXPECT_THAT(solve({XOrX}), sat(_)); + expectSatisfiable(solve({XOrX}), _); } TEST(SolverTest, ConjunctionSameVarsConflict) { @@ -149,7 +172,7 @@ TEST(SolverTest, ConjunctionSameVarsConflict) { auto XAndNotX = Ctx.conj(X, NotX); // X ^ !X - EXPECT_THAT(solve({XAndNotX}), unsat()); + expectUnsatisfiable(solve({XAndNotX})); } TEST(SolverTest, ConjunctionSameVar) { @@ -158,7 +181,7 @@ TEST(SolverTest, ConjunctionSameVar) { auto XAndX = Ctx.conj(X, X); // X ^ X - EXPECT_THAT(solve({XAndX}), sat(_)); + expectSatisfiable(solve({XAndX}), _); } TEST(SolverTest, PureVar) { @@ -171,9 +194,10 @@ TEST(SolverTest, PureVar) { auto NotXOrNotY = Ctx.disj(NotX, NotY); // (!X v Y) ^ (!X v !Y) - EXPECT_THAT(solve({NotXOrY, NotXOrNotY}), - sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse), - Pair(Y->getAtom(), _)))); + expectSatisfiable( + solve({NotXOrY, NotXOrNotY}), + UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse), + Pair(Y, _))); } TEST(SolverTest, MustAssumeVarIsFalse) { @@ -187,9 +211,10 @@ TEST(SolverTest, MustAssumeVarIsFalse) { auto NotXOrNotY = Ctx.disj(NotX, NotY); // (X v Y) ^ (!X v Y) ^ (!X v !Y) - EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY}), - sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse), - Pair(Y->getAtom(), AssignedTrue)))); + expectSatisfiable( + solve({XOrY, NotXOrY, NotXOrNotY}), + UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedFalse), + Pair(Y, Solver::Result::Assignment::AssignedTrue))); } TEST(SolverTest, DeepConflict) { @@ -204,7 +229,7 @@ TEST(SolverTest, DeepConflict) { auto XOrNotY = Ctx.disj(X, NotY); // (X v Y) ^ (!X v Y) ^ (!X v !Y) ^ (X v !Y) - EXPECT_THAT(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY}), unsat()); + expectUnsatisfiable(solve({XOrY, NotXOrY, NotXOrNotY, XOrNotY})); } TEST(SolverTest, IffIsEquivalentToDNF) { @@ -218,7 +243,7 @@ TEST(SolverTest, IffIsEquivalentToDNF) { auto NotEquivalent = Ctx.neg(Ctx.iff(XIffY, XIffYDNF)); // !((X <=> Y) <=> ((X ^ Y) v (!X ^ !Y))) - EXPECT_THAT(solve({NotEquivalent}), unsat()); + expectUnsatisfiable(solve({NotEquivalent})); } TEST(SolverTest, IffSameVars) { @@ -227,7 +252,7 @@ TEST(SolverTest, IffSameVars) { auto XEqX = Ctx.iff(X, X); // X <=> X - EXPECT_THAT(solve({XEqX}), sat(_)); + expectSatisfiable(solve({XEqX}), _); } TEST(SolverTest, IffDistinctVars) { @@ -237,12 +262,14 @@ TEST(SolverTest, IffDistinctVars) { auto XEqY = Ctx.iff(X, Y); // X <=> Y - EXPECT_THAT( + expectSatisfiable( solve({XEqY}), - sat(AnyOf(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue), - Pair(Y->getAtom(), AssignedTrue)), - UnorderedElementsAre(Pair(X->getAtom(), AssignedFalse), - Pair(Y->getAtom(), AssignedFalse))))); + AnyOf(UnorderedElementsAre( + Pair(X, Solver::Result::Assignment::AssignedTrue), + Pair(Y, Solver::Result::Assignment::AssignedTrue)), + UnorderedElementsAre( + Pair(X, Solver::Result::Assignment::AssignedFalse), + Pair(Y, Solver::Result::Assignment::AssignedFalse)))); } TEST(SolverTest, IffWithUnits) { @@ -252,9 +279,10 @@ TEST(SolverTest, IffWithUnits) { auto XEqY = Ctx.iff(X, Y); // (X <=> Y) ^ X ^ Y - EXPECT_THAT(solve({XEqY, X, Y}), - sat(UnorderedElementsAre(Pair(X->getAtom(), AssignedTrue), - Pair(Y->getAtom(), AssignedTrue)))); + expectSatisfiable( + solve({XEqY, X, Y}), + UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue), + Pair(Y, Solver::Result::Assignment::AssignedTrue))); } TEST(SolverTest, IffWithUnitsConflict) { @@ -265,7 +293,7 @@ TEST(SolverTest, IffWithUnitsConflict) { auto NotY = Ctx.neg(Y); // (X <=> Y) ^ X !Y - EXPECT_THAT(solve({XEqY, X, NotY}), unsat()); + expectUnsatisfiable(solve({XEqY, X, NotY})); } TEST(SolverTest, IffTransitiveConflict) { @@ -278,7 +306,7 @@ TEST(SolverTest, IffTransitiveConflict) { auto NotX = Ctx.neg(X); // (X <=> Y) ^ (Y <=> Z) ^ Z ^ !X - EXPECT_THAT(solve({XEqY, YEqZ, Z, NotX}), unsat()); + expectUnsatisfiable(solve({XEqY, YEqZ, Z, NotX})); } TEST(SolverTest, DeMorgan) { @@ -295,7 +323,7 @@ TEST(SolverTest, DeMorgan) { auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W))); // A ^ B - EXPECT_THAT(solve({A, B}), sat(_)); + expectSatisfiable(solve({A, B}), _); } TEST(SolverTest, RespectsAdditionalConstraints) { @@ -306,7 +334,7 @@ TEST(SolverTest, RespectsAdditionalConstraints) { auto NotY = Ctx.neg(Y); // (X <=> Y) ^ X ^ !Y - EXPECT_THAT(solve({XEqY, X, NotY}), unsat()); + expectUnsatisfiable(solve({XEqY, X, NotY})); } TEST(SolverTest, ImplicationIsEquivalentToDNF) { @@ -318,7 +346,7 @@ TEST(SolverTest, ImplicationIsEquivalentToDNF) { auto NotEquivalent = Ctx.neg(Ctx.iff(XImpliesY, XImpliesYDNF)); // !((X => Y) <=> (!X v Y)) - EXPECT_THAT(solve({NotEquivalent}), unsat()); + expectUnsatisfiable(solve({NotEquivalent})); } TEST(SolverTest, ImplicationConflict) { @@ -329,7 +357,7 @@ TEST(SolverTest, ImplicationConflict) { auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y)); // X => Y ^ X ^ !Y - EXPECT_THAT(solve({XImplY, XAndNotY}), unsat()); + expectUnsatisfiable(solve({XImplY, XAndNotY})); } TEST(SolverTest, LowTimeoutResultsInTimedOut) { diff --git a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h index 2eaa783..e258eb7 100644 --- a/clang/unittests/Analysis/FlowSensitive/TestingSupport.h +++ b/clang/unittests/Analysis/FlowSensitive/TestingSupport.h @@ -43,7 +43,6 @@ #include "llvm/ADT/DenseMap.h" #include "llvm/ADT/StringMap.h" #include "llvm/ADT/StringRef.h" -#include "llvm/Support/Allocator.h" #include "llvm/Support/Errc.h" #include "llvm/Support/Error.h" #include "llvm/Testing/Annotations/Annotations.h" @@ -443,49 +442,55 @@ ValueT &getValueForDecl(ASTContext &ASTCtx, const Environment &Env, /// Creates and owns constraints which are boolean values. class ConstraintContext { - unsigned NextAtom = 0; - llvm::BumpPtrAllocator A; - - const Formula *make(Formula::Kind K, - llvm::ArrayRef<const Formula *> Operands) { - return &Formula::create(A, K, Operands); - } - public: - // Returns a reference to a fresh atomic variable. - const Formula *atom() { - return &Formula::create(A, Formula::AtomRef, {}, NextAtom++); + // Creates an atomic boolean value. + BoolValue *atom() { + Vals.push_back(std::make_unique<AtomicBoolValue>()); + return Vals.back().get(); } - // Returns a reference to a literal boolean value. - const Formula *literal(bool B) { - return &Formula::create(A, Formula::Literal, {}, B); + // Creates an instance of the Top boolean value. + BoolValue *top() { + Vals.push_back(std::make_unique<TopBoolValue>()); + return Vals.back().get(); } - // Creates a boolean conjunction. - const Formula *conj(const Formula *LHS, const Formula *RHS) { - return make(Formula::And, {LHS, RHS}); + // Creates a boolean conjunction value. + BoolValue *conj(BoolValue *LeftSubVal, BoolValue *RightSubVal) { + Vals.push_back( + std::make_unique<ConjunctionValue>(*LeftSubVal, *RightSubVal)); + return Vals.back().get(); } - // Creates a boolean disjunction. - const Formula *disj(const Formula *LHS, const Formula *RHS) { - return make(Formula::Or, {LHS, RHS}); + // Creates a boolean disjunction value. + BoolValue *disj(BoolValue *LeftSubVal, BoolValue *RightSubVal) { + Vals.push_back( + std::make_unique<DisjunctionValue>(*LeftSubVal, *RightSubVal)); + return Vals.back().get(); } - // Creates a boolean negation. - const Formula *neg(const Formula *Operand) { - return make(Formula::Not, {Operand}); + // Creates a boolean negation value. + BoolValue *neg(BoolValue *SubVal) { + Vals.push_back(std::make_unique<NegationValue>(*SubVal)); + return Vals.back().get(); } - // Creates a boolean implication. - const Formula *impl(const Formula *LHS, const Formula *RHS) { - return make(Formula::Implies, {LHS, RHS}); + // Creates a boolean implication value. + BoolValue *impl(BoolValue *LeftSubVal, BoolValue *RightSubVal) { + Vals.push_back( + std::make_unique<ImplicationValue>(*LeftSubVal, *RightSubVal)); + return Vals.back().get(); } - // Creates a boolean biconditional. - const Formula *iff(const Formula *LHS, const Formula *RHS) { - return make(Formula::Equal, {LHS, RHS}); + // Creates a boolean biconditional value. + BoolValue *iff(BoolValue *LeftSubVal, BoolValue *RightSubVal) { + Vals.push_back( + std::make_unique<BiconditionalValue>(*LeftSubVal, *RightSubVal)); + return Vals.back().get(); } + +private: + std::vector<std::unique_ptr<BoolValue>> Vals; }; } // namespace test diff --git a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp index 4da5987..3f99ff5 100644 --- a/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/TransferTest.cpp @@ -2963,14 +2963,14 @@ TEST(TransferTest, AssignFromBoolLiteral) { ASSERT_THAT(FooDecl, NotNull()); const auto *FooVal = - dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl)); + dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*FooDecl)); ASSERT_THAT(FooVal, NotNull()); const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); const auto *BarVal = - dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl)); + dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*BarDecl)); ASSERT_THAT(BarVal, NotNull()); EXPECT_EQ(FooVal, &Env.getBoolLiteralValue(true)); @@ -3018,12 +3018,14 @@ TEST(TransferTest, AssignFromCompositeBoolExpression) { ASSERT_THAT(BazDecl, NotNull()); const auto *BazVal = - dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl)); + dyn_cast_or_null<ConjunctionValue>(Env.getValue(*BazDecl)); ASSERT_THAT(BazVal, NotNull()); - auto &A = Env.arena(); - EXPECT_EQ(&BazVal->formula(), - &A.makeAnd(FooVal->formula(), - A.makeOr(BarVal->formula(), QuxVal->formula()))); + EXPECT_EQ(&BazVal->getLeftSubValue(), FooVal); + + const auto *BazRightSubValVal = + cast<DisjunctionValue>(&BazVal->getRightSubValue()); + EXPECT_EQ(&BazRightSubValVal->getLeftSubValue(), BarVal); + EXPECT_EQ(&BazRightSubValVal->getRightSubValue(), QuxVal); }); } @@ -3066,12 +3068,15 @@ TEST(TransferTest, AssignFromCompositeBoolExpression) { ASSERT_THAT(BazDecl, NotNull()); const auto *BazVal = - dyn_cast_or_null<BoolValue>(Env.getValue(*BazDecl)); + dyn_cast_or_null<DisjunctionValue>(Env.getValue(*BazDecl)); ASSERT_THAT(BazVal, NotNull()); - auto &A = Env.arena(); - EXPECT_EQ(&BazVal->formula(), - &A.makeOr(A.makeAnd(FooVal->formula(), QuxVal->formula()), - BarVal->formula())); + + const auto *BazLeftSubValVal = + cast<ConjunctionValue>(&BazVal->getLeftSubValue()); + EXPECT_EQ(&BazLeftSubValVal->getLeftSubValue(), FooVal); + EXPECT_EQ(&BazLeftSubValVal->getRightSubValue(), QuxVal); + + EXPECT_EQ(&BazVal->getRightSubValue(), BarVal); }); } @@ -3117,14 +3122,17 @@ TEST(TransferTest, AssignFromCompositeBoolExpression) { ASSERT_THAT(FooDecl, NotNull()); const auto *FooVal = - dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl)); + dyn_cast_or_null<ConjunctionValue>(Env.getValue(*FooDecl)); ASSERT_THAT(FooVal, NotNull()); - auto &A = Env.arena(); - EXPECT_EQ( - &FooVal->formula(), - &A.makeAnd(A.makeAnd(A.makeAnd(AVal->formula(), BVal->formula()), - CVal->formula()), - DVal->formula())); + + const auto &FooLeftSubVal = + cast<ConjunctionValue>(FooVal->getLeftSubValue()); + const auto &FooLeftLeftSubVal = + cast<ConjunctionValue>(FooLeftSubVal.getLeftSubValue()); + EXPECT_EQ(&FooLeftLeftSubVal.getLeftSubValue(), AVal); + EXPECT_EQ(&FooLeftLeftSubVal.getRightSubValue(), BVal); + EXPECT_EQ(&FooLeftSubVal.getRightSubValue(), CVal); + EXPECT_EQ(&FooVal->getRightSubValue(), DVal); }); } } @@ -3148,17 +3156,17 @@ TEST(TransferTest, AssignFromBoolNegation) { ASSERT_THAT(FooDecl, NotNull()); const auto *FooVal = - dyn_cast_or_null<BoolValue>(Env.getValue(*FooDecl)); + dyn_cast_or_null<AtomicBoolValue>(Env.getValue(*FooDecl)); ASSERT_THAT(FooVal, NotNull()); const ValueDecl *BarDecl = findValueDecl(ASTCtx, "Bar"); ASSERT_THAT(BarDecl, NotNull()); const auto *BarVal = - dyn_cast_or_null<BoolValue>(Env.getValue(*BarDecl)); + dyn_cast_or_null<NegationValue>(Env.getValue(*BarDecl)); ASSERT_THAT(BarVal, NotNull()); - auto &A = Env.arena(); - EXPECT_EQ(&BarVal->formula(), &A.makeNot(FooVal->formula())); + + EXPECT_EQ(&BarVal->getSubVal(), FooVal); }); } diff --git a/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp b/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp index 02f3ade..2b7341b 100644 --- a/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/ValueTest.cpp @@ -7,7 +7,6 @@ //===----------------------------------------------------------------------===// #include "clang/Analysis/FlowSensitive/Value.h" -#include "clang/Analysis/FlowSensitive/Arena.h" #include "clang/Analysis/FlowSensitive/StorageLocation.h" #include "gmock/gmock.h" #include "gtest/gtest.h" @@ -40,19 +39,17 @@ TEST(ValueTest, AliasedPointersEquivalent) { } TEST(ValueTest, TopsEquivalent) { - Arena A; - TopBoolValue V1(A.makeAtomRef(Atom(0))); - TopBoolValue V2(A.makeAtomRef(Atom(1))); + TopBoolValue V1; + TopBoolValue V2; EXPECT_TRUE(areEquivalentValues(V1, V2)); EXPECT_TRUE(areEquivalentValues(V2, V1)); } TEST(ValueTest, EquivalentValuesWithDifferentPropsEquivalent) { - Arena A; - TopBoolValue Prop1(A.makeAtomRef(Atom(0))); - TopBoolValue Prop2(A.makeAtomRef(Atom(1))); - TopBoolValue V1(A.makeAtomRef(Atom(2))); - TopBoolValue V2(A.makeAtomRef(Atom(3))); + TopBoolValue Prop1; + TopBoolValue Prop2; + TopBoolValue V1; + TopBoolValue V2; V1.setProperty("foo", Prop1); V2.setProperty("bar", Prop2); EXPECT_TRUE(areEquivalentValues(V1, V2)); @@ -60,10 +57,9 @@ TEST(ValueTest, EquivalentValuesWithDifferentPropsEquivalent) { } TEST(ValueTest, DifferentKindsNotEquivalent) { - Arena A; auto L = ScalarStorageLocation(QualType()); ReferenceValue V1(L); - TopBoolValue V2(A.makeAtomRef(Atom(0))); + TopBoolValue V2; EXPECT_FALSE(areEquivalentValues(V1, V2)); EXPECT_FALSE(areEquivalentValues(V2, V1)); } |