[pulse] PulseFormula fails to detect simple UNSAT, leading to false positives in Pulse-ISL

[tobycmurray]

Infer version v1.1.0-ed1af6a90

(i.e. built from commit HEAD ed1af6a90b034d6b1c6362aad53a7923c872fda8)

MacOS Monterey 12.5.1, on ARM M1

A minimal example is below. Of course the null-pointer dereference is not actually reachable. Pulse (and Pulse-ISL) think that it is. PulseFormula is seemingly not detecting that the path condition is UNSAT, after the summary for test_func is applied at the callsite in main. Note that, as the comments say, the issue appears to be an interaction of the prior if-condition and the resulting addition to the path condition.

#include <stdio.h>
#include <stdlib.h>

void test_func(int m, int b){
  /* commenting out this if-statement makes the false bug disappear */
  if (b >= 34) {
    abort(); 
  } 

  /* uncommenting an additional if-test like this also makes it disappear/
  if (b+1<b){
    abort();
  }
  */

  if (m < b * 2) {
    printf("Against all the odds, I'm going to dereference a null-pointer\n");
    int *p = NULL;
    (void)*p;
  }else{
    printf("Of course I'm not going to dereference a null-pointer\n");
  }
}

int main(){
  test_func(64,32);
  return 0;
}

Infer command (the same false bug is also reported regardless of whether --pulse-isl is present, so this seems to be an issue for Pulse in addition to Pulse-ISL).

./infer/bin/infer  --pulse-only --pulse-isl --no-pulse-report-latent-issues -- cc -c  test.c

Command output:

Capturing in make/cc mode...
Found 1 source file to analyze in /Users/tobiasm1/git/infer/infer-out
1/1 [################################################################################] 100% 22.326ms

/Users/tobiasm1/tmp/libsodium_binhex.c:27: error: Null Dereference
  The call to `test_func` may trigger the following issue: `p` could be null (from the call to `test_func()` on line 18) and is dereferenced in the call to `test_func()`.
  25. 
  26. int main(){
  27.   test_func(64,32);
        ^
  28.   return 0;
  29. }

Found 1 issue
             Issue Type(ISSUED_TYPE_ID): #
  Null Dereference(NULLPTR_DEREFERENCE): 1

[jvillard]

Thanks for the bug report, it surfaces an interesting weakness in the current way the "tableau" arithmetic domain we use for inequalities interacts (not enough) with the linear arithmetic domain.

[tobycmurray]

Here is another similar example, in case it's helpful. Also tested against ed1af6a90b034d6b1c6362aad53a7923c872fda8

#include <stdio.h>

void
test_func2(int size){
  int len = (size + 31) / 32;
  printf("len: %u\n",len);
  // commenting out the outer if-test removes the spurious NULL dereference report
  if (0 < len){
    if (1 < len){
      int *p = NULL;
      (void)*p;
    }else{
      printf("Of course not.\n");
    }
  }
}

int main(){
  test_func2(2);
  return 0;
}

% ./infer/bin/infer --pulse-only --pulse-isl --no-pulse-report-latent-issues -- cc -c ~/tmp/cttk_int31_ppp.c
Capturing in make/cc mode...
Found 1 source file to analyze in /Users/tobiasm1/git/infer/infer-out
1/1 [################################################################################] 100% 16.645ms

/Users/tobiasm1/tmp/cttk_int31_ppp.c:20: error: Null Dereference
  The call to `test_func2` may trigger the following issue: `p` could be null (from the call to `test_func2()` on line 11) and is dereferenced in the call to `test_func2()`.
  18. 
  19. int main(){
  20.   test_func2(2);
        ^
  21.   return 0;
  22. }

Found 1 issue
             Issue Type(ISSUED_TYPE_ID): #
  Null Dereference(NULLPTR_DEREFERENCE): 1

[jvillard]

Thanks again for the report @tobycmurray, this led to a nice improvement. I've verified that 74fdf59a3b39f02b3da0baf6c971444209e392f1 fixes the issue in both of your examples and there's a new unit test for the arithmetic domain that captures the crux of the problem.