Float constant propagation is unsound

[peterschrammel]

It does not seem to take into account the rounding mode.
Patch #349 turns it off until this gets fixed.

The problem can be reproduced as follows on this benchmark
https://raw.githubusercontent.com/sosy-lab/sv-benchmarks/master/c/floats-cbmc-regression/float-rounding1_true-unreach-call.i

goto-cc/goto-cc sv-benchmarks/c/floats-cbmc-regression/float-rounding1_true-unreach-call.i -o test.o
goto-instrument/goto-instrument test.o test.o-cp --constant-propagator --inline --add-library
cbmc/cbmc test.o-cp

** Results:
[roundingTest.assertion.1] : SUCCESS
[roundingTest.assertion.2] : FAILURE
[roundingTest.assertion.3] : SUCCESS
[roundingTest.assertion.4] : SUCCESS

vs (after turning it off)

** Results:
[roundingTest.assertion.1] : SUCCESS
[roundingTest.assertion.2] : SUCCESS
[roundingTest.assertion.3] : SUCCESS
[roundingTest.assertion.4] : SUCCESS

[martin-cs]

On Sun, 2016-12-11 at 15:08 -0800, Peter Schrammel wrote: It does not seem to take into account the rounding mode. Patch #349 turns it off until this gets fixed. The problem can be reproduced as follows on this benchmark https://raw.githubusercontent.com/sosy-lab/sv-benchmarks/master/c/floats-cbmc-regression/float-rounding1_true-unreach-call.i goto-cc/goto-cc sv-benchmarks/c/floats-cbmc-regression/float-rounding1_true-unreach-call.i -o test.o goto-instrument/goto-instrument test.o test.o-cp --constant-propagator --inline --add-library cbmc/cbmc test.o-cp ** Results: [roundingTest.assertion.1] : SUCCESS [roundingTest.assertion.2] : FAILURE [roundingTest.assertion.3] : SUCCESS [roundingTest.assertion.4] : SUCCESS vs (after turning it off) ** Results: [roundingTest.assertion.1] : SUCCESS [roundingTest.assertion.2] : SUCCESS [roundingTest.assertion.3] : SUCCESS [roundingTest.assertion.4] : SUCCESS

A couple of things; 1. The constant propagator is unsound at the moment for a number of reasons. We are working on fixing it. 2. C does allow evaluation of some floating-point numbers at "compile" time / statically. I'll try to hunt these down. One recent extension we put in was to allow: int array [3.0f / 1.0f]; Please check that this continues to work. 3. There are also a number of cases in which the rounding mode does not matter so they can be evaluated. Off the top of my head I think evaluating with round to positive and round to negative and only returning a result if you get the same from both should be sufficient. HTH Cheers, - Martin

[kroening]

This should be fixed in the constant propagator, not in the simplifier.

The simplifier works on a first-order fragment, where there is no such thing as a rounding mode.

[peterschrammel]

Got it.

[martin-cs]

Do you want to assign this one to me? I've no idea when I'll be able to deal with it but it would at least keep track of it and it's on a system I'm working on / responsible for.

[thomasspriggs]

I have just been checking over this issue, as a review of old issues. It looks like this is still a problem as I can still reproduce the failure. The original link in this issue seems to be broken, but I think the example can still be found here - https://github.com/sosy-lab/sv-benchmarks/blob/master/c/floats-cbmc-regression/float-rounding1.i

[thomasspriggs]

@martin-cs I have assigned this to you, as you had volunteered and the issue was unassigned.