[clang][dataflow] Add an early-out to `flowConditionImplies()` / `flowConditionAllows()`. (#78172)

This saves having to assemble the set of constraints and run the SAT
solver in
the trivial case of

[clang][dataflow] Add an early-out to `flowConditionImplies()` / `flowConditionAllows()`. (#78172)

This saves having to assemble the set of constraints and run the SAT
solver in
the trivial case of `flowConditionImplies(true)` or
`flowConditionAllows(false)`.

This is an update / reland of my previous reverted
[#77453](https://github.com/llvm/llvm-project/pull/77453). That PR
contained a
logic bug -- the early-out for `flowConditionAllows()` was wrong because
my
intuition about the logic was wrong. (In particular, note that
`flowConditionImplies(F)` does not imply `flowConditionAllows(F)`, even
though
this may run counter to intuition.)

I've now done what I should have done on the first iteration and added
more
tests. These pass both with and without my early-outs.

This patch is a performance win on the benchmarks for the Crubit
nullability
checker, except for one slight regression on a relatively short
benchmark:

```
name old cpu/op new cpu/op delta
BM_PointerAnalysisCopyPointer 68.5µs ± 7% 67.6µs ± 4% ~ (p=0.159 n=18+19)
BM_PointerAnalysisIntLoop 173µs ± 3% 162µs ± 4% -6.40% (p=0.000 n=19+20)
BM_PointerAnalysisPointerLoop 307µs ± 2% 312µs ± 4% +1.56% (p=0.013 n=18+20)
BM_PointerAnalysisBranch 199µs ± 4% 181µs ± 4% -8.81% (p=0.000 n=20+20)
BM_PointerAnalysisLoopAndBranch 503µs ± 3% 508µs ± 2% ~ (p=0.081 n=18+19)
BM_PointerAnalysisTwoLoops 304µs ± 4% 286µs ± 2% -6.04% (p=0.000 n=19+20)
BM_PointerAnalysisJoinFilePath 4.78ms ± 3% 4.54ms ± 4% -4.97% (p=0.000 n=20+20)
BM_PointerAnalysisCallInLoop 3.05ms ± 3% 2.90ms ± 4% -5.05% (p=0.000 n=19+20)
```

When running clang-tidy on real-world code, the results are less clear.
In
three runs, averaged, on an arbitrarily chosen input file, I get 11.60 s
of user
time without this patch and 11.40 s with it, though with considerable
measurement noise (I'm seeing up to 0.2 s of variation between runs).

Still, this is a very simple change, and it is a clear win in
benchmarks, so I
think it is worth making.

show more ...

[clang][dataflow] Remove `DataflowAnalysisContext::flowConditionIsTautology()`. (#69601)

It's only used in its own unit tests.

[dataflow] Add global invariant condition to DataflowAnalysisContext (#65949)

This records facts that are not sensitive to the current flow condition,
and should apply to all environments.

The m

[dataflow] Add global invariant condition to DataflowAnalysisContext (#65949)

This records facts that are not sensitive to the current flow condition,
and should apply to all environments.

The motivating case is recording information about where a Value
originated, such as nullability:
- we may see the same Value for multiple expressions (e.g. reads of the
same field) in multiple environments (multiple blocks or iterations)
- we want to record information only when we first see the Value
(e.g. Nullability annotations on fields only add information if we
don't know where the value came from)
- this information should be expressible as a SAT condition
- we must add this SAT condition to every environment where the
Value may appear

We solve this by recording the information in the global condition.
This doesn't seem particularly elegant, but solves the problem and is
a fairly small and natural extension of the Environment.

Alternatives considered:
- store the constraint directly as a property on the Value.
But it's more composable for such properties to always be variables
(AtomicBoolValue), and constrain them with SAT conditions.
- add a hook whenever values are created, giving the analysis the
chance to populate them.
However the framework relies on/provides the ability to construct
values in arbitrary places without providing the context such a hook
would need, this would be a very invasive change.

show more ...

Reland "[dataflow] Add dedicated representation of boolean formulas"

This reverts commit 7a72ce98224be76d9328e65eee472381f7c8e7fe.

Test problems were due to unspecified order of function arg evalua

Reland "[dataflow] Add dedicated representation of boolean formulas"

This reverts commit 7a72ce98224be76d9328e65eee472381f7c8e7fe.

Test problems were due to unspecified order of function arg evaluation.

Reland "[dataflow] Replace most BoolValue subclasses with references to Formula (and AtomicBoolValue => Atom and BoolValue => Formula where appropriate)"

This properly frees the Value hierarchy from managing boolean formulas.

We still distinguish AtomicBoolValue; this type is used in client code.
However we expect to convert such uses to BoolValue (where the
distinction is not needed) or Atom (where atomic identity is intended),
and then fold AtomicBoolValue into FormulaBoolValue.

We also distinguish TopBoolValue; this has distinct rules for
widen/join/equivalence, and top-ness is not represented in Formula.
It'd be nice to find a cleaner representation (e.g. the absence of a
formula), but no immediate plans.

For now, BoolValues with the same Formula are deduplicated. This doesn't
seem desirable, as Values are mutable by their creators (properties).
We can probably drop this for FormulaBoolValue immediately (not in this
patch, to isolate changes). For AtomicBoolValue we first need to update
clients to stop using value pointers for atom identity.

The data structures around flow conditions are updated:
- flow condition tokens are Atom, rather than AtomicBoolValue*
- conditions are Formula, rather than BoolValue
Most APIs were changed directly, some with many clients had a
new version added and the existing one deprecated.

The factories for BoolValues in Environment keep their existing
signatures for now (e.g. makeOr(BoolValue, BoolValue) => BoolValue)
and are not deprecated. These have very many clients and finding the
most ergonomic API & migration path still needs some thought.

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

show more ...

Revert "Reland "[dataflow] Add dedicated representation of boolean formulas" and followups

These changes are OK, but they break downstream stuff that needs more time to adapt :-(

This reverts commi

Revert "Reland "[dataflow] Add dedicated representation of boolean formulas" and followups

These changes are OK, but they break downstream stuff that needs more time to adapt :-(

This reverts commit 71579569f4399d3cf6bc618dcd449b5388d749cc.
This reverts commit 5e4ad816bf100b0325ed45ab1cfea18deb3ab3d1.
This reverts commit 1c3ac8dfa16c42a631968aadd0396cfe7f7778e0.

show more ...

[dataflow] Replace most BoolValue subclasses with references to Formula (and AtomicBoolValue => Atom and BoolValue => Formula where appropriate)

This properly frees the Value hierarchy from managing

[dataflow] Replace most BoolValue subclasses with references to Formula (and AtomicBoolValue => Atom and BoolValue => Formula where appropriate)

This properly frees the Value hierarchy from managing boolean formulas.

We still distinguish AtomicBoolValue; this type is used in client code.
However we expect to convert such uses to BoolValue (where the
distinction is not needed) or Atom (where atomic identity is intended),
and then fold AtomicBoolValue into FormulaBoolValue.

We also distinguish TopBoolValue; this has distinct rules for
widen/join/equivalence, and top-ness is not represented in Formula.
It'd be nice to find a cleaner representation (e.g. the absence of a
formula), but no immediate plans.

For now, BoolValues with the same Formula are deduplicated. This doesn't
seem desirable, as Values are mutable by their creators (properties).
We can probably drop this for FormulaBoolValue immediately (not in this
patch, to isolate changes). For AtomicBoolValue we first need to update
clients to stop using value pointers for atom identity.

The data structures around flow conditions are updated:
- flow condition tokens are Atom, rather than AtomicBoolValue*
- conditions are Formula, rather than BoolValue
Most APIs were changed directly, some with many clients had a
new version added and the existing one deprecated.

The factories for BoolValues in Environment keep their existing
signatures for now (e.g. makeOr(BoolValue, BoolValue) => BoolValue)
and are not deprecated. These have very many clients and finding the
most ergonomic API & migration path still needs some thought.

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

show more ...

[dataflow] Extract arena for Value/StorageLocation out of DataflowAnalysisContext

DataflowAnalysisContext has a few too many responsibilities, this narrows them.

It also allows the Arena to be shar

[dataflow] Extract arena for Value/StorageLocation out of DataflowAnalysisContext

DataflowAnalysisContext has a few too many responsibilities, this narrows them.

It also allows the Arena to be shared with analysis steps, which need to create
Values, without exposing the whole DACtx API (flow conditions etc).
This means Environment no longer needs to proxy all these methods.
(For now it still does, because there are many callsites to update, and maybe
if we separate bool formulas from values we can avoid churning them twice)

In future, if we untangle the concepts of Values from boolean formulas/atoms,
Arena would also be responsible for creating formulas and managing atom IDs.

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

show more ...

[clang][dataflow] Fix -Wdeprecated-declarations after D147302 (NFC)

Replace:
1. createAtomicBoolValue() --> create<AtomicBoolValue>()
2. createTopBoolValue() --> create<TopBoolValue>()

/Users/

[clang][dataflow] Fix -Wdeprecated-declarations after D147302 (NFC)

Replace:
1. createAtomicBoolValue() --> create<AtomicBoolValue>()
2. createTopBoolValue() --> create<TopBoolValue>()

/Users/jiefu/llvm-project/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h:386:19: error: 'createAtomicBoolValue' is deprecated: use create<AtomicBoolValue> instead [-Werror,-Wdeprecated-declarations]
return DACtx->createAtomicBoolValue();
^~~~~~~~~~~~~~~~~~~~~
create<AtomicBoolValue>
/Users/jiefu/llvm-project/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:215:3: note: 'createAtomicBoolValue' has been explicitly marked deprecated here
LLVM_DEPRECATED("use create<AtomicBoolValue> instead",
^
/Users/jiefu/llvm-project/llvm/include/llvm/Support/Compiler.h:143:50: note: expanded from macro 'LLVM_DEPRECATED'
^
In file included from /Users/jiefu/llvm-project/clang/lib/Analysis/FlowSensitive/Transfer.cpp:14:
In file included from /Users/jiefu/llvm-project/clang/include/clang/Analysis/FlowSensitive/Transfer.h:19:
/Users/jiefu/llvm-project/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h:391:19: error: 'createTopBoolValue' is deprecated: use create<TopBoolValue> instead [-Werror,-Wdeprecated-declarations]
return DACtx->createTopBoolValue();
^~~~~~~~~~~~~~~~~~
create<TopBoolValue>
/Users/jiefu/llvm-project/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h:227:3: note: 'createTopBoolValue' has been explicitly marked deprecated here
LLVM_DEPRECATED("use create<TopBoolValue> instead", "create<TopBoolValue>")
^
/Users/jiefu/llvm-project/llvm/include/llvm/Support/Compiler.h:143:50: note: expanded from macro 'LLVM_DEPRECATED'
^
2 errors generated.

show more ...

[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

[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

show more ...

[clang][dataflow] Add explicit "AST" nodes for implications and iff

Previously we used to desugar implications and biconditionals into
equivalent CNF/DNF as soon as possible. However, this desugarin

[clang][dataflow] Add explicit "AST" nodes for implications and iff

Previously we used to desugar implications and biconditionals into
equivalent CNF/DNF as soon as possible. However, this desugaring makes
debug output (Environment::dump()) less readable than it could be.
Therefore, it makes sense to keep the sugared representation of a
boolean formula, and desugar it in the solver.

Reviewed By: sgatev, xazax.hun, wyt

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

show more ...

[clang][dataflow] Do not allow substitution of true/false boolean literals in `buildAndSubstituteFlowCondition`

Reviewed By: gribozavr2, xazax.hun

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

[clang][dataflow] Do not allow substitution of true/false boolean literals in `buildAndSubstituteFlowCondition`

Reviewed By: gribozavr2, xazax.hun

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

show more ...

[clang][dataflow] Implement functionality for flow condition variable substitution.

This patch introduces `buildAndSubstituteFlowCondition` - given a flow condition token, this function returns the

[clang][dataflow] Implement functionality for flow condition variable substitution.

This patch introduces `buildAndSubstituteFlowCondition` - given a flow condition token, this function returns the expression of constraints defining the flow condition, with values substituted where specified.

As an example:
Say we have tokens `FC1`, `FC2`, `FC3`:
```
FlowConditionConstraints: {
FC1: C1,
FC2: C2,
FC3: (FC1 v FC2) ^ C3,
}
```
`buildAndSubstituteFlowCondition(FC3, /*Substitutions:*/{{C1 -> C1'}})`
returns a value corresponding to `(C1' v C2) ^ C3`.

Note:
This function returns the flow condition expressed directly as its constraints, which differs to how we currently represent the flow condition as a token bound to a set of constraints and dependencies. Making the representation consistent may be an option to consider in the future.

Depends On D128357

Reviewed By: gribozavr2, xazax.hun

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

show more ...

[clang][dataflow] Implement functionality to compare if two boolean values are equivalent.

`equivalentBoolValues` compares equivalence between two booleans. The current implementation does not consi

[clang][dataflow] Implement functionality to compare if two boolean values are equivalent.

`equivalentBoolValues` compares equivalence between two booleans. The current implementation does not consider constraints imposed by flow conditions on the booleans and its subvalues.

Depends On D128520

Reviewed By: gribozavr2, xazax.hun

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

show more ...

[clang][dataflow] Move logic for creating implication and iff expressions into `DataflowAnalysisContext` from `DataflowEnvironment`.

To keep functionality of creating boolean expressions in a consis

[clang][dataflow] Move logic for creating implication and iff expressions into `DataflowAnalysisContext` from `DataflowEnvironment`.

To keep functionality of creating boolean expressions in a consistent location.

Depends On D128357

Reviewed By: gribozavr2, sgatev, xazax.hun

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

show more ...

[clang][dataflow] Add flowConditionIsTautology function

Provide a way for users to check if a flow condition is
unconditionally true.

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

[clang][dataflow] Optimize flow condition representation

Enable efficient implementation of context-aware joining of distinct
boolean values. It can be used to join distinct boolean values while
pre

[clang][dataflow] Optimize flow condition representation

Enable efficient implementation of context-aware joining of distinct
boolean values. It can be used to join distinct boolean values while
preserving flow condition information.

Flow conditions are represented as Token <=> Clause iff formulas. To
perform context-aware joining, one can simply add the tokens of flow
conditions to the formula when joining distinct boolean values, e.g:
`makeOr(makeAnd(FC1, Val1), makeAnd(FC2, Val2))`. This significantly
simplifies the implementation of `Environment::join`.

This patch removes the `DataflowAnalysisContext::getSolver` method.
The `DataflowAnalysisContext::flowConditionImplies` method should be
used instead.

Reviewed-by: ymandel, xazax.hun

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

show more ...

[clang][dataflow] Add flow condition constraints to Environment

This is part of the implementation of the dataflow analysis framework.
See "[RFC] A dataflow analysis framework for Clang AST" on cfe-

[clang][dataflow] Add flow condition constraints to Environment

This is part of the implementation of the dataflow analysis framework.
See "[RFC] A dataflow analysis framework for Clang AST" on cfe-dev.

Reviewed-by: ymandel, xazax.hun

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

show more ...