[PATCH] D153584: [dataflow] Make SAT solver deterministic

[Sam McCall via Phabricator via cfe-commits]

sammccall created this revision.
sammccall added reviewers: ymandel, xazax.hun.
Herald added subscribers: 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.

The SAT solver imported its constraints by iterating over an unordered DenseSet.
The path taken, and ultimately the runtime, the specific solution found, and
whether it would time out or complete could depend on the iteration order.

Instead, have the caller specify an ordered collection of constraints.
If this is built in a deterministic way, the system can have deterministic
behavior.
(The main alternative is to sort the constraints by value, but this option
is simpler today).

A lot of nondeterminism still appears to be remain in the framework, so today
the solver's inputs themselves are not deterministic yet.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D153584

Files:
  clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
  clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
  clang/include/clang/Analysis/FlowSensitive/Solver.h
  clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
  clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
  clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
  clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
  clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
  clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D153584.533740.patch
Type: text/x-patch
Size: 13646 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20230622/b7d7014c/attachment.bin>