Unsoundness from null-byte arrayDomain merge

[karoliineh]

By some miracle, I happened to analyze the smtprc from the bench repository with several master versions, revealing that a bug was introduced and then 'fixed' by merging an unrelated PR.

The bug manifested in an unsoundness where 1125 lines were dead out of 2033 lines analyzed (instead of 93 dead out of 2053 as usual) so that all of the pthread_create calls were dead.

The bug appeared with 3b2f4a55736e83350fe71b345cf0d0beb1fd66ef and was 'fixed' by merging #1233. However, as #1233 did not edit anything related to base, which was the only non-test file modified by 3b2f4a55736e83350fe71b345cf0d0beb1fd66ef, the original bug might still be there but to some extent just be masked by #1233.

I haven't been able to extract a smaller test showing the unsoundness introduced by 3b2f4a55736e83350fe71b345cf0d0beb1fd66ef, but an example of the original is the following:

smtprc-2.0.3/parse_config_files.c 70-94:

if(strstr(iprange, ",") == NULL) {
    strncpy(buf, iprange, MAXDATA);
    buf[strlen(iprange)] ='\0';
    last = 1;
    goto GETIP;
} else {
    p = iprange;
    t = p;
    while(*p++) {
        if(*p==',') {
            *p = '\0';
            p+=1;
            strncpy(buf, t, MAXDATA);
        GETIP:
            iprange2=s_malloc((strlen(buf)+1) * sizeof(char));
            strncpy(iprange2, buf, strlen(buf));
            iprange2[strlen(buf)] = '\0';

            addy[0] = addy[1] = addy[2] = addy[3] = addy[4] = NULL;

            addy[0] = r = buf;

            debug("R == %s\n", r);

            while(*++r) { // detected as always false by Goblint

[sim642]

The issue was introduced by #1076. It's not just with the null byte array domain because it also happens with that domain disabled. The PR also modified str* function handling for arrays in general and some change there was unsound.

In smtprc, the unsoundness was simply revealed by one branch dead (because of probably unsound array contents after str* operations). PR #1233 fixed a more wild unsoundness issue of both branches dead, at the point of branching, not any earlier operations. This is why I believe #1233 did not fix the root cause, but is only covering it up. If the array contents are unsound, that might lead to unsoundness in some other way as well, not necessarily a branch on the array contents.