[PATCH] D156658: [clang][dataflow] When checking `ExprToLoc` convergence, only consider children of block terminator.

Wed Aug 2 08:46:30 PDT 2023

xazax.hun added a comment.

In D156658#4552965 <https://reviews.llvm.org/D156658#4552965>, @mboehme wrote:

> I've investigated this in more detail. Unfortunately, it turns out that it's not quite as simple as just implementing widening on `ExprToLoc`.
>
> One of the reasons for this is that we only apply widening at loop heads, but the expressions that are "blocking" convergence may be contained in a block that is not a loop head.

I am probably missing something, but I why does it matter where are we doing the widening? It is possible that we might need to redesign how parts of the program state is represented, but I do not immediately see any fundamental roadblocks.

> I think the real solution to this would be to introduce widening for `PointerValue`s.

Fully agreed.

> Essentially, what we want is a "top" `PointerValue` that does not have an associated `StorageLocation`. However, we don't want to eliminate the `PointerValue` entirely; we still want to be able to attach properties to it, so that, for example, an analysis can record that the `PointerValue` is non-null, even though we don't know what its exact location is.

Another way to interpret "top": it points to a "summary" `StorageLocation` that can be any other `StorageLocation`, we just do not know which one. This interpretation/formulation has some advantages:

- We have a `StorageLocation` to use when we dereference these top pointers.
- It is compatible with the alias sets representation.
- It is compatible with some other representations where we have other "summary" locations, like "UnkownStackLocation" or "UnkownHeapLocation".

These summary memory locations are sort of the union of all the potential memory locations they could represent. I think in general it might be useful to embrace this idea, e.g., when we model arrays, we can have a single element region representing all the knowledge we know to be true for all elements of the array.

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D156658