[clang] d2e4aaf - [clang][dataflow][NFC] Fix comments related to widening.

[Yitzhak Mandelbaum via cfe-commits]

Author: Yitzhak Mandelbaum
Date: 2022-12-19T21:01:27Z
New Revision: d2e4aaf6ac3bc7c72a81f050512afa17a9ceb54b

URL: https://github.com/llvm/llvm-project/commit/d2e4aaf6ac3bc7c72a81f050512afa17a9ceb54b
DIFF: https://github.com/llvm/llvm-project/commit/d2e4aaf6ac3bc7c72a81f050512afa17a9ceb54b.diff

LOG: [clang][dataflow][NFC] Fix comments related to widening.

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.

Differential Revision: https://reviews.llvm.org/D140308

Added: 
    

Modified: 
    clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
    clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
index ec2706c9fd1f0..c1653c2ab4ed2 100644
--- a/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
+++ b/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
@@ -137,10 +137,6 @@ class Environment {
     ///
     /// 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 @@ class Environment {
   ///
   /// 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);

diff  --git a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
index 597e39e271707..70fcb6be787aa 100644
--- a/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
+++ b/clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
@@ -370,15 +370,18 @@ LatticeJoinEffect Environment::widen(const Environment &PrevEnv,
 
   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());