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