Unsoundness of 64-bit floating point rounding #111
Comments
|
This only seems to affect Polyhedra. For Octagons I get the correct result: |
antoinemine
added a commit
that referenced
this issue
Jul 3, 2024
|
Hi. |
|
Thanks for the patch 👍 The issue I posted above seems to be fixed. However, rounding does not seem to round up to infinity. For example, The problem seems to be that polyhedra convert I refactored the test to test for these cases as well: import apron.*;
public class FloatingPointTest {
public static void main(String args[]) throws ApronException {
test(new Polka(true), 0.0, -6.561472834256157E307d);
test(new Polka(true), 1E308d, 1E308d);
test(new Polka(true), -1E308d, -1E308d);
test(new Polka(true), -Double.MAX_VALUE, -Double.MAX_VALUE);
}
public static void test(Manager manager, double x, double y) throws ApronException {
Abstract1 abs = new Abstract1(manager, new Environment());
double result = x + y;
System.out.printf("Test (%s): %e + %e = %e\n", manager.getClass().getSimpleName(), x, y, result);
contains("double rnd", manager, abs.getBound(manager, add(new DoubleScalar(x), new DoubleScalar(y), Texpr1Node.RTYPE_DOUBLE, Texpr1Node.RDIR_RND)), result);
System.out.println();
}
public static void contains(String message, Manager manager, Interval iv, double result) {
if(new Interval(new DoubleScalar(result), new DoubleScalar(result)).isLeq(iv)) {
System.out.printf("Test Succeeded (%s): %s contains %e\n", message, iv, result);
} else {
System.out.printf("Test Failed (%s): %s does not contain %e\n", message, iv, result);
}
}
public static Texpr1Intern add(Coeff x, Coeff y, int rtype, int rdir) {
return new Texpr1Intern(new Environment(),
new Texpr1BinNode(
Texpr1BinNode.OP_ADD,
rtype,
rdir,
new Texpr1CstNode(x),
new Texpr1CstNode(y)));
}
}Output: |
|
Actually, Apron does not track overflows, underflows and NaN in its floating-point semantics of the analyzed programs. In order to detect floating-point errors, tools (such as MOPSA) add additional checks for overflows and divisions by zero on the invariants output by polyhedra, and they maintain separate flags for possible infinities and NaN. |
|
Makes sense, same as for integer variables. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Hi Antoine,
Thanks for maintaining this library 👍
I get some weird behavior when rounding numbers to double-precision. For example,
0 + -6.561472834256157E307results in[-132...784,-oo]. I would expect[-6.561472834256157E307, -6.561472834256157E307]since -6.561472834256157E307 is a valid IEEE 64-bit floating point number and does not need to get rounded.I tried different rounding modes, but the result is the same.
Here is a Java program that reproduces this behavior:
Output:
The text was updated successfully, but these errors were encountered: