[clang][dataflow] Add support for a Top value in boolean formulas.
authorYitzhak Mandelbaum <yitzhakm@google.com>
Thu, 6 Oct 2022 17:56:41 +0000 (17:56 +0000)
committerYitzhak Mandelbaum <yitzhakm@google.com>
Fri, 14 Oct 2022 17:41:53 +0000 (17:41 +0000)
commit39b9d4f188ca1f99515658334d57c2961db33289
tree8f6d89c30c476cc4173f1345dc4de350043795c3
parent28f7087c9163f66b07e17bd47a1bfb5d9448467d
[clang][dataflow] Add support for a Top value in boolean formulas.

Currently, our boolean formulas (`BoolValue`) don't form a lattice, since they
have no Top element. This patch adds such an element, thereby "completing" the
built-in model of bools to be a proper semi-lattice. It still has infinite
height, which is its own problem, but that can be solved separately, through
widening and the like.

Patch 1 for Issue #56931.

Differential Revision: https://reviews.llvm.org/D135397
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h
clang/include/clang/Analysis/FlowSensitive/Value.h
clang/lib/Analysis/FlowSensitive/DataflowEnvironment.cpp
clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
clang/lib/Analysis/FlowSensitive/Transfer.cpp
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
clang/unittests/Analysis/FlowSensitive/TestingSupport.h
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp