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

Support for context-aware intervals #1564

Merged
merged 15 commits into from Jan 19, 2024
Merged

Support for context-aware intervals #1564

merged 15 commits into from Jan 19, 2024

Conversation

rafaelsamenezes
Copy link
Contributor

@rafaelsamenezes rafaelsamenezes commented Dec 31, 2023

This PR enables the abstract domain to have more information about the context where it is invoked. Specifically, this enables:

  1. Global variables
  2. Reasoning about functions calls: parameters and return values.
  3. Disables the interval analysis unit tests due to Goto generation in unit test is not initializing the namespace correctly #1567 (solved by PR migrate_namespace_lookup now managed by language_uit #1568)

@rafaelsamenezes
Copy link
Contributor Author

rafaelsamenezes commented Jan 1, 2024

Master

Statistics:          23805 Files
  correct:           15016
    correct true:     8444
    correct false:    6572
  incorrect:            50
    incorrect true:     17
    incorrect false:    33
  unknown:            8739
  Score:             22388 (max: 38482)

PR

Statistics:          23805 Files
  correct:           15127
    correct true:     8555
    correct false:    6572
  incorrect:            49
    incorrect true:     18
    incorrect false:    31
  unknown:            8629
  Score:             22610 (max: 38482)

@rafaelsamenezes rafaelsamenezes marked this pull request as ready for review January 1, 2024 17:53
@rafaelsamenezes rafaelsamenezes force-pushed the global-intervals branch 2 times, most recently from 4f8b2ba to a425172 Compare January 2, 2024 10:56
Copy link
Member

@fbrausse fbrausse left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In general LGTM, just a few comments.

Copy link
Member

@fbrausse fbrausse left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

@lucasccordeiro
Copy link
Contributor

@rafaelsamenezes: could you please fix the CI issues here?

@rafaelsamenezes
Copy link
Contributor Author

I changed the failing test case. It seems that the issue is related to using a function pointer. The function ptr is making the abstract interpreter confused about where is the next instruction, resulting in a bottom.

I also added the original test case as a knownbug. It seems to be related to having the function ptr call at the end of a block.

@rafaelsamenezes rafaelsamenezes merged commit 8411580 into master Jan 19, 2024
10 checks passed
@rafaelsamenezes rafaelsamenezes deleted the global-intervals branch January 19, 2024 14:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants