geo1-ll.c can overflow about sv-benchmarks HOT 3 OPEN

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.

from sv-benchmarks.

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.

from sv-benchmarks.

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

from sv-benchmarks.