[all-commits] [llvm/llvm-project] 2fd614: [dataflow] Add dedicated representation of boolean...

[Sam McCall via All-commits]

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

  Changed paths:
    M clang/include/clang/Analysis/FlowSensitive/Arena.h
    M clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
    A clang/include/clang/Analysis/FlowSensitive/Formula.h
    M clang/include/clang/Analysis/FlowSensitive/Solver.h
    M clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
    M clang/lib/Analysis/FlowSensitive/Arena.cpp
    M clang/lib/Analysis/FlowSensitive/CMakeLists.txt
    M clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
    M clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
    A clang/lib/Analysis/FlowSensitive/Formula.cpp
    M clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
    M clang/unittests/Analysis/FlowSensitive/ArenaTest.cpp
    M clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
    M clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
    M clang/unittests/Analysis/FlowSensitive/TestingSupport.h

  Log Message:
  -----------
  [dataflow] Add dedicated representation of boolean formulas

This is the first step in untangling the two current jobs of BoolValue.

=== Desired end-state: ===

- BoolValue will model C++ booleans e.g. held in StorageLocations.
  this includes describing uncertainty (e.g. "top" is a Value concern)
- Formula describes analysis-level assertions in terms of SAT atoms.

These can still be linked together: a BoolValue may have a corresponding
SAT atom which is constrained by formulas.

=== Done in this patch: ===

BoolValue is left intact, Formula is just the input type to the
SAT solver, and we build formulas as needed to invoke the solver.

=== Incidental changes to debug string printing: ===

- variables renamed from B0 etc to V0 etc
  B0 collides with the names of basic blocks, which is confusing when
  debugging flow conditions.
- debug printing of formulas (Formula and Atom) uses operator<<
  rather than debugString(), so works with gtest.
  Therefore moved out of DebugSupport.h
- Did the same to Solver::Result, and some helper changes to SolverTest,
  so that we get useful messages on unit test failures
- formulas are now printed as infix expressions on one line, rather than
  wrapped/indented S-exprs. My experience is that this is easier to scan
  FCs for small examples, and large ones are unreadable either way.
- most of the several debugString() functions for constraints/results
  are unused, so removed them rather than updating tests.
  Inlined the one that was actually used into its callsite.

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