--- /dev/null
+//===-- 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 <vector>
+
+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<AtomicBoolValue>()),
+ FalseVal(create<AtomicBoolValue>()) {}
+ 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 <typename T, typename... Args>
+ std::enable_if_t<std::is_base_of<StorageLocation, T>::value, T &>
+ create(Args &&...args) {
+ // Note: If allocation of individual `StorageLocation`s turns out to be
+ // costly, consider creating specializations of `create<T>` for commonly
+ // used `StorageLocation` subclasses and make them use a `BumpPtrAllocator`.
+ return *cast<T>(
+ Locs.emplace_back(std::make_unique<T>(std::forward<Args>(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 <typename T, typename... Args>
+ std::enable_if_t<std::is_base_of<Value, T>::value, T &>
+ create(Args &&...args) {
+ // Note: If allocation of individual `Value`s turns out to be costly,
+ // consider creating specializations of `create<T>` for commonly used
+ // `Value` subclasses and make them use a `BumpPtrAllocator`.
+ return *cast<T>(
+ Vals.emplace_back(std::make_unique<T>(std::forward<Args>(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<AtomicBoolValue>();
+ }
+
+private:
+ // Storage for the state of a program.
+ std::vector<std::unique_ptr<StorageLocation>> Locs;
+ std::vector<std::unique_ptr<Value>> Vals;
+
+ // Indices that are used to avoid recreating the same composite boolean
+ // values.
+ llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
+ ConjunctionVals;
+ llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
+ DisjunctionVals;
+ llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
+ llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ImplicationValue *>
+ ImplicationVals;
+ llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
+ BiconditionalVals;
+
+ AtomicBoolValue &TrueVal;
+ AtomicBoolValue &FalseVal;
+};
+
+} // namespace clang::dataflow
#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"
/*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 <typename T, typename... Args>
- std::enable_if_t<std::is_base_of<StorageLocation, T>::value, T &>
- create(Args &&...args) {
- // Note: If allocation of individual `StorageLocation`s turns out to be
- // costly, consider creating specializations of `create<T>` for commonly
- // used `StorageLocation` subclasses and make them use a `BumpPtrAllocator`.
- return *cast<T>(
- Locs.emplace_back(std::make_unique<T>(std::forward<Args>(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 <typename T, typename... Args>
- std::enable_if_t<std::is_base_of<Value, T>::value, T &>
- create(Args &&...args) {
- // Note: If allocation of individual `Value`s turns out to be costly,
- // consider creating specializations of `create<T>` for commonly used
- // `Value` subclasses and make them use a `BumpPtrAllocator`.
- return *cast<T>(
- Vals.emplace_back(std::make_unique<T>(std::forward<Args>(args)...))
- .get());
- }
-
- /// Takes ownership of `Loc` and returns a reference to it.
- ///
- /// This function is deprecated. Instead of
- /// `takeOwnership(std::make_unique<SomeStorageLocation>(args))`, prefer
- /// `create<SomeStorageLocation>(args)`.
- ///
- /// Requirements:
- ///
- /// `Loc` must not be null.
- template <typename T>
- LLVM_DEPRECATED("use create<T> instead", "")
- std::enable_if_t<std::is_base_of<StorageLocation, T>::value,
- T &> takeOwnership(std::unique_ptr<T> Loc) {
- assert(Loc != nullptr);
- Locs.push_back(std::move(Loc));
- return *cast<T>(Locs.back().get());
- }
-
- /// Takes ownership of `Val` and returns a reference to it.
- ///
- /// This function is deprecated. Instead of
- /// `takeOwnership(std::make_unique<SomeValue>(args))`, prefer
- /// `create<SomeValue>(args)`.
- ///
- /// Requirements:
- ///
- /// `Val` must not be null.
- template <typename T>
- LLVM_DEPRECATED("use create<T> instead", "")
- std::enable_if_t<std::is_base_of<Value, T>::value, T &> takeOwnership(
- std::unique_ptr<T> Val) {
- assert(Val != nullptr);
- Vals.push_back(std::move(Val));
- return *cast<T>(Vals.back().get());
- }
-
/// Returns a new storage location appropriate for `Type`.
///
/// A null `Type` is interpreted as the pointee type of `std::nullptr_t`.
/// 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<AtomicBoolValue> instead",
- "create<AtomicBoolValue>")
- AtomicBoolValue &createAtomicBoolValue() { return create<AtomicBoolValue>(); }
-
- /// 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<TopBoolValue> instead", "create<TopBoolValue>")
- TopBoolValue &createTopBoolValue() { return create<TopBoolValue>(); }
-
- /// 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);
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<AtomicBoolValue *, BoolValue *> 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);
const Options &getOptions() { return Opts; }
+ Arena &arena() { return *A; }
+
private:
friend class Environment;
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<BoolValue *, BoolValue *> &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<BoolValue *, BoolValue *> &SubstitutionsCache);
-
std::unique_ptr<Solver> S;
-
- // Storage for the state of a program.
- std::vector<std::unique_ptr<StorageLocation>> Locs;
- std::vector<std::unique_ptr<Value>> Vals;
+ std::unique_ptr<Arena> A;
// Maps from program declarations and statements to storage locations that are
// assigned to them. These assignments are global (aggregated across all basic
llvm::DenseMap<QualType, PointerValue *, NullableQualTypeDenseMapInfo>
NullPointerVals;
- AtomicBoolValue &TrueVal;
- AtomicBoolValue &FalseVal;
-
Options Opts;
- // Indices that are used to avoid recreating the same composite boolean
- // values.
- llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ConjunctionValue *>
- ConjunctionVals;
- llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, DisjunctionValue *>
- DisjunctionVals;
- llvm::DenseMap<BoolValue *, NegationValue *> NegationVals;
- llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, ImplicationValue *>
- ImplicationVals;
- llvm::DenseMap<std::pair<BoolValue *, BoolValue *>, BiconditionalValue *>
- BiconditionalVals;
-
// 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
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
/// 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 <typename T, typename... Args>
- std::enable_if_t<std::is_base_of<StorageLocation, T>::value, T &>
- create(Args &&...args) {
- return DACtx->create<T>(std::forward<Args>(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.
template <typename T, typename... Args>
std::enable_if_t<std::is_base_of<Value, T>::value, T &>
create(Args &&...args) {
- return DACtx->create<T>(std::forward<Args>(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<SomeStorageLocation>(args))`, prefer
- /// `create<SomeStorageLocation>(args)`.
- ///
- /// Requirements:
- ///
- /// `Loc` must not be null.
- template <typename T>
- LLVM_DEPRECATED("use create<T> instead", "")
- std::enable_if_t<std::is_base_of<StorageLocation, T>::value,
- T &> takeOwnership(std::unique_ptr<T> 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<SomeValue>(args))`, prefer
- /// `create<SomeValue>(args)`.
- ///
- /// Requirements:
- ///
- /// `Val` must not be null.
- template <typename T>
- LLVM_DEPRECATED("use create<T> instead", "")
- std::enable_if_t<std::is_base_of<Value, T>::value, T &> takeOwnership(
- std::unique_ptr<T> Val) {
- return DACtx->takeOwnership(std::move(Val));
+ return arena().create<T>(std::forward<Args>(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<AtomicBoolValue>();
+ return
arena().create<AtomicBoolValue>();
}
/// Returns a unique instance of boolean Top.
BoolValue &makeTopBoolValue() const {
- return DACtx->create<TopBoolValue>();
+ return arena().create<TopBoolValue>();
}
/// Returns a boolean value that represents the conjunction of `LHS` and
/// 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
/// 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
/// 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
/// 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<AtomicBoolValue *, BoolValue *> Substitutions) {
- return DACtx->buildAndSubstituteFlowCondition(Token,
- std::move(Substitutions));
- }
-
/// Adds `Val` to the set of clauses that constitute the flow condition.
void addToFlowCondition(BoolValue &Val);
--- /dev/null
+//===-- 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<BoolValue *, BoolValue *>
+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<ConjunctionValue>(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<DisjunctionValue>(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<NegationValue>(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<ImplicationValue>(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<BiconditionalValue>(LHS, RHS);
+ return *Res.first->second;
+}
+
+} // namespace clang::dataflow
add_clang_library(clangAnalysisFlowSensitive
+ Arena.cpp
ControlFlowContext.cpp
DataflowAnalysisContext.cpp
DataflowEnvironment.cpp
: getReferencedFields(Type);
for (const FieldDecl *Field : Fields)
FieldLocs.insert({Field, &createStorageLocation(Field->getType())});
- return create<AggregateStorageLocation>(Type, std::move(FieldLocs));
+ return
arena().create<AggregateStorageLocation>(Type, std::move(FieldLocs));
}
- return create<ScalarStorageLocation>(Type);
+ return arena().create<ScalarStorageLocation>(Type);
}
StorageLocation &
auto Res = NullPointerVals.try_emplace(CanonicalPointeeType, nullptr);
if (Res.second) {
auto &PointeeLoc = createStorageLocation(CanonicalPointeeType);
- Res.first->second = &create<PointerValue>(PointeeLoc);
+ Res.first->second = &
arena().create<PointerValue>(PointeeLoc);
}
return *Res.first->second;
}
-static std::pair<BoolValue *, BoolValue *>
-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<ConjunctionValue>(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<DisjunctionValue>(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<NegationValue>(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<ImplicationValue>(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<BiconditionalValue>(LHS, RHS);
- return *Res.first->second;
-}
-
-AtomicBoolValue &DataflowAnalysisContext::makeFlowConditionToken() {
- return create<AtomicBoolValue>();
-}
-
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;
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<BoolValue *> 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));
}
// 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<BoolValue *> Constraints = {&Token, &getOrCreateNegation(Val)};
+ llvm::DenseSet<BoolValue *> Constraints = {&Token,
+ &arena().makeNot(Val)};
llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
return isUnsatisfiable(std::move(Constraints));
bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
// Returns true if and only if we cannot prove that the flow condition can
// ever be false.
- llvm::DenseSet<BoolValue *> Constraints = {&getOrCreateNegation(Token)};
+ llvm::DenseSet<BoolValue *> Constraints = {
+ &arena().makeNot(Token)};
llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
return isUnsatisfiable(std::move(Constraints));
bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
BoolValue &Val2) {
llvm::DenseSet<BoolValue *> Constraints = {
- &getOrCreateNegation(getOrCreateIff(Val1, Val2))};
+ &arena().makeNot(arena().makeEquals(Val1, Val2))};
return isUnsatisfiable(Constraints);
}
} 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);
}
}
-BoolValue &DataflowAnalysisContext::substituteBoolValue(
- BoolValue &Val,
- llvm::DenseMap<BoolValue *, BoolValue *> &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<NegationValue>(&Val);
- auto &Sub = substituteBoolValue(Negation.getSubVal(), SubstitutionsCache);
- Result = &getOrCreateNegation(Sub);
- break;
- }
- case Value::Kind::Disjunction: {
- auto &Disjunct = *cast<DisjunctionValue>(&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<ConjunctionValue>(&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<ImplicationValue>(&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<BiconditionalValue>(&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<AtomicBoolValue *, BoolValue *> Substitutions) {
- assert(!Substitutions.contains(&getBoolLiteralValue(true)) &&
- !Substitutions.contains(&getBoolLiteralValue(false)) &&
- "Do not substitute true/false boolean literals");
- llvm::DenseMap<BoolValue *, BoolValue *> SubstitutionsCache(
- Substitutions.begin(), Substitutions.end());
- return buildAndSubstituteFlowConditionWithCache(Token, SubstitutionsCache);
-}
-
-BoolValue &DataflowAnalysisContext::buildAndSubstituteFlowConditionWithCache(
- AtomicBoolValue &Token,
- llvm::DenseMap<BoolValue *, BoolValue *> &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<BoolValue *> Constraints = {&Token};
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {
- {&getBoolLiteralValue(false), "False"},
- {&getBoolLiteralValue(true), "True"}};
+ {&arena().makeLiteral(false), "False"},
+ {&arena().makeLiteral(true), "True"}};
OS << debugString(Constraints, AtomNames);
}
DataflowAnalysisContext::DataflowAnalysisContext(std::unique_ptr<Solver> S,
Options Opts)
- : S(std::move(S)), TrueVal(create<AtomicBoolValue>()),
- FalseVal(create<AtomicBoolValue>()), Opts(Opts) {
+ : S(std::move(S)), A(std::make_unique<Arena>()), 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-
}
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),
QualType ParamType = Param->getType();
if (ParamType->isReferenceType()) {
- auto &Val = create<ReferenceValue>(*ArgLoc);
+ auto &Val = arena().create<ReferenceValue>(*ArgLoc);
setValue(Loc, Val);
} else if (auto *ArgVal = getValue(*ArgLoc)) {
setValue(Loc, *ArgVal);
// with integers, and so distinguishing them serves no purpose, but could
// prevent convergence.
CreatedValuesCount++;
- return &create<IntegerValue>();
+ return &arena().create<IntegerValue>();
}
if (Type->isReferenceType() || Type->isPointerType()) {
}
if (Type->isReferenceType())
- return &create<ReferenceValue>(PointeeLoc);
+ return &arena().create<ReferenceValue>(PointeeLoc);
else
- return &create<PointerValue>(PointeeLoc);
+ return &
arena().create<PointerValue>(PointeeLoc);
}
if (Type->isRecordType()) {
Visited.erase(FieldType.getCanonicalType());
}
- return &create<StructValue>(std::move(FieldValues));
+ return &arena().create<StructValue>(std::move(FieldValues));
}
return nullptr;
--- /dev/null
+//===- 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<AtomicBoolValue>();
+ auto &Y = A.create<AtomicBoolValue>();
+ EXPECT_NE(&X, &Y);
+}
+
+TEST_F(ArenaTest, CreateTopBoolValueReturnsDistinctValues) {
+ auto &X = A.create<TopBoolValue>();
+ auto &Y = A.create<TopBoolValue>();
+ EXPECT_NE(&X, &Y);
+}
+
+TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &XAndX = A.makeAnd(X, X);
+ EXPECT_EQ(&XAndX, &X);
+}
+
+TEST_F(ArenaTest, GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &Y = A.create<AtomicBoolValue>();
+ 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<AtomicBoolValue>();
+ auto &XAndZ = A.makeAnd(X, Z);
+ EXPECT_NE(&XAndY1, &XAndZ);
+}
+
+TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &XOrX = A.makeOr(X, X);
+ EXPECT_EQ(&XOrX, &X);
+}
+
+TEST_F(ArenaTest, GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &Y = A.create<AtomicBoolValue>();
+ 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<AtomicBoolValue>();
+ auto &XOrZ = A.makeOr(X, Z);
+ EXPECT_NE(&XOrY1, &XOrZ);
+}
+
+TEST_F(ArenaTest, GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &NotX1 = A.makeNot(X);
+ auto &NotX2 = A.makeNot(X);
+ EXPECT_EQ(&NotX1, &NotX2);
+
+ auto &Y = A.create<AtomicBoolValue>();
+ auto &NotY = A.makeNot(Y);
+ EXPECT_NE(&NotX1, &NotY);
+}
+
+TEST_F(ArenaTest, GetOrCreateImplicationReturnsTrueGivenSameArgs) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &XImpliesX = A.makeImplies(X, X);
+ EXPECT_EQ(&XImpliesX, &A.makeLiteral(true));
+}
+
+TEST_F(ArenaTest, GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &Y = A.create<AtomicBoolValue>();
+ 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<AtomicBoolValue>();
+ auto &XImpliesZ = A.makeImplies(X, Z);
+ EXPECT_NE(&XImpliesY1, &XImpliesZ);
+}
+
+TEST_F(ArenaTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &XIffX = A.makeEquals(X, X);
+ EXPECT_EQ(&XIffX, &A.makeLiteral(true));
+}
+
+TEST_F(ArenaTest, GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
+ auto &X = A.create<AtomicBoolValue>();
+ auto &Y = A.create<AtomicBoolValue>();
+ 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<AtomicBoolValue>();
+ auto &XIffZ = A.makeEquals(X, Z);
+ EXPECT_NE(&XIffY1, &XIffZ);
+}
+
+} // namespace
+} // namespace clang::dataflow
)
add_clang_unittest(ClangAnalysisFlowSensitiveTests
+ ArenaTest.cpp
CFGMatchSwitchTest.cpp
ChromiumCheckModelTest.cpp
DataflowAnalysisContextTest.cpp
class DataflowAnalysisContextTest : public ::testing::Test {
protected:
DataflowAnalysisContextTest()
- : Context(std::make_unique<WatchedLiteralsSolver>()) {}
+ : Context(std::make_unique<WatchedLiteralsSolver>()), A(Context.arena()) {
+ }
DataflowAnalysisContext Context;
+ Arena &A;
};
-TEST_F(DataflowAnalysisContextTest,
- CreateAtomicBoolValueReturnsDistinctValues) {
- auto &X = Context.create<AtomicBoolValue>();
- auto &Y = Context.create<AtomicBoolValue>();
- EXPECT_NE(&X, &Y);
-}
-
-TEST_F(DataflowAnalysisContextTest,
- CreateTopBoolValueReturnsDistinctValues) {
- auto &X = Context.create<TopBoolValue>();
- auto &Y = Context.create<TopBoolValue>();
- EXPECT_NE(&X, &Y);
-}
-
TEST_F(DataflowAnalysisContextTest, DistinctTopsNotEquivalent) {
- auto &X = Context.create<TopBoolValue>();
- auto &Y = Context.create<TopBoolValue>();
+ auto &X = A.create<TopBoolValue>();
+ auto &Y = A.create<TopBoolValue>();
EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
}
-TEST_F(DataflowAnalysisContextTest,
- GetOrCreateConjunctionReturnsSameExprGivenSameArgs) {
- auto &X = Context.create<AtomicBoolValue>();
- auto &XAndX = Context.getOrCreateConjunction(X, X);
- EXPECT_EQ(&XAndX, &X);
-}
-
-TEST_F(DataflowAnalysisContextTest,
- GetOrCreateConjunctionReturnsSameExprOnSubsequentCalls) {
- auto &X = Context.create<AtomicBoolValue>();
- auto &Y = Context.create<AtomicBoolValue>();
- 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<AtomicBoolValue>();
- auto &XAndZ = Context.getOrCreateConjunction(X, Z);
- EXPECT_NE(&XAndY1, &XAndZ);
-}
-
-TEST_F(DataflowAnalysisContextTest,
- GetOrCreateDisjunctionReturnsSameExprGivenSameArgs) {
- auto &X = Context.create<AtomicBoolValue>();
- auto &XOrX = Context.getOrCreateDisjunction(X, X);
- EXPECT_EQ(&XOrX, &X);
-}
-
-TEST_F(DataflowAnalysisContextTest,
- GetOrCreateDisjunctionReturnsSameExprOnSubsequentCalls) {
- auto &X = Context.create<AtomicBoolValue>();
- auto &Y = Context.create<AtomicBoolValue>();
- 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<AtomicBoolValue>();
- auto &XOrZ = Context.getOrCreateDisjunction(X, Z);
- EXPECT_NE(&XOrY1, &XOrZ);
-}
-
-TEST_F(DataflowAnalysisContextTest,
- GetOrCreateNegationReturnsSameExprOnSubsequentCalls) {
- auto &X = Context.create<AtomicBoolValue>();
- auto &NotX1 = Context.getOrCreateNegation(X);
- auto &NotX2 = Context.getOrCreateNegation(X);
- EXPECT_EQ(&NotX1, &NotX2);
-
- auto &Y = Context.create<AtomicBoolValue>();
- auto &NotY = Context.getOrCreateNegation(Y);
- EXPECT_NE(&NotX1, &NotY);
-}
-
-TEST_F(DataflowAnalysisContextTest,
- GetOrCreateImplicationReturnsTrueGivenSameArgs) {
- auto &X = Context.create<AtomicBoolValue>();
- auto &XImpliesX = Context.getOrCreateImplication(X, X);
- EXPECT_EQ(&XImpliesX, &Context.getBoolLiteralValue(true));
-}
-
-TEST_F(DataflowAnalysisContextTest,
- GetOrCreateImplicationReturnsSameExprOnSubsequentCalls) {
- auto &X = Context.create<AtomicBoolValue>();
- auto &Y = Context.create<AtomicBoolValue>();
- 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<AtomicBoolValue>();
- auto &XImpliesZ = Context.getOrCreateImplication(X, Z);
- EXPECT_NE(&XImpliesY1, &XImpliesZ);
-}
-
-TEST_F(DataflowAnalysisContextTest, GetOrCreateIffReturnsTrueGivenSameArgs) {
- auto &X = Context.create<AtomicBoolValue>();
- auto &XIffX = Context.getOrCreateIff(X, X);
- EXPECT_EQ(&XIffX, &Context.getBoolLiteralValue(true));
-}
-
-TEST_F(DataflowAnalysisContextTest,
- GetOrCreateIffReturnsSameExprOnSubsequentCalls) {
- auto &X = Context.create<AtomicBoolValue>();
- auto &Y = Context.create<AtomicBoolValue>();
- 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<AtomicBoolValue>();
- auto &XIffZ = Context.getOrCreateIff(X, Z);
- EXPECT_NE(&XIffY1, &XIffZ);
-}
-
TEST_F(DataflowAnalysisContextTest, EmptyFlowCondition) {
- auto &FC = Context.makeFlowConditionToken();
- auto &C =
Context.create<AtomicBoolValue>();
+ auto &FC = A.makeFlowConditionToken();
+ auto &C =
A.create<AtomicBoolValue>();
EXPECT_FALSE(Context.flowConditionImplies(FC, C));
}
TEST_F(DataflowAnalysisContextTest, AddFlowConditionConstraint) {
- auto &FC = Context.makeFlowConditionToken();
- auto &C =
Context.create<AtomicBoolValue>();
+ auto &FC = A.makeFlowConditionToken();
+ auto &C =
A.create<AtomicBoolValue>();
Context.addFlowConditionConstraint(FC, C);
EXPECT_TRUE(Context.flowConditionImplies(FC, C));
}
TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) {
- auto &FC1 = Context.makeFlowConditionToken();
- auto &C1 =
Context.create<AtomicBoolValue>();
+ auto &FC1 = A.makeFlowConditionToken();
+ auto &C1 =
A.create<AtomicBoolValue>();
Context.addFlowConditionConstraint(FC1, C1);
// Forked flow condition inherits the constraints of its parent flow
// Adding a new constraint to the forked flow condition does not affect its
// parent flow condition.
- auto &C2 =
Context.create<AtomicBoolValue>();
+ auto &C2 =
A.create<AtomicBoolValue>();
Context.addFlowConditionConstraint(FC2, C2);
EXPECT_TRUE(Context.flowConditionImplies(FC2, C2));
EXPECT_FALSE(Context.flowConditionImplies(FC1, C2));
}
TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
- auto &C1 =
Context.create<AtomicBoolValue>();
- auto &C2 =
Context.create<AtomicBoolValue>();
- auto &C3 =
Context.create<AtomicBoolValue>();
+ auto &C1 =
A.create<AtomicBoolValue>();
+ auto &C2 =
A.create<AtomicBoolValue>();
+ auto &C3 =
A.create<AtomicBoolValue>();
- 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);
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<AtomicBoolValue>();
- auto &FC4 = Context.makeFlowConditionToken();
+ auto &C1 =
A.create<AtomicBoolValue>();
+ auto &FC4 = A.makeFlowConditionToken();
Context.addFlowConditionConstraint(FC4, C1);
EXPECT_FALSE(Context.flowConditionIsTautology(FC4));
// ... but we can prove A || !A is true.
- 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<AtomicBoolValue>();
- auto &Y =
Context.create<AtomicBoolValue>();
- auto &Z =
Context.create<AtomicBoolValue>();
- auto &True = Context.getBoolLiteralValue(true);
- auto &False = Context.getBoolLiteralValue(false);
+ auto &X =
A.create<AtomicBoolValue>();
+ auto &Y =
A.create<AtomicBoolValue>();
+ auto &Z =
A.create<AtomicBoolValue>();
+ auto &True = A.makeLiteral(true);
+ auto &False = A.makeLiteral(false);
// X == X
EXPECT_TRUE(Context.equivalentBoolValues(X, X));
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<AtomicBoolValue>();
-
- // 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<AtomicBoolValue>();
-
- // 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<AtomicBoolValue>();
- 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<AtomicBoolValue>();
- 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<AtomicBoolValue>();
- auto &Y = Context.create<AtomicBoolValue>();
- 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<AtomicBoolValue>();
- auto &Y = Context.create<AtomicBoolValue>();
- 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<AtomicBoolValue>();
- auto &Y = Context.create<AtomicBoolValue>();
- 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<AtomicBoolValue>();
- auto &Y = Context.create<AtomicBoolValue>();
- 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<AtomicBoolValue>();
- auto &Y = Context.create<AtomicBoolValue>();
- auto &Z = Context.create<AtomicBoolValue>();
- 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<AtomicBoolValue>();
- auto &Y = Context.create<AtomicBoolValue>();
- auto &Z = Context.create<AtomicBoolValue>();
- 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
projects / platform / upstream / llvm.git / commitdiff