geo1-ll.c can overflow

[hernanponcedeleon]

The following program can overflow

int main() {
    int z, k;
    long long x, y, c;
    z = __VERIFIER_nondet_int();
    k = __VERIFIER_nondet_int();
    assume_abort_if_not(z >= 1);
    assume_abort_if_not(k >= 1);

    x = 1;
    y = z;
    c = 1;

    while (1) {
        __VERIFIER_assert(x*z - x - y + 1 == 0);

        if (!(c < k)) 
            break;

        c = c + 1;
        x = x * z + 1;
        y = y * z;

    }  //geo1

    x = x * (z - 1);

    __VERIFIER_assert(1 + x - y == 0);
    return 0;
}

Let z = 2147483647. After the first while iteration

x = 2147483648
y = 2147483647

After the second iteration

x = 4611686014132420610
y = 4611686014132420609

The overflow can happen in the next iteration when the multiplication x*z happens inside the first __VERIFIER_assert.

The overflow is confirmed by CBMC if I replace the non deterministic values by 2147483647

cbmc --signed-overflow-check git/sv-benchmarks/c/nla-digbench/geo1-ll.c -unwind 2
CBMC version 5.11 (cbmc-5.11) 64-bit x86_64 macos
Parsing git/sv-benchmarks/c/nla-digbench/geo1-ll.c
Converting
Type-checking geo1-ll
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Unwinding loop main.0 iteration 1 file git/sv-benchmarks/c/nla-digbench/geo1-ll.c line 34 function main thread 0
Not unwinding loop main.0 iteration 2 file git/sv-benchmarks/c/nla-digbench/geo1-ll.c line 34 function main thread 0
size of program expression: 99 steps
simple slicing removed 10 assignments
Generated 20 VCC(s), 20 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
396 variables, 143 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
396 variables, 0 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime decision procedure: 0.00125636s

** Results:
git/sv-benchmarks/c/nla-digbench/geo1-ll.c function reach_error
[reach_error.assertion.1] line 9 assertion 0: SUCCESS

git/sv-benchmarks/c/nla-digbench/geo1-ll.c function main
[main.overflow.1] line 35 arithmetic overflow on signed * in x * (signed long int)z: SUCCESS
[main.overflow.2] line 35 arithmetic overflow on signed - in x * (signed long int)z - x: SUCCESS
[main.overflow.3] line 35 arithmetic overflow on signed - in (x * (signed long int)z - x) - y: SUCCESS
[main.overflow.4] line 35 arithmetic overflow on signed + in ((x * (signed long int)z - x) - y) + (signed long int)1: SUCCESS
[main.overflow.5] line 40 arithmetic overflow on signed + in c + (signed long int)1: SUCCESS
[main.overflow.6] line 41 arithmetic overflow on signed * in x * (signed long int)z: SUCCESS
[main.overflow.7] line 41 arithmetic overflow on signed + in x * (signed long int)z + (signed long int)1: SUCCESS
[main.overflow.8] line 42 arithmetic overflow on signed * in y * (signed long int)z: FAILURE
[main.overflow.9] line 46 arithmetic overflow on signed - in z - 1: SUCCESS
[main.overflow.10] line 46 arithmetic overflow on signed * in x * (signed long int)(z - 1): SUCCESS
[main.overflow.11] line 48 arithmetic overflow on signed + in (signed long int)1 + x: SUCCESS
[main.overflow.12] line 48 arithmetic overflow on signed - in ((signed long int)1 + x) - y: SUCCESS

** 1 of 13 failed (2 iterations)
VERIFICATION FAILED

What I'm not sure is what would be the best solution for these kind of overflows due to big ints multiplications (I suspect the same problem happens in other benchmarks).

In this particular case, one possibility would be to restrict the value of k (which bounds the number of iterations) to something rather small (e.g. 6) and the value of z to something "big" but which could not overflow given the bound of k (e.g. 1000)

[MartinSpiessl]

Usually we would limit the value range, but this task is ridiculously exponential in nature.
The property should still hold if we calculate modulo ULLONG_MAX, so using unsigned integers would get rid of the undefined behavior. A task where this was done actually already exists as geo1-u.c. So we could add a task geo1-ull.c where we use unsigned long long. This is somewhat unsatisfactory since we want to also have a task where the negative numbers are present. The best way to do this from a software engineers perspective would be to use the builtin overflow functions to check for overflows and terminate in those cases. These overflow checks are not supported by all tools, but coding them in manually is not the way to go if you ask me.

[hernanponcedeleon]

Would be the following a general solution for overflows involving multiplication? If we have y * z (I assume both variables are of type int), add the following check before assume_abort_if_not(2147483647 / z >= y). I tried in a couple of examples where I was having problems (possible because of integer overflows due to multiplications) and it seems to work.

[MartinSpiessl]

This works if both integers are positive only. The general check is more complicated, cf. https://wiki.sei.cmu.edu/confluence/display/c/INT32-C.+Ensure+that+operations+on+signed+integers+do+not+result+in+overflow#INT32C.Ensurethatoperationsonsignedintegersdonotresultinoverflow-CompliantSolution.3 (you might need to reload this page once it is loaded to jump to the right anchor I linked, some weird browser bug at least in chrome)

A general solution in my opinion would be to write assume_abort_if_not(__builtin_smulll_overflow(y,z,*y)); instead of y = y * z;

One of the objectives with sv-benchmarks is to have benchmarks that are close to code that would be found in real software. For real software I would either use builtin overflow functions and report to the callee of such an algorithm whether the calculations worked without an overflow or I would limit the range of inputs to ones that guarantee that there is no overflow.

Bounded tasks are generated anyways in nla-digbench-scaling. So for this issue I would generate two additional tasks:

• geo1-ull.c where we solve the problem by using unsigned long long
• geo1-ll-ovfcheck.c where we use builtin overflow functions to ensure defined behavior