Failed to detect null derreference in nested C block

[dgutson]

Please include the following information:

• [x] The version of infer from infer --version.
• [x] Your operating system and version, for example "Debian 9", "MacOS High Sierra", whether you are using Docker, etc.
• [x] Which command you ran, for example infer -- make.
• [x] The full output in a paste, for instance a gist.
• [x] If possible, a minimal example to reproduce your problem (for instance, some code where infer reports incorrectly, together with the way you run infer to reproduce the incorrect report).

When trying this example:

#define NULL 0
#define KABOOM()  *(char*)(NULL) = 'a'

typedef int GUID;
typedef int EFI_HANDLE;
typedef int EFI_STATUS;
typedef unsigned int UINTN;

static const int someConstant = 0x74D936FA;
extern int gVar2;
extern int gVar1;
#ifndef __fastcall
#   define __fastcall
#endif

struct
{
    EFI_STATUS (*funPtr)(const GUID* guid, int arg, int* outProtocol);
} *gVar3;

EFI_STATUS __fastcall SmiHandler(EFI_HANDLE DispatchHandle, const void *Context, void *CommBuffer, UINTN *CommBufferSize)
{
    KABOOM();
    if ( CommBuffer && CommBufferSize && !gVar1 )
    {
        if ( !gVar2 )
        {
            if ((gVar3->funPtr)(&someConstant, 0, &gVar2) < 0 )
            {
                KABOOM();
            }
        }
    }
    (void)DispatchHandle;
    (void)Context;
    return 0;
}

infer correctly detects the first null derreference (KABOOM), but not the second.

Infer version: 1.1.0 OS: WSL 2, Ubuntu 22.04.1, downloaded linux binary Command: infer run --starvation --linters --biabduction --bufferoverrun --siof --pulse --annotation-reachability --liveness --loop-hoisting --quandary --uninit -- clang -c bug_infer.c Output:

bug_infer.c:23: error: Nullptr Dereference
  Pulse found a potential null pointer dereference  on line 23.
  21. EFI_STATUS __fastcall SmiHandler(EFI_HANDLE DispatchHandle, const void *Context, void *CommBuffer, UINTN *CommBufferSize)
  22. {
  23.     KABOOM();
          ^
  24.     if ( CommBuffer && CommBufferSize && !gVar1 )
  25.     {

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

Datum: infer does detect an uninitialized read instead of the null pointer derref. For example, replacing the second KABOOM by adding an uninitialized variable to one of the globals.

[dgutson]

CC @qequ

[jvillard]

The analysis stops after errors such as null dereference so no memory bug will be detected after the first KABOOM(). If I comment out the first KABOOM() I get a report about the second one by both pulse and biabduction. However, since it depends on the values of global variables, pulse classifies it as "latent" and biabduction gives it a low-confidence bucket (B5):

$ infer --pulse-only -F -g  --biabduction -- clang -c issue1685.c
issue1685.c:30: warning: Biabduction Analysis Stops
  exception: NULL_DEREFERENCE.
  28.             if ((gVar3->funPtr)(&someConstant, 0, &gVar2) < 0 )
  29.             {
  30.                 KABOOM();
                      ^
  31.             }
  32.         }

issue1685.c:30: error: Null Dereference
  null (last assigned on line 28) is dereferenced.
  28.             if ((gVar3->funPtr)(&someConstant, 0, &gVar2) < 0 )
  29.             {
  30.                 KABOOM();
                      ^
  31.             }
  32.         }

issue1685.c:30: error: Null Dereference
  [B5] pointer `*null` could be null and is dereferenced at line 30, column 17.
  28.             if ((gVar3->funPtr)(&someConstant, 0, &gVar2) < 0 )
  29.             {
  30.                 KABOOM();
                      ^
  31.             }
  32.         }

Found 3 issues
                              Issue Type(ISSUED_TYPE_ID): #
                      Null Dereference(NULL_DEREFERENCE): 1
            Null Dereference(NULLPTR_DEREFERENCE_LATENT): 1
  Biabduction Analysis Stops(BIABDUCTION_ANALYSIS_STOPS): 1

The reason that pulse and biabduction stop the analysis on such errors is because they model the memory behaviour of the program precisely and when something goes wrong like null is dereferenced then it's not clear how to recover a coherent abstract state. Also, if the analysis is right and there is a null deref then nothing after it will get executed, and if it's wrong then it is already confused about what's happening and so it's probably better to stop there too.

[dgutson]

@jvillard I tried, accidentally, in a different order: infer --biabduction --pulse-only -F -g -- clang -c bug_infer.c and didn't find it (even removing the first KABOOM). Is this expected behavior?

[jvillard]

@dgutson maybe on 1.1.0 pulse doesn't find the issue for some reason, I tried with the latest main branch (which should be stable enough to use as a rule) with your command and the error does get reported.

Note that --biabduction --pulse-only will run only pulse as command line arguments are interpreted in sequence.

[dgutson]

@jvillard what do you mean by "interpreted in sequence"? Does it mean that order matters? That would be a bit unexpected that the analysis changes depending on the order of the cli args. Am I missing something?