[PATCH] D153366: [dataflow] Add dedicated representation of boolean formulas

[Sam McCall via Phabricator via cfe-commits]

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

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

- 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.

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


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D153366

Files:
  clang/include/clang/Analysis/FlowSensitive/Arena.h
  clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
  clang/include/clang/Analysis/FlowSensitive/Formula.h
  clang/include/clang/Analysis/FlowSensitive/Solver.h
  clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
  clang/lib/Analysis/FlowSensitive/Arena.cpp
  clang/lib/Analysis/FlowSensitive/CMakeLists.txt
  clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
  clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
  clang/lib/Analysis/FlowSensitive/Formula.cpp
  clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
  clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
  clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
  clang/unittests/Analysis/FlowSensitive/TestingSupport.h

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D153366.532961.patch
Type: text/x-patch
Size: 61380 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20230620/f8f33d12/attachment-0001.bin>