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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
