Skip to content

prophecy_r_or_w_ok_exprt lowering: adjust for dynamic/static objects #8629

New issue

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

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

Already on GitHub? # to your account

Closed
wants to merge 1 commit into from

Conversation

tautschnig
Copy link
Collaborator

We do not need to create comparisons to dead and/or deallocated when handling a dynamic object (which will never be marked "dead") or a static object (which will neither be marked "dead" nor "deallocated"). This avoids unnecessary branches when the prophecy_r_or_w_ok_exprt can now be simplified to a constant.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

We do not need to create comparisons to dead and/or deallocated when
handling a dynamic object (which will never be marked "dead") or a
static object (which will neither be marked "dead" nor "deallocated").
This avoids unnecessary branches when the prophecy_r_or_w_ok_exprt can
now be simplified to a constant.
Copy link

codecov bot commented Apr 16, 2025

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 80.37%. Comparing base (5dc709d) to head (9587978).
Report is 10 commits behind head on develop.

Additional details and impacted files
@@           Coverage Diff            @@
##           develop    #8629   +/-   ##
========================================
  Coverage    80.37%   80.37%           
========================================
  Files         1686     1686           
  Lines       206872   206896   +24     
  Branches        73       73           
========================================
+ Hits        166265   166288   +23     
- Misses       40607    40608    +1     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@remi-delmas-3000
Copy link
Collaborator

remi-delmas-3000 commented Apr 16, 2025

@tautschnig Will this change play nicely with objects created by __builtin_alloca ?

#include <stddef.h>
#include <assert.h>
void* allocate_on_stack(size_t size) {
    void* ptr = __builtin_alloca(size);
    return ptr;
}

void main() {
    size_t size;
    __CPROVER_assume(0 < size 0 && size <= 1000);    
    unsigned char* ptr = (unsigned char*)allocate_on_stack(size);
    assert(__CPROVER_r_ok(ptr)); // expect FAILURE
}

@kroening
Copy link
Member

The simplifier doesn't already do that with the lowered expression?

@tautschnig
Copy link
Collaborator Author

The simplifier doesn't already do that with the lowered expression?

No, simplify_inequality_pointer_object does not go that far, but maybe that's the better way to implement this. Will do instead.

@tautschnig
Copy link
Collaborator Author

@tautschnig Will this change play nicely with objects created by __builtin_alloca ?

Good call-out - I am now contemplating a very different implementation that will defer these kinds of simplifications to symex.

@tautschnig tautschnig self-assigned this Apr 22, 2025
@tautschnig
Copy link
Collaborator Author

Closing as this will be more properly addressed through #8642.

@tautschnig tautschnig closed this May 28, 2025
@tautschnig tautschnig deleted the simp-r_ok branch May 28, 2025 11:13
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants