[PATCH] D123586: [clang][dataflow] Weaken abstract comparison to enable loop termination.

[Yitzhak Mandelbaum via Phabricator via cfe-commits]

ymandel created this revision.
ymandel added reviewers: xazax.hun, sgatev.
Herald added subscribers: tschuett, steakhal, rnkovacs.
Herald added a project: All.
ymandel requested review of this revision.
Herald added a project: clang.

Currently, when the framework is used with an analysis that does not override
`compareEquivalent`, it does not terminate for most loops. The root cause is the
interaction of (the default implementation of) environment comparison
(`compareEquivalent`) and the means by which locations and values are
allocated. Specifically, the creation of certain values (including: reference
and pointer values; merged values) results in allocations of fresh locations in
the environment. As a result, analysis of even trivial loop bodies produces
different (if isomorphic) environments, on identical inputs. At the same time,
the default analysis relies on strict equality (versus some relaxed notion of
equivalence). Together, when the analysis compares these isomorphic, yet
unequal, environments, to determine whether the successors of the given block
need to be (re)processed, the result is invariably "yes", thus preventing loop
analysis from reaching a fixed point.

There are many possible solutions to this problem, including equivalence that is
less than strict pointer equality (like structural equivalence) and/or the
introduction of an explicit widening operation. However, these solutions will
require care to be implemented correctly. While a high priority, it seems more
urgent that we fix the current default implentation to allow
termination. Therefore, this patch proposes, essentially, to change the default
comparison to trivally equate any two values. As a result, we can say precisely
that the analysis will process the loop exactly twice -- once to establish an
initial result state and the second to produce an updated result which will
(always) compare equal to the previous. While clearly unsound -- we are not
reaching a fix point of the transfer function, in practice, this level of
analysis will find many practical issues where a single iteration of the loop
impacts abstract program state.

Note, however, that the change to the default `merge` operation does not affect
soundness, because the framework already produces a fresh (sound) abstraction of
the value when the two values are distinct. The previous setting was overly
conservative.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D123586

Files:
  clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
  clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
  clang/unittests/Analysis/FlowSensitive/TransferTest.cpp
  clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D123586.422177.patch
Type: text/x-patch
Size: 6244 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20220412/efad1685/attachment-0001.bin>