Skip to content

Improvements to duplicate_per_byte to simplify the input value #7887

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

Merged

Conversation

esteffin
Copy link
Contributor

The function duplicate_per_byte contains an efficient implementation when init_expr is a constant.

However this feature is never used as the shadow memory module almost always wraps init_expr with a typecast to the type of the shadow memory.

This PR applies a simplification step in duplicate_per_byte, calling simplify_expr, so that the casts may be removed and the more efficient implementation will be used.

This PR also adds unit tests to make sure the simplification step is performed.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • 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).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

Enrico Steffinlongo added 2 commits September 12, 2023 15:37
The function `duplicate_per_byte` contains a more efficient implementation
when `init_expr` is a constant.
However this feature is never used as the shadow memory module almost
always wraps `init_expr` with a typecast to the type of the shadow
memory.

This commit applies a simplification step in `duplicate_per_byte`,
calling `simplify_expr`, so that the casts may be removed and the more
efficient implementation will be used.
@codecov
Copy link

codecov bot commented Sep 12, 2023

Codecov Report

Patch coverage: 91.07% and project coverage change: -0.05% ⚠️

Comparison is base (f2fd9c6) 79.00% compared to head (1756460) 78.96%.
Report is 4 commits behind head on develop.

Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #7887      +/-   ##
===========================================
- Coverage    79.00%   78.96%   -0.05%     
===========================================
  Files         1696     1696              
  Lines       195105   195126      +21     
===========================================
- Hits        154143   154077      -66     
- Misses       40962    41049      +87     
Files Changed Coverage Δ
src/util/expr_initializer.cpp 83.96% <70.00%> (+0.15%) ⬆️
unit/util/expr_initializer.cpp 99.74% <95.65%> (-0.13%) ⬇️

... and 11 files with indirect coverage changes

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

@esteffin esteffin merged commit 4b31aee into diffblue:develop Sep 13, 2023
@esteffin esteffin deleted the esteffin/duplicate-per-byte-improvements branch September 13, 2023 13:16
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.

3 participants