https://github.com/ymand updated https://github.com/llvm/llvm-project/pull/87233
>From b7f63ed7ca3c503f55eccc215f0a66368e2c5e5e Mon Sep 17 00:00:00 2001
From: Yitzhak Mandelbaum <yitzh...@google.com>
Date: Mon, 1 Apr 2024 12:13:39 +0000
Subject: [PATCH] [clang][dataflow] Refactor `widen` API to be explicit about
change effect.
The previous API relied on pointer equality of inputs and outputs to signal
whether a change occured. This was too subtle and led to bugs in practice. It
was also very limiting: the override could not return an equivalent (but not
identical) value.
---
.../FlowSensitive/DataflowEnvironment.h | 47 ++++++++++++-------
.../FlowSensitive/DataflowEnvironment.cpp | 43 ++++++++++-------
2 files changed, 56 insertions(+), 34 deletions(-)
diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
index c30bccd06674a4..0a37d9d68e2898 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -97,6 +97,16 @@ class Environment {
const Value &Val2, const Environment &Env2,
Value &JoinedVal, Environment &JoinedEnv) {}
+ /// The result of the `widen` operation.
+ struct WidenResult {
+ /// Non-null pointer to a potentially widened version of the widening
+ /// input.
+ Value *V;
+ /// Whether `V` represents a "change" (that is, a different value) with
+ /// respect to the previous value in the sequence.
+ LatticeJoinEffect Effect;
+ };
+
/// This function may widen the current value -- replace it with an
/// approximation that can reach a fixed point more quickly than iterated
/// application of the transfer function alone. The previous value is
@@ -104,14 +114,17 @@ class Environment {
/// serve as a comparison operation, by indicating whether the widened
value
/// is equivalent to the previous value.
///
- /// Returns either:
- ///
- /// `nullptr`, if this value is not of interest to the model, or
- ///
- /// `&Prev`, if the widened value is equivalent to `Prev`, or
- ///
- /// A non-null value that approximates `Current`. `Prev` is available to
- /// inform the chosen approximation.
+ /// Returns one of the folowing:
+ /// * `std::nullopt`, if this value is not of interest to the
+ /// model.
+ /// * A `WidenResult` with:
+ /// * A non-null `Value *` that points either to `Current` or a widened
+ /// version of `Current`. This value must be consistent with
+ /// the flow condition of `CurrentEnv`. We particularly caution
+ /// against using `Prev`, which is rarely consistent.
+ /// * A `LatticeJoinEffect` indicating whether the value should be
+ /// considered a new value (`Changed`) or one *equivalent* (if not
+ /// necessarily equal) to `Prev` (`Unchanged`).
///
/// `PrevEnv` and `CurrentEnv` can be used to query child values and path
/// condition implications of `Prev` and `Current`, respectively.
@@ -122,17 +135,19 @@ class Environment {
///
/// `Prev` and `Current` must be assigned to the same storage location in
/// `PrevEnv` and `CurrentEnv`, respectively.
- virtual Value *widen(QualType Type, Value &Prev, const Environment
&PrevEnv,
- Value &Current, Environment &CurrentEnv) {
+ virtual std::optional<WidenResult> widen(QualType Type, Value &Prev,
+ const Environment &PrevEnv,
+ Value &Current,
+ Environment &CurrentEnv) {
// The default implementation reduces to just comparison, since
comparison
// is required by the API, even if no widening is performed.
switch (compare(Type, Prev, PrevEnv, Current, CurrentEnv)) {
- case ComparisonResult::Same:
- return &Prev;
- case ComparisonResult::Different:
- return &Current;
- case ComparisonResult::Unknown:
- return nullptr;
+ case ComparisonResult::Unknown:
+ return std::nullopt;
+ case ComparisonResult::Same:
+ return WidenResult{&Current, LatticeJoinEffect::Unchanged};
+ case ComparisonResult::Different:
+ return WidenResult{&Current, LatticeJoinEffect::Changed};
}
llvm_unreachable("all cases in switch covered");
}
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
index f729d676dd0de8..8ae51b7cdb444d 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -166,17 +166,20 @@ static Value *joinDistinctValues(QualType Type, Value
&Val1,
return JoinedVal;
}
-// When widening does not change `Current`, return value will equal `&Prev`.
-static Value &widenDistinctValues(QualType Type, Value &Prev,
- const Environment &PrevEnv, Value &Current,
- Environment &CurrentEnv,
- Environment::ValueModel &Model) {
+namespace {
+using WidenResult = Environment::ValueModel::WidenResult;
+}
+
+static WidenResult widenDistinctValues(QualType Type, Value &Prev,
+ const Environment &PrevEnv,
+ Value &Current, Environment &CurrentEnv,
+ Environment::ValueModel &Model) {
// Boolean-model widening.
if (auto *PrevBool = dyn_cast<BoolValue>(&Prev)) {
- // If previous value was already Top, re-use that to (implicitly) indicate
- // that no change occurred.
if (isa<TopBoolValue>(Prev))
- return Prev;
+ // Safe to return `Prev` here, because Top is never dependent on the
+ // environment.
+ return {&Prev, LatticeJoinEffect::Unchanged};
// We may need to widen to Top, but before we do so, check whether both
// values are implied to be either true or false in the current
environment.
@@ -185,22 +188,26 @@ static Value &widenDistinctValues(QualType Type, Value
&Prev,
bool TruePrev = PrevEnv.proves(PrevBool->formula());
bool TrueCur = CurrentEnv.proves(CurBool.formula());
if (TruePrev && TrueCur)
- return CurrentEnv.getBoolLiteralValue(true);
+ return {&CurrentEnv.getBoolLiteralValue(true),
+ LatticeJoinEffect::Unchanged};
if (!TruePrev && !TrueCur &&
PrevEnv.proves(PrevEnv.arena().makeNot(PrevBool->formula())) &&
CurrentEnv.proves(CurrentEnv.arena().makeNot(CurBool.formula())))
- return CurrentEnv.getBoolLiteralValue(false);
+ return {&CurrentEnv.getBoolLiteralValue(false),
+ LatticeJoinEffect::Unchanged};
- return CurrentEnv.makeTopBoolValue();
+ return {&CurrentEnv.makeTopBoolValue(), LatticeJoinEffect::Changed};
}
// FIXME: Add other built-in model widening.
// Custom-model widening.
- if (auto *W = Model.widen(Type, Prev, PrevEnv, Current, CurrentEnv))
- return *W;
+ if (auto Result = Model.widen(Type, Prev, PrevEnv, Current, CurrentEnv))
+ return *Result;
- return equateUnknownValues(Prev.getKind()) ? Prev : Current;
+ return {&Current, equateUnknownValues(Prev.getKind())
+ ? LatticeJoinEffect::Unchanged
+ : LatticeJoinEffect::Changed};
}
// Returns whether the values in `Map1` and `Map2` compare equal for those
@@ -290,10 +297,10 @@ widenKeyToValueMap(const llvm::MapVector<Key, Value *>
&CurMap,
continue;
}
- Value &WidenedVal = widenDistinctValues(K->getType(), *PrevIt->second,
- PrevEnv, *Val, CurEnv, Model);
- WidenedMap.insert({K, &WidenedVal});
- if (&WidenedVal != PrevIt->second)
+ auto [WidenedVal, ValEffect] = widenDistinctValues(
+ K->getType(), *PrevIt->second, PrevEnv, *Val, CurEnv, Model);
+ WidenedMap.insert({K, WidenedVal});
+ if (ValEffect == LatticeJoinEffect::Changed)
Effect = LatticeJoinEffect::Changed;
}
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
