This is an archive of the discontinued LLVM Phabricator instance.

[dataflow] improve determinism of generated SAT system
ClosedPublic

Authored by sammccall on Jul 11 2023, 4:02 AM.

Details

Summary

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.

Diff Detail

Event Timeline

sammccall created this revision.Jul 11 2023, 4:02 AM
Herald added a project: Restricted Project. · View Herald Transcript
sammccall requested review of this revision.Jul 11 2023, 4:02 AM
Herald added a project: Restricted Project. · View Herald TranscriptJul 11 2023, 4:02 AM
Herald added a subscriber: cfe-commits. · View Herald Transcript
gribozavr2 accepted this revision.Jul 11 2023, 4:39 AM
gribozavr2 added a subscriber: gribozavr2.
gribozavr2 added inline comments.
clang/unittests/Analysis/FlowSensitive/DeterminismTest.cpp
63
This revision is now accepted and ready to land.Jul 11 2023, 4:39 AM
ymandel accepted this revision.Jul 11 2023, 4:48 AM

Thank you, Sam!

xazax.hun accepted this revision.Jul 11 2023, 7:23 AM
This revision was landed with ongoing or failed builds.Jul 11 2023, 11:09 PM
This revision was automatically updated to reflect the committed changes.