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

Optimize floats memset for zero initialization #1509

Merged
merged 5 commits into from Nov 18, 2023

Conversation

rafaelsamenezes
Copy link
Contributor

As shown in #1508 esbmc can't handle float memset properly as it breaks k-induction for some reason. This PR is just a workaround by enabling an extra simplification for the case of float f; memset(&f, 0, sizeof(float));

Copy link
Contributor

@lucasccordeiro lucasccordeiro left a comment

Choose a reason for hiding this comment

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

@rafaelsamenezes: could you also add a regression test that gives "VERIFICATION SUCCESSFUL"?

@rafaelsamenezes
Copy link
Contributor Author

Results (30s):

Statistics:          23805 Files
  correct:           14433
    correct true:     8013
    correct false:    6420
  incorrect:            64
    incorrect true:     14
    incorrect false:    50
  unknown:            9308
  Score:             21198 (max: 38482)

It solves a few extra cases.

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. @rafaelsamenezes are these numbers for svcomp main branch or svcomp23 or which ones? Could you add the link?

@fbrausse fbrausse mentioned this pull request Nov 18, 2023
47 tasks
@lucasccordeiro lucasccordeiro merged commit 5705d5c into master Nov 18, 2023
9 checks passed
@lucasccordeiro lucasccordeiro deleted the zero-float-memset branch November 18, 2023 21:02
@lucasccordeiro
Copy link
Contributor

Thanks for submitting this PR, @rafaelsamenezes.

@fbrausse fbrausse restored the zero-float-memset branch November 19, 2023 08:18
@fbrausse fbrausse deleted the zero-float-memset branch November 19, 2023 08:18
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.

None yet

3 participants