CSA evaluates `( ((b)-0) <= ((c)-0) ) ` to be FALSE with the fact `c >= b`

[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){}

int a(int* b, int *c) {

d:
  if (c >= b) {
    clang_analyzer_eval((c >= b)==true);
    clang_analyzer_eval(((b)+0)<=((c)+0));

    clang_analyzer_eval(((b)-0)<=((c)-0));

    clang_analyzer_eval((!(c >= b))==false);
    clang_analyzer_eval((((c)<=(b))&&((c)!=(b)))==false);
    clang_analyzer_eval(true);
    goto d;
  }
}

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

[Geoffrey1014]

Hi, I found a problem that CSA evaluates ( ((b)-0) <= ((c)-0) ) to be FALSE in the true branch of if (c >= b).

https://godbolt.org/z/bPYsTzEMj

Input:

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

int a(int* b, int *c) {

d:
  if (c >= b) {
    clang_analyzer_eval((c >= b)==true);
    clang_analyzer_eval(((b)+0)<=((c)+0));

    clang_analyzer_eval(((b)-0)<=((c)-0));

    clang_analyzer_eval((!(c >= b))==false);
    clang_analyzer_eval((((c)<=(b))&&((c)!=(b)))==false);
    clang_analyzer_eval(true);
    goto d;
  }
}

Output:

<source>:10:5: warning: TRUE [debug.ExprInspection]
    clang_analyzer_eval((c >= b)==true);
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:11:5: warning: FALSE [debug.ExprInspection]
    clang_analyzer_eval(((b)+0)<=((c)+0));
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:11:5: warning: TRUE [debug.ExprInspection]
    clang_analyzer_eval(((b)+0)<=((c)+0));
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:5: warning: FALSE [debug.ExprInspection]
    clang_analyzer_eval(((b)-0)<=((c)-0));
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:5: warning: TRUE [debug.ExprInspection]
    clang_analyzer_eval(((b)-0)<=((c)-0));
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:5: warning: TRUE [debug.ExprInspection]
    clang_analyzer_eval((!(c >= b))==false);
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:16:5: warning: TRUE [debug.ExprInspection]
    clang_analyzer_eval((((c)<=(b))&&((c)!=(b)))==false);
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:17:5: warning: TRUE [debug.ExprInspection]
    clang_analyzer_eval(true);
    ^~~~~~~~~~~~~~~~~~~~~~~~~
===-------------------------------------------------------------------------===
                                Analyzer timers
===-------------------------------------------------------------------------===
  Total Execution Time: 0.0057 seconds (0.0181 wall clock)

   ---User Time---   --System Time--   --User+System--   ---Wall Time---  --- Name ---
   0.0033 ( 88.6%)   0.0003 ( 14.3%)   0.0036 ( 63.8%)   0.0102 ( 56.3%)  Path exploration time
   0.0001 (  2.3%)   0.0004 ( 21.9%)   0.0005 (  8.8%)   0.0048 ( 26.4%)  Syntax-based analysis time
   0.0003 (  9.1%)   0.0012 ( 63.8%)   0.0015 ( 27.3%)   0.0031 ( 17.3%)  Path-sensitive report post-processing time
   0.0038 (100.0%)   0.0019 (100.0%)   0.0057 (100.0%)   0.0181 (100.0%)  Total

8 warnings generated.
Compiler returned: 0

[Geoffrey1014]

Further reduced case is showed as follows. CSA knows: "constraints": [ { "symbol": "(reg$1<int * b>) - (reg$0<int * c>)", "range": "{ [-9223372036854775808, 0] }" } ]. But CSA does not know "((b)+0)<=((c)+0)" is TRUE.

Does this means it is a feature not supported? Could you answer my doubts? Thanks a lot!

GCC static analyzer is ok: https://godbolt.org/z/KqvG3z8b9

CSA: https://godbolt.org/z/7s7bdW1s5

#include "stdio.h"
#include <stdint.h>
#include <stdbool.h>

void clang_analyzer_eval();
void clang_analyzer_printState();
void clang_analyzer_dump();
void clang_analyzer_express();

int a(int* b, int *c) {

  if (c >= b) {
    clang_analyzer_printState();
    clang_analyzer_dump( (c +1) );
    clang_analyzer_dump( c );
    clang_analyzer_dump( b );
    clang_analyzer_eval((c >= b));
    clang_analyzer_eval((c >= b)==true);
    clang_analyzer_eval(((b)+0)<=((c)+0));

    clang_analyzer_eval(((b)-0)<=((c)-0));

  }
}

compiling with options: --analyze -Xclang -analyzer-stats -Xclang -analyzer-config -Xclang eagerly-assume=false -Xclang -analyzer-checker=core,debug.ExprInspection

"program_state": {
  "store": null,
  "environment": { "pointer": "0x561b2f4da3c0", "items": [
    { "lctx_id": 1, "location_context": "#0 Call", "calling": "a", "location": null, "items": [
      { "stmt_id": 12077, "kind": "ImplicitCastExpr", "pretty": "clang_analyzer_printState", "value": "&code{clang_analyzer_printState}" }
    ]}
  ]},
  "constraints": [
    { "symbol": "(reg_$1<int * b>) - (reg_$0<int * c>)", "range": "{ [-9223372036854775808, 0] }" }
  ],
  "equivalence_classes": null,
  "disequality_info": null,
  "dynamic_types": null,
  "dynamic_casts": null,
  "checker_messages": null
}<source>:14:5: warning: &Element{SymRegion{reg_$0<int * c>},1 S64b,int} [debug.ExprInspection]
    clang_analyzer_dump( (c +1) );
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:5: warning: &SymRegion{reg_$0<int * c>} [debug.ExprInspection]
    clang_analyzer_dump( c );
    ^~~~~~~~~~~~~~~~~~~~~~~~
<source>:16:5: warning: &SymRegion{reg_$1<int * b>} [debug.ExprInspection]
    clang_analyzer_dump( b );
    ^~~~~~~~~~~~~~~~~~~~~~~~
<source>:17:5: warning: TRUE [debug.ExprInspection]
    clang_analyzer_eval((c >= b));
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:18:5: warning: UNKNOWN [debug.ExprInspection]
    clang_analyzer_eval((c >= b)==true);
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:19:5: warning: UNKNOWN [debug.ExprInspection]
    clang_analyzer_eval(((b)+0)<=((c)+0));
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:21:5: warning: UNKNOWN [debug.ExprInspection]
    clang_analyzer_eval(((b)-0)<=((c)-0));
    ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
===-------------------------------------------------------------------------===
                                Analyzer timers
===-------------------------------------------------------------------------===
  Total Execution Time: 0.0048 seconds (0.0497 wall clock)

   ---User Time---   --System Time--   --User+System--   ---Wall Time---  --- Name ---
   0.0000 (  0.0%)   0.0032 ( 71.4%)   0.0032 ( 66.6%)   0.0329 ( 66.1%)  Path exploration time
   0.0002 ( 69.7%)   0.0004 ( 10.0%)   0.0007 ( 14.0%)   0.0151 ( 30.3%)  Syntax-based analysis time
   0.0001 ( 30.3%)   0.0008 ( 18.6%)   0.0009 ( 19.4%)   0.0017 (  3.5%)  Path-sensitive report post-processing time
   0.0003 (100.0%)   0.0045 (100.0%)   0.0048 (100.0%)   0.0497 (100.0%)  Total

7 warnings generated.
Compiler returned: 0

[Geoffrey1014]

This should be related to arithmetics on pointers.

[ghost]

As mentioned above, GSA can handle: https://godbolt.org/z/KqvG3z8b9.

[Geoffrey1014]