[all-commits] [llvm/llvm-project] d85c23: [dataflow] Make SAT solver deterministic

[Sam McCall via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: d85c233e4b05497a6d8c6e3f2a5fd63d9eeb200d
      https://github.com/llvm/llvm-project/commit/d85c233e4b05497a6d8c6e3f2a5fd63d9eeb200d
  Author: Sam McCall <sam.mccall at gmail.com>
  Date:   2023-06-26 (Mon, 26 Jun 2023)

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

  Log Message:
  -----------
  [dataflow] Make SAT solver deterministic

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.

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