ymandel created this revision.
ymandel added reviewers: gribozavr2, xazax.hun.
Herald added subscribers: martong, rnkovacs.
Herald added a reviewer: NoQ.
Herald added a project: All.
ymandel requested review of this revision.
Herald added a project: clang.
The comments describing the API for analysis `widen` and the environment `widen`
were overly strict in the preconditions they assumed for the operation. In
particular, both assumed that the previous value preceded the current value in
the relevant ordering. However, that's not generally how widen operators work
and widening itself can violate this property. That is, when the previous value
is the result of a widening, it can easily be "greater" than the current value.
This patch updates the comments to accurately reflect the expectations.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D140308
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
Index: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -370,15 +370,18 @@
auto Effect = LatticeJoinEffect::Unchanged;
- // By the API, `PrevEnv` <= `*this`, meaning `join(PrevEnv, *this) =
- // *this`. That guarantees that these maps are subsets of the maps in
- // `PrevEnv`. So, we don't need change their current values to widen (in
- // contrast to `join`).
+ // By the API, `PrevEnv` is a previous version of the environment for the
same
+ // block, so we have some guarantees about its shape. In particular, it will
+ // be the result of a join or widen operation on previous values for this
+ // block. For `DeclToLoc` and `ExprToLoc`, join guarantees that these maps
are
+ // subsets of the maps in `PrevEnv`. So, as long as we maintain this property
+ // here, we don't need change their current values to widen.
//
- // FIXME: The above is violated for `MemberLocToStruct`, because `join` can
- // cause the map size to increase (when we add fresh data in places of
- // conflict). Once this issue with join is resolved, re-enable the assertion
- // below or replace with something that captures the desired invariant.
+ // FIXME: `MemberLocToStruct` does not share the above property, because
+ // `join` can cause the map size to increase (when we add fresh data in
places
+ // of conflict). Once this issue with join is resolved, re-enable the
+ // assertion below or replace with something that captures the desired
+ // invariant.
assert(DeclToLoc.size() <= PrevEnv.DeclToLoc.size());
assert(ExprToLoc.size() <= PrevEnv.ExprToLoc.size());
// assert(MemberLocToStruct.size() <= PrevEnv.MemberLocToStruct.size());
Index: clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -137,10 +137,6 @@
///
/// Requirements:
///
- /// `Prev` must precede `Current` in the value ordering. Widening is *not*
- /// called when the current value is already equivalent to the previous
- /// value.
- ///
/// `Prev` and `Current` must model values of type `Type`.
///
/// `Prev` and `Current` must be assigned to the same storage location in
@@ -229,7 +225,7 @@
///
/// Requirements:
///
- /// `PrevEnv` must precede `this` in the environment ordering.
+ /// `PrevEnv` must be the immediate previous version of the environment.
/// `PrevEnv` and `this` must use the same `DataflowAnalysisContext`.
LatticeJoinEffect widen(const Environment &PrevEnv,
Environment::ValueModel &Model);
Index: clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -370,15 +370,18 @@
auto Effect = LatticeJoinEffect::Unchanged;
- // By the API, `PrevEnv` <= `*this`, meaning `join(PrevEnv, *this) =
- // *this`. That guarantees that these maps are subsets of the maps in
- // `PrevEnv`. So, we don't need change their current values to widen (in
- // contrast to `join`).
+ // By the API, `PrevEnv` is a previous version of the environment for the same
+ // block, so we have some guarantees about its shape. In particular, it will
+ // be the result of a join or widen operation on previous values for this
+ // block. For `DeclToLoc` and `ExprToLoc`, join guarantees that these maps are
+ // subsets of the maps in `PrevEnv`. So, as long as we maintain this property
+ // here, we don't need change their current values to widen.
//
- // FIXME: The above is violated for `MemberLocToStruct`, because `join` can
- // cause the map size to increase (when we add fresh data in places of
- // conflict). Once this issue with join is resolved, re-enable the assertion
- // below or replace with something that captures the desired invariant.
+ // FIXME: `MemberLocToStruct` does not share the above property, because
+ // `join` can cause the map size to increase (when we add fresh data in places
+ // of conflict). Once this issue with join is resolved, re-enable the
+ // assertion below or replace with something that captures the desired
+ // invariant.
assert(DeclToLoc.size() <= PrevEnv.DeclToLoc.size());
assert(ExprToLoc.size() <= PrevEnv.ExprToLoc.size());
// assert(MemberLocToStruct.size() <= PrevEnv.MemberLocToStruct.size());
Index: clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -137,10 +137,6 @@
///
/// Requirements:
///
- /// `Prev` must precede `Current` in the value ordering. Widening is *not*
- /// called when the current value is already equivalent to the previous
- /// value.
- ///
/// `Prev` and `Current` must model values of type `Type`.
///
/// `Prev` and `Current` must be assigned to the same storage location in
@@ -229,7 +225,7 @@
///
/// Requirements:
///
- /// `PrevEnv` must precede `this` in the environment ordering.
+ /// `PrevEnv` must be the immediate previous version of the environment.
/// `PrevEnv` and `this` must use the same `DataflowAnalysisContext`.
LatticeJoinEffect widen(const Environment &PrevEnv,
Environment::ValueModel &Model);
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
