Commit Graph

18 Commits

Author SHA1 Message Date
Yitzhak Mandelbaum 692e03039d [clang][dataflow] Add cache of `ControlFlowContext`s for function decls.
This patch modifies context-sensitive analysis of functions to use a cache,
rather than recreate the `ControlFlowContext` from a function decl on each
encounter. However, this is just step 1 (of N) in adding support for a
configurable map of "modeled" function decls (see issue #56879). The map will go
from the actual function decl to the `ControlFlowContext` used to model it. Only
functions pre-configured in the map will be modeled in a context-sensitive way.

We start with a cache because it introduces the desired map, while retaining the
current behavior. Here, functions are mapped to their actual implementations
(when available).

Differential Revision: https://reviews.llvm.org/D131039
2022-08-03 15:17:49 +00:00
Stanislav Gatev 817dd5e3fd [clang][dataflow] Rename member to make it clear that it isn't stable
Rename `DataflowAnalysisContext::getStableStorageLocation(QualType)`
to `createStorageLocation`, to make it clear that it doesn't return
a stable storage location.

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

Reviewed-by: ymandel, xazax.hun, gribozavr2
2022-08-03 06:25:02 +00:00
Dmitri Gribenko b5e3dac33d [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
2022-07-26 14:19:22 +02:00
Dmitri Gribenko c0c9d717df [clang][dataflow] Rename iterators from IT to It
The latter way to abbreviate is a lot more common in the LLVM codebase.

Reviewed By: sgatev, xazax.hun

Differential Revision: https://reviews.llvm.org/D130423
2022-07-25 20:28:47 +02:00
Dmitri Gribenko b5414b566a [clang][dataflow] Add DataflowEnvironment::dump()
Start by dumping the flow condition.

Reviewed By: ymandel

Differential Revision: https://reviews.llvm.org/D130398
2022-07-23 01:31:53 +02:00
Eric Li f10d271ae2 [clang][dataflow] Handle null pointers of type std::nullptr_t
Treat `std::nullptr_t` as a regular scalar type to avoid tripping
assertions when analyzing code that uses `std::nullptr_t`.

Differential Revision: https://reviews.llvm.org/D129097
2022-07-05 13:49:26 +00:00
Wei Yi Tee fa34210fa6 [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
2022-06-27 21:04:52 +02:00
Wei Yi Tee b611376e7e [clang][dataflow] Singleton pointer values for null pointers.
When a `nullptr` is assigned to a pointer variable, it is wrapped in a `ImplicitCastExpr` with cast kind `CK_NullTo(Member)Pointer`. This patch assigns singleton pointer values representing null to these expressions.

For each pointee type, a singleton null `PointerValue` is created and stored in the `NullPointerVals` map of the `DataflowAnalysisContext` class. The pointee type is retrieved from the implicit cast expression, and used to initialise the `PointeeLoc` field of the `PointerValue`. The `PointeeLoc` created is not mapped to any `Value`, reflecting the absence of value indicated by null pointers.

Reviewed By: gribozavr2, sgatev, xazax.hun

Differential Revision: https://reviews.llvm.org/D128056
2022-06-27 14:17:34 +02:00
Wei Yi Tee bdfe556dd8 [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
2022-06-27 11:37:46 +02:00
Wei Yi Tee 12c7352fa4 [clang][dataflow] Move logic for `createStorageLocation` from `DataflowEnvironment` to `DataflowAnalysisContext`.
`createStorageLocation` in `DataflowEnvironment` is now a trivial wrapper around the logic in `DataflowAnalysisContext`.
Additionally, `getObjectFields` and `getFieldsFromClassHierarchy` (required for the implementation of `createStorageLocation`) are also moved to `DataflowAnalysisContext`.

Reviewed By: gribozavr2, sgatev

Differential Revision: https://reviews.llvm.org/D128359
2022-06-27 11:16:51 +02:00
Wei Yi Tee 0f65a3e610 [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
2022-06-25 00:10:35 +02:00
Wei Yi Tee 42a7ddb428 [clang][dataflow] Refactor function that queries the solver for satisfiability checking.
Given a set of `Constraints`, `querySolver` adds common background information across queries (`TrueVal` is always true and `FalseVal` is always false) and passes the query to the solver.

`checkUnsatisfiable` is a simple wrapper around `querySolver` for checking that the solver returns an unsatisfiable result.

Depends On D128519

Reviewed By: gribozavr2, xazax.hun

Differential Revision: https://reviews.llvm.org/D128520
2022-06-25 00:05:43 +02:00
Wei Yi Tee 00e9d53453 [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
2022-06-24 23:16:44 +02:00
Wei Yi Tee fb88ea6260 [clang][dataflow] Store flow condition constraints in a single `FlowConditionConstraints` map.
A flow condition is represented with an atomic boolean token, and it is bound to a set of constraints: `(FC <=> C1 ^ C2 ^ ...)`. \
This was internally represented as `(FC v !C1 v !C2 v ...) ^ (C1 v !FC) ^ (C2 v !FC) ^ ...` and tracked by 2 maps:
- `FlowConditionFirstConjunct` stores the first conjunct `(FC v !C1 v !C2 v ...)`
- `FlowConditionRemainingConjuncts` stores the remaining conjuncts `(C1 v !FC) ^ (C2 v !FC) ^ ...`

This patch simplifies the tracking of the constraints by using a single `FlowConditionConstraints` map which stores `(C1 ^ C2 ^ ...)`, eliminating the use of two maps.

Reviewed By: gribozavr2, sgatev, xazax.hun

Differential Revision: https://reviews.llvm.org/D128357
2022-06-24 21:52:16 +02:00
Eric Li 45643cfcc1 [clang][dataflow] Centralize expression skipping logic
A follow-up to 62b2a47 to centralize the logic that skips expressions
that the CFG does not emit. This allows client code to avoid
sprinkling this logic everywhere.

Add redirects in the transfer function to similarly skip such
expressions by forwarding the visit to the sub-expression.

Differential Revision: https://reviews.llvm.org/D124965
2022-05-05 20:28:11 +00:00
Eric Li 58abe36ae7 [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
2022-05-05 03:57:43 +00:00
Stanislav Gatev 955a05a278 [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
2022-05-01 16:25:29 +00:00
Stanislav Gatev ae60884dfe [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
2022-03-02 08:57:27 +00:00