Infinity floating-point values in Octagons

[svenkeidel]

Hi Antione,

Is there a way to represent infinite floating point values in Octagons?

Currently, octagons yield bottom on infinity values:

import apron.*;

public class OctagonTest {
    public static void main(String args[]) throws ApronException {
                Manager manager = new apron.Octagon();
        Environment env = new Environment(new String[]{}, new String[]{"x"});
        Abstract1 abstract1 = new Abstract1(manager, env);
        abstract1.assign(manager, "x", new Texpr1Intern(env, new Texpr1CstNode(new DoubleScalar(Double.POSITIVE_INFINITY))), null);

        // prints <empty>
        System.out.println(abstract1);

        // prints [1.0, -1.0]
        System.out.println(abstract1.getBound(manager, new Texpr1Intern(env, new Texpr1VarNode("x"))));
    }
}

This is unsound.

Best, Sven

[antoinemine]

Hi, No this is not possible. The numeric domains in Apron only abstract the non-special values of floating-point numbers. Hence, a set reduced to the float +oo is considered as an empty set. As special values do not obey the traditional algebraic rules of reals, it is difficult to provide a meaning, and thus a sound abstraction, using relations (such as linear relations, as used by polyhedra and octagons). Apron only provides sound abstractions for mathematical integers and real arithmetics (enriched with the rounding operators of floats, considered as a subset of reals). This is really very similar to the discussion in #111. To handle special float values, e.g. to build a static analyzer, you'll have to treat them separately. This is what we do. e.g., in MOPSA https://gitlab.com/mopsa/mopsa-analyzer/-/blob/main/analyzer/languages/c/memory/machine_numbers.ml

[svenkeidel]

Yes, sorry for asking again. I was confused because the same program with polyhedra is sound and returns [-infinity, infinity]. So I thought apron would be handling infinity.