CSA makes a unreasonable assumption that `a() <= 0` is true

[Geoffrey1014]

date: 2023-1-9 commit: args: --analyze -Xclang -analyzer-stats -Xclang -analyzer-checker=core,debug.ExprInspection test:

#include "stdio.h"
#include <stdint.h>
#include <stdbool.h>
void clang_analyzer_eval(int){}

uint16_t a() {
  for (;;)
    if (a() <= 0) {
      clang_analyzer_eval((a() <= 0)==true);
      clang_analyzer_eval(((a())<(0))||((a())==(0)));
      clang_analyzer_eval(((a())+0)<=((0)+0));
      clang_analyzer_eval(((a())+0)<=((0)+1));
      clang_analyzer_eval(((a())+1)<=((0)+1));
      clang_analyzer_eval(((a())+0)<=((0)+2));
      clang_analyzer_eval(((a())+1)<=((0)+2));
      clang_analyzer_eval(((a())+2)<=((0)+2));
      clang_analyzer_eval(((a())-0)<=((0)-0));
      clang_analyzer_eval((!(a() <= 0))==false);
      clang_analyzer_eval((((a())>=(0))&&((a())!=(0)))==false);
      clang_analyzer_eval(true);
      ;
    }
return 2;
}

report: https://github.com/llvm/llvm-project/issues/59964 fix: original:

[Geoffrey1014]

Hi, I found a problem that CSA RecursionChecker has false negative for for (;;) if (a() <= 0) { .... https://godbolt.org/z/57EGG8sYK

I think CSA should not makes the assumption that a() <= 0 could be true.

And, GCC Static Analyzer does not make the assumption and reports [-Wanalyzer-infinite-recursion]. https://godbolt.org/z/79789dKec

Compilation optons: --analyze -Xclang -analyzer-stats -Xclang -analyzer-checker=core,alpha.security.taint,debug.ExprInspection,debug.TaintTest

Input:

#include "stdio.h"
#include <stdint.h>
#include <stdbool.h>
void clang_analyzer_eval(int){}

uint16_t a() {
  for (;;)
    if (a() <= 0) {
      clang_analyzer_eval((a() <= 0)==true);
      clang_analyzer_eval(((a())<(0))||((a())==(0)));
      clang_analyzer_eval(((a())+0)<=((0)+0));
      clang_analyzer_eval(((a())+0)<=((0)+1));
      clang_analyzer_eval(((a())+1)<=((0)+1));
      clang_analyzer_eval(((a())+0)<=((0)+2));
      clang_analyzer_eval(((a())+1)<=((0)+2));
      clang_analyzer_eval(((a())+2)<=((0)+2));
      clang_analyzer_eval(((a())-0)<=((0)-0));
      clang_analyzer_eval((!(a() <= 0))==false);
      clang_analyzer_eval((((a())>=(0))&&((a())!=(0)))==false);
      clang_analyzer_eval(true);
      ;
    }
return 2;
}

Output:

<source>:9:7: warning: FALSE [debug.ExprInspection]
      clang_analyzer_eval((a() <= 0)==true);
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:9:7: warning: TRUE [debug.ExprInspection]
      clang_analyzer_eval((a() <= 0)==true);
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:10:7: warning: FALSE [debug.ExprInspection]
      clang_analyzer_eval(((a())<(0))||((a())==(0)));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:10:7: warning: TRUE [debug.ExprInspection]
      clang_analyzer_eval(((a())<(0))||((a())==(0)));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:11:7: warning: FALSE [debug.ExprInspection]
      clang_analyzer_eval(((a())+0)<=((0)+0));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:11:7: warning: TRUE [debug.ExprInspection]
      clang_analyzer_eval(((a())+0)<=((0)+0));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:12:7: warning: FALSE [debug.ExprInspection]
      clang_analyzer_eval(((a())+0)<=((0)+1));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:12:7: warning: TRUE [debug.ExprInspection]
      clang_analyzer_eval(((a())+0)<=((0)+1));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:7: warning: FALSE [debug.ExprInspection]
      clang_analyzer_eval(((a())+1)<=((0)+1));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:7: warning: TRUE [debug.ExprInspection]
      clang_analyzer_eval(((a())+1)<=((0)+1));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:14:7: warning: FALSE [debug.ExprInspection]
      clang_analyzer_eval(((a())+0)<=((0)+2));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:14:7: warning: TRUE [debug.ExprInspection]
      clang_analyzer_eval(((a())+0)<=((0)+2));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:7: warning: FALSE [debug.ExprInspection]
      clang_analyzer_eval(((a())+1)<=((0)+2));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:7: warning: TRUE [debug.ExprInspection]
      clang_analyzer_eval(((a())+1)<=((0)+2));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:16:7: warning: FALSE [debug.ExprInspection]
      clang_analyzer_eval(((a())+2)<=((0)+2));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:16:7: warning: TRUE [debug.ExprInspection]
      clang_analyzer_eval(((a())+2)<=((0)+2));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:17:7: warning: FALSE [debug.ExprInspection]
      clang_analyzer_eval(((a())-0)<=((0)-0));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:17:7: warning: TRUE [debug.ExprInspection]
      clang_analyzer_eval(((a())-0)<=((0)-0));
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:18:7: warning: FALSE [debug.ExprInspection]
      clang_analyzer_eval((!(a() <= 0))==false);
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:18:7: warning: TRUE [debug.ExprInspection]
      clang_analyzer_eval((!(a() <= 0))==false);
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:19:7: warning: FALSE [debug.ExprInspection]
      clang_analyzer_eval((((a())>=(0))&&((a())!=(0)))==false);
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:19:7: warning: TRUE [debug.ExprInspection]
      clang_analyzer_eval((((a())>=(0))&&((a())!=(0)))==false);
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:20:7: warning: TRUE [debug.ExprInspection]
      clang_analyzer_eval(true);
      ^~~~~~~~~~~~~~~~~~~~~~~~~
===-------------------------------------------------------------------------===
                                Analyzer timers
===-------------------------------------------------------------------------===
  Total Execution Time: 0.0641 seconds (0.1070 wall clock)

   ---User Time---   --System Time--   --User+System--   ---Wall Time---  --- Name ---
   0.0550 ( 87.0%)   0.0003 ( 35.9%)   0.0553 ( 86.3%)   0.0907 ( 84.7%)  Path exploration time
   0.0082 ( 12.9%)   0.0002 ( 21.6%)   0.0083 ( 13.0%)   0.0123 ( 11.5%)  Path-sensitive report post-processing time
   0.0001 (  0.1%)   0.0003 ( 42.5%)   0.0004 (  0.7%)   0.0040 (  3.8%)  Syntax-based analysis time
   0.0633 (100.0%)   0.0008 (100.0%)   0.0641 (100.0%)   0.1070 (100.0%)  Total

23 warnings generated.
Compiler returned: 0

[Geoffrey1014]

NoQ adds static analyzer checker for finding infinite recursion. https://reviews.llvm.org/D26589 But it is abandoned.

[Geoffrey1014]

They should handle infinite recursion.

They do not handle infinite recursion well. https://godbolt.org/z/esxrdz5bK https://godbolt.org/z/4j1Ehe8dj