Joining operation throws overflow exception for small coefficients/dimensions

[yiyunliu]

Hi, The code here joins two 6-dimension boxes. For each dimension, the width is no more than 100. Despite the coefficients, constants, dimensions being relatively small, ELINA throws overflow exception when joining is performed. Running gdb shows there indeed is an overflow, but what could possibly cause that?

Thanks, Yiyun

[GgnDpSngh]

Hi Yiyun,

The join operator tries to convert the constraint representation of polyhedron to the generator representation using the standard Chernikova algorithm. This algorithm involves multiplying coefficients in the constraints with each other multiple times. As a result, depending on the polyhedron, the coefficients can grow arbitrarily large starting from small coefficients (I have seen constraints with coefficients <=5 causing overflow).

Cheers, Gagan

[mwhicks1]

Hi Gagan.

Your answer seems to suggest that you think there's nothing to do. Even if the algorithm is "standard," isn't it a problem if its use can easily produce an overflow in the way you are using it?

A related question is: Would this situation come up in PPL, or is it specific to ELINA because of the conversion you are doing? If the latter, it seems that ELINA has a (potentially severe) limitation compared to PPL, despite ELINA's better performance.

What are your thoughts?

Thanks, -Mike

[GgnDpSngh]

Hi Mike,

Thanks for your question and comments. The overflow can happen during analysis with 64-bit integers for both ELINA and PPL. We note that since there is no canonical constraint or generator representation of Polyhedra, it can happen that depending on the representation ELINA detects an overflow but PPL does not and vice versa. There are two reasons for using 64-bit integers in ELINA:

1. The performance with arbitrary precision integers can be up to 4x slower.
2. In our experience, the Polyhedra widening gets rid of constraints with large coefficients.

Different libraries handle the overflow differently, e.g. APRON can enter an infinite loop (as discussed in the manual here ) while PPL requires certain assumptions for correctness that may not always hold (as discussed in the manual here: ).

In ELINA, we try to be conservative but sound by setting the affected Polyhedron to top in the case of an overflow. We leverage decomposition to minimize the loss of information by setting only the affected decomposed piece to Top (however, in the example above since there is only one decomposed piece, the result is Top). One could also try to just remove the constraint that causes overflow but combining this with decomposition is quite complicated.

On a side note, we are looking on adding support for analysis with arbitrary precision arithmetic which should ensure that there is no loss of precision due to overflow when using ELINA. Let me know if my response answers your query.

Cheers, Gagan

[jmct]

Hello again,

We're looking at this stuff again and I'm wondering if you can help us understand the line between where overflows are sound (i.e. where you can convert that decomposed piece to top) and where it is not sound (i.e. a coefficient itself is too large and overflows).

In particular we'd like to be able to silence any stderr warnings about overflow if they are sound (I'd make this a configuration flag, of course). I'd happily write this up as a pull-request if you point me in the right direction.

The way I'm seeing it now is that the overflow detection happens in opt_pk_vector.c at the functions like opt_int64_add and opt_int64_mult. These functions won't actually do the arithmetic if they detect an overflow and instead signal to their caller (opt_vector_combine that there was an overflow). The call graph goes up (through opt_matrix_combine_rows) to the functions in opt_pk_meetjoin.c where exceptions are checked.

However, I'm not seeing where it actually checks for ELINA_EXC_OVERFLOW, though it seems that it's the default(?) on line 276 of opt_pk_resize.c.

To be as concrete as possible:

• Is the flag set on 571 of opt_pk_vector.c always the sound version of overflow?
• If so, is silencing the printing of the exception acceptable as a flag or configuration option?

[GgnDpSngh]

Hi Jose,

The exceptions for ELINA are defined here: https://github.com/eth-sri/ELINA/blob/4fb9be047a29a41eaca21a5c7b08b7fd5e5264bf/elina_auxiliary/elina_manager.h#L125

We check for an exception by checking if opk->exn is not zero (both in the meetjoin and resize files). The flag at line 571 sets opk->exn to a non zero value. I can add an option for silencing the printing shortly and let you know when it is added (alternatively, feel free to send a pull request in case if you already implemented this feature).

Cheers, Gagandeep Singh

[jmct]

I'm happy to make a pull-request.

Just so that I'm super clear:

• Is the flag set on 571 of opt_pk_vector.c always sound overflow?

So silencing the warning won't mean we miss any warnings of unsoundness, correct?

[GgnDpSngh]

Hi Jose,

Thanks let me know when you have the request ready. Yes removing the printing of warning will have no effect on the soundness of the analysis as long as the flag is set before the print statement.

Cheers, Gagandeep Singh

[ezaffanella]

Hi Mike, [...] ) while PPL requires certain assumptions for correctness that may not always hold (as discussed in the manual here: ).

Hello.

I just noted this (old) comment and I would like to correct what seems to be a misunderstanding regarding PPL.

That part of the PPL manual is not referring to overflows occurring inside the PPL library; rather it is referring to how the library can approximate the behaviors of overflows in the concrete semantics of the analyzed program.

For the PPL library computations, things are meant to be simpler:

• if PPL is configured to use unbounded integers, the library computations will not overflow;
• otherwise, if it is configured to used checked machine integers, the library will detect all overflows and throw an exception.

Cheers, Enea Zaffanella.