diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h new file mode 100644 --- /dev/null +++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h @@ -0,0 +1,128 @@ +//===-- 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; + } + + /// 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); + + /// 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 \ No newline at end of file diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h --- 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 @@ /*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 @@ /// 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 @@ 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 @@ const Options &getOptions() { return Opts; } + Arena &arena() { return *A; } + private: friend class Environment; @@ -361,28 +219,8 @@ 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 @@ 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 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h @@ -182,6 +182,8 @@ 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 @@ /// 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 @@ 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 @@ /// 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 @@ /// 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 @@ /// 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 @@ /// 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 --- /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 --- 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 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -58,9 +58,9 @@ : 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 @@ 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 @@ 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 @@ // 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::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::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 @@ } 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 @@ } } -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 @@ 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::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 --- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp @@ -240,7 +240,8 @@ } 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), @@ -358,7 +359,7 @@ 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); @@ -684,7 +685,7 @@ // with integers, and so distinguishing them serves no purpose, but could // prevent convergence. CreatedValuesCount++; - return &create(); + return &arena().create(); } if (Type->isReferenceType() || Type->isPointerType()) { @@ -702,9 +703,9 @@ } if (Type->isReferenceType()) - return &create(PointeeLoc); + return &arena().create(PointeeLoc); else - return &create(PointeeLoc); + return &arena().create(PointeeLoc); } if (Type->isRecordType()) { @@ -724,7 +725,7 @@ 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 --- /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 --- a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt +++ b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt @@ -4,6 +4,7 @@ ) 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 --- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp @@ -20,150 +20,35 @@ 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 @@ // 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, 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 @@ 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