IKOS should tolerate snprintf(NULL, 0, ...)

[szhorvat]

ikos claims that the following C program is unsafe because of the null pointer passed to snprintf():

#include <stdio.h>

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

However, according to cppreference, when the second argument is 0, the first argument is allowed to be NULL.

https://en.cppreference.com/w/c/io/fprintf

If bufsz is zero, nothing is written and buffer may be a null pointer, however the return value (number of bytes that would be written not including the null terminator) is still calculated and returned.

We use this feature to determine the number of characters that would be written before actually writing them.

[ivanperez-keera]

I could be wrong, but at first glance I think we'd need to change:

ikos/analyzer/src/checker/null_dereference.cpp

Lines 335 to 338 in ae8200b

	case ar::Intrinsic::LibcSnprintf: {
	return {this->check_null(call, call->argument(0), inv),
	this->check_null(call, call->argument(2), inv)};
	}

so that this->check_null(call, call->argument(0), inv) is only included when this->_lit_factory.get_scalar(call->argument(1)); is not zero. There may be several cases that we'd have to consider, such as it not being zero but being a variable (which may contain the value zero) and so on.

[arthaud]

Maybe handling the special case of argument 1 being the 0 constant would be fine for now since that seems like a common use case.

[ivanperez-keera]

I've just pushed to a branch what I consider may be a possible implementation. I have not tried to compile it on my machine, but I think it should be pretty close. Feel free to check it and point out any issues you see. It's possible that there's a simpler way to check for the argument to be zero than what I'm doing.

[ivanperez-keera]

I've placed a first attempt at fixing this issue here:

ivanperez-keera@e31c16b

I haven't tried it yet, but it does compile.

I feel like there may be a simpler way of checking whether the value is the literal zero, and I'm just not seeing it (it's just lack of familiarity with all of IKOS). I could also check whether it's a variable and it's zero, and it seems like that should not be hard to do.

@arthaud is what I'm doing too far off?