[clang] bf47c1e - [dataflow] Extract arena for Value/StorageLocation out of DataflowAnalysisContext
Sam McCall via cfe-commits
cfe-commits at lists.llvm.org
Wed Apr 19 05:32:21 PDT 2023
Author: Sam McCall
Date: 2023-04-19T14:32:13+02:00
New Revision: bf47c1ed855605324efcca4af92517026c7e53e5
URL: https://github.com/llvm/llvm-project/commit/bf47c1ed855605324efcca4af92517026c7e53e5
DIFF: https://github.com/llvm/llvm-project/commit/bf47c1ed855605324efcca4af92517026c7e53e5.diff
LOG: [dataflow] Extract arena for Value/StorageLocation out of DataflowAnalysisContext
DataflowAnalysisContext has a few too many responsibilities, this narrows them.
It also allows the Arena to be shared with analysis steps, which need to create
Values, without exposing the whole DACtx API (flow conditions etc).
This means Environment no longer needs to proxy all these methods.
(For now it still does, because there are many callsites to update, and maybe
if we separate bool formulas from values we can avoid churning them twice)
In future, if we untangle the concepts of Values from boolean formulas/atoms,
Arena would also be responsible for creating formulas and managing atom IDs.
Differential Revision: https://reviews.llvm.org/D148554
Added:
clang/include/clang/Analysis/FlowSensitive/Arena.h
clang/lib/Analysis/FlowSensitive/Arena.cpp
clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
Modified:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/lib/Analysis/FlowSensitive/CMakeLists.txt
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
Removed:
################################################################################
diff --git a/clang/include/clang/Analysis/FlowSensitive/Arena.h b/clang/include/clang/Analysis/FlowSensitive/Arena.h
new file mode 100644
index 0000000000000..8dc51e044b14f
--- /dev/null
+++ b/clang/include/clang/Analysis/FlowSensitive/Arena.h
@@ -0,0 +1,120 @@
+//===-- Arena.h -------------------------------*- C++ -------------------*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/StorageLocation.h"
+#include "clang/Analysis/FlowSensitive/Value.h"
+#include <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
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
index 31bd9809a72a0..9695884c00c98 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -18,6 +18,7 @@
#include "clang/AST/Decl.h"
#include "clang/AST/Expr.h"
#include "clang/AST/TypeOrdering.h"
+#include "clang/Analysis/FlowSensitive/Arena.h"
#include "clang/Analysis/FlowSensitive/ControlFlowContext.h"
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/StorageLocation.h"
@@ -86,74 +87,6 @@ class DataflowAnalysisContext {
/*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`.
@@ -205,62 +138,6 @@ class DataflowAnalysisContext {
/// 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);
@@ -275,27 +152,6 @@ class DataflowAnalysisContext {
AtomicBoolValue &joinFlowConditions(AtomicBoolValue &FirstToken,
AtomicBoolValue &SecondToken);
- // FIXME: This function returns the flow condition expressed directly as its
- // constraints: (C1 AND C2 AND ...). This
diff ers 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);
@@ -318,6 +174,8 @@ class DataflowAnalysisContext {
const Options &getOptions() { return Opts; }
+ Arena &arena() { return *A; }
+
private:
friend class Environment;
@@ -361,28 +219,8 @@ class DataflowAnalysisContext {
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
@@ -401,23 +239,8 @@ class DataflowAnalysisContext {
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
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
index 4e65d974133a6..8690616411db9 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -182,6 +182,8 @@ class Environment {
return DACtx->getOptions();
}
+ Arena &arena() const { return DACtx->arena(); }
+
Logger &logger() const { return *DACtx->getOptions().Log; }
/// Creates and returns an environment to use for an inline analysis of the
@@ -319,16 +321,7 @@ class Environment {
/// 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.
@@ -338,57 +331,23 @@ class Environment {
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
@@ -396,7 +355,7 @@ class Environment {
/// order, will return the same result. If the given boolean values represent
/// the same value, the result will be the value itself.
BoolValue &makeAnd(BoolValue &LHS, BoolValue &RHS) const {
- return DACtx->getOrCreateConjunction(LHS, RHS);
+ return arena().makeAnd(LHS, RHS);
}
/// Returns a boolean value that represents the disjunction of `LHS` and
@@ -404,13 +363,13 @@ class Environment {
/// order, will return the same result. If the given boolean values represent
/// the same value, the result will be the value itself.
BoolValue &makeOr(BoolValue &LHS, BoolValue &RHS) const {
- return DACtx->getOrCreateDisjunction(LHS, RHS);
+ return arena().makeOr(LHS, RHS);
}
/// Returns a boolean value that represents the negation of `Val`. Subsequent
/// calls with the same argument will return the same result.
BoolValue &makeNot(BoolValue &Val) const {
- return DACtx->getOrCreateNegation(Val);
+ return arena().makeNot(Val);
}
/// Returns a boolean value represents `LHS` => `RHS`. Subsequent calls with
@@ -418,7 +377,7 @@ class Environment {
/// values represent the same value, the result will be a value that
/// represents the true boolean literal.
BoolValue &makeImplication(BoolValue &LHS, BoolValue &RHS) const {
- return DACtx->getOrCreateImplication(LHS, RHS);
+ return arena().makeImplies(LHS, RHS);
}
/// Returns a boolean value represents `LHS` <=> `RHS`. Subsequent calls with
@@ -426,22 +385,12 @@ class Environment {
/// result. If the given boolean values represent the same value, the result
/// will be a value that represents the true boolean literal.
BoolValue &makeIff(BoolValue &LHS, BoolValue &RHS) const {
- return DACtx->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);
diff --git a/clang/lib/Analysis/FlowSensitive/Arena.cpp b/clang/lib/Analysis/FlowSensitive/Arena.cpp
new file mode 100644
index 0000000000000..a0182af85a228
--- /dev/null
+++ b/clang/lib/Analysis/FlowSensitive/Arena.cpp
@@ -0,0 +1,71 @@
+//===-- Arena.cpp ---------------------------------------------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/Arena.h"
+
+namespace clang::dataflow {
+
+static std::pair<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
diff --git a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
index a3216518f4dba..86646662c4da9 100644
--- a/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/lib/Analysis/FlowSensitive/CMakeLists.txt
@@ -1,4 +1,5 @@
add_clang_library(clangAnalysisFlowSensitive
+ Arena.cpp
ControlFlowContext.cpp
DataflowAnalysisContext.cpp
DataflowEnvironment.cpp
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
index 1fbc3759747e8..ad57fd156f443 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -58,9 +58,9 @@ StorageLocation &DataflowAnalysisContext::createStorageLocation(QualType Type) {
: getReferencedFields(Type);
for (const FieldDecl *Field : Fields)
FieldLocs.insert({Field, &createStorageLocation(Field->getType())});
- return create<AggregateStorageLocation>(Type, std::move(FieldLocs));
+ return arena().create<AggregateStorageLocation>(Type, std::move(FieldLocs));
}
- return create<ScalarStorageLocation>(Type);
+ return arena().create<ScalarStorageLocation>(Type);
}
StorageLocation &
@@ -88,88 +88,23 @@ DataflowAnalysisContext::getOrCreateNullPointerValue(QualType PointeeType) {
auto Res = NullPointerVals.try_emplace(CanonicalPointeeType, nullptr);
if (Res.second) {
auto &PointeeLoc = createStorageLocation(CanonicalPointeeType);
- Res.first->second = &create<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;
@@ -178,18 +113,19 @@ DataflowAnalysisContext::forkFlowCondition(AtomicBoolValue &Token) {
AtomicBoolValue &
DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken,
AtomicBoolValue &SecondToken) {
- auto &Token = makeFlowConditionToken();
+ auto &Token = arena().makeFlowConditionToken();
FlowConditionDeps[&Token].insert(&FirstToken);
FlowConditionDeps[&Token].insert(&SecondToken);
- addFlowConditionConstraint(Token,
- getOrCreateDisjunction(FirstToken, SecondToken));
+ addFlowConditionConstraint(
+ Token, arena().makeOr(FirstToken, SecondToken));
return Token;
}
Solver::Result
DataflowAnalysisContext::querySolver(llvm::DenseSet<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));
}
@@ -200,7 +136,8 @@ bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
// reducing the problem to satisfiability checking. In other words, we attempt
// to show that assuming `Val` is false makes the constraints induced by the
// flow condition unsatisfiable.
- llvm::DenseSet<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));
@@ -209,7 +146,8 @@ bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
// Returns true if and only if we cannot prove that the flow condition can
// ever be false.
- llvm::DenseSet<BoolValue *> Constraints = {&getOrCreateNegation(Token)};
+ llvm::DenseSet<BoolValue *> Constraints = {
+ &arena().makeNot(Token)};
llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
return isUnsatisfiable(std::move(Constraints));
@@ -218,7 +156,7 @@ bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) {
bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1,
BoolValue &Val2) {
llvm::DenseSet<BoolValue *> Constraints = {
- &getOrCreateNegation(getOrCreateIff(Val1, Val2))};
+ &arena().makeNot(arena().makeEquals(Val1, Val2))};
return isUnsatisfiable(Constraints);
}
@@ -235,7 +173,7 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
} else {
// Bind flow condition token via `iff` to its set of constraints:
// FC <=> (C1 ^ C2 ^ ...), where Ci are constraints
- Constraints.insert(&getOrCreateIff(Token, *ConstraintsIt->second));
+ Constraints.insert(&arena().makeEquals(Token, *ConstraintsIt->second));
}
auto DepsIt = FlowConditionDeps.find(&Token);
@@ -247,101 +185,6 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
}
}
-BoolValue &DataflowAnalysisContext::substituteBoolValue(
- BoolValue &Val,
- llvm::DenseMap<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};
@@ -349,8 +192,8 @@ void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &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);
}
@@ -377,8 +220,7 @@ DataflowAnalysisContext::getControlFlowContext(const FunctionDecl *F) {
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-
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
index 9f5b3adc8b1b1..446178a2a5eae 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -262,7 +262,8 @@ void Environment::initFieldsGlobalsAndFuncs(const FunctionDecl *FuncDecl) {
}
Environment::Environment(DataflowAnalysisContext &DACtx)
- : DACtx(&DACtx), FlowConditionToken(&DACtx.makeFlowConditionToken()) {}
+ : DACtx(&DACtx),
+ FlowConditionToken(&DACtx.arena().makeFlowConditionToken()) {}
Environment::Environment(const Environment &Other)
: DACtx(Other.DACtx), CallStack(Other.CallStack),
@@ -380,7 +381,7 @@ void Environment::pushCallInternal(const FunctionDecl *FuncDecl,
QualType ParamType = Param->getType();
if (ParamType->isReferenceType()) {
- auto &Val = create<ReferenceValue>(*ArgLoc);
+ auto &Val = arena().create<ReferenceValue>(*ArgLoc);
setValue(Loc, Val);
} else if (auto *ArgVal = getValue(*ArgLoc)) {
setValue(Loc, *ArgVal);
@@ -706,7 +707,7 @@ Value *Environment::createValueUnlessSelfReferential(
// with integers, and so distinguishing them serves no purpose, but could
// prevent convergence.
CreatedValuesCount++;
- return &create<IntegerValue>();
+ return &arena().create<IntegerValue>();
}
if (Type->isReferenceType() || Type->isPointerType()) {
@@ -724,9 +725,9 @@ Value *Environment::createValueUnlessSelfReferential(
}
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()) {
@@ -746,7 +747,7 @@ Value *Environment::createValueUnlessSelfReferential(
Visited.erase(FieldType.getCanonicalType());
}
- return &create<StructValue>(std::move(FieldValues));
+ return &arena().create<StructValue>(std::move(FieldValues));
}
return nullptr;
diff --git a/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
new file mode 100644
index 0000000000000..407abf58529a5
--- /dev/null
+++ b/clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
@@ -0,0 +1,129 @@
+//===- ArenaTest.cpp ------------------------------------------------------===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/Analysis/FlowSensitive/Arena.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+
+namespace clang::dataflow {
+namespace {
+
+class ArenaTest : public ::testing::Test {
+protected:
+ Arena A;
+};
+
+TEST_F(ArenaTest, CreateAtomicBoolValueReturnsDistinctValues) {
+ auto &X = A.create<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
diff --git a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
index 0895cdeaabb3e..e1e9581bd25b4 100644
--- a/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
+++ b/clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
@@ -4,6 +4,7 @@ set(LLVM_LINK_COMPONENTS
)
add_clang_unittest(ClangAnalysisFlowSensitiveTests
+ ArenaTest.cpp
CFGMatchSwitchTest.cpp
ChromiumCheckModelTest.cpp
DataflowAnalysisContextTest.cpp
diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
index 52b2d5c7a33a3..bb76648abdc05 100644
--- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
@@ -20,150 +20,35 @@ using namespace dataflow;
class DataflowAnalysisContextTest : public ::testing::Test {
protected:
DataflowAnalysisContextTest()
- : Context(std::make_unique<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
@@ -173,22 +58,22 @@ TEST_F(DataflowAnalysisContextTest, ForkFlowCondition) {
// Adding a new constraint to the forked flow condition does not affect its
// parent flow condition.
- auto &C2 = Context.create<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);
@@ -200,38 +85,37 @@ TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) {
TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) {
// Fresh flow condition with empty/no constraints is always true.
- auto &FC1 = Context.makeFlowConditionToken();
+ auto &FC1 = A.makeFlowConditionToken();
EXPECT_TRUE(Context.flowConditionIsTautology(FC1));
// Literal `true` is always true.
- auto &FC2 = Context.makeFlowConditionToken();
- Context.addFlowConditionConstraint(FC2, Context.getBoolLiteralValue(true));
+ auto &FC2 = A.makeFlowConditionToken();
+ Context.addFlowConditionConstraint(FC2, A.makeLiteral(true));
EXPECT_TRUE(Context.flowConditionIsTautology(FC2));
// Literal `false` is never true.
- auto &FC3 = Context.makeFlowConditionToken();
- Context.addFlowConditionConstraint(FC3, Context.getBoolLiteralValue(false));
+ auto &FC3 = A.makeFlowConditionToken();
+ Context.addFlowConditionConstraint(FC3, A.makeLiteral(false));
EXPECT_FALSE(Context.flowConditionIsTautology(FC3));
// We can't prove that an arbitrary bool A is always true...
- auto &C1 = Context.create<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));
@@ -239,313 +123,39 @@ TEST_F(DataflowAnalysisContextTest, EquivBoolVals) {
EXPECT_FALSE(Context.equivalentBoolValues(X, Y));
// !X != X
- EXPECT_FALSE(Context.equivalentBoolValues(Context.getOrCreateNegation(X), X));
+ EXPECT_FALSE(Context.equivalentBoolValues(A.makeNot(X), X));
// !(!X) = X
- EXPECT_TRUE(Context.equivalentBoolValues(
- Context.getOrCreateNegation(Context.getOrCreateNegation(X)), X));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeNot(A.makeNot(X)), X));
// (X || X) == X
- EXPECT_TRUE(
- Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, X), X));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, X), X));
// (X || Y) != X
- EXPECT_FALSE(
- Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y), X));
+ EXPECT_FALSE(Context.equivalentBoolValues(A.makeOr(X, Y), X));
// (X || True) == True
- EXPECT_TRUE(Context.equivalentBoolValues(
- Context.getOrCreateDisjunction(X, True), True));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, True), True));
// (X || False) == X
- EXPECT_TRUE(Context.equivalentBoolValues(
- Context.getOrCreateDisjunction(X, False), X));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, False), X));
// (X && X) == X
- EXPECT_TRUE(
- Context.equivalentBoolValues(Context.getOrCreateConjunction(X, X), X));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, X), X));
// (X && Y) != X
- EXPECT_FALSE(
- Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y), X));
+ EXPECT_FALSE(Context.equivalentBoolValues(A.makeAnd(X, Y), X));
// (X && True) == X
- EXPECT_TRUE(
- Context.equivalentBoolValues(Context.getOrCreateConjunction(X, True), X));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, True), X));
// (X && False) == False
- EXPECT_TRUE(Context.equivalentBoolValues(
- Context.getOrCreateConjunction(X, False), False));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, False), False));
// (X || Y) == (Y || X)
- EXPECT_TRUE(
- Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y),
- Context.getOrCreateDisjunction(Y, X)));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(X, Y), A.makeOr(Y, X)));
// (X && Y) == (Y && X)
- EXPECT_TRUE(
- Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y),
- Context.getOrCreateConjunction(Y, X)));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeAnd(X, Y), A.makeAnd(Y, X)));
// ((X || Y) || Z) == (X || (Y || Z))
- EXPECT_TRUE(Context.equivalentBoolValues(
- Context.getOrCreateDisjunction(Context.getOrCreateDisjunction(X, Y), Z),
- Context.getOrCreateDisjunction(X, Context.getOrCreateDisjunction(Y, Z))));
+ EXPECT_TRUE(Context.equivalentBoolValues(A.makeOr(A.makeOr(X, Y), Z),
+ A.makeOr(X, A.makeOr(Y, Z))));
// ((X && Y) && Z) == (X && (Y && Z))
- EXPECT_TRUE(Context.equivalentBoolValues(
- Context.getOrCreateConjunction(Context.getOrCreateConjunction(X, Y), Z),
- Context.getOrCreateConjunction(X, Context.getOrCreateConjunction(Y, Z))));
-}
-
-#if !defined(NDEBUG) && GTEST_HAS_DEATH_TEST
-TEST_F(DataflowAnalysisContextTest, SubstituteFlowConditionsTrueUnchanged) {
- auto &True = Context.getBoolLiteralValue(true);
- auto &Other = Context.create<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
More information about the cfe-commits
mailing list