[PATCH] D88019: [analyzer][solver] Fix issue with symbol non-equality tracking

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

steakhal added a comment.

In D88019#2303078 <https://reviews.llvm.org/D88019#2303078>, @martong wrote:

> I like the second approach, i.e. to have a debug checker. But I don't see, how would this checker validate all constraints at the moment when they are added to the State.

`ProgramStateRef evalAssume(ProgramStateRef State, SVal Cond, bool Assumption)` checker callback is called **after** any assume call.
So, we would have a `State` which has all? the constraints stored in the appropriate GDM. I'm not sure if we should aggregate all the constraints till this node - like we do for refutation. I think, in this case, we should just make sure that the **current** state does not have any contradiction.

---

Here is my proof-of-concept:

I've  dumped the state and args of evalAssume for the repro example, pretending that we don't reach a code-path on the infeasable path to crash:

  void avoidInfeasibleConstraintforGT(int a, int b) {
    int c = b - a;
    if (c <= 0)
      return;
    if (a != b) {
      clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
      return;
    }
    clang_analyzer_warnIfReached(); // eh, we will reach this..., #1
    // These are commented out, to pretend that we don't find out that we are on an infeasable path...
    // a == b
    // if (c < 0)
    //   ;
  }

We reach the `#1` line, but more importantly, we will have the following state dumps:

  evalAssume: assuming Cond: (reg_$1<int a>) != (reg_$0<int b>) to be true in state:
  "program_state": {
    "constraints": [
      { "symbol": "(reg_$0<int b>) - (reg_$1<int a>)", "range": "{ [1, 2147483647] }" },
      { "symbol": "(reg_$1<int a>) != (reg_$0<int b>)", "range": "{ [-2147483648, -1], [1, 2147483647] }" }
    ]
  }
  
  evalAssume: assuming Cond: (reg_$1<int a>) != (reg_$0<int b>) to be false in state:
  "program_state": {
    "constraints": [
      { "symbol": "(reg_$0<int b>) - (reg_$1<int a>)", "range": "{ [1, 2147483647] }" },
      { "symbol": "(reg_$1<int a>) != (reg_$0<int b>)", "range": "{ [0, 0] }" }
    ]
  }

As you can see, the **latter** is the //infeasable// path, and if we have had serialized the constraints and let the Z3 check it, we would have gotten that it's unfeasable.
At this point the checker can dump any useful data for debugging, and crash the analyzer to let us know that something really bad happened.

> [...] And that might be too slow, it would have the same speed as using z3 instead of the range based solver.

Yes, it will probably freaking slow, but at least we have something.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D88019