Corrected verdict of hard.c (from PR #808) and added its correct version

[divyeshunadkat]

The assertion in the hard.c program is violable. Counter example was obtained using a bounded model checker and manually verified. Hence this pull request changes the verdict of this program. Also, corrected program version hard2.c with verifiable assertion is added.

Benchmarks from PR #808
Similar issues discussed in PR #813
Partial corrections issued in PR #837

• programs added to new and appropriately named directory

• license present and acceptable (either in separate file or as comment at beginning of program)

• contributed-by present (either in README file or as comment at beginning of program)

• programs added to a .set file of an existing category, or new sub-category established (if justified)

• intended property matches the corresponding .prp file

• programs and expected answer added to a .yml file according to task definitions

• architecture (32 bit vs. 64 bit) matches the corresponding .cfg file
• original sources present
• preprocessed files present
• preprocessed files generated with correct architecture
• Makefile added with correct content and without overly broad suppression of warnings

[divyeshunadkat]

Assertion within the second loop in the program hard.c is violable as depicted by the following counter-example:

INITIALIZATION
A = 1776289795 B = 1073954769

Before the 0th iteration of first loop
d = 1073954769, p = 1, B*p = 1073954769

Before the 1th iteration of first loop
d = -2147057758, p = 2, B*p = -2147057758

Before the 2th iteration of first loop
d = 851780, p = 4, B*p = 851780

Before the 3th iteration of first loop
d = 1703560, p = 8, B*p = 1703560

Before the 4th iteration of first loop
d = 3407120, p = 16, B*p = 3407120

Before the 5th iteration of first loop
d = 6814240, p = 32, B*p = 6814240

Before the 6th iteration of first loop
d = 13628480, p = 64, B*p = 13628480

Before the 7th iteration of first loop
d = 27256960, p = 128, B*p = 27256960

Before the 8th iteration of first loop
d = 54513920, p = 256, B*p = 54513920

Before the 9th iteration of first loop
d = 109027840, p = 512, B*p = 109027840

Before the 10th iteration of first loop
d = 218055680, p = 1024, B*p = 218055680

Before the 11th iteration of first loop
d = 436111360, p = 2048, B*p = 436111360

Before the 12th iteration of first loop
d = 872222720, p = 4096, B*p = 872222720

Before the 13th iteration of first loop
d = 1744445440, p = 8192, B*p = 1744445440

Before the 14th iteration of first loop
d = -806076416, p = 16384, B*p = -806076416

Before the 15th iteration of first loop
d = -1612152832, p = 32768, B*p = -1612152832

Before the 16th iteration of first loop
d = 1070661632, p = 65536, B*p = 1070661632

Before the 17th iteration of first loop
d = 2141323264, p = 131072, B*p = 2141323264

Before the 0th iteration of second loop
d = 2141323264, p = 131072, Bp = 2141323264
A = 1776289795, r = 1776289795, qB = 0, q*B+r = 1776289795

Before the 1th iteration of second loop
d = 1070661632, p = 65536, Bp = 1070661632
A = 1776289795, r = 705628163, qB = 1070661632, q*B+r = 1776289795

Before the 2th iteration of second loop
d = 535330816, p = 32768, Bp = -1612152832
A = 1776289795, r = 170297347, qB = -541491200, q*B+r = -371193853

VERIFICATION FAILED for the assertion A = q*B + r

Corrected program sets the value of 'B' to 1 in the beginning which ensures that the value of the variable 'd' is always an even number and a multiple of 2, avoiding any round off errors.

[mikhailramalho]

ESBMC, CBMC, and CPA find property violations in the benchmark.

[dbeyer]

Thanks for the correction.

[dbeyer]

... and also thanks for adding the corrected version of the program!

[MartinSpiessl]

I see some problems with this PR:

1. The corrected version of the program just sets the divisor to 1 instead of the previously non-deterministic value, this is hardly a fix since it does not preserve the original problem complexity ( returning the integer division "A//B" for non-deterministic values of A and B).

2. The counterexample provided here actually contains an overflow, i.e., undefined behavior. As such, simply setting the verdict to false is not the right thing to do. Instead the value ranges should be limited such that no overflow can occur or appropriate overflow checks should be introduced (GCC has functions for that). The original task can be kept with the overflow verdict set to true and all other verdicts removed.

[divyeshunadkat]

I see some problems with this PR:

1. The corrected version of the program just sets the divisor to 1 instead of the previously non-deterministic value, this is hardly a fix since it does not preserve the original problem complexity ( returning the integer division "A//B" for non-deterministic values of A and B).

2. The counterexample provided here actually contains an overflow, i.e., undefined behavior. As such, simply setting the verdict to false is not the right thing to do. Instead the value ranges should be limited such that no overflow can occur or appropriate overflow checks should be introduced (GCC has functions for that). The original task can be kept with the overflow verdict set to true and all other verdicts removed.

@MartinSpiessl Thank you for the mentioned points.

While the corrected version of the program (hard2.c - that sets the divisor to 1 instead of a previous non-deterministic value) does not preserve the complexity of the original program, several tools are unable to very it! Since it can distinguish between tools, I think we can retain the program (hard2.c), even if it is of lower complexity. I believe that I had tried to add guards before I submitted #920 but couldn't manage to get an appropriate correct version of the program before the competition deadline, hence this route. I would also like to vote for keeping the original program (hard.c) with a reachability verdict set to false as well (apart from setting overflow verdict to true as requested), again since it helps distinguish tools.

In a separate pull request we can :
update hard.yml and add the overflow verdict set to true (apart from retaining the reachability verdict set to false).
try to add a new benchmark with appropriate guards against the overflows with the reachability verdict set to true and overflow verdict set to false.