[PATCH] D103314: [Analyzer][solver] Simplify existing constraints when a new constraint is added

Wed Jun 9 07:54:50 PDT 2021

martong added a comment.

In D103314#2798968 <https://reviews.llvm.org/D103314#2798968>, @martong wrote:

> In D103314#2790868 <https://reviews.llvm.org/D103314#2790868>, @vsavchenko wrote:
>
>> Awesome!
>> I know, I said that we are ready to land, but I think I was too excited about this change. We probably should have some data on how it performs on real-life codebases.
>
> Just some quick update on the status of this patch. I've done some measurements on smaller open source C projects (e.g tmux) and didn't see any noticeable slow-down. However, I've run into a bad-bad assertion failure in my favorite Checker (StdLibraryFu...). The assertion indicates that neither !State nor State is feasible, so this throws me back to the debugger for a while.

Finally, I could boil down the infeasible parent state problem and added a test case `test_deferred_contradiction` to catch that. The solution is surprisingly simple: just try to simplify the symbolic expression of an equivalency before we start to update the State with the equivalency info.

Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103314