[PATCH] D103317: [Analyzer][engine][solver] Simplify complex constraints

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

Returning to the discussion raised in D102696 <https://reviews.llvm.org/D102696>, I'd like to share my vision.
I think we can use much easier approach to use valid constraints at any point of time.
The main idea is lazy-reasoning of the ranges.
This approach:

- **doesn't** need to use **canonicalization**;
- **doesn't** need to **update all** the constraints on **each** `setConstraint` call (using brute-force or any other structure traversals);
- **add** an additional bindings for **every** simple operand on **each** //assignment// or //initialization//.
- **remove** an invalid bindings for **every** simple operand on **each** //assignment// or //initialization//.
- **recursively** get the **range** when and only when needed (lazy-reasoning).

Example:

  a = b + 1;
  c = a - 5;
  if (b != 42) return 0;
  if(c == 38) return 1;
  return 0;

`a = b + 1;`

1. LHS `a` lookup. LHS not found.
2. Add binding `$a = $b + 1`
3. Traverse through RHS `b + 1`.
4. `b` lookup. `b` not found.
5. Built a new expression `a - 1` for `b`.
6. Add binding for `b`: `$b = $a - 1`
7. `1` is a constant. Skip.

`c = a - 1;`

1. LHS `c` lookup. LHS not found.
2. Add binding `$c = $a - 1`
3. Traverse through RHS `a - 1`.
4. `a` lookup. `a` found.
5. If LHS not found and `a` found, then skip.
6. `1` is a constant. Skip.

`if (b != 42) return;`

1. Get the range of `$b`. Direct range not found. Add `$b` to the list of visited symbols.
2. Substitute bindings. From `$b != 42` to `$a - 1 == 42`.
3. Traverse through `$a - 1`.
4. Get the range of `$a`. Direct range not found. Add `$a` to the list of visited symbols.
5. `1` is a constant. Skip.
6. Substitute bindings. From `$a - 1 == 42` to `$b + 1 - 1 == 42`.
7. Traverse through `$b + 1 - 1`.
8. `$b` is in the list of already visited symbols. No way to find a range.
9. Create a range from the type [MIN, MAX].
10. Perform comparison and produce a constraint for `b` [42, 42].

`if(c == 38) return;`

1. Get the range of `$c`. Direct range not found. Add `$c` to the list of visited symbols.
2. Substitute bindings. From `$c == 38` to `$a - 1 == 38`.
3. Traverse through `$a - 1`.
4. Get the range of `$a`. Direct range not found. Add `$a` to the list of visited symbols.
5. `1` is a constant. Skip.
6. Substitute bindings. From `$a - 1 == 38` to `$b + 1 - 5 == 38`.
7. Traverse through `$b + 1 - 5`.
8. Get the range of `$b`. Direct range **found** [42, 42].
9. `1` is a constant. Skip.
10. `5` is a constant. Skip.
11. Calculate a new range for `$c` [38, 38].
12. Condition is //true//.

`return 1`

P.S. I've just started thinking of the way to solve this problem. For now it's just a sketch of where I'm going.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D103317/new/

https://reviews.llvm.org/D103317