[all-commits] [llvm/llvm-project] 7d935d: [dataflow] improve determinism of generated SAT sy...

[Sam McCall via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 7d935d083659c9ddaf3389c1747fc8c59f07e3fc
      https://github.com/llvm/llvm-project/commit/7d935d083659c9ddaf3389c1747fc8c59f07e3fc
  Author: Sam McCall <sam.mccall at gmail.com>
  Date:   2023-07-12 (Wed, 12 Jul 2023)

  Changed paths:
    M clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
    M clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
    M clang/lib/Analysis/FlowSensitive/TypeErasedDataflowAnalysis.cpp
    M clang/unittests/Analysis/FlowSensitive/CMakeLists.txt
    A clang/unittests/Analysis/FlowSensitive/DeterminismTest.cpp

  Log Message:
  -----------
  [dataflow] improve determinism of generated SAT system

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.

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