Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add ./configure option to suppress overflow warnings #52

Merged
merged 1 commit into from
Oct 1, 2019

Conversation

jmct
Copy link
Contributor

@jmct jmct commented Oct 1, 2019

This addresses part of the concerns in issue #39. Namely, if we know the
overflow is sound, then we can choose to skip printing to stderr when the
sound overflow occurs.

The implementation is straightforward:

  • We added an option to ./configure: -no-warn-overflow

  • When enabled, this adds -DNO_WARN_OVERFLOW to extra_elina_options

  • The printing to stderr in elina_poly/opt_pk/vector.c:570 is now under
    a CPP macro that checks whether -DNO_WARN_OVERFLOW is defined.

This addresses part of the concerns in issue eth-sri#39. If we know
the overflow is sound, then we can choose to skip printing
to `stderr` when the sound overflow occurs.

The implementation is straightforward:

* We added an option to `./configure`: `-no-warn-overflow`

* When enabled, this adds `-DNO_WARN_OVERFLOW` to `extra_elina_options`

* The printing to `stderr` in `elina_poly/opt_pk/vector.c:570` is now under
  a CPP macro that checks whether `-DNO_WARN_OVERFLOW` is defined.
@jmct
Copy link
Contributor Author

jmct commented Oct 1, 2019

One thing that I'm not sure about is whether all the occurrences of ELINA_EXC_OVERFLOW are sound in the same way.

@GgnDpSngh GgnDpSngh merged commit 7147092 into eth-sri:master Oct 1, 2019
@GgnDpSngh
Copy link
Contributor

Hi Jose,

Thanks for the update. Whenever there is an overflow our implementation tries to handle it in a sound way by setting the exception flag. This is detected in the calling method which sets the corresponding polyhedron to Top.

There has been recent work (https://dl.acm.org/citation.cfm?doid=3238147.3240464) that tested ELINA's soundness guarantees on challenging inputs. Many of these inputs generate test cases where one observes overflows and helped us fix issues. Ofcourse, there can be control paths that we may have missed and if you observe any unsoundness, let me know.

Cheers,
Gagandeep Singh

cwright7101 pushed a commit to cwright7101/ELINA that referenced this pull request Nov 12, 2020
Add ./configure option to suppress overflow warnings
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants