DataflowAnalysisContext has a few too many responsibilities, this narrows them.
It also allows the Arena to be shared with analysis steps, which need to create
Values, without exposing the whole DACtx API (flow conditions etc).
This means Environment no longer needs to proxy all these methods.
(For now it still does, because there are many callsites to update, and maybe
if we separate bool formulas from values we can avoid churning them twice)
In future, if we untangle the concepts of Values from boolean formulas/atoms,
Arena would also be responsible for creating formulas and managing atom IDs.
Differential Revision: https://reviews.llvm.org/D148554
--- /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