From: Sam McCall Date: Mon, 17 Apr 2023 18:35:20 +0000 (+0200) Subject: [dataflow] Extract arena for Value/StorageLocation out of DataflowAnalysisContext X-Git-Tag: upstream/17.0.6~11091 X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=bf47c1ed855605324efcca4af92517026c7e53e5;p=platform%2Fupstream%2Fllvm.git [dataflow] Extract arena for Value/StorageLocation out of DataflowAnalysisContext DataflowAnalysisContext has a few too many responsibilities, this narrows them. It also allows the Arena to be shared with analysis steps, which need to create Values, without exposing the whole DACtx API (flow conditions etc). This means Environment no longer needs to proxy all these methods. (For now it still does, because there are many callsites to update, and maybe if we separate bool formulas from values we can avoid churning them twice) In future, if we untangle the concepts of Values from boolean formulas/atoms, Arena would also be responsible for creating formulas and managing atom IDs. Differential Revision: https://reviews.llvm.org/D148554 --- diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h new file mode 100644 index 000000000000..8dc51e044b14 --- /dev/null +++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h @@ -0,0 +1,120 @@ +//===-- Arena.h -------------------------------*- 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/StorageLocation.h" +#include "clang/Analysis/FlowSensitive/Value.h" +#include + +namespace clang::dataflow { + +/// The Arena owns the objects that model data within an analysis. +/// For example, `Value` and `StorageLocation`. +class Arena { +public: + Arena() + : TrueVal(create()), + FalseVal(create()) {} + Arena(const Arena &) = delete; + Arena &operator=(const Arena &) = delete; + + /// Creates a `T` (some subclass of `StorageLocation`), forwarding `args` to + /// the constructor, and returns a reference to it. + /// + /// The `DataflowAnalysisContext` takes ownership of the created object. The + /// object will be destroyed when the `DataflowAnalysisContext` is destroyed. + template + std::enable_if_t::value, T &> + create(Args &&...args) { + // Note: If allocation of individual `StorageLocation`s turns out to be + // costly, consider creating specializations of `create` for commonly + // used `StorageLocation` subclasses and make them use a `BumpPtrAllocator`. + return *cast( + Locs.emplace_back(std::make_unique(std::forward(args)...)) + .get()); + } + + /// Creates a `T` (some subclass of `Value`), forwarding `args` to the + /// constructor, and returns a reference to it. + /// + /// The `DataflowAnalysisContext` takes ownership of the created object. The + /// object will be destroyed when the `DataflowAnalysisContext` is destroyed. + template + std::enable_if_t::value, T &> + create(Args &&...args) { + // Note: If allocation of individual `Value`s turns out to be costly, + // consider creating specializations of `create` for commonly used + // `Value` subclasses and make them use a `BumpPtrAllocator`. + return *cast( + Vals.emplace_back(std::make_unique(std::forward(args)...)) + .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); + + /// Returns a symbolic boolean value that models a boolean literal equal to + /// `Value`. These literals are the same every time. + AtomicBoolValue &makeLiteral(bool Value) const { + return Value ? TrueVal : FalseVal; + } + + /// Creates a fresh flow condition and returns a token that identifies it. The + /// token can be used to perform various operations on the flow condition such + /// as adding constraints to it, forking it, joining it with another flow + /// condition, or checking implications. + AtomicBoolValue &makeFlowConditionToken() { + return create(); + } + +private: + // Storage for the state of a program. + std::vector> Locs; + std::vector> Vals; + + // Indices that are used to avoid recreating the same composite boolean + // values. + llvm::DenseMap, ConjunctionValue *> + ConjunctionVals; + llvm::DenseMap, DisjunctionValue *> + DisjunctionVals; + llvm::DenseMap NegationVals; + llvm::DenseMap, ImplicationValue *> + ImplicationVals; + llvm::DenseMap, BiconditionalValue *> + BiconditionalVals; + + AtomicBoolValue &TrueVal; + AtomicBoolValue &FalseVal; +}; + +} // namespace clang::dataflow diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h index 31bd9809a72a..9695884c00c9 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -18,6 +18,7 @@ #include "clang/AST/Decl.h" #include "clang/AST/Expr.h" #include "clang/AST/TypeOrdering.h" +#include "clang/Analysis/FlowSensitive/Arena.h" #include "clang/Analysis/FlowSensitive/ControlFlowContext.h" #include "clang/Analysis/FlowSensitive/Solver.h" #include "clang/Analysis/FlowSensitive/StorageLocation.h" @@ -86,74 +87,6 @@ public: /*Logger=*/nullptr}); ~DataflowAnalysisContext(); - /// Creates a `T` (some subclass of `StorageLocation`), forwarding `args` to - /// the constructor, and returns a reference to it. - /// - /// The `DataflowAnalysisContext` takes ownership of the created object. The - /// object will be destroyed when the `DataflowAnalysisContext` is destroyed. - template - std::enable_if_t::value, T &> - create(Args &&...args) { - // Note: If allocation of individual `StorageLocation`s turns out to be - // costly, consider creating specializations of `create` for commonly - // used `StorageLocation` subclasses and make them use a `BumpPtrAllocator`. - return *cast( - Locs.emplace_back(std::make_unique(std::forward(args)...)) - .get()); - } - - /// Creates a `T` (some subclass of `Value`), forwarding `args` to the - /// constructor, and returns a reference to it. - /// - /// The `DataflowAnalysisContext` takes ownership of the created object. The - /// object will be destroyed when the `DataflowAnalysisContext` is destroyed. - template - std::enable_if_t::value, T &> - create(Args &&...args) { - // Note: If allocation of individual `Value`s turns out to be costly, - // consider creating specializations of `create` for commonly used - // `Value` subclasses and make them use a `BumpPtrAllocator`. - return *cast( - Vals.emplace_back(std::make_unique(std::forward(args)...)) - .get()); - } - - /// Takes ownership of `Loc` and returns a reference to it. - /// - /// This function is deprecated. Instead of - /// `takeOwnership(std::make_unique(args))`, prefer - /// `create(args)`. - /// - /// Requirements: - /// - /// `Loc` must not be null. - template - LLVM_DEPRECATED("use create instead", "") - std::enable_if_t::value, - T &> takeOwnership(std::unique_ptr Loc) { - assert(Loc != nullptr); - Locs.push_back(std::move(Loc)); - return *cast(Locs.back().get()); - } - - /// Takes ownership of `Val` and returns a reference to it. - /// - /// This function is deprecated. Instead of - /// `takeOwnership(std::make_unique(args))`, prefer - /// `create(args)`. - /// - /// Requirements: - /// - /// `Val` must not be null. - template - LLVM_DEPRECATED("use create instead", "") - std::enable_if_t::value, T &> takeOwnership( - std::unique_ptr Val) { - assert(Val != nullptr); - Vals.push_back(std::move(Val)); - return *cast(Vals.back().get()); - } - /// Returns a new storage location appropriate for `Type`. /// /// A null `Type` is interpreted as the pointee type of `std::nullptr_t`. @@ -205,62 +138,6 @@ public: /// A null `PointeeType` can be used for the pointee of `std::nullptr_t`. PointerValue &getOrCreateNullPointerValue(QualType PointeeType); - /// Returns a symbolic boolean value that models a boolean literal equal to - /// `Value`. - AtomicBoolValue &getBoolLiteralValue(bool Value) const { - return Value ? TrueVal : FalseVal; - } - - /// Creates an atomic boolean value. - LLVM_DEPRECATED("use create instead", - "create") - AtomicBoolValue &createAtomicBoolValue() { return create(); } - - /// Creates a Top value for booleans. Each instance is unique and can be - /// assigned a distinct truth value during solving. - /// - /// FIXME: `Top iff Top` is true when both Tops are identical (by pointer - /// equality), but not when they are distinct values. We should improve the - /// implementation so that `Top iff Top` has a consistent meaning, regardless - /// of the identity of `Top`. Moreover, I think the meaning should be - /// `false`. - LLVM_DEPRECATED("use create instead", "create") - TopBoolValue &createTopBoolValue() { return create(); } - - /// 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 &getOrCreateConjunction(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 &getOrCreateDisjunction(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 &getOrCreateNegation(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 &getOrCreateImplication(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 &getOrCreateIff(BoolValue &LHS, BoolValue &RHS); - - /// 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(); - /// Adds `Constraint` to the flow condition identified by `Token`. void addFlowConditionConstraint(AtomicBoolValue &Token, BoolValue &Constraint); @@ -275,27 +152,6 @@ public: AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken, AtomicBoolValue &SecondToken); - // FIXME: This function returns the flow condition expressed directly as its - // constraints: (C1 AND C2 AND ...). This differs from the general approach in - // the framework where a flow condition is represented as a token (an atomic - // boolean) with dependencies and constraints tracked in `FlowConditionDeps` - // and `FlowConditionConstraints`: (FC <=> C1 AND C2 AND ...). - // Consider if we should make the representation of flow condition consistent, - // returning an atomic boolean token with separate constraints instead. - // - /// Builds and returns the logical formula defining the flow condition - /// identified by `Token`. If a value in the formula is present as a key in - /// `Substitutions`, it will be substituted with the value it maps to. - /// As an example, say we have flow condition tokens FC1, FC2, FC3 and - /// FlowConditionConstraints: { FC1: C1, - /// FC2: C2, - /// FC3: (FC1 v FC2) ^ C3 } - /// buildAndSubstituteFlowCondition(FC3, {{C1 -> C1'}}) will return a value - /// corresponding to (C1' v C2) ^ C3. - BoolValue &buildAndSubstituteFlowCondition( - AtomicBoolValue &Token, - llvm::DenseMap Substitutions); - /// 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); @@ -318,6 +174,8 @@ public: const Options &getOptions() { return Opts; } + Arena &arena() { return *A; } + private: friend class Environment; @@ -361,28 +219,8 @@ private: Solver::Result::Status::Unsatisfiable; } - /// Returns a boolean value as a result of substituting `Val` and its sub - /// values based on entries in `SubstitutionsCache`. Intermediate results are - /// stored in `SubstitutionsCache` to avoid reprocessing values that have - /// already been visited. - BoolValue &substituteBoolValue( - BoolValue &Val, - llvm::DenseMap &SubstitutionsCache); - - /// Builds and returns the logical formula defining the flow condition - /// identified by `Token`, sub values may be substituted based on entries in - /// `SubstitutionsCache`. Intermediate results are stored in - /// `SubstitutionsCache` to avoid reprocessing values that have already been - /// visited. - BoolValue &buildAndSubstituteFlowConditionWithCache( - AtomicBoolValue &Token, - llvm::DenseMap &SubstitutionsCache); - std::unique_ptr S; - - // Storage for the state of a program. - std::vector> Locs; - std::vector> Vals; + std::unique_ptr A; // Maps from program declarations and statements to storage locations that are // assigned to them. These assignments are global (aggregated across all basic @@ -401,23 +239,8 @@ private: llvm::DenseMap NullPointerVals; - AtomicBoolValue &TrueVal; - AtomicBoolValue &FalseVal; - Options Opts; - // Indices that are used to avoid recreating the same composite boolean - // values. - llvm::DenseMap, ConjunctionValue *> - ConjunctionVals; - llvm::DenseMap, DisjunctionValue *> - DisjunctionVals; - llvm::DenseMap NegationVals; - llvm::DenseMap, ImplicationValue *> - ImplicationVals; - llvm::DenseMap, BiconditionalValue *> - BiconditionalVals; - // Flow conditions are tracked symbolically: each unique flow condition is // associated with a fresh symbolic variable (token), bound to the clause that // defines the flow condition. Conceptually, each binding corresponds to an diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h index 4e65d974133a..8690616411db 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h @@ -182,6 +182,8 @@ public: return DACtx->getOptions(); } + Arena &arena() const { return DACtx->arena(); } + Logger &logger() const { return *DACtx->getOptions().Log; } /// Creates and returns an environment to use for an inline analysis of the @@ -319,16 +321,7 @@ public: /// is assigned a storage location in the environment, otherwise returns null. Value *getValue(const Expr &E, SkipPast SP) const; - /// Creates a `T` (some subclass of `StorageLocation`), forwarding `args` to - /// the constructor, and returns a reference to it. - /// - /// The analysis context takes ownership of the created object. The object - /// will be destroyed when the analysis context is destroyed. - template - std::enable_if_t::value, T &> - create(Args &&...args) { - return DACtx->create(std::forward(args)...); - } + // FIXME: should we deprecate the following & call arena().create() directly? /// Creates a `T` (some subclass of `Value`), forwarding `args` to the /// constructor, and returns a reference to it. @@ -338,57 +331,23 @@ public: template std::enable_if_t::value, T &> create(Args &&...args) { - return DACtx->create(std::forward(args)...); - } - - /// Transfers ownership of `Loc` to the analysis context and returns a - /// reference to it. - /// - /// This function is deprecated. Instead of - /// `takeOwnership(std::make_unique(args))`, prefer - /// `create(args)`. - /// - /// Requirements: - /// - /// `Loc` must not be null. - template - LLVM_DEPRECATED("use create instead", "") - std::enable_if_t::value, - T &> takeOwnership(std::unique_ptr Loc) { - return DACtx->takeOwnership(std::move(Loc)); - } - - /// Transfers ownership of `Val` to the analysis context and returns a - /// reference to it. - /// - /// This function is deprecated. Instead of - /// `takeOwnership(std::make_unique(args))`, prefer - /// `create(args)`. - /// - /// Requirements: - /// - /// `Val` must not be null. - template - LLVM_DEPRECATED("use create instead", "") - std::enable_if_t::value, T &> takeOwnership( - std::unique_ptr Val) { - return DACtx->takeOwnership(std::move(Val)); + return arena().create(std::forward(args)...); } /// Returns a symbolic boolean value that models a boolean literal equal to /// `Value` AtomicBoolValue &getBoolLiteralValue(bool Value) const { - return DACtx->getBoolLiteralValue(Value); + return arena().makeLiteral(Value); } /// Returns an atomic boolean value. BoolValue &makeAtomicBoolValue() const { - return DACtx->create(); + return arena().create(); } /// Returns a unique instance of boolean Top. BoolValue &makeTopBoolValue() const { - return DACtx->create(); + return arena().create(); } /// Returns a boolean value that represents the conjunction of `LHS` and @@ -396,7 +355,7 @@ public: /// order, will return the same result. If the given boolean values represent /// the same value, the result will be the value itself. BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS) const { - return DACtx->getOrCreateConjunction(LHS, RHS); + return arena().makeAnd(LHS, RHS); } /// Returns a boolean value that represents the disjunction of `LHS` and @@ -404,13 +363,13 @@ public: /// order, will return the same result. If the given boolean values represent /// the same value, the result will be the value itself. BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS) const { - return DACtx->getOrCreateDisjunction(LHS, RHS); + return arena().makeOr(LHS, RHS); } /// Returns a boolean value that represents the negation of `Val`. Subsequent /// calls with the same argument will return the same result. BoolValue &makeNot(BoolValue &Val) const { - return DACtx->getOrCreateNegation(Val); + return arena().makeNot(Val); } /// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with @@ -418,7 +377,7 @@ public: /// values represent the same value, the result will be a value that /// represents the true boolean literal. BoolValue &makeImplication(BoolValue &LHS, BoolValue &RHS) const { - return DACtx->getOrCreateImplication(LHS, RHS); + return arena().makeImplies(LHS, RHS); } /// Returns a boolean value represents `LHS` <=> `RHS`. Subsequent calls with @@ -426,22 +385,12 @@ public: /// result. If the given boolean values represent the same value, the result /// will be a value that represents the true boolean literal. BoolValue &makeIff(BoolValue &LHS, BoolValue &RHS) const { - return DACtx->getOrCreateIff(LHS, RHS); + return arena().makeEquals(LHS, RHS); } /// Returns the token that identifies the flow condition of the environment. AtomicBoolValue &getFlowConditionToken() const { return *FlowConditionToken; } - /// Builds and returns the logical formula defining the flow condition - /// identified by `Token`. If a value in the formula is present as a key in - /// `Substitutions`, it will be substituted with the value it maps to. - BoolValue &buildAndSubstituteFlowCondition( - AtomicBoolValue &Token, - llvm::DenseMap Substitutions) { - return DACtx->buildAndSubstituteFlowCondition(Token, - std::move(Substitutions)); - } - /// Adds `Val` to the set of clauses that constitute the flow condition. void addToFlowCondition(BoolValue &Val); diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp new file mode 100644 index 000000000000..a0182af85a22 --- /dev/null +++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp @@ -0,0 +1,71 @@ +//===-- Arena.cpp ---------------------------------------------------------===// +// +// 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/Arena.h" + +namespace clang::dataflow { + +static std::pair +makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) { + auto Res = std::make_pair(&LHS, &RHS); + if (&RHS < &LHS) + std::swap(Res.first, Res.second); + return Res; +} + +BoolValue &Arena::makeAnd(BoolValue &LHS, BoolValue &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; +} + +BoolValue &Arena::makeOr(BoolValue &LHS, BoolValue &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; +} + +BoolValue &Arena::makeNot(BoolValue &Val) { + auto Res = NegationVals.try_emplace(&Val, nullptr); + if (Res.second) + Res.first->second = &create(Val); + return *Res.first->second; +} + +BoolValue &Arena::makeImplies(BoolValue &LHS, BoolValue &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; +} + +BoolValue &Arena::makeEquals(BoolValue &LHS, BoolValue &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; +} + +} // namespace clang::dataflow diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt index a3216518f4db..86646662c4da 100644 --- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt +++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt @@ -1,4 +1,5 @@ add_clang_library(clangAnalysisFlowSensitive + Arena.cpp ControlFlowContext.cpp DataflowAnalysisContext.cpp DataflowEnvironment.cpp diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp index 1fbc3759747e..ad57fd156f44 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -58,9 +58,9 @@ StorageLocation &DataflowAnalysisContext::createStorageLocation(QualType Type) { : getReferencedFields(Type); for (const FieldDecl *Field : Fields) FieldLocs.insert({Field, &createStorageLocation(Field->getType())}); - return create(Type, std::move(FieldLocs)); + return arena().create(Type, std::move(FieldLocs)); } - return create(Type); + return arena().create(Type); } StorageLocation & @@ -88,88 +88,23 @@ DataflowAnalysisContext::getOrCreateNullPointerValue(QualType PointeeType) { auto Res = NullPointerVals.try_emplace(CanonicalPointeeType, nullptr); if (Res.second) { auto &PointeeLoc = createStorageLocation(CanonicalPointeeType); - Res.first->second = &create(PointeeLoc); + Res.first->second = &arena().create(PointeeLoc); } return *Res.first->second; } -static std::pair -makeCanonicalBoolValuePair(BoolValue &LHS, BoolValue &RHS) { - auto Res = std::make_pair(&LHS, &RHS); - if (&RHS < &LHS) - std::swap(Res.first, Res.second); - return Res; -} - -BoolValue &DataflowAnalysisContext::getOrCreateConjunction(BoolValue &LHS, - BoolValue &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; -} - -BoolValue &DataflowAnalysisContext::getOrCreateDisjunction(BoolValue &LHS, - BoolValue &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; -} - -BoolValue &DataflowAnalysisContext::getOrCreateNegation(BoolValue &Val) { - auto Res = NegationVals.try_emplace(&Val, nullptr); - if (Res.second) - Res.first->second = &create(Val); - return *Res.first->second; -} - -BoolValue &DataflowAnalysisContext::getOrCreateImplication(BoolValue &LHS, - BoolValue &RHS) { - if (&LHS == &RHS) - return getBoolLiteralValue(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; -} - -BoolValue &DataflowAnalysisContext::getOrCreateIff(BoolValue &LHS, - BoolValue &RHS) { - if (&LHS == &RHS) - return getBoolLiteralValue(true); - - auto Res = BiconditionalVals.try_emplace(makeCanonicalBoolValuePair(LHS, RHS), - nullptr); - if (Res.second) - Res.first->second = &create(LHS, RHS); - return *Res.first->second; -} - -AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() { - return create(); -} - void DataflowAnalysisContext::addFlowConditionConstraint( AtomicBoolValue &Token, BoolValue &Constraint) { auto Res = FlowConditionConstraints.try_emplace(&Token, &Constraint); if (!Res.second) { - Res.first->second = &getOrCreateConjunction(*Res.first->second, Constraint); + Res.first->second = + &arena().makeAnd(*Res.first->second, Constraint); } } AtomicBoolValue & DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) { - auto &ForkToken = makeFlowConditionToken(); + auto &ForkToken = arena().makeFlowConditionToken(); FlowConditionDeps[&ForkToken].insert(&Token); addFlowConditionConstraint(ForkToken, Token); return ForkToken; @@ -178,18 +113,19 @@ DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) { AtomicBoolValue & DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken, AtomicBoolValue &SecondToken) { - auto &Token = makeFlowConditionToken(); + auto &Token = arena().makeFlowConditionToken(); FlowConditionDeps[&Token].insert(&FirstToken); FlowConditionDeps[&Token].insert(&SecondToken); - addFlowConditionConstraint(Token, - getOrCreateDisjunction(FirstToken, SecondToken)); + addFlowConditionConstraint( + Token, arena().makeOr(FirstToken, SecondToken)); return Token; } Solver::Result DataflowAnalysisContext::querySolver(llvm::DenseSet Constraints) { - Constraints.insert(&getBoolLiteralValue(true)); - Constraints.insert(&getOrCreateNegation(getBoolLiteralValue(false))); + Constraints.insert(&arena().makeLiteral(true)); + Constraints.insert( + &arena().makeNot(arena().makeLiteral(false))); return S->solve(std::move(Constraints)); } @@ -200,7 +136,8 @@ bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token, // 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::DenseSet Constraints = {&Token, &getOrCreateNegation(Val)}; + llvm::DenseSet Constraints = {&Token, + &arena().makeNot(Val)}; llvm::DenseSet VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); return isUnsatisfiable(std::move(Constraints)); @@ -209,7 +146,8 @@ bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token, bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) { // Returns true if and only if we cannot prove that the flow condition can // ever be false. - llvm::DenseSet Constraints = {&getOrCreateNegation(Token)}; + llvm::DenseSet Constraints = { + &arena().makeNot(Token)}; llvm::DenseSet VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); return isUnsatisfiable(std::move(Constraints)); @@ -218,7 +156,7 @@ bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) { bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1, BoolValue &Val2) { llvm::DenseSet Constraints = { - &getOrCreateNegation(getOrCreateIff(Val1, Val2))}; + &arena().makeNot(arena().makeEquals(Val1, Val2))}; return isUnsatisfiable(Constraints); } @@ -235,7 +173,7 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( } else { // Bind flow condition token via `iff` to its set of constraints: // FC <=> (C1 ^ C2 ^ ...), where Ci are constraints - Constraints.insert(&getOrCreateIff(Token, *ConstraintsIt->second)); + Constraints.insert(&arena().makeEquals(Token, *ConstraintsIt->second)); } auto DepsIt = FlowConditionDeps.find(&Token); @@ -247,101 +185,6 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( } } -BoolValue &DataflowAnalysisContext::substituteBoolValue( - BoolValue &Val, - llvm::DenseMap &SubstitutionsCache) { - auto It = SubstitutionsCache.find(&Val); - if (It != SubstitutionsCache.end()) { - // Return memoized result of substituting this boolean value. - return *It->second; - } - - // Handle substitution on the boolean value (and its subvalues), saving the - // result into `SubstitutionsCache`. - BoolValue *Result; - switch (Val.getKind()) { - case Value::Kind::AtomicBool: { - Result = &Val; - break; - } - case Value::Kind::Negation: { - auto &Negation = *cast(&Val); - auto &Sub = substituteBoolValue(Negation.getSubVal(), SubstitutionsCache); - Result = &getOrCreateNegation(Sub); - break; - } - case Value::Kind::Disjunction: { - auto &Disjunct = *cast(&Val); - auto &LeftSub = - substituteBoolValue(Disjunct.getLeftSubValue(), SubstitutionsCache); - auto &RightSub = - substituteBoolValue(Disjunct.getRightSubValue(), SubstitutionsCache); - Result = &getOrCreateDisjunction(LeftSub, RightSub); - break; - } - case Value::Kind::Conjunction: { - auto &Conjunct = *cast(&Val); - auto &LeftSub = - substituteBoolValue(Conjunct.getLeftSubValue(), SubstitutionsCache); - auto &RightSub = - substituteBoolValue(Conjunct.getRightSubValue(), SubstitutionsCache); - Result = &getOrCreateConjunction(LeftSub, RightSub); - break; - } - case Value::Kind::Implication: { - auto &IV = *cast(&Val); - auto &LeftSub = - substituteBoolValue(IV.getLeftSubValue(), SubstitutionsCache); - auto &RightSub = - substituteBoolValue(IV.getRightSubValue(), SubstitutionsCache); - Result = &getOrCreateImplication(LeftSub, RightSub); - break; - } - case Value::Kind::Biconditional: { - auto &BV = *cast(&Val); - auto &LeftSub = - substituteBoolValue(BV.getLeftSubValue(), SubstitutionsCache); - auto &RightSub = - substituteBoolValue(BV.getRightSubValue(), SubstitutionsCache); - Result = &getOrCreateIff(LeftSub, RightSub); - break; - } - default: - llvm_unreachable("Unhandled Value Kind"); - } - SubstitutionsCache[&Val] = Result; - return *Result; -} - -BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowCondition( - AtomicBoolValue &Token, - llvm::DenseMap Substitutions) { - assert(!Substitutions.contains(&getBoolLiteralValue(true)) && - !Substitutions.contains(&getBoolLiteralValue(false)) && - "Do not substitute true/false boolean literals"); - llvm::DenseMap SubstitutionsCache( - Substitutions.begin(), Substitutions.end()); - return buildAndSubstituteFlowConditionWithCache(Token, SubstitutionsCache); -} - -BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowConditionWithCache( - AtomicBoolValue &Token, - llvm::DenseMap &SubstitutionsCache) { - auto ConstraintsIt = FlowConditionConstraints.find(&Token); - if (ConstraintsIt == FlowConditionConstraints.end()) { - return getBoolLiteralValue(true); - } - auto DepsIt = FlowConditionDeps.find(&Token); - if (DepsIt != FlowConditionDeps.end()) { - for (AtomicBoolValue *DepToken : DepsIt->second) { - auto &NewDep = buildAndSubstituteFlowConditionWithCache( - *DepToken, SubstitutionsCache); - SubstitutionsCache[DepToken] = &NewDep; - } - } - return substituteBoolValue(*ConstraintsIt->second, SubstitutionsCache); -} - void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token, llvm::raw_ostream &OS) { llvm::DenseSet Constraints = {&Token}; @@ -349,8 +192,8 @@ void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token, addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); llvm::DenseMap AtomNames = { - {&getBoolLiteralValue(false), "False"}, - {&getBoolLiteralValue(true), "True"}}; + {&arena().makeLiteral(false), "False"}, + {&arena().makeLiteral(true), "True"}}; OS << debugString(Constraints, AtomNames); } @@ -377,8 +220,7 @@ DataflowAnalysisContext::getControlFlowContext(const FunctionDecl *F) { DataflowAnalysisContext::DataflowAnalysisContext(std::unique_ptr S, Options Opts) - : S(std::move(S)), TrueVal(create()), - FalseVal(create()), Opts(Opts) { + : S(std::move(S)), A(std::make_unique()), Opts(Opts) { assert(this->S != nullptr); // If the -dataflow-log command-line flag was set, synthesize a logger. // This is ugly but provides a uniform method for ad-hoc debugging dataflow- diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp index 9f5b3adc8b1b..446178a2a5ea 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp @@ -262,7 +262,8 @@ void Environment::initFieldsGlobalsAndFuncs(const FunctionDecl *FuncDecl) { } Environment::Environment(DataflowAnalysisContext &DACtx) - : DACtx(&DACtx), FlowConditionToken(&DACtx.makeFlowConditionToken()) {} + : DACtx(&DACtx), + FlowConditionToken(&DACtx.arena().makeFlowConditionToken()) {} Environment::Environment(const Environment &Other) : DACtx(Other.DACtx), CallStack(Other.CallStack), @@ -380,7 +381,7 @@ void Environment::pushCallInternal(const FunctionDecl *FuncDecl, QualType ParamType = Param->getType(); if (ParamType->isReferenceType()) { - auto &Val = create(*ArgLoc); + auto &Val = arena().create(*ArgLoc); setValue(Loc, Val); } else if (auto *ArgVal = getValue(*ArgLoc)) { setValue(Loc, *ArgVal); @@ -706,7 +707,7 @@ Value *Environment::createValueUnlessSelfReferential( // with integers, and so distinguishing them serves no purpose, but could // prevent convergence. CreatedValuesCount++; - return &create(); + return &arena().create(); } if (Type->isReferenceType() || Type->isPointerType()) { @@ -724,9 +725,9 @@ Value *Environment::createValueUnlessSelfReferential( } if (Type->isReferenceType()) - return &create(PointeeLoc); + return &arena().create(PointeeLoc); else - return &create(PointeeLoc); + return &arena().create(PointeeLoc); } if (Type->isRecordType()) { @@ -746,7 +747,7 @@ Value *Environment::createValueUnlessSelfReferential( Visited.erase(FieldType.getCanonicalType()); } - return &create(std::move(FieldValues)); + return &arena().create(std::move(FieldValues)); } return nullptr; diff --git a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp new file mode 100644 index 000000000000..407abf58529a --- /dev/null +++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp @@ -0,0 +1,129 @@ +//===- ArenaTest.cpp ------------------------------------------------------===// +// +// 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/Arena.h" +#include "gmock/gmock.h" +#include "gtest/gtest.h" + +namespace clang::dataflow { +namespace { + +class ArenaTest : public ::testing::Test { +protected: + Arena A; +}; + +TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) { + auto &X = A.create(); + auto &Y = A.create(); + EXPECT_NE(&X, &Y); +} + +TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) { + auto &X = A.create(); + auto &Y = A.create(); + EXPECT_NE(&X, &Y); +} + +TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) { + auto &X = A.create(); + auto &XAndX = A.makeAnd(X, X); + EXPECT_EQ(&XAndX, &X); +} + +TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) { + auto &X = A.create(); + auto &Y = A.create(); + auto &XAndY1 = A.makeAnd(X, Y); + auto &XAndY2 = A.makeAnd(X, Y); + EXPECT_EQ(&XAndY1, &XAndY2); + + auto &YAndX = A.makeAnd(Y, X); + EXPECT_EQ(&XAndY1, &YAndX); + + auto &Z = A.create(); + auto &XAndZ = A.makeAnd(X, Z); + EXPECT_NE(&XAndY1, &XAndZ); +} + +TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) { + auto &X = A.create(); + auto &XOrX = A.makeOr(X, X); + EXPECT_EQ(&XOrX, &X); +} + +TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) { + auto &X = A.create(); + auto &Y = A.create(); + auto &XOrY1 = A.makeOr(X, Y); + auto &XOrY2 = A.makeOr(X, Y); + EXPECT_EQ(&XOrY1, &XOrY2); + + auto &YOrX = A.makeOr(Y, X); + EXPECT_EQ(&XOrY1, &YOrX); + + auto &Z = A.create(); + auto &XOrZ = A.makeOr(X, Z); + EXPECT_NE(&XOrY1, &XOrZ); +} + +TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) { + auto &X = A.create(); + auto &NotX1 = A.makeNot(X); + auto &NotX2 = A.makeNot(X); + EXPECT_EQ(&NotX1, &NotX2); + + auto &Y = A.create(); + auto &NotY = A.makeNot(Y); + EXPECT_NE(&NotX1, &NotY); +} + +TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) { + auto &X = A.create(); + 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 &XImpliesY1 = A.makeImplies(X, Y); + auto &XImpliesY2 = A.makeImplies(X, Y); + EXPECT_EQ(&XImpliesY1, &XImpliesY2); + + auto &YImpliesX = A.makeImplies(Y, X); + EXPECT_NE(&XImpliesY1, &YImpliesX); + + auto &Z = A.create(); + auto &XImpliesZ = A.makeImplies(X, Z); + EXPECT_NE(&XImpliesY1, &XImpliesZ); +} + +TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) { + auto &X = A.create(); + 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 &XIffY1 = A.makeEquals(X, Y); + auto &XIffY2 = A.makeEquals(X, Y); + EXPECT_EQ(&XIffY1, &XIffY2); + + auto &YIffX = A.makeEquals(Y, X); + EXPECT_EQ(&XIffY1, &YIffX); + + auto &Z = A.create(); + auto &XIffZ = A.makeEquals(X, Z); + EXPECT_NE(&XIffY1, &XIffZ); +} + +} // namespace +} // namespace clang::dataflow diff --git a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt index 0895cdeaabb3..e1e9581bd25b 100644 --- a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt +++ b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt @@ -4,6 +4,7 @@ set(LLVM_LINK_COMPONENTS ) add_clang_unittest(ClangAnalysisFlowSensitiveTests + ArenaTest.cpp CFGMatchSwitchTest.cpp ChromiumCheckModelTest.cpp DataflowAnalysisContextTest.cpp diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp index 52b2d5c7a33a..bb76648abdc0 100644 --- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp @@ -20,150 +20,35 @@ using namespace dataflow; class DataflowAnalysisContextTest : public ::testing::Test { protected: DataflowAnalysisContextTest() - : Context(std::make_unique()) {} + : Context(std::make_unique()), A(Context.arena()) { + } DataflowAnalysisContext Context; + Arena &A; }; -TEST_F(DataflowAnalysisContextTest, - CreateAtomicBoolValueReturnsDistinctValues) { - auto &X = Context.create(); - auto &Y = Context.create(); - EXPECT_NE(&X, &Y); -} - -TEST_F(DataflowAnalysisContextTest, - CreateTopBoolValueReturnsDistinctValues) { - auto &X = Context.create(); - auto &Y = Context.create(); - EXPECT_NE(&X, &Y); -} - TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) { - auto &X = Context.create(); - auto &Y = Context.create(); + auto &X = A.create(); + auto &Y = A.create(); EXPECT_FALSE(Context.equivalentBoolValues(X, Y)); } -TEST_F(DataflowAnalysisContextTest, - GetOrCreateConjunctionReturnsSameExprGivenSameArgs) { - auto &X = Context.create(); - auto &XAndX = Context.getOrCreateConjunction(X, X); - EXPECT_EQ(&XAndX, &X); -} - -TEST_F(DataflowAnalysisContextTest, - GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) { - auto &X = Context.create(); - auto &Y = Context.create(); - auto &XAndY1 = Context.getOrCreateConjunction(X, Y); - auto &XAndY2 = Context.getOrCreateConjunction(X, Y); - EXPECT_EQ(&XAndY1, &XAndY2); - - auto &YAndX = Context.getOrCreateConjunction(Y, X); - EXPECT_EQ(&XAndY1, &YAndX); - - auto &Z = Context.create(); - auto &XAndZ = Context.getOrCreateConjunction(X, Z); - EXPECT_NE(&XAndY1, &XAndZ); -} - -TEST_F(DataflowAnalysisContextTest, - GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) { - auto &X = Context.create(); - auto &XOrX = Context.getOrCreateDisjunction(X, X); - EXPECT_EQ(&XOrX, &X); -} - -TEST_F(DataflowAnalysisContextTest, - GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) { - auto &X = Context.create(); - auto &Y = Context.create(); - auto &XOrY1 = Context.getOrCreateDisjunction(X, Y); - auto &XOrY2 = Context.getOrCreateDisjunction(X, Y); - EXPECT_EQ(&XOrY1, &XOrY2); - - auto &YOrX = Context.getOrCreateDisjunction(Y, X); - EXPECT_EQ(&XOrY1, &YOrX); - - auto &Z = Context.create(); - auto &XOrZ = Context.getOrCreateDisjunction(X, Z); - EXPECT_NE(&XOrY1, &XOrZ); -} - -TEST_F(DataflowAnalysisContextTest, - GetOrCreateNegationReturnsSameExprOnSubsequentCalls) { - auto &X = Context.create(); - auto &NotX1 = Context.getOrCreateNegation(X); - auto &NotX2 = Context.getOrCreateNegation(X); - EXPECT_EQ(&NotX1, &NotX2); - - auto &Y = Context.create(); - auto &NotY = Context.getOrCreateNegation(Y); - EXPECT_NE(&NotX1, &NotY); -} - -TEST_F(DataflowAnalysisContextTest, - GetOrCreateImplicationReturnsTrueGivenSameArgs) { - auto &X = Context.create(); - auto &XImpliesX = Context.getOrCreateImplication(X, X); - EXPECT_EQ(&XImpliesX, &Context.getBoolLiteralValue(true)); -} - -TEST_F(DataflowAnalysisContextTest, - GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) { - auto &X = Context.create(); - auto &Y = Context.create(); - auto &XImpliesY1 = Context.getOrCreateImplication(X, Y); - auto &XImpliesY2 = Context.getOrCreateImplication(X, Y); - EXPECT_EQ(&XImpliesY1, &XImpliesY2); - - auto &YImpliesX = Context.getOrCreateImplication(Y, X); - EXPECT_NE(&XImpliesY1, &YImpliesX); - - auto &Z = Context.create(); - auto &XImpliesZ = Context.getOrCreateImplication(X, Z); - EXPECT_NE(&XImpliesY1, &XImpliesZ); -} - -TEST_F(DataflowAnalysisContextTest, GetOrCreateIffReturnsTrueGivenSameArgs) { - auto &X = Context.create(); - auto &XIffX = Context.getOrCreateIff(X, X); - EXPECT_EQ(&XIffX, &Context.getBoolLiteralValue(true)); -} - -TEST_F(DataflowAnalysisContextTest, - GetOrCreateIffReturnsSameExprOnSubsequentCalls) { - auto &X = Context.create(); - auto &Y = Context.create(); - auto &XIffY1 = Context.getOrCreateIff(X, Y); - auto &XIffY2 = Context.getOrCreateIff(X, Y); - EXPECT_EQ(&XIffY1, &XIffY2); - - auto &YIffX = Context.getOrCreateIff(Y, X); - EXPECT_EQ(&XIffY1, &YIffX); - - auto &Z = Context.create(); - auto &XIffZ = Context.getOrCreateIff(X, Z); - EXPECT_NE(&XIffY1, &XIffZ); -} - TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) { - auto &FC = Context.makeFlowConditionToken(); - auto &C = Context.create(); + auto &FC = A.makeFlowConditionToken(); + auto &C = A.create(); EXPECT_FALSE(Context.flowConditionImplies(FC, C)); } TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) { - auto &FC = Context.makeFlowConditionToken(); - auto &C = Context.create(); + auto &FC = A.makeFlowConditionToken(); + auto &C = A.create(); Context.addFlowConditionConstraint(FC, C); EXPECT_TRUE(Context.flowConditionImplies(FC, C)); } TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) { - auto &FC1 = Context.makeFlowConditionToken(); - auto &C1 = Context.create(); + auto &FC1 = A.makeFlowConditionToken(); + auto &C1 = A.create(); Context.addFlowConditionConstraint(FC1, C1); // Forked flow condition inherits the constraints of its parent flow @@ -173,22 +58,22 @@ TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) { // Adding a new constraint to the forked flow condition does not affect its // parent flow condition. - auto &C2 = Context.create(); + auto &C2 = A.create(); Context.addFlowConditionConstraint(FC2, C2); EXPECT_TRUE(Context.flowConditionImplies(FC2, C2)); EXPECT_FALSE(Context.flowConditionImplies(FC1, C2)); } TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) { - auto &C1 = Context.create(); - auto &C2 = Context.create(); - auto &C3 = Context.create(); + auto &C1 = A.create(); + auto &C2 = A.create(); + auto &C3 = A.create(); - auto &FC1 = Context.makeFlowConditionToken(); + auto &FC1 = A.makeFlowConditionToken(); Context.addFlowConditionConstraint(FC1, C1); Context.addFlowConditionConstraint(FC1, C3); - auto &FC2 = Context.makeFlowConditionToken(); + auto &FC2 = A.makeFlowConditionToken(); Context.addFlowConditionConstraint(FC2, C2); Context.addFlowConditionConstraint(FC2, C3); @@ -200,38 +85,37 @@ TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) { TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) { // Fresh flow condition with empty/no constraints is always true. - auto &FC1 = Context.makeFlowConditionToken(); + auto &FC1 = A.makeFlowConditionToken(); EXPECT_TRUE(Context.flowConditionIsTautology(FC1)); // Literal `true` is always true. - auto &FC2 = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint(FC2, Context.getBoolLiteralValue(true)); + auto &FC2 = A.makeFlowConditionToken(); + Context.addFlowConditionConstraint(FC2, A.makeLiteral(true)); EXPECT_TRUE(Context.flowConditionIsTautology(FC2)); // Literal `false` is never true. - auto &FC3 = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint(FC3, Context.getBoolLiteralValue(false)); + auto &FC3 = A.makeFlowConditionToken(); + Context.addFlowConditionConstraint(FC3, A.makeLiteral(false)); EXPECT_FALSE(Context.flowConditionIsTautology(FC3)); // We can't prove that an arbitrary bool A is always true... - auto &C1 = Context.create(); - auto &FC4 = Context.makeFlowConditionToken(); + auto &C1 = A.create(); + auto &FC4 = A.makeFlowConditionToken(); Context.addFlowConditionConstraint(FC4, C1); EXPECT_FALSE(Context.flowConditionIsTautology(FC4)); // ... but we can prove A || !A is true. - auto &FC5 = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint( - FC5, Context.getOrCreateDisjunction(C1, Context.getOrCreateNegation(C1))); + auto &FC5 = A.makeFlowConditionToken(); + Context.addFlowConditionConstraint(FC5, A.makeOr(C1, A.makeNot(C1))); EXPECT_TRUE(Context.flowConditionIsTautology(FC5)); } TEST_F(DataflowAnalysisContextTest, EquivBoolVals) { - auto &X = Context.create(); - auto &Y = Context.create(); - auto &Z = Context.create(); - auto &True = Context.getBoolLiteralValue(true); - auto &False = Context.getBoolLiteralValue(false); + auto &X = A.create(); + auto &Y = A.create(); + auto &Z = A.create(); + auto &True = A.makeLiteral(true); + auto &False = A.makeLiteral(false); // X == X EXPECT_TRUE(Context.equivalentBoolValues(X, X)); @@ -239,313 +123,39 @@ TEST_F(DataflowAnalysisContextTest, EquivBoolVals) { EXPECT_FALSE(Context.equivalentBoolValues(X, Y)); // !X != X - EXPECT_FALSE(Context.equivalentBoolValues(Context.getOrCreateNegation(X), X)); + EXPECT_FALSE(Context.equivalentBoolValues(A.makeNot(X), X)); // !(!X) = X - EXPECT_TRUE(Context.equivalentBoolValues( - Context.getOrCreateNegation(Context.getOrCreateNegation(X)), X)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeNot(A.makeNot(X)), X)); // (X || X) == X - EXPECT_TRUE( - Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, X), X)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, X), X)); // (X || Y) != X - EXPECT_FALSE( - Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y), X)); + EXPECT_FALSE(Context.equivalentBoolValues(A.makeOr(X, Y), X)); // (X || True) == True - EXPECT_TRUE(Context.equivalentBoolValues( - Context.getOrCreateDisjunction(X, True), True)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, True), True)); // (X || False) == X - EXPECT_TRUE(Context.equivalentBoolValues( - Context.getOrCreateDisjunction(X, False), X)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, False), X)); // (X && X) == X - EXPECT_TRUE( - Context.equivalentBoolValues(Context.getOrCreateConjunction(X, X), X)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, X), X)); // (X && Y) != X - EXPECT_FALSE( - Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y), X)); + EXPECT_FALSE(Context.equivalentBoolValues(A.makeAnd(X, Y), X)); // (X && True) == X - EXPECT_TRUE( - Context.equivalentBoolValues(Context.getOrCreateConjunction(X, True), X)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, True), X)); // (X && False) == False - EXPECT_TRUE(Context.equivalentBoolValues( - Context.getOrCreateConjunction(X, False), False)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, False), False)); // (X || Y) == (Y || X) - EXPECT_TRUE( - Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y), - Context.getOrCreateDisjunction(Y, X))); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, Y), A.makeOr(Y, X))); // (X && Y) == (Y && X) - EXPECT_TRUE( - Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y), - Context.getOrCreateConjunction(Y, X))); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, Y), A.makeAnd(Y, X))); // ((X || Y) || Z) == (X || (Y || Z)) - EXPECT_TRUE(Context.equivalentBoolValues( - Context.getOrCreateDisjunction(Context.getOrCreateDisjunction(X, Y), Z), - Context.getOrCreateDisjunction(X, Context.getOrCreateDisjunction(Y, Z)))); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(A.makeOr(X, Y), Z), + A.makeOr(X, A.makeOr(Y, Z)))); // ((X && Y) && Z) == (X && (Y && Z)) - EXPECT_TRUE(Context.equivalentBoolValues( - Context.getOrCreateConjunction(Context.getOrCreateConjunction(X, Y), Z), - Context.getOrCreateConjunction(X, Context.getOrCreateConjunction(Y, Z)))); -} - -#if !defined(NDEBUG) && GTEST_HAS_DEATH_TEST -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsTrueUnchanged) { - auto &True = Context.getBoolLiteralValue(true); - auto &Other = Context.create(); - - // FC = True - auto &FC = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint(FC, True); - - // `True` should never be substituted - EXPECT_DEATH(Context.buildAndSubstituteFlowCondition(FC, {{&True, &Other}}), - "Do not substitute true/false boolean literals"); -} - -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsFalseUnchanged) { - auto &False = Context.getBoolLiteralValue(false); - auto &Other = Context.create(); - - // FC = False - auto &FC = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint(FC, False); - - // `False` should never be substituted - EXPECT_DEATH(Context.buildAndSubstituteFlowCondition(FC, {{&False, &Other}}), - "Do not substitute true/false boolean literals"); -} -#endif - -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingAtomic) { - auto &X = Context.create(); - auto &True = Context.getBoolLiteralValue(true); - auto &False = Context.getBoolLiteralValue(false); - - // FC = X - auto &FC = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint(FC, X); - - // If X is true, FC is true - auto &FCWithXTrue = - Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}}); - EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True)); - - // If X is false, FC is false - auto &FC1WithXFalse = - Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}}); - EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, False)); -} - -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingNegation) { - auto &X = Context.create(); - auto &True = Context.getBoolLiteralValue(true); - auto &False = Context.getBoolLiteralValue(false); - - // FC = !X - auto &FC = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint(FC, Context.getOrCreateNegation(X)); - - // If X is true, FC is false - auto &FCWithXTrue = - Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}}); - EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, False)); - - // If X is false, FC is true - auto &FC1WithXFalse = - Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}}); - EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True)); -} - -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingDisjunction) { - auto &X = Context.create(); - auto &Y = Context.create(); - auto &True = Context.getBoolLiteralValue(true); - auto &False = Context.getBoolLiteralValue(false); - - // FC = X || Y - auto &FC = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint(FC, Context.getOrCreateDisjunction(X, Y)); - - // If X is true, FC is true - auto &FCWithXTrue = - Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}}); - EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, True)); - - // If X is false, FC is equivalent to Y - auto &FC1WithXFalse = - Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}}); - EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, Y)); -} - -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingConjunction) { - auto &X = Context.create(); - auto &Y = Context.create(); - auto &True = Context.getBoolLiteralValue(true); - auto &False = Context.getBoolLiteralValue(false); - - // FC = X && Y - auto &FC = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y)); - - // If X is true, FC is equivalent to Y - auto &FCWithXTrue = - Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}}); - EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y)); - - // If X is false, FC is false - auto &FCWithXFalse = - Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}}); - EXPECT_TRUE(Context.equivalentBoolValues(FCWithXFalse, False)); -} - -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingImplication) { - auto &X = Context.create(); - auto &Y = Context.create(); - auto &True = Context.getBoolLiteralValue(true); - auto &False = Context.getBoolLiteralValue(false); - - // FC = (X => Y) - auto &FC = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint(FC, Context.getOrCreateImplication(X, Y)); - - // If X is true, FC is equivalent to Y - auto &FCWithXTrue = - Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}}); - EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y)); - - // If X is false, FC is true - auto &FC1WithXFalse = - Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}}); - EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, True)); - - // If Y is true, FC is true - auto &FCWithYTrue = - Context.buildAndSubstituteFlowCondition(FC, {{&Y, &True}}); - EXPECT_TRUE(Context.equivalentBoolValues(FCWithYTrue, True)); - - // If Y is false, FC is equivalent to !X - auto &FCWithYFalse = - Context.buildAndSubstituteFlowCondition(FC, {{&Y, &False}}); - EXPECT_TRUE(Context.equivalentBoolValues(FCWithYFalse, - Context.getOrCreateNegation(X))); -} - -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionContainingBiconditional) { - auto &X = Context.create(); - auto &Y = Context.create(); - auto &True = Context.getBoolLiteralValue(true); - auto &False = Context.getBoolLiteralValue(false); - - // FC = (X <=> Y) - auto &FC = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint(FC, Context.getOrCreateIff(X, Y)); - - // If X is true, FC is equivalent to Y - auto &FCWithXTrue = - Context.buildAndSubstituteFlowCondition(FC, {{&X, &True}}); - EXPECT_TRUE(Context.equivalentBoolValues(FCWithXTrue, Y)); - - // If X is false, FC is equivalent to !Y - auto &FC1WithXFalse = - Context.buildAndSubstituteFlowCondition(FC, {{&X, &False}}); - EXPECT_TRUE(Context.equivalentBoolValues(FC1WithXFalse, - Context.getOrCreateNegation(Y))); - - // If Y is true, FC is equivalent to X - auto &FCWithYTrue = - Context.buildAndSubstituteFlowCondition(FC, {{&Y, &True}}); - EXPECT_TRUE(Context.equivalentBoolValues(FCWithYTrue, X)); - - // If Y is false, FC is equivalent to !X - auto &FCWithYFalse = - Context.buildAndSubstituteFlowCondition(FC, {{&Y, &False}}); - EXPECT_TRUE(Context.equivalentBoolValues(FCWithYFalse, - Context.getOrCreateNegation(X))); -} - -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsForkedFC) { - auto &X = Context.create(); - auto &Y = Context.create(); - auto &Z = Context.create(); - auto &True = Context.getBoolLiteralValue(true); - auto &False = Context.getBoolLiteralValue(false); - - // FC = X && Y - auto &FC = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint(FC, Context.getOrCreateConjunction(X, Y)); - // ForkedFC = FC && Z = X && Y && Z - auto &ForkedFC = Context.forkFlowCondition(FC); - Context.addFlowConditionConstraint(ForkedFC, Z); - - // If any of X,Y,Z is true in ForkedFC, ForkedFC = X && Y && Z is equivalent - // to evaluating the conjunction of the remaining values - auto &ForkedFCWithZTrue = - Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &True}}); - EXPECT_TRUE(Context.equivalentBoolValues( - ForkedFCWithZTrue, Context.getOrCreateConjunction(X, Y))); - auto &ForkedFCWithYAndZTrue = Context.buildAndSubstituteFlowCondition( - ForkedFC, {{&Y, &True}, {&Z, &True}}); - EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYAndZTrue, X)); - - // If any of X,Y,Z is false, ForkedFC is false - auto &ForkedFCWithXFalse = - Context.buildAndSubstituteFlowCondition(ForkedFC, {{&X, &False}}); - auto &ForkedFCWithYFalse = - Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Y, &False}}); - auto &ForkedFCWithZFalse = - Context.buildAndSubstituteFlowCondition(ForkedFC, {{&Z, &False}}); - EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithXFalse, False)); - EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithYFalse, False)); - EXPECT_TRUE(Context.equivalentBoolValues(ForkedFCWithZFalse, False)); -} - -TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsJoinedFC) { - auto &X = Context.create(); - auto &Y = Context.create(); - auto &Z = Context.create(); - auto &True = Context.getBoolLiteralValue(true); - auto &False = Context.getBoolLiteralValue(false); - - // FC1 = X - auto &FC1 = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint(FC1, X); - // FC2 = Y - auto &FC2 = Context.makeFlowConditionToken(); - Context.addFlowConditionConstraint(FC2, Y); - // JoinedFC = (FC1 || FC2) && Z = (X || Y) && Z - auto &JoinedFC = Context.joinFlowConditions(FC1, FC2); - Context.addFlowConditionConstraint(JoinedFC, Z); - - // If any of X, Y is true, JoinedFC is equivalent to Z - auto &JoinedFCWithXTrue = - Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &True}}); - auto &JoinedFCWithYTrue = - Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &True}}); - EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithXTrue, Z)); - EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithYTrue, Z)); - - // If Z is true, JoinedFC is equivalent to (X || Y) - auto &JoinedFCWithZTrue = - Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &True}}); - EXPECT_TRUE(Context.equivalentBoolValues( - JoinedFCWithZTrue, Context.getOrCreateDisjunction(X, Y))); - - // If any of X, Y is false, JoinedFC is equivalent to the conjunction of the - // other value and Z - auto &JoinedFCWithXFalse = - Context.buildAndSubstituteFlowCondition(JoinedFC, {{&X, &False}}); - auto &JoinedFCWithYFalse = - Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Y, &False}}); - EXPECT_TRUE(Context.equivalentBoolValues( - JoinedFCWithXFalse, Context.getOrCreateConjunction(Y, Z))); - EXPECT_TRUE(Context.equivalentBoolValues( - JoinedFCWithYFalse, Context.getOrCreateConjunction(X, Z))); - - // If Z is false, JoinedFC is false - auto &JoinedFCWithZFalse = - Context.buildAndSubstituteFlowCondition(JoinedFC, {{&Z, &False}}); - EXPECT_TRUE(Context.equivalentBoolValues(JoinedFCWithZFalse, False)); + EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(A.makeAnd(X, Y), Z), + A.makeAnd(X, A.makeAnd(Y, Z)))); } } // namespace