[PATCH] D154948: [dataflow] improve determinism of generated SAT system

[Sam McCall via Phabricator via cfe-commits]

sammccall created this revision.
sammccall added reviewers: ymandel, xazax.hun.
Herald added subscribers: ChuanqiXu, martong, mgrang.
Herald added a reviewer: NoQ.
Herald added a project: All.
sammccall requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

Fixes two places where we relied on map iteration order when processing
values, which leaked nondeterminism into the generated SAT formulas.
Adds a couple of tests that directly assert that the SAT system is
equivalent on each run.

It's desirable that the formulas are deterministic based on the input:

- our SAT solver is naive and perfermance is sensitive to even simple semantics-preserving transformations like A|B to B|A. (e.g. it's likely to choose a different variable to split on). Timeout failures are bad, but *flaky* ones are terrible to debug.
- similarly when debugging, it's important to have a consistent understanding of what e.g. "V23" means across runs.

---

Both changes in this patch were isolated from a nullability analysis of
real-world code which was extremely slow, spending ages in the SAT
solver at "random" points that varied on each run.
I've included a reduced version of the code as a regression test.

One of the changes shows up directly as flow-condition nondeterminism
with a no-op analysis, the other relied on bits of the nullability
analysis but I found a synthetic example to show the problem.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D154948

Files:
  clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
  clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
  clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
  clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
  clang/unittests/Analysis/FlowSensitive/DeterminismTest.cpp

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D154948.539012.patch
Type: text/x-patch
Size: 8305 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20230711/76fa1cdb/attachment.bin>