[Issue with benchmark] loop-floats-scientific-comp/loop4_true-unreach-call.c verdict

[animeshbchowdhury]

Hi,

I am getting a counterexample for which __VERIFIER_error is reachable in the program loop-floats-scientific-comp/loop4_true-unreach-call.c. The violation witness is also validated by CPAchecker.

Is anyone else facing the same issue ?

Regards, Animesh Basak Chowdhury

loop4_true-unreach-call.zip

[kfriedberger]

CPAchecker cannot handle SIN and COS and simply ignores these functioncalls (when used as validator). Thus I would not trust CPAchecker as a validator for this task. :-)

@animeshbchowdhury Your witness is quite sparse. Could you give more information about the found counterexample? Values for x and temp would be very helpful.

[animeshbchowdhury]

Values of x = 36 and temp = 0. Even with simple gcc compilation with flag -lm, __VERIFIER_error is reachable.

[animeshbchowdhury]

Basically what I understand from the knowledge of trigonometric transformations , here angleInRadian should be in range of (-pi,pi). Now, sin(angleInRadian + 2pi) is simply equals to sin(angleInRadian). Similarly, cos(angleInRadian + pi/2) equals - sin(angleInRadian). Now, when angleInRadian is pi/2, i.e. x = 90, then sum2 = sin(pi/2) = 1, and sum1 = -sin(pi/2) = -1. Difference of sum2 and sum1 = 2, but count would be equals to 1, which violates the assertion. I can say the benchmark is really false, unless assert is modified as __VERIFIER_assert(diff(sum2,sum1) <= 2count)

[animeshbchowdhury]

Also, looks like the logic written in comment section is not matching the implementation too. The Author says sin(x+2pi) and cos(x+pi) are in same phase, which is correct. However, in calculation of sum1, cos(angleInRadian+phaseLag) has been written. If it had been sum1 = sum1 + cos(angleInRadian+phaseLead), the benchmark would have been true. @tautschnig Let me know, if this explanation is okay.

[tautschnig]

@animeshbchowdhury I'm not sure why it would be my call, but I certainly do appreciate all your work on this! I think we just need a pull request relabelling the benchmark.

[zvonimir]

Coming back to this. As far as I know, trigonometric functions are not specified in the IEEE floating-point standard, and libraries choose to implement them differently, meaing that different implementations in various standard C libraries (e.g., GNU C, LLVM, Intel) might produce different floating-point errors. So what are we supposed to assume about sin and cos in this example? Are we supposed to take some particular implementation as "standard"?

[animeshbchowdhury]

I think there is a need to raise the issue which @zvonimir has mentioned amongst SVCOMP jury members to come to a unanimous decision.

I have taken GNU C implementation of sin and cos, but again there can be different implementations of such functions in other standard C libraries.

[PhilippWendler]

We should use the GNU C implementation if no standard semantics are defined. The README also mentions GNU C.

[animeshbchowdhury]

Thanks @PhilippWendler . Created a PR #708 to appropriately label the benchmark as false.

[zvonimir]

The implementation in GNU C is system-dependent. I presume it uses inlined assembly and such, which varies depending on for which processor the code is compiled. So could someone point me exactly to the implementation we should assume for sin and cos? Otherwise, I don't see how we can label this benchmark as true or false.

[peterschrammel]

As @zvonimir is poining out GNU libm is platform dependent: https://www.gnu.org/software/libc/manual/html_node/Errors-in-Math-Functions.html#Errors-in-Math-Functions

Alternatives are:

• fdlibm: https://www.netlib.org/fdlibm/readme, also used by the JDK
• openlibm: https://github.com/JuliaMath/openlibm, which claims to be platform independent
• crlibm: https://www.swmath.org/software/12390, which claims to be proven to round results correctly

[tautschnig]

Isn't the specific benchmark false for any implementation? As discussed elsewhere, it might be best to exclude benchmarks using trigonometric functions. For the particular benchmark in question, however, it seems irrelevant even?

[zvonimir]

I don't think that's true of any implementation, since maybe you could have weird implementations of sin and cos that do not obey any of the rules we might expect of them. It might be true of any reasonable implementation I guess. When I read what the documentation says for e.g. sin it is just "implements sin function" but nothing is said about floating-point errors. That to me means that even a dumb implementation that generates really large errors so that results are basically total nonsense also obeys the documentation.

[zvonimir]

Oh, and now the discussion is split between the mailing list and github. We should probably pick one and stick with it.