[PATCH] D77792: [analyzer] Extend constraint manager to be able to compare simple SymSymExprs

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

In D77792#1971921 <https://reviews.llvm.org/D77792#1971921>, @Szelethus wrote:

> You seem to have forgotten `-U9999` :^)


Nice catch!



================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:774
 
+Optional<ProgramStateRef> RangeConstraintManager::tryAssumeSymSymOp(
+    ProgramStateRef State, BinaryOperator::Opcode Op, SymbolRef LHSSym,
----------------
martong wrote:
> Is it possible to ever return with `None`? Other `assume` functions usually just return with `nullptr` on infeasible state as you do. What would be the meaning if `None` is returned, is that another kind of infeasibility?
The rest of the functions there is no `maybe` answer. There is always `yes` or `no`, returning the `State` or the `nullptr`.
In our case, we don't know in advance that we know a definitive answer.

Imagine the following:
When the analyzer sees the `a < b` comparison.
It queries whether it `canReasonAbout()`. In our case that would return `true` due to my change.
When tries to reason about the given `SymSymExpr` (`a < b`), we don't know if the corresponding value ranges of `a` and `b` are disjunct or not, we need to check that.
If we can prove that the ranges are disjunct (or just connected: `a: [a1,x]` and `b: [x,b2]`) then we know an answer. That can be `true` (`State`) or `false` (`nullptr`). Otherwise the result should be `UNKNOWN` (`llvm::None`).


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:797
+
+  switch (Op) {
+  case BO_LT:
----------------
martong wrote:
> Perhaps this hunk could be greatly simplified if `CompareResult` was actually `BinaryOperator::Opcode`.
> 
> Maybe (?):
> ```
> if (Res == Op)
>   return State;
> return InfeasibleState;
> ```
Honestly, I had exactly the same thoughts.

I think an `Opcode` is a different thing than a result of a comparison.
Here, we have a partial ordering among `RangeSet`s.
But you can convince me :)

But I agree, it looks clunky, looking forward to a better solution. Any idea?


================
Comment at: clang/test/Analysis/constraint-manager-sym-sym.c:70
+
+// [2,5] and [5,10]
+void test_range6(int l, int r) {
----------------
martong wrote:
> How is it different than `// [0,5] and [5,10]`?
It covers the same. I just wanted a full and clear showcase of the possible intervals.
I can be convinced to remove this testcase.


================
Comment at: clang/test/Analysis/constraint-manager-sym-sym.c:172
+}
+
----------------
martong wrote:
> I think we could benefit from tests for cases like this: 
> ```
> {[0,1],[5,6]} < {[9,9],[11,42],[44,44]}
> ```
Really good idea.

I added tests for these. But I'm not really sure what's going on there :D
I'm sure that these test cases are not testing what I meant to test.
//(The exploded graphs are showing that each subrange is assumed for a given value (`l` and `r`) on a given path)//

Any idea of how to express the proper value ranges?


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

https://reviews.llvm.org/D77792