Clang Static Analyzer and the Z3 constraint solver

As far as static analyzers are concerned, one of the most important point to consider is filtering out false positives as much as possible, in order for the reports to be actionable.

This is an area on which Coverity did an excellent job, and likely a major reason why they got so popular within the open source community, despite being a closed-source product.

LLVM has the LLVM_ENABLE_Z3_SOLVER build option, which allows building LLVM against the Z3 constraint solver.

It is documented as follow:

LLVM_ENABLE_Z3_SOLVER:BOOL
    If enabled, the Z3 constraint solver is activated for the Clang static analyzer.
    A recent version of the z3 library needs to be available on the system.

The option is enabled in the Debian 11 package (clang-tools-11), but not in Fedora 36 or Ubuntu 22.04 ones. I added a build option (not enabled by default) to the llvm and clang packages in Pkgsrc, and successfully built Z3 enabled packages on NetBSD.

For Pkgsrc users, add the following in mk.conf, and build lang/clang:

PKG_OPTIONS.llvm=      z3
PKG_OPTIONS.clang=    z3

There are two ways of using Z3 with the Clang Static Analyzer, and to demonstrate them, let’s reuse the small demo snippet from the SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer paper.

unsigned int func(unsigned int a) {
      unsigned int *z = 0;

      if ((a & 1) && ((a & 1) ^1))
              return *z; // unreachable

      return 0;
}

For each method, we can use Clang directly on a given translation unit or use scan-build.

The first way is using Z3 as an external constraint solver:

$ clang --analyze -Xanalyzer -analyzer-constraints=z3 main.c

$ scan-build -constraints z3 clang -c main.c
scan-build: Using '/usr/lib/llvm-11/bin/clang' for static analysis
scan-build: Analysis run complete.
scan-build: Removing directory '/tmp/scan-build-2022-06-21-171854-18215-1' because it contains no reports.
scan-build: No bugs found.

This is a lot slower than the default, and the commit which documented the feature mentions a ~15x slowdown over the built-in constraint solver.

The second way is using the default range based solver but having Z3 do refutation to filter out false positives, which is a lot faster:

$ clang --analyze -Xanalyzer -analyzer-config -Xanalyzer crosscheck-with-z3=true main.c

$ scan-build -analyzer-config crosscheck-with-z3=true clang -c main.c
scan-build: Using '/usr/lib/llvm-11/bin/clang' for static analysis
scan-build: Analysis run complete.
scan-build: Removing directory '/tmp/scan-build-2022-06-21-171924-18226-1' because it contains no reports.
scan-build: No bugs found.

Again, no bugs found. How boring.

We can verify what happens if we run the analyzer without involving Z3 at all:

$ clang --analyze main.c
main.c:5:9: warning: Dereference of null pointer (loaded from variable 'z') [core.NullDereference]
        return *z; // unreachable
               ^~
1 warning generated.

We get a false positive, because the default constraint solver cannot reason about bitwise operations (among other things), and report an unreachable NULL pointer dereference.

from Hacker News https://ift.tt/LnUOT2B