[all-commits] [llvm/llvm-project] 2fd614: [dataflow] Add dedicated representation of boolean...
Sam McCall via All-commits
all-commits at lists.llvm.org
Tue Jul 4 03:20:04 PDT 2023
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
More information about the All-commits
mailing list