[PATCH] D131646: [clang][dataflow] Restructure loops to call widen on back edges

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added inline comments.


================
Comment at: clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp:228-234
+  // If we are at the start of a loop, we will have two precessors, but we don't
+  // want to join these two predecessors. Instead, we want to take the back edge
+  // block (i.e. the result of the previous iteration) and use that directly as
+  // the input block.
+  //
+  // For the first iteration of loop, the "zeroth" iteration state is set up by
+  // `prepareBackEdges`.
----------------
xazax.hun wrote:
> li.zhe.hua wrote:
> > xazax.hun wrote:
> > > Could you elaborate on this? Let's consider this loop:
> > > 
> > > ```
> > >  Pred
> > >    |
> > >    v
> > >  LoopHeader <---BackEdge
> > > ```
> > > 
> > > Do we ignore the state coming from `Pred` on purpose? Is that sound?
> > > 
> > > I would expect the analysis to always compute `join(PredState, BackEdgeState)`, and I would expect the widening to happen between the previous iteration of `BackEdgeState` and the current iteration of `BackEdgeState`. So, I wonder if we already invoke the widening operator along back edges, wouldn't the regular logic work just fine? Do I miss something?
> > > 
> > > Do we ignore the state coming from `Pred` on purpose? Is that sound?
> > 
> > We don't, and this is what the comment
> > 
> > ```
> >   // For the first iteration of loop, the "zeroth" iteration state is set up by
> >   // `prepareBackEdges`.
> > ```
> > failed to explain. After transferring `PredState`, we copy `PredState` into `BackEdgeState`, which is done in `prepareBackEdges`.
> > 
> > > I would expect the analysis to always compute `join(PredState, BackEdgeState)`
> > 
> > I'm not sure I see that we should always join `PredState` and `BackEdgeState`. Execution doesn't go from `Pred` into the Nth iteration of the loop, it only goes from `Pred` into the first iteration of the loop, e.g. the predecessor for the 4th iteration of the loop is only the back-edge from the 3rd iteration of the loop, not `Pred`.
> > 
> > Let me know if this makes sense.
> > I'm not sure I see that we should always join `PredState` and `BackEdgeState`. Execution doesn't go from `Pred` into the Nth iteration of the loop, it only goes from `Pred` into the first iteration of the loop, e.g. the predecessor for the 4th iteration of the loop is only the back-edge from the 3rd iteration of the loop, not `Pred`.
> > 
> > Let me know if this makes sense.
> 
> The analysis state of the dataflow analysis supposed to overestimate all of the paths. Consider the following loop and imagine we want to calculate intervals for integer variables:
> 
> ```
> int i = 0;
> while (...) {
>   [[program point A]];
>   ++i;
> }
> ```
> 
> During the analysis of this loop, the value `i ==0` flows to `[[program point A]]`. This is the motivation to join the state from the back edge and from PredState. As far as I understand, you want to achieve this by copying PredState to the BackEdgeState before the first iteration. But this also means that we will use the widening operator to combine PredState with the state after N iterations instead of the regular join operation. I am not entirely sure whether these two approaches always produce the same results. 
> 
> 
A contrived example (just came up with this in a couple minutes so feel free to double check if it is OK):
Consider:
```
int i = 0;
while (...) {
  if (i == 0)
    i = -2;
  ++i;
}
```

Some states:
```
PredState = i : [0, 0]
BackEdgeState (after first iteration) = i : [-1, -1]
```

And the results of join vs widen:
```
PredState.join(BackEdgeState) = i : [-1, 0]
PredState.widen(BackEdge) = i : [-inf, 0]
```

The extra widening with the PredState can result in extra imprecision. 


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D131646/new/

https://reviews.llvm.org/D131646