GaloisInc / BESSPIN-Tool-Suite

The core tool of the BESSPIN Framework.
Other
5 stars 2 forks source link

generated bufferError test with no error #1250

Open brooksdavis opened 3 years ago

brooksdavis commented 3 years ago

I've encountered a generated bufferError test which does not appear to contain an overflow. The full test can be found at https://gist.github.com/brooksdavis/b800bbc2dfc273e7e75e9e9db6e03806 and a more readable version run through unifdefall at https://gist.github.com/brooksdavis/0ca414645c42989e1f6add7c06bf3505. Manually reduced we see this fragment which would contain an overflow if there was one, but there isn't because the for body is only entered once with idx==0.

    printf("<begin overflow read/write loop>\r\n");
    fflush(stdout);
    /*
     * Buffer Access: Read/Write
     */
    for(int idx=0; idx>=(0+0); idx=idx+-1)
    {
            /* Attempt to catch the case where we overwrite idx, causing non-termination */
            if (((-1 < 0) && (idx > 0)) ||
                ((-1 > 0) && (idx < 0)))
            {
                /* If we are here, then somehow 'idx' is GREATER than its initial value
                   even though it is monotonically DECREASING (resp. LESS/INCREASING) */
                printf("<write to idx detected>\r\n");
                fflush(stdout);
                break;
            }

         *(buf_qzRhpSqfg + idx) = tmp_EuEdfoERQKtjt;
    }
    printf("<end overflow read/write loop>\r\n");
    fflush(stdout);

The config.ini contains the following which should make this reproducible:

[bufferErrors]
# Before generating `nTests` tests, generate and throw away `nSkip` tests
useSeed   = Yes
# Whether to use a specific seed (instead of a random one)
seed      = 0
brooksdavis commented 3 years ago

FWIW, switching to

[bufferErrors]
# Before generating `nTests` tests, generate and throw away `nSkip` tests
useSeed   = Yes
# Whether to use a specific seed (instead of a random one)
seed      = 1

is a viable workaround.