Some false positives and false negatives of INFER --pulse

[YizhuoZhai]

Hi, I'm trying the INFER on some small pieces of code, but seems infer does not give the correct answer.

1. A false positive: And also this one, here we should not have any bug here as the "arg" does not have any uninitialized use.

   void callee(int arg) {
   arg = 5;
   arg++;
   }
   void caller() {
   int arg;
   callee(arg);
   }

$infer --pulse --enable-issue-type PULSE_UNINITIALIZED_VALUE_LATENT -- clang -c test3.c
Capturing in make/cc mode...
...
test.c:7: error: Uninitialized Value
  The value read from arg was never initialized.
  5. void caller() {
  6.     int arg;
  7.     callee(arg);
         ^
  8. }  

$infer --version
Infer version v1.1.0
Copyright 2009 - present Facebook. All Rights Reserved.

2. Another false positive:

void callee(int arg1, int arg2) {
    int *p;
    int a = 0;
    if (arg1 && arg2) 
        p = &a;
    *p++;
}
void caller(){
    callee(1, 1);
}

$ infer --pulse --enable-issue-type PULSE_UNINITIALIZED_VALUE_LATENT -- clang -c cond.c
Capturing in make/cc mode...
Found 1 source file to analyze in /opt/infer-linux64-v1.1.0/test/alias/infer-out
1/1 [################################################################################] 100% 80.858ms

cond.c:8: error: Dead Store
  The value written to &p (type int*) is never used.
   6.             p = &a;
   7.     }
   8.     *p++;
           ^
   10. }
  11. void caller() {

cond.c:8: error: Uninitialized Value
  The value read from p was never initialized.
   6.             p = &a;
   7.     }
   8.     *p++;
           ^
   9. }
  10. void caller() {

Found 2 issues
                Issue Type(ISSUED_TYPE_ID): #
  Uninitialized Value(UNINITIALIZED_VALUE): 1
                    Dead Store(DEAD_STORE): 1

3. A false negative:

   void callee(int *arg) {
   *arg++; //Should have an uninitialized use warning here.
   }
   void caller() {
   int arg;
   callee(&arg);
   arg++; //Should have another uninitialized use warning here.
   }

   
   $ # infer --pulse --enable-issue-type PULSE_UNINITIALIZED_VALUE_LATENT -- clang -c test2.c
   Capturing in make/cc mode...
   Found 1 source file to analyze in /opt/infer-linux64-v1.1.0/test/alias/infer-out
   1/1 [################################################################################] 100% 91.584ms

test2.c:2: error: Dead Store The value written to &arg (type int*) is never used.

1. void callee(int *arg){
2. *arg ++; ^
3. }
4. void caller() {

Found 1 issue Issue Type(ISSUED_TYPE_ID): # Dead Store(DEAD_STORE): 1

[jvillard]

Hi @YizhuoZhai, thanks for your report.

1. I think this is a true positive: caller does read arg and passes its value to callee, even if callee doesn't use it. Looking at the produced llvm we see that the uninitialised value that %1 points to is loaded: https://godbolt.org/z/ohYqYMMdE
2. I think we want to report this one so the output is ok here: reading p is only ok if arg1 && arg2 so the function will have a bug in any other case.
3. I do get a report from pulse in this example so it seems this is no longer FN:

   $ cat issue1612.c
   void callee(int *arg) {
   *arg++; //Should have an uninitialized use warning here.
   }
   void caller() {
   int arg;
   callee(&arg);
   arg++; //Should have another uninitialized use warning here.
   }
   $ infer --pulse-only -- clang -c ~/tmp/issue1612.c 
   [...]
   issue1612.c:6: error: Uninitialized Value
   `arg` is read without initialization during the call to `callee()`.
   4. void caller() {
   5.     int arg;
   6.     callee(&arg);
        ^
   7.    arg++; //Should have another uninitialized use warning here.
   8. }