Skip to content

Simplify byte-extract from struct or union expressions #5873

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
merged 1 commit into from
May 13, 2021

Conversation

tautschnig
Copy link
Collaborator

With rewrite_union introducing rewriting union accesses to byte-extract
operations, simplifying such expressions must cover as many cases as
possible. Constants were mostly already being rewritten via expr2bits,
but that wouldn't be able to handle expressions involving pointers (even
when they are effectively constants when using address-of operations).
The additional simplification rules mimic what lower_byte_extract
already did at a later stage, but such late rewrites would not benefit
constant propagation done by goto-symex.

  • 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).
  • 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.

@tautschnig tautschnig changed the title Simplify byteyextract from struct or union expressions Simplify byte-extract from struct or union expressions Feb 27, 2021
@tautschnig tautschnig force-pushed the simplify-byte-extract branch from c0f4668 to a6f29ba Compare February 27, 2021 01:54
@codecov
Copy link

codecov bot commented Feb 27, 2021

Codecov Report

Merging #5873 (6544f7c) into develop (dd36155) will increase coverage by 0.20%.
The diff coverage is 92.30%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5873      +/-   ##
===========================================
+ Coverage    75.33%   75.53%   +0.20%     
===========================================
  Files         1447     1447              
  Lines       157988   158116     +128     
===========================================
+ Hits        119013   119437     +424     
+ Misses       38975    38679     -296     
Impacted Files Coverage Δ
src/ansi-c/c_typecheck_base.h 100.00% <ø> (+13.33%) ⬆️
src/goto-checker/symex_coverage.cpp 95.76% <ø> (ø)
src/goto-instrument/code_contracts.h 94.11% <ø> (ø)
src/goto-programs/goto_inline_class.cpp 84.09% <ø> (-0.09%) ⬇️
src/ansi-c/c_typecheck_expr.cpp 74.89% <81.25%> (+13.49%) ⬆️
src/util/simplify_expr.cpp 85.07% <88.88%> (+0.58%) ⬆️
src/util/pointer_offset_size.cpp 86.94% <91.66%> (+0.15%) ⬆️
src/goto-instrument/code_contracts.cpp 85.31% <95.45%> (+0.56%) ⬆️
src/ansi-c/c_expr.h 100.00% <100.00%> (ø)
src/ansi-c/c_typecheck_base.cpp 78.29% <100.00%> (+22.37%) ⬆️
... and 40 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update e9b5f5c...6544f7c. Read the comment docs.

Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

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

This feels like the kind of thing that could have or acquire subtle bugs. Would it be possible to add a test case or two? It feels like 100% patch coverage is possible and might be worth having.

@tautschnig tautschnig force-pushed the simplify-byte-extract branch from a6f29ba to faa02d4 Compare March 1, 2021 13:05
@tautschnig
Copy link
Collaborator Author

This feels like the kind of thing that could have or acquire subtle bugs. Would it be possible to add a test case or two? It feels like 100% patch coverage is possible and might be worth having.

Indeed, test added.

@martin-cs
Copy link
Collaborator

Thanks.

@tautschnig tautschnig force-pushed the simplify-byte-extract branch from faa02d4 to 971178b Compare March 1, 2021 16:39
@tautschnig tautschnig force-pushed the simplify-byte-extract branch from 971178b to b3985eb Compare March 1, 2021 16:40
@tautschnig tautschnig force-pushed the simplify-byte-extract branch from b3985eb to c412a6b Compare March 30, 2021 15:46
@tautschnig tautschnig force-pushed the simplify-byte-extract branch from c412a6b to 033835a Compare May 7, 2021 06:34
@tautschnig tautschnig self-assigned this May 11, 2021
@tautschnig tautschnig force-pushed the simplify-byte-extract branch from 033835a to 1270713 Compare May 13, 2021 20:24
With rewrite_union rewriting union accesses to byte-extract operations,
simplifying such expressions must cover as many cases as possible.
Constants were mostly already being rewritten via expr2bits, but that
wouldn't be able to handle expressions involving pointers (even when
they are effectively constants when using address-of operations).  The
additional simplification rules mimic what lower_byte_extract already
did at a later stage, but such late rewrites would not benefit constant
propagation done by goto-symex.
@tautschnig tautschnig force-pushed the simplify-byte-extract branch from 1270713 to 6544f7c Compare May 13, 2021 20:58
@tautschnig tautschnig merged commit 5239c68 into diffblue:develop May 13, 2021
@tautschnig tautschnig deleted the simplify-byte-extract branch May 13, 2021 22:59
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.

4 participants