[PATCH] D82445: [analyzer][solver] Track symbol equivalence

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

In D82445#2284680 <https://reviews.llvm.org/D82445#2284680>, @martong wrote:

> Hi Valery,
>
> Together with @steakhal we have found a serious issue.
> The below code crashes if you compile with `-DEXPENSIVE_CHECKS`.
> The analyzer goes on an unfeasible path, the State has a contradiction.
>
> We think that `getRange(Sym("a != b")` should return a set that does not contain `0`.
> https://github.com/llvm/llvm-project/blob/e63b488f2755f91e8147fd678ed525cf6ba007cc/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp#L2064
> Currently that goes down to `infer(QualType("int"))` which results a `RangeSet[INT_MIN, INT_MAX]`.
> Stach trace attached.
>
>   // RUN: %clang_analyze_cc1 %s \
>   // RUN:   -analyzer-checker=core \
>   // RUN:   -analyzer-checker=debug.ExprInspection \
>   // RUN:   -triple x86_64-unknown-linux \
>   // RUN:   -verify
>   
>   // expected-no-diagnostics
>   
>   void f(int a, int b) {
>     int c = b - a;
>     if (c <= 0)
>       return;
>     // c > 0
>     // b - a > 0
>     // b > a
>     if (a != b)
>       return;
>     // a == b
>     // This is an unfeasible path, the State has a contradiction.
>     if (c < 0) // crash here
>       ;
>   }
>
>
>
>   #0  (anonymous namespace)::SymbolicRangeInferrer::inferRange<clang::ento::SymExpr const*> (BV=..., F=..., State=..., Origin=0x55b9979bed08) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:715
>   #1  0x00007fa2314dddc9 in (anonymous namespace)::RangeConstraintManager::getRange (this=0x55b99791ab10, State=..., Sym=0x55b9979bed08) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2012
>   #2  0x00007fa2314de1e9 in (anonymous namespace)::RangeConstraintManager::assumeSymEQ (this=0x55b99791ab10, St=..., Sym=0x55b9979bed08, Int=..., Adjustment=...) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:2064
>   #3  0x00007fa23150470d in clang::ento::RangedConstraintManager::assumeSymUnsupported (this=0x55b99791ab10, State=..., Sym=0x55b9979bed08, Assumption=false) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp:136
>   #4  0x00007fa2315353a9 in clang::ento::SimpleConstraintManager::assumeAux (this=0x55b99791ab10, State=..., Cond=..., Assumption=false) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp:62
>   #5  0x00007fa23153518b in clang::ento::SimpleConstraintManager::assume (this=0x55b99791ab10, State=..., Cond=..., Assumption=false) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp:46
>   #6  0x00007fa2315350e5 in clang::ento::SimpleConstraintManager::assume (this=0x55b99791ab10, State=..., Cond=..., Assumption=false) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp:41
>   #7  0x00007fa2313d39b3 in clang::ento::ConstraintManager::assumeDual (this=0x55b99791ab10, State=..., Cond=...) at ../../git/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:105
>   #8  0x00007fa2313d3bfc in clang::ento::ProgramState::assume (this=0x55b9979beef8, Cond=...) at ../../git/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:681
>   #9  0x00007fa231436b8a in clang::ento::ExprEngine::evalEagerlyAssumeBinOpBifurcation (this=0x7fffdf9ce9d0, Dst=..., Src=..., Ex=0x55b9979893f0) at ../../git/llvm-project/clang/lib/StaticAnalyzer/Core/ExprEngine.cpp:3058

Hi Gabor,

I'll take a look at this problem ASAP!

Thanks for such a thorough analysis of the issue!


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D82445