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

Gabor Marton via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Mon Sep 21 01:16:19 PDT 2020


martong added a subscriber: steakhal.
martong added a comment.

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


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D82445



More information about the cfe-commits mailing list