analyzer: Allow snprintf(NULL, 0, ...) (#221).

[ivanperez-keera]

IKOS currently considers that the first argument of snprintf should never be null. However, a first argument null is allowed when the second argument is zero.

This commit introduces a check for that second value; only when it is not the literal zero is the first argument checked. The check applies to the null dereference checker, the buffer overflow checker and the numerical execution engine.

This check is not perfect: the second argument could also be a variable with the value or function call that returns zero. However, since passing the literal zero is the most common scenario, we check for that case for now.

[ivanperez-keera]

I checked that this fixes the issue with the following dockerfile and test files:

# Based on image by Maxime Arthaud
FROM debian:latest
MAINTAINER Ivan Perez <ivan.perezdominguez@nasa.gov>
ARG njobs=2
ARG build_type=Release

# Upgrade
RUN apt-get update
RUN apt-get upgrade -y

# Refresh cache
RUN apt-get update

# Install all dependencies
RUN apt-get install --yes gcc g++ cmake libgmp-dev libboost-dev libboost-filesystem-dev \
    libboost-thread-dev libboost-test-dev python3 python3-pygments libsqlite3-dev libtbb-dev \
    libz-dev libedit-dev llvm-14 llvm-14-dev llvm-14-tools clang-14 \
    git python3.11-venv python3-pip

RUN apt install --yes vim

# Add ikos source code
WORKDIR /root
RUN git clone -b develop-snprintf-null https://github.com/NASA-SW-VnV/ikos

# Build ikos
RUN rm -rf /root/ikos/build && mkdir /root/ikos/build
WORKDIR /root/ikos/build
ENV MAKEFLAGS "-j$njobs"
RUN cmake \
        -DCMAKE_INSTALL_PREFIX="/opt/ikos" \
        -DCMAKE_BUILD_TYPE="$build_type" \
        -DLLVM_CONFIG_EXECUTABLE="/usr/lib/llvm-14/bin/llvm-config" \
        ..
RUN make
RUN make install

# Add ikos to the path
ENV PATH "/opt/ikos/bin:$PATH"

# Done
WORKDIR /

First test (should pass)

Test file:

#include <stdio.h>

int main(void) {
    snprintf(NULL, 0, "%d", 123);
    return 0;
}

Output:

$ ikos test.c 
[*] Compiling test.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'

# Time stats:
clang        : 0.613 sec
ikos-analyzer: 0.089 sec
ikos-pp      : 0.173 sec

# Summary:
Total number of checks                : 3
Total number of unreachable checks    : 0
Total number of safe checks           : 3
Total number of definite unsafe checks: 0
Total number of warnings              : 0

The program is SAFE

# Results
No entries.

Second test (should fail)

Test file:

#include <stdio.h>

int main(void) {
    snprintf(NULL, 1, "%d", 123);
    return 0;
}

Output:

$ ikos test.c 
[*] Compiling test.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'

# Time stats:
clang        : 0.040 sec
ikos-analyzer: 0.010 sec
ikos-pp      : 0.007 sec

# Summary:
Total number of checks                : 3
Total number of unreachable checks    : 1
Total number of safe checks           : 1
Total number of definite unsafe checks: 1
Total number of warnings              : 0

The program is definitely UNSAFE

# Results
test.c: In function 'main':
test.c:4:5: error: first argument is null
    snprintf(NULL, 1, "%d", 123);
    ^
test.c: In function 'main':
test.c:5:5: unreachable: code is dead
    return 0;
    ^